LAWS.bend

bend-kit-collections@0.1.4.1 · 711 lines · 95 definitions

1import Base
2import bend-kit-collections@0.1.4.1/omap.bend as O
3import bend-kit-collections@0.1.4.1/hmap.bend as M
4import bend-kit-collections@0.1.4.1/vec.bend as V
5import bend-kit-collections@0.1.4.1/deque.bend as D
6import bend-kit-collections@0.1.4.1/heap.bend as H
7import bend-kit-collections@0.1.4.1/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}