StorageReadback.fetch_fresh: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_readback.bend as StorageReadback
Lines 157-163 of stelliferous@0.0.2.0/proofs/storage_readback.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_readback.bend&start_line=157&end_line=163

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

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

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_readback.bend&name=pick_same
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=fetch
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=fresh