Created
August 24, 2024 07:43
-
-
Save mukeshtiwari/7559210495b84ef69c7a8c420b0a1f82 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| function encode (plain : nat, key : nat) : (out : nat) | |
| requires 0 <= plain < 26 | |
| requires 0 <= key < 26 | |
| ensures 0 <= out < 26 | |
| ensures (plain + key >= 26) ==> out == plain + key - 26 | |
| ensures plain + key < 26 ==> out == plain + key | |
| { | |
| if plain + key >= 26 then | |
| plain + key - 26 | |
| else | |
| plain + key | |
| } | |
| function decode (cipher : nat, key : nat) : (out : nat) | |
| requires 0 <= cipher < 26 | |
| requires 0 <= key < 26 | |
| ensures 0 <= out < 26 | |
| ensures key > cipher ==> out == (cipher + 26) - key | |
| ensures key <= cipher ==> out == cipher - key | |
| { | |
| if key > cipher then | |
| (cipher + 26) - key | |
| else | |
| cipher - key | |
| } | |
| lemma idNat (p : nat, k : nat) returns (out : nat) | |
| requires 0 <= p < 26 | |
| requires 0 <= k < 26 | |
| ensures p == out | |
| { | |
| var tmp : nat := encode(p,k); | |
| out := decode (tmp,k); | |
| } | |
| type myChar = c : char | c in "abcdefghijklmnopqrstuvwxyz" witness 'a' | |
| function toNat (c: myChar) : (out: nat) | |
| requires 97 <= c as int < 123 | |
| ensures 0 <= out < 26 | |
| { c as int - 97} | |
| function toChar (n: nat) : (out: myChar ) | |
| requires 0 <= n < 26 | |
| ensures 97 <= out as int < 123 | |
| { (n + 97) as char} | |
| /* | |
| lemma idNatChar (p: nat) returns (out: nat) | |
| requires 0 <= p < 26 | |
| ensures 0 <= out < 26 | |
| ensures p == out | |
| { | |
| var tmp : myChar := toChar(p); | |
| assert 97 <= tmp as int < 123; | |
| out := toNat(tmp); | |
| assert 0 <= out < 26; | |
| } | |
| method idNatChar (p: nat) returns (out: nat) | |
| requires 0 <= p < 26 | |
| ensures 0 <= out < 26 | |
| ensures p == out | |
| { | |
| var tmp : myChar := (p + 97) as char; | |
| assert 97 <= tmp as int < 123; | |
| out := tmp as int - 97; | |
| assert 0 <= out < 26; | |
| } | |
| lemma idCharNat (p: myChar) returns (out: myChar) | |
| requires 97 <= p as int < 123 | |
| ensures 97 <= out as int < 123 | |
| ensures p == out | |
| { | |
| assert 97 <= p as int < 123; | |
| var p_nat : nat := toNat(p); | |
| assert 0 <= p_nat < 26; | |
| var c_char : myChar := toChar(p_nat); | |
| assert 97 <= c_char as int < 123; | |
| out := c_char; | |
| } | |
| */ | |
| function encode_c (plain : myChar, key : myChar) : (out : myChar) | |
| { | |
| var p : nat := toNat(plain); | |
| var k : nat := toNat(key); | |
| var tmp : nat := encode(p,k); | |
| toChar(tmp) | |
| } | |
| function decode_c (cipher: myChar, key: myChar) : (out: myChar) | |
| { | |
| var c: nat := toNat(cipher); | |
| assert 0 <= c < 26; | |
| var k: nat := toNat(key); | |
| var tmp: nat := decode(c,k); | |
| toChar(tmp) | |
| } | |
| lemma idChar (p_char: myChar, k_char: myChar) | |
| ensures p_char == decode_c(encode_c(p_char, k_char), k_char) | |
| { | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment