def fetch_fresh

stelliferous@0.0.2.0 · proofs/storage_readback.bend:157

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

157def fetch_fresh(~Element: Data,depth: Nat,+value: Element,+size: U32,+index: U32) -> {Tree.fetch(Element,Tree.fresh(Element,depth,value),size,index) == value : Element}:
158  match depth:
159    case 0n: {==}
160    case 1n+ +rest:
161      pick_same(~Element,U32.is_lt(index,U32.shr(size)),Tree.fetch(Element,Tree.fresh(Element,rest,value),U32.shr(size),index),
162        Tree.fetch(Element,Tree.fresh(Element,rest,value),U32.shr(size),U32.sub(index,U32.shr(size))),value,
163        fetch_fresh(~Element,rest,value,U32.shr(size),index),fetch_fresh(~Element,rest,value,U32.shr(size),U32.sub(index,U32.shr(size))))