1 import Base 2 import ./model.bend as Model 3 import ./array.bend as Core 4 import ./size.bend as Size 5 6 def trace(d: Nat, +n: U32, +i: U32, z: Bool) -> Model.Path(d): 7 match d z: 8 case 0n _: 9 Unit{} 10 case 1n+p True{}: 11 Model.Step{False{}, trace(p, U32.shr(n), i, 12 U32.is_lt(i, U32.shr(U32.shr(n))))} 13 case 1n+p False{}: 14 +j = U32.sub(i, U32.shr(n)) 15 Model.Step{True{}, trace(p, U32.shr(n), j, 16 U32.is_lt(j, U32.shr(U32.shr(n))))} 17 18 def first(-T: Type, pair: Array & T) -> Array: 19 (array, value) = pair 20 array 21 22 def second(-T: Type, pair: Array & T) -> T: 23 (array, value) = pair 24 value 25 26 type Get<-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, -z: Bool> is Type: 27 Get{array: Array, value: T, 28 equal: {(array, value) == Array.get.go(T, original, n, i, z) : Array & T}, 29 kept: {array == original : Array}, 30 observed: {Some{value} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}, 31 balanced: Model.Balanced(T, d, array)} 32 33 def get_low(-T: Data, -p: Nat, -original: Array, -n: U32, -i: U32, 34 ys: Array, 35 child: Get, 36 ey: Model.Balanced(T, p, ys)) -> Get: 37 match child: 38 case Get{xs, value, equal, kept, observed, ex}: 39 Get{ANode{xs, ys}, value, 40 Equal.cong(Array & T, Array & T, r => Array.swap.lo(T, ys, r), 41 (xs, value), Array.get.go(T, original, U32.shr(n), i, 42 U32.is_lt(i, U32.shr(U32.shr(n)))), equal), 43 Equal.cong(Array, Array, x => ANode{x, ys}, xs, original, kept), 44 observed, (ex, ey)} 45 46 def get_high(-T: Data, -p: Nat, -original: Array, -n: U32, -i: U32, 47 xs: Array, 48 child: Get, 50 ex: Model.Balanced(T, p, xs)) -> Get: 51 match child: 52 case Get{ys, value, equal, kept, observed, ey}: 53 Get{ANode{xs, ys}, value, 54 Equal.cong(Array & T, Array & T, r => Array.swap.hi(T, xs, r), 55 (ys, value), Array.get.go(T, original, U32.shr(n), U32.sub(i, U32.shr(n)), 56 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), equal), 57 Equal.cong(Array, Array, y => ANode{xs, y}, ys, original, kept), 58 observed, (ex, ey)} 59 60 def get_go(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, z: Bool, 61 valid: Model.Balanced(T, d, array)) -> Get: 62 match d array z: 63 case 0n ALeaf{+value} _: 64 Get{ALeaf{value}, value, {==}, {==}, {==}, valid} 65 case 0n ANode{xs, ys} _: 66 match valid: 67 case 1n+p ALeaf{value} _: 68 match valid: 69 case 1n+p ANode{xs, ys} True{}: 70 (ex, ey) = valid 71 get_low(T, p, xs, n, i, ys, 72 get_go(T, p, xs, U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n))), ex), ey) 73 case 1n+p ANode{xs, ys} False{}: 74 (ex, ey) = valid 75 +j = U32.sub(i, U32.shr(n)) 76 get_high(T, p, ys, n, i, xs, 77 get_go(T, p, ys, U32.shr(n), j, U32.is_lt(j, U32.shr(U32.shr(n))), ey), ex) 78 79 def get_go_retained(-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, -z: Bool, 80 cert: Get) -> 81 {first(T, Array.get.go(T, original, n, i, z)) == original : Array}: 82 match cert: 83 case Get{array, value, equal, kept, observed, valid}: 84 %equal : {first(T, _) == original : Array} 85 kept 86 87 def get_go_observed(-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, -z: Bool, 88 cert: Get) -> 89 {Some{second(T, Array.get.go(T, original, n, i, z))} == 90 Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}: 91 match cert: 92 case Get{array, value, equal, kept, observed, valid}: 93 %equal : {Some{second(T, _)} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>} 94 observed 95 96 def get_go_balanced(-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, -z: Bool, 97 cert: Get) -> 98 Model.Balanced(T, d, first(T, Array.get.go(T, original, n, i, z))): 99 match cert: 100 case Get{array, value, equal, kept, observed, valid}: 101 %equal : Model.Balanced(T, d, first(T, _)) 102 valid 103 104 def law_get_go_retains(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, z: Bool, 105 valid: Model.Balanced(T, d, array)) -> 106 {first(T, Array.get.go(T, array, n, i, z)) == array : Array}: 107 get_go_retained(T, d, array, n, i, z, get_go(T, d, array, n, i, z, valid)) 108 109 def law_get_go_refines(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, z: Bool, 110 valid: Model.Balanced(T, d, array)) -> 111 {Some{second(T, Array.get.go(T, array, n, i, z))} == 112 Model.observe(T, d, array, trace(d, n, i, z)) : Maybe<&2, T>}: 113 get_go_observed(T, d, array, n, i, z, get_go(T, d, array, n, i, z, valid)) 114 115 def law_get_go_balanced(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, z: Bool, 116 valid: Model.Balanced(T, d, array)) -> 117 Model.Balanced(T, d, first(T, Array.get.go(T, array, n, i, z))): 118 get_go_balanced(T, d, array, n, i, z, get_go(T, d, array, n, i, z, valid)) 119 120 type Swap<-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, -z: Bool, -new: T> is Type: 121 Swap{array: Array, old: T, 122 equal: {(array, old) == Array.swap.go(T, original, n, i, new, z) : Array & T}, 123 written: {array == Core.write_path(T, d, original, trace(d, n, i, z), new) : Array}, 124 observed: {Some{old} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}, 125 balanced: Model.Balanced(T, d, array)} 126 127 def swap_low(-T: Data, -p: Nat, -original: Array, -n: U32, -i: U32, -new: T, 128 ys: Array, 129 child: Swap, 130 ey: Model.Balanced(T, p, ys)) -> Swap: 131 match child: 132 case Swap{xs, old, equal, written, observed, ex}: 133 Swap{ANode{xs, ys}, old, 134 Equal.cong(Array & T, Array & T, r => Array.swap.lo(T, ys, r), 135 (xs, old), Array.swap.go(T, original, U32.shr(n), i, new, 136 U32.is_lt(i, U32.shr(U32.shr(n)))), equal), 137 Equal.cong(Array, Array, x => ANode{x, ys}, xs, 138 Core.write_path(T, p, original, 139 trace(p, U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n)))), new), written), 140 observed, (ex, ey)} 141 142 def swap_high(-T: Data, -p: Nat, -original: Array, -n: U32, -i: U32, -new: T, 143 xs: Array, 144 child: Swap, 146 ex: Model.Balanced(T, p, xs)) -> Swap: 147 match child: 148 case Swap{ys, old, equal, written, observed, ey}: 149 Swap{ANode{xs, ys}, old, 150 Equal.cong(Array & T, Array & T, r => Array.swap.hi(T, xs, r), 151 (ys, old), Array.swap.go(T, original, U32.shr(n), U32.sub(i, U32.shr(n)), new, 152 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), equal), 153 Equal.cong(Array, Array, y => ANode{xs, y}, ys, 154 Core.write_path(T, p, original, 155 trace(p, U32.shr(n), U32.sub(i, U32.shr(n)), 156 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), new), written), 157 observed, (ex, ey)} 158 159 def swap_go(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, new: T, z: Bool, 160 valid: Model.Balanced(T, d, array)) -> Swap: 161 match d array z: 162 case 0n ALeaf{old} _: 163 Swap{ALeaf{new}, old, {==}, {==}, {==}, valid} 164 case 0n ANode{xs, ys} _: 165 match valid: 166 case 1n+p ALeaf{old} _: 167 match valid: 168 case 1n+p ANode{xs, ys} True{}: 169 (ex, ey) = valid 170 swap_low(T, p, xs, n, i, new, ys, 171 swap_go(T, p, xs, U32.shr(n), i, new, 172 U32.is_lt(i, U32.shr(U32.shr(n))), ex), ey) 173 case 1n+p ANode{xs, ys} False{}: 174 (ex, ey) = valid 175 +j = U32.sub(i, U32.shr(n)) 176 swap_high(T, p, ys, n, i, new, xs, 177 swap_go(T, p, ys, U32.shr(n), j, new, 178 U32.is_lt(j, U32.shr(U32.shr(n))), ey), ex) 179 180 def swap_go_written(-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, 181 -z: Bool, -new: T, cert: Swap) -> 182 {first(T, Array.swap.go(T, original, n, i, new, z)) == 183 Core.write_path(T, d, original, trace(d, n, i, z), new) : Array}: 184 match cert: 185 case Swap{array, old, equal, written, observed, valid}: 186 %equal : {first(T, _) == Core.write_path(T, d, original, trace(d, n, i, z), new) : Array} 187 written 188 189 def swap_go_observed(-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, 190 -z: Bool, -new: T, cert: Swap) -> 191 {Some{second(T, Array.swap.go(T, original, n, i, new, z))} == 192 Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}: 193 match cert: 194 case Swap{array, old, equal, written, observed, valid}: 195 %equal : {Some{second(T, _)} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>} 196 observed 197 198 def swap_go_balanced(-T: Data, -d: Nat, -original: Array, -n: U32, -i: U32, 199 -z: Bool, -new: T, cert: Swap) -> 200 Model.Balanced(T, d, first(T, Array.swap.go(T, original, n, i, new, z))): 201 match cert: 202 case Swap{array, old, equal, written, observed, valid}: 203 %equal : Model.Balanced(T, d, first(T, _)) 204 valid 205 206 def law_swap_go_refines(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, 207 new: T, z: Bool, valid: Model.Balanced(T, d, array)) -> 208 {first(T, Array.swap.go(T, array, n, i, new, z)) == 209 Core.write_path(T, d, array, trace(d, n, i, z), new) : Array}: 210 swap_go_written(T, d, array, n, i, z, new, swap_go(T, d, array, n, i, new, z, valid)) 211 212 def law_swap_go_balanced(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, 213 new: T, z: Bool, valid: Model.Balanced(T, d, array)) -> 214 Model.Balanced(T, d, first(T, Array.swap.go(T, array, n, i, new, z))): 215 swap_go_balanced(T, d, array, n, i, z, new, swap_go(T, d, array, n, i, new, z, valid)) 216 217 def law_swap_go_observed(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, 218 new: T, z: Bool, valid: Model.Balanced(T, d, array)) -> 219 {Some{second(T, Array.swap.go(T, array, n, i, new, z))} == 220 Model.observe(T, d, array, trace(d, n, i, z)) : Maybe<&2, T>}: 221 swap_go_observed(T, d, array, n, i, z, new, swap_go(T, d, array, n, i, new, z, valid)) 222 223 def masked(+n: U32, i: U32) -> U32: 224 U32.and(i, U32.sub(n, 1)) 225 226 def route_n(d: Nat, +n: U32, i: U32) -> Model.Path(d): 227 +j = masked(n, i) 228 trace(d, n, j, U32.is_lt(j, U32.shr(n))) 229 230 def route(+d: Nat, i: U32) -> Model.Path(d): 231 route_n(d, Size.capacity(d), i) 232 233 def observed_transport(-T: Data, -d: Nat, -array: Array, -original: Array, 234 -n: U32, -i: U32, -value: T, 235 kept: {array == original : Array}, extent: {n == Size.capacity(d) : U32}, 236 observed: {Some{value} == Model.observe(T, d, array, route_n(d, n, i)) : Maybe<&2, T>}) -> 237 {Some{value} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}: 238 %kept : {Some{value} == Model.observe(T, d, _, route(d, i)) : Maybe<&2, T>} 239 %extent : {Some{value} == Model.observe(T, d, array, route_n(d, _, i)) : Maybe<&2, T>} 240 observed 241 242 type GetFull<-T: Data, -d: Nat, -original: Array, -i: U32> is Type: 243 GetFull{array: Array, value: T, 244 equal: {(array, value) == Array.get(T, original, i) : Array & T}, 245 kept: {array == original : Array}, 246 observed: {Some{value} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}, 247 balanced: Model.Balanced(T, d, array)} 248 249 def get_final(-T: Data, -d: Nat, -original: Array, -sized_array: Array, -n: U32, -i: U32, 250 measured: {(sized_array, n) == Array.size(T, original) : Array & U32}, 251 +retained: {sized_array == original : Array}, extent: {n == Size.capacity(d) : U32}, 252 child: Get) -> 253 GetFull: 254 match child: 255 case Get{array, value, equal, kept, observed, valid}: 256 GetFull{array, value, 257 Equal.trans(Array & T, (array, value), Array.get.at(T, i, (sized_array, n)), 258 Array.get(T, original, i), equal, 259 Equal.cong(Array & U32, Array & T, r => Array.get.at(T, i, r), 260 (sized_array, n), Array.size(T, original), measured)), 261 Equal.trans(Array, array, sized_array, original, kept, retained), 262 observed_transport(T, d, sized_array, original, n, i, value, retained, extent, observed), 263 valid} 264 265 def get_sized(-T: Data, +d: Nat, -original: Array, +i: U32, 266 sized: Size.Sized) -> GetFull: 267 match sized: 268 case Size.Sized{array, +n, retained, measured, extent, valid}: 269 get_final(T, d, original, array, n, i, measured, retained, extent, 270 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid)) 271 272 def get(-T: Data, +d: Nat, array: Array, +i: U32, 273 valid: Model.Balanced(T, d, array)) -> GetFull: 274 get_sized(T, d, array, i, Size.certify(T, d, array, valid)) 275 276 def get_retained(-T: Data, -d: Nat, -original: Array, -i: U32, 277 cert: GetFull) -> {first(T, Array.get(T, original, i)) == original : Array}: 278 match cert: 279 case GetFull{array, value, equal, kept, observed, valid}: 280 %equal : {first(T, _) == original : Array} 281 kept 282 283 def get_observed(-T: Data, -d: Nat, -original: Array, -i: U32, 284 cert: GetFull) -> 285 {Some{second(T, Array.get(T, original, i))} == 286 Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}: 287 match cert: 288 case GetFull{array, value, equal, kept, observed, valid}: 289 %equal : {Some{second(T, _)} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>} 290 observed 291 292 def get_balanced(-T: Data, -d: Nat, -original: Array, -i: U32, 293 cert: GetFull) -> Model.Balanced(T, d, first(T, Array.get(T, original, i))): 294 match cert: 295 case GetFull{array, value, equal, kept, observed, valid}: 296 %equal : Model.Balanced(T, d, first(T, _)) 297 valid 298 299 def law_get_retains(-T: Data, +d: Nat, array: Array, +i: U32, 300 valid: Model.Balanced(T, d, array)) -> {first(T, Array.get(T, array, i)) == array : Array}: 301 get_retained(T, d, array, i, get(T, d, array, i, valid)) 302 303 def law_get_refines(-T: Data, +d: Nat, array: Array, +i: U32, 304 valid: Model.Balanced(T, d, array)) -> 305 {Some{second(T, Array.get(T, array, i))} == Model.observe(T, d, array, route(d, i)) : Maybe<&2, T>}: 306 get_observed(T, d, array, i, get(T, d, array, i, valid)) 307 308 def law_get_balanced(-T: Data, +d: Nat, array: Array, +i: U32, 309 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, first(T, Array.get(T, array, i))): 310 get_balanced(T, d, array, i, get(T, d, array, i, valid)) 311 312 def written_transport(-T: Data, -d: Nat, -array: Array, -original: Array, 313 -n: U32, -i: U32, -new: T, -result: Array, 314 kept: {array == original : Array}, extent: {n == Size.capacity(d) : U32}, 315 written: {result == Core.write_path(T, d, array, route_n(d, n, i), new) : Array}) -> 316 {result == Core.write_path(T, d, original, route(d, i), new) : Array}: 317 %kept : {result == Core.write_path(T, d, _, route(d, i), new) : Array} 318 %extent : {result == Core.write_path(T, d, array, route_n(d, _, i), new) : Array} 319 written 320 321 type SwapFull<-T: Data, -d: Nat, -original: Array, -i: U32, -new: T> is Type: 322 SwapFull{array: Array, old: T, 323 equal: {(array, old) == Array.swap(T, original, i, new) : Array & T}, 324 written: {array == Core.write_path(T, d, original, route(d, i), new) : Array}, 325 observed: {Some{old} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}, 326 balanced: Model.Balanced(T, d, array)} 327 328 def swap_final(-T: Data, -d: Nat, -original: Array, -sized_array: Array, -n: U32, 329 -i: U32, -new: T, 330 measured: {(sized_array, n) == Array.size(T, original) : Array & U32}, 331 +retained: {sized_array == original : Array}, +extent: {n == Size.capacity(d) : U32}, 332 child: Swap) -> 333 SwapFull: 334 match child: 335 case Swap{array, old, equal, written, observed, valid}: 336 SwapFull{array, old, 337 Equal.trans(Array & T, (array, old), Array.swap.at(T, i, new, (sized_array, n)), 338 Array.swap(T, original, i, new), equal, 339 Equal.cong(Array & U32, Array & T, r => Array.swap.at(T, i, new, r), 340 (sized_array, n), Array.size(T, original), measured)), 341 written_transport(T, d, sized_array, original, n, i, new, array, retained, extent, written), 342 observed_transport(T, d, sized_array, original, n, i, old, retained, extent, observed), 343 valid} 344 345 def swap_sized(-T: Data, +d: Nat, -original: Array, +i: U32, new: T, 346 sized: Size.Sized) -> SwapFull: 347 match sized: 348 case Size.Sized{array, +n, retained, measured, extent, valid}: 349 swap_final(T, d, original, array, n, i, new, measured, retained, extent, 350 swap_go(T, d, array, n, masked(n, i), new, U32.is_lt(masked(n, i), U32.shr(n)), valid)) 351 352 def swap(-T: Data, +d: Nat, array: Array, +i: U32, new: T, 353 valid: Model.Balanced(T, d, array)) -> SwapFull: 354 swap_sized(T, d, array, i, new, Size.certify(T, d, array, valid)) 355 356 def swap_written(-T: Data, -d: Nat, -original: Array, -i: U32, -new: T, 357 cert: SwapFull) -> 358 {first(T, Array.swap(T, original, i, new)) == Core.write_path(T, d, original, route(d, i), new) : Array}: 359 match cert: 360 case SwapFull{array, old, equal, written, observed, valid}: 361 %equal : {first(T, _) == Core.write_path(T, d, original, route(d, i), new) : Array} 362 written 363 364 def swap_observed(-T: Data, -d: Nat, -original: Array, -i: U32, -new: T, 365 cert: SwapFull) -> 366 {Some{second(T, Array.swap(T, original, i, new))} == 367 Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}: 368 match cert: 369 case SwapFull{array, old, equal, written, observed, valid}: 370 %equal : {Some{second(T, _)} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>} 371 observed 372 373 def swap_balanced(-T: Data, -d: Nat, -original: Array, -i: U32, -new: T, 374 cert: SwapFull) -> 375 Model.Balanced(T, d, first(T, Array.swap(T, original, i, new))): 376 match cert: 377 case SwapFull{array, old, equal, written, observed, valid}: 378 %equal : Model.Balanced(T, d, first(T, _)) 379 valid 380 381 def set_written(-T: Data, -d: Nat, -original: Array, -i: U32, -new: T, 382 cert: SwapFull) -> 383 {Array.set(T, original, i, new) == Core.write_path(T, d, original, route(d, i), new) : Array}: 384 match cert: 385 case SwapFull{array, old, equal, written, observed, valid}: 386 %equal : {Array.set.fin(T, _) == Core.write_path(T, d, original, route(d, i), new) : Array} 387 written 388 389 def set_balanced(-T: Data, -d: Nat, -original: Array, -i: U32, -new: T, 390 cert: SwapFull) -> Model.Balanced(T, d, Array.set(T, original, i, new)): 391 match cert: 392 case SwapFull{array, old, equal, written, observed, valid}: 393 %equal : Model.Balanced(T, d, Array.set.fin(T, _)) 394 valid 395 396 def law_swap_refines(-T: Data, +d: Nat, array: Array, +i: U32, new: T, 397 valid: Model.Balanced(T, d, array)) -> 398 {first(T, Array.swap(T, array, i, new)) == Core.write_path(T, d, array, route(d, i), new) : Array}: 399 swap_written(T, d, array, i, new, swap(T, d, array, i, new, valid)) 400 401 def law_swap_observed(-T: Data, +d: Nat, array: Array, +i: U32, new: T, 402 valid: Model.Balanced(T, d, array)) -> 403 {Some{second(T, Array.swap(T, array, i, new))} == Model.observe(T, d, array, route(d, i)) : Maybe<&2, T>}: 404 swap_observed(T, d, array, i, new, swap(T, d, array, i, new, valid)) 405 406 def law_swap_balanced(-T: Data, +d: Nat, array: Array, +i: U32, new: T, 407 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, first(T, Array.swap(T, array, i, new))): 408 swap_balanced(T, d, array, i, new, swap(T, d, array, i, new, valid)) 409 410 def law_set_refines(-T: Data, +d: Nat, array: Array, +i: U32, new: T, 411 valid: Model.Balanced(T, d, array)) -> 412 {Array.set(T, array, i, new) == Core.write_path(T, d, array, route(d, i), new) : Array}: 413 set_written(T, d, array, i, new, swap(T, d, array, i, new, valid)) 414 415 def law_set_balanced(-T: Data, +d: Nat, array: Array, +i: U32, new: T, 416 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, Array.set(T, array, i, new)): 417 set_balanced(T, d, array, i, new, swap(T, d, array, i, new, valid)) 418 419 def law_get_at_refines(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, 420 valid: Model.Balanced(T, d, array)) -> 421 {Some{second(T, Array.get.at(T, i, (array, n)))} == 422 Model.observe(T, d, array, route_n(d, n, i)) : Maybe<&2, T>}: 423 get_go_observed(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), 424 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid)) 425 426 def law_get_at_retains(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, 427 valid: Model.Balanced(T, d, array)) -> 428 {first(T, Array.get.at(T, i, (array, n))) == array : Array}: 429 get_go_retained(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), 430 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid)) 431 432 def law_get_at_balanced(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, 433 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, first(T, Array.get.at(T, i, (array, n)))): 434 get_go_balanced(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), 435 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid)) 436 437 def law_swap_at_refines(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, new: T, 438 valid: Model.Balanced(T, d, array)) -> 439 {first(T, Array.swap.at(T, i, new, (array, n))) == 440 Core.write_path(T, d, array, route_n(d, n, i), new) : Array}: 441 swap_go_written(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), new, 442 swap_go(T, d, array, n, masked(n, i), new, U32.is_lt(masked(n, i), U32.shr(n)), valid)) 443 444 def law_swap_at_balanced(-T: Data, d: Nat, array: Array, +n: U32, +i: U32, new: T, 445 valid: Model.Balanced(T, d, array)) -> 446 Model.Balanced(T, d, first(T, Array.swap.at(T, i, new, (array, n)))): 447 swap_go_balanced(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), new, 448 swap_go(T, d, array, n, masked(n, i), new, U32.is_lt(masked(n, i), U32.shr(n)), valid))