Ceaser.dfy

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)
{
}