proofs/crypto/keccak/array.bend

bend-collections-laws-crypto@1.0.0.0 · 36 lines · 4 definitions

1import Base
2
3# A duplicable proof-only description of an array. Never used by the hash.
4type Tree is Data:
5  Leaf{value: U32}
6  Node{left: Tree, right: Tree}
7
8def thaw(t: Tree) -> Array<U32>:
9  match t:
10    case Leaf{x}: ALeaf{x}
11    case Node{l,r}: ANode{thaw(l),thaw(r)}
12
13# Consume any linear array once, retaining a proof of its exact representation.
14law reify:
15  for a: Array<U32>
16  Sigma<&2,&1,Tree,t => {a == thaw(t) : Array<U32>}>
17
18law reify_node:
19  for -l: Array<U32>
20  for -r: Array<U32>
21  for left: Sigma<&2,&1,Tree,t => {l == thaw(t) : Array<U32>}>
22  for right: Sigma<&2,&1,Tree,t => {r == thaw(t) : Array<U32>}>
23  Sigma<&2,&1,Tree,t => {ANode{l,r} == thaw(t) : Array<U32>}>
24
25def reify_node(l,r,left,right):
26  match left right:
27    case Tuple{+lt,lp} Tuple{+rt,rp}:
28      (Node{lt,rt},
29        Equal.trans(Array<U32>,ANode{l,r},ANode{thaw(lt),r},ANode{thaw(lt),thaw(rt)},
30          Equal.cong(Array<U32>,Array<U32>,x => ANode{x,r},l,thaw(lt),lp),
31          Equal.cong(Array<U32>,Array<U32>,x => ANode{thaw(lt),x},r,thaw(rt),rp)))
32
33def reify(a):
34  match a:
35    case ALeaf{+x}: (Leaf{x},{==})
36    case ANode{l,r}: reify_node(l,r,reify(l),reify(r))