# Library Spec

forall b. exists t. b ~ t

A)

// ok ==> b ~ t
b, ok, t := receive()

x, ok := decrypt(key, message) // ok ==> x in B
if !ok { return }
//POSTCONDITION: exists k, p :: message ~ enc(k, p)

axiom {
  forall b: []byte :: b in B ==> exists t: Term :: b ~ t
}

NiceBytes = { b | exists t. b ~ t }



B1)

x, ok := decrypt(key, message)
if !ok { return }
//POSTCONDITION: forall k, p :: key ~ k && x ~ p ==> message ~ enc(k, p)
//TOTALITY: exists p :: x ~ p 
//ENTAILS: exists k, p :: message ~ enc(k, p)

axiom {
  forall b: []byte :: exists t: Term :: b ~ t      (t might be garbage)
}

// ok ==> forall x, y :: l ~ x && r ~ y ==> b ~ pair(x,y)
l, r, ok := unpair(b)




Criticel Term Axioms: 
  forall b in Bytes. p in CriticalTerms. t in GroundTerms.
    (exists \sigma. b ~ p\sigma) && b ~ t ==> (exists \sigma. t == p \sigma)



method example1()
{
  var b: ByteString; var t: Term
  b, ok, t := receive() // expect <x, h(x)>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := unpair(b)
  if (!ok) { goto end }

  var v: ByteString
  v := hash(l)

  ok := equals(v, r)
  if (!ok) { goto end }

  assert b ~ t && b ~ pair(x, h(x)) && l ~ x
  
  // by CriticalTerm Axiom:
  assert exists x2 :: t == pair(x2, h(x2)) && l ~ x
  
  { // with forall x', y' :: l ~ x' && r ~ y' <== b ~ pair(x',y') 
      we know b ~ t and t == pair(x2, h(x2)) for some x2
      thus l ~ x2
  }
  
  // goal: l ~ x2
}


ensures forall x, y :: l ~ x && r ~ y ==> b ~ pair(x,y)
func makePair(l, r []byte) (b []byte)

ensures ok ==> forall x, y :: l ~ x && r ~ y <==> b ~ pair(x,y) 
IGLOO: ensures ok ==> alpha(b) == pair(alpha(l), alpha(r))
func unpair(b byte[]) (l, r []byte, ok bool)


b := makePair(l,r)
l2, r2 := unpair(b)
assert l == l2 && r == r2


assume l ~ x && r ~ y 
b := makePair(l,r)
l2, r2 := unpair(b)
assert l2 ~ x && r2 ~ y 




ensures ok <==> len(b) == lsize + rsize
ensures ok  ==> len(l) == lsize && l == b[0:lsize]
ensures ok  ==> len(r) == rsize && r == b[lsize:rsize]
ensures ok  ==> forall x, y :: l ~ x && r ~ y ==> b ~ pair(x, y)

Variant 1)
  ensures ok  ==> forall x, y :: len(gamma(x)) == lsize && len(gamma(y)) == rsize && b ~ pair(x,y) ==> l ~ x && r ~ y
  
Variant 2)
  ensures ok  ==> forall x, y :: (exists u. u ~ x && len(u) == lsize) && (exists u. u ~ y && len(u) == rsize) && b ~ pair(x,y) ==> l ~ x && r ~ y
  
Variant 3)
  ensures ok  ==> forall x, y :: (forall u. u ~ x && len(u) == lsize) && (forall u. u ~ y && len(u) == rsize) && b ~ pair(x,y) ==> l ~ x && r ~ y

func split(b, lsize, rsize) (l, r, ok)



size(enc(k,x)) == 16 + size(x)
size(h(x)) == 18
size('n') == 4
size(<l,r>) == size(l) + size(r)

axiom {
  forall b, x, y :: b is Pair ==> Left(b) ~ x && Right(b) ~ y ==> b ~ pair(x,y)
  forall l, r :: Left(Pair(l,r)) == l && Right(Pair(l,r)) == r
}



