~/jendhub

def write

stelliferous@0.0.2.0 · proofs/storage_witness.bend:131

import stelliferous@0.0.2.0/proofs/storage_witness.bend as StorageWitness
import Base

131def write(-Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,-value: Element,
132  +witness: Witness(Element,depth,storage)) -> Witness(Element,depth,Array.set(Element,storage,index,value)):
133  %Equal.sym(Array<Element> & U32,Array.size(Element,storage),(storage,U32.shln(1,depth)),size(Element,depth,storage,witness)) :
134    Witness(Element,depth,Array.set.fin(Element,Array.swap.at(Element,index,value,_)))
135  +start = U32.and(index,U32.sub(U32.shln(1,depth),1))
136  +choose_left = U32.is_lt(start,U32.shr(U32.shln(1,depth)))
137  finish(Element,depth,Array.swap.go(Element,storage,U32.shln(1,depth),start,value,choose_left),
138    swap(Element,depth,storage,U32.shln(1,depth),start,value,choose_left,witness))

Uses (20)

Used by (14)