def size

stelliferous@0.0.2.0 · proofs/storage_witness.bend:58

import Base

58def size(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
59  {Array.size(Element,storage) == (storage,U32.shln(1,depth)) : Array<Element> & U32}:
60  match depth witness:
61    case 0n Leaf{value,owner}:
62      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : {Array.size(Element,_) == (_,U32.shln(1,0n)) : Array<Element> & U32}
63      {==}
64    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
65      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : {Array.size(Element,_) == (_,U32.shln(1,1n+rest)) : Array<Element> & U32}
66      %size(Element,rest,left,left_balanced) :
67        {Array.size.node(Element,right,Array.size(Element,left)) == Array.size.node(Element,right,_) : Array<Element> & U32}
68      {==}