law get_node

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:86

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

86# Base passes the branch z that the caller computed as i < n/2; each child
87# receives its own comparison against its half. The tree model picks the same
88# branch, so every lemma holds for any z and the recursion supplies its value.
89law get_node:
90  for -T: Data
91  for +l: Tree.Tree<T>
92  for +r: Tree.Tree<T>
93  for +n: U32
94  for +i: U32
95  for +z: Bool
96  for pl: {Array.get.go(T,Tree.pack(T,l),U32.shr(n),i,U32.is_lt(i,U32.shr(U32.shr(n)))) ==
97      (Tree.pack(T,l),Tree.fetch(T,l,U32.shr(n),i)) : Array<T> & T}
98  for pr: {Array.get.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n)))) ==
99      (Tree.pack(T,r),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n)))) : Array<T> & T}
100  {Array.get.go(T,Tree.pack(T,Tree.Node{l,r}),n,i,z) == (Tree.pack(T,Tree.Node{l,r}),Bool.pick(T,z,
101        Tree.fetch(T,l,U32.shr(n),i),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))) : Array<T> & T}