proofs/lib/lemmas/proofs/native_map.bend

bend-collections-laws-crypto@1.0.0.0 · 540 lines · 49 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend as MB
3
4# These unfold installed Base algorithms; no map axioms or replacement map.
5law empty_lookup:
6  for -V: Data
7  for d: V
8  for k: String
9  {Map.get(V, d, Map.new(&2, V), k) == (MTip{}, d) : Map<&2, V> & V}
10def empty_lookup(V, d, k):
11  {==}
12
13law empty_set:
14  for -V: Data
15  for k: String
16  for v: V
17  {Map.set(&2, V, Map.new(&2, V), k, v) == MLeaf{k, v} : Map<&2, V>}
18def empty_set(V, k, v):
19  {==}
20
21law empty_delete:
22  for -V: Data
23  for k: String
24  {Map.del(&2, V, Map.new(&2, V), k) == MTip{} : Map<&2, V>}
25def empty_delete(V, k):
26  {==}
27
28law empty_has:
29  for -V: Data
30  for k: String
31  {Map.has(&2, V, Map.new(&2, V), k) == (MTip{}, False{}) : Map<&2, V> & Bool}
32def empty_has(V, k):
33  {==}
34
35# Presence bits are the key distinction between zero characters and end of string.
36law zero_character_presence:
37  for tail: String
38  {Map.bit.go(SCon{Chr{0}, tail}, 0n, 0n) == (SCon{Chr{0}, tail}, True{}) : String & Bool}
39def zero_character_presence(tail):
40  {==}
41
42law empty_presence:
43  {Map.bit.go(SNil{}, 0n, 0n) == (SNil{}, False{}) : String & Bool}
44def empty_presence():
45  {==}
46
47law boolean_compare_self:
48  for b: Bool
49  {Bool.cmp(b, b) == EQ{} : Cmp}
50def boolean_compare_self(b):
51  match b:
52    case False{}:
53      {==}
54    case True{}:
55      {==}
56
57law word_compare_self:
58  for n: Nat
59  for w: Word(n)
60  {Word.cmp(n, w, w) == EQ{} : Cmp}
61def word_compare_self(n, w):
62  match n:
63    case 0n:
64      {==}
65    case 1n+p:
66      match w:
67        case WCon{+b, t}:
68          Equal.trans(Cmp, Word.cmp.fin(b, b, Word.cmp(p, t, t)), Bool.cmp(b, b), EQ{},
69            Equal.cong(Cmp, Cmp, x => Word.cmp.fin(b, b, x), Word.cmp(p, t, t), EQ{}, word_compare_self(p, t)),
70            boolean_compare_self(b))
71
72law character_compare_self:
73  for c: Char
74  {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
75def character_compare_self(c):
76  match c:
77    case Chr{U32{w}}:
78      %word_compare_self(32n, w) : {((Chr{U32{w}}, Chr{U32{w}}), Word.cmp(32n, w, w)) == ((Chr{U32{w}}, Chr{U32{w}}), _) : (Char & Char) & Cmp}
79      {==}
80
81law string_compare_self:
82  for s: String
83  {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
84def string_compare_self(s):
85  match s:
86    case SNil{}:
87      {==}
88    case SCon{h, t}:
89      %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), character_compare_self(h)) : {String.cmp.fin(t, t, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
90      %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), string_compare_self(t)) : {String.cmp.rec(h, h, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
91      {==}
92
93law singleton_get:
94  for -V: Data
95  for d: V
96  for k: String
97  for v: V
98  {Map.get(V, d, MLeaf{k, v}, k) == (MLeaf{k, v}, v) : Map<&2, V> & V}
99def singleton_get(V, d, k, v):
100  %Equal.sym((String & String) & Cmp, String.cmp(k, k), ((k, k), EQ{}), string_compare_self(k)) : {Map.get.leaf(V, d, v, _) == (MLeaf{k, v}, v) : Map<&2, V> & V}
101  {==}
102
103law singleton_update:
104  for -V: Data
105  for k: String
106  for old: V
107  for value: V
108  {Map.set(&2, V, MLeaf{k, old}, k, value) == MLeaf{k, value} : Map<&2, V>}
109def singleton_update(V, k, old, value):
110  %Equal.sym((String & String) & Cmp, String.cmp(k, k), ((k, k), EQ{}), string_compare_self(k)) : {Map.set.fin.go(&2, V, MLeaf{k, old}, k, value, _) == MLeaf{k, value} : Map<&2, V>}
111  {==}
112
113law singleton_delete:
114  for -V: Data
115  for k: String
116  for v: V
117  {Map.del(&2, V, MLeaf{k, v}, k) == MTip{} : Map<&2, V>}
118def singleton_delete(V, k, v):
119  %Equal.sym((String & String) & Cmp, String.cmp(k, k), ((k, k), EQ{}), string_compare_self(k)) : {Map.del.fin(&2, V, Map.pop.leaf(&2, V, v, _)) == MTip{} : Map<&2, V>}
120  {==}
121
122# General routing foundation: actual Base bit traversal preserves the entire
123# string, irrespective of the requested bit, character codes, or tree validity.
124def routed_key(r: String & Bool) -> String:
125  (key, bit) = r
126  key
127
128law recursive_bit_key:
129  for c: Char
130  for r: String & Bool
131  {routed_key(Map.bit.go.rec(c, r)) == SCon{c, routed_key(r)} : String}
132def recursive_bit_key(c, r):
133  match r:
134    case Tuple{key, bit}:
135      {==}
136
137law bit_go_preserves_key:
138  for key: String
139  for +character: Nat
140  for +offset: Nat
141  {routed_key(Map.bit.go(key, character, offset)) == key : String}
142def bit_go_preserves_key(key, character, offset):
143  match key character offset:
144    case SNil{} ci off:
145      {==}
146    case SCon{Chr{x}, tail} 0n 0n:
147      {==}
148    case SCon{Chr{x}, tail} 0n 1n+off:
149      {==}
150    case SCon{Chr{x}, +tail} 1n+ci off:
151      +c = {Chr{x} : Char}
152      Equal.trans(String, routed_key(Map.bit.go.rec(c, Map.bit.go(tail, ci, off))),
153        SCon{c, routed_key(Map.bit.go(tail, ci, off))}, SCon{c, tail},
154        recursive_bit_key(c, Map.bit.go(tail, ci, off)),
155        Equal.cong(String, String, t => SCon{c, t}, routed_key(Map.bit.go(tail, ci, off)), tail, bit_go_preserves_key(tail, ci, off)))
156
157law bit_at_preserves_key:
158  for key: String
159  for coordinates: Nat & Nat
160  {routed_key(Map.bit.at(key, coordinates)) == key : String}
161def bit_at_preserves_key(key, coordinates):
162  match coordinates:
163    case Tuple{ci, off}:
164      bit_go_preserves_key(key, ci, off)
165
166law bit_preserves_key:
167  for key: String
168  for position: Nat
169  {routed_key(Map.bit(key, position)) == key : String}
170def bit_preserves_key(key, position):
171  bit_at_preserves_key(key, Nat.divmod(position, 33n))
172
173# A comparison certificate has content precisely in the EQ branch.
174def comparison_identity(-A: Type, a: A, b: A, c: Cmp) -> Type:
175  match c:
176    case LT{}:
177      Unit
178    case EQ{}:
179      {a == b : A}
180    case GT{}:
181      Unit
182
183law word_comparison_step:
184  for n: Nat
185  for a: Word(n)
186  for b: Word(n)
187  for c: Cmp
188  for x: Bool
189  for y: Bool
190  for proof: comparison_identity(Word(n), a, b, c)
191  comparison_identity(Word(1n+n), WCon{x, a}, WCon{y, b}, Word.cmp.fin(x, y, c))
192def word_comparison_step(n, a, b, c, x, y, proof):
193  match c:
194    case LT{}:
195      Unit{}
196    case GT{}:
197      Unit{}
198    case EQ{}:
199      match x y:
200        case False{} False{}:
201          Equal.cong(Word(n), Word(1n+n), t => WCon{False{}, t}, a, b, proof)
202        case True{} True{}:
203          Equal.cong(Word(n), Word(1n+n), t => WCon{True{}, t}, a, b, proof)
204        case False{} True{}:
205          Unit{}
206        case True{} False{}:
207          Unit{}
208
209law word_comparison_identity:
210  for n: Nat
211  for a: Word(n)
212  for b: Word(n)
213  comparison_identity(Word(n), a, b, Word.cmp(n, a, b))
214def word_comparison_identity(n, a, b):
215  match n:
216    case 0n:
217      match a b:
218        case WNil{} WNil{}:
219          {==}
220    case 1n+ +p:
221      match a b:
222        case WCon{x, +at} WCon{y, +bt}:
223          word_comparison_step(p, at, bt, Word.cmp(p, at, bt), x, y, word_comparison_identity(p, at, bt))
224
225law comparison_lift:
226  for -A: Type
227  for -B: Type
228  for f: A -> B
229  for a: A
230  for b: A
231  for c: Cmp
232  for proof: comparison_identity(A, a, b, c)
233  comparison_identity(B, f(a), f(b), c)
234def comparison_lift(A, B, f, a, b, c, proof):
235  match c:
236    case LT{}:
237      Unit{}
238    case GT{}:
239      Unit{}
240    case EQ{}:
241      Equal.cong(A, B, f, a, b, proof)
242
243def comparison_result_identity(-A: Type, r: (A & A) & Cmp) -> Type:
244  ((a, b), c) = r
245  comparison_identity(A, a, b, c)
246
247law character_comparison_identity:
248  for a: Char
249  for b: Char
250  comparison_result_identity(Char, Char.cmp(a, b))
251def character_comparison_identity(a, b):
252  match a b:
253    case Chr{U32{+x}} Chr{U32{+y}}:
254      comparison_lift(Word(32n), Char, w => Chr{U32{w}}, x, y, Word.cmp(32n, x, y), word_comparison_identity(32n, x, y))
255
256law string_comparison_rec_identity:
257  for h: Char
258  for r: (String & String) & Cmp
259  for proof: comparison_result_identity(String, r)
260  comparison_result_identity(String, String.cmp.rec(h, h, r))
261def string_comparison_rec_identity(h, r, proof):
262  match r:
263    case Tuple{Tuple{a, b}, c}:
264      comparison_lift(String, String, t => SCon{h, t}, a, b, c, proof)
265
266law string_comparison_fin_identity:
267  for t1: String
268  for t2: String
269  for hc: (Char & Char) & Cmp
270  for hp: comparison_result_identity(Char, hc)
271  for tp: comparison_result_identity(String, String.cmp(t1, t2))
272  comparison_result_identity(String, String.cmp.fin(t1, t2, hc))
273def string_comparison_fin_identity(t1, t2, hc, hp, tp):
274  match hc:
275    case Tuple{Tuple{h1, h2}, LT{}}:
276      Unit{}
277    case Tuple{Tuple{h1, h2}, GT{}}:
278      Unit{}
279    case Tuple{Tuple{h1, h2}, EQ{}}:
280      %hp : comparison_result_identity(String, String.cmp.rec(h1, _, String.cmp(t1, t2)))
281      string_comparison_rec_identity(h1, String.cmp(t1, t2), tp)
282
283law string_comparison_identity:
284  for a: String
285  for b: String
286  comparison_result_identity(String, String.cmp(a, b))
287def string_comparison_identity(a, b):
288  match a b:
289    case SNil{} SNil{}:
290      {==}
291    case SNil{} SCon{h, t}:
292      Unit{}
293    case SCon{h, t} SNil{}:
294      Unit{}
295    case SCon{+h1, +t1} SCon{+h2, +t2}:
296      string_comparison_fin_identity(t1, t2, Char.cmp(h1, h2), character_comparison_identity(h1, h2), string_comparison_identity(t1, t2))
297
298def comparison_tag(-A: Type, r: (A & A) & Cmp) -> Cmp:
299  (pair, c) = r
300  c
301
302law string_comparison_shape_step:
303  for h1: Char
304  for h2: Char
305  for t1: String
306  for t2: String
307  for c: Cmp
308  for tp: {String.cmp(t1, t2) == ((t1, t2), comparison_tag(String, String.cmp(t1, t2))) : (String & String) & Cmp}
309  {String.cmp.fin(t1, t2, ((h1, h2), c)) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.fin(t1, t2, ((h1, h2), c)))) : (String & String) & Cmp}
310def string_comparison_shape_step(h1, h2, t1, t2, c, tp):
311  match c:
312    case LT{}:
313      {==}
314    case GT{}:
315      {==}
316    case EQ{}:
317      %Equal.sym((String & String) & Cmp, String.cmp(t1, t2), ((t1, t2), comparison_tag(String, String.cmp(t1, t2))), tp) : {String.cmp.rec(h1, h2, _) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.rec(h1, h2, _))) : (String & String) & Cmp}
318      {==}
319
320law string_comparison_shape:
321  for a: String
322  for b: String
323  {String.cmp(a, b) == ((a, b), comparison_tag(String, String.cmp(a, b))) : (String & String) & Cmp}
324def string_comparison_shape(a, b):
325  match a b:
326    case SNil{} SNil{}:
327      {==}
328    case SNil{} SCon{h, t}:
329      {==}
330    case SCon{h, t} SNil{}:
331      {==}
332    case SCon{Chr{U32{+x}}, +t1} SCon{Chr{U32{+y}}, +t2}:
333      string_comparison_shape_step(Chr{U32{x}}, Chr{U32{y}}, t1, t2, Word.cmp(32n, x, y), string_comparison_shape(t1, t2))
334
335law string_comparison_original_identity:
336  for +a: String
337  for +b: String
338  comparison_identity(String, a, b, comparison_tag(String, String.cmp(a, b)))
339def string_comparison_original_identity(a, b):
340  %string_comparison_shape(a, b) : comparison_result_identity(String, _)
341  string_comparison_identity(a, b)
342
343law string_equal_from_comparison:
344  for a: String
345  for b: String
346  for e: {comparison_tag(String, String.cmp(a, b)) == EQ{} : Cmp}
347  {a == b : String}
348def string_equal_from_comparison(a, b, e):
349  %e : comparison_identity(String, a, b, _)
350  string_comparison_original_identity(a, b)
351
352law string_equal_comparison:
353  for a: String
354  for b: String
355  for e: {a == b : String}
356  {String.cmp(a, b) == ((a, b), EQ{}) : (String & String) & Cmp}
357def string_equal_comparison(a, b, e):
358  %e : {String.cmp(a, _) == ((a, _), EQ{}) : (String & String) & Cmp}
359  string_compare_self(a)
360
361# First-difference base and common-prefix reduction laws for the existing
362# algorithm. The unequal-character msb/routing theorem is still outstanding.
363law difference_empty_left:
364  for h: Char
365  for tail: String
366  {Map.diff(SNil{}, SCon{h, tail}) == 0n : Nat}
367def difference_empty_left(h, tail):
368  {==}
369
370law difference_empty_right:
371  for h: Char
372  for tail: String
373  {Map.diff(SCon{h, tail}, SNil{}) == 0n : Nat}
374def difference_empty_right(h, tail):
375  {==}
376
377law difference_common_character:
378  for h: Char
379  for a: String
380  for b: String
381  {Map.diff(SCon{h, a}, SCon{h, b}) == Nat.add(33n, Map.diff(a, b)) : Nat}
382def difference_common_character(h, a, b):
383  match h:
384    case Chr{U32{w}}:
385      %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, word_compare_self(32n, w)) : {Map.diff.fin(a, b, (Map.diff.chr(U32.xor(U32{w}, U32{w})), Cmp.is_eq(_))) == Nat.add(33n, Map.diff(a, b)) : Nat}
386      {==}
387
388law difference_empty_presence:
389  for h: Char
390  for tail: String
391  {Map.bit.go(SCon{h, tail}, Map.diff(SNil{}, SCon{h, tail}), 0n) == (SCon{h, tail}, True{}) : String & Bool}
392def difference_empty_presence(h, tail):
393  match h:
394    case Chr{x}:
395      {==}
396
397def lookup_map(-V: Data, r: Map<&2, V> & V) -> Map<&2, V>:
398  (m, value) = r
399  m
400
401law lookup_leaf_preserves:
402  for -V: Data
403  for d: V
404  for v: V
405  for key: String
406  for stored: String
407  for c: Cmp
408  {lookup_map(V, Map.get.leaf(V, d, v, ((key, stored), c))) == MLeaf{stored, v} : Map<&2, V>}
409def lookup_leaf_preserves(V, d, v, key, stored, c):
410  match c:
411    case LT{}:
412      {==}
413    case EQ{}:
414      {==}
415    case GT{}:
416      {==}
417
418law lookup_lo_projection:
419  for -V: Data
420  for p: Nat
421  for hi: Map<&2, V>
422  for r: Map<&2, V> & V
423  {lookup_map(V, Map.lo(&2, V, V, p, hi, r)) == MNode{p, lookup_map(V, r), hi} : Map<&2, V>}
424def lookup_lo_projection(V, p, hi, r):
425  match r:
426    case Tuple{lo, value}:
427      {==}
428
429law lookup_hi_projection:
430  for -V: Data
431  for p: Nat
432  for lo: Map<&2, V>
433  for r: Map<&2, V> & V
434  {lookup_map(V, Map.hi(&2, V, V, p, lo, r)) == MNode{p, lo, lookup_map(V, r)} : Map<&2, V>}
435def lookup_hi_projection(V, p, lo, r):
436  match r:
437    case Tuple{hi, value}:
438      {==}
439
440law lookup_branch_preserves:
441  for -V: Data
442  for +d: V
443  for +lo: Map<&2, V>
444  for +hi: Map<&2, V>
445  for +p: Nat
446  for kb: String & Bool
447  for lp: @key: String -> {lookup_map(V, Map.get(V, d, lo, key)) == lo : Map<&2, V>}
448  for hp: @key: String -> {lookup_map(V, Map.get(V, d, hi, key)) == hi : Map<&2, V>}
449  {lookup_map(V, MB.get_bit(V, d, lo, hi, p, kb)) == MNode{p, lo, hi} : Map<&2, V>}
450def lookup_branch_preserves(V, d, lo, hi, p, kb, lp, hp):
451  match kb:
452    case Tuple{+key, False{}}:
453      Equal.trans(Map<&2, V>, lookup_map(V, Map.lo(&2, V, V, p, hi, Map.get(V, d, lo, key))), MNode{p, lookup_map(V, Map.get(V, d, lo, key)), hi}, MNode{p, lo, hi}, lookup_lo_projection(V, p, hi, Map.get(V, d, lo, key)), Equal.cong(Map<&2, V>, Map<&2, V>, m => MNode{p, m, hi}, lookup_map(V, Map.get(V, d, lo, key)), lo, lp(key)))
454    case Tuple{+key, True{}}:
455      Equal.trans(Map<&2, V>, lookup_map(V, Map.hi(&2, V, V, p, lo, Map.get(V, d, hi, key))), MNode{p, lo, lookup_map(V, Map.get(V, d, hi, key))}, MNode{p, lo, hi}, lookup_hi_projection(V, p, lo, Map.get(V, d, hi, key)), Equal.cong(Map<&2, V>, Map<&2, V>, m => MNode{p, lo, m}, lookup_map(V, Map.get(V, d, hi, key)), hi, hp(key)))
456
457law lookup_preserves_map:
458  for -V: Data
459  for +d: V
460  for m: Map<&2, V>
461  for +key: String
462  {lookup_map(V, Map.get(V, d, m, key)) == m : Map<&2, V>}
463def lookup_preserves_map(V, d, m, key):
464  match m:
465    case MTip{}:
466      {==}
467    case MLeaf{+stored, v}:
468      %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), comparison_tag(String, String.cmp(key, stored))), string_comparison_shape(key, stored)) : {lookup_map(V, Map.get.leaf(V, d, v, _)) == MLeaf{stored, v} : Map<&2, V>}
469      lookup_leaf_preserves(V, d, v, key, stored, comparison_tag(String, String.cmp(key, stored)))
470    case MNode{+p, +lo, +hi}:
471      %Equal.sym(Map<&2, V> & V, Map.get(V, d, MNode{p, lo, hi}, key), MB.get_bit(V, d, lo, hi, p, Map.bit(key, p)), MB.get_node(V, d, p, lo, hi, key)) : {lookup_map(V, _) == MNode{p, lo, hi} : Map<&2, V>}
472      lookup_branch_preserves(V, d, lo, hi, p, Map.bit(key, p), q => lookup_preserves_map(V, d, lo, q), q => lookup_preserves_map(V, d, hi, q))
473
474law natural_add_associative:
475  for a: Nat
476  for b: Nat
477  for c: Nat
478  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
479def natural_add_associative(a, b, c):
480  match a:
481    case 0n:
482      {==}
483    case 1n+p:
484      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, Nat.add(b, c)), Nat.add(Nat.add(p, b), c), natural_add_associative(p, b, c))
485
486law natural_add_right_zero:
487  for a: Nat
488  {Nat.add(a, 0n) == a : Nat}
489def natural_add_right_zero(a):
490  match a:
491    case 0n:
492      {==}
493    case 1n+p:
494      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, natural_add_right_zero(p))
495
496law keys_accumulator_size:
497  for -V: Data
498  for m: Map<&2, V>
499  for +acc: List<&2, String>
500  {List.length(&2, String, Map.keys.go(&2, V, m, acc)) == Nat.add(Map.size(&2, V, m), List.length(&2, String, acc)) : Nat}
501def keys_accumulator_size(V, m, acc):
502  match m:
503    case MTip{}:
504      {==}
505    case MLeaf{key, value}:
506      {==}
507    case MNode{p, +lo, +hi}:
508      %Equal.sym(Nat, List.length(&2, String, Map.keys.go(&2, V, lo, Map.keys.go(&2, V, hi, acc))), Nat.add(Map.size(&2, V, lo), List.length(&2, String, Map.keys.go(&2, V, hi, acc))), keys_accumulator_size(V, lo, Map.keys.go(&2, V, hi, acc))) : {_ == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, String, acc)) : Nat}
509      %Equal.sym(Nat, List.length(&2, String, Map.keys.go(&2, V, hi, acc)), Nat.add(Map.size(&2, V, hi), List.length(&2, String, acc)), keys_accumulator_size(V, hi, acc)) : {Nat.add(Map.size(&2, V, lo), _) == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, String, acc)) : Nat}
510      natural_add_associative(Map.size(&2, V, lo), Map.size(&2, V, hi), List.length(&2, String, acc))
511
512law keys_size:
513  for -V: Data
514  for +m: Map<&2, V>
515  {List.length(&2, String, Map.keys(&2, V, m)) == Map.size(&2, V, m) : Nat}
516def keys_size(V, m):
517  Equal.trans(Nat, List.length(&2, String, Map.keys(&2, V, m)), Nat.add(Map.size(&2, V, m), 0n), Map.size(&2, V, m), keys_accumulator_size(V, m, Nil{}), natural_add_right_zero(Map.size(&2, V, m)))
518
519law entries_accumulator_size:
520  for -V: Data
521  for m: Map<&2, V>
522  for +acc: List<&2, Sigma<&2, &2, String, _ => V>>
523  {List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, m, acc)) == Nat.add(Map.size(&2, V, m), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)) : Nat}
524def entries_accumulator_size(V, m, acc):
525  match m:
526    case MTip{}:
527      {==}
528    case MLeaf{key, value}:
529      {==}
530    case MNode{p, +lo, +hi}:
531      %Equal.sym(Nat, List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, lo, Map.to_list.go(&2, V, hi, acc))), Nat.add(Map.size(&2, V, lo), List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, hi, acc))), entries_accumulator_size(V, lo, Map.to_list.go(&2, V, hi, acc))) : {_ == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)) : Nat}
532      %Equal.sym(Nat, List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, hi, acc)), Nat.add(Map.size(&2, V, hi), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)), entries_accumulator_size(V, hi, acc)) : {Nat.add(Map.size(&2, V, lo), _) == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)) : Nat}
533      natural_add_associative(Map.size(&2, V, lo), Map.size(&2, V, hi), List.length(&2, Sigma<&2, &2, String, _ => V>, acc))
534
535law entries_size:
536  for -V: Data
537  for +m: Map<&2, V>
538  {List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list(&2, V, m)) == Map.size(&2, V, m) : Nat}
539def entries_size(V, m):
540  Equal.trans(Nat, List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list(&2, V, m)), Nat.add(Map.size(&2, V, m), 0n), Map.size(&2, V, m), entries_accumulator_size(V, m, Nil{}), natural_add_right_zero(Map.size(&2, V, m)))