def fetch_node

stelliferous@0.0.2.0 · proofs/storage_readback.bend:31

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

31def fetch_node(~Element: Data,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+capacity: U32,+index: U32,+value: Element,choice: Bool,
32  choice_equal: {U32.is_lt(index,U32.shr(capacity)) == choice : Bool},
33  left_read: {Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),index) == value : Element},
34  right_read: {Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(index - U32.shr(capacity) : U32)) == value : Element}) ->
35  {Tree.fetch(Element,Bool.pick(Tree.Tree<Element>,choice,Tree.Node{Tree.store(Element,left,U32.shr(capacity),index,value),right},
36      Tree.Node{left,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value)}),capacity,index) == value : Element}:
37  match choice:
38    case True{}:
39      %Equal.sym(Bool,U32.is_lt(index,U32.shr(capacity)),True{},choice_equal) :
40        {Bool.pick(Element,_,Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),index),
41          Tree.fetch(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32))) == value : Element}
42      left_read
43    case False{}:
44      %Equal.sym(Bool,U32.is_lt(index,U32.shr(capacity)),False{},choice_equal) :
45        {Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),index),
46          Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(index - U32.shr(capacity) : U32))) == value : Element}
47      right_read