ensures ok ==> forall t1, t2, t3, t4, t5 :: 
    x1 ~ t1 && ... && x5 ~ t5 <==> b ~ <'1', t1, t2, t3, t4, t5>
func unmarshal1(b) (x1, x2, x3, x4, x5, ok)

ensures ok ==> forall t1, t2, t3, t4 :: 
    x1 ~ t1 && ... && x4 ~ t4 <==> b ~ <'2', t1, t2, t3, t4>
func unmarshal2(b) (x1, x2, x3, x4, ok)

ensures ok ==> forall t1, t2, t3 :: 
    x1 ~ t1 && ... && x3 ~ t3 <==> b ~ <'4', t1, t2, t3>
func unmarshal3(b) (x1, x2, x3, ok)








ensures ok ==> forall k, p, m :: key ~ k ==> (pla ~ p <==> msg ~ m)
func decrypt(key, msg) (pla, ok)


ensures ok ==> forall x, y :: l ~ x && r ~ y <==> b ~ pair(x,y)







SDEC(key, SENC(key, msg)) == msg




// terms instantiating a pattern p:
//   Q_p = Inst(p) = { p\sigma | dom(\sigma) = vars(p) && \sigma ground }
// term-related bytestrings: 
//   B = {b | exists t. b ~ t} \subset Bytes   (no garbage term!)
// image of b under ~:
//   T(b) = {t | b ~ t}
// 
// Q-axiom:  b ~ t && b ~ u && u in Q_p ==> t in Q_p
//   equiv:  T(b) \subseteq Q_p || T(b) \subseteq Terms-Q_p
//   
// Totality: exists t. b ~ t       (Terms includes a special junk/garbage term)
//    equiv: T(b) != {}            (only needed in scenario B1)
// 
// term construction: b1 ~ t1 && ... && bn ~ tn ==> F(b1, ..., bn) ~ f(t1, ..., tn)
// (used in a form or another in the library specifications)
//
// b, t = recv()
// { b ~ t }  // scenario A 
// (res, b1, ..., bn) = parser(b, p(x1,..., xn))
// { b1, ..., bn in B }
// { exists t'. b ~ t' && t' in Q_p }
// { t in Q_p }      (by Q-axiom)

// Scenarios
// A.  only consider bytestrings in B (no junk term needed)
//     problem to solve: ~ not a function, i.e., potentially several correct interpretations
// B1. all of Bytes + junk constant + ~ total
// B2. all of Bytes, no junk constant, ~ not total, received b may contain junk bytestring bi
//     Problem: if bi is a junk byte string then b not in B!
//
// junk term: term with junk constant as subterm
// junk bytestring: b not in B


//////////////////////////////
////   Type Definitions   ////
//////////////////////////////

domain Term {
  function pair(l: Term, r: Term): Term
  function h(t: Term): Term
  function enc(k: Term, p: Term): Term
  function const(v: Int): Term
}

domain ByteString { 
  function len(b: ByteString): Int
}

domain Alpha {
  function consistent(b: ByteString, t: Term): Bool
}

domain Assumption {
  function Q(t: Term): Bool

  function firstVersionOfQAxiom(): Bool // used to toggle on the axiom

  axiom FirstVersionOfQAxiom {
    // forall t :: t in Q ==> forall b :: b ~ t ==> forall t':: b ~ t' ==> t' == t
    firstVersionOfQAxiom() ==> forall t: Term, b: ByteString, t2: Term :: {Q(t), consistent(b, t), consistent(b, t2)} 
      Q(t) && consistent(b, t) && consistent(b, t2) ==> t == t2
  }

  axiom SecondVersionOfQAxiom {
    // forall p in Q, b. (exists sigma :: b ~ p sigma) ==> forall t. b ~ t ==> exists sigma :: t == p sigma
    true 
    // Not straightforwardly expressible in Viper due to the substitutions.
    // Instead, we instantiate the axiom for each p in Q to simplify the axiom and remove the substitutions.

    // Example for p == <x, h(x)>
    // forall b, x :: b ~ <x, h(x)> ==> forall t :: b ~ t ==> exists x' :: t == <x', h(x')> 
  }
}


