law swap_go

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:158

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

158law swap_go:
159  for -T: Data
160  for +tree: Tree.Tree<T>
161  for +n: U32
162  for +i: U32
163  for +v: T
164  {Array.swap.go(T,Tree.pack(T,tree),n,i,v,U32.is_lt(i,U32.shr(n))) == (Tree.pack(T,Tree.store(T,tree,n,i,v)),
165      Tree.fetch(T,tree,n,i)) : Array<T> & T}