---
# System prepended metadata

title: Untitled

---



```go=

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

```

```go=
// 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)



```

```go=

// 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'))
```




```go=

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












```