LAWS.bend
bend-kit-collections@0.1.3.0 · 711 lines · 0 definitions
1import Base
2import bend-kit-collections@0.1.3.0/omap.bend as O
3import bend-kit-collections@0.1.3.0/hmap.bend as M
4import bend-kit-collections@0.1.3.0/vec.bend as V
5import bend-kit-collections@0.1.3.0/deque.bend as D
6import bend-kit-collections@0.1.3.0/heap.bend as H
7import bend-kit-collections@0.1.3.0/order.bend as Order
8
9def scmp.fin(r: (String & String) & Cmp) -> Cmp:
10 (ab, c) = r
11 c
12
13def scmp(a: String, b: String) -> Cmp:
14 scmp.fin(String.cmp(a, b))
15
16def m3() -> O.OMap<U32, U32>:
17 m = O.OMap.put(~U32, ~U32, ~U32.cmp, O.OMap.new(U32, U32), 5, 50)
18 m = O.OMap.put(~U32, ~U32, ~U32.cmp, m, 1, 10)
19 O.OMap.put(~U32, ~U32, ~U32.cmp, m, 3, 30)
20
21def m7.go(n: Nat, +i: U32, m: O.OMap<U32, U32>) -> O.OMap<U32, U32>:
22 match n:
23 case 0n:
24 m
25 case 1n+p:
26 m7.go(p, (i + 1 : U32), O.OMap.put(~U32, ~U32, ~U32.cmp, m, i, (i * 10 : U32)))
27
28def m7() -> O.OMap<U32, U32>:
29 m7.go(7n, 1, O.OMap.new(U32, U32))
30
31law omap_keys_ascending_puts:
32 {O.OMap.keys(U32, U32, m7()) == [1, 2, 3, 4, 5, 6, 7] : List<&2, U32>}
33
34law omap_size_del:
35 {O.OMap.size(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4)) == 6 : U32}
36
37law omap_get_after_rotations:
38 {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4), 6)
39 == Some{60} : Maybe<&2, U32>}
40
41law omap_keys_del_root:
42 {O.OMap.keys(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4))
43 == [1, 2, 3, 5, 6, 7] : List<&2, U32>}
44
45law omap_get_put:
46 {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 4, 40), 4)
47 == Some{40} : Maybe<&2, U32>}
48
49law omap_get_put_replace:
50 {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 3, 33), 3)
51 == Some{33} : Maybe<&2, U32>}
52
53law omap_get_put_other:
54 {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 4, 40), 3)
55 == O.OMap.get(~U32, ~U32, ~U32.cmp, m3(), 3) : Maybe<&2, U32>}
56
57law omap_get_missing:
58 {O.OMap.get(~U32, ~U32, ~U32.cmp, m3(), 2) == None{} : Maybe<&2, U32>}
59
60law omap_keys_sorted:
61 {O.OMap.keys(U32, U32, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 4, 40))
62 == [1, 3, 4, 5] : List<&2, U32>}
63
64law omap_size_replace:
65 {O.OMap.size(U32, U32, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 5, 55)) == 3 : U32}
66
67law omap_get_del:
68 {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.del(~U32, ~U32, ~U32.cmp, m3(), 3), 3)
69 == None{} : Maybe<&2, U32>}
70
71law omap_get_del_other:
72 {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.del(~U32, ~U32, ~U32.cmp, m3(), 3), 5)
73 == Some{50} : Maybe<&2, U32>}
74
75law omap_keys_del:
76 {O.OMap.keys(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m3(), 5))
77 == [1, 3] : List<&2, U32>}
78
79law omap_string_keys:
80 {O.OMap.keys(String, U32,
81 O.OMap.put(~String, ~U32, ~scmp,
82 O.OMap.put(~String, ~U32, ~scmp, O.OMap.new(String, U32), "b", 2),
83 "a", 1))
84 == ["a", "b"] : List<&2, String>}
85
86law oset_to_list:
87 {O.OSet.to_list(U32,
88 O.OSet.add(~U32, ~U32.cmp, O.OSet.add(~U32, ~U32.cmp,
89 O.OSet.add(~U32, ~U32.cmp, O.OSet.new(U32), 3), 1), 3))
90 == [1, 3] : List<&2, U32>}
91
92law oset_has_del:
93 {O.OSet.has(~U32, ~U32.cmp,
94 O.OSet.del(~U32, ~U32.cmp, O.OSet.add(~U32, ~U32.cmp, O.OSet.new(U32), 3), 3), 3)
95 == False{} : Bool}
96
97# The laws below hold for every comparator that is a total order, with EQ
98# meaning equal keys.
99def flip(c: Cmp) -> Cmp:
100 match c:
101 case LT{}:
102 GT{}
103 case EQ{}:
104 EQ{}
105 case GT{}:
106 LT{}
107
108def above(~K: Data, ~cmp: K -> K -> Cmp, lb: Maybe<&2, K>, +k: K) -> Bool:
109 match lb:
110 case None{}:
111 True{}
112 case Some{b}:
113 Cmp.is_lt(cmp(b, k))
114
115def below(~K: Data, ~cmp: K -> K -> Cmp, ub: Maybe<&2, K>, +k: K) -> Bool:
116 match ub:
117 case None{}:
118 True{}
119 case Some{b}:
120 Cmp.is_lt(cmp(k, b))
121
122# Every key of m lies strictly between the bounds, in search-tree order.
123def bounded(
124 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap<K, V>, +lb: Maybe<&2, K>,
125 +ub: Maybe<&2, K>
126) -> Bool:
127 match m:
128 case O.OTip{}:
129 True{}
130 case O.OBin{s, +k, v, lo, hi}:
131 above(~K, ~cmp, lb, k) && below(~K, ~cmp, ub, k)
132 && bounded(~K, ~V, ~cmp, lo, lb, Some{k})
133 && bounded(~K, ~V, ~cmp, hi, Some{k}, ub)
134
135def searchtree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap<K, V>) -> Bool:
136 bounded(~K, ~V, ~cmp, m, None{}, None{})
137
138def sorted.go(~K: Data, ~cmp: K -> K -> Cmp, xs: List<&2, K>, +prev: K) -> Bool:
139 match xs:
140 case Nil{}:
141 True{}
142 case Con{+h, t}:
143 Cmp.is_lt(cmp(prev, h)) && sorted.go(~K, ~cmp, t, h)
144
145def sorted(~K: Data, ~cmp: K -> K -> Cmp, xs: List<&2, K>) -> Bool:
146 match xs:
147 case Nil{}:
148 True{}
149 case Con{+h, t}:
150 sorted.go(~K, ~cmp, t, h)
151
152law omap_new_searchtree:
153 for ~K: Data
154 for ~V: Data
155 for ~cmp: K -> K -> Cmp
156 {searchtree(~K, ~V, ~cmp, O.OMap.new(K, V)) == True{} : Bool}
157
158law omap_put_searchtree:
159 for ~K: Data
160 for ~V: Data
161 for ~cmp: K -> K -> Cmp
162 for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
163 for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
164 for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
165 for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
166 for m: O.OMap<K, V>
167 for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
168 for +k: K
169 for +v: V
170 {searchtree(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k, v)) == True{} : Bool}
171
172law omap_del_searchtree:
173 for ~K: Data
174 for ~V: Data
175 for ~cmp: K -> K -> Cmp
176 for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
177 for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
178 for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
179 for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
180 for m: O.OMap<K, V>
181 for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
182 for +k: K
183 {searchtree(~K, ~V, ~cmp, O.OMap.del(~K, ~V, ~cmp, m, k)) == True{} : Bool}
184
185law omap_searchtree_keys_sorted:
186 for ~K: Data
187 for ~V: Data
188 for ~cmp: K -> K -> Cmp
189 for m: O.OMap<K, V>
190 for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
191 {sorted(~K, ~cmp, O.OMap.keys(K, V, m)) == True{} : Bool}
192
193law omap_get_put_same:
194 for ~K: Data
195 for ~V: Data
196 for ~cmp: K -> K -> Cmp
197 for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
198 for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
199 for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
200 for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
201 for m: O.OMap<K, V>
202 for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
203 for +k: K
204 for +v: V
205 {O.OMap.get(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k, v), k) == Some{v} : Maybe<&2, V>}
206
207law omap_get_put_other_key:
208 for ~K: Data
209 for ~V: Data
210 for ~cmp: K -> K -> Cmp
211 for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
212 for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
213 for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
214 for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
215 for m: O.OMap<K, V>
216 for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
217 for +k2: K
218 for +k: K
219 for ne: {cmp(k2, k) != EQ{} : Cmp}
220 for +v: V
221 {O.OMap.get(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k2, v), k)
222 == O.OMap.get(~K, ~V, ~cmp, m, k) : Maybe<&2, V>}
223
224# Order.string is a total order with EQ meaning equal strings: it meets the
225# refl, eq, flip and trans facts that the OMap laws above take. It answers for
226# every pair, so it is total; flip makes it antisymmetric.
227law order_string_refl:
228 for x: String
229 {Order.string(x, x) == EQ{} : Cmp}
230
231law order_string_eq:
232 for x: String
233 for y: String
234 for e: {Order.string(x, y) == EQ{} : Cmp}
235 {x == y : String}
236
237law order_string_flip:
238 for x: String
239 for y: String
240 {Order.string(y, x) == flip(Order.string(x, y)) : Cmp}
241
242law order_string_trans:
243 for x: String
244 for y: String
245 for z: String
246 for e1: {Order.string(x, y) == LT{} : Cmp}
247 for e2: {Order.string(y, z) == LT{} : Cmp}
248 {Order.string(x, z) == LT{} : Cmp}
249
250# Lower code points first, and a prefix before its extensions.
251law order_string_fixtures:
252 {[Order.string("a", "b"), Order.string("ab", "a"), Order.string("", "a"), Order.string("é", "z")]
253 == [LT{}, GT{}, LT{}, GT{}] : List<&2, Cmp>}
254
255# Ghost weight from tree shape: weight = stored size + 1, so OTip has weight 1 and
256# OBin{lo, hi} has weight w(lo) + w(hi). Balance is Hirai-Yamamoto (delta 3, gamma 2).
257def omap_weight(-K: Data, -V: Data, m: O.OMap<K, V>) -> Nat:
258 match m:
259 case O.OTip{}:
260 1n
261 case O.OBin{s, k, v, lo, hi}:
262 Nat.add(omap_weight(K, V, lo), omap_weight(K, V, hi))
263
264def weight_ok(+wl: Nat, +wh: Nat) -> Bool:
265 Nat.is_le(wh, Nat.mul(3n, wl)) && Nat.is_le(wl, Nat.mul(3n, wh))
266
267def weight_balanced(-K: Data, -V: Data, m: O.OMap<K, V>) -> Bool:
268 match m:
269 case O.OTip{}:
270 True{}
271 case O.OBin{s, k, v, +lo, +hi}:
272 weight_ok(omap_weight(K, V, lo), omap_weight(K, V, hi))
273 && weight_balanced(K, V, lo) && weight_balanced(K, V, hi)
274
275# The ghost map below has the shape of OMap: it builds nodes with the same
276# OMap.bin and rotations, but it compares Nat weights where OMap compares U32
277# sizes. While 3 * (size + 1) stays below 2^32, the U32 tests give the same
278# answers, so g_put and g_del give the same tree as put and del. The checker
279# cannot see into U32, so that link is an assumption, checked on fixtures below.
280def g_heavy_hi(-K: Data, -V: Data, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>) -> Bool:
281 Nat.is_gt(omap_weight(K, V, hi), Nat.mul(3n, omap_weight(K, V, lo)))
282
283def g_heavy_lo(-K: Data, -V: Data, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>) -> Bool:
284 Nat.is_gt(omap_weight(K, V, lo), Nat.mul(3n, omap_weight(K, V, hi)))
285
286def g_rot_lo(-K: Data, -V: Data, k: K, v: V, lo: O.OMap<K, V>, hi: O.OMap<K, V>) -> O.OMap<K, V>:
287 match hi:
288 case O.OTip{}:
289 O.OMap.bin(K, V, k, v, lo, O.OTip{})
290 case O.OBin{s, hk, hv, +hl, +hh}:
291 O.OMap.rot_lo.pick(K, V,
292 Nat.is_lt(omap_weight(K, V, hl), Nat.mul(2n, omap_weight(K, V, hh))),
293 k, v, lo, hk, hv, hl, hh)
294
295def g_rot_hi(-K: Data, -V: Data, k: K, v: V, lo: O.OMap<K, V>, hi: O.OMap<K, V>) -> O.OMap<K, V>:
296 match lo:
297 case O.OTip{}:
298 O.OMap.bin(K, V, k, v, O.OTip{}, hi)
299 case O.OBin{s, lk, lv, +ll, +lh}:
300 O.OMap.rot_hi.pick(K, V,
301 Nat.is_lt(omap_weight(K, V, lh), Nat.mul(2n, omap_weight(K, V, ll))),
302 k, v, lk, lv, ll, lh, hi)
303
304def g_balance.if(
305 -K: Data, -V: Data, heavy_hi: Bool, heavy_lo: Bool, k: K, v: V,
306 lo: O.OMap<K, V>, hi: O.OMap<K, V>
307) -> O.OMap<K, V>:
308 match heavy_hi heavy_lo:
309 case True{} _:
310 g_rot_lo(K, V, k, v, lo, hi)
311 case False{} True{}:
312 g_rot_hi(K, V, k, v, lo, hi)
313 case False{} False{}:
314 O.OMap.bin(K, V, k, v, lo, hi)
315
316def g_balance(-K: Data, -V: Data, k: K, v: V, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>) -> O.OMap<K, V>:
317 g_balance.if(K, V, g_heavy_hi(K, V, lo, hi), g_heavy_lo(K, V, lo, hi), k, v, lo, hi)
318
319def g_put(
320 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap<K, V>, +k: K, +v: V
321) -> O.OMap<K, V>:
322 match m:
323 case O.OTip{}:
324 O.OBin{1, k, v, O.OTip{}, O.OTip{}}
325 case O.OBin{+s, +key, +val, +lo, +hi}:
326 O.Cmp.case(O.OMap<K, V>, cmp(k, key),
327 u => g_balance(K, V, key, val, g_put(~K, ~V, ~cmp, lo, k, v), hi),
328 u => O.OBin{s, key, v, lo, hi},
329 u => g_balance(K, V, key, val, lo, g_put(~K, ~V, ~cmp, hi, k, v)))
330
331def g_pop_min.fin(
332 -K: Data, -V: Data, k: K, v: V, hi: O.OMap<K, V>, r: K & V & O.OMap<K, V>
333) -> K & V & O.OMap<K, V>:
334 (mk, mv, lo) = r
335 (mk, mv, g_balance(K, V, k, v, lo, hi))
336
337def g_pop_min(
338 -K: Data, -V: Data, lo: O.OMap<K, V>, k: K, v: V, hi: O.OMap<K, V>
339) -> K & V & O.OMap<K, V>:
340 match lo:
341 case O.OTip{}:
342 (k, v, hi)
343 case O.OBin{s, lk, lv, ll, lh}:
344 g_pop_min.fin(K, V, k, v, hi, g_pop_min(K, V, ll, lk, lv, lh))
345
346def g_glue.fin(-K: Data, -V: Data, lo: O.OMap<K, V>, r: K & V & O.OMap<K, V>) -> O.OMap<K, V>:
347 (k, v, hi) = r
348 g_balance(K, V, k, v, lo, hi)
349
350def g_glue(-K: Data, -V: Data, lo: O.OMap<K, V>, hi: O.OMap<K, V>) -> O.OMap<K, V>:
351 match hi:
352 case O.OTip{}:
353 lo
354 case O.OBin{s, k, v, hl, hh}:
355 g_glue.fin(K, V, lo, g_pop_min(K, V, hl, k, v, hh))
356
357def g_del(
358 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap<K, V>, +k: K
359) -> O.OMap<K, V>:
360 match m:
361 case O.OTip{}:
362 O.OTip{}
363 case O.OBin{+s, +key, +val, +lo, +hi}:
364 O.Cmp.case(O.OMap<K, V>, cmp(k, key),
365 u => g_balance(K, V, key, val, g_del(~K, ~V, ~cmp, lo, k), hi),
366 u => g_glue(K, V, lo, hi),
367 u => g_balance(K, V, key, val, lo, g_del(~K, ~V, ~cmp, hi, k)))
368
369law omap_new_weight_balanced:
370 for ~K: Data
371 for ~V: Data
372 {weight_balanced(K, V, O.OMap.new(K, V)) == True{} : Bool}
373
374law omap_g_put_matches:
375 {g_put(~U32, ~U32, ~U32.cmp, m7(), 8, 80)
376 == O.OMap.put(~U32, ~U32, ~U32.cmp, m7(), 8, 80) : O.OMap<U32, U32>}
377
378law omap_g_del_matches:
379 {g_del(~U32, ~U32, ~U32.cmp, m7(), 4)
380 == O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4) : O.OMap<U32, U32>}
381
382law omap_put_weight_balanced:
383 for ~K: Data
384 for ~V: Data
385 for ~cmp: K -> K -> Cmp
386 for +m: O.OMap<K, V>
387 for wb: {weight_balanced(K, V, m) == True{} : Bool}
388 for +k: K
389 for +v: V
390 {weight_balanced(K, V, g_put(~K, ~V, ~cmp, m, k, v)) == True{} : Bool}
391
392law omap_del_weight_balanced:
393 for ~K: Data
394 for ~V: Data
395 for ~cmp: K -> K -> Cmp
396 for +m: O.OMap<K, V>
397 for wb: {weight_balanced(K, V, m) == True{} : Bool}
398 for +k: K
399 {weight_balanced(K, V, g_del(~K, ~V, ~cmp, m, k)) == True{} : Bool}
400
401
402law vec_from_list:
403 {V.Vec.to_list(~U32, V.Vec.from_list(~U32, [1, 2, 3, 4, 5]))
404 == [1, 2, 3, 4, 5] : List<&2, U32>}
405
406law vec_get:
407 {Pair.snd(V.Vec<U32>, Maybe<&2, U32>, V.Vec.get(~U32, V.Vec.from_list(~U32, [1, 2, 3]), 2))
408 == Some{3} : Maybe<&2, U32>}
409
410law vec_get_past_len:
411 {Pair.snd(V.Vec<U32>, Maybe<&2, U32>, V.Vec.get(~U32, V.Vec.from_list(~U32, [1, 2, 3]), 3))
412 == None{} : Maybe<&2, U32>}
413
414law vec_set:
415 {V.Vec.to_list(~U32, V.Vec.set(~U32, V.Vec.from_list(~U32, [1, 2, 3]), 1, 9))
416 == [1, 9, 3] : List<&2, U32>}
417
418law vec_pop:
419 {Pair.snd(V.Vec<U32>, Maybe<&2, U32>, V.Vec.pop(~U32, V.Vec.from_list(~U32, [1, 2, 3])))
420 == Some{3} : Maybe<&2, U32>}
421
422law vec_pop_empty:
423 {Pair.snd(V.Vec<U32>, Maybe<&2, U32>, V.Vec.pop(~U32, V.Vec.new(~U32)))
424 == None{} : Maybe<&2, U32>}
425
426law vec_pop_to_list:
427 {V.Vec.to_list(~U32, Pair.fst(V.Vec<U32>, Maybe<&2, U32>,
428 V.Vec.pop(~U32, V.Vec.from_list(~U32, [1, 2, 3]))))
429 == [1, 2] : List<&2, U32>}
430
431law deque_ends:
432 {D.Deque.to_list(&2, U32, D.Deque.push_front(&2, U32, 0,
433 D.Deque.push_back(&2, U32, 2, D.Deque.push_back(&2, U32, 1, D.Deque.new(&2, U32)))))
434 == [0, 1, 2] : List<&2, U32>}
435
436law heap_sort:
437 {H.Heap.sort(~U32, ~U32.is_le, [3, 1, 4, 1, 5]) == [1, 1, 3, 4, 5] : List<&2, U32>}
438
439def hkey(k: U32) -> U32:
440 (k .&. 1 : U32)
441
442def hm() -> M.HMap<U32, U32>:
443 m = M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, M.HMap.new(U32, U32), 2, 20)
444 M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, m, 3, 30)
445
446law hmap_get_put:
447 {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq,
448 M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4, 40), 4)
449 == Some{40} : Maybe<&2, U32>}
450
451law hmap_get_put_other:
452 {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq,
453 M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4, 40), 3)
454 == M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 3) : Maybe<&2, U32>}
455
456law hmap_collision:
457 {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq,
458 M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4, 40), 2)
459 == Some{20} : Maybe<&2, U32>}
460
461law hmap_replace_collision:
462 {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq,
463 M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 2, 22), 2)
464 == Some{22} : Maybe<&2, U32>}
465
466def full(k: U32) -> U32:
467 k
468
469law hmap_high_bit:
470 {M.HMap.get(~U32, ~U32, ~full, ~U32.is_eq,
471 M.HMap.put(~U32, ~U32, ~full, ~U32.is_eq,
472 M.HMap.put(~U32, ~U32, ~full, ~U32.is_eq, M.HMap.new(U32, U32), 0, 10),
473 2147483648, 20), 0)
474 == Some{10} : Maybe<&2, U32>}
475
476law hmap_missing_collision:
477 {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4)
478 == None{} : Maybe<&2, U32>}
479
480# The HMap laws below hold for every eq that is reflexive (eq(x, x) is True)
481# and sound (eq(x, y) is True only when x == y), as each law states. Equal keys
482# then hash alike because hash is a function, so the hash needs no assumption.
483# They hold for well-formed maps: hmap_wf, which HMap.new, put and del keep.
484
485# No entry of xs has a key equal to k.
486def hmap_absent(
487 ~K: Data, ~V: Data, ~eq: K -> K -> Bool, xs: List<&2, M.Entry<K, V>>, +k: K
488) -> Bool:
489 match xs:
490 case Nil{}:
491 True{}
492 case Con{M.Entry{+key, val}, rest}:
493 Bool.not(eq(k, key)) && hmap_absent(~K, ~V, ~eq, rest, k)
494
495# No two entries of xs have equal keys.
496def hmap_distinct(~K: Data, ~V: Data, ~eq: K -> K -> Bool, xs: List<&2, M.Entry<K, V>>) -> Bool:
497 match xs:
498 case Nil{}:
499 True{}
500 case Con{M.Entry{+key, val}, +rest}:
501 hmap_absent(~K, ~V, ~eq, rest, key) && hmap_distinct(~K, ~V, ~eq, rest)
502
503# Every key of xs hashes to h.
504def hmap_hashed(
505 ~K: Data, ~V: Data, ~hash: K -> U32, xs: List<&2, M.Entry<K, V>>, +h: U32
506) -> Bool:
507 match xs:
508 case Nil{}:
509 True{}
510 case Con{M.Entry{key, val}, rest}:
511 U32.is_eq(h, hash(key)) && hmap_hashed(~K, ~V, ~hash, rest, h)
512
513# A trie with n levels left: buckets hold distinct keys; above the last level,
514# a bucket's keys hash to its hash; the last level has no branches.
515def hmap_wf.go(
516 ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, +n: Nat, m: M.HMap<K, V>
517) -> Bool:
518 match n:
519 case 0n:
520 match m:
521 case M.HNil{}:
522 True{}
523 case M.HLeaf{h, es}:
524 hmap_distinct(~K, ~V, ~eq, es)
525 case M.HBranch{lo, hi}:
526 False{}
527 case 1n+p:
528 match m:
529 case M.HNil{}:
530 True{}
531 case M.HLeaf{h, +es}:
532 hmap_hashed(~K, ~V, ~hash, es, h) && hmap_distinct(~K, ~V, ~eq, es)
533 case M.HBranch{lo, hi}:
534 hmap_wf.go(~K, ~V, ~hash, ~eq, p, lo) && hmap_wf.go(~K, ~V, ~hash, ~eq, p, hi)
535
536def hmap_wf(~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, m: M.HMap<K, V>) -> Bool:
537 hmap_wf.go(~K, ~V, ~hash, ~eq, 32n, m)
538
539law hmap_new_wf:
540 for ~K: Data
541 for ~V: Data
542 for ~hash: K -> U32
543 for ~eq: K -> K -> Bool
544 {hmap_wf(~K, ~V, ~hash, ~eq, M.HMap.new(K, V)) == True{} : Bool}
545
546law hmap_put_wf:
547 for ~K: Data
548 for ~V: Data
549 for ~hash: K -> U32
550 for ~eq: K -> K -> Bool
551 for ~refl: @x: K -> {eq(x, x) == True{} : Bool}
552 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
553 for m: M.HMap<K, V>
554 for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
555 for +k: K
556 for +v: V
557 {hmap_wf(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v)) == True{} : Bool}
558
559law hmap_del_wf:
560 for ~K: Data
561 for ~V: Data
562 for ~hash: K -> U32
563 for ~eq: K -> K -> Bool
564 for m: M.HMap<K, V>
565 for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
566 for +k: K
567 {hmap_wf(~K, ~V, ~hash, ~eq, M.HMap.del(~K, ~V, ~hash, ~eq, m, k)) == True{} : Bool}
568
569law hmap_get_put_same:
570 for ~K: Data
571 for ~V: Data
572 for ~hash: K -> U32
573 for ~eq: K -> K -> Bool
574 for ~refl: @x: K -> {eq(x, x) == True{} : Bool}
575 for m: M.HMap<K, V>
576 for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
577 for +k: K
578 for +v: V
579 {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v), k)
580 == Some{v} : Maybe<&2, V>}
581
582law hmap_get_put_other_key:
583 for ~K: Data
584 for ~V: Data
585 for ~hash: K -> U32
586 for ~eq: K -> K -> Bool
587 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
588 for m: M.HMap<K, V>
589 for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
590 for +k2: K
591 for +k: K
592 for ne: {k2 != k : K}
593 for +v: V
594 {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k2, v), k)
595 == M.HMap.get(~K, ~V, ~hash, ~eq, m, k) : Maybe<&2, V>}
596
597law hmap_get_del_same:
598 for ~K: Data
599 for ~V: Data
600 for ~hash: K -> U32
601 for ~eq: K -> K -> Bool
602 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
603 for m: M.HMap<K, V>
604 for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
605 for +k: K
606 {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.del(~K, ~V, ~hash, ~eq, m, k), k)
607 == None{} : Maybe<&2, V>}
608
609law hmap_get_del_other_key:
610 for ~K: Data
611 for ~V: Data
612 for ~hash: K -> U32
613 for ~eq: K -> K -> Bool
614 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
615 for m: M.HMap<K, V>
616 for +k2: K
617 for +k: K
618 for ne: {k2 != k : K}
619 {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.del(~K, ~V, ~hash, ~eq, m, k2), k)
620 == M.HMap.get(~K, ~V, ~hash, ~eq, m, k) : Maybe<&2, V>}
621
622law hmap_size_put_new:
623 for ~K: Data
624 for ~V: Data
625 for ~hash: K -> U32
626 for ~eq: K -> K -> Bool
627 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
628 for m: M.HMap<K, V>
629 for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
630 for +k: K
631 for +v: V
632 for miss: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == None{} : Maybe<&2, V>}
633 {M.HMap.size(K, V, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v))
634 == 1n+M.HMap.size(K, V, m) : Nat}
635
636law hmap_size_put_replace:
637 for ~K: Data
638 for ~V: Data
639 for ~hash: K -> U32
640 for ~eq: K -> K -> Bool
641 for m: M.HMap<K, V>
642 for +k: K
643 for +v: V
644 for -w: V
645 for hit: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == Some{w} : Maybe<&2, V>}
646 {M.HMap.size(K, V, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v))
647 == M.HMap.size(K, V, m) : Nat}
648
649law hmap_size_del:
650 for ~K: Data
651 for ~V: Data
652 for ~hash: K -> U32
653 for ~eq: K -> K -> Bool
654 for m: M.HMap<K, V>
655 for +k: K
656 for -w: V
657 for hit: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == Some{w} : Maybe<&2, V>}
658 {1n+M.HMap.size(K, V, M.HMap.del(~K, ~V, ~hash, ~eq, m, k))
659 == M.HMap.size(K, V, m) : Nat}
660
661law hmap_size_del_missing:
662 for ~K: Data
663 for ~V: Data
664 for ~hash: K -> U32
665 for ~eq: K -> K -> Bool
666 for m: M.HMap<K, V>
667 for +k: K
668 for miss: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == None{} : Maybe<&2, V>}
669 {M.HMap.size(K, V, M.HMap.del(~K, ~V, ~hash, ~eq, m, k))
670 == M.HMap.size(K, V, m) : Nat}
671
672# Two distinct keys with one hash share a bucket; both stay reachable.
673law hmap_collision_get:
674 for ~K: Data
675 for ~V: Data
676 for ~hash: K -> U32
677 for ~eq: K -> K -> Bool
678 for ~refl: @x: K -> {eq(x, x) == True{} : Bool}
679 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
680 for +m: M.HMap<K, V>
681 for +wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
682 for +k1: K
683 for +k2: K
684 for ne: {k2 != k1 : K}
685 for same: {hash(k1) == hash(k2) : U32}
686 for +v1: V
687 for +v2: V
688 {M.HMap.get(~K, ~V, ~hash, ~eq,
689 M.HMap.put(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k1, v1), k2, v2), k1)
690 == Some{v1} : Maybe<&2, V>}
691
692law hmap_collision_size:
693 for ~K: Data
694 for ~V: Data
695 for ~hash: K -> U32
696 for ~eq: K -> K -> Bool
697 for ~refl: @x: K -> {eq(x, x) == True{} : Bool}
698 for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K}
699 for +m: M.HMap<K, V>
700 for +wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool}
701 for +k1: K
702 for +k2: K
703 for ne: {k1 != k2 : K}
704 for same: {hash(k1) == hash(k2) : U32}
705 for +v1: V
706 for +v2: V
707 for miss1: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k1) == None{} : Maybe<&2, V>}
708 for miss2: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k2) == None{} : Maybe<&2, V>}
709 {M.HMap.size(K, V,
710 M.HMap.put(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k1, v1), k2, v2))
711 == 2n+M.HMap.size(K, V, m) : Nat}