proofs/containers/balanced_search_tree/slot.bend
bend-collections-laws-containers@1.0.0.0 · 183 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/frame.bend as FR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/agree.bend as AG
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
14
15# A list grown by one slot, or rewritten at one: every other position reads
16# as before, the slot reads the new value; so the entries, links and free
17# chain of ids avoiding the slot are unchanged. (source: tools/generators/tm_hand/slot.src)
18
19
20def nth_snoc_other(-X: Data, +xs: List<&2, X>, +x: X, +i: Nat, +dv: X, +h: {Nat.is_eq(i, SC.length(X, xs)) == False{} : Bool}) -> {ST.nth_or(X, SC.snoc(X, xs, x), i, dv) == ST.nth_or(X, xs, i, dv) : X}:
21 match xs i:
22 case Nil{} 0n:
23 Empty.absurd({ST.nth_or(X, SC.snoc(X, Nil{}, x), 0n, dv) == ST.nth_or(X, Nil{}, 0n, dv) : X}, L.true_false(h))
24 case Nil{} 1n+j:
25 {==}
26 case Con{+hd, +t} 0n:
27 {==}
28 case Con{+hd, +t} 1n+j:
29 nth_snoc_other(X, t, x, j, dv, h)
30
31def nth_snoc_same(-X: Data, +xs: List<&2, X>, +x: X, +dv: X) -> {ST.nth_or(X, SC.snoc(X, xs, x), SC.length(X, xs), dv) == x : X}:
32 match xs:
33 case Nil{}:
34 {==}
35 case Con{+hd, +t}:
36 nth_snoc_same(X, t, x, dv)
37
38def nth_upd_c(-X: Data, +xs: List<&2, X>, +i: Nat, +x: X, +j: Nat, +dv: X, +hne: {Nat.is_eq(i, j) == False{} : Bool}, +b: Bool) -> {ST.nth_or(X, ST.pk(List<&2, X>, b, SC.update(X, xs, i, x), xs), j, dv) == ST.nth_or(X, xs, j, dv) : X}:
39 match b:
40 case True{}:
41 %Equal.sym(X, ST.nth_or(X, SC.update(X, xs, i, x), j, dv), PR.or_else(X, SC.nth(X, SC.update(X, xs, i, x), j), dv), PR.nth_or_nth(X, SC.update(X, xs, i, x), j, dv)) : {_ == ST.nth_or(X, xs, j, dv) : X}
42 %Equal.sym(X, ST.nth_or(X, xs, j, dv), PR.or_else(X, SC.nth(X, xs, j), dv), PR.nth_or_nth(X, xs, j, dv)) : {PR.or_else(X, SC.nth(X, SC.update(X, xs, i, x), j), dv) == _ : X}
43 %Equal.sym(Maybe<&2, X>, SC.nth(X, SC.update(X, xs, i, x), j), SC.nth(X, xs, j), LL.nth_update_other(X, xs, i, j, x, hne)) : {PR.or_else(X, _, dv) == PR.or_else(X, SC.nth(X, xs, j), dv) : X}
44 {==}
45 case False{}:
46 {==}
47
48# ---- the node list ----
49
50
51def nd_snoc_other(-K: Data, +nl: List<&2, M.Node<K>>, +x: M.Node<K>, +j: Nat, +h: {Nat.is_eq(j, 1n+SC.length(M.Node<K>, nl)) == False{} : Bool}) -> {ST.nd(K, SC.snoc(M.Node<K>, nl, x), j) == ST.nd(K, nl, j) : M.Node<K>}:
52 match j:
53 case 0n:
54 {==}
55 case 1n+i:
56 nth_snoc_other(M.Node<K>, nl, x, i, M.Free{0n}, h)
57
58def nd_snoc_same(-K: Data, +nl: List<&2, M.Node<K>>, +x: M.Node<K>) -> {ST.nd(K, SC.snoc(M.Node<K>, nl, x), 1n+SC.length(M.Node<K>, nl)) == x : M.Node<K>}:
59 nth_snoc_same(M.Node<K>, nl, x, M.Free{0n})
60
61
62# a new slot agrees off it
63def agr_snoc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +x: M.Node<K>, +hn: {NL.memn(1n+SC.length(M.Node<K>, nl), xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, SC.snoc(M.Node<K>, nl, x)) == True{} : Bool}:
64 match xs:
65 case Nil{}:
66 {==}
67 case Con{+j, +t}:
68 L.and_intro(AG.ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, SC.snoc(M.Node<K>, nl, x), j)), AG.agr(~K, ~cmp, t, nl, SC.snoc(M.Node<K>, nl, x)), AG.ndeq_of_eq(~K, ~cmp, ~o, ST.nd(K, nl, j), ST.nd(K, SC.snoc(M.Node<K>, nl, x), j), Equal.sym(M.Node<K>, ST.nd(K, SC.snoc(M.Node<K>, nl, x), j), ST.nd(K, nl, j), nd_snoc_other(K, nl, x, j, FR.or_f_l(Nat.is_eq(j, 1n+SC.length(M.Node<K>, nl)), NL.memn(1n+SC.length(M.Node<K>, nl), t), hn)))), agr_snoc(~K, ~cmp, ~o, t, nl, x, FR.or_f_r(Nat.is_eq(j, 1n+SC.length(M.Node<K>, nl)), NL.memn(1n+SC.length(M.Node<K>, nl), t), hn)))
69
70# ---- the payload list ----
71
72
73def pv_snoc_other(-V: Data, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>, +j: Nat, +h: {Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)) == False{} : Bool}) -> {ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), j) == ST.pv(V, pl, j) : Maybe<&2, V>}:
74 match j:
75 case 0n:
76 {==}
77 case 1n+i:
78 nth_snoc_other(Maybe<&2, V>, pl, w, i, None{}, h)
79
80def pv_snoc_same(-V: Data, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>) -> {ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), 1n+SC.length(Maybe<&2, V>, pl)) == w : Maybe<&2, V>}:
81 nth_snoc_same(Maybe<&2, V>, pl, w, None{})
82
83def pv_ex_other(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +j: Nat, +hne: {Nat.is_eq(id, j) == False{} : Bool}) -> {ST.pv(V, PR.ex_pl(V, pl, id, w), j) == ST.pv(V, pl, j) : Maybe<&2, V>}:
84 match id j:
85 case 0n +j:
86 {==}
87 case 1n+i 0n:
88 {==}
89 case 1n+i 1n+jj:
90 nth_upd_c(Maybe<&2, V>, pl, i, w, jj, None{}, hne, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)))
91
92def pv_ex_same(-V: Data, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +w: Maybe<&2, V>, +h: {Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)) == True{} : Bool}) -> {ST.pv(V, PR.ex_pl(V, pl, 1n+i, w), 1n+i) == w : Maybe<&2, V>}:
93 %Equal.sym(Bool, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), True{}, h) : {ST.nth_or(Maybe<&2, V>, ST.pk(List<&2, Maybe<&2, V>>, _, SC.update(Maybe<&2, V>, pl, i, w), pl), i, None{}) == w : Maybe<&2, V>}
94 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i, None{}), PR.or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i), None{}), PR.nth_or_nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i, None{})) : {_ == w : Maybe<&2, V>}
95 %Equal.sym(Maybe<&2, Maybe<&2, V>>, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i), Some{w}, LL.nth_update_same(Maybe<&2, V>, pl, i, w, h)) : {PR.or_else(Maybe<&2, V>, _, None{}) == w : Maybe<&2, V>}
96 {==}
97
98
99def ents_psnoc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>, +hn: {NL.memn(1n+SC.length(Maybe<&2, V>, pl), xs) == False{} : Bool}) -> {ST.ents(~K, ~V, xs, nl, SC.snoc(Maybe<&2, V>, pl, w)) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
100 match xs:
101 case Nil{}:
102 {==}
103 case Con{+j, +t}:
104 %Equal.sym(Maybe<&2, V>, ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), j), ST.pv(V, pl, j), pv_snoc_other(V, pl, w, j, FR.or_f_l(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), _), ST.ents(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w))) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
105 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w)), ST.ents(~K, ~V, t, nl, pl), ents_psnoc(~K, ~V, t, nl, pl, w, FR.or_f_r(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
106 {==}
107
108def ents_pex(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, pl, id, w)) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
109 match xs:
110 case Nil{}:
111 {==}
112 case Con{+j, +t}:
113 %Equal.sym(Maybe<&2, V>, ST.pv(V, PR.ex_pl(V, pl, id, w), j), ST.pv(V, pl, j), pv_ex_other(V, pl, id, w, j, FR.ne_sym(j, id, FR.or_f_l(Nat.is_eq(j, id), NL.memn(id, t), hn)))) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), _), ST.ents(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w))) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
114 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w)), ST.ents(~K, ~V, t, nl, pl), ents_pex(~K, ~V, t, nl, pl, id, w, FR.or_f_r(Nat.is_eq(j, id), NL.memn(id, t), hn))) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
115 {==}
116
117
118def oks_psnoc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>, +hn: {NL.memn(1n+SC.length(Maybe<&2, V>, pl), xs) == False{} : Bool}) -> {EN.oks(~K, ~V, xs, nl, SC.snoc(Maybe<&2, V>, pl, w)) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
119 match xs:
120 case Nil{}:
121 {==}
122 case Con{+j, +t}:
123 %Equal.sym(Maybe<&2, V>, ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), j), ST.pv(V, pl, j), pv_snoc_other(V, pl, w, j, FR.or_f_l(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), _)), EN.oks(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w))) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
124 %Equal.sym(Bool, EN.oks(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w)), EN.oks(~K, ~V, t, nl, pl), oks_psnoc(~K, ~V, t, nl, pl, w, FR.or_f_r(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
125 {==}
126
127def oks_pex(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {EN.oks(~K, ~V, xs, nl, PR.ex_pl(V, pl, id, w)) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
128 match xs:
129 case Nil{}:
130 {==}
131 case Con{+j, +t}:
132 %Equal.sym(Maybe<&2, V>, ST.pv(V, PR.ex_pl(V, pl, id, w), j), ST.pv(V, pl, j), pv_ex_other(V, pl, id, w, j, FR.ne_sym(j, id, FR.or_f_l(Nat.is_eq(j, id), NL.memn(id, t), hn)))) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), _)), EN.oks(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w))) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
133 %Equal.sym(Bool, EN.oks(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w)), EN.oks(~K, ~V, t, nl, pl), oks_pex(~K, ~V, t, nl, pl, id, w, FR.or_f_r(Nat.is_eq(j, id), NL.memn(id, t), hn))) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
134 {==}
135
136# ---- values from entries ----
137
138def some_of_ent(-K: Data, -V: Data, +x: M.Node<K>, +m: Maybe<&2, V>, +h: {S.is_some(M.Entry<K, V>, ST.ent(K, V, x, m)) == True{} : Bool}) -> {ST.some2(V, m) == True{} : Bool}:
139 match x m:
140 case M.Free{f} +m:
141 Empty.absurd({ST.some2(V, m) == True{} : Bool}, L.false_true(h))
142 case M.N{c, a, b, q, k} None{}:
143 Empty.absurd({ST.some2(V, None{}) == True{} : Bool}, L.false_true(h))
144 case M.N{c, a, b, q, k} Some{w}:
145 {==}
146
147
148def oks_split_l(~K: Data, ~V: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +h: {EN.oks(~K, ~V, SC.append(Nat, a, b), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, a, nl, pl) == True{} : Bool}:
149 match a:
150 case Nil{}:
151 {==}
152 case Con{+j, +t}:
153 L.and_intro(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, t, nl, pl), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, SC.append(Nat, t, b), nl, pl), h), oks_split_l(~K, ~V, t, b, nl, pl, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, SC.append(Nat, t, b), nl, pl), h)))
154
155def oks_split_r(~K: Data, ~V: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +h: {EN.oks(~K, ~V, SC.append(Nat, a, b), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, b, nl, pl) == True{} : Bool}:
156 match a:
157 case Nil{}:
158 h
159 case Con{+j, +t}:
160 oks_split_r(~K, ~V, t, b, nl, pl, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, SC.append(Nat, t, b), nl, pl), h))
161
162# a tree whose ids all have entries has values
163def pay_oks(~K: Data, ~V: Data, +t: ST.Tr, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +h: {EN.oks(~K, ~V, ST.ids(t), nl, pl) == True{} : Bool}) -> {ST.pay(~V, t, pl) == True{} : Bool}:
164 match t:
165 case ST.TE{}:
166 {==}
167 case ST.TN{+i, +a, +b}:
168 +hr = oks_split_r(~K, ~V, ST.ids(a), Con{i, ST.ids(b)}, nl, pl, h)
169 L.and_intro(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, a, pl), ST.pay(~V, b, pl)), some_of_ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i))), EN.oks(~K, ~V, ST.ids(b), nl, pl), hr)), L.and_intro(ST.pay(~V, a, pl), ST.pay(~V, b, pl), pay_oks(~K, ~V, a, nl, pl, oks_split_l(~K, ~V, ST.ids(a), Con{i, ST.ids(b)}, nl, pl, h)), pay_oks(~K, ~V, b, nl, pl, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i))), EN.oks(~K, ~V, ST.ids(b), nl, pl), hr))))
170
171def len_ex_c(-V: Data, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +w: Maybe<&2, V>, +b: Bool) -> {SC.length(Maybe<&2, V>, ST.pk(List<&2, Maybe<&2, V>>, b, SC.update(Maybe<&2, V>, pl, i, w), pl)) == SC.length(Maybe<&2, V>, pl) : Nat}:
172 match b:
173 case True{}:
174 LL.length_update(Maybe<&2, V>, pl, i, w)
175 case False{}:
176 {==}
177
178def len_ex(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>) -> {SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, id, w)) == SC.length(Maybe<&2, V>, pl) : Nat}:
179 match id:
180 case 0n:
181 {==}
182 case 1n+i:
183 len_ex_c(V, pl, i, w, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)))