def capacity_node

stelliferous@0.0.2.0 · proofs/storage_readback.bend:11

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

11def capacity_node(~Element: Data,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+half: U32,+index: U32,+value: Element,choice: Bool,
12  left_capacity: {Tree.capacity(Element,Tree.store(Element,left,half,index,value)) == Tree.capacity(Element,left) : U32}) ->
13  {Tree.capacity(Element,Bool.pick(Tree.Tree<Element>,choice,Tree.Node{Tree.store(Element,left,half,index,value),right},
14      Tree.Node{left,Tree.store(Element,right,half,(index - half : U32),value)})) == U32.shl(Tree.capacity(Element,left)) : U32}:
15  match choice:
16    case True{}:
17      Equal.cong(U32,U32,U32.shl,Tree.capacity(Element,Tree.store(Element,left,half,index,value)),Tree.capacity(Element,left),left_capacity)
18    case False{}: {==}