//////////////////////////////
////       Utility        ////
//////////////////////////////

method equals(l: ByteString, r: ByteString) returns (ok: Bool)
  ensures ok ==> l == r

method receive() returns (b: ByteString, ok: Bool, /* ghost */ t: Term)
  ensures ok ==> consistent(b, t)



//////////////////////////////
////       Library        ////
//////////////////////////////

// ensures forall t :: b ~ t ==> v ~ h(t)
method hash(b: ByteString) returns (v: ByteString) 
  ensures forall t: Term :: {consistent(b, t)} consistent(b, t) ==> consistent(v, h(t)) 

// ensures ok ==> l ~ x && r ~ y && forall x', y' :: l ~ x' && r ~ y' ==> b ~ <x',y'>
method parse1(b: ByteString) returns (l: ByteString, r: ByteString, ok: Bool, /* ghost */ x: Term, y: Term)
  ensures  ok ==> len(l) == 32 && len(r) == 32
  ensures  ok ==> (
    consistent(l, x) && consistent(r, y) &&
    forall x2: Term, y2: Term :: {consistent(l, x2), consistent(r, y2)} consistent(l, x2) && consistent(r, y2) ==> consistent(b, pair(x2,y2)) 
  )

// ensures ok ==> b ~ constant(v)
method parseConst(b: ByteString) returns (v: Int, ok: Bool)
  ensures ok ==> consistent(b, const(v)) 

// ensures b ~ constant(v)
method makeConst(v: Int) returns (b: ByteString)
  ensures consistent(b, const(v))

// ensures ok ==> forall k, p :: key ~ k && pla ~ p ==> cip ~ enc(k,p)
method encrypt(key: ByteString, pla: ByteString) returns (cip: ByteString, ok: Bool)
  ensures ok ==> forall k: Term, p: Term :: {consistent(key,k),consistent(pla,p)} 
    consistent(key,k) && consistent(pla,p) ==> consistent(cip,enc(k,p)) 

// ensures ok ==> forall k, m :: key ~ k && cip ~ m ==> (exists p :: pla ~ p) && (forall p :: pla ~ p ==> cip ~ enc(k,p))
method decryptVersion2(key: ByteString, cip: ByteString) returns (pla: ByteString, ok: Bool)
  ensures ok ==> forall k: Term, m: Term :: {consistent(key, k), consistent(cip, m)}
    consistent(key, k) && consistent(cip, m) ==> (
      (exists p: Term :: consistent(pla, p)) &&
      (forall p: Term :: {consistent(pla, p)} consistent(pla, p) ==> consistent(cip, enc(k, p)))
    )

// ensures ok ==> forall k, p :: key ~ k && pla ~ p ==> cip ~ enc(k,p)
method decryptVersion1(key: ByteString, cip: ByteString) returns (pla: ByteString, ok: Bool)
  ensures ok ==> forall k: Term, p: Term :: {consistent(key,k),consistent(pla,p)} 
    consistent(key,k) && consistent(pla,p) ==> consistent(cip,enc(k,p))



//////////////////////////////
////       Examples       ////
//////////////////////////////

// terms instantiating a pattern p:
//   Q_p = Inst(p) = { p\sigma | dom(\sigma) = vars(p) && \sigma ground }
// term-related bytestrings: 
//   B = {b | exists t. b ~ t} \subset Bytes   (no garbage term!)
// image of b under ~:
//   T(b) = {t | b ~ t}
// 
// Q-axiom:  b ~ t && b ~ u && u in Q_p ==> t in Q_p
//   equiv:  T(b) \subseteq Q_p || T(b) \subseteq Terms-Q_p

/*
// forall b in Bytes. forall p in CriticalTerm. forall t in GroundTerm.
//     (exists \sigma. b ~ p\sigma) && b ~ t ==> exists \sigma. t == p\sigma
  
b := receive() // expecting <x,h(x)>
// exists t. b ~ t && in(t)

ok, b' := perform_parsing(b)
// ok ==> exists x. b ~ <x, h(x)> && b' ~ x


// goal: in(t') \in soup with exists x. t' == <x,h(x)>
// continue with the protocol

*/


