1 import Base 2 import ./lib/array.bend as AR 3 import ./lib/logic.bend as L 4 import ../spec/lib/common.bend as SC 5 import ../src/containers/dynamic_array.bend as DA 6 import ../spec/containers/dynamic_array.bend as DAS 7 import ../src/containers/types/dynamic_array.bend as DAT 8 import ./containers/dynamic_array/proof.bend as DAP 9 import ./containers/dynamic_array/state.bend as DAST 10 import ../src/containers/deque.bend as DQ 11 import ../spec/containers/deque.bend as DQS 12 import ../src/containers/types/deque.bend as DQT 13 import ./containers/deque/proof.bend as DQP 14 import ./containers/deque/state.bend as DQSH 15 import ./containers/deque/stepok.bend as DQK 16 import ./containers/deque/trace.bend as DQTR 17 import ../src/containers/queue.bend as QU 18 import ../spec/containers/queue.bend as QUS 19 import ../src/containers/types/queue.bend as QUT 20 import ./containers/queue/proof.bend as QUP 21 import ./containers/queue/state.bend as QUSH 22 import ./containers/queue/steps.bend as QUST 23 import ./containers/queue/trace.bend as QUTR 24 import ./lib/order.bend as O 25 import ../src/containers/binary_heap.bend as BH 26 import ../spec/containers/binary_heap.bend as BHS 27 import ../src/containers/types/binary_heap.bend as BHT 28 import ./containers/binary_heap/proof.bend as BHP 29 import ./containers/binary_heap/state.bend as BHSH 30 import ./containers/binary_heap/steps.bend as BHST 31 import ./containers/binary_heap/trace.bend as BHTR 32 import ../src/containers/bitset.bend as BI 33 import ../spec/lib/common.bend as SCOM 34 import ../spec/containers/bitset.bend as BIS 35 import ../src/containers/types/bitset.bend as BIT 36 import ./containers/bitset/proof.bend as BIP 37 import ./containers/bitset/state.bend as BIST 38 import ./containers/bitset/steps.bend as BISP 39 import ./containers/bitset/trace.bend as BITR 40 import ../src/containers/bitlist.bend as BLI 41 import ../src/containers/types/bitlist.bend as BLT 42 import ../spec/containers/bitlist.bend as BLS 43 import ./containers/bitlist/state.bend as BLST 44 import ./containers/bitlist/steps.bend as BLSP 45 import ./containers/bitlist/trace.bend as BLTR 46 import ./containers/bitlist/proof.bend as BLP 47 import ../spec/containers/balanced_search_tree/recursive.bend as BTS 48 import ../src/containers/types/balanced_search_tree.bend as BTT 49 50 # Public correctness and trace laws, stated over the real src/ APIs and the 51 # independent spec/ models. Each law is discharged by its structure's proof 52 # entry module (proofs/.bend). PROOF.bend imports this file. 53 54 # ============================ retained LRU ============================ 55 56 law array_get_after_set_same: 57 for -T: Data 58 for +d: Nat 59 for +t: AR.Tree 60 for +i: U32 61 for +v: T 62 for +x: T 63 for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} 64 for +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool} 65 for +hx: {SC.nth(T, AR.slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} 66 for +pf: {AR.perfect(T, d, t) == True{} : Bool} 67 {Array.get(T, Array.set(T, AR.thaw(T, t), i, v), i) == (AR.thaw(T, AR.upd(T, d, t, U32.to_nat(i), v)), v) : Array & T} 68 def array_get_after_set_same(T, d, t, i, v, x, hd, hi, hx, pf): 69 AR.get_set_same(T, d, t, i, v, x, hd, hi, hx, pf) 70 71 law array_get_after_set_other: 72 for -T: Data 73 for +d: Nat 74 for +t: AR.Tree 75 for +i: U32 76 for +j: U32 77 for +v: T 78 for +x: T 79 for +y: T 80 for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} 81 for +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool} 82 for +hj: {Nat.is_lt(U32.to_nat(j), SC.pow2(d)) == True{} : Bool} 83 for +ne: {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == False{} : Bool} 84 for +hx: {SC.nth(T, AR.slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} 85 for +hy: {SC.nth(T, AR.slots(T, t), U32.to_nat(j)) == Some{y} : Maybe<&2, T>} 86 for +pf: {AR.perfect(T, d, t) == True{} : Bool} 87 {Array.get(T, Array.set(T, AR.thaw(T, t), i, v), j) == (AR.thaw(T, AR.upd(T, d, t, U32.to_nat(i), v)), y) : Array & T} 88 def array_get_after_set_other(T, d, t, i, j, v, x, y, hd, hi, hj, ne, hx, hy, pf): 89 AR.get_set_other(T, d, t, i, j, v, x, y, hd, hi, hj, ne, hx, hy, pf) 90 91 law array_new: 92 for -T: Data 93 for +d: Nat 94 for +v: T 95 {Array.new(T, d, v) == AR.thaw(T, AR.trep(T, d, v)) : Array} 96 def array_new(T, d, v): 97 AR.new(T, d, v) 98 99 # ============================ dynamic_array =========================== 100 101 law dynamic_array_new: 102 for -T: Data 103 {DAST.abs(T, DA.new(T)) == DAS.new(T) : DAS.Model} 104 def dynamic_array_new(T): 105 DAP.new_abs(T) 106 107 law dynamic_array_new_invariant: 108 for -T: Data 109 DAST.Inv(T, DA.new(T)) 110 def dynamic_array_new_invariant(T): 111 DAP.new_inv(T) 112 113 law dynamic_array_with_limit: 114 for -T: Data 115 for +k: Nat 116 {DAST.abs(T, DA.with_limit(T, k)) == DAS.with_limit(T, k) : DAS.Model} 117 def dynamic_array_with_limit(T, k): 118 DAP.with_limit_abs(T, k) 119 120 law dynamic_array_step: 121 for -T: Data 122 for +sh: DAST.Shadow 123 for +op: DAT.Op 124 for +g: {DAST.good(T, sh) == True{} : Bool} 125 {DAP.view1(T, DA.step(T, DAST.real(T, sh), op)) == DAS.step(T, DAST.abs(T, DAST.real(T, sh)), op) : DAS.Model & DAT.Obs} 126 def dynamic_array_step(T, sh, op, g): 127 DAP.step_refines(T, sh, op, g) 128 129 law dynamic_array_step_invariant: 130 for -T: Data 131 for +sh: DAST.Shadow 132 for +op: DAT.Op 133 for +g: {DAST.good(T, sh) == True{} : Bool} 134 DAST.Inv(T, Pair.fst(DA.DynArray<&2, T>, DAT.Obs, DA.step(T, DAST.real(T, sh), op))) 135 def dynamic_array_step_invariant(T, sh, op, g): 136 DAP.step_preserves(T, sh, op, g) 137 138 law dynamic_array_trace: 139 for -T: Data 140 for +ops: List<&2, DAT.Op> 141 {DAP.view(T, DA.run(T, ops, DA.new(T))) == DAS.run(T, ops, DAS.new(T)) : DAS.Model & List<&2, DAT.Obs>} 142 def dynamic_array_trace(T, ops): 143 DAP.trace_new(T, ops) 144 145 law dynamic_array_trace_invariant: 146 for -T: Data 147 for +ops: List<&2, DAT.Op> 148 DAST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, DAT.Obs>, DA.run(T, ops, DA.new(T)))) 149 def dynamic_array_trace_invariant(T, ops): 150 DAP.trace_new_inv(T, ops) 151 152 law dynamic_array_trace_limited: 153 for -T: Data 154 for +k: Nat 155 for +ops: List<&2, DAT.Op> 156 {DAP.view(T, DA.run(T, ops, DA.with_limit(T, k))) == DAS.run(T, ops, DAS.with_limit(T, k)) : DAS.Model & List<&2, DAT.Obs>} 157 def dynamic_array_trace_limited(T, k, ops): 158 DAP.trace_with_limit(T, k, ops) 159 160 law dynamic_array_trace_limited_invariant: 161 for -T: Data 162 for +k: Nat 163 for +ops: List<&2, DAT.Op> 164 DAST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, DAT.Obs>, DA.run(T, ops, DA.with_limit(T, k)))) 165 def dynamic_array_trace_limited_invariant(T, k, ops): 166 DAP.trace_with_limit_inv(T, k, ops) 167 168 169 # ---- executable specializations (closed element type; see src/dynamic_array.bend) ---- 170 # The `*_at` definitions are the ones tests and benchmarks actually run. They 171 # are proved equal to the parametric definitions above, so these laws are the 172 # same statements at the element types the project instantiates. 173 174 law dynamic_array_new_at_u32: 175 {DAST.abs(U32, DA.new_at(~U32)) == DAS.new(U32) : DAS.Model} 176 def dynamic_array_new_at_u32(): 177 DAP.new_at_abs(~U32) 178 179 law dynamic_array_new_at_invariant_u32: 180 DAST.Inv(U32, DA.new_at(~U32)) 181 def dynamic_array_new_at_invariant_u32(): 182 DAP.new_at_inv(~U32) 183 184 law dynamic_array_with_limit_at_u32: 185 for +k: Nat 186 {DAST.abs(U32, DA.with_limit_at(~U32, k)) == DAS.with_limit(U32, k) : DAS.Model} 187 def dynamic_array_with_limit_at_u32(k): 188 DAP.with_limit_at_abs(~U32, k) 189 190 law dynamic_array_step_at_u32: 191 for +sh: DAST.Shadow 192 for +op: DAT.Op 193 for +g: {DAST.good(U32, sh) == True{} : Bool} 194 {DAP.view1(U32, DA.step_at(~U32, DAST.real(U32, sh), op)) == DAS.step(U32, DAST.abs(U32, DAST.real(U32, sh)), op) : DAS.Model & DAT.Obs} 195 def dynamic_array_step_at_u32(sh, op, g): 196 DAP.step_at_refines(~U32, sh, op, g) 197 198 law dynamic_array_step_at_invariant_u32: 199 for +sh: DAST.Shadow 200 for +op: DAT.Op 201 for +g: {DAST.good(U32, sh) == True{} : Bool} 202 DAST.Inv(U32, Pair.fst(DA.DynArray<&2, U32>, DAT.Obs, DA.step_at(~U32, DAST.real(U32, sh), op))) 203 def dynamic_array_step_at_invariant_u32(sh, op, g): 204 DAP.step_at_preserves(~U32, sh, op, g) 205 206 law dynamic_array_trace_at_u32: 207 for +ops: List<&2, DAT.Op> 208 {DAP.view(U32, DA.run_at(~U32, ops, DA.new_at(~U32))) == DAS.run(U32, ops, DAS.new(U32)) : DAS.Model & List<&2, DAT.Obs>} 209 def dynamic_array_trace_at_u32(ops): 210 DAP.trace_new_at(~U32, ops) 211 212 law dynamic_array_trace_at_invariant_u32: 213 for +ops: List<&2, DAT.Op> 214 DAST.Inv(U32, Pair.fst(DA.DynArray<&2, U32>, List<&2, DAT.Obs>, DA.run_at(~U32, ops, DA.new_at(~U32)))) 215 def dynamic_array_trace_at_invariant_u32(ops): 216 DAP.trace_new_at_inv(~U32, ops) 217 218 law dynamic_array_trace_limited_at_u32: 219 for +k: Nat 220 for +ops: List<&2, DAT.Op> 221 {DAP.view(U32, DA.run_at(~U32, ops, DA.with_limit_at(~U32, k))) == DAS.run(U32, ops, DAS.with_limit(U32, k)) : DAS.Model & List<&2, DAT.Obs>} 222 def dynamic_array_trace_limited_at_u32(k, ops): 223 DAP.trace_with_limit_at(~U32, k, ops) 224 225 law dynamic_array_trace_limited_at_invariant_u32: 226 for +k: Nat 227 for +ops: List<&2, DAT.Op> 228 DAST.Inv(U32, Pair.fst(DA.DynArray<&2, U32>, List<&2, DAT.Obs>, DA.run_at(~U32, ops, DA.with_limit_at(~U32, k)))) 229 def dynamic_array_trace_limited_at_invariant_u32(k, ops): 230 DAP.trace_with_limit_at_inv(~U32, k, ops) 231 232 law dynamic_array_new_at_nat: 233 {DAST.abs(Nat, DA.new_at(~Nat)) == DAS.new(Nat) : DAS.Model} 234 def dynamic_array_new_at_nat(): 235 DAP.new_at_abs(~Nat) 236 237 law dynamic_array_new_at_invariant_nat: 238 DAST.Inv(Nat, DA.new_at(~Nat)) 239 def dynamic_array_new_at_invariant_nat(): 240 DAP.new_at_inv(~Nat) 241 242 law dynamic_array_with_limit_at_nat: 243 for +k: Nat 244 {DAST.abs(Nat, DA.with_limit_at(~Nat, k)) == DAS.with_limit(Nat, k) : DAS.Model} 245 def dynamic_array_with_limit_at_nat(k): 246 DAP.with_limit_at_abs(~Nat, k) 247 248 law dynamic_array_step_at_nat: 249 for +sh: DAST.Shadow 250 for +op: DAT.Op 251 for +g: {DAST.good(Nat, sh) == True{} : Bool} 252 {DAP.view1(Nat, DA.step_at(~Nat, DAST.real(Nat, sh), op)) == DAS.step(Nat, DAST.abs(Nat, DAST.real(Nat, sh)), op) : DAS.Model & DAT.Obs} 253 def dynamic_array_step_at_nat(sh, op, g): 254 DAP.step_at_refines(~Nat, sh, op, g) 255 256 law dynamic_array_step_at_invariant_nat: 257 for +sh: DAST.Shadow 258 for +op: DAT.Op 259 for +g: {DAST.good(Nat, sh) == True{} : Bool} 260 DAST.Inv(Nat, Pair.fst(DA.DynArray<&2, Nat>, DAT.Obs, DA.step_at(~Nat, DAST.real(Nat, sh), op))) 261 def dynamic_array_step_at_invariant_nat(sh, op, g): 262 DAP.step_at_preserves(~Nat, sh, op, g) 263 264 law dynamic_array_trace_at_nat: 265 for +ops: List<&2, DAT.Op> 266 {DAP.view(Nat, DA.run_at(~Nat, ops, DA.new_at(~Nat))) == DAS.run(Nat, ops, DAS.new(Nat)) : DAS.Model & List<&2, DAT.Obs>} 267 def dynamic_array_trace_at_nat(ops): 268 DAP.trace_new_at(~Nat, ops) 269 270 law dynamic_array_trace_at_invariant_nat: 271 for +ops: List<&2, DAT.Op> 272 DAST.Inv(Nat, Pair.fst(DA.DynArray<&2, Nat>, List<&2, DAT.Obs>, DA.run_at(~Nat, ops, DA.new_at(~Nat)))) 273 def dynamic_array_trace_at_invariant_nat(ops): 274 DAP.trace_new_at_inv(~Nat, ops) 275 276 law dynamic_array_trace_limited_at_nat: 277 for +k: Nat 278 for +ops: List<&2, DAT.Op> 279 {DAP.view(Nat, DA.run_at(~Nat, ops, DA.with_limit_at(~Nat, k))) == DAS.run(Nat, ops, DAS.with_limit(Nat, k)) : DAS.Model & List<&2, DAT.Obs>} 280 def dynamic_array_trace_limited_at_nat(k, ops): 281 DAP.trace_with_limit_at(~Nat, k, ops) 282 283 law dynamic_array_trace_limited_at_invariant_nat: 284 for +k: Nat 285 for +ops: List<&2, DAT.Op> 286 DAST.Inv(Nat, Pair.fst(DA.DynArray<&2, Nat>, List<&2, DAT.Obs>, DA.run_at(~Nat, ops, DA.with_limit_at(~Nat, k)))) 287 def dynamic_array_trace_limited_at_invariant_nat(k, ops): 288 DAP.trace_with_limit_at_inv(~Nat, k, ops) 289 290 law dynamic_array_new_at_string: 291 {DAST.abs(String, DA.new_at(~String)) == DAS.new(String) : DAS.Model} 292 def dynamic_array_new_at_string(): 293 DAP.new_at_abs(~String) 294 295 law dynamic_array_new_at_invariant_string: 296 DAST.Inv(String, DA.new_at(~String)) 297 def dynamic_array_new_at_invariant_string(): 298 DAP.new_at_inv(~String) 299 300 law dynamic_array_with_limit_at_string: 301 for +k: Nat 302 {DAST.abs(String, DA.with_limit_at(~String, k)) == DAS.with_limit(String, k) : DAS.Model} 303 def dynamic_array_with_limit_at_string(k): 304 DAP.with_limit_at_abs(~String, k) 305 306 law dynamic_array_step_at_string: 307 for +sh: DAST.Shadow 308 for +op: DAT.Op 309 for +g: {DAST.good(String, sh) == True{} : Bool} 310 {DAP.view1(String, DA.step_at(~String, DAST.real(String, sh), op)) == DAS.step(String, DAST.abs(String, DAST.real(String, sh)), op) : DAS.Model & DAT.Obs} 311 def dynamic_array_step_at_string(sh, op, g): 312 DAP.step_at_refines(~String, sh, op, g) 313 314 law dynamic_array_step_at_invariant_string: 315 for +sh: DAST.Shadow 316 for +op: DAT.Op 317 for +g: {DAST.good(String, sh) == True{} : Bool} 318 DAST.Inv(String, Pair.fst(DA.DynArray<&2, String>, DAT.Obs, DA.step_at(~String, DAST.real(String, sh), op))) 319 def dynamic_array_step_at_invariant_string(sh, op, g): 320 DAP.step_at_preserves(~String, sh, op, g) 321 322 law dynamic_array_trace_at_string: 323 for +ops: List<&2, DAT.Op> 324 {DAP.view(String, DA.run_at(~String, ops, DA.new_at(~String))) == DAS.run(String, ops, DAS.new(String)) : DAS.Model & List<&2, DAT.Obs>} 325 def dynamic_array_trace_at_string(ops): 326 DAP.trace_new_at(~String, ops) 327 328 law dynamic_array_trace_at_invariant_string: 329 for +ops: List<&2, DAT.Op> 330 DAST.Inv(String, Pair.fst(DA.DynArray<&2, String>, List<&2, DAT.Obs>, DA.run_at(~String, ops, DA.new_at(~String)))) 331 def dynamic_array_trace_at_invariant_string(ops): 332 DAP.trace_new_at_inv(~String, ops) 333 334 law dynamic_array_trace_limited_at_string: 335 for +k: Nat 336 for +ops: List<&2, DAT.Op> 337 {DAP.view(String, DA.run_at(~String, ops, DA.with_limit_at(~String, k))) == DAS.run(String, ops, DAS.with_limit(String, k)) : DAS.Model & List<&2, DAT.Obs>} 338 def dynamic_array_trace_limited_at_string(k, ops): 339 DAP.trace_with_limit_at(~String, k, ops) 340 341 law dynamic_array_trace_limited_at_invariant_string: 342 for +k: Nat 343 for +ops: List<&2, DAT.Op> 344 DAST.Inv(String, Pair.fst(DA.DynArray<&2, String>, List<&2, DAT.Obs>, DA.run_at(~String, ops, DA.with_limit_at(~String, k)))) 345 def dynamic_array_trace_limited_at_invariant_string(k, ops): 346 DAP.trace_with_limit_at_inv(~String, k, ops) 347 348 # ============================== deque ================================= 349 # Two lists (src/containers/deque.bend): the laws are about the deque of a 350 # Data shadow Sh{front, back} (DQSH.real); model = front ++ reverse(back). 351 # No premise: any finite trace, any size. Restated at U32 and String. 352 353 law deque_u32_new: 354 {DQSH.model(U32, DQSH.initial(U32)) == Nil{} : List<&2, U32>} 355 def deque_u32_new(): 356 DQP.new_abs(~U32) 357 358 law deque_u32_new_is_the_constructor: 359 {DQ.new(~U32) == DQSH.real(U32, DQSH.initial(U32)) : DQ.Deque} 360 def deque_u32_new_is_the_constructor(): 361 DQP.new_real(~U32) 362 363 law deque_u32_step: 364 for +sh: DQSH.Shadow 365 for +op: DQT.Op 366 DQK.StepOK(~U32, sh, op) 367 def deque_u32_step(sh, op): 368 DQP.step_ok(~U32, sh, op) 369 370 law deque_u32_shadow_unique: 371 for +a: DQSH.Shadow 372 for +b: DQSH.Shadow 373 for +e: {DQSH.real(U32, a) == DQSH.real(U32, b) : DQ.Deque} 374 {a == b : DQSH.Shadow} 375 def deque_u32_shadow_unique(a, b, e): 376 DQP.shadow_unique(~U32, a, b, e) 377 378 law deque_u32_trace: 379 for +ops: List<&2, DQT.Op> 380 DQTR.TraceOK(~U32, ops, DQSH.initial(U32)) 381 def deque_u32_trace(ops): 382 DQP.trace_new(~U32, ops) 383 384 law deque_string_new: 385 {DQSH.model(String, DQSH.initial(String)) == Nil{} : List<&2, String>} 386 def deque_string_new(): 387 DQP.new_abs(~String) 388 389 law deque_string_new_is_the_constructor: 390 {DQ.new(~String) == DQSH.real(String, DQSH.initial(String)) : DQ.Deque} 391 def deque_string_new_is_the_constructor(): 392 DQP.new_real(~String) 393 394 law deque_string_step: 395 for +sh: DQSH.Shadow 396 for +op: DQT.Op 397 DQK.StepOK(~String, sh, op) 398 def deque_string_step(sh, op): 399 DQP.step_ok(~String, sh, op) 400 401 law deque_string_shadow_unique: 402 for +a: DQSH.Shadow 403 for +b: DQSH.Shadow 404 for +e: {DQSH.real(String, a) == DQSH.real(String, b) : DQ.Deque} 405 {a == b : DQSH.Shadow} 406 def deque_string_shadow_unique(a, b, e): 407 DQP.shadow_unique(~String, a, b, e) 408 409 law deque_string_trace: 410 for +ops: List<&2, DQT.Op> 411 DQTR.TraceOK(~String, ops, DQSH.initial(String)) 412 def deque_string_trace(ops): 413 DQP.trace_new(~String, ops) 414 415 # ============================== queue ================================= 416 # Two lists (src/containers/queue.bend), independent of the deque; the 417 # same shadow form, no premise. 418 419 law queue_u32_new: 420 {QUSH.model(U32, QUSH.initial(U32)) == Nil{} : List<&2, U32>} 421 def queue_u32_new(): 422 QUP.new_abs(~U32) 423 424 law queue_u32_new_is_the_constructor: 425 {QU.new(~U32) == QUSH.real(U32, QUSH.initial(U32)) : QU.Queue} 426 def queue_u32_new_is_the_constructor(): 427 QUP.new_real(~U32) 428 429 law queue_u32_step: 430 for +sh: QUSH.Shadow 431 for +op: QUT.Op 432 QUST.StepOK(~U32, sh, op) 433 def queue_u32_step(sh, op): 434 QUP.step_ok(~U32, sh, op) 435 436 law queue_u32_shadow_unique: 437 for +a: QUSH.Shadow 438 for +b: QUSH.Shadow 439 for +e: {QUSH.real(U32, a) == QUSH.real(U32, b) : QU.Queue} 440 {a == b : QUSH.Shadow} 441 def queue_u32_shadow_unique(a, b, e): 442 QUP.shadow_unique(~U32, a, b, e) 443 444 law queue_u32_trace: 445 for +ops: List<&2, QUT.Op> 446 QUTR.TraceOK(~U32, ops, QUSH.initial(U32)) 447 def queue_u32_trace(ops): 448 QUP.trace_new(~U32, ops) 449 450 law queue_string_new: 451 {QUSH.model(String, QUSH.initial(String)) == Nil{} : List<&2, String>} 452 def queue_string_new(): 453 QUP.new_abs(~String) 454 455 law queue_string_new_is_the_constructor: 456 {QU.new(~String) == QUSH.real(String, QUSH.initial(String)) : QU.Queue} 457 def queue_string_new_is_the_constructor(): 458 QUP.new_real(~String) 459 460 law queue_string_step: 461 for +sh: QUSH.Shadow 462 for +op: QUT.Op 463 QUST.StepOK(~String, sh, op) 464 def queue_string_step(sh, op): 465 QUP.step_ok(~String, sh, op) 466 467 law queue_string_shadow_unique: 468 for +a: QUSH.Shadow 469 for +b: QUSH.Shadow 470 for +e: {QUSH.real(String, a) == QUSH.real(String, b) : QU.Queue} 471 {a == b : QUSH.Shadow} 472 def queue_string_shadow_unique(a, b, e): 473 QUP.shadow_unique(~String, a, b, e) 474 475 law queue_string_trace: 476 for +ops: List<&2, QUT.Op> 477 QUTR.TraceOK(~String, ops, QUSH.initial(String)) 478 def queue_string_trace(ops): 479 QUP.trace_new(~String, ops) 480 481 # =========================== binary_heap ============================== 482 # The block is a linear Base.Array, so -- as for dynamic_array, bitset and 483 # deque -- the laws are about the heap BUILT from a Data mirror tree 484 # (BHSH.real of a shadow). Generic over a comparator; restated at both 485 # checked instances. `room` is the representation's capacity condition: the 486 # size plus the elements still to be added stays below 2^q, q <= 31 (Base 487 # arrays have at most 2^31 slots); it does not bound the trace length. 488 489 law binary_heap_u32_new: 490 {BHSH.model(~U32, ~U32.cmp, BHSH.initial(~U32)) == Nil{} : List<&2, U32>} 491 def binary_heap_u32_new(): 492 BHP.new_abs(~U32, ~U32.cmp) 493 494 law binary_heap_u32_new_good: 495 {BHSH.good(~U32, ~U32.cmp, BHSH.initial(~U32)) == True{} : Bool} 496 def binary_heap_u32_new_good(): 497 BHP.new_inv(~U32, ~U32.cmp) 498 499 law binary_heap_u32_new_is_the_constructor: 500 {BH.new(~U32) == BHSH.real(~U32, BHSH.initial(~U32)) : BH.Heap} 501 def binary_heap_u32_new_is_the_constructor(): 502 BHP.new_real(~U32, ~U32.cmp) 503 504 law binary_heap_u32_abstraction_of_a_real_heap: 505 for +sh: BHSH.Shadow 506 {BHSH.abs(~U32, ~U32.cmp, BHSH.real(~U32, sh)) == BHSH.model(~U32, ~U32.cmp, sh) : List<&2, U32>} 507 def binary_heap_u32_abstraction_of_a_real_heap(sh): 508 BHP.abs_real(~U32, ~U32.cmp, sh) 509 510 law binary_heap_string_new: 511 {BHSH.model(~String, ~String.order, BHSH.initial(~String)) == Nil{} : List<&2, String>} 512 def binary_heap_string_new(): 513 BHP.new_abs(~String, ~String.order) 514 515 law binary_heap_string_new_is_the_constructor: 516 {BH.new(~String) == BHSH.real(~String, BHSH.initial(~String)) : BH.Heap} 517 def binary_heap_string_new_is_the_constructor(): 518 BHP.new_real(~String, ~String.order) 519 520 law binary_heap_string_abstraction_of_a_real_heap: 521 for +sh: BHSH.Shadow 522 {BHSH.abs(~String, ~String.order, BHSH.real(~String, sh)) == BHSH.model(~String, ~String.order, sh) : List<&2, String>} 523 def binary_heap_string_abstraction_of_a_real_heap(sh): 524 BHP.abs_real(~String, ~String.order, sh) 525 526 law binary_heap_u32_step: 527 for sh: BHSH.Shadow 528 for op: BHT.Op 529 for +g: {BHSH.good(~U32, ~U32.cmp, sh) == True{} : Bool} 530 for +q: Nat 531 for +hq: {Nat.is_le(q, 31n) == True{} : Bool} 532 for +room: {Nat.is_lt(Nat.add(BHSH.sh_size(~U32, sh), BHST.pushcost(~U32, op)), SCOM.pow2(q)) == True{} : Bool} 533 BHST.StepOK(~U32, ~U32.cmp, sh, op) 534 def binary_heap_u32_step(sh, op, g, q, hq, room): 535 BHP.u32_step_ok(sh, op, g, q, hq, room) 536 537 law binary_heap_u32_trace: 538 for +ops: List<&2, BHT.Op> 539 for +q: Nat 540 for +hq: {Nat.is_le(q, 31n) == True{} : Bool} 541 for +room: {Nat.is_lt(BHTR.pushes(~U32, ops), SCOM.pow2(q)) == True{} : Bool} 542 BHTR.TraceOK(~U32, ~U32.cmp, ops, BHSH.initial(~U32)) 543 def binary_heap_u32_trace(ops, q, hq, room): 544 BHP.u32_trace(ops, q, hq, room) 545 546 law binary_heap_u32_new_invariant: 547 BHSH.Inv(~U32, ~U32.cmp, BH.new(~U32)) 548 def binary_heap_u32_new_invariant(): 549 BHP.u32_new_inv() 550 551 law binary_heap_string_step: 552 for sh: BHSH.Shadow 553 for op: BHT.Op 554 for +g: {BHSH.good(~String, ~String.order, sh) == True{} : Bool} 555 for +q: Nat 556 for +hq: {Nat.is_le(q, 31n) == True{} : Bool} 557 for +room: {Nat.is_lt(Nat.add(BHSH.sh_size(~String, sh), BHST.pushcost(~String, op)), SCOM.pow2(q)) == True{} : Bool} 558 BHST.StepOK(~String, ~String.order, sh, op) 559 def binary_heap_string_step(sh, op, g, q, hq, room): 560 BHP.string_step_ok(sh, op, g, q, hq, room) 561 562 law binary_heap_string_trace: 563 for +ops: List<&2, BHT.Op> 564 for +q: Nat 565 for +hq: {Nat.is_le(q, 31n) == True{} : Bool} 566 for +room: {Nat.is_lt(BHTR.pushes(~String, ops), SCOM.pow2(q)) == True{} : Bool} 567 BHTR.TraceOK(~String, ~String.order, ops, BHSH.initial(~String)) 568 def binary_heap_string_trace(ops, q, hq, room): 569 BHP.string_trace(ops, q, hq, room) 570 571 law binary_heap_string_new_invariant: 572 BHSH.Inv(~String, ~String.order, BH.new(~String)) 573 def binary_heap_string_new_invariant(): 574 BHP.string_new_inv() 575 576 # ============================== bitset ================================ 577 578 law bitset_new: 579 for +n: Nat 580 for +h: {Nat.is_le(n, Nat.mul(SCOM.pow2(BI.depth_for(n)), 32n)) == True{} : Bool} 581 {BIST.model(BITR.initial(n)) == BIS.new(n) : List<&2, Bool>} 582 def bitset_new(n, h): 583 BIP.new_abs(n, h) 584 585 law bitset_new_invariant: 586 for +n: Nat 587 for +h: {Nat.is_le(n, Nat.mul(SCOM.pow2(BI.depth_for(n)), 32n)) == True{} : Bool} 588 {BIST.good(BITR.initial(n)) == True{} : Bool} 589 def bitset_new_invariant(n, h): 590 BIP.new_inv(n, h) 591 592 law bitset_new_is_the_constructor: 593 for +n: Nat 594 {BI.new(n) == BIST.real(BITR.initial(n)) : BI.Bitset} 595 def bitset_new_is_the_constructor(n): 596 BIP.new_real(n) 597 598 law bitset_from_bools: 599 for +ys: List<&2, Bool> 600 for +hf: {Nat.is_le(BI.bool_count(ys), Nat.mul(SCOM.pow2(BI.depth_for(BI.bool_count(ys))), 32n)) == True{} : Bool} 601 BISP.FromOK(ys) 602 def bitset_from_bools(ys, hf): 603 BIP.from_bools(ys, hf) 604 605 law bitset_step: 606 for sh: BIST.Sh 607 for op: BIT.Op 608 for +g: {BIST.good(sh) == True{} : Bool} 609 BISP.StepOK(sh, op) 610 def bitset_step(sh, op, g): 611 BIP.step_ok(sh, op, g) 612 613 law bitset_shadow_unique: 614 for +a: BIST.Sh 615 for +b: BIST.Sh 616 for +e: {BIST.real(a) == BIST.real(b) : BI.Bitset} 617 {a == b : BIST.Sh} 618 def bitset_shadow_unique(a, b, e): 619 BIP.shadow_unique(a, b, e) 620 621 law bitset_trace: 622 for +n: Nat 623 for +ops: List<&2, BIT.Op> 624 for +h: {Nat.is_le(n, Nat.mul(SCOM.pow2(BI.depth_for(n)), 32n)) == True{} : Bool} 625 BITR.TraceOK(ops, BITR.initial(n)) 626 def bitset_trace(n, ops, h): 627 BIP.trace_new(n, ops, h) 628 629 # ======================== legacy balanced_search_tree ======================== 630 # The laws below apply to the retained recursive implementation only. 631 # New indexed TreeMap component laws are in TREE_MAP_COMPONENT_PROOF.bend. 632 # Red-black binary tree ordered map (reference/legacy_balanced_search_tree.bend). The 633 # proofs are templates over a comparator with total-order laws; the laws are 634 # stated at the two instances src/ exposes: (U32, U32.cmp) and 635 # (String, String.order). Values are an erased type. The invariant 636 # (strictly increasing keys, red-black balance, cached size) is kept by 637 # every operation, and balance is also restated in textbook form. 638 639 # ============================== bitlist =============================== 640 641 law bitlist_new_is_the_constructor: 642 {BLI.new() == BLST.real(BLTR.initial(None{})) : BLI.Bitlist} 643 def bitlist_new_is_the_constructor(): 644 BLP.new_real() 645 646 law bitlist_new: 647 {BLST.model(BLTR.initial(None{})) == BLS.new() : BLS.Model} 648 def bitlist_new(): 649 BLP.new_model() 650 651 law bitlist_with_limit: 652 for +n: Nat 653 {BLST.model(BLTR.initial(Some{n})) == BLS.with_limit(n) : BLS.Model} 654 def bitlist_with_limit(n): 655 BLP.with_limit_model(n) 656 657 law bitlist_step: 658 for +sh: BLST.Sh 659 for +op: BLT.Op 660 for +g: {BLST.good(sh) == True{} : Bool} 661 BLSP.StepOK(sh, op) 662 def bitlist_step(sh, op, g): 663 BLP.step_ok(sh, op, g) 664 665 law bitlist_trace: 666 for +ops: List<&2, BLT.Op> 667 BLTR.TraceOK(ops, BLTR.initial(None{})) 668 def bitlist_trace(ops): 669 BLP.trace_new(ops) 670 671 law bitlist_trace_limited: 672 for +n: Nat 673 for +ops: List<&2, BLT.Op> 674 BLTR.TraceOK(ops, BLTR.initial(Some{n})) 675 def bitlist_trace_limited(n, ops): 676 BLP.trace_with_limit(n, ops) 677 678 law bitlist_from_bools: 679 for +bs: List<&2, Bool> 680 BLTR.FromOK(bs, BLTR.initial(None{})) 681 def bitlist_from_bools(bs): 682 BLP.from_bools(bs)