ok ==>
  forall k, m:Term :: key ~ k && cip ~ m
  ==> (exists p:Term :: pla ~ p) &&
    (forall p':: pla ~ p' ==> cip ~ enc(p',k)))

// version 1
ensures forall t :: b ~ t ==> res ~ h(t) 
    && h(t) in Q ==> forall t° :: res ~ t° ==> t° == h(t)
func hash(b []byte) (res []byte)

// version 2
ensures forall t :: b ~ t ==> res ~ h(t) && forall t° :: res ~ t° ==> t° == h(t)
func hash(b []byte) (res []byte)

// version 3
ensures (forall t :: b ~ t ==> res ~ h(t))
ensures
 forall t ::
 (b ~ t && forall t' :: b ~ t' ==> t = t')
 ==> (forall   t'' :: res ~ t'' ==> t'' == h(t))
func hash(b []byte) (res []byte)

// example: expects <x, h(x)>
Q = forall t' :: pair(t', h(t'))

b, t, ok := receive()
if !ok { return }
assert b ~ t

l, r, ok, x, y := parsePair(b)
if !ok { return }
assert l ~ x && r ~ y
assert forall x' y' :: (l ~ x' && r ~ y' && pair(x',y') in Q) ==> b ~ pair(x',y'))


v := hash(l)
assert forall t° :: l ~ t° ==> v ~ h(t°) 
assert forall t° :: unique l ~ t° ==> unique v ~ h(t°) 
if r != v { return }
assert forall t° :: l ~ t° ==> r ~ h(t°) 
assert r ~ h(x) 
assert forall t° :: unique l ~ t° ==> unique r ~ h(t°) 

assert l ~ x && r ~ h(x) 
assert b ~ pair(x, h(x))

assert "parsing of b was successful"
         =/= exists t'. b ~ pair(t', h(t'))


assert assert y == h(x)

assert exists t'. pair(x,y) = pair(t', h(t'))

assert exists t'. b ~ pair(t', h(t'))

goal: assert exists t'. t == pair(t', h(t'))

required b ~ t
func alpha(t Term, b ByteString): Term = t

func gamma(t Term): Set[ByteString]
b ~ t <==> b in gamma(t)

forall t° in Q, t, b :: b ~ t° && b ~ t ==> t == t°


// Library

ensures ok ==> b ~ t
func receive() (b ByteString, ghost t Term, ok bool)

ensures forall t Term :: b ~ t  ==> v ~ h(t)
func hash(b ByteString) (v ByteString)

ensures ok ==> forall x, y Term :: l ~ x && r ~ y ==> b ~ pair(x,y)
ensures ok ==> forall t Term :: 
  b ~ t ==> exists x y Term :: t == pair(x,y) && l ~ x && r ~ y
func parsePair(b ByteString) (l, r ByteString, ok bool)


Assumption: forall t° in Q, t, b :: b ~ t° && b ~ t ==> t == t°
Assumption: forall t :: ( exists x, b :: x ~ b && len(b) == 32 && t == pair(x, h(x)) ) ==> t in Q

// example: expects <x, h(x)>

b, t, ok := receive()
if !ok { return }
assert b ~ t

l, r, ok := parsePair(b)
if !ok { return }
assert forall x, y :: l ~ x && r ~ y ==> b ~ pair(x,y)

v := hash(l)
assert forall t° :: l ~ t° ==> v ~ h(t°) 
if r != v { return }
assert forall t° :: l ~ t° ==> r ~ h(t°)

assert forall x :: l ~ x ==> b ~ pair(x,h(x))

assert forall x :: l ~ x ==> t == pair(x, h(x))

// exists x. t == pair(x, hash(x))



// example 2

Assumption: forall t :: (exists x, b :: x ~ b && t == h(x) ) ==> t in Q

ensures forall t :: b ~ t ==> res ~ h(t) 
    && h(t) in Q ==> forall t° :: res ~ t° ==> t° == h(t)
func hash(b []byte) (res []byte)

ensures b ~ t && t in Q ==> res ~ h(t) && 
    (h(t) in Q ==> forall t° :: res ~ t° ==> t° == h(t))
func hash(b []byte, t Term) (res []byte)


forall b []byte, t Term ::
(b ~ t && t in Q) ==>
(forall t2 Term :: b ~ t2 ==> t == t2)


ensures ok ==> 
func parsePair(b []byte, t Term) (l, r []byte, x, y Term, ok bool)

ensures ok ==> 
    forall b ~ t ==>
    exists x, y :: (l ~ x && r ~ y ==> pair(x,y) in Q) ==>
      l ~ x && r ~ y && 
             t == pair(x,y)
ensures ok ==> 
  forall t :: b ~ t ==>
  (exists x, y ::
    l ~ x && r ~ y &&
    (pair(x,y) in Q ==> t == pair(x,y))         
func parsePair(b []byte) (l, r []byte, ok bool)

// example: expect <x, h(x)>

b, t, ok := receive()
if !ok { return }
assert b ~ t

l, r, x, y, ok := parsePair(b)
if !ok { return }
assert l ~ x && r ~ y
assert (pair(x, y) in Q ==> t == pair(x,y))

v := hash(l)
assert v ~ h(x) 
if r != v { return }
assert r ~ h(x)

assert l ~ x && r ~ h(x) && r ~ y
assert y == h(x)
assert pair(x, y) == pair(x, h(x)) in Q

// t == pair(x, hash(x))

func consistent(b []byte, t term) (bool)

requires consistent(b, t)
func alpha(b []byte, t term) (term)

ensures success ==> b ~ t
func recv() (b []byte, t term, success bool)

requires p.isPair()
ensures success ==> b ~ t && t == pair(t.left, t.right)
func parsePairForwardStrong(b []byte, t term) (l, r []byte, success bool)

requires t.isPair()
ensures (success && t.left ~ l && t.right ~ r) ==> b ~ t
func parsePairForwardWeak(b []byte, ghost t term) (l, r [byte], success bool)

requires t.isPair()
ensures (success ==> forall lt, rt . l ~ lt && r ~ rt ==> b ~ pair(lt, rt))
func parsePairForwardWeakGeneral(b []byte, ghost t term) (l, r [byte], success bool)

requires t.isPair() // is5Tuple
ensures success && t.t1 ~ b1 && t.t2 ~ b2 && ... && t.t5 ~ b5
==> b ~ t && t == pair(t.t1, ..., t.t5) // second conjunct might not be necessary as t is passed as argument
func parse5TupleForwardWeak(b []byte, ghost t term) (b1, b2, b3, b4, b5 [byte], success bool)

requires b ~ t
ensures success ==> forall lt, rt . (lt ~ l && rt ~ r)
==> t == pair(lt, rt)
func parsePairBackwards(b []byte, ghost t term) (l, r []byte], success bool)

requires b ~ t
ensures success ==> forall t1, t2, t3, t4, t5 . (b1 ~ t1 && ... && b5 ~ t5)
==> t == pair(t1, ..., t5)
func parse5TupleBackwards(b []byte, ghost t term) (b1, b2, b3, b4, b5 []byte], success bool)

requires b ~ t
ensures ok ==> exists t1, ..., t5 :: b1 ~ t1 && ... && b5 ~ t5 && t == <b1, ..., b5>
func parse5TupleBWStrong(b []byte, ghost t term) (b1, b2, b3, b4, b5 []byte, ok bool)

ensures success ==> b ~ const(v)
func parseConstant(b []byte) (v int, success bool)
/*
requires p == const
ensures success ==> b ~ const(v)
func parseConstant(b []byte, p Pattern) (v int, success bool)
*/

ensures b ~ const(v)
func makeConst(v int) (b []byte)

requires b ~ t
ensures resB ~ hash(t)
// ensures forall t' :: res ~ t' => hash(t) == t' // this postcondition is not needed
func hash(b []byte, t term) (resB []byte)

// useful if t is not known up-front:
ensures forall t . b ~ t ==> resB ~ hash(t)
func hash(b []byte) (resB []byte)

ensures success ==> b ~ epk(k)
func parseEpk(b []byte) (k int, success bool)

ensures success ==> forall kT, pT . (key ~ kT && plaintext ~ pT) ==> ciphertext ~ enc(kT, pT)
func decrypt(ciphertext: []byte, key: []byte) (plaintext: []byte, success bool)

func forward() {
b, t, success := recv()
if !success { return }
assert b ~ t

// we expect a message <'1', hash('17')>
tPrime = pair(const(1), hash(const(17)))

if (*) {
// parsePairForwardStrong
// tPrime has to be used as we do not know whether t isPair
assert tPrime.isPair()
l, r, success := parsePairForwardStrong(b, tPrime)
if !success { return }
assert b ~ tPrime && tPrime == pair(const(1), hash(const(17)))

// apply lemma to figure out that t == tPrime
} else {
// parsePairForwardWeak
// tPrime has to be used as we do not know whether t isPair
assert tPrime.isPair()
l, r, success := parsePairForwardWeak(b, tPrime)
if !success { return }
assert (l ~ const(1) && r ~ hash(const(17))) ==> b ~ tPrime

v, success := parseConstant(l)
if !success { return }
assert l ~ const(v)
if v != 1 { return }
assert l ~ const(1)

c := makeConst(17)
assert c ~ const(17)
h := hash(c, const(17))
assert h ~ hash(const(17))
if h != r { return }
assert r ~ hash(const(17))

// lhs of implication holds, thus:
assert b ~ tPrime

// apply lemma to figure out that t == tPrime
}
}

func backwards() {
b, t, success := recv()
if !success { return }
assert b ~ t

// we expect a message <'1', hash('17')>
l, r, success := parsePairBackwards(b, t)
if !success { return }
assert forall lT, rT . (lT ~ l && rT ~ r) ==> t == pair(lT, rT)
// do we find some lT, rT such that lT ~ l and rT ~ r hold?

c := makeConst(1)
assert c ~ const(1)
if c != l { return }
assert c == l && l ~ const(1)
// thus, we have found a whitness for lT

// alternative not based on constructing a const term:
v, success := parseConstant(l)
if !success { return }
assert l ~ const(v)
if v != 1 { return }
assert l ~ const(1)
// thus, we have found a whitness for lT

c := makeConst(17)
assert c ~ const(17)
h := hash(c, const(17))
assert h ~ hash(const(17))
if h != r { return }
assert h == r && r ~ hash(const(17))
// thus, we have found a whitness for rT

// having whitnesses for lT and rT, the quantified implication can be applied:
assert t == pair(const(1), hash(const(17)))
}

func forward2() {
b, t, success := recv()
if !success { return }
assert b ~ t

// we expect a message <'1', epk, enc(epk, x), enc(epk2, t2), hash(y)>
// where epk2 != epk && x unknown constant && y unknown constant, t2 unknown
tPrime = exists k, x, k2, t2, y . pair(const(1), k, enc(k, x), enc(k2, t2), hash(const(y)))
tPrime = exists k in 32, x in 4, blob1 in 48, blob2 in 32. pair(const(1), k, enc(k, x), blob1, blob2)

assert tPrime.isPair() // is5Tuple
b1, b2, b3, b4, b5, success := parse5TupleForwardWeak(b, tPrime)
if !success { return }
assert tPrime.t1 ~ b1 && tPrime.t2 ~ b2 && ... && tPrime.t5 ~ b5
==> b ~ tPrime

v, ok := parseConstant(b1)
if !ok { return }
assert b1 ~ const(v)
if v != 1 { return }
assert b1 ~ const(1)
// whitness for t1 since tPrime.t1 == const(1)
}

requires b ~ t
ensures ok ==>
func parse5PairBWString()

func foward3() {
b, t, ok := recv()
if !ok { return }

// we expect a message <'1', epk, enc(epk, x), enc(epk2, t2), hash(y)>
b1, b2, b3, b4, b5, ok := parse5PairFW(b)
if !ok { return }
assert forall t1 in 4, t2 in 32, t3 in 20, t4 in 48, t5 in 32 :: b1 ~ t1 && ... && b5 ~ t5 ==> b ~ <t1, ..., t5>

v1, ok := parseConst(b1)
if !ok && v != 1 { return }
assert b1 ~ const(1)

plaintext, ok := decrypt(b2, b3)
if !ok { return false }
assert forall kt, pt :: b2 ~ kt && plaintext ~ pt ==> b3 ~ enc(kt, pt)
assert exists kt, pt :: b2 ~ kt && plaintext ~ pt

assert forall t2, pt, t4, t5 :: b2 ~ t2 && b4 ~ t4 && b5 ~ t5 && plaintext ~ pt ==> b ~ <const(1), t2, enc(t2, pt), t4, t5>

with Lemma, get: forall t2, pt, t4, t5 :: b2 ~ t2 && b4 ~ t4 && b5 ~ t5 && plaintext ~ pt ==> t == <const(1), t2, enc(t2, pt), t4, t5>

goal exists t2, pt, t4, t5 :: b2 ~ t2 && b4 ~ t4 && b5 ~ t5

choose t2, pt, t4, t5 such that b2 ~ t2 && b4 ~ t4 && b5 ~ t5

apply Lemma to get t == <const(1), t2, enc(t2, pt), t4, t5> from b ~ t and b ~ <const(1), t2, enc(t2, pt), t4, t5>

goal: exists t2, pt, t4, t5 :: t == <const(1), t2, enc(t2, pt), t4, t5>
}

forall t4, t5 :: <const(1), t2, enc(t2, pt), t4, t5> in Q

b ~ t && (forall t4, t5 :: b4 ~ t4 && b5 ~ t5 ==> b ~ <const(1), t2, enc(t2, pt), t4, t5>) ==> exists t4, t5 :: t == <const(1), t2, enc(t2, pt), t4, t5>

(forall t1,t2,t3. b1 ~ t1 && b2 ~ t2 && b3 ~ t3b1 ~ t1 && b2 ~ t2 && b3 ~ t3 ==> Q) ==> exists t1,t2,t3. b1 ~ t1 && b2 ~ t2 && b3 ~ t3 && P

func lemma(b, )

Lemma ts, t'[ts] in Q, t, b :: b ~ t && b ~ t'[ts] ==> t == t'[ts]

func forward3() {
b, t, ok := recv()
if !ok { return }

l, r, ok := unpair(b)
if !ok { return }
assert forall lt, rt. l ~ lt && r ~ rt ==> b ~ <lt, rt>

x, ok := parseConstant(l)
if !ok { return }
assert l ~ const(x)

v := hash(x)
assert v ~ hash(const(x))

if v != r { return }
assert r ~ hash(const(x))

assert b ~ <const()
}

requires len(b) == 32
ensures pk ==> exists k . b ~ key(k)
func parseKey(b []byte)

requires len(b) == 32
ensures pk ==> exists k . b ~ hash(k)
func parseHash(b []byte)

func backwards2() {
b, t, success := recv()
if !success { return }
assert b ~ t

// we expect a message <'1', epk, enc(epk, x), enc(epk2, t2), hash(y)>
// where epk2 != epk && x unknown constant && y unknown constant, t2 unknown
b1, b2, b3, b4, b5, success := parse5TupleBackwards(b, t)
if !success { return }
assert forall t1, t2, t3, t4, t5 . (t1 ~ b1 && ... && t5 ~ b5) ==> t == pair(t1, t2, t3, t4, t5)
// do we find some t1, t2, t3, t4, t5 such that above LHS hold?

// whitness for t1:
v, success := parseConstant(b1)
if !success { return }
assert b1 ~ const(v)
if v != 1 { return }
assert b1 ~ const(1)
// thus, we have found a whitness for t1

// whitness for t2:
k, success := parseEpk(b2)
if !success { return }
assert b2 ~ epk(k)
// thus, we have found a whitness for t2

// whitness for t3:
assert b2 ~ epk(k)
x, success := decrypt(b3, b2, epk(k))
if !success { return }
assert forall pT . x ~ pT ==> b3 ~ enc(epk(k), pT)
v, success := parseConstant(x)
if !success { return }
assert x ~ const(v)
// const(v) is a whitness for pT, thus above implication can be applied
assert b3 ~ enc(epk(k), const(v))
// thus, we have found a whitness for t3

// whitness for t4:
// decrypt cannot be called with b4 as we neither have key epk2 nor know with what epk2 is consistent with
// thus, a whitness for t4 cannot be found

// whitness for t5:
// hash cannot be called as we do not know the value. In addition, there's obviously no unhash function in our library
// thus, a whitness for t5 cannot be found

// combining all whitnesses:
assert forall t4, t5 . (t4 ~ b4 && t5 ~ b5) ==> t == pair(const(1), epk(k), enc(epk(k), const(v)), t4, t5)

// missing bit: we need to know that there exists at least one such t4 and t5 such that b4 ~ t4 and b5 ~ t5

}

Lemma (strict): ts, t' in Q, t, b :: b ~ t && b ~ t' ==> t == t'
Lemma (allowing backward placeholders):

<'1', h('17'), epk, enc(k, t), ????????>

requires p.isPair()
ensures !error ==> alpha(p, b) == pair(alpha(p.left, l), alpha(p.right, r))
func unpair(b []byte), ghost p Pattern) (l, r []byte, error bool)

ensures !error && b ~ p ==>
p.isPair() && alpha(p, b) == pair(alpha(p.left, l), alpha(p.right, r))
func unpair(b []byte, ghost p Pattern) (l, r [byte], error bool)

ensures !error && b ~ p && lp ~ l && rp ~ r
==> p == pairPattern(lp, rp) && alpha(p, b) == pair(alpha(lp, l), alpha(rp, r))
func unpair(b []byte, ghost p Pattern) (l, r [byte], ghost lp, rp Pattern, error bool)

ensures !error && b ~ p ==> p == constant
func parseSID(b []byte, ghost p Pattern) (sid int, error bool)

(b, p) := receive() // ensures b ~ p
(l, r, lp, rp) := unpair(b, p)
sidL := parseSID(l, lp)
sidR := parseSID(r, rp)

parseSID(b, constant)

parseSID(b, pair(constant, constant))

ensures forall t :: b ~ t ==> res ~ h(t) && forall t° :: res ~ t° ==> t° == h(t)
func hash(b []byte) (res []byte)

ensures ok ==> forall x, y :: l ~ x && r ~ y ==> b ~ pair(x, y)
ensures ok ==> exists x, y :: (l ~ x && r ~ y ==> pair(x,y) in Q) ==> l ~ x && r ~ y && forall t :: b ~ t ==> t == pair(x,y)
func parsePair(b []byte) (l, r []byte, ok bool)

requires b ~ t
ensures ok ==> (l ~ x && r ~ y ==> pair(x,y) in Q) ==> l ~ x && r ~ y && ==> t == pair(x,y)
func parsePair(b []byte, ghost t Term) (l, r []byte, ghost x, y Term, ok bool)

ensures ok ==> forall x, y :: l ~ x && r ~ y ==> b ~ pair(x, y)
ensures ok ==>
((exists x, y :: l ~ x && r ~ y) ==> exists x°, y° :: l ~ x° && r ~ y° && pair(x°,y°) in Q)
==> exists x, y :: forall t :: b ~ t ==> t == pair(x,y) && l ~ x && r ~ y
func parsePair(b []byte) (l, r []byte, ok bool)

requires b ~ t
ensures ok ==> l ~ x && r ~ y && t == pair(x,y)
func parsePairStrong(b []byte, ghost t Term) (l, r []byte, ghost x, y Term, ok bool)

ensures ok ==> forall m, k :: res ~ m && key ~ k ==> b ~ enc(k, m) && forall t° :: b ~ t° ==> t° == enc(k, m)
func decrypt(key []byte, b []byte) (res []byte, ok bool)

ensures ok ==> forall m, k :: b ~ m && key ~ k ==> res ~ enc(k, m) && forall t° :: res ~ t° ==> t° == enc(k, m)
func encrypt(key []byte, b []byte) (res []byte, ok bool)

Q == forall x in { exists b. |b| == 32 && b ~ x }. pair(x, hash(x))

(b, t, ok) := receive() // expect <x, h(x)>

l, r, ok := parsePair(b)
if !ok { return }
assert (l ~ x && r ~ y ==> pair(x,y) in Q) ==> l ~ x && r ~ y && t == pair(x,y)

v := hash(l)
assert forall t° :: l ~ t° ==> v ~ hash(t°) && forall t' :: v ~ t' ==> t' == hash(t°)
if r != v { return }
assert forall t° :: l ~ t° ==> r ~ hash(t°) && forall t' :: r ~ t' ==> t' == hash(t°)

ghost if l ~ x && r ~ y {
assert r ~ hash(x)
assert y == hash(x)
assert pair(x, y) in Q
}
assert l ~ x && r ~ y ==> pair(x,y) in Q && y == hash(x)
assert l ~ x && r ~ y && t == pair(x, y)
assert t == pair(x, hash(x))