1	import Base
2	import ./omap.bend as O
3	import ./hmap.bend as M
4	import ./vec.bend as V
5	import ./deque.bend as D
6	import ./heap.bend as H
7	import ./order.bend as Order
8	
9	def scmp.fin(r: (String & String) & Cmp) -> Cmp:
10	  (ab, c) = r
11	  c
12	
13	def scmp(a: String, b: String) -> Cmp:
14	  scmp.fin(String.cmp(a, b))
15	
16	def 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	
21	def 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	
28	def m7() -> O.OMap<U32, U32>:
29	  m7.go(7n, 1, O.OMap.new(U32, U32))
30	
31	law omap_keys_ascending_puts:
32	  {O.OMap.keys(U32, U32, m7()) == [1, 2, 3, 4, 5, 6, 7] : List<&2, U32>}
33	
34	law omap_size_del:
35	  {O.OMap.size(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4)) == 6 : U32}
36	
37	law 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	
41	law 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	
45	law 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	
49	law 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	
53	law 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	
57	law omap_get_missing:
58	  {O.OMap.get(~U32, ~U32, ~U32.cmp, m3(), 2) == None{} : Maybe<&2, U32>}
59	
60	law 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	
64	law omap_size_replace:
65	  {O.OMap.size(U32, U32, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 5, 55)) == 3 : U32}
66	
67	law 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	
71	law 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	
75	law 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	
79	law 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	
86	law 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	
92	law 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.
99	def flip(c: Cmp) -> Cmp:
100	  match c:
101	    case LT{}:
102	      GT{}
103	    case EQ{}:
104	      EQ{}
105	    case GT{}:
106	      LT{}
107	
108	def 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	
115	def 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.
123	def 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	
135	def searchtree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap<K, V>) -> Bool:
136	  bounded(~K, ~V, ~cmp, m, None{}, None{})
137	
138	def 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	
145	def 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	
152	law 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	
158	law 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	
172	law 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	
185	law 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	
193	law 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	
207	law 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.
227	law order_string_refl:
228	  for x: String
229	  {Order.string(x, x) == EQ{} : Cmp}
230	
231	law 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	
237	law order_string_flip:
238	  for x: String
239	  for y: String
240	  {Order.string(y, x) == flip(Order.string(x, y)) : Cmp}
241	
242	law 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.
251	law 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).
257	def 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	
264	def 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	
267	def 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.
280	def 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	
283	def 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	
286	def 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	
295	def 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	
304	def 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	
316	def 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	
319	def 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	
331	def 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	
337	def 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	
346	def 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	
350	def 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	
357	def 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	
369	law 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	
374	law 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	
378	law 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	
382	law 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	
392	law 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	
402	law 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	
406	law 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	
410	law 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	
414	law 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	
418	law 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	
422	law 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	
426	law 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	
431	law 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	
436	law heap_sort:
437	  {H.Heap.sort(~U32, ~U32.is_le, [3, 1, 4, 1, 5]) == [1, 1, 3, 4, 5] : List<&2, U32>}
438	
439	def hkey(k: U32) -> U32:
440	  (k .&. 1 : U32)
441	
442	def 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	
446	law 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	
451	law 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	
456	law 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	
461	law 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	
466	def full(k: U32) -> U32:
467	  k
468	
469	law 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	
476	law 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.
486	def 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.
496	def 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.
504	def 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.
515	def 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	
536	def 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	
539	law 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	
546	law 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	
559	law 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	
569	law 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	
582	law 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	
597	law 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	
609	law 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	
622	law 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	
636	law 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	
649	law 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	
661	law 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.
673	law 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	
692	law 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}