proofs/lib/lemmas/proofs/map_bridge.bend

bend-collections-laws-crypto@1.0.0.0 · 417 lines · 26 definitions

1import Base
2
3# Bend 2.0.32 rewrote Base's Map descents (get, has, put, pop, seek, ins) as
4# one-level `Map.X.go` functions over the whole node. The lemmas in this
5# library were written against 2.0.28's shape, where Map.X on a node branched
6# through a `.bit` helper (`.deep`/`.if` for ins) that recursed with Map.X on
7# the chosen child. Mutual recursion is no longer allowed, so those helpers
8# are defined here non-recursively, each calling Base's current Map.X on the
9# child, and each comes with a bridge law: Map.X on a node equals the helper.
10# Every bridge holds by unfolding both sides (no induction).
11
12# ---- the routed key: Map.bit keeps the key (from native_map.bend) ----
13
14def routed_key(r: String & Bool) -> String:
15  (key, bit) = r
16  key
17
18law recursive_bit_key:
19  for c: Char
20  for r: String & Bool
21  {routed_key(Map.bit.go.rec(c, r)) == SCon{c, routed_key(r)} : String}
22def recursive_bit_key(c, r):
23  match r:
24    case Tuple{key, bit}:
25      {==}
26
27law bit_go_preserves_key:
28  for key: String
29  for +character: Nat
30  for +offset: Nat
31  {routed_key(Map.bit.go(key, character, offset)) == key : String}
32def bit_go_preserves_key(key, character, offset):
33  match key character offset:
34    case SNil{} ci off:
35      {==}
36    case SCon{Chr{x}, tail} 0n 0n:
37      {==}
38    case SCon{Chr{x}, tail} 0n 1n+off:
39      {==}
40    case SCon{Chr{x}, +tail} 1n+ci off:
41      +c = {Chr{x} : Char}
42      Equal.trans(String, routed_key(Map.bit.go.rec(c, Map.bit.go(tail, ci, off))),
43        SCon{c, routed_key(Map.bit.go(tail, ci, off))}, SCon{c, tail},
44        recursive_bit_key(c, Map.bit.go(tail, ci, off)),
45        Equal.cong(String, String, t => SCon{c, t}, routed_key(Map.bit.go(tail, ci, off)), tail, bit_go_preserves_key(tail, ci, off)))
46
47law bit_at_preserves_key:
48  for key: String
49  for coordinates: Nat & Nat
50  {routed_key(Map.bit.at(key, coordinates)) == key : String}
51def bit_at_preserves_key(key, coordinates):
52  match coordinates:
53    case Tuple{ci, off}:
54      bit_go_preserves_key(key, ci, off)
55
56law bit_preserves_key:
57  for key: String
58  for position: Nat
59  {routed_key(Map.bit(key, position)) == key : String}
60def bit_preserves_key(key, position):
61  bit_at_preserves_key(key, Nat.divmod(position, 33n))
62
63# ---- one-step helpers (2.0.28's `.bit` shape over Base's current Map) ----
64
65def get_bit(-V: Data, d: V, lo: Map<&2, V>, hi: Map<&2, V>, p2: Nat, kb: String & Bool) -> Map<&2, V> & V:
66  (key2, b) = kb
67  match b:
68    case False{}:
69      Map.lo(&2, V, V, p2, hi, Map.get(V, d, lo, key2))
70    case True{}:
71      Map.hi(&2, V, V, p2, lo, Map.get(V, d, hi, key2))
72
73def has_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & Bool:
74  (key2, b) = kb
75  match b:
76    case False{}:
77      Map.lo(a, V, Bool, p2, hi, Map.has(a, V, lo, key2))
78    case True{}:
79      Map.hi(a, V, Bool, p2, lo, Map.has(a, V, hi, key2))
80
81def put_bit(-a: Quant, -V: Kind(a), x: V, p2: Nat, lo: Map<a, V>, hi: Map<a, V>, kb: String & Bool) -> Map<a, V>:
82  (key2, b) = kb
83  match b:
84    case False{}:
85      MNode{p2, Map.put(a, V, lo, key2, x), hi}
86    case True{}:
87      MNode{p2, lo, Map.put(a, V, hi, key2, x)}
88
89def pop_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & Maybe<a, V>:
90  (key2, b) = kb
91  match b:
92    case False{}:
93      Map.pop.lo(a, V, p2, hi, Map.pop(a, V, lo, key2))
94    case True{}:
95      Map.pop.hi(a, V, p2, lo, Map.pop(a, V, hi, key2))
96
97def seek_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & String & Maybe<&2, String>:
98  (key2, b) = kb
99  match b:
100    case False{}:
101      Map.lo(a, V, String & Maybe<&2, String>, p2, hi, Map.seek(a, V, lo, key2))
102    case True{}:
103      Map.hi(a, V, String & Maybe<&2, String>, p2, lo, Map.seek(a, V, hi, key2))
104
105def ins_deep(-a: Quant, -V: Kind(a), x: V, lo: Map<a, V>, hi: Map<a, V>, pb: Nat, qb: Nat, kb: String & Bool) -> Map<a, V>:
106  (key2, b) = kb
107  match b:
108    case False{}:
109      MNode{qb, Map.ins(a, V, lo, key2, x, pb), hi}
110    case True{}:
111      MNode{qb, lo, Map.ins(a, V, hi, key2, x, pb)}
112
113def ins_if(-a: Quant, -V: Kind(a), key: String, x: V, lo: Map<a, V>, hi: Map<a, V>, +p2: Nat, pb: Nat, t: Bool) -> Map<a, V>:
114  match t:
115    case False{}:
116      Map.ins.splice(a, V, pb, key, x, MNode{p2, lo, hi})
117    case True{}:
118      ins_deep(a, V, x, lo, hi, pb, p2, Map.bit(key, p2))
119
120# ---- bridges: Base Map.X on a node is the one-step helper ----
121
122law get_go_bridge:
123  for -V: Data
124    for d: V
125for +p: Nat
126  for lo: Map<&2, V>
127  for hi: Map<&2, V>
128  for kb: String & Bool
129  {Map.get.go(V, MNode{p, lo, hi}, d, kb) == get_bit(V, d, lo, hi, p, kb) : Map<&2, V> & V}
130def get_go_bridge(V, d, p, lo, hi, kb):
131  match lo hi kb:
132    case MTip{} _ Tuple{key2, False{}}:
133      {==}
134    case MLeaf{k, v} _ Tuple{key2, False{}}:
135      {==}
136    case MNode{q, c, e} _ Tuple{key2, False{}}:
137      {==}
138    case _ MTip{} Tuple{key2, True{}}:
139      {==}
140    case _ MLeaf{k, v} Tuple{key2, True{}}:
141      {==}
142    case _ MNode{q, c, e} Tuple{key2, True{}}:
143      {==}
144
145law get_node:
146  for -V: Data
147    for d: V
148for +p: Nat
149  for lo: Map<&2, V>
150  for hi: Map<&2, V>
151  for key: String
152  {Map.get(V, d, MNode{p, lo, hi}, key) == get_bit(V, d, lo, hi, p, Map.bit(key, p)) : Map<&2, V> & V}
153def get_node(V, d, p, lo, hi, key):
154  get_go_bridge(V, d, p, lo, hi, Map.bit(key, p))
155
156law has_go_bridge:
157  for -a: Quant
158  for -V: Kind(a)
159  for +p: Nat
160  for lo: Map<a, V>
161  for hi: Map<a, V>
162  for kb: String & Bool
163  {Map.has.go(a, V, MNode{p, lo, hi}, kb) == has_bit(a, V, lo, hi, p, kb) : Map<a, V> & Bool}
164def has_go_bridge(a, V, p, lo, hi, kb):
165  match lo hi kb:
166    case MTip{} _ Tuple{key2, False{}}:
167      {==}
168    case MLeaf{k, v} _ Tuple{key2, False{}}:
169      {==}
170    case MNode{q, c, e} _ Tuple{key2, False{}}:
171      {==}
172    case _ MTip{} Tuple{key2, True{}}:
173      {==}
174    case _ MLeaf{k, v} Tuple{key2, True{}}:
175      {==}
176    case _ MNode{q, c, e} Tuple{key2, True{}}:
177      {==}
178
179law has_node:
180  for -a: Quant
181  for -V: Kind(a)
182  for +p: Nat
183  for lo: Map<a, V>
184  for hi: Map<a, V>
185  for key: String
186  {Map.has(a, V, MNode{p, lo, hi}, key) == has_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map<a, V> & Bool}
187def has_node(a, V, p, lo, hi, key):
188  has_go_bridge(a, V, p, lo, hi, Map.bit(key, p))
189
190law put_go_bridge:
191  for -a: Quant
192  for -V: Kind(a)
193    for x: V
194for +p: Nat
195  for lo: Map<a, V>
196  for hi: Map<a, V>
197  for kb: String & Bool
198  {Map.put.go(a, V, MNode{p, lo, hi}, x, kb) == put_bit(a, V, x, p, lo, hi, kb) : Map<a, V>}
199def put_go_bridge(a, V, x, p, lo, hi, kb):
200  match lo hi kb:
201    case MTip{} _ Tuple{key2, False{}}:
202      {==}
203    case MLeaf{k, v} _ Tuple{key2, False{}}:
204      {==}
205    case MNode{q, c, e} _ Tuple{key2, False{}}:
206      {==}
207    case _ MTip{} Tuple{key2, True{}}:
208      {==}
209    case _ MLeaf{k, v} Tuple{key2, True{}}:
210      {==}
211    case _ MNode{q, c, e} Tuple{key2, True{}}:
212      {==}
213
214law put_node:
215  for -a: Quant
216  for -V: Kind(a)
217    for x: V
218for +p: Nat
219  for lo: Map<a, V>
220  for hi: Map<a, V>
221  for key: String
222  {Map.put(a, V, MNode{p, lo, hi}, key, x) == put_bit(a, V, x, p, lo, hi, Map.bit(key, p)) : Map<a, V>}
223def put_node(a, V, x, p, lo, hi, key):
224  put_go_bridge(a, V, x, p, lo, hi, Map.bit(key, p))
225
226law pop_go_bridge:
227  for -a: Quant
228  for -V: Kind(a)
229  for +p: Nat
230  for lo: Map<a, V>
231  for hi: Map<a, V>
232  for kb: String & Bool
233  {Map.pop.go(a, V, MNode{p, lo, hi}, kb) == pop_bit(a, V, lo, hi, p, kb) : Map<a, V> & Maybe<a, V>}
234def pop_go_bridge(a, V, p, lo, hi, kb):
235  match lo hi kb:
236    case MTip{} _ Tuple{key2, False{}}:
237      {==}
238    case MLeaf{k, v} _ Tuple{key2, False{}}:
239      {==}
240    case MNode{q, c, e} _ Tuple{key2, False{}}:
241      {==}
242    case _ MTip{} Tuple{key2, True{}}:
243      {==}
244    case _ MLeaf{k, v} Tuple{key2, True{}}:
245      {==}
246    case _ MNode{q, c, e} Tuple{key2, True{}}:
247      {==}
248
249law pop_node:
250  for -a: Quant
251  for -V: Kind(a)
252  for +p: Nat
253  for lo: Map<a, V>
254  for hi: Map<a, V>
255  for key: String
256  {Map.pop(a, V, MNode{p, lo, hi}, key) == pop_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map<a, V> & Maybe<a, V>}
257def pop_node(a, V, p, lo, hi, key):
258  pop_go_bridge(a, V, p, lo, hi, Map.bit(key, p))
259
260law seek_go_bridge:
261  for -a: Quant
262  for -V: Kind(a)
263  for +p: Nat
264  for lo: Map<a, V>
265  for hi: Map<a, V>
266  for kb: String & Bool
267  {Map.seek.go(a, V, MNode{p, lo, hi}, kb) == seek_bit(a, V, lo, hi, p, kb) : Map<a, V> & String & Maybe<&2, String>}
268def seek_go_bridge(a, V, p, lo, hi, kb):
269  match lo hi kb:
270    case MTip{} _ Tuple{key2, False{}}:
271      {==}
272    case MLeaf{k, v} _ Tuple{key2, False{}}:
273      {==}
274    case MNode{q, c, e} _ Tuple{key2, False{}}:
275      {==}
276    case _ MTip{} Tuple{key2, True{}}:
277      {==}
278    case _ MLeaf{k, v} Tuple{key2, True{}}:
279      {==}
280    case _ MNode{q, c, e} Tuple{key2, True{}}:
281      {==}
282
283law seek_node:
284  for -a: Quant
285  for -V: Kind(a)
286  for +p: Nat
287  for lo: Map<a, V>
288  for hi: Map<a, V>
289  for key: String
290  {Map.seek(a, V, MNode{p, lo, hi}, key) == seek_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map<a, V> & String & Maybe<&2, String>}
291def seek_node(a, V, p, lo, hi, key):
292  seek_go_bridge(a, V, p, lo, hi, Map.bit(key, p))
293
294law ins_splice_bridge:
295  for -a: Quant
296  for -V: Kind(a)
297  for +q: Nat
298  for lo: Map<a, V>
299  for hi: Map<a, V>
300  for x: V
301  for +p: Nat
302  for key: String
303  for kb: String & Bool
304  for hk: {routed_key(kb) == key : String}
305  {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, False{}) == Map.ins.splice(a, V, p, key, x, MNode{q, lo, hi}) : Map<a, V>}
306def ins_splice_bridge(a, V, q, lo, hi, x, p, key, kb, hk):
307  match lo hi kb:
308    case MTip{} MTip{} Tuple{k2, False{}}:
309      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MTip{}}) : Map<a, V>}
310      {==}
311    case MTip{} MTip{} Tuple{k2, True{}}:
312      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MTip{}}) : Map<a, V>}
313      {==}
314    case MTip{} MLeaf{k3, v3} Tuple{k2, False{}}:
315      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MLeaf{k3, v3}}) : Map<a, V>}
316      {==}
317    case MTip{} MLeaf{k3, v3} Tuple{k2, True{}}:
318      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MLeaf{k3, v3}}) : Map<a, V>}
319      {==}
320    case MTip{} MNode{r3, c3, e3} Tuple{k2, False{}}:
321      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) : Map<a, V>}
322      {==}
323    case MTip{} MNode{r3, c3, e3} Tuple{k2, True{}}:
324      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) : Map<a, V>}
325      {==}
326    case MLeaf{k1, v1} MTip{} Tuple{k2, False{}}:
327      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MTip{}}) : Map<a, V>}
328      {==}
329    case MLeaf{k1, v1} MTip{} Tuple{k2, True{}}:
330      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MTip{}}) : Map<a, V>}
331      {==}
332    case MLeaf{k1, v1} MLeaf{k3, v3} Tuple{k2, False{}}:
333      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) : Map<a, V>}
334      {==}
335    case MLeaf{k1, v1} MLeaf{k3, v3} Tuple{k2, True{}}:
336      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) : Map<a, V>}
337      {==}
338    case MLeaf{k1, v1} MNode{r3, c3, e3} Tuple{k2, False{}}:
339      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) : Map<a, V>}
340      {==}
341    case MLeaf{k1, v1} MNode{r3, c3, e3} Tuple{k2, True{}}:
342      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) : Map<a, V>}
343      {==}
344    case MNode{r1, c1, e1} MTip{} Tuple{k2, False{}}:
345      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) : Map<a, V>}
346      {==}
347    case MNode{r1, c1, e1} MTip{} Tuple{k2, True{}}:
348      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) : Map<a, V>}
349      {==}
350    case MNode{r1, c1, e1} MLeaf{k3, v3} Tuple{k2, False{}}:
351      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) : Map<a, V>}
352      {==}
353    case MNode{r1, c1, e1} MLeaf{k3, v3} Tuple{k2, True{}}:
354      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) : Map<a, V>}
355      {==}
356    case MNode{r1, c1, e1} MNode{r3, c3, e3} Tuple{k2, False{}}:
357      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) : Map<a, V>}
358      {==}
359    case MNode{r1, c1, e1} MNode{r3, c3, e3} Tuple{k2, True{}}:
360      %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) : Map<a, V>}
361      {==}
362
363law ins_deep_bridge:
364  for -a: Quant
365  for -V: Kind(a)
366  for +q: Nat
367  for lo: Map<a, V>
368  for hi: Map<a, V>
369  for x: V
370  for +p: Nat
371  for kb: String & Bool
372  {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, True{}) == ins_deep(a, V, x, lo, hi, p, q, kb) : Map<a, V>}
373def ins_deep_bridge(a, V, q, lo, hi, x, p, kb):
374  match lo hi kb:
375    case MTip{} _ Tuple{key2, False{}}:
376      {==}
377    case MLeaf{k, v} _ Tuple{key2, False{}}:
378      {==}
379    case MNode{r, c, e} _ Tuple{key2, False{}}:
380      {==}
381    case _ MTip{} Tuple{key2, True{}}:
382      {==}
383    case _ MLeaf{k, v} Tuple{key2, True{}}:
384      {==}
385    case _ MNode{r, c, e} Tuple{key2, True{}}:
386      {==}
387
388law ins_t:
389  for -a: Quant
390  for -V: Kind(a)
391  for +pos: Nat
392  for lo: Map<a, V>
393  for hi: Map<a, V>
394  for +key: String
395  for x: V
396  for +p: Nat
397  for t: Bool
398  {Map.ins.go(a, V, MNode{pos, lo, hi}, x, p, Map.bit(key, pos), t) == ins_if(a, V, key, x, lo, hi, pos, p, t) : Map<a, V>}
399def ins_t(a, V, pos, lo, hi, key, x, p, t):
400  match t:
401    case False{}:
402      ins_splice_bridge(a, V, pos, lo, hi, x, p, key, Map.bit(key, pos), bit_preserves_key(key, pos))
403    case True{}:
404      ins_deep_bridge(a, V, pos, lo, hi, x, p, Map.bit(key, pos))
405
406law ins_node:
407  for -a: Quant
408  for -V: Kind(a)
409  for +pos: Nat
410  for lo: Map<a, V>
411  for hi: Map<a, V>
412  for +key: String
413  for x: V
414  for +p: Nat
415  {Map.ins(a, V, MNode{pos, lo, hi}, key, x, p) == ins_if(a, V, key, x, lo, hi, pos, p, Nat.is_lt(pos, p)) : Map<a, V>}
416def ins_node(a, V, pos, lo, hi, key, x, p):
417  ins_t(a, V, pos, lo, hi, key, x, p, Nat.is_lt(pos, p))