// Example 1 - <x, h(x)>

method code1() returns (res: Term, ok: Bool)
  /* With the first version of the axiom */
  // requires firstVersionOfQAxiom()
  // // forall t, b :: b ~ t && len(b) == 32 ==> <t, h(t)> in Q
  // requires forall t: Term, b: ByteString :: {consistent(b, t)} consistent(b, t) && len(b) == 32 ==> Q(pair(t, h(t)))
  /* With the second version of the axiom */
  // forall b, x :: b ~ <x, h(x)> ==> forall t :: b ~ t ==> exists x' :: t == <x',h(x')>
  requires forall b: ByteString, x: Term :: {consistent(b, pair(x, h(x)))} 
    consistent(b, pair(x, h(x))) ==> 
      forall t: Term :: {consistent(b, t)} consistent(b, t) ==> exists x2: Term :: t == pair(x2, h(x2))

  ensures ok ==> exists x: Term :: res == pair(x, h(x))
{
  var b: ByteString; var t: Term
  b, ok, t := receive() // expect <x, h(x)>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v: ByteString
  v := hash(l)

  ok := equals(v, r)
  if (!ok) { goto end }

  assert exists x2: Term :: t == pair(x2, h(x2))
  res := t

  label end
}



// Example 2 - <'4', h('17')>

method code2() // uses parseConst
  /* With the first version of the axiom */
  requires firstVersionOfQAxiom()
  // <'4', h('17')> in Q
  requires Q(pair(const(4), h(const(17))))
  /* The second version of the axiom is essentially the same for constant terms */
{
  var b: ByteString; var t: Term; var ok: Bool
  b, ok, t := receive() // expect <'4', h('17')>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v1: Int
  v1, ok := parseConst(l)
  if (!ok || v1 != 4) { goto end } 

  var v2: ByteString;
  v2 := makeConst(17)
  v2 := hash(v2)
  ok := equals(r, v2)
  if (!ok) { goto end }

  assert t == pair(const(4), h(const(17)))

  label end
}


method code3() // uses makeConst
  /* With the first version of the axiom */
  requires firstVersionOfQAxiom()
  // <'4', h('17')> in Q
  requires Q(pair(const(4), h(const(17))))
  /* The second version of the axiom is essentially the same for constant terms */
{
  var b: ByteString; var t: Term; var ok: Bool
  b, ok, t := receive() // expect <'4', h('17')>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v1: ByteString
  v1 := makeConst(4)
  ok := equals(l, v1)
  if (!ok) { goto end }

  var v2: ByteString;
  v2 := makeConst(17)
  v2 := hash(v2)
  ok := equals(r, v2)
  if (!ok) { goto end }

  assert t == pair(const(4), h(const(17)))

  label end
}

method code4() 
  /* With the first version of the axiom */
  // requires firstVersionOfQAxiom()
  // // forall t, b :: b ~ t && len(b) == 32 ==> <t, h('17')> in Q
  // requires forall t: Term, b: ByteString :: {consistent(b, t)} consistent(b, t) && len(b) == 32 ==> Q(pair(t, h(const(17))))
  /* With the second version of the axiom */
  // forall b, x :: b ~ <x, h(x)> ==> forall t :: b ~ t ==> exists x' :: t == <x',h('17')>
  requires forall b: ByteString, x: Term :: {consistent(b, pair(x, h(const(17))))} 
    consistent(b, pair(x, h(const(17)))) ==> 
      forall t: Term :: {consistent(b, t)} consistent(b, t) ==> exists x2: Term :: t == pair(x2, h(const(17)))
{
  var b: ByteString; var t: Term; var ok: Bool
  b, ok, t := receive() // expect <x, h('17')>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v2: ByteString;
  v2 := makeConst(17)
  v2 := hash(v2)
  ok := equals(r, v2)
  if (!ok) { goto end }

  assert exists x2: Term :: t == pair(x2, h(const(17)))

  label end
}


// Example 3 - <x, enc(k,x)>

