1 import Base 2 import ./model.bend as Model 3 import ./array.bend as ArrayCore 4 import ./refinement.bend as Refinement 5 import ./certificates.bend as Certificates 6 import ./clone.bend as Clone 7 import ./main.bend as Storage 8 import ./LAWS.bend as Laws 9 import ./frame.bend as Frame 10 import ./route.bend as Route 11 import ./arith.bend as Arith 12 import ./size.bend as Size 13 14 def finish_value(+d: Nat, n: Nat, -original: Array, -i: U32, result: Array & F32, 15 -exact: {result == Array.get(F32, original, i) : Array & F32}, 16 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) -> 17 {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.finish_read(d, n, original, i, result, exact, balanced, valid)) == 18 Done{Refinement.second(F32, result)} : Result<&2, &2, Storage.Error, F32>}: 19 (array, value) = result 20 {==} 21 22 def get_checked_hit(+d: Nat, +n: Nat, array: Array, +i: U32, allowed: Bool, 23 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool}, 24 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}, 25 yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 26 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> 27 {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) == 28 Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}: 29 match allowed: 30 case True{}: 31 finish_value(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid) 32 case False{}: 33 Empty.absurd({Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, False{}, decision, balanced, valid)) == 34 Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes)) 35 36 def read_hit(+d: Nat, +n: Nat, array: Array, -balanced: Model.Balanced(F32, d, array), 37 -valid: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 38 +i: U32, +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> 39 {Laws.read(Storage.Owned{d, n, array, balanced, valid}, i) == 40 Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}: 41 get_checked_hit(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid, 42 Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), True{}, inside), fits, inside) 43 44 def get_checked_miss(+d: Nat, +n: Nat, -array: Array, +i: U32, allowed: Bool, 45 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool}, 46 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}, 47 no: {False{} == allowed : Bool}) -> 48 {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) == 49 Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}: 50 match allowed: 51 case False{}: 52 {==} 53 case True{}: 54 Empty.absurd({Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, True{}, decision, balanced, valid)) == 55 Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}, Arith.clash(no)) 56 57 def set_checked_miss(+d: Nat, +n: Nat, -array: Array, +i: U32, -value: F32, allowed: Bool, 58 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool}, 59 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}, 60 no: {False{} == allowed : Bool}) -> 61 {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) == 62 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}: 63 match allowed: 64 case False{}: 65 {==} 66 case True{}: 67 Empty.absurd({Storage.set_checked(d, n, array, i, value, True{}, decision, balanced, valid) == 68 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}, Arith.clash(no)) 69 70 def set_checked_hit(+d: Nat, +n: Nat, -array: Array, +i: U32, +value: F32, allowed: Bool, 71 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool}, 72 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}, 73 yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 74 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> 75 {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) == 76 (Storage.Owned{d, n, Array.set(F32, array, i, value), 77 Certificates.set_result(F32, d, array, i, value, Array.set(F32, array, i, value), {==}, balanced), valid}, Done{Unit{}}) 78 : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}: 79 match allowed: 80 case True{}: 81 {==} 82 case False{}: 83 Empty.absurd({Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid) == 84 (Storage.Owned{d, n, Array.set(F32, array, i, value), 85 Certificates.set_result(F32, d, array, i, value, Array.set(F32, array, i, value), {==}, balanced), valid}, Done{Unit{}}) 86 : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}, Arith.clash_true(yes)) 87 88 def finish_owner(+d: Nat, +n: Nat, -original: Array, +i: U32, result: Array & F32, 89 -exact: {result == Array.get(F32, original, i) : Array & F32}, 90 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) -> 91 {Storage.finish_read(d, n, original, i, result, exact, balanced, valid) == 92 (Storage.Owned{d, n, Refinement.first(F32, result), Certificates.get_result(F32, d, original, i, result, exact, balanced), valid}, 93 Done{Refinement.second(F32, result)}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}: 94 (array, value) = result 95 {==} 96 97 def get_checked_keep(+d: Nat, +n: Nat, array: Array, +i: U32, allowed: Bool, 98 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool}, 99 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}, 100 yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 101 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> 102 {Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid) == 103 (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, array, i)), 104 Certificates.get_result(F32, d, array, i, Array.get(F32, array, i), {==}, balanced), valid}, 105 Done{Refinement.second(F32, Array.get(F32, array, i))}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}: 106 match allowed: 107 case True{}: 108 finish_owner(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid) 109 case False{}: 110 Empty.absurd({Storage.get_checked(d, n, array, i, False{}, decision, balanced, valid) == 111 (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, array, i)), 112 Certificates.get_result(F32, d, array, i, Array.get(F32, array, i), {==}, balanced), valid}, 113 Done{Refinement.second(F32, Array.get(F32, array, i))}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes)) 114 115 def get_checked_stay(+d: Nat, +n: Nat, -array: Array, +i: U32, allowed: Bool, 116 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool}, 117 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}, 118 no: {False{} == allowed : Bool}) -> 119 {Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid) == 120 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}: 121 match allowed: 122 case False{}: 123 {==} 124 case True{}: 125 Empty.absurd({Storage.get_checked(d, n, array, i, True{}, decision, balanced, valid) == 126 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}, Arith.clash(no)) 127 128 def finish_pair(+d: Nat, +n: Nat, -original: Array, pair: Array & Array, 129 -exact: {pair == Array.clone(F32, original) : Array & Array}, 130 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) -> 131 {Storage.finish_clone(d, n, original, pair, exact, balanced, valid) == 132 (Storage.Owned{d, n, Pair.fst(Array, Array, pair), Certificates.clone_first(F32, d, original, pair, exact, balanced), valid}, 133 Storage.Owned{d, n, Pair.snd(Array, Array, pair), Certificates.clone_second(F32, d, original, pair, exact, balanced), valid}) 134 : Storage.Storage & Storage.Storage}: 135 (first, second) = pair 136 {==} 137 138 def to_result(found: Maybe<&2, F32>) -> Result<&2, &2, Storage.Error, F32>: 139 match found: 140 case None{}: 141 Fail{Storage.InvalidIndex{}} 142 case Some{value}: 143 Done{value} 144 145 def le_refl(+k: Nat) -> {Nat.is_le(k, k) == True{} : Bool}: 146 match k: 147 case 0n: 148 {==} 149 case 1n+p: 150 le_refl(p) 151 152 def le_add_left(+f: Nat, +k: Nat) -> {Nat.is_le(k, Nat.add(f, k)) == True{} : Bool}: 153 match f: 154 case 0n: 155 le_refl(k) 156 case 1n+q: 157 Arith.le_succ(k, Nat.add(q, k), le_add_left(q, k)) 158 159 def le_add_right(+c: Nat, +x: Nat) -> {Nat.is_le(c, Nat.add(c, x)) == True{} : Bool}: 160 match c: 161 case 0n: 162 Arith.le_zero(x) 163 case 1n+r: 164 le_add_right(r, x) 165 166 def lt_add_left(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> 167 {Nat.is_lt(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}: 168 match c: 169 case 0n: 170 h 171 case 1n+r: 172 lt_add_left(r, x, y, h) 173 174 def eq_add_cancel(+c: Nat, +x: Nat, +y: Nat) -> {Nat.is_eq(x, y) == Nat.is_eq(Nat.add(c, x), Nat.add(c, y)) : Bool}: 175 match c: 176 case 0n: 177 {==} 178 case 1n+r: 179 eq_add_cancel(r, x, y) 180 181 def ne_low(+x: Nat, +c: Nat, +y: Nat, h: {Nat.is_lt(x, c) == True{} : Bool}) -> {False{} == Nat.is_eq(x, Nat.add(c, y)) : Bool}: 182 match x: 183 case 0n: 184 match c: 185 case 0n: 186 Empty.absurd({False{} == Nat.is_eq(0n, y) : Bool}, Arith.clash(h)) 187 case 1n+q: 188 {==} 189 case 1n+p: 190 match c: 191 case 0n: 192 Empty.absurd({False{} == Nat.is_eq(1n+p, y) : Bool}, Arith.clash(h)) 193 case 1n+q: 194 ne_low(p, q, y, h) 195 196 def ne_high(+x: Nat, +c: Nat, +y: Nat, h: {Nat.is_lt(x, c) == True{} : Bool}) -> {False{} == Nat.is_eq(Nat.add(c, y), x) : Bool}: 197 match x: 198 case 0n: 199 match c: 200 case 0n: 201 Empty.absurd({False{} == Nat.is_eq(y, 0n) : Bool}, Arith.clash(h)) 202 case 1n+q: 203 {==} 204 case 1n+p: 205 match c: 206 case 0n: 207 Empty.absurd({False{} == Nat.is_eq(y, 1n+p) : Bool}, Arith.clash(h)) 208 case 1n+q: 209 ne_high(p, q, y, h) 210 211 def offset_lt(+d: Nat, +path: Model.Path(d)) -> {Nat.is_lt(Model.offset(d, path), Model.capacity(d)) == True{} : Bool}: 212 match d: 213 case 0n: 214 {==} 215 case 1n+p: 216 Model.Step{+b, +rest} = path 217 match b: 218 case False{}: 219 Arith.lt_le_trans(Model.offset(p, rest), Model.capacity(p), Nat.add(Model.capacity(p), Model.capacity(p)), 220 offset_lt(p, rest), le_add_right(Model.capacity(p), Model.capacity(p))) 221 case True{}: 222 lt_add_left(Model.capacity(p), Model.offset(p, rest), Model.capacity(p), offset_lt(p, rest)) 223 224 def same_eq(+d: Nat, +p: Model.Path(d), +q: Model.Path(d)) -> 225 {Nat.is_eq(Model.offset(d, p), Model.offset(d, q)) == Model.same(d, p, q) : Bool}: 226 match d: 227 case 0n: 228 {==} 229 case 1n+r: 230 Model.Step{+pb, +pr} = p 231 match pb: 232 case False{}: 233 Model.Step{+qb, +qr} = q 234 match qb: 235 case False{}: 236 same_eq(r, pr, qr) 237 case True{}: 238 Equal.sym(Bool, False{}, Nat.is_eq(Model.offset(r, pr), Nat.add(Model.capacity(r), Model.offset(r, qr))), 239 ne_low(Model.offset(r, pr), Model.capacity(r), Model.offset(r, qr), offset_lt(r, pr))) 240 case True{}: 241 Model.Step{+qb, +qr} = q 242 match qb: 243 case False{}: 244 Equal.sym(Bool, False{}, Nat.is_eq(Nat.add(Model.capacity(r), Model.offset(r, pr)), Model.offset(r, qr)), 245 ne_high(Model.offset(r, qr), Model.capacity(r), Model.offset(r, pr), offset_lt(r, qr))) 246 case True{}: 247 %eq_add_cancel(Model.capacity(r), Model.offset(r, pr), Model.offset(r, qr)) : {_ == Model.same(r, pr, qr) : Bool} 248 same_eq(r, pr, qr) 249 250 def depth_of(+d: Nat, +n: Nat, +fits: {Storage.bounds(d, n) == True{} : Bool}) -> {Nat.is_le(d, 20n) == True{} : Bool}: 251 Arith.and_left(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), fits) 252 253 def slot_of(+d: Nat, +n: Nat, +i: U32, +fits: {Storage.bounds(d, n) == True{} : Bool}, 254 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}: 255 +rest = Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), fits) 256 Arith.lt_le_trans(U32.to_nat(i), n, Model.capacity(d), inside, 257 Arith.and_right(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)), rest)) 258 259 def route_same(+d: Nat, +n: Nat, +i: U32, +j: U32, +fits: {Storage.bounds(d, n) == True{} : Bool}, 260 +inside_i: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}, +inside_j: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 261 {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == Model.same(d, Refinement.route(d, i), Refinement.route(d, j)) : Bool}: 262 %same_eq(d, Refinement.route(d, i), Refinement.route(d, j)) : {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == _ : Bool} 263 %Route.route_offset(d, i, depth_of(d, n, fits), slot_of(d, n, i, fits, inside_i)) : 264 {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == Nat.is_eq(_, Model.offset(d, Refinement.route(d, j))) : Bool} 265 %Route.route_offset(d, j, depth_of(d, n, fits), slot_of(d, n, j, fits, inside_j)) : 266 {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == Nat.is_eq(U32.to_nat(i), _) : Bool} 267 {==} 268 269 type Effect is Data: 270 Wrote{index: U32, value: F32} 271 Kept{index: U32} 272 Left{} 273 Right{} 274 275 def grow(array: Array, +effect: Effect) -> Array: 276 match effect: 277 case Wrote{+i, +w}: 278 Array.set(F32, array, i, w) 279 case Kept{+i}: 280 Refinement.first(F32, Array.get(F32, array, i)) 281 case Left{}: 282 Pair.fst(Array, Array, Array.clone(F32, array)) 283 case Right{}: 284 Pair.snd(Array, Array, Array.clone(F32, array)) 285 286 def arr(+history: List<&2, Effect>, +d: Nat, +fill: F32) -> Array: 287 match history: 288 case Nil{}: 289 Array.new(F32, d, fill) 290 case +effect <> +past: 291 grow(arr(past, d, fill), effect) 292 293 def current(+history: List<&2, Effect>, +j: U32, +fill: F32) -> F32: 294 match history: 295 case Nil{}: 296 fill 297 case +effect <> +past: 298 match effect: 299 case Wrote{+i, +w}: 300 Bool.pick(F32, Nat.is_eq(U32.to_nat(i), U32.to_nat(j)), w, current(past, j, fill)) 301 case Kept{i}: 302 current(past, j, fill) 303 case Left{}: 304 current(past, j, fill) 305 case Right{}: 306 current(past, j, fill) 307 308 def Valid(+n: Nat, +history: List<&2, Effect>) -> Type: 309 match history: 310 case Nil{}: 311 Unit 312 case +effect <> +past: 313 match effect: 314 case Wrote{+i, w}: 315 {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool} & Valid(n, past) 316 case Kept{i}: 317 Valid(n, past) 318 case Left{}: 319 Valid(n, past) 320 case Right{}: 321 Valid(n, past) 322 323 def grow_balanced(+d: Nat, array: Array, +effect: Effect, valid: Model.Balanced(F32, d, array)) -> 324 Model.Balanced(F32, d, grow(array, effect)): 325 match effect: 326 case Wrote{+i, +w}: 327 Refinement.law_set_balanced(F32, d, array, i, w, valid) 328 case Kept{+i}: 329 Refinement.law_get_balanced(F32, d, array, i, valid) 330 case Left{}: 331 Clone.first_balanced(F32, d, array, Clone.certify(F32, d, array, valid)) 332 case Right{}: 333 Clone.second_balanced(F32, d, array, Clone.certify(F32, d, array, valid)) 334 335 def bal(+history: List<&2, Effect>, +d: Nat, +fill: F32) -> Model.Balanced(F32, d, arr(history, d, fill)): 336 match history: 337 case Nil{}: 338 ArrayCore.new_balanced(F32, d, fill) 339 case +effect <> +past: 340 grow_balanced(d, arr(past, d, fill), effect, bal(past, d, fill)) 341 342 def observe_new(+d: Nat, +value: F32, +path: Model.Path(d)) -> 343 {Some{value} == Model.observe(F32, d, Array.new(F32, d, value), path) : Maybe<&2, F32>}: 344 match d: 345 case 0n: 346 {==} 347 case 1n+p: 348 Model.Step{+bit, +rest} = path 349 match bit: 350 case False{}: 351 observe_new(p, value, rest) 352 case True{}: 353 observe_new(p, value, rest) 354 355 def select_pick(+b: Bool, +w: F32, +c: F32) -> {Some{Bool.pick(F32, b, w, c)} == Model.select(F32, b, w, Some{c}) : Maybe<&2, F32>}: 356 match b: 357 case False{}: 358 {==} 359 case True{}: 360 {==} 361 362 # Every in-bounds index has its own route, so the array after the effects 363 # answers each read with the last value written there, or the fill. 364 def model(+history: List<&2, Effect>, +d: Nat, +n: Nat, +fill: F32, +j: U32, 365 +fits: {Storage.bounds(d, n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}, 366 valid: Valid(n, history)) -> 367 {Some{current(history, j, fill)} == Model.observe(F32, d, arr(history, d, fill), Refinement.route(d, j)) : Maybe<&2, F32>}: 368 match history: 369 case Nil{}: 370 observe_new(d, fill, Refinement.route(d, j)) 371 case +effect <> +past: 372 match effect: 373 case Wrote{+i, +w}: 374 (inside_i, rest) = valid 375 %Equal.sym(Maybe<&2, F32>, 376 Model.observe(F32, d, Array.set(F32, arr(past, d, fill), i, w), Refinement.route(d, j)), 377 Model.select(F32, Model.same(d, Refinement.route(d, i), Refinement.route(d, j)), w, 378 Model.observe(F32, d, arr(past, d, fill), Refinement.route(d, j))), 379 Frame.primitive_update_frame(F32, d, arr(past, d, fill), i, Refinement.route(d, j), w, bal(past, d, fill))) : 380 {Some{current(Wrote{i, w} <> past, j, fill)} == _ : Maybe<&2, F32>} 381 %route_same(d, n, i, j, fits, inside_i, inside) : 382 {Some{current(Wrote{i, w} <> past, j, fill)} == 383 Model.select(F32, _, w, Model.observe(F32, d, arr(past, d, fill), Refinement.route(d, j))) : Maybe<&2, F32>} 384 %model(past, d, n, fill, j, fits, inside, rest) : 385 {Some{current(Wrote{i, w} <> past, j, fill)} == 386 Model.select(F32, Nat.is_eq(U32.to_nat(i), U32.to_nat(j)), w, _) : Maybe<&2, F32>} 387 select_pick(Nat.is_eq(U32.to_nat(i), U32.to_nat(j)), w, current(past, j, fill)) 388 case Kept{+i}: 389 %Equal.sym(Array, Refinement.first(F32, Array.get(F32, arr(past, d, fill), i)), arr(past, d, fill), 390 Refinement.law_get_retains(F32, d, arr(past, d, fill), i, bal(past, d, fill))) : 391 {Some{current(past, j, fill)} == Model.observe(F32, d, _, Refinement.route(d, j)) : Maybe<&2, F32>} 392 model(past, d, n, fill, j, fits, inside, valid) 393 case Left{}: 394 %Equal.sym(Array, Pair.fst(Array, Array, Array.clone(F32, arr(past, d, fill))), arr(past, d, fill), 395 Clone.first_equal(F32, d, arr(past, d, fill), Clone.certify(F32, d, arr(past, d, fill), bal(past, d, fill)))) : 396 {Some{current(past, j, fill)} == Model.observe(F32, d, _, Refinement.route(d, j)) : Maybe<&2, F32>} 397 model(past, d, n, fill, j, fits, inside, valid) 398 case Right{}: 399 %Equal.sym(Array, Pair.snd(Array, Array, Array.clone(F32, arr(past, d, fill))), arr(past, d, fill), 400 Clone.second_equal(F32, d, arr(past, d, fill), Clone.certify(F32, d, arr(past, d, fill), bal(past, d, fill)))) : 401 {Some{current(past, j, fill)} == Model.observe(F32, d, _, Refinement.route(d, j)) : Maybe<&2, F32>} 402 model(past, d, n, fill, j, fits, inside, valid) 403 404 def hit_of(+n: Nat, +ops: List<&2, Laws.Op>) -> Bool: 405 match ops: 406 case Nil{}: 407 True{} 408 case +op <> +later: 409 match op: 410 case Laws.Write{+i, w}: 411 Nat.is_lt(U32.to_nat(i), n) 412 case Laws.Read{+i}: 413 Nat.is_lt(U32.to_nat(i), n) 414 case Laws.First{}: 415 True{} 416 case Laws.Second{}: 417 True{} 418 case Laws.Length{}: 419 True{} 420 421 def replay_read(+rest: List<&2, Laws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Effect>, +j: U32, 422 hit: Bool, +dhit: {hit == hit_of(n, rest) : Bool}, 423 -b: Model.Balanced(F32, d, arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool}, 424 +fits: {Storage.bounds(d, n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}, 425 valid: Valid(n, history)) -> 426 {Laws.read(Laws.replay(rest, Storage.Owned{d, n, arr(history, d, fill), b, f}), j) == Done{Laws.expected(rest, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>}: 427 match rest: 428 case Nil{}: 429 %Equal.sym(Result<&2, &2, Storage.Error, F32>, Laws.read(Storage.Owned{d, n, arr(history, d, fill), b, f}, j), Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), j))}, 430 read_hit(d, n, arr(history, d, fill), b, f, fits, j, inside)) : {_ == Done{current(history, j, fill)} : Result<&2, &2, Storage.Error, F32>} 431 Equal.cong(Maybe<&2, F32>, Result<&2, &2, Storage.Error, F32>, to_result, Some{Refinement.second(F32, Array.get(F32, arr(history, d, fill), j))}, Some{current(history, j, fill)}, 432 Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, arr(history, d, fill), j))}, 433 Model.observe(F32, d, arr(history, d, fill), Refinement.route(d, j)), Some{current(history, j, fill)}, 434 Refinement.law_get_refines(F32, d, arr(history, d, fill), j, bal(history, d, fill)), 435 Equal.sym(Maybe<&2, F32>, Some{current(history, j, fill)}, Model.observe(F32, d, arr(history, d, fill), Refinement.route(d, j)), 436 model(history, d, n, fill, j, fits, inside, valid)))) 437 case +op <> +later: 438 match op: 439 case Laws.Write{+i, +w}: 440 match hit: 441 case True{}: 442 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) 443 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}), set_checked_hit(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) : 444 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j) == Done{Laws.expected(later, n, j, Laws.latest(n, Laws.Write{i, w}, j, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>} 445 %dhit : {Laws.read(Laws.replay(later, Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}), j) == 446 Done{Laws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>} 447 replay_read(later, d, n, fill, Wrote{i, w} <> history, j, hit_of(n, later), {==}, Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f, fits, inside, (inside_i, valid)) 448 case False{}: 449 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), set_checked_miss(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) : 450 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j) == Done{Laws.expected(later, n, j, Laws.latest(n, Laws.Write{i, w}, j, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>} 451 %dhit : {Laws.read(Laws.replay(later, Storage.Owned{d, n, arr(history, d, fill), b, f}), j) == Done{Laws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>} 452 replay_read(later, d, n, fill, history, j, hit_of(n, later), {==}, b, f, fits, inside, valid) 453 case Laws.Read{+i}: 454 match hit: 455 case True{}: 456 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) 457 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, arr(history, d, fill), i)), Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f}, Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), i))}), get_checked_keep(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) : 458 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>} 459 replay_read(later, d, n, fill, Kept{i} <> history, j, hit_of(n, later), {==}, Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f, fits, inside, valid) 460 case False{}: 461 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), get_checked_stay(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) : 462 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>} 463 replay_read(later, d, n, fill, history, j, hit_of(n, later), {==}, b, f, fits, inside, valid) 464 case Laws.First{}: 465 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) : 466 {Laws.read(Laws.replay(later, Laws.owner(Storage.Storage, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>} 467 replay_read(later, d, n, fill, Left{} <> history, j, hit_of(n, later), {==}, Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside, valid) 468 case Laws.Second{}: 469 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) : 470 {Laws.read(Laws.replay(later, Laws.outcome(Storage.Storage, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>} 471 replay_read(later, d, n, fill, Right{} <> history, j, hit_of(n, later), {==}, Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside, valid) 472 case Laws.Length{}: 473 replay_read(later, d, n, fill, history, j, hit_of(n, later), {==}, b, f, fits, inside, valid) 474 475 def replay_size_owned(+rest: List<&2, Laws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Effect>, 476 hit: Bool, +dhit: {hit == hit_of(n, rest) : Bool}, 477 -b: Model.Balanced(F32, d, arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool}, 478 +fits: {Storage.bounds(d, n) == True{} : Bool}) -> 479 {Laws.size(Laws.replay(rest, Storage.Owned{d, n, arr(history, d, fill), b, f})) == n : Nat}: 480 match rest: 481 case Nil{}: 482 {==} 483 case +op <> +later: 484 match op: 485 case Laws.Write{+i, +w}: 486 match hit: 487 case True{}: 488 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) 489 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}), set_checked_hit(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) : 490 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _))) == n : Nat} 491 replay_size_owned(later, d, n, fill, Wrote{i, w} <> history, hit_of(n, later), {==}, Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f, fits) 492 case False{}: 493 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), set_checked_miss(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) : 494 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _))) == n : Nat} 495 replay_size_owned(later, d, n, fill, history, hit_of(n, later), {==}, b, f, fits) 496 case Laws.Read{+i}: 497 match hit: 498 case True{}: 499 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) 500 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, arr(history, d, fill), i)), Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f}, Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), i))}), get_checked_keep(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) : 501 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _))) == n : Nat} 502 replay_size_owned(later, d, n, fill, Kept{i} <> history, hit_of(n, later), {==}, Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f, fits) 503 case False{}: 504 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), get_checked_stay(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) : 505 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _))) == n : Nat} 506 replay_size_owned(later, d, n, fill, history, hit_of(n, later), {==}, b, f, fits) 507 case Laws.First{}: 508 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) : 509 {Laws.size(Laws.replay(later, Laws.owner(Storage.Storage, _))) == n : Nat} 510 replay_size_owned(later, d, n, fill, Left{} <> history, hit_of(n, later), {==}, Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits) 511 case Laws.Second{}: 512 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) : 513 {Laws.size(Laws.replay(later, Laws.outcome(Storage.Storage, _))) == n : Nat} 514 replay_size_owned(later, d, n, fill, Right{} <> history, hit_of(n, later), {==}, Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits) 515 case Laws.Length{}: 516 replay_size_owned(later, d, n, fill, history, hit_of(n, later), {==}, b, f, fits) 517 518 def replay_size_empty(+ops: List<&2, Laws.Op>) -> {Laws.size(Laws.replay(ops, Storage.Empty{})) == 0n : Nat}: 519 match ops: 520 case Nil{}: 521 {==} 522 case +op <> +later: 523 match op: 524 case Laws.Write{+i, w}: 525 replay_size_empty(later) 526 case Laws.Read{+i}: 527 replay_size_empty(later) 528 case Laws.First{}: 529 replay_size_empty(later) 530 case Laws.Second{}: 531 replay_size_empty(later) 532 case Laws.Length{}: 533 replay_size_empty(later) 534 535 def status_hit(+d: Nat, +n: Nat, array: Array, -b: Model.Balanced(F32, d, array), 536 -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 537 +j: U32, +v: F32, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 538 {Laws.status(Storage.Owned{d, n, array, b, f}, j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}: 539 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, array, j, v, Nat.is_lt(U32.to_nat(j), n), {==}, b, f), 540 (Storage.Owned{d, n, Array.set(F32, array, j, v), Certificates.set_result(F32, d, array, j, v, Array.set(F32, array, j, v), {==}, b), f}, Done{Unit{}}), 541 set_checked_hit(d, n, array, j, v, Nat.is_lt(U32.to_nat(j), n), {==}, b, f, 542 Equal.sym(Bool, Nat.is_lt(U32.to_nat(j), n), True{}, inside), fits, inside)) : 543 {Laws.outcome(Result<&2, &2, Storage.Error, Unit>, _) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 544 {==} 545 546 def replay_status(+rest: List<&2, Laws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Effect>, +j: U32, +v: F32, 547 hit: Bool, +dhit: {hit == hit_of(n, rest) : Bool}, 548 -b: Model.Balanced(F32, d, arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool}, 549 +fits: {Storage.bounds(d, n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 550 {Laws.status(Laws.replay(rest, Storage.Owned{d, n, arr(history, d, fill), b, f}), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}: 551 match rest: 552 case Nil{}: 553 status_hit(d, n, arr(history, d, fill), b, f, fits, j, v, inside) 554 case +op <> +later: 555 match op: 556 case Laws.Write{+i, +w}: 557 match hit: 558 case True{}: 559 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) 560 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}), set_checked_hit(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) : 561 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 562 replay_status(later, d, n, fill, Wrote{i, w} <> history, j, v, hit_of(n, later), {==}, Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f, fits, inside) 563 case False{}: 564 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), set_checked_miss(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) : 565 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 566 replay_status(later, d, n, fill, history, j, v, hit_of(n, later), {==}, b, f, fits, inside) 567 case Laws.Read{+i}: 568 match hit: 569 case True{}: 570 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) 571 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, arr(history, d, fill), i)), Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f}, Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), i))}), get_checked_keep(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) : 572 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 573 replay_status(later, d, n, fill, Kept{i} <> history, j, v, hit_of(n, later), {==}, Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f, fits, inside) 574 case False{}: 575 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), get_checked_stay(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) : 576 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 577 replay_status(later, d, n, fill, history, j, v, hit_of(n, later), {==}, b, f, fits, inside) 578 case Laws.First{}: 579 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) : 580 {Laws.status(Laws.replay(later, Laws.owner(Storage.Storage, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 581 replay_status(later, d, n, fill, Left{} <> history, j, v, hit_of(n, later), {==}, Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside) 582 case Laws.Second{}: 583 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array, Array, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) : 584 {Laws.status(Laws.replay(later, Laws.outcome(Storage.Storage, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>} 585 replay_status(later, d, n, fill, Right{} <> history, j, v, hit_of(n, later), {==}, Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside) 586 case Laws.Length{}: 587 replay_status(later, d, n, fill, history, j, v, hit_of(n, later), {==}, b, f, fits, inside) 588 589 def bounds_from(+d: Nat, +n: Nat, depth: {Nat.is_le(d, 20n) == True{} : Bool}, positive: {Nat.is_lt(0n, n) == True{} : Bool}, 590 full: {Nat.is_le(n, Model.capacity(d)) == True{} : Bool}) -> {Storage.bounds(d, n) == True{} : Bool}: 591 %Equal.sym(Bool, Nat.is_le(d, 20n), True{}, depth) : {Bool.and(_, Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)))) == True{} : Bool} 592 %Equal.sym(Bool, Nat.is_lt(0n, n), True{}, positive) : {Bool.and(_, Nat.is_le(n, Model.capacity(d))) == True{} : Bool} 593 full 594 595 def seek_depth(+k: Nat, +left: {Nat.add(0n, k) == 20n : Nat}) -> {Nat.is_le(k, 20n) == True{} : Bool}: 596 %Equal.sym(Nat, k, 20n, left) : {Nat.is_le(_, 20n) == True{} : Bool} 597 {==} 598 599 def seek_full(+n: Nat, +k: Nat, +left: {Nat.add(0n, k) == 20n : Nat}, 600 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}) -> {Nat.is_le(n, Model.capacity(k)) == True{} : Bool}: 601 %Equal.sym(Nat, k, 20n, left) : {Nat.is_le(n, Model.capacity(_)) == True{} : Bool} 602 limit 603 604 def seek_room(+f: Nat, +k: Nat, +left: {Nat.add(f, k) == 20n : Nat}) -> {Nat.is_le(k, 20n) == True{} : Bool}: 605 %left : {Nat.is_le(k, _) == True{} : Bool} 606 le_add_left(f, k) 607 608 def seek_fit(+n: Nat, +k: Nat, +c: Nat, +decided: {True{} == Nat.is_le(n, c) : Bool}, +sized: {c == Model.capacity(k) : Nat}) -> 609 {Nat.is_le(n, Model.capacity(k)) == True{} : Bool}: 610 %sized : {Nat.is_le(n, _) == True{} : Bool} 611 Equal.sym(Bool, True{}, Nat.is_le(n, c), decided) 612 613 def seek_double(+k: Nat, +c: Nat, +sized: {c == Model.capacity(k) : Nat}) -> {Nat.add(c, c) == Model.capacity(1n+k) : Nat}: 614 %sized : {Nat.add(c, c) == Nat.add(_, _) : Nat} 615 {==} 616 617 def seek_left(+p: Nat, +k: Nat, +left: {Nat.add(1n+p, k) == 20n : Nat}) -> {Nat.add(p, 1n+k) == 20n : Nat}: 618 %Equal.sym(Nat, Nat.add(p, 1n+k), 1n+Nat.add(p, k), Arith.add_succ(p, k)) : {_ == 20n : Nat} 619 left 620 621 def seek_bounds(+fuel: Nat, +n: Nat, +k: Nat, +c: Nat, done: Bool, +decided: {done == Nat.is_le(n, c) : Bool}, 622 +sized: {c == Model.capacity(k) : Nat}, +left: {Nat.add(fuel, k) == 20n : Nat}, 623 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +positive: {Nat.is_lt(0n, n) == True{} : Bool}) -> 624 {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(fuel, n, k, c, done)), n) == True{} : Bool}: 625 match fuel: 626 case 0n: 627 bounds_from(k, n, seek_depth(k, left), positive, seek_full(n, k, left, limit)) 628 case 1n+p: 629 match done: 630 case True{}: 631 bounds_from(k, n, seek_room(1n+p, k, left), positive, seek_fit(n, k, c, decided, sized)) 632 case False{}: 633 seek_bounds(p, n, 1n+k, Nat.add(c, c), Nat.is_le(n, Nat.add(c, c)), {==}, seek_double(k, c, sized), 634 seek_left(p, k, left), limit, positive) 635 636 def limit_word() -> {1048576 == Size.capacity(20n) : U32}: 637 {==} 638 639 def cap_from(+n: U32, +fits: {U32.is_le(n, 1048576) == True{} : Bool}) -> 640 {Nat.is_le(U32.to_nat(n), Model.capacity(20n)) == True{} : Bool}: 641 %Route.cap_word(20n, {==}) : {Nat.is_le(U32.to_nat(n), _) == True{} : Bool} 642 %limit_word() : {Nat.is_le(U32.to_nat(n), U32.to_nat(_)) == True{} : Bool} 643 %Equal.sym(Bool, Nat.is_le(U32.to_nat(n), U32.to_nat(1048576)), U32.is_le(n, 1048576), Arith.u32_le(n, 1048576)) : {_ == True{} : Bool} 644 fits 645 646 def seek(+n: Nat, +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +positive: {Nat.is_lt(0n, n) == True{} : Bool}) -> 647 {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(20n, n, 0n, 1n, Nat.is_le(n, 1n))), n) == True{} : Bool}: 648 seek_bounds(20n, n, 0n, 1n, Nat.is_le(n, 1n), {==}, {==}, {==}, limit, positive) 649 650 def alloc_read(+d: Nat, +n: Nat, +value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool}, 651 +ops: List<&2, Laws.Op>, +j: U32, yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 652 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 653 {Laws.read(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, valid, decision))), j) == 654 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}: 655 match valid: 656 case True{}: 657 replay_read(ops, d, n, value, Nil{}, j, hit_of(n, ops), {==}, ArrayCore.new_balanced(F32, d, value), 658 Equal.sym(Bool, True{}, Storage.bounds(d, n), decision), fits, inside, Unit{}) 659 case False{}: 660 Empty.absurd({Laws.read(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, False{}, decision))), j) == 661 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes)) 662 663 def meta_read(+n: Nat, +value: F32, metadata: Nat & Nat, +ops: List<&2, Laws.Op>, +j: U32, 664 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}, 665 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 666 {Laws.read(Laws.replay(ops, Laws.created.of(Storage.allocate_at(n, value, metadata))), j) == 667 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}: 668 (+d, +capacity) = metadata 669 alloc_read(d, n, value, Storage.bounds(d, n), {==}, ops, j, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits, inside) 670 671 def new_read(+n: Nat, +value: F32, allowed: Bool, +ops: List<&2, Laws.Op>, +j: U32, yes: {True{} == allowed : Bool}, 672 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 673 {Laws.read(Laws.replay(ops, Laws.created.of(Storage.new_checked(n, value, allowed))), j) == 674 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}: 675 match n: 676 case 0n: 677 Empty.absurd({Laws.read(Laws.replay(ops, Laws.created.of(Storage.new_checked(0n, value, allowed))), j) == 678 Done{Laws.expected(ops, 0n, j, value)} : Result<&2, &2, Storage.Error, F32>}, Arith.lt_zero(U32.to_nat(j), inside)) 679 case 1n+p: 680 match allowed: 681 case True{}: 682 meta_read(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), ops, j, seek(1n+p, limit, {==}), inside) 683 case False{}: 684 Empty.absurd({Laws.read(Laws.replay(ops, Laws.created.of(Storage.new_checked(1n+p, value, False{}))), j) == 685 Done{Laws.expected(ops, 1n+p, j, value)} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes)) 686 687 def alloc_size(+d: Nat, +n: Nat, +value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool}, 688 +ops: List<&2, Laws.Op>, yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}) -> 689 {Laws.size(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, valid, decision)))) == n : Nat}: 690 match valid: 691 case True{}: 692 replay_size_owned(ops, d, n, value, Nil{}, hit_of(n, ops), {==}, ArrayCore.new_balanced(F32, d, value), 693 Equal.sym(Bool, True{}, Storage.bounds(d, n), decision), fits) 694 case False{}: 695 Empty.absurd({Laws.size(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, False{}, decision)))) == n : Nat}, 696 Arith.clash_true(yes)) 697 698 def meta_size(+n: Nat, +value: F32, metadata: Nat & Nat, +ops: List<&2, Laws.Op>, 699 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}) -> 700 {Laws.size(Laws.replay(ops, Laws.created.of(Storage.allocate_at(n, value, metadata)))) == n : Nat}: 701 (+d, +capacity) = metadata 702 alloc_size(d, n, value, Storage.bounds(d, n), {==}, ops, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits) 703 704 def new_size(+n: Nat, +value: F32, allowed: Bool, +ops: List<&2, Laws.Op>, yes: {True{} == allowed : Bool}, 705 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}) -> 706 {Laws.size(Laws.replay(ops, Laws.created.of(Storage.new_checked(n, value, allowed)))) == n : Nat}: 707 match n: 708 case 0n: 709 replay_size_empty(ops) 710 case 1n+p: 711 match allowed: 712 case True{}: 713 meta_size(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), ops, seek(1n+p, limit, {==})) 714 case False{}: 715 Empty.absurd({Laws.size(Laws.replay(ops, Laws.created.of(Storage.new_checked(1n+p, value, False{})))) == 1n+p : Nat}, 716 Arith.clash_true(yes)) 717 718 def positive_of(+n: Nat, +m: Nat, +over: {Nat.is_le(n, m) == False{} : Bool}) -> {Nat.is_lt(0n, n) == True{} : Bool}: 719 match n: 720 case 0n: 721 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, 722 Arith.clash_true(Equal.trans(Bool, True{}, Nat.is_le(0n, m), False{}, Equal.sym(Bool, Nat.is_le(0n, m), True{}, Arith.le_zero(m)), over))) 723 case 1n+p: 724 {==} 725 726 def new_refused(+n: Nat, -value: F32, allowed: Bool, no: {False{} == allowed : Bool}, 727 +positive: {Nat.is_lt(0n, n) == True{} : Bool}) -> 728 {Laws.refused.of(Storage.new_checked(n, value, allowed)) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>}: 729 match n: 730 case 0n: 731 Empty.absurd({Laws.refused.of(Storage.new_checked(0n, value, allowed)) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>}, 732 Arith.clash(positive)) 733 case 1n+p: 734 match allowed: 735 case False{}: 736 {==} 737 case True{}: 738 Empty.absurd({Laws.refused.of(Storage.new_checked(1n+p, value, True{})) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>}, 739 Arith.clash(no)) 740 741 def over_nat(+n: U32, +over: {U32.is_le(n, 1048576) == False{} : Bool}) -> 742 {Nat.is_le(U32.to_nat(n), U32.to_nat(1048576)) == False{} : Bool}: 743 %Equal.sym(Bool, Nat.is_le(U32.to_nat(n), U32.to_nat(1048576)), U32.is_le(n, 1048576), Arith.u32_le(n, 1048576)) : {_ == False{} : Bool} 744 over 745 746 def alloc_status(+d: Nat, +n: Nat, +value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool}, 747 +ops: List<&2, Laws.Op>, +j: U32, +v: F32, yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 748 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 749 {Laws.status(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, valid, decision))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}: 750 match valid: 751 case True{}: 752 replay_status(ops, d, n, value, Nil{}, j, v, hit_of(n, ops), {==}, ArrayCore.new_balanced(F32, d, value), 753 Equal.sym(Bool, True{}, Storage.bounds(d, n), decision), fits, inside) 754 case False{}: 755 Empty.absurd({Laws.status(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, False{}, decision))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}, 756 Arith.clash_true(yes)) 757 758 def meta_status(+n: Nat, +value: F32, metadata: Nat & Nat, +ops: List<&2, Laws.Op>, +j: U32, +v: F32, 759 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}, 760 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 761 {Laws.status(Laws.replay(ops, Laws.created.of(Storage.allocate_at(n, value, metadata))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}: 762 (+d, +capacity) = metadata 763 alloc_status(d, n, value, Storage.bounds(d, n), {==}, ops, j, v, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits, inside) 764 765 def new_status(+n: Nat, +value: F32, allowed: Bool, +ops: List<&2, Laws.Op>, +j: U32, +v: F32, yes: {True{} == allowed : Bool}, 766 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) -> 767 {Laws.status(Laws.replay(ops, Laws.created.of(Storage.new_checked(n, value, allowed))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}: 768 match n: 769 case 0n: 770 Empty.absurd({Laws.status(Laws.replay(ops, Laws.created.of(Storage.new_checked(0n, value, allowed))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}, 771 Arith.lt_zero(U32.to_nat(j), inside)) 772 case 1n+p: 773 match allowed: 774 case True{}: 775 meta_status(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), ops, j, v, seek(1n+p, limit, {==}), inside) 776 case False{}: 777 Empty.absurd({Laws.status(Laws.replay(ops, Laws.created.of(Storage.new_checked(1n+p, value, False{}))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}, 778 Arith.clash_true(yes)) 779 780 def alloc_fits(+d: Nat, +n: Nat, -value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool}, 781 yes: {True{} == valid : Bool}) -> 782 {Laws.refused.of(Storage.allocate(d, n, value, valid, decision)) == None{} : Maybe<&2, Storage.Error>}: 783 match valid: 784 case True{}: 785 {==} 786 case False{}: 787 Empty.absurd({Laws.refused.of(Storage.allocate(d, n, value, False{}, decision)) == None{} : Maybe<&2, Storage.Error>}, Arith.clash_true(yes)) 788 789 def meta_fits(+n: Nat, -value: F32, metadata: Nat & Nat, +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}) -> 790 {Laws.refused.of(Storage.allocate_at(n, value, metadata)) == None{} : Maybe<&2, Storage.Error>}: 791 (+d, +capacity) = metadata 792 alloc_fits(d, n, value, Storage.bounds(d, n), {==}, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits)) 793 794 def new_fits(+n: Nat, -value: F32, allowed: Bool, yes: {True{} == allowed : Bool}, 795 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}) -> 796 {Laws.refused.of(Storage.new_checked(n, value, allowed)) == None{} : Maybe<&2, Storage.Error>}: 797 match n: 798 case 0n: 799 {==} 800 case 1n+p: 801 match allowed: 802 case True{}: 803 meta_fits(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), seek(1n+p, limit, {==})) 804 case False{}: 805 Empty.absurd({Laws.refused.of(Storage.new_checked(1n+p, value, False{})) == None{} : Maybe<&2, Storage.Error>}, Arith.clash_true(yes))