def read_tree

stelliferous@0.0.2.0 · proofs/storage_witness.bend:171

import Base

171def read_tree(-Element: Data,+depth: Nat,-storage: Array<Element>,+capacity: U32,+index: U32,choose_left: Bool,
172  witness: Witness(Element,depth,storage)) -> Read<Element,storage,Array.get.go(Element,storage,capacity,index,choose_left)>:
173  match depth witness:
174    case 0n Leaf{value,owner}:
175      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : Read<Element,_,Array.get.go(Element,_,capacity,index,choose_left)>
176      Read{value,{==}}
177    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
178      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : Read<Element,_,Array.get.go(Element,_,capacity,index,choose_left)>
179      read_choose(Element,left,right,capacity,index,choose_left,
180        read_tree(Element,rest,left,U32.shr(capacity),index,U32.is_lt(index,U32.shr(U32.shr(capacity))),left_balanced),
181        read_tree(Element,rest,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),
182          U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity))),right_balanced))