method code5(bk: ByteString, k: Term) // uses encrypt
  // bk ~ k
  requires consistent(bk, k) 
  /* With the first version of the axiom */
  // requires firstVersionOfQAxiom()
  // // forall t, b :: b ~ t && len(b) == 32 ==> <t,enc(k, t)> in Q
  // requires forall t: Term, b: ByteString :: {consistent(b, t)} consistent(b, t) && len(b) == 32 ==> Q(pair(t, enc(k,t)))
  /* With the second version of the axiom */
  // forall b, x :: b ~ <x, enc(k,x)> ==> forall t :: b ~ t ==> exists x' :: t == <x',enc(k,x')>
  requires forall b: ByteString, x: Term :: {consistent(b, pair(x, enc(k, x)))} 
    consistent(b, pair(x, enc(k, x))) ==> 
      forall t: Term :: {consistent(b, t)} consistent(b, t) ==> exists x2: Term :: t == pair(x2, enc(k, x2))
{
  var b: ByteString; var ok: Bool; var t: Term
  b, ok, t := receive() // expect <x, enc(k,x)>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v: ByteString
  v, ok := encrypt(bk, l)
  if (!ok) { goto end }

  ok := equals(v, r)
  if (!ok) { goto end }

  assert exists x2: Term :: t == pair(x2, enc(k, x2))

  label end
}

method code6(bk: ByteString, k: Term) // uses decrypt
  // bk ~ k
  requires consistent(bk, k) 
  /* With the first version of the axiom */
  // requires firstVersionOfQAxiom()
  // // forall t, b :: b ~ t && len(b) == 32 ==> <t,enc(k, t)> in Q
  // requires forall t: Term, b: ByteString :: {consistent(b, t)} consistent(b, t) && len(b) == 32 ==> Q(pair(t, enc(k,t)))
  /* With the second version of the axiom */
  // forall b, x :: b ~ <x, enc(k,x)> ==> forall t :: b ~ t ==> exists x' :: t == <x',enc(k,x')>
  requires forall b: ByteString, x: Term :: {consistent(b, pair(x, enc(k, x)))} 
    consistent(b, pair(x, enc(k, x))) ==> 
      forall t: Term :: {consistent(b, t)} consistent(b, t) ==> exists x2: Term :: t == pair(x2, enc(k, x2))
{
  var b: ByteString; var ok: Bool; var t: Term
  b, ok, t := receive() // expect <x, enc(k,x)>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v: ByteString
  v, ok := decryptVersion2(bk, r) // both version work
  if (!ok) { goto end }

  ok := equals(v, l)
  if (!ok) { goto end }

  assert exists x2: Term :: t == pair(x2, enc(k, x2))

  label end
}















method example1()
{
  var b: ByteString; var t: Term
  b, ok, t := receive() // expect <x, h(x)>
  if (!ok) { goto end }

  var l: ByteString; var r: ByteString; var x: Term var y: Term
  l, r, ok, x, y := parse1(b)
  if (!ok) { goto end }

  var v: ByteString
  v := hash(l)

  ok := equals(v, r)
  if (!ok) { goto end }

  assert exists x. b ~ pair(x, h(x)) && l ~ x
 
  
  Q-Axiom:
  (exists x. b ~ <x, h(x)>) && b ~ t ==> exists x°. t == <x°, h(x°)> 
      && get1(b) ~ x° && get2(b) ~ h(x°)
  
  
  (exists \sigma. b ~ p\sigma) && b ~ t ==> 
         exist \sigma. t == \sigma 
      && forall position in Positions(p). position(b) ~ position(\sigma)
  
  <x,h(x)> --> left( . ) in Positions(<x,h(x)>)
  [left( . )] -> get1( . ) 
  
  // goal :: exists x2: Term :: t == pair(x2, h(x2)) && l ~ x2
  
  
  b ~ t /\ b ~ p\sigma /\ b_i ~ \sigma(x_i) for i=1,..,n
  ==> \exists \sigma'. t = p\sigma' /\ b_i ~ \sigma'(x_i) for i=1,..,n
}