proofs/END_TO_END.bend
bend-collections-laws-containers@1.0.0.0 · 682 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
6import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as DAS
7import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as DAT
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/proof.bend as DAP
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as DAST
10import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as DQ
11import bend-collections-laws-containers@1.0.0.0/spec/containers/deque.bend as DQS
12import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as DQT
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/proof.bend as DQP
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as DQSH
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/stepok.bend as DQK
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/trace.bend as DQTR
17import bend-collections-laws-containers@1.0.0.0/src/containers/queue.bend as QU
18import bend-collections-laws-containers@1.0.0.0/spec/containers/queue.bend as QUS
19import bend-collections-laws-containers@1.0.0.0/src/containers/types/queue.bend as QUT
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/proof.bend as QUP
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/state.bend as QUSH
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/steps.bend as QUST
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/trace.bend as QUTR
24import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
25import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as BH
26import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as BHS
27import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as BHT
28import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/proof.bend as BHP
29import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/state.bend as BHSH
30import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/steps.bend as BHST
31import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/trace.bend as BHTR
32import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as BI
33import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SCOM
34import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as BIS
35import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitset.bend as BIT
36import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/proof.bend as BIP
37import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as BIST
38import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/steps.bend as BISP
39import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/trace.bend as BITR
40import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as BLI
41import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitlist.bend as BLT
42import bend-collections-laws-containers@1.0.0.0/spec/containers/bitlist.bend as BLS
43import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/state.bend as BLST
44import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/steps.bend as BLSP
45import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/trace.bend as BLTR
46import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/proof.bend as BLP
47import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/recursive.bend as BTS
48import bend-collections-laws-containers@1.0.0.0/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/<id>.bend). PROOF.bend imports this file.
53
54# ============================ retained LRU ============================
55
56law array_get_after_set_same:
57 for -T: Data
58 for +d: Nat
59 for +t: AR.Tree<T>
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> & T}
68def 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
71law array_get_after_set_other:
72 for -T: Data
73 for +d: Nat
74 for +t: AR.Tree<T>
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> & T}
88def 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
91law 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<T>}
96def array_new(T, d, v):
97 AR.new(T, d, v)
98
99# ============================ dynamic_array ===========================
100
101law dynamic_array_new:
102 for -T: Data
103 {DAST.abs(T, DA.new(T)) == DAS.new(T) : DAS.Model<T>}
104def dynamic_array_new(T):
105 DAP.new_abs(T)
106
107law dynamic_array_new_invariant:
108 for -T: Data
109 DAST.Inv(T, DA.new(T))
110def dynamic_array_new_invariant(T):
111 DAP.new_inv(T)
112
113law 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<T>}
117def dynamic_array_with_limit(T, k):
118 DAP.with_limit_abs(T, k)
119
120law dynamic_array_step:
121 for -T: Data
122 for +sh: DAST.Shadow<T>
123 for +op: DAT.Op<T>
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<T> & DAT.Obs<T>}
126def dynamic_array_step(T, sh, op, g):
127 DAP.step_refines(T, sh, op, g)
128
129law dynamic_array_step_invariant:
130 for -T: Data
131 for +sh: DAST.Shadow<T>
132 for +op: DAT.Op<T>
133 for +g: {DAST.good(T, sh) == True{} : Bool}
134 DAST.Inv(T, Pair.fst(DA.DynArray<&2, T>, DAT.Obs<T>, DA.step(T, DAST.real(T, sh), op)))
135def dynamic_array_step_invariant(T, sh, op, g):
136 DAP.step_preserves(T, sh, op, g)
137
138law dynamic_array_trace:
139 for -T: Data
140 for +ops: List<&2, DAT.Op<T>>
141 {DAP.view(T, DA.run(T, ops, DA.new(T))) == DAS.run(T, ops, DAS.new(T)) : DAS.Model<T> & List<&2, DAT.Obs<T>>}
142def dynamic_array_trace(T, ops):
143 DAP.trace_new(T, ops)
144
145law dynamic_array_trace_invariant:
146 for -T: Data
147 for +ops: List<&2, DAT.Op<T>>
148 DAST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, DAT.Obs<T>>, DA.run(T, ops, DA.new(T))))
149def dynamic_array_trace_invariant(T, ops):
150 DAP.trace_new_inv(T, ops)
151
152law dynamic_array_trace_limited:
153 for -T: Data
154 for +k: Nat
155 for +ops: List<&2, DAT.Op<T>>
156 {DAP.view(T, DA.run(T, ops, DA.with_limit(T, k))) == DAS.run(T, ops, DAS.with_limit(T, k)) : DAS.Model<T> & List<&2, DAT.Obs<T>>}
157def dynamic_array_trace_limited(T, k, ops):
158 DAP.trace_with_limit(T, k, ops)
159
160law dynamic_array_trace_limited_invariant:
161 for -T: Data
162 for +k: Nat
163 for +ops: List<&2, DAT.Op<T>>
164 DAST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, DAT.Obs<T>>, DA.run(T, ops, DA.with_limit(T, k))))
165def 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
174law dynamic_array_new_at_u32:
175 {DAST.abs(U32, DA.new_at(~U32)) == DAS.new(U32) : DAS.Model<U32>}
176def dynamic_array_new_at_u32():
177 DAP.new_at_abs(~U32)
178
179law dynamic_array_new_at_invariant_u32:
180 DAST.Inv(U32, DA.new_at(~U32))
181def dynamic_array_new_at_invariant_u32():
182 DAP.new_at_inv(~U32)
183
184law 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<U32>}
187def dynamic_array_with_limit_at_u32(k):
188 DAP.with_limit_at_abs(~U32, k)
189
190law dynamic_array_step_at_u32:
191 for +sh: DAST.Shadow<U32>
192 for +op: DAT.Op<U32>
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<U32> & DAT.Obs<U32>}
195def dynamic_array_step_at_u32(sh, op, g):
196 DAP.step_at_refines(~U32, sh, op, g)
197
198law dynamic_array_step_at_invariant_u32:
199 for +sh: DAST.Shadow<U32>
200 for +op: DAT.Op<U32>
201 for +g: {DAST.good(U32, sh) == True{} : Bool}
202 DAST.Inv(U32, Pair.fst(DA.DynArray<&2, U32>, DAT.Obs<U32>, DA.step_at(~U32, DAST.real(U32, sh), op)))
203def dynamic_array_step_at_invariant_u32(sh, op, g):
204 DAP.step_at_preserves(~U32, sh, op, g)
205
206law dynamic_array_trace_at_u32:
207 for +ops: List<&2, DAT.Op<U32>>
208 {DAP.view(U32, DA.run_at(~U32, ops, DA.new_at(~U32))) == DAS.run(U32, ops, DAS.new(U32)) : DAS.Model<U32> & List<&2, DAT.Obs<U32>>}
209def dynamic_array_trace_at_u32(ops):
210 DAP.trace_new_at(~U32, ops)
211
212law dynamic_array_trace_at_invariant_u32:
213 for +ops: List<&2, DAT.Op<U32>>
214 DAST.Inv(U32, Pair.fst(DA.DynArray<&2, U32>, List<&2, DAT.Obs<U32>>, DA.run_at(~U32, ops, DA.new_at(~U32))))
215def dynamic_array_trace_at_invariant_u32(ops):
216 DAP.trace_new_at_inv(~U32, ops)
217
218law dynamic_array_trace_limited_at_u32:
219 for +k: Nat
220 for +ops: List<&2, DAT.Op<U32>>
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<U32> & List<&2, DAT.Obs<U32>>}
222def dynamic_array_trace_limited_at_u32(k, ops):
223 DAP.trace_with_limit_at(~U32, k, ops)
224
225law dynamic_array_trace_limited_at_invariant_u32:
226 for +k: Nat
227 for +ops: List<&2, DAT.Op<U32>>
228 DAST.Inv(U32, Pair.fst(DA.DynArray<&2, U32>, List<&2, DAT.Obs<U32>>, DA.run_at(~U32, ops, DA.with_limit_at(~U32, k))))
229def dynamic_array_trace_limited_at_invariant_u32(k, ops):
230 DAP.trace_with_limit_at_inv(~U32, k, ops)
231
232law dynamic_array_new_at_nat:
233 {DAST.abs(Nat, DA.new_at(~Nat)) == DAS.new(Nat) : DAS.Model<Nat>}
234def dynamic_array_new_at_nat():
235 DAP.new_at_abs(~Nat)
236
237law dynamic_array_new_at_invariant_nat:
238 DAST.Inv(Nat, DA.new_at(~Nat))
239def dynamic_array_new_at_invariant_nat():
240 DAP.new_at_inv(~Nat)
241
242law 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<Nat>}
245def dynamic_array_with_limit_at_nat(k):
246 DAP.with_limit_at_abs(~Nat, k)
247
248law dynamic_array_step_at_nat:
249 for +sh: DAST.Shadow<Nat>
250 for +op: DAT.Op<Nat>
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<Nat> & DAT.Obs<Nat>}
253def dynamic_array_step_at_nat(sh, op, g):
254 DAP.step_at_refines(~Nat, sh, op, g)
255
256law dynamic_array_step_at_invariant_nat:
257 for +sh: DAST.Shadow<Nat>
258 for +op: DAT.Op<Nat>
259 for +g: {DAST.good(Nat, sh) == True{} : Bool}
260 DAST.Inv(Nat, Pair.fst(DA.DynArray<&2, Nat>, DAT.Obs<Nat>, DA.step_at(~Nat, DAST.real(Nat, sh), op)))
261def dynamic_array_step_at_invariant_nat(sh, op, g):
262 DAP.step_at_preserves(~Nat, sh, op, g)
263
264law dynamic_array_trace_at_nat:
265 for +ops: List<&2, DAT.Op<Nat>>
266 {DAP.view(Nat, DA.run_at(~Nat, ops, DA.new_at(~Nat))) == DAS.run(Nat, ops, DAS.new(Nat)) : DAS.Model<Nat> & List<&2, DAT.Obs<Nat>>}
267def dynamic_array_trace_at_nat(ops):
268 DAP.trace_new_at(~Nat, ops)
269
270law dynamic_array_trace_at_invariant_nat:
271 for +ops: List<&2, DAT.Op<Nat>>
272 DAST.Inv(Nat, Pair.fst(DA.DynArray<&2, Nat>, List<&2, DAT.Obs<Nat>>, DA.run_at(~Nat, ops, DA.new_at(~Nat))))
273def dynamic_array_trace_at_invariant_nat(ops):
274 DAP.trace_new_at_inv(~Nat, ops)
275
276law dynamic_array_trace_limited_at_nat:
277 for +k: Nat
278 for +ops: List<&2, DAT.Op<Nat>>
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<Nat> & List<&2, DAT.Obs<Nat>>}
280def dynamic_array_trace_limited_at_nat(k, ops):
281 DAP.trace_with_limit_at(~Nat, k, ops)
282
283law dynamic_array_trace_limited_at_invariant_nat:
284 for +k: Nat
285 for +ops: List<&2, DAT.Op<Nat>>
286 DAST.Inv(Nat, Pair.fst(DA.DynArray<&2, Nat>, List<&2, DAT.Obs<Nat>>, DA.run_at(~Nat, ops, DA.with_limit_at(~Nat, k))))
287def dynamic_array_trace_limited_at_invariant_nat(k, ops):
288 DAP.trace_with_limit_at_inv(~Nat, k, ops)
289
290law dynamic_array_new_at_string:
291 {DAST.abs(String, DA.new_at(~String)) == DAS.new(String) : DAS.Model<String>}
292def dynamic_array_new_at_string():
293 DAP.new_at_abs(~String)
294
295law dynamic_array_new_at_invariant_string:
296 DAST.Inv(String, DA.new_at(~String))
297def dynamic_array_new_at_invariant_string():
298 DAP.new_at_inv(~String)
299
300law 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<String>}
303def dynamic_array_with_limit_at_string(k):
304 DAP.with_limit_at_abs(~String, k)
305
306law dynamic_array_step_at_string:
307 for +sh: DAST.Shadow<String>
308 for +op: DAT.Op<String>
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<String> & DAT.Obs<String>}
311def dynamic_array_step_at_string(sh, op, g):
312 DAP.step_at_refines(~String, sh, op, g)
313
314law dynamic_array_step_at_invariant_string:
315 for +sh: DAST.Shadow<String>
316 for +op: DAT.Op<String>
317 for +g: {DAST.good(String, sh) == True{} : Bool}
318 DAST.Inv(String, Pair.fst(DA.DynArray<&2, String>, DAT.Obs<String>, DA.step_at(~String, DAST.real(String, sh), op)))
319def dynamic_array_step_at_invariant_string(sh, op, g):
320 DAP.step_at_preserves(~String, sh, op, g)
321
322law dynamic_array_trace_at_string:
323 for +ops: List<&2, DAT.Op<String>>
324 {DAP.view(String, DA.run_at(~String, ops, DA.new_at(~String))) == DAS.run(String, ops, DAS.new(String)) : DAS.Model<String> & List<&2, DAT.Obs<String>>}
325def dynamic_array_trace_at_string(ops):
326 DAP.trace_new_at(~String, ops)
327
328law dynamic_array_trace_at_invariant_string:
329 for +ops: List<&2, DAT.Op<String>>
330 DAST.Inv(String, Pair.fst(DA.DynArray<&2, String>, List<&2, DAT.Obs<String>>, DA.run_at(~String, ops, DA.new_at(~String))))
331def dynamic_array_trace_at_invariant_string(ops):
332 DAP.trace_new_at_inv(~String, ops)
333
334law dynamic_array_trace_limited_at_string:
335 for +k: Nat
336 for +ops: List<&2, DAT.Op<String>>
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<String> & List<&2, DAT.Obs<String>>}
338def dynamic_array_trace_limited_at_string(k, ops):
339 DAP.trace_with_limit_at(~String, k, ops)
340
341law dynamic_array_trace_limited_at_invariant_string:
342 for +k: Nat
343 for +ops: List<&2, DAT.Op<String>>
344 DAST.Inv(String, Pair.fst(DA.DynArray<&2, String>, List<&2, DAT.Obs<String>>, DA.run_at(~String, ops, DA.with_limit_at(~String, k))))
345def 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
353law deque_u32_new:
354 {DQSH.model(U32, DQSH.initial(U32)) == Nil{} : List<&2, U32>}
355def deque_u32_new():
356 DQP.new_abs(~U32)
357
358law deque_u32_new_is_the_constructor:
359 {DQ.new(~U32) == DQSH.real(U32, DQSH.initial(U32)) : DQ.Deque<U32>}
360def deque_u32_new_is_the_constructor():
361 DQP.new_real(~U32)
362
363law deque_u32_step:
364 for +sh: DQSH.Shadow<U32>
365 for +op: DQT.Op<U32>
366 DQK.StepOK(~U32, sh, op)
367def deque_u32_step(sh, op):
368 DQP.step_ok(~U32, sh, op)
369
370law deque_u32_shadow_unique:
371 for +a: DQSH.Shadow<U32>
372 for +b: DQSH.Shadow<U32>
373 for +e: {DQSH.real(U32, a) == DQSH.real(U32, b) : DQ.Deque<U32>}
374 {a == b : DQSH.Shadow<U32>}
375def deque_u32_shadow_unique(a, b, e):
376 DQP.shadow_unique(~U32, a, b, e)
377
378law deque_u32_trace:
379 for +ops: List<&2, DQT.Op<U32>>
380 DQTR.TraceOK(~U32, ops, DQSH.initial(U32))
381def deque_u32_trace(ops):
382 DQP.trace_new(~U32, ops)
383
384law deque_string_new:
385 {DQSH.model(String, DQSH.initial(String)) == Nil{} : List<&2, String>}
386def deque_string_new():
387 DQP.new_abs(~String)
388
389law deque_string_new_is_the_constructor:
390 {DQ.new(~String) == DQSH.real(String, DQSH.initial(String)) : DQ.Deque<String>}
391def deque_string_new_is_the_constructor():
392 DQP.new_real(~String)
393
394law deque_string_step:
395 for +sh: DQSH.Shadow<String>
396 for +op: DQT.Op<String>
397 DQK.StepOK(~String, sh, op)
398def deque_string_step(sh, op):
399 DQP.step_ok(~String, sh, op)
400
401law deque_string_shadow_unique:
402 for +a: DQSH.Shadow<String>
403 for +b: DQSH.Shadow<String>
404 for +e: {DQSH.real(String, a) == DQSH.real(String, b) : DQ.Deque<String>}
405 {a == b : DQSH.Shadow<String>}
406def deque_string_shadow_unique(a, b, e):
407 DQP.shadow_unique(~String, a, b, e)
408
409law deque_string_trace:
410 for +ops: List<&2, DQT.Op<String>>
411 DQTR.TraceOK(~String, ops, DQSH.initial(String))
412def 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
419law queue_u32_new:
420 {QUSH.model(U32, QUSH.initial(U32)) == Nil{} : List<&2, U32>}
421def queue_u32_new():
422 QUP.new_abs(~U32)
423
424law queue_u32_new_is_the_constructor:
425 {QU.new(~U32) == QUSH.real(U32, QUSH.initial(U32)) : QU.Queue<U32>}
426def queue_u32_new_is_the_constructor():
427 QUP.new_real(~U32)
428
429law queue_u32_step:
430 for +sh: QUSH.Shadow<U32>
431 for +op: QUT.Op<U32>
432 QUST.StepOK(~U32, sh, op)
433def queue_u32_step(sh, op):
434 QUP.step_ok(~U32, sh, op)
435
436law queue_u32_shadow_unique:
437 for +a: QUSH.Shadow<U32>
438 for +b: QUSH.Shadow<U32>
439 for +e: {QUSH.real(U32, a) == QUSH.real(U32, b) : QU.Queue<U32>}
440 {a == b : QUSH.Shadow<U32>}
441def queue_u32_shadow_unique(a, b, e):
442 QUP.shadow_unique(~U32, a, b, e)
443
444law queue_u32_trace:
445 for +ops: List<&2, QUT.Op<U32>>
446 QUTR.TraceOK(~U32, ops, QUSH.initial(U32))
447def queue_u32_trace(ops):
448 QUP.trace_new(~U32, ops)
449
450law queue_string_new:
451 {QUSH.model(String, QUSH.initial(String)) == Nil{} : List<&2, String>}
452def queue_string_new():
453 QUP.new_abs(~String)
454
455law queue_string_new_is_the_constructor:
456 {QU.new(~String) == QUSH.real(String, QUSH.initial(String)) : QU.Queue<String>}
457def queue_string_new_is_the_constructor():
458 QUP.new_real(~String)
459
460law queue_string_step:
461 for +sh: QUSH.Shadow<String>
462 for +op: QUT.Op<String>
463 QUST.StepOK(~String, sh, op)
464def queue_string_step(sh, op):
465 QUP.step_ok(~String, sh, op)
466
467law queue_string_shadow_unique:
468 for +a: QUSH.Shadow<String>
469 for +b: QUSH.Shadow<String>
470 for +e: {QUSH.real(String, a) == QUSH.real(String, b) : QU.Queue<String>}
471 {a == b : QUSH.Shadow<String>}
472def queue_string_shadow_unique(a, b, e):
473 QUP.shadow_unique(~String, a, b, e)
474
475law queue_string_trace:
476 for +ops: List<&2, QUT.Op<String>>
477 QUTR.TraceOK(~String, ops, QUSH.initial(String))
478def 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
489law binary_heap_u32_new:
490 {BHSH.model(~U32, ~U32.cmp, BHSH.initial(~U32)) == Nil{} : List<&2, U32>}
491def binary_heap_u32_new():
492 BHP.new_abs(~U32, ~U32.cmp)
493
494law binary_heap_u32_new_good:
495 {BHSH.good(~U32, ~U32.cmp, BHSH.initial(~U32)) == True{} : Bool}
496def binary_heap_u32_new_good():
497 BHP.new_inv(~U32, ~U32.cmp)
498
499law binary_heap_u32_new_is_the_constructor:
500 {BH.new(~U32) == BHSH.real(~U32, BHSH.initial(~U32)) : BH.Heap<U32>}
501def binary_heap_u32_new_is_the_constructor():
502 BHP.new_real(~U32, ~U32.cmp)
503
504law binary_heap_u32_abstraction_of_a_real_heap:
505 for +sh: BHSH.Shadow<U32>
506 {BHSH.abs(~U32, ~U32.cmp, BHSH.real(~U32, sh)) == BHSH.model(~U32, ~U32.cmp, sh) : List<&2, U32>}
507def binary_heap_u32_abstraction_of_a_real_heap(sh):
508 BHP.abs_real(~U32, ~U32.cmp, sh)
509
510law binary_heap_string_new:
511 {BHSH.model(~String, ~String.order, BHSH.initial(~String)) == Nil{} : List<&2, String>}
512def binary_heap_string_new():
513 BHP.new_abs(~String, ~String.order)
514
515law binary_heap_string_new_is_the_constructor:
516 {BH.new(~String) == BHSH.real(~String, BHSH.initial(~String)) : BH.Heap<String>}
517def binary_heap_string_new_is_the_constructor():
518 BHP.new_real(~String, ~String.order)
519
520law binary_heap_string_abstraction_of_a_real_heap:
521 for +sh: BHSH.Shadow<String>
522 {BHSH.abs(~String, ~String.order, BHSH.real(~String, sh)) == BHSH.model(~String, ~String.order, sh) : List<&2, String>}
523def binary_heap_string_abstraction_of_a_real_heap(sh):
524 BHP.abs_real(~String, ~String.order, sh)
525
526law binary_heap_u32_step:
527 for sh: BHSH.Shadow<U32>
528 for op: BHT.Op<U32>
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)
534def binary_heap_u32_step(sh, op, g, q, hq, room):
535 BHP.u32_step_ok(sh, op, g, q, hq, room)
536
537law binary_heap_u32_trace:
538 for +ops: List<&2, BHT.Op<U32>>
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))
543def binary_heap_u32_trace(ops, q, hq, room):
544 BHP.u32_trace(ops, q, hq, room)
545
546law binary_heap_u32_new_invariant:
547 BHSH.Inv(~U32, ~U32.cmp, BH.new(~U32))
548def binary_heap_u32_new_invariant():
549 BHP.u32_new_inv()
550
551law binary_heap_string_step:
552 for sh: BHSH.Shadow<String>
553 for op: BHT.Op<String>
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)
559def binary_heap_string_step(sh, op, g, q, hq, room):
560 BHP.string_step_ok(sh, op, g, q, hq, room)
561
562law binary_heap_string_trace:
563 for +ops: List<&2, BHT.Op<String>>
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))
568def binary_heap_string_trace(ops, q, hq, room):
569 BHP.string_trace(ops, q, hq, room)
570
571law binary_heap_string_new_invariant:
572 BHSH.Inv(~String, ~String.order, BH.new(~String))
573def binary_heap_string_new_invariant():
574 BHP.string_new_inv()
575
576# ============================== bitset ================================
577
578law 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>}
582def bitset_new(n, h):
583 BIP.new_abs(n, h)
584
585law 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}
589def bitset_new_invariant(n, h):
590 BIP.new_inv(n, h)
591
592law bitset_new_is_the_constructor:
593 for +n: Nat
594 {BI.new(n) == BIST.real(BITR.initial(n)) : BI.Bitset}
595def bitset_new_is_the_constructor(n):
596 BIP.new_real(n)
597
598law 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)
602def bitset_from_bools(ys, hf):
603 BIP.from_bools(ys, hf)
604
605law 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)
610def bitset_step(sh, op, g):
611 BIP.step_ok(sh, op, g)
612
613law 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}
618def bitset_shadow_unique(a, b, e):
619 BIP.shadow_unique(a, b, e)
620
621law 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))
626def 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
641law bitlist_new_is_the_constructor:
642 {BLI.new() == BLST.real(BLTR.initial(None{})) : BLI.Bitlist}
643def bitlist_new_is_the_constructor():
644 BLP.new_real()
645
646law bitlist_new:
647 {BLST.model(BLTR.initial(None{})) == BLS.new() : BLS.Model}
648def bitlist_new():
649 BLP.new_model()
650
651law bitlist_with_limit:
652 for +n: Nat
653 {BLST.model(BLTR.initial(Some{n})) == BLS.with_limit(n) : BLS.Model}
654def bitlist_with_limit(n):
655 BLP.with_limit_model(n)
656
657law 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)
662def bitlist_step(sh, op, g):
663 BLP.step_ok(sh, op, g)
664
665law bitlist_trace:
666 for +ops: List<&2, BLT.Op>
667 BLTR.TraceOK(ops, BLTR.initial(None{}))
668def bitlist_trace(ops):
669 BLP.trace_new(ops)
670
671law bitlist_trace_limited:
672 for +n: Nat
673 for +ops: List<&2, BLT.Op>
674 BLTR.TraceOK(ops, BLTR.initial(Some{n}))
675def bitlist_trace_limited(n, ops):
676 BLP.trace_with_limit(n, ops)
677
678law bitlist_from_bools:
679 for +bs: List<&2, Bool>
680 BLTR.FromOK(bs, BLTR.initial(None{}))
681def bitlist_from_bools(bs):
682 BLP.from_bools(bs)