def capacity_indexed

stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:26

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

26def capacity_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: U32,+context: Context,+input: Tree.Tree<Element>) ->
27  {Tree.capacity(Element,run_indexed(~Element,~Context,~operation,count,position,context,input)) == Tree.capacity(Element,input) : U32}:
28  match count:
29    case 0n: {==}
30    case 1n+rest:
31      +value = operation(context,position,Tree.read(Element,input,position))
32      +written = Tree.write(Element,input,position,value)
33      Equal.trans(U32,Tree.capacity(Element,run_indexed(~Element,~Context,~operation,rest,(position + 1 : U32),context,written)),Tree.capacity(Element,written),Tree.capacity(Element,input),
34        capacity_indexed(~Element,~Context,~operation,rest,(position + 1 : U32),context,written),StorageReadback.write_capacity(~Element,input,position,value))