def other_node

stelliferous@0.0.2.0 · proofs/storage_readback.bend:63

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

63def other_node(~Element: Data,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+capacity: U32,+index: U32,+query: U32,+value: Element,write_left: Bool,read_left: Bool,
64  +write_choice: {U32.is_lt(index,U32.shr(capacity)) == write_left : Bool},+read_choice: {U32.is_lt(query,U32.shr(capacity)) == read_left : Bool},
65  left_case: {U32.is_lt(index,U32.shr(capacity)) == True{} : Bool} -> {U32.is_lt(query,U32.shr(capacity)) == True{} : Bool} ->
66    {Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),query) == Tree.fetch(Element,left,U32.shr(capacity),query) : Element},
67  right_case: {U32.is_lt(index,U32.shr(capacity)) == False{} : Bool} -> {U32.is_lt(query,U32.shr(capacity)) == False{} : Bool} ->
68    {Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(query - U32.shr(capacity) : U32)) ==
69      Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32)) : Element}) ->
70  {Tree.fetch(Element,Bool.pick(Tree.Tree<Element>,write_left,Tree.Node{Tree.store(Element,left,U32.shr(capacity),index,value),right},
71      Tree.Node{left,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value)}),capacity,query) == Tree.fetch(Element,Tree.Node{left,right},capacity,query) : Element}:
72  match write_left read_left:
73    case True{} True{}:
74      %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),True{},read_choice) :
75        {Bool.pick(Element,_,Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
76          Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
77      left_case(write_choice)(read_choice)
78    case True{} False{}:
79      %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),False{},read_choice) :
80        {Bool.pick(Element,_,Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
81          Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
82      {==}
83    case False{} True{}:
84      %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),True{},read_choice) :
85        {Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
86          Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
87      {==}
88    case False{} False{}:
89      %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),False{},read_choice) :
90        {Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
91          Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
92      right_case(write_choice)(read_choice)