1 import Base 2 import ../storage_buffer.bend as Storage 3 import ./storage_tree_model.bend as Tree 4 import ./storage_witness.bend as Witness 5 import ./loop_projection.bend as Projection 6 import ./bounded_u32_arithmetic.bend as Arithmetic 7 import ./word_encoding.bend as WordEncoding 8 import ./u32_comparison.bend as Comparison 9 import ./u32_division.bend as U32Division 10 11 # The tree model covers every native Array owner, including capacities larger 12 # than its logical sequence. These equalities allocate no runtime conversion. 13 def reflect_packed(-Element: Data,+tree: Tree.Tree) -> 14 {Tree.reflect(Element,Tree.pack(Element,tree)) == tree : Tree.Tree}: 15 match tree: 16 case Tree.Leaf{value}: {==} 17 case Tree.Node{+left,+right}: 18 %Equal.sym(Tree.Tree,Tree.reflect(Element,Tree.pack(Element,left)),left,reflect_packed(Element,left)) : 19 {Tree.Node{_,Tree.reflect(Element,Tree.pack(Element,right))} == Tree.Node{left,right} : Tree.Tree} 20 %Equal.sym(Tree.Tree,Tree.reflect(Element,Tree.pack(Element,right)),right,reflect_packed(Element,right)) : 21 {Tree.Node{left,_} == Tree.Node{left,right} : Tree.Tree} 22 {==} 23 24 def pack_reflected(-Element: Data,storage: Array) -> 25 {Tree.pack(Element,Tree.reflect(Element,storage)) == storage : Array}: 26 match storage: 27 case ALeaf{value}: {==} 28 case ANode{left,right}: 29 %pack_reflected(Element,left) : 30 {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{_,right} : Array} 31 %pack_reflected(Element,right) : 32 {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{Tree.pack(Element,Tree.reflect(Element,left)),_} : Array} 33 {==} 34 35 law fresh: 36 for -T: Data 37 for +depth: Nat 38 for +value: T 39 {Array.new(T,depth,value) == Tree.pack(T,Tree.fresh(T,depth,value)) : Array} 40 law clone: 41 for -T: Data 42 for +tree: Tree.Tree 43 {Array.clone(T,Tree.pack(T,tree)) == (Tree.pack(T,tree),Tree.pack(T,tree)) : Array & Array} 44 law read: 45 for -T: Data 46 for +tree: Tree.Tree 47 for +i: U32 48 {Array.get(T,Tree.pack(T,tree),i) == (Tree.pack(T,tree),Tree.read(T,tree,i)) : Array & T} 49 law write: 50 for -T: Data 51 for +tree: Tree.Tree 52 for +i: U32 53 for +value: T 54 {Array.set(T,Tree.pack(T,tree),i,value) == Tree.pack(T,Tree.write(T,tree,i,value)) : Array} 55 56 def fresh(T,depth,value): 57 Witness.fresh_model(T,depth,value) 58 59 def clone(T,tree): 60 match tree: 61 case Tree.Leaf{v}: 62 {==} 63 case Tree.Node{+l,+r}: 64 %Equal.sym(Array & Array,Array.clone(T,Tree.pack(T,l)),(Tree.pack(T,l),Tree.pack(T,l)), 65 clone(T,l)) : {Array.clone.node(T,_,Array.clone(T,Tree.pack(T,r))) == (Tree.pack(T, 66 Tree.Node{l,r}),Tree.pack(T,Tree.Node{l,r})) : Array & Array} 67 %Equal.sym(Array & Array,Array.clone(T,Tree.pack(T,r)),(Tree.pack(T,r),Tree.pack(T,r)), 68 clone(T,r)) : {Array.clone.node(T,(Tree.pack(T,l),Tree.pack(T,l)),_) == (Tree.pack(T, 69 Tree.Node{l,r}),Tree.pack(T,Tree.Node{l,r})) : Array & Array} 70 {==} 71 72 law size: 73 for -T: Data 74 for +tree: Tree.Tree 75 {Array.size(T,Tree.pack(T,tree)) == (Tree.pack(T,tree),Tree.capacity(T,tree)) : Array & U32} 76 def size(T,tree): 77 match tree: 78 case Tree.Leaf{v}: 79 {==} 80 case Tree.Node{+l,+r}: 81 %Equal.sym(Array & U32,Array.size(T,Tree.pack(T,l)),(Tree.pack(T,l),Tree.capacity(T,l)),size(T, 82 l)) : {Array.size.node(T,Tree.pack(T,r),_) == (Tree.pack(T,Tree.Node{l,r}),U32.shl(Tree.capacity(T, 83 l))) : Array & U32} 84 {==} 85 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. 89 law get_node: 90 for -T: Data 91 for +l: Tree.Tree 92 for +r: Tree.Tree 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} 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} 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} 102 def get_node(T,l,r,n,i,z,pl,pr): 103 match z: 104 case True{}: 105 %pl : {Array.swap.lo(T,Tree.pack(T,r),Array.get.go(T,Tree.pack(T,l),U32.shr(n),i,U32.is_lt(i,U32.shr(U32.shr(n))))) == 106 Array.swap.lo(T,Tree.pack(T,r),_) : Array & T} 107 {==} 108 case False{}: 109 %pr : {Array.swap.hi(T,Tree.pack(T,l),Array.get.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)), 110 U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n))))) == Array.swap.hi(T,Tree.pack(T,l),_) : Array & T} 111 {==} 112 113 law get_go: 114 for -T: Data 115 for +tree: Tree.Tree 116 for +n: U32 117 for +i: U32 118 {Array.get.go(T,Tree.pack(T,tree),n,i,U32.is_lt(i,U32.shr(n))) == (Tree.pack(T,tree),Tree.fetch(T,tree,n,i)) : Array & T} 119 def get_go(T,tree,n,i): 120 match tree: 121 case Tree.Leaf{v}: 122 {==} 123 case Tree.Node{+l,+r}: 124 get_node(T,l,r,n,i,U32.is_lt(i,U32.shr(n)),get_go(T,l,U32.shr(n),i),get_go(T,r,U32.shr(n),U32.sub(i,U32.shr(n)))) 125 126 def read(T,tree,i): 127 %get_go(T,tree,Tree.capacity(T,tree),U32.and(i,U32.sub(Tree.capacity(T,tree),1))) : {Array.get.at(T,i,Array.size(T, 128 Tree.pack(T,tree))) == _ : Array & T} 129 %size(T,tree) : {Array.get.at(T,i,Array.size(T,Tree.pack(T,tree))) == Array.get.at(T,i,_) : Array & T} 130 {==} 131 132 law swap_node: 133 for -T: Data 134 for +l: Tree.Tree 135 for +r: Tree.Tree 136 for +n: U32 137 for +i: U32 138 for +v: T 139 for +z: Bool 140 for pl: {Array.swap.go(T,Tree.pack(T,l),U32.shr(n),i,v,U32.is_lt(i,U32.shr(U32.shr(n)))) == 141 (Tree.pack(T,Tree.store(T,l,U32.shr(n),i,v)),Tree.fetch(T,l,U32.shr(n),i)) : Array & T} 142 for pr: {Array.swap.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),v,U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n)))) == 143 (Tree.pack(T,Tree.store(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n)))) : Array & T} 144 {Array.swap.go(T,Tree.pack(T,Tree.Node{l,r}),n,i,v,z) == (Tree.pack(T,Bool.pick(Tree.Tree,z, 145 Tree.Node{Tree.store(T,l,U32.shr(n),i,v),r},Tree.Node{l,Tree.store(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)})), 146 Bool.pick(T,z,Tree.fetch(T,l,U32.shr(n),i),Tree.fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))) : Array & T} 147 def swap_node(T,l,r,n,i,v,z,pl,pr): 148 match z: 149 case True{}: 150 %pl : {Array.swap.lo(T,Tree.pack(T,r),Array.swap.go(T,Tree.pack(T,l),U32.shr(n),i,v,U32.is_lt(i,U32.shr(U32.shr(n))))) == 151 Array.swap.lo(T,Tree.pack(T,r),_) : Array & T} 152 {==} 153 case False{}: 154 %pr : {Array.swap.hi(T,Tree.pack(T,l),Array.swap.go(T,Tree.pack(T,r),U32.shr(n),U32.sub(i,U32.shr(n)),v, 155 U32.is_lt(U32.sub(i,U32.shr(n)),U32.shr(U32.shr(n))))) == Array.swap.hi(T,Tree.pack(T,l),_) : Array & T} 156 {==} 157 158 law swap_go: 159 for -T: Data 160 for +tree: Tree.Tree 161 for +n: U32 162 for +i: U32 163 for +v: T 164 {Array.swap.go(T,Tree.pack(T,tree),n,i,v,U32.is_lt(i,U32.shr(n))) == (Tree.pack(T,Tree.store(T,tree,n,i,v)), 165 Tree.fetch(T,tree,n,i)) : Array & T} 166 def swap_go(T,tree,n,i,v): 167 match tree: 168 case Tree.Leaf{old}: 169 {==} 170 case Tree.Node{+l,+r}: 171 swap_node(T,l,r,n,i,v,U32.is_lt(i,U32.shr(n)),swap_go(T,l,U32.shr(n),i,v),swap_go(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)) 172 173 law swap: 174 for -T: Data 175 for +tree: Tree.Tree 176 for +i: U32 177 for +v: T 178 {Array.swap(T,Tree.pack(T,tree),i,v) == (Tree.pack(T,Tree.write(T,tree,i,v)),Tree.read(T,tree,i)) : Array & T} 179 def swap(T,tree,i,v): 180 %swap_go(T,tree,Tree.capacity(T,tree),U32.and(i,U32.sub(Tree.capacity(T,tree),1)),v) : {Array.swap.at(T,i,v,Array.size(T, 181 Tree.pack(T,tree))) == _ : Array & T} 182 %size(T,tree) : {Array.swap.at(T,i,v,Array.size(T,Tree.pack(T,tree))) == Array.swap.at(T,i,v,_) : Array & T} 183 {==} 184 185 def write(T,tree,i,value): 186 %Equal.sym(Array & T,Array.swap(T,Tree.pack(T,tree),i,value),(Tree.pack(T,Tree.write(T,tree,i,value)), 187 Tree.read(T,tree,i)),swap(T,tree,i,value)) : {Array.set.fin(T,_) == Tree.pack(T,Tree.write(T,tree,i,value)) : Array} 188 {==} 189 190 def guarded_read(~Element: Data,+fallback: Element,+valid: Bool,+tree: Tree.Tree,+index: U32) -> 191 {Storage.read_when(Element,fallback,valid,Tree.pack(Element,tree),index) == 192 (Tree.pack(Element,tree),Bool.pick(Element,valid,Tree.read(Element,tree,index),fallback)) : Array & Element}: 193 match valid: 194 case False{}: {==} 195 case True{}: read(Element,tree,index) 196 197 def bounded_read(~Element: Data,+fallback: Element,+tree: Tree.Tree,+index: U32,+logical_length: U32) -> 198 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) == 199 (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)), 200 Tree.read(Element,tree,index),fallback)) : Array & Element}: 201 %Equal.sym(Array & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)), 202 size(Element,tree)) : 203 {Storage.read_sized(Element,fallback,index,logical_length,_) == 204 (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)), 205 Tree.read(Element,tree,index),fallback)) : Array & Element} 206 guarded_read(~Element,fallback,U32.is_lt(index,logical_length) && U32.is_le(logical_length,Tree.capacity(Element,tree)),tree,index) 207 208 def bounded_read_is_get(~Element: Data,+fallback: Element,+tree: Tree.Tree,+index: U32,+logical_length: U32, 209 inside: {U32.is_lt(index,logical_length) == True{} : Bool}, 210 room: {U32.is_le(logical_length,Tree.capacity(Element,tree)) == True{} : Bool}) -> 211 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,logical_length) == 212 Array.get(Element,Tree.pack(Element,tree),index) : Array & Element}: 213 %Equal.sym(Array & U32,Array.size(Element,Tree.pack(Element,tree)),(Tree.pack(Element,tree),Tree.capacity(Element,tree)), 214 size(Element,tree)) : 215 {Storage.read_sized(Element,fallback,index,logical_length,_) == Array.get(Element,Tree.pack(Element,tree),index) : Array & Element} 216 %Equal.sym(Bool,U32.is_lt(index,logical_length),True{},inside) : 217 {Storage.read_when(Element,fallback,_ && U32.is_le(logical_length,Tree.capacity(Element,tree)),Tree.pack(Element,tree),index) == 218 Array.get(Element,Tree.pack(Element,tree),index) : Array & Element} 219 %Equal.sym(Bool,U32.is_le(logical_length,Tree.capacity(Element,tree)),True{},room) : 220 {Storage.read_when(Element,fallback,_,Tree.pack(Element,tree),index) == Array.get(Element,Tree.pack(Element,tree),index) : Array & Element} 221 {==} 222 223 # Sequence transfers preserve native modular addressing for every element type. 224 # Logical bounds belong to callers, independently of this representation law. 225 def write_sequence(~Element: Data,+values: List<&2,Element>,+offset: U32,+tree: Tree.Tree) -> 226 {Storage.write_list(Element,values,offset,Tree.pack(Element,tree)) == 227 Tree.pack(Element,Tree.write_sequence(~Element,values,offset,tree)) : Array}: 228 match values: 229 case Nil{}: {==} 230 case +head <> +tail: 231 %Equal.sym(Array,Array.set(Element,Tree.pack(Element,tree),offset,head), 232 Tree.pack(Element,Tree.write(Element,tree,offset,head)),write(Element,tree,offset,head)) : 233 {Storage.write_list(Element,tail,(offset + 1 : U32),_) == 234 Tree.pack(Element,Tree.write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))) : Array} 235 write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head)) 236 237 def read_sequence(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree) -> 238 {Storage.read_list(Element,count,offset,Tree.pack(Element,tree)) == 239 Tree.read_sequence(~Element,count,offset,tree) : List<&2,Element>}: 240 match count: 241 case 0n: {==} 242 case 1n+ +rest: 243 %Equal.sym(Array & Element,Array.get(Element,Tree.pack(Element,tree),offset), 244 (Tree.pack(Element,tree),Tree.read(Element,tree,offset)),read(Element,tree,offset)) : 245 {Storage.bind_pair(Array,Element,List<&2,Element>,_,storage => value => 246 value <> Storage.read_list(Element,rest,(offset + 1 : U32),storage)) == 247 Tree.read(Element,tree,offset) <> Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree) : List<&2,Element>} 248 %read_sequence(~Element,rest,(offset + 1 : U32),tree) : 249 {Tree.read(Element,tree,offset) <> Storage.read_list(Element,rest,(offset + 1 : U32),Tree.pack(Element,tree)) == 250 Tree.read(Element,tree,offset) <> _ : List<&2,Element>} 251 {==} 252 253 def sequence_length(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree) -> 254 {List.length(&2,Element,Tree.read_sequence(~Element,count,offset,tree)) == count : Nat}: 255 match count: 256 case 0n: {==} 257 case 1n+ +rest: 258 %sequence_length(~Element,rest,(offset + 1 : U32),tree) : 259 {1n+List.length(&2,Element,Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree)) == 1n+_ : Nat} 260 {==} 261 262 # An observed logical prefix has the actual stored element at every valid index. 263 # Capacity need not equal count; address overflow remains explicitly modular. 264 def sequence_element(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree,+index: Nat, 265 inside: {Nat.is_lt(index,count) == True{} : Bool}) -> 266 {List.get(&2,Element,Tree.read_sequence(~Element,count,offset,tree),index) == 267 Some{Tree.read(Element,tree,(offset + U32.from_nat(index) : U32))} : Maybe<&2,Element>}: 268 match count index: 269 case 0n 0n: 270 Empty.absurd({None{} == Some{Tree.read(Element,tree,(offset + 0 : U32))} : Maybe<&2,Element>},WordEncoding.false_true(inside)) 271 case 0n 1n+previous: 272 Empty.absurd({None{} == Some{Tree.read(Element,tree,(offset + U32.from_nat(1n+previous) : U32))} : Maybe<&2,Element>},WordEncoding.false_true(inside)) 273 case 1n+rest 0n: 274 %Equal.sym(U32,(offset + 0 : U32),offset,Arithmetic.add_zero(offset)) : 275 {Some{Tree.read(Element,tree,offset)} == Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>} 276 {==} 277 case 1n+ +rest 1n+ +previous: 278 %Equal.sym(U32,(offset + U32.from_nat(1n+previous) : U32),((offset + 1 : U32) + U32.from_nat(previous) : U32), 279 Projection.indexed_successor(offset,previous)) : 280 {List.get(&2,Element,Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree),previous) == 281 Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>} 282 sequence_element(~Element,rest,(offset + 1 : U32),tree,previous,inside) 283 284 def sequence_missing(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree,+index: Nat, 285 outside: {Nat.is_lt(index,count) == False{} : Bool}) -> 286 {List.get(&2,Element,Tree.read_sequence(~Element,count,offset,tree),index) == None{} : Maybe<&2,Element>}: 287 match count index: 288 case 0n index: {==} 289 case 1n+rest 0n: 290 Empty.absurd({Some{Tree.read(Element,tree,offset)} == None{} : Maybe<&2,Element>}, 291 WordEncoding.false_true(Equal.sym(Bool,True{},False{},outside))) 292 case 1n+rest 1n+previous: 293 sequence_missing(~Element,rest,(offset + 1 : U32),tree,previous,outside) 294 295 def sequence_lookup_case(~Element: Data,+present: Bool,+length: U32,+tree: Tree.Tree,+index: U32, 296 order: {U32.is_lt(index,length) == present : Bool}) -> 297 {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) == 298 Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}) : Maybe<&2,Element>}: 299 match present: 300 case False{}: 301 sequence_missing(~Element,U32.to_nat(length),0,tree,U32.to_nat(index), 302 %Comparison.lt(index,length) : {_ == False{} : Bool} 303 order) 304 case True{}: 305 %Arithmetic.native_roundtrip(index) : 306 {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) == 307 Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>} 308 %Arithmetic.add_zero_left(U32.from_nat(U32.to_nat(index))) : 309 {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) == 310 Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>} 311 sequence_element(~Element,U32.to_nat(length),0,tree,U32.to_nat(index), 312 %Comparison.lt(index,length) : {_ == True{} : Bool} 313 order) 314 315 def default_after_presence(~Element: Data,+fallback: Element,+present: Bool,+value: Element) -> 316 {Bool.pick(Element,present && True{},value,fallback) == 317 Maybe.default(&2,Element,Bool.pick(Maybe<&2,Element>,present,Some{value},None{}),fallback) : Element}: 318 match present: 319 case False{}: {==} 320 case True{}: {==} 321 322 def bounded_read_observation_case(~Element: Data,+fallback: Element,+present: Bool,+length: U32,+tree: Tree.Tree,+index: U32, 323 +order: {U32.is_lt(index,length) == present : Bool},room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) -> 324 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) == 325 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element, 326 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array & Element}: 327 %Equal.sym(Array & Element,Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length), 328 (Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,length) && U32.is_le(length,Tree.capacity(Element,tree)),Tree.read(Element,tree,index),fallback)), 329 bounded_read(~Element,fallback,tree,index,length)) : 330 {_ == (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element, 331 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array & Element} 332 %Equal.sym(Bool,U32.is_le(length,Tree.capacity(Element,tree)),True{},room) : 333 {(Tree.pack(Element,tree),Bool.pick(Element,U32.is_lt(index,length) && _,Tree.read(Element,tree,index),fallback)) == 334 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element, 335 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array & Element} 336 %Equal.sym(Bool,U32.is_lt(index,length),present,order) : 337 {(Tree.pack(Element,tree),Bool.pick(Element,_ && True{},Tree.read(Element,tree,index),fallback)) == 338 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element, 339 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array & Element} 340 %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)), 341 Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}),sequence_lookup_case(~Element,present,length,tree,index,order)) : 342 {(Tree.pack(Element,tree),Bool.pick(Element,present && True{},Tree.read(Element,tree,index),fallback)) == 343 (Tree.pack(Element,tree),Maybe.default(&2,Element,_,fallback)) : Array & Element} 344 %default_after_presence(~Element,fallback,present,Tree.read(Element,tree,index)) : 345 {(Tree.pack(Element,tree),Bool.pick(Element,present && True{},Tree.read(Element,tree,index),fallback)) == 346 (Tree.pack(Element,tree),_) : Array & Element} 347 {==} 348 349 # Full logical-read contract, including out-of-range fallback. Only real 350 # capacity is required; the logical length need not fill the allocation. 351 def bounded_read_observation(~Element: Data,+fallback: Element,+length: U32,+tree: Tree.Tree,+index: U32, 352 room: {U32.is_le(length,Tree.capacity(Element,tree)) == True{} : Bool}) -> 353 {Storage.read_or(Element,fallback,Tree.pack(Element,tree),index,length) == 354 (Tree.pack(Element,tree),Maybe.default(&2,Element,List.get(&2,Element, 355 Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)),fallback)) : Array & Element}: 356 bounded_read_observation_case(~Element,fallback,U32.is_lt(index,length),length,tree,index,{==},room) 357 358 # A fact about an existing storage prefix, not another runtime container. 359 # Both the allocator and an external Array owner must establish these fields. 360 type SequenceEvidence<-Element: Data,-length: Nat,-values: List<&2,Element>> is Data: 361 SequenceEvidence{storage: Tree.Tree, 362 contents: {Tree.read_sequence(~Element,length,0,storage) == values : List<&2,Element>}, 363 room: {Nat.is_le(length,U32.to_nat(Tree.capacity(Element,storage))) == True{} : Bool}} 364 365 def sequence_storage(-Element: Data,-length: Nat,-values: List<&2,Element>, 366 evidence: SequenceEvidence) -> Tree.Tree: 367 SequenceEvidence{storage,contents,room} = evidence 368 storage 369 370 def sequence_owner(-Element: Data,-length: Nat,-values: List<&2,Element>, 371 evidence: SequenceEvidence) -> Array: 372 Tree.pack(Element,sequence_storage(Element,length,values,evidence)) 373 374 # The unchecked primitive is usable after the caller establishes its logical 375 # index bound. This is independent of allocation shape and unused capacity. 376 def stored_sequence_element(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>, 377 +evidence: SequenceEvidence,+index: Nat, 378 inside: {Nat.is_lt(index,length) == True{} : Bool}) -> 379 {Tree.read(Element,sequence_storage(Element,length,values,evidence),U32.from_nat(index)) == 380 Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback) : Element}: 381 SequenceEvidence{+storage,+contents,room} = evidence 382 %contents : 383 {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,List.get(&2,Element,_,index),fallback) : Element} 384 %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,length,0,storage),index), 385 Some{Tree.read(Element,storage,(0 + U32.from_nat(index) : U32))},sequence_element(~Element,length,0,storage,index,inside)) : 386 {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,_,fallback) : Element} 387 %Equal.sym(U32,(0 + U32.from_nat(index) : U32),U32.from_nat(index),Arithmetic.add_zero_left(U32.from_nat(index))) : 388 {Tree.read(Element,storage,U32.from_nat(index)) == Tree.read(Element,storage,_) : Element} 389 {==} 390 391 def read_sequence_evidence(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>, 392 +evidence: SequenceEvidence,+index: U32,+native_length: U32, 393 +length_exact: {U32.to_nat(native_length) == length : Nat}) -> 394 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),index,native_length) == 395 (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,U32.to_nat(index)),fallback)) : Array & Element}: 396 SequenceEvidence{+storage,+contents,room} = evidence 397 %contents : 398 {Storage.read_or(Element,fallback,Tree.pack(Element,storage),index,native_length) == 399 (Tree.pack(Element,storage),Maybe.default(&2,Element,List.get(&2,Element,_,U32.to_nat(index)),fallback)) : Array & Element} 400 %length_exact : 401 {Storage.read_or(Element,fallback,Tree.pack(Element,storage),index,native_length) == 402 (Tree.pack(Element,storage),Maybe.default(&2,Element,List.get(&2,Element,Tree.read_sequence(~Element,_,0,storage),U32.to_nat(index)),fallback)) : Array & Element} 403 bounded_read_observation(~Element,fallback,native_length,storage,index, 404 U32Division.nat_le_native(native_length,Tree.capacity(Element,storage), 405 %Equal.sym(Nat,U32.to_nat(native_length),length,length_exact) : 406 {Nat.is_le(_,U32.to_nat(Tree.capacity(Element,storage))) == True{} : Bool} 407 room)) 408 409 # The logical address conversion is separate from the physical owner. 410 def read_encoded_sequence(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>, 411 +evidence: SequenceEvidence,+address: U32,+index: Nat,+native_length: U32, 412 address_exact: {U32.to_nat(address) == index : Nat},length_exact: {U32.to_nat(native_length) == length : Nat}) -> 413 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),address,native_length) == 414 (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback)) : Array & Element}: 415 %address_exact : 416 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,evidence),address,native_length) == 417 (sequence_owner(Element,length,values,evidence),Maybe.default(&2,Element,List.get(&2,Element,values,_),fallback)) : Array & Element} 418 read_sequence_evidence(~Element,fallback,length,values,evidence,address,native_length,length_exact) 419 420 # Used only in propositions to compare reads from different physical owners. 421 def replace_read_owner(~Owner: Type,~Element: Data,owner: Owner,result: Owner & Element) -> Owner & Element: 422 (previous,value) = result 423 (owner,value) 424 425 def equivalent_sequence_read(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>, 426 +left: SequenceEvidence,+right: SequenceEvidence, 427 +index: U32,+native_length: U32,+length_exact: {U32.to_nat(native_length) == length : Nat}) -> 428 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,left),index,native_length) == 429 replace_read_owner(~Array,~Element,sequence_owner(Element,length,values,left), 430 Storage.read_or(Element,fallback,sequence_owner(Element,length,values,right),index,native_length)) : Array & Element}: 431 %Equal.sym(Array & Element, 432 Storage.read_or(Element,fallback,sequence_owner(Element,length,values,right),index,native_length), 433 (sequence_owner(Element,length,values,right),Maybe.default(&2,Element,List.get(&2,Element,values,U32.to_nat(index)),fallback)), 434 read_sequence_evidence(~Element,fallback,length,values,right,index,native_length,length_exact)) : 435 {Storage.read_or(Element,fallback,sequence_owner(Element,length,values,left),index,native_length) == 436 replace_read_owner(~Array,~Element,sequence_owner(Element,length,values,left),_) : Array & Element} 437 read_sequence_evidence(~Element,fallback,length,values,left,index,native_length,length_exact) 438 439 # Reify an affine owner once for proof consumers that need both its Data model 440 # and the relation. This helper is never imported by a numerical runtime path. 441 type Observation<-Element: Data,-storage: Array> is Data: 442 Observation{tree: Tree.Tree,packed: {Tree.pack(Element,tree) == storage : Array}, 443 reflected: {tree == Tree.reflect(Element,storage) : Tree.Tree}} 444 445 def observed_node_equation(-Element: Data,-left: Array,-right: Array,+left_tree: Tree.Tree,+right_tree: Tree.Tree, 446 left_packed: {Tree.pack(Element,left_tree) == left : Array},right_packed: {Tree.pack(Element,right_tree) == right : Array}) -> 447 {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{left,right} : Array}: 448 %left_packed : {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{_,right} : Array} 449 %right_packed : {Tree.pack(Element,Tree.Node{left_tree,right_tree}) == ANode{Tree.pack(Element,left_tree),_} : Array} 450 {==} 451 452 def observed_node_reflection(-Element: Data,-left: Array,-right: Array,+left_tree: Tree.Tree,+right_tree: Tree.Tree, 453 left_reflected: {left_tree == Tree.reflect(Element,left) : Tree.Tree}, 454 right_reflected: {right_tree == Tree.reflect(Element,right) : Tree.Tree}) -> 455 {Tree.Node{left_tree,right_tree} == Tree.reflect(Element,ANode{left,right}) : Tree.Tree}: 456 %left_reflected : {Tree.Node{left_tree,right_tree} == Tree.Node{_,Tree.reflect(Element,right)} : Tree.Tree} 457 %right_reflected : {Tree.Node{left_tree,right_tree} == Tree.Node{left_tree,_} : Tree.Tree} 458 {==} 459 460 def observed_node(-Element: Data,-left: Array,-right: Array, 461 left_observation: Observation,right_observation: Observation) -> Observation: 462 Observation{+left_tree,left_packed,left_reflected} = left_observation 463 Observation{+right_tree,right_packed,right_reflected} = right_observation 464 Observation{Tree.Node{left_tree,right_tree},observed_node_equation(Element,left,right,left_tree,right_tree,left_packed,right_packed), 465 observed_node_reflection(Element,left,right,left_tree,right_tree,left_reflected,right_reflected)} 466 def observe(-Element: Data,storage: Array) -> Observation: 467 match storage: 468 case ALeaf{+value}: Observation{Tree.Leaf{value},{==},{==}} 469 case ANode{left,right}: observed_node(Element,left,right,observe(Element,left),observe(Element,right)) 470 471 # Transport a concrete owner observation into a proposition checked on trees. 472 # The proposition and canonical proof are proof-only; they are not loop inputs. 473 def lift_observation(~Element: Data,~Context: Data, 474 ~Proposition: Context -> @-storage: Array -> @-tree: Tree.Tree -> Type, 475 +context: Context,-storage: Array,observation: Observation, 476 canonical: @+tree: Tree.Tree -> Proposition(context,Tree.pack(Element,tree),tree)) -> 477 Proposition(context,storage,Tree.reflect(Element,storage)): 478 Observation{+tree,packed,reflected} = observation 479 %reflected : Proposition(context,storage,_) 480 %packed : Proposition(context,_,tree) 481 canonical(tree) 482 483 def lift_pair_observation(~Element: Data,~Context: Data, 484 ~Proposition: Context -> @-input: Array -> @-output: Array -> 485 @-input_tree: Tree.Tree -> @-output_tree: Tree.Tree -> Type, 486 +context: Context,-input: Array,-output: Array, 487 input_observation: Observation,output_observation: Observation, 488 canonical: @+input_tree: Tree.Tree -> @+output_tree: Tree.Tree -> 489 Proposition(context,Tree.pack(Element,input_tree),Tree.pack(Element,output_tree),input_tree,output_tree)) -> 490 Proposition(context,input,output,Tree.reflect(Element,input),Tree.reflect(Element,output)): 491 Observation{+input_tree,input_packed,input_reflected} = input_observation 492 Observation{+output_tree,output_packed,output_reflected} = output_observation 493 %input_reflected : Proposition(context,input,output,_,Tree.reflect(Element,output)) 494 %output_reflected : Proposition(context,input,output,input_tree,_) 495 %input_packed : Proposition(context,_,output,input_tree,output_tree) 496 %output_packed : Proposition(context,Tree.pack(Element,input_tree),_,input_tree,output_tree) 497 canonical(input_tree)(output_tree)