proofs/lib/lemmas/proofs/map_insert.bend
bend-collections-laws-containers@1.0.0.0 · 474 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend as MB
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as N
4
5# Projections of actual native results; no alternative lookup algorithm.
6def value(-V: Data, result: Map<&2, V> & V) -> V:
7 (tree, found) = result
8 found
9
10def lookup(-V: Data, d: V, m: Map<&2, V>, key: String) -> V:
11 value(V, Map.get(V, d, m, key))
12
13def route_bit(r: String & Bool) -> Bool:
14 (key, bit) = r
15 bit
16
17law route_pair:
18 for r: String & Bool
19 {r == (N.routed_key(r), route_bit(r)) : String & Bool}
20def route_pair(r):
21 match r:
22 case Tuple{key, bit}:
23 {==}
24
25law route_shape:
26 for +key: String
27 for +position: Nat
28 {Map.bit(key, position) == (key, route_bit(Map.bit(key, position))) : String & Bool}
29def route_shape(key, position):
30 %N.bit_preserves_key(key, position) : {Map.bit(key, position) == (_, route_bit(Map.bit(key, position))) : String & Bool}
31 route_pair(Map.bit(key, position))
32
33law low_value:
34 for -V: Data
35 for p: Nat
36 for hi: Map<&2, V>
37 for r: Map<&2, V> & V
38 {value(V, Map.lo(&2, V, V, p, hi, r)) == value(V, r) : V}
39def low_value(V, p, hi, r):
40 match r:
41 case Tuple{tree, found}:
42 {==}
43
44law high_value:
45 for -V: Data
46 for p: Nat
47 for lo: Map<&2, V>
48 for r: Map<&2, V> & V
49 {value(V, Map.hi(&2, V, V, p, lo, r)) == value(V, r) : V}
50def high_value(V, p, lo, r):
51 match r:
52 case Tuple{tree, found}:
53 {==}
54
55law node_left:
56 for -V: Data
57 for +d: V
58 for +lo: Map<&2, V>
59 for +hi: Map<&2, V>
60 for +p: Nat
61 for +key: String
62 for e: {Map.bit(key, p) == (key, False{}) : String & Bool}
63 {lookup(V, d, MNode{p, lo, hi}, key) == lookup(V, d, lo, key) : V}
64def node_left(V, d, lo, hi, p, key, e):
65 %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)) : {value(V, _) == lookup(V, d, lo, key) : V}
66 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {value(V, MB.get_bit(V, d, lo, hi, p, _)) == lookup(V, d, lo, key) : V}
67 low_value(V, p, hi, Map.get(V, d, lo, key))
68
69law node_right:
70 for -V: Data
71 for +d: V
72 for +lo: Map<&2, V>
73 for +hi: Map<&2, V>
74 for +p: Nat
75 for +key: String
76 for e: {Map.bit(key, p) == (key, True{}) : String & Bool}
77 {lookup(V, d, MNode{p, lo, hi}, key) == lookup(V, d, hi, key) : V}
78def node_right(V, d, lo, hi, p, key, e):
79 %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)) : {value(V, _) == lookup(V, d, hi, key) : V}
80 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {value(V, MB.get_bit(V, d, lo, hi, p, _)) == lookup(V, d, hi, key) : V}
81 high_value(V, p, lo, Map.get(V, d, hi, key))
82
83law leaf_same:
84 for -V: Data
85 for d: V
86 for key: String
87 for x: V
88 {lookup(V, d, MLeaf{key, x}, key) == x : V}
89def leaf_same(V, d, key, x):
90 Equal.cong(Map<&2, V> & V, V, r => value(V, r), Map.get(V, d, MLeaf{key, x}, key), (MLeaf{key, x}, x), N.singleton_get(V, d, key, x))
91
92law splice_same_bit:
93 for -V: Data
94 for +d: V
95 for +x: V
96 for +rest: Map<&2, V>
97 for +p: Nat
98 for +key: String
99 for bit: Bool
100 for e: {Map.bit(key, p) == (key, bit) : String & Bool}
101 {lookup(V, d, Map.ins.splice.bit(&2, V, x, rest, p, (key, bit)), key) == x : V}
102def splice_same_bit(V, d, x, rest, p, key, bit, e):
103 match bit:
104 case False{}:
105 Equal.trans(V, lookup(V, d, MNode{p, MLeaf{key, x}, rest}, key), lookup(V, d, MLeaf{key, x}, key), x, node_left(V, d, MLeaf{key, x}, rest, p, key, e), leaf_same(V, d, key, x))
106 case True{}:
107 Equal.trans(V, lookup(V, d, MNode{p, rest, MLeaf{key, x}}, key), lookup(V, d, MLeaf{key, x}, key), x, node_right(V, d, rest, MLeaf{key, x}, p, key, e), leaf_same(V, d, key, x))
108
109law splice_same:
110 for -V: Data
111 for d: V
112 for x: V
113 for rest: Map<&2, V>
114 for +p: Nat
115 for +key: String
116 {lookup(V, d, Map.ins.splice(&2, V, p, key, x, rest), key) == x : V}
117def splice_same(V, d, x, rest, p, key):
118 %Equal.sym(String & Bool, Map.bit(key, p), (key, route_bit(Map.bit(key, p))), route_shape(key, p)) : {lookup(V, d, Map.ins.splice.bit(&2, V, x, rest, p, _), key) == x : V}
119 splice_same_bit(V, d, x, rest, p, key, route_bit(Map.bit(key, p)), route_shape(key, p))
120
121law deep_same_bit:
122 for -V: Data
123 for +d: V
124 for +x: V
125 for +lo: Map<&2, V>
126 for +hi: Map<&2, V>
127 for +p: Nat
128 for +q: Nat
129 for +key: String
130 for bit: Bool
131 for e: {Map.bit(key, q) == (key, bit) : String & Bool}
132 for lp: {lookup(V, d, Map.ins(&2, V, lo, key, x, p), key) == x : V}
133 for hp: {lookup(V, d, Map.ins(&2, V, hi, key, x, p), key) == x : V}
134 {lookup(V, d, MB.ins_deep(&2, V, x, lo, hi, p, q, (key, bit)), key) == x : V}
135def deep_same_bit(V, d, x, lo, hi, p, q, key, bit, e, lp, hp):
136 match bit:
137 case False{}:
138 Equal.trans(V, lookup(V, d, MNode{q, Map.ins(&2, V, lo, key, x, p), hi}, key), lookup(V, d, Map.ins(&2, V, lo, key, x, p), key), x, node_left(V, d, Map.ins(&2, V, lo, key, x, p), hi, q, key, e), lp)
139 case True{}:
140 Equal.trans(V, lookup(V, d, MNode{q, lo, Map.ins(&2, V, hi, key, x, p)}, key), lookup(V, d, Map.ins(&2, V, hi, key, x, p), key), x, node_right(V, d, lo, Map.ins(&2, V, hi, key, x, p), q, key, e), hp)
141
142law insertion_branch_same:
143 for -V: Data
144 for d: V
145 for x: V
146 for lo: Map<&2, V>
147 for hi: Map<&2, V>
148 for p: Nat
149 for +q: Nat
150 for +key: String
151 for descend: Bool
152 for lp: {lookup(V, d, Map.ins(&2, V, lo, key, x, p), key) == x : V}
153 for hp: {lookup(V, d, Map.ins(&2, V, hi, key, x, p), key) == x : V}
154 {lookup(V, d, MB.ins_if(&2, V, key, x, lo, hi, q, p, descend), key) == x : V}
155def insertion_branch_same(V, d, x, lo, hi, p, q, key, descend, lp, hp):
156 match descend:
157 case False{}:
158 splice_same(V, d, x, MNode{q, lo, hi}, p, key)
159 case True{}:
160 %Equal.sym(String & Bool, Map.bit(key, q), (key, route_bit(Map.bit(key, q))), route_shape(key, q)) : {lookup(V, d, MB.ins_deep(&2, V, x, lo, hi, p, q, _), key) == x : V}
161 deep_same_bit(V, d, x, lo, hi, p, q, key, route_bit(Map.bit(key, q)), route_shape(key, q), lp, hp)
162
163# This actual native insertion law needs no well-formedness assumption: querying
164# the new key follows the same bits used to choose its newly inserted leaf.
165# Other-key preservation DOES require valid discriminator/difference properties.
166law insertion_same:
167 for -V: Data
168 for +d: V
169 for m: Map<&2, V>
170 for +key: String
171 for +x: V
172 for +p: Nat
173 {lookup(V, d, Map.ins(&2, V, m, key, x, p), key) == x : V}
174def insertion_same(V, d, m, key, x, p):
175 match m:
176 case MTip{}:
177 leaf_same(V, d, key, x)
178 case MLeaf{k, v}:
179 splice_same(V, d, x, MLeaf{k, v}, p, key)
180 case MNode{+q, +lo, +hi}:
181 %Equal.sym(Map<&2, V>, Map.ins(&2, V, MNode{q, lo, hi}, key, x, p), MB.ins_if(&2, V, key, x, lo, hi, q, p, Nat.is_lt(q, p)), MB.ins_node(&2, V, q, lo, hi, key, x, p)) : {lookup(V, d, _, key) == x : V}
182 insertion_branch_same(V, d, x, lo, hi, p, q, key, Nat.is_lt(q, p), insertion_same(V, d, lo, key, x, p), insertion_same(V, d, hi, key, x, p))
183
184def seek_found(-V: Data, r: Map<&2, V> & String & Maybe<&2, String>) -> Maybe<&2, String>:
185 (tree, key, found) = r
186 found
187
188law seek_low_found:
189 for -V: Data
190 for p: Nat
191 for hi: Map<&2, V>
192 for r: Map<&2, V> & String & Maybe<&2, String>
193 {seek_found(V, Map.lo(&2, V, String & Maybe<&2, String>, p, hi, r)) == seek_found(V, r) : Maybe<&2, String>}
194def seek_low_found(V, p, hi, r):
195 match r:
196 case Tuple{tree, Tuple{key, found}}:
197 {==}
198
199law seek_high_found:
200 for -V: Data
201 for p: Nat
202 for lo: Map<&2, V>
203 for r: Map<&2, V> & String & Maybe<&2, String>
204 {seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r)) == seek_found(V, r) : Maybe<&2, String>}
205def seek_high_found(V, p, lo, r):
206 match r:
207 case Tuple{tree, Tuple{key, found}}:
208 {==}
209
210law seek_left:
211 for -V: Data
212 for +lo: Map<&2, V>
213 for +hi: Map<&2, V>
214 for +p: Nat
215 for +key: String
216 for e: {Map.bit(key, p) == (key, False{}) : String & Bool}
217 {seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)) == seek_found(V, Map.seek(&2, V, lo, key)) : Maybe<&2, String>}
218def seek_left(V, lo, hi, p, key, e):
219 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {seek_found(V, _) == seek_found(V, Map.seek(&2, V, lo, key)) : Maybe<&2, String>}
220 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _)) == seek_found(V, Map.seek(&2, V, lo, key)) : Maybe<&2, String>}
221 seek_low_found(V, p, hi, Map.seek(&2, V, lo, key))
222
223law seek_right:
224 for -V: Data
225 for +lo: Map<&2, V>
226 for +hi: Map<&2, V>
227 for +p: Nat
228 for +key: String
229 for e: {Map.bit(key, p) == (key, True{}) : String & Bool}
230 {seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)) == seek_found(V, Map.seek(&2, V, hi, key)) : Maybe<&2, String>}
231def seek_right(V, lo, hi, p, key, e):
232 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {seek_found(V, _) == seek_found(V, Map.seek(&2, V, hi, key)) : Maybe<&2, String>}
233 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _)) == seek_found(V, Map.seek(&2, V, hi, key)) : Maybe<&2, String>}
234 seek_high_found(V, p, lo, Map.seek(&2, V, hi, key))
235
236law replace_left:
237 for -V: Data
238 for d: V
239 for +lo: Map<&2, V>
240 for +hi: Map<&2, V>
241 for +p: Nat
242 for +key: String
243 for +x: V
244 for +e: {Map.bit(key, p) == (key, False{}) : String & Bool}
245 {lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key) == lookup(V, d, Map.put(&2, V, lo, key, x), key) : V}
246def replace_left(V, d, lo, hi, p, key, x, e):
247 %Equal.sym(Map<&2, V>, Map.put(&2, V, MNode{p, lo, hi}, key, x), MB.put_bit(&2, V, x, p, lo, hi, Map.bit(key, p)), MB.put_node(&2, V, x, p, lo, hi, key)) : {lookup(V, d, _, key) == lookup(V, d, Map.put(&2, V, lo, key, x), key) : V}
248 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {lookup(V, d, MB.put_bit(&2, V, x, p, lo, hi, _), key) == lookup(V, d, Map.put(&2, V, lo, key, x), key) : V}
249 node_left(V, d, Map.put(&2, V, lo, key, x), hi, p, key, e)
250
251law replace_right:
252 for -V: Data
253 for d: V
254 for +lo: Map<&2, V>
255 for +hi: Map<&2, V>
256 for +p: Nat
257 for +key: String
258 for +x: V
259 for +e: {Map.bit(key, p) == (key, True{}) : String & Bool}
260 {lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key) == lookup(V, d, Map.put(&2, V, hi, key, x), key) : V}
261def replace_right(V, d, lo, hi, p, key, x, e):
262 %Equal.sym(Map<&2, V>, Map.put(&2, V, MNode{p, lo, hi}, key, x), MB.put_bit(&2, V, x, p, lo, hi, Map.bit(key, p)), MB.put_node(&2, V, x, p, lo, hi, key)) : {lookup(V, d, _, key) == lookup(V, d, Map.put(&2, V, hi, key, x), key) : V}
263 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {lookup(V, d, MB.put_bit(&2, V, x, p, lo, hi, _), key) == lookup(V, d, Map.put(&2, V, hi, key, x), key) : V}
264 node_right(V, d, lo, Map.put(&2, V, hi, key, x), p, key, e)
265
266def replacement_certificate(-V: Data, d: V, m: Map<&2, V>, key: String, x: V, found: Maybe<&2, String>) -> Type:
267 match found:
268 case None{}:
269 Unit
270 case Some{stored}:
271 @equal: {key == stored : String} -> {lookup(V, d, Map.put(&2, V, m, key, x), key) == x : V}
272
273law certificate_left:
274 for -V: Data
275 for +d: V
276 for +lo: Map<&2, V>
277 for +hi: Map<&2, V>
278 for +p: Nat
279 for +key: String
280 for +x: V
281 for found: Maybe<&2, String>
282 for e: {Map.bit(key, p) == (key, False{}) : String & Bool}
283 for cp: replacement_certificate(V, d, lo, key, x, found)
284 replacement_certificate(V, d, MNode{p, lo, hi}, key, x, found)
285def certificate_left(V, d, lo, hi, p, key, x, found, e, cp):
286 match found:
287 case None{}:
288 Unit{}
289 case Some{stored}:
290 equal => Equal.trans(V, lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key), lookup(V, d, Map.put(&2, V, lo, key, x), key), x, replace_left(V, d, lo, hi, p, key, x, e), cp(equal))
291
292law certificate_right:
293 for -V: Data
294 for +d: V
295 for +lo: Map<&2, V>
296 for +hi: Map<&2, V>
297 for +p: Nat
298 for +key: String
299 for +x: V
300 for found: Maybe<&2, String>
301 for e: {Map.bit(key, p) == (key, True{}) : String & Bool}
302 for cp: replacement_certificate(V, d, hi, key, x, found)
303 replacement_certificate(V, d, MNode{p, lo, hi}, key, x, found)
304def certificate_right(V, d, lo, hi, p, key, x, found, e, cp):
305 match found:
306 case None{}:
307 Unit{}
308 case Some{stored}:
309 equal => Equal.trans(V, lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key), lookup(V, d, Map.put(&2, V, hi, key, x), key), x, replace_right(V, d, lo, hi, p, key, x, e), cp(equal))
310
311law certificate_branch:
312 for -V: Data
313 for d: V
314 for +lo: Map<&2, V>
315 for +hi: Map<&2, V>
316 for +p: Nat
317 for +key: String
318 for x: V
319 for bit: Bool
320 for +e: {Map.bit(key, p) == (key, bit) : String & Bool}
321 for lp: replacement_certificate(V, d, lo, key, x, seek_found(V, Map.seek(&2, V, lo, key)))
322 for hp: replacement_certificate(V, d, hi, key, x, seek_found(V, Map.seek(&2, V, hi, key)))
323 replacement_certificate(V, d, MNode{p, lo, hi}, key, x, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)))
324def certificate_branch(V, d, lo, hi, p, key, x, bit, e, lp, hp):
325 match bit:
326 case False{}:
327 %Equal.sym(Maybe<&2, String>, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), seek_found(V, Map.seek(&2, V, lo, key)), seek_left(V, lo, hi, p, key, e)) : replacement_certificate(V, d, MNode{p, lo, hi}, key, x, _)
328 certificate_left(V, d, lo, hi, p, key, x, seek_found(V, Map.seek(&2, V, lo, key)), e, lp)
329 case True{}:
330 %Equal.sym(Maybe<&2, String>, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), seek_found(V, Map.seek(&2, V, hi, key)), seek_right(V, lo, hi, p, key, e)) : replacement_certificate(V, d, MNode{p, lo, hi}, key, x, _)
331 certificate_right(V, d, lo, hi, p, key, x, seek_found(V, Map.seek(&2, V, hi, key)), e, hp)
332
333law replacement_at_seek:
334 for -V: Data
335 for +d: V
336 for m: Map<&2, V>
337 for +key: String
338 for +x: V
339 replacement_certificate(V, d, m, key, x, seek_found(V, Map.seek(&2, V, m, key)))
340def replacement_at_seek(V, d, m, key, x):
341 match m:
342 case MTip{}:
343 Unit{}
344 case MLeaf{stored, old}:
345 equal =>
346 %equal : {lookup(V, d, MLeaf{_, x}, key) == x : V}
347 leaf_same(V, d, key, x)
348 case MNode{+p, +lo, +hi}:
349 certificate_branch(V, d, lo, hi, p, key, x, route_bit(Map.bit(key, p)), route_shape(key, p), replacement_at_seek(V, d, lo, key, x), replacement_at_seek(V, d, hi, key, x))
350
351law seek_low_shape:
352 for -V: Data
353 for p: Nat
354 for lo: Map<&2, V>
355 for hi: Map<&2, V>
356 for key: String
357 for r: Map<&2, V> & String & Maybe<&2, String>
358 for e: {r == (lo, key, seek_found(V, r)) : Map<&2, V> & String & Maybe<&2, String>}
359 {Map.lo(&2, V, String & Maybe<&2, String>, p, hi, r) == (MNode{p, lo, hi}, key, seek_found(V, Map.lo(&2, V, String & Maybe<&2, String>, p, hi, r))) : Map<&2, V> & String & Maybe<&2, String>}
360def seek_low_shape(V, p, lo, hi, key, r, e):
361 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, r, (lo, key, seek_found(V, r)), e) : {Map.lo(&2, V, String & Maybe<&2, String>, p, hi, _) == (MNode{p, lo, hi}, key, seek_found(V, Map.lo(&2, V, String & Maybe<&2, String>, p, hi, _))) : Map<&2, V> & String & Maybe<&2, String>}
362 {==}
363
364law seek_high_shape:
365 for -V: Data
366 for p: Nat
367 for lo: Map<&2, V>
368 for hi: Map<&2, V>
369 for key: String
370 for r: Map<&2, V> & String & Maybe<&2, String>
371 for e: {r == (hi, key, seek_found(V, r)) : Map<&2, V> & String & Maybe<&2, String>}
372 {Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r) == (MNode{p, lo, hi}, key, seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r))) : Map<&2, V> & String & Maybe<&2, String>}
373def seek_high_shape(V, p, lo, hi, key, r, e):
374 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, r, (hi, key, seek_found(V, r)), e) : {Map.hi(&2, V, String & Maybe<&2, String>, p, lo, _) == (MNode{p, lo, hi}, key, seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, _))) : Map<&2, V> & String & Maybe<&2, String>}
375 {==}
376
377law seek_branch_shape:
378 for -V: Data
379 for +lo: Map<&2, V>
380 for +hi: Map<&2, V>
381 for +p: Nat
382 for +key: String
383 for +bit: Bool
384 for e: {Map.bit(key, p) == (key, bit) : String & Bool}
385 for lp: {Map.seek(&2, V, lo, key) == (lo, key, seek_found(V, Map.seek(&2, V, lo, key))) : Map<&2, V> & String & Maybe<&2, String>}
386 for hp: {Map.seek(&2, V, hi, key) == (hi, key, seek_found(V, Map.seek(&2, V, hi, key))) : Map<&2, V> & String & Maybe<&2, String>}
387 {Map.seek(&2, V, MNode{p, lo, hi}, key) == (MNode{p, lo, hi}, key, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))) : Map<&2, V> & String & Maybe<&2, String>}
388def seek_branch_shape(V, lo, hi, p, key, bit, e, lp, hp):
389 match bit:
390 case False{}:
391 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {_ == (MNode{p, lo, hi}, key, seek_found(V, _)) : Map<&2, V> & String & Maybe<&2, String>}
392 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {MB.seek_bit(&2, V, lo, hi, p, _) == (MNode{p, lo, hi}, key, seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _))) : Map<&2, V> & String & Maybe<&2, String>}
393 seek_low_shape(V, p, lo, hi, key, Map.seek(&2, V, lo, key), lp)
394 case True{}:
395 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {_ == (MNode{p, lo, hi}, key, seek_found(V, _)) : Map<&2, V> & String & Maybe<&2, String>}
396 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {MB.seek_bit(&2, V, lo, hi, p, _) == (MNode{p, lo, hi}, key, seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _))) : Map<&2, V> & String & Maybe<&2, String>}
397 seek_high_shape(V, p, lo, hi, key, Map.seek(&2, V, hi, key), hp)
398
399law seek_shape:
400 for -V: Data
401 for m: Map<&2, V>
402 for +key: String
403 {Map.seek(&2, V, m, key) == (m, key, seek_found(V, Map.seek(&2, V, m, key))) : Map<&2, V> & String & Maybe<&2, String>}
404def seek_shape(V, m, key):
405 match m:
406 case MTip{}:
407 {==}
408 case MLeaf{k, v}:
409 {==}
410 case MNode{+p, +lo, +hi}:
411 seek_branch_shape(V, lo, hi, p, key, route_bit(Map.bit(key, p)), route_shape(key, p), seek_shape(V, lo, key), seek_shape(V, hi, key))
412
413law set_comparison_case:
414 for -V: Data
415 for +d: V
416 for m: Map<&2, V>
417 for +key: String
418 for +stored: String
419 for x: V
420 for c: Cmp
421 for e: {N.comparison_tag(String, String.cmp(key, stored)) == c : Cmp}
422 for cp: @equal: {key == stored : String} -> {lookup(V, d, Map.put(&2, V, m, key, x), key) == x : V}
423 {lookup(V, d, Map.set.fin.go(&2, V, m, key, x, ((key, stored), c)), key) == x : V}
424def set_comparison_case(V, d, m, key, stored, x, c, e, cp):
425 match c:
426 case LT{}:
427 insertion_same(V, d, m, key, x, Map.diff(key, stored))
428 case GT{}:
429 insertion_same(V, d, m, key, x, Map.diff(key, stored))
430 case EQ{}:
431 cp(N.string_equal_from_comparison(key, stored, e))
432
433law set_found_case:
434 for -V: Data
435 for d: V
436 for m: Map<&2, V>
437 for +key: String
438 for +stored: String
439 for x: V
440 for cp: @equal: {key == stored : String} -> {lookup(V, d, Map.put(&2, V, m, key, x), key) == x : V}
441 {lookup(V, d, Map.set.fin(&2, V, m, key, x, key, stored), key) == x : V}
442def set_found_case(V, d, m, key, stored, x, cp):
443 %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), N.comparison_tag(String, String.cmp(key, stored))), N.string_comparison_shape(key, stored)) : {lookup(V, d, Map.set.fin.go(&2, V, m, key, x, _), key) == x : V}
444 set_comparison_case(V, d, m, key, stored, x, N.comparison_tag(String, String.cmp(key, stored)), {==}, cp)
445
446law set_seek_case:
447 for -V: Data
448 for d: V
449 for m: Map<&2, V>
450 for key: String
451 for x: V
452 for found: Maybe<&2, String>
453 for cp: replacement_certificate(V, d, m, key, x, found)
454 {lookup(V, d, Map.set.go(&2, V, x, (m, key, found)), key) == x : V}
455def set_seek_case(V, d, m, key, x, found, cp):
456 match found:
457 case None{}:
458 leaf_same(V, d, key, x)
459 case Some{stored}:
460 set_found_case(V, d, m, key, stored, x, cp)
461
462# Public native Map update/lookup same-key law. All seek/routing/comparator
463# premises are discharged above against Base; no valid-tree premise is needed
464# for this particular property. Other-key preservation remains a separate law.
465law set_same:
466 for -V: Data
467 for +d: V
468 for +m: Map<&2, V>
469 for +key: String
470 for +x: V
471 {lookup(V, d, Map.set(&2, V, m, key, x), key) == x : V}
472def set_same(V, d, m, key, x):
473 %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, m, key), (m, key, seek_found(V, Map.seek(&2, V, m, key))), seek_shape(V, m, key)) : {lookup(V, d, Map.set.go(&2, V, x, _), key) == x : V}
474 set_seek_case(V, d, m, key, x, seek_found(V, Map.seek(&2, V, m, key)), replacement_at_seek(V, d, m, key, x))