def restored

stelliferous@0.0.2.0 · proofs/storage_certificate.bend:39

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

39def restored(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness.Witness(Element,depth,storage)) ->
40  {Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) == storage : Array<Element>}:
41  match depth witness:
42    case 0n Witness.Leaf{value,owner}:
43      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) :
44        {Tree.pack(Element,normalized(Element,0n,Tree.reflect(Element,_))) == _ : Array<Element>}
45      {==}
46    case 1n+ +rest Witness.Node{left,right,owner,left_balanced,right_balanced}:
47      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) :
48        {Tree.pack(Element,normalized(Element,1n+rest,Tree.reflect(Element,_))) == _ : Array<Element>}
49      %restored(Element,rest,left,left_balanced) :
50        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),
51          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} == ANode{_,right} : Array<Element>}
52      %restored(Element,rest,right,right_balanced) :
53        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),
54          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} ==
55          ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),_} : Array<Element>}
56      {==}