1	import Base
2	
3	# A duplicable proof-only description of an array. Never used by the hash (copied from proofs/crypto/keccak/array.bend).
4	type Tree is Data:
5	  Leaf{value: U32}
6	  Node{left: Tree, right: Tree}
7	
8	def 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.
14	law reify:
15	  for a: Array<U32>
16	  Sigma<&2,&1,Tree,t => {a == thaw(t) : Array<U32>}>
17	
18	law 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	
25	def 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	
33	def reify(a):
34	  match a:
35	    case ALeaf{+x}: (Leaf{x},{==})
36	    case ANode{l,r}: reify_node(l,r,reify(l),reify(r))