def read
stelliferous@0.0.2.0 · proofs/storage_witness.bend:184
import stelliferous@0.0.2.0/proofs/storage_witness.bend as StorageWitness
import Base
184def read(-Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,+witness: Witness(Element,depth,storage)) ->
185 Read<Element,storage,Array.get(Element,storage,index)>:
186 %Equal.sym(Array<Element> & U32,Array.size(Element,storage),(storage,U32.shln(1,depth)),size(Element,depth,storage,witness)) :
187 Read<Element,storage,Array.get.at(Element,index,_)>
188 +start = U32.and(index,U32.sub(U32.shln(1,depth),1))
189 read_tree(Element,depth,storage,U32.shln(1,depth),start,U32.is_lt(start,U32.shr(U32.shln(1,depth))),witness)