proofs/lib/lemmas/proofs/map_delete_prefix.bend
bend-collections-laws-containers@1.0.0.0 · 126 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/string_compare.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as I
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as R
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
7
8# Deletion preserves every existing query/prefix constraint.
9# This law unfolds native pop, including collapsing an empty child.
10law conjunction:
11 for a: Bool
12 for b: Bool
13 for left: {a == True{} : Bool}
14 for right: {b == True{} : Bool}
15 {a && b == True{} : Bool}
16def conjunction(a, b, left, right):
17 %Equal.sym(Bool, a, True{}, left) : {_ && b == True{} : Bool}
18 right
19
20law low:
21 for -V: Data
22 for p: Nat
23 for +hi: Map<&2, V>
24 for r: Map<&2, V> & Maybe<&2, V>
25 for +query: String
26 for +limit: Nat
27 for left: {Inv.prefix_against(V, query, Map.del.fin(&2, V, r), limit) == True{} : Bool}
28 for right: {Inv.prefix_against(V, query, hi, limit) == True{} : Bool}
29 {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.lo(&2, V, p, hi, r)), limit) == True{} : Bool}
30def low(V, p, hi, r, query, limit, left, right):
31 match r:
32 case Tuple{tree, found}:
33 match tree:
34 case MTip{}:
35 right
36 case MLeaf{+k, +v}:
37 conjunction(Inv.same_prefix(query, k, limit), Inv.prefix_against(V, query, hi, limit), left, right)
38 case MNode{+q, +lo, +other}:
39 conjunction(Inv.prefix_against(V, query, MNode{q, lo, other}, limit), Inv.prefix_against(V, query, hi, limit), left, right)
40
41law high:
42 for -V: Data
43 for p: Nat
44 for +lo: Map<&2, V>
45 for r: Map<&2, V> & Maybe<&2, V>
46 for +query: String
47 for +limit: Nat
48 for left: {Inv.prefix_against(V, query, lo, limit) == True{} : Bool}
49 for right: {Inv.prefix_against(V, query, Map.del.fin(&2, V, r), limit) == True{} : Bool}
50 {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.hi(&2, V, p, lo, r)), limit) == True{} : Bool}
51def high(V, p, lo, r, query, limit, left, right):
52 match r:
53 case Tuple{tree, found}:
54 match tree:
55 case MTip{}:
56 left
57 case MLeaf{+k, +v}:
58 conjunction(Inv.prefix_against(V, query, lo, limit), Inv.same_prefix(query, k, limit), left, right)
59 case MNode{+q, +other, +hi}:
60 conjunction(Inv.prefix_against(V, query, lo, limit), Inv.prefix_against(V, query, MNode{q, other, hi}, limit), left, right)
61
62law leaf:
63 for -V: Data
64 for value: V
65 for key: String
66 for stored: String
67 for c: Cmp
68 for query: String
69 for limit: Nat
70 for route: {Inv.same_prefix(query, stored, limit) == True{} : Bool}
71 {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, ((key, stored), c))), limit) == True{} : Bool}
72def leaf(V, value, key, stored, c, query, limit, route):
73 match c:
74 case LT{}:
75 route
76 case EQ{}:
77 {==}
78 case GT{}:
79 route
80
81law branch:
82 for -V: Data
83 for +lo: Map<&2, V>
84 for +hi: Map<&2, V>
85 for +p: Nat
86 for +key: String
87 for bit: Bool
88 for e: {Map.bit(key, p) == (key, bit) : String & Bool}
89 for +query: String
90 for +limit: Nat
91 for left: {Inv.prefix_against(V, query, lo, limit) == True{} : Bool}
92 for right: {Inv.prefix_against(V, query, hi, limit) == True{} : Bool}
93 for lp: {Inv.prefix_against(V, query, lo, limit) == True{} : Bool} -> {Inv.prefix_against(V, query, Map.del(&2, V, lo, key), limit) == True{} : Bool}
94 for hp: {Inv.prefix_against(V, query, hi, limit) == True{} : Bool} -> {Inv.prefix_against(V, query, Map.del(&2, V, hi, key), limit) == True{} : Bool}
95 {Inv.prefix_against(V, query, Map.del(&2, V, MNode{p, lo, hi}, key), limit) == True{} : Bool}
96def branch(V, lo, hi, p, key, bit, e, query, limit, left, right, lp, hp):
97 match bit:
98 case False{}:
99 %Equal.sym(Map<&2, V> & Maybe<&2, V>, Map.pop(&2, V, MNode{p, lo, hi}, key), MB.pop_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, V, p, lo, hi, key)) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, _), limit) == True{} : Bool}
100 %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), limit) == True{} : Bool}
101 low(V, p, hi, Map.pop(&2, V, lo, key), query, limit, lp(left), right)
102 case True{}:
103 %Equal.sym(Map<&2, V> & Maybe<&2, V>, Map.pop(&2, V, MNode{p, lo, hi}, key), MB.pop_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.pop_node(&2, V, p, lo, hi, key)) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, _), limit) == True{} : Bool}
104 %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, MB.pop_bit(&2, V, lo, hi, p, _)), limit) == True{} : Bool}
105 high(V, p, lo, Map.pop(&2, V, hi, key), query, limit, left, hp(right))
106
107law preserves_prefix_against:
108 for -V: Data
109 for tree: Map<&2, V>
110 for +key: String
111 for +query: String
112 for +limit: Nat
113 for +routes: {Inv.prefix_against(V, query, tree, limit) == True{} : Bool}
114 {Inv.prefix_against(V, query, Map.del(&2, V, tree, key), limit) == True{} : Bool}
115def preserves_prefix_against(V, tree, key, query, limit, routes):
116 match tree:
117 case MTip{}:
118 {==}
119 case MLeaf{+stored, +value}:
120 %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)) : {Inv.prefix_against(V, query, Map.del.fin(&2, V, Map.pop.leaf(&2, V, value, _)), limit) == True{} : Bool}
121 leaf(V, value, key, stored, N.comparison_tag(String, String.cmp(key, stored)), query, limit, routes)
122 case MNode{+p, +lo, +hi}:
123 left = R.and_left(Inv.prefix_against(V, query, lo, limit), Inv.prefix_against(V, query, hi, limit), routes)
124 right = R.and_right(Inv.prefix_against(V, query, lo, limit), Inv.prefix_against(V, query, hi, limit), routes)
125 branch(V, lo, hi, p, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), query, limit, left, right, r => preserves_prefix_against(V, lo, key, query, limit, r), r => preserves_prefix_against(V, hi, key, query, limit, r))
126