proofs/lib/array.bend
bend-collections-laws-containers@1.0.0.0 · 347 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/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8
9# Functional correctness of the installed Base.Array get/swap/set/new
10# algorithms (base.bend 2142-2272), proved against their actual definitions.
11#
12# Arrays are linear, so every statement is about thaw(t): the array built from a
13# Data mirror tree t of identical shape. This keeps arrays out of live proof
14# terms. The meaning of a tree is its in-order slot list; indices are U32 below
15# the Base size 2^d (d < 32), so Base index masking is the identity.
16
17type Tree<-T: Data> is Data:
18 TLeaf{value: T}
19 TNode{lo: Tree<T>, hi: Tree<T>}
20
21def thaw(-T: Data, t: Tree<T>) -> Array<T>:
22 match t:
23 case TLeaf{x}:
24 ALeaf{x}
25 case TNode{l, r}:
26 ANode{thaw(T, l), thaw(T, r)}
27
28def freeze(-T: Data, a: Array<T>) -> Tree<T>:
29 match a:
30 case ALeaf{+x}:
31 TLeaf{x}
32 case ANode{xs, ys}:
33 TNode{freeze(T, xs), freeze(T, ys)}
34
35def slots(-T: Data, t: Tree<T>) -> List<&2, T>:
36 match t:
37 case TLeaf{x}:
38 Con{x, Nil{}}
39 case TNode{l, r}:
40 SC.append(T, slots(T, l), slots(T, r))
41
42def perfect(-T: Data, +d: Nat, t: Tree<T>) -> Bool:
43 match d t:
44 case 0n TLeaf{x}:
45 True{}
46 case 0n TNode{l, r}:
47 False{}
48 case 1n+p TLeaf{x}:
49 False{}
50 case 1n+p TNode{l, r}:
51 Bool.and(perfect(T, p, l), perfect(T, p, r))
52
53# Mirror of an update at a Nat index (proof-level description of the new tree).
54# `left` is this node's branch decision (see ndec); passing it as a parameter
55# avoids matching on a computed value.
56def ndec(d: Nat, +j: Nat) -> Bool:
57 match d:
58 case 0n:
59 False{}
60 case 1n+q:
61 Nat.is_lt(j, SC.pow2(q))
62
63def tupd(-T: Data, d: Nat, t: Tree<T>, +j: Nat, +v: T, left: Bool) -> Tree<T>:
64 match d t left:
65 case 0n TLeaf{x} _:
66 TLeaf{v}
67 case 0n TNode{l, r} _:
68 TNode{l, r}
69 case 1n+p TLeaf{x} _:
70 TLeaf{x}
71 case 1n+ +p TNode{l, r} True{}:
72 TNode{tupd(T, p, l, j, v, ndec(p, j)), r}
73 case 1n+ +p TNode{l, r} False{}:
74 TNode{l, tupd(T, p, r, Nat.sub(j, SC.pow2(p)), v, ndec(p, Nat.sub(j, SC.pow2(p))))}
75
76def upd(-T: Data, +d: Nat, t: Tree<T>, +j: Nat, +v: T) -> Tree<T>:
77 tupd(T, d, t, j, v, ndec(d, j))
78
79def trep(-T: Data, +d: Nat, +v: T) -> Tree<T>:
80 match d:
81 case 0n:
82 TLeaf{v}
83 case 1n+p:
84 TNode{trep(T, p, v), trep(T, p, v)}
85
86# ---- pure tree facts ----
87
88def freeze_thaw(-T: Data, +t: Tree<T>) -> {freeze(T, thaw(T, t)) == t : Tree<T>}:
89 match t:
90 case TLeaf{x}:
91 {==}
92 case TNode{+l, +r}:
93 %Equal.sym(Tree<T>, freeze(T, thaw(T, l)), l, freeze_thaw(T, l)) : {TNode{_, freeze(T, thaw(T, r))} == TNode{l, r} : Tree<T>}
94 %Equal.sym(Tree<T>, freeze(T, thaw(T, r)), r, freeze_thaw(T, r)) : {TNode{l, _} == TNode{l, r} : Tree<T>}
95 {==}
96
97def pf_left(-T: Data, +p: Nat, +l: Tree<T>, +r: Tree<T>, +pf: {perfect(T, 1n+p, TNode{l, r}) == True{} : Bool}) -> {perfect(T, p, l) == True{} : Bool}:
98 L.and_left(perfect(T, p, l), perfect(T, p, r), pf)
99
100def pf_right(-T: Data, +p: Nat, +l: Tree<T>, +r: Tree<T>, +pf: {perfect(T, 1n+p, TNode{l, r}) == True{} : Bool}) -> {perfect(T, p, r) == True{} : Bool}:
101 L.and_right(perfect(T, p, l), perfect(T, p, r), pf)
102
103def slots_length(-T: Data, +d: Nat, +t: Tree<T>, +pf: {perfect(T, d, t) == True{} : Bool}) -> {SC.length(T, slots(T, t)) == SC.pow2(d) : Nat}:
104 match d t:
105 case 0n TLeaf{x}:
106 {==}
107 case 0n TNode{l, r}:
108 Empty.absurd({SC.length(T, slots(T, TNode{l, r})) == 1n : Nat}, L.false_true(pf))
109 case 1n+p TLeaf{x}:
110 Empty.absurd({1n == Nat.double(SC.pow2(p)) : Nat}, L.false_true(pf))
111 case 1n+ +p TNode{+l, +r}:
112 %Equal.sym(Nat, SC.length(T, SC.append(T, slots(T, l), slots(T, r))), Nat.add(SC.length(T, slots(T, l)), SC.length(T, slots(T, r))), LL.length_append(T, slots(T, l), slots(T, r))) : {_ == Nat.double(SC.pow2(p)) : Nat}
113 %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pf_left(T, p, l, r, pf))) : {Nat.add(_, SC.length(T, slots(T, r))) == Nat.double(SC.pow2(p)) : Nat}
114 %Equal.sym(Nat, SC.length(T, slots(T, r)), SC.pow2(p), slots_length(T, p, r, pf_right(T, p, l, r, pf))) : {Nat.add(SC.pow2(p), _) == Nat.double(SC.pow2(p)) : Nat}
115 Equal.sym(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p)))
116
117def trep_perfect(-T: Data, +d: Nat, +v: T) -> {perfect(T, d, trep(T, d, v)) == True{} : Bool}:
118 match d:
119 case 0n:
120 {==}
121 case 1n+p:
122 L.and_intro(perfect(T, p, trep(T, p, v)), perfect(T, p, trep(T, p, v)), trep_perfect(T, p, v), trep_perfect(T, p, v))
123
124def trep_slots(-T: Data, +d: Nat, +v: T) -> {slots(T, trep(T, d, v)) == SC.replicate(T, SC.pow2(d), v) : List<&2, T>}:
125 match d:
126 case 0n:
127 {==}
128 case 1n+p:
129 %Equal.sym(List<&2, T>, slots(T, trep(T, p, v)), SC.replicate(T, SC.pow2(p), v), trep_slots(T, p, v)) : {SC.append(T, _, _) == SC.replicate(T, Nat.double(SC.pow2(p)), v) : List<&2, T>}
130 %Equal.sym(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p))) : {SC.append(T, SC.replicate(T, SC.pow2(p), v), SC.replicate(T, SC.pow2(p), v)) == SC.replicate(T, _, v) : List<&2, T>}
131 LL.replicate_add(T, SC.pow2(p), SC.pow2(p), v)
132
133# ---- index helpers ----
134
135def leaf_update(-T: Data, +x: T, +v: T, +j: Nat, +hj: {Nat.is_lt(j, 1n) == True{} : Bool}) -> {Con{v, Nil{}} == SC.update(T, Con{x, Nil{}}, j, v) : List<&2, T>}:
136 match j:
137 case 0n:
138 {==}
139 case 1n+q:
140 Empty.absurd({Con{v, Nil{}} == Con{x, Nil{}} : List<&2, T>}, N.lt_zero_absurd(q, hj))
141
142def leaf_value(-T: Data, +y: T, +j: Nat, +x: T, +hj: {Nat.is_lt(j, 1n) == True{} : Bool}, +hx: {SC.nth(T, Con{y, Nil{}}, j) == Some{x} : Maybe<&2, T>}) -> {y == x : T}:
143 match j:
144 case 0n:
145 L.some_inj(T, y, x, hx)
146 case 1n+q:
147 Empty.absurd({y == x : T}, N.lt_zero_absurd(q, hj))
148
149def len_lt(-T: Data, +p: Nat, +l: Tree<T>, +j: Nat, +pl: {perfect(T, p, l) == True{} : Bool}, +h: {Nat.is_lt(j, SC.pow2(p)) == True{} : Bool}) -> {Nat.is_lt(j, SC.length(T, slots(T, l))) == True{} : Bool}:
150 %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pl)) : {Nat.is_lt(j, _) == True{} : Bool}
151 h
152
153def len_le(-T: Data, +p: Nat, +l: Tree<T>, +j: Nat, +pl: {perfect(T, p, l) == True{} : Bool}, +h: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {Nat.is_le(SC.length(T, slots(T, l)), j) == True{} : Bool}:
154 %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pl)) : {Nat.is_le(_, j) == True{} : Bool}
155 h
156
157def upper_lt(+j: Nat, +p: Nat, +hj: {Nat.is_lt(j, SC.pow2(1n+p)) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(j, SC.pow2(p)), SC.pow2(p)) == True{} : Bool}:
158 N.sub_lt(j, SC.pow2(p), SC.pow2(p), le, L.subst(Nat, n => {Nat.is_lt(j, n) == True{} : Bool}, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p)), hj))
159
160def right_update(-T: Data, +p: Nat, +l: Tree<T>, +r: Tree<T>, +j: Nat, +v: T, +pl: {perfect(T, p, l) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v) == SC.append(T, slots(T, l), SC.update(T, slots(T, r), Nat.sub(j, SC.pow2(p)), v)) : List<&2, T>}:
161 %slots_length(T, p, l, pl) : {SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v) == SC.append(T, slots(T, l), SC.update(T, slots(T, r), Nat.sub(j, _), v)) : List<&2, T>}
162 LL.update_append_right(T, slots(T, l), slots(T, r), j, v, len_le(T, p, l, j, pl, le))
163
164def right_nth(-T: Data, +p: Nat, +l: Tree<T>, +r: Tree<T>, +j: Nat, +pl: {perfect(T, p, l) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), j) == True{} : Bool}) -> {SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j) == SC.nth(T, slots(T, r), Nat.sub(j, SC.pow2(p))) : Maybe<&2, T>}:
165 %slots_length(T, p, l, pl) : {SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), j) == SC.nth(T, slots(T, r), Nat.sub(j, _)) : Maybe<&2, T>}
166 LL.nth_append_right(T, slots(T, l), slots(T, r), j, len_le(T, p, l, j, pl, le))
167
168# ---- the Nat mirror of an update ----
169
170def tupd_perfect(-T: Data, +d: Nat, +t: Tree<T>, +j: Nat, +v: T, +b: Bool, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, tupd(T, d, t, j, v, b)) == True{} : Bool}:
171 match d t b:
172 case 0n TLeaf{x} _:
173 {==}
174 case 0n TNode{l, r} _:
175 pf
176 case 1n+p TLeaf{x} _:
177 pf
178 case 1n+ +p TNode{+l, +r} True{}:
179 L.and_intro(perfect(T, p, tupd(T, p, l, j, v, ndec(p, j))), perfect(T, p, r), tupd_perfect(T, p, l, j, v, ndec(p, j), pf_left(T, p, l, r, pf)), pf_right(T, p, l, r, pf))
180 case 1n+ +p TNode{+l, +r} False{}:
181 L.and_intro(perfect(T, p, l), perfect(T, p, tupd(T, p, r, Nat.sub(j, SC.pow2(p)), v, ndec(p, Nat.sub(j, SC.pow2(p))))), pf_left(T, p, l, r, pf), tupd_perfect(T, p, r, Nat.sub(j, SC.pow2(p)), v, ndec(p, Nat.sub(j, SC.pow2(p))), pf_right(T, p, l, r, pf)))
182
183def tupd_slots(-T: Data, +d: Nat, +t: Tree<T>, +j: Nat, +v: T, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +b: Bool, +eb: {ndec(d, j) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, tupd(T, d, t, j, v, b)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}:
184 match d t b:
185 case 0n TLeaf{x} _:
186 leaf_update(T, x, v, j, hj)
187 case 0n TNode{l, r} _:
188 Empty.absurd({slots(T, TNode{l, r}) == SC.update(T, slots(T, TNode{l, r}), j, v) : List<&2, T>}, L.false_true(pf))
189 case 1n+p TLeaf{x} _:
190 Empty.absurd({Con{x, Nil{}} == SC.update(T, Con{x, Nil{}}, j, v) : List<&2, T>}, L.false_true(pf))
191 case 1n+ +p TNode{+l, +r} True{}:
192 Equal.trans(List<&2, T>, SC.append(T, slots(T, tupd(T, p, l, j, v, ndec(p, j))), slots(T, r)), SC.append(T, SC.update(T, slots(T, l), j, v), slots(T, r)), SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v),
193 Equal.cong(List<&2, T>, List<&2, T>, xs => SC.append(T, xs, slots(T, r)), slots(T, tupd(T, p, l, j, v, ndec(p, j))), SC.update(T, slots(T, l), j, v), tupd_slots(T, p, l, j, v, eb, ndec(p, j), {==}, pf_left(T, p, l, r, pf))),
194 Equal.sym(List<&2, T>, SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), SC.append(T, SC.update(T, slots(T, l), j, v), slots(T, r)), LL.update_append_left(T, slots(T, l), slots(T, r), j, v, len_lt(T, p, l, j, pf_left(T, p, l, r, pf), eb))))
195 case 1n+ +p TNode{+l, +r} False{}:
196 +k = Nat.sub(j, SC.pow2(p))
197 +le = N.not_lt_le(j, SC.pow2(p), eb)
198 Equal.trans(List<&2, T>, SC.append(T, slots(T, l), slots(T, tupd(T, p, r, k, v, ndec(p, k)))), SC.append(T, slots(T, l), SC.update(T, slots(T, r), k, v)), SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v),
199 Equal.cong(List<&2, T>, List<&2, T>, xs => SC.append(T, slots(T, l), xs), slots(T, tupd(T, p, r, k, v, ndec(p, k))), SC.update(T, slots(T, r), k, v), tupd_slots(T, p, r, k, v, upper_lt(j, p, hj, le), ndec(p, k), {==}, pf_right(T, p, l, r, pf))),
200 Equal.sym(List<&2, T>, SC.update(T, SC.append(T, slots(T, l), slots(T, r)), j, v), SC.append(T, slots(T, l), SC.update(T, slots(T, r), k, v)), right_update(T, p, l, r, j, v, pf_left(T, p, l, r, pf), le)))
201
202def upd_perfect(-T: Data, +d: Nat, +t: Tree<T>, +j: Nat, +v: T, +pf: {perfect(T, d, t) == True{} : Bool}) -> {perfect(T, d, upd(T, d, t, j, v)) == True{} : Bool}:
203 tupd_perfect(T, d, t, j, v, ndec(d, j), pf)
204
205def upd_slots(-T: Data, +d: Nat, +t: Tree<T>, +j: Nat, +v: T, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {slots(T, upd(T, d, t, j, v)) == SC.update(T, slots(T, t), j, v) : List<&2, T>}:
206 tupd_slots(T, d, t, j, v, hj, ndec(d, j), {==}, pf)
207
208# ---- U32 index bridges ----
209
210def lt_bridge(+i: U32, +p: Nat, +hp: {Nat.is_lt(p, 32n) == True{} : Bool}, +b: Bool, +eb: {U32.is_lt(i, U.pow2u(p)) == b : Bool}) -> {Nat.is_lt(U32.to_nat(i), SC.pow2(p)) == b : Bool}:
211 Equal.trans(Bool, Nat.is_lt(U32.to_nat(i), SC.pow2(p)), Nat.is_lt(U32.to_nat(i), U32.to_nat(U.pow2u(p))), b,
212 Equal.cong(Nat, Bool, n => Nat.is_lt(U32.to_nat(i), n), SC.pow2(p), U32.to_nat(U.pow2u(p)), Equal.sym(Nat, U32.to_nat(U.pow2u(p)), SC.pow2(p), U.pow2u_value(p, hp))),
213 Equal.trans(Bool, Nat.is_lt(U32.to_nat(i), U32.to_nat(U.pow2u(p))), U32.is_lt(i, U.pow2u(p)), b, Equal.sym(Bool, U32.is_lt(i, U.pow2u(p)), Nat.is_lt(U32.to_nat(i), U32.to_nat(U.pow2u(p))), U.is_lt_nat(i, U.pow2u(p))), eb))
214
215def sub_bridge(+i: U32, +p: Nat, +hp: {Nat.is_lt(p, 32n) == True{} : Bool}, +le: {Nat.is_le(SC.pow2(p), U32.to_nat(i)) == True{} : Bool}) -> {U32.to_nat(U32.sub(i, U.pow2u(p))) == Nat.sub(U32.to_nat(i), SC.pow2(p)) : Nat}:
216 Equal.trans(Nat, U32.to_nat(U32.sub(i, U.pow2u(p))), Nat.sub(U32.to_nat(i), U32.to_nat(U.pow2u(p))), Nat.sub(U32.to_nat(i), SC.pow2(p)),
217 U.sub_nat(i, U.pow2u(p), L.subst(Nat, n => {Nat.is_le(n, U32.to_nat(i)) == True{} : Bool}, SC.pow2(p), U32.to_nat(U.pow2u(p)), Equal.sym(Nat, U32.to_nat(U.pow2u(p)), SC.pow2(p), U.pow2u_value(p, hp)), le)),
218 Equal.cong(Nat, Nat, n => Nat.sub(U32.to_nat(i), n), U32.to_nat(U.pow2u(p)), SC.pow2(p), U.pow2u_value(p, hp)))
219
220# ---- Base.Array.size / get / swap / set / new ----
221
222def size_thaw(-T: Data, +d: Nat, +t: Tree<T>, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.size(T, thaw(T, t)) == (thaw(T, t), U.pow2u(d)) : Array<T> & U32}:
223 match d t:
224 case 0n TLeaf{x}:
225 {==}
226 case 0n TNode{l, r}:
227 Empty.absurd({Array.size(T, thaw(T, TNode{l, r})) == (thaw(T, TNode{l, r}), 1) : Array<T> & U32}, L.false_true(pf))
228 case 1n+p TLeaf{x}:
229 Empty.absurd({Array.size(T, ALeaf{x}) == (ALeaf{x}, U.pow2u(1n+p)) : Array<T> & U32}, L.false_true(pf))
230 case 1n+ +p TNode{+l, +r}:
231 %Equal.sym(Array<T> & U32, Array.size(T, thaw(T, l)), (thaw(T, l), U.pow2u(p)), size_thaw(T, p, l, pf_left(T, p, l, r, pf))) : {Array.size.node(T, thaw(T, r), _) == (ANode{thaw(T, l), thaw(T, r)}, U32.shl(U.pow2u(p))) : Array<T> & U32}
232 {==}
233
234# Base 2.0.32 passes each descent step its branch decision z; eb names it as
235# U32.is_lt(i, U32.shr(2^d)), the value Base computes, so callers pass {==}.
236def get_go(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +b: Bool, +eb: {U32.is_lt(i, U32.shr(U.pow2u(d))) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get.go(T, thaw(T, t), U.pow2u(d), i, b) == (thaw(T, t), x) : Array<T> & T}:
237 match d t b:
238 case 0n TLeaf{+y} _:
239 %leaf_value(T, y, U32.to_nat(i), x, hi, hx) : {(ALeaf{y}, y) == (ALeaf{y}, _) : Array<T> & T}
240 {==}
241 case 0n TNode{l, r} _:
242 Empty.absurd({Array.get.go(T, thaw(T, TNode{l, r}), 1, i, b) == (thaw(T, TNode{l, r}), x) : Array<T> & T}, L.false_true(pf))
243 case 1n+p TLeaf{y} _:
244 Empty.absurd({Array.get.go(T, ALeaf{y}, U.pow2u(1n+p), i, b) == (ALeaf{y}, x) : Array<T> & T}, L.false_true(pf))
245 case 1n+ +p TNode{+l, +r} True{}:
246 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd)
247 +pl = pf_left(T, p, l, r, pf)
248 +hil = lt_bridge(i, p, hp, True{}, L.subst(U32, w => {U32.is_lt(i, w) == True{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb))
249 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.lo(T, thaw(T, r), Array.get.go(T, thaw(T, l), _, i, U32.is_lt(i, U32.shr(_)))) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
250 %Equal.sym(Array<T> & T, Array.get.go(T, thaw(T, l), U.pow2u(p), i, U32.is_lt(i, U32.shr(U.pow2u(p)))), (thaw(T, l), x), get_go(T, p, l, i, x, hp, hil, Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, l), U32.to_nat(i)), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), SC.nth(T, slots(T, l), U32.to_nat(i)), LL.nth_append_left(T, slots(T, l), slots(T, r), U32.to_nat(i), len_lt(T, p, l, U32.to_nat(i), pl, hil))), hx), U32.is_lt(i, U32.shr(U.pow2u(p))), {==}, pl)) : {Array.swap.lo(T, thaw(T, r), _) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
251 {==}
252 case 1n+ +p TNode{+l, +r} False{}:
253 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd)
254 +pl = pf_left(T, p, l, r, pf)
255 +le = N.not_lt_le(U32.to_nat(i), SC.pow2(p), lt_bridge(i, p, hp, False{}, L.subst(U32, w => {U32.is_lt(i, w) == False{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb)))
256 +j = U32.sub(i, U.pow2u(p))
257 +ej = sub_bridge(i, p, hp, le)
258 +hir = L.subst(Nat, n => {Nat.is_lt(n, SC.pow2(p)) == True{} : Bool}, Nat.sub(U32.to_nat(i), SC.pow2(p)), U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), Nat.sub(U32.to_nat(i), SC.pow2(p)), ej), upper_lt(U32.to_nat(i), p, hi, le))
259 +hxr = L.subst(Nat, n => {SC.nth(T, slots(T, r), n) == Some{x} : Maybe<&2, T>}, Nat.sub(U32.to_nat(i), SC.pow2(p)), U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), Nat.sub(U32.to_nat(i), SC.pow2(p)), ej), Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, r), Nat.sub(U32.to_nat(i), SC.pow2(p))), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), SC.nth(T, slots(T, r), Nat.sub(U32.to_nat(i), SC.pow2(p))), right_nth(T, p, l, r, U32.to_nat(i), pl, le)), hx))
260 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.hi(T, thaw(T, l), Array.get.go(T, thaw(T, r), _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
261 %Equal.sym(Array<T> & T, Array.get.go(T, thaw(T, r), U.pow2u(p), j, U32.is_lt(j, U32.shr(U.pow2u(p)))), (thaw(T, r), x), get_go(T, p, r, j, x, hp, hir, hxr, U32.is_lt(j, U32.shr(U.pow2u(p))), {==}, pf_right(T, p, l, r, pf))) : {Array.swap.hi(T, thaw(T, l), _) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
262 {==}
263
264def swap_go(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +b: Bool, +eb: {U32.is_lt(i, U32.shr(U.pow2u(d))) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.swap.go(T, thaw(T, t), U.pow2u(d), i, v, b) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array<T> & T}:
265 match d t b:
266 case 0n TLeaf{+y} _:
267 %leaf_value(T, y, U32.to_nat(i), x, hi, hx) : {(ALeaf{v}, y) == (ALeaf{v}, _) : Array<T> & T}
268 {==}
269 case 0n TNode{l, r} _:
270 Empty.absurd({Array.swap.go(T, thaw(T, TNode{l, r}), 1, i, v, b) == (thaw(T, upd(T, 0n, TNode{l, r}, U32.to_nat(i), v)), x) : Array<T> & T}, L.false_true(pf))
271 case 1n+p TLeaf{y} _:
272 Empty.absurd({Array.swap.go(T, ALeaf{y}, U.pow2u(1n+p), i, v, b) == (thaw(T, upd(T, 1n+p, TLeaf{y}, U32.to_nat(i), v)), x) : Array<T> & T}, L.false_true(pf))
273 case 1n+ +p TNode{+l, +r} True{}:
274 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd)
275 +pl = pf_left(T, p, l, r, pf)
276 +hil = lt_bridge(i, p, hp, True{}, L.subst(U32, w => {U32.is_lt(i, w) == True{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb))
277 +ti = U32.to_nat(i)
278 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.lo(T, thaw(T, r), Array.swap.go(T, thaw(T, l), _, i, v, U32.is_lt(i, U32.shr(_)))) == (thaw(T, upd(T, 1n+p, TNode{l, r}, ti, v)), x) : Array<T> & T}
279 %Equal.sym(Bool, Nat.is_lt(ti, SC.pow2(p)), True{}, hil) : {Array.swap.lo(T, thaw(T, r), Array.swap.go(T, thaw(T, l), U.pow2u(p), i, v, U32.is_lt(i, U32.shr(U.pow2u(p))))) == (thaw(T, tupd(T, 1n+p, TNode{l, r}, ti, v, _)), x) : Array<T> & T}
280 %Equal.sym(Array<T> & T, Array.swap.go(T, thaw(T, l), U.pow2u(p), i, v, U32.is_lt(i, U32.shr(U.pow2u(p)))), (thaw(T, upd(T, p, l, ti, v)), x), swap_go(T, p, l, i, v, x, hp, hil, Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, l), ti), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), SC.nth(T, slots(T, l), ti), LL.nth_append_left(T, slots(T, l), slots(T, r), ti, len_lt(T, p, l, ti, pl, hil))), hx), U32.is_lt(i, U32.shr(U.pow2u(p))), {==}, pl)) : {Array.swap.lo(T, thaw(T, r), _) == (thaw(T, TNode{tupd(T, p, l, ti, v, ndec(p, ti)), r}), x) : Array<T> & T}
281 {==}
282 case 1n+ +p TNode{+l, +r} False{}:
283 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd)
284 +pl = pf_left(T, p, l, r, pf)
285 +ti = U32.to_nat(i)
286 +nb = lt_bridge(i, p, hp, False{}, L.subst(U32, w => {U32.is_lt(i, w) == False{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb))
287 +le = N.not_lt_le(ti, SC.pow2(p), nb)
288 +j = U32.sub(i, U.pow2u(p))
289 +k = Nat.sub(ti, SC.pow2(p))
290 +ej = sub_bridge(i, p, hp, le)
291 +hir = L.subst(Nat, n => {Nat.is_lt(n, SC.pow2(p)) == True{} : Bool}, k, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), k, ej), upper_lt(ti, p, hi, le))
292 +hxr = L.subst(Nat, n => {SC.nth(T, slots(T, r), n) == Some{x} : Maybe<&2, T>}, k, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), k, ej), Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, r), k), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), ti), SC.nth(T, slots(T, r), k), right_nth(T, p, l, r, ti, pl, le)), hx))
293 +ih = swap_go(T, p, r, j, v, x, hp, hir, hxr, U32.is_lt(j, U32.shr(U.pow2u(p))), {==}, pf_right(T, p, l, r, pf))
294 +ih2 = L.subst(Nat, n => {Array.swap.go(T, thaw(T, r), U.pow2u(p), j, v, U32.is_lt(j, U32.shr(U.pow2u(p)))) == (thaw(T, upd(T, p, r, n, v)), x) : Array<T> & T}, U32.to_nat(j), k, ej, ih)
295 %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.hi(T, thaw(T, l), Array.swap.go(T, thaw(T, r), _, U32.sub(i, _), v, U32.is_lt(U32.sub(i, _), U32.shr(_)))) == (thaw(T, upd(T, 1n+p, TNode{l, r}, ti, v)), x) : Array<T> & T}
296 %Equal.sym(Bool, Nat.is_lt(ti, SC.pow2(p)), False{}, nb) : {Array.swap.hi(T, thaw(T, l), Array.swap.go(T, thaw(T, r), U.pow2u(p), j, v, U32.is_lt(j, U32.shr(U.pow2u(p))))) == (thaw(T, tupd(T, 1n+p, TNode{l, r}, ti, v, _)), x) : Array<T> & T}
297 %Equal.sym(Array<T> & T, Array.swap.go(T, thaw(T, r), U.pow2u(p), j, v, U32.is_lt(j, U32.shr(U.pow2u(p)))), (thaw(T, upd(T, p, r, k, v)), x), ih2) : {Array.swap.hi(T, thaw(T, l), _) == (thaw(T, TNode{l, tupd(T, p, r, k, v, ndec(p, k))}), x) : Array<T> & T}
298 {==}
299
300# Public Base entry points. Premises: the tree is perfect of depth d < 32 and
301# the index is below 2^d; x is the value currently stored at that index.
302def get(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, thaw(T, t), i) == (thaw(T, t), x) : Array<T> & T}:
303 %Equal.sym(Array<T> & U32, Array.size(T, thaw(T, t)), (thaw(T, t), U.pow2u(d)), size_thaw(T, d, t, pf)) : {Array.get.at(T, i, _) == (thaw(T, t), x) : Array<T> & T}
304 %Equal.sym(U32, U32.and(i, U32.sub(U.pow2u(d), 1)), i, U.mask_pow2u(i, d, hd, hi)) : {Array.get.go(T, thaw(T, t), U.pow2u(d), _, U32.is_lt(_, U32.shr(U.pow2u(d)))) == (thaw(T, t), x) : Array<T> & T}
305 get_go(T, d, t, i, x, hd, hi, hx, U32.is_lt(i, U32.shr(U.pow2u(d))), {==}, pf)
306
307def swap(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.swap(T, thaw(T, t), i, v) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array<T> & T}:
308 %Equal.sym(Array<T> & U32, Array.size(T, thaw(T, t)), (thaw(T, t), U.pow2u(d)), size_thaw(T, d, t, pf)) : {Array.swap.at(T, i, v, _) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array<T> & T}
309 %Equal.sym(U32, U32.and(i, U32.sub(U.pow2u(d), 1)), i, U.mask_pow2u(i, d, hd, hi)) : {Array.swap.go(T, thaw(T, t), U.pow2u(d), _, v, U32.is_lt(_, U32.shr(U.pow2u(d)))) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x) : Array<T> & T}
310 swap_go(T, d, t, i, v, x, hd, hi, hx, U32.is_lt(i, U32.shr(U.pow2u(d))), {==}, pf)
311
312def set(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.set(T, thaw(T, t), i, v) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array<T>}:
313 %Equal.sym(Array<T> & T, Array.swap(T, thaw(T, t), i, v), (thaw(T, upd(T, d, t, U32.to_nat(i), v)), x), swap(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.set.fin(T, _) == thaw(T, upd(T, d, t, U32.to_nat(i), v)) : Array<T>}
314 {==}
315
316def new(-T: Data, +d: Nat, +v: T) -> {Array.new(T, d, v) == thaw(T, trep(T, d, v)) : Array<T>}:
317 match d:
318 case 0n:
319 {==}
320 case 1n+p:
321 %Equal.sym(Array<T>, Array.new(T, p, v), thaw(T, trep(T, p, v)), new(T, p, v)) : {ANode{_, _} == ANode{thaw(T, trep(T, p, v)), thaw(T, trep(T, p, v))} : Array<T>}
322 {==}
323
324def clone(-T: Data, +t: Tree<T>) -> {Array.clone(T, thaw(T, t)) == (thaw(T, t), thaw(T, t)) : Array<T> & Array<T>}:
325 match t:
326 case TLeaf{x}:
327 {==}
328 case TNode{+l, +r}:
329 %Equal.sym(Array<T> & Array<T>, Array.clone(T, thaw(T, l)), (thaw(T, l), thaw(T, l)), clone(T, l)) : {Array.clone.node(T, _, Array.clone(T, thaw(T, r))) == (ANode{thaw(T, l), thaw(T, r)}, ANode{thaw(T, l), thaw(T, r)}) : Array<T> & Array<T>}
330 %Equal.sym(Array<T> & Array<T>, Array.clone(T, thaw(T, r)), (thaw(T, r), thaw(T, r)), clone(T, r)) : {Array.clone.node(T, (thaw(T, l), thaw(T, l)), _) == (ANode{thaw(T, l), thaw(T, r)}, ANode{thaw(T, l), thaw(T, r)}) : Array<T> & Array<T>}
331 {==}
332
333# ---- get after set (Base.Array.set then Base.Array.get) ----
334
335def get_set_same(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +v: T, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, Array.set(T, thaw(T, t), i, v), i) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), v) : Array<T> & T}:
336 +t2 = upd(T, d, t, U32.to_nat(i), v)
337 %Equal.sym(Array<T>, Array.set(T, thaw(T, t), i, v), thaw(T, t2), set(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.get(T, _, i) == (thaw(T, t2), v) : Array<T> & T}
338 get(T, d, t2, i, v, hd, hi,
339 L.subst(List<&2, T>, ys => {SC.nth(T, ys, U32.to_nat(i)) == Some{v} : Maybe<&2, T>}, SC.update(T, slots(T, t), U32.to_nat(i), v), slots(T, t2), Equal.sym(List<&2, T>, slots(T, t2), SC.update(T, slots(T, t), U32.to_nat(i), v), upd_slots(T, d, t, U32.to_nat(i), v, hi, pf)), LL.nth_update_same(T, slots(T, t), U32.to_nat(i), v, LL.nth_lt_length(T, slots(T, t), U32.to_nat(i), x, hx))),
340 upd_perfect(T, d, t, U32.to_nat(i), v, pf))
341
342def get_set_other(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +j: U32, +v: T, +x: T, +y: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hj: {Nat.is_lt(U32.to_nat(j), SC.pow2(d)) == True{} : Bool}, +ne: {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == False{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +hy: {SC.nth(T, slots(T, t), U32.to_nat(j)) == Some{y} : Maybe<&2, T>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, Array.set(T, thaw(T, t), i, v), j) == (thaw(T, upd(T, d, t, U32.to_nat(i), v)), y) : Array<T> & T}:
343 +t2 = upd(T, d, t, U32.to_nat(i), v)
344 %Equal.sym(Array<T>, Array.set(T, thaw(T, t), i, v), thaw(T, t2), set(T, d, t, i, v, x, hd, hi, hx, pf)) : {Array.get(T, _, j) == (thaw(T, t2), y) : Array<T> & T}
345 get(T, d, t2, j, y, hd, hj,
346 L.subst(List<&2, T>, ys => {SC.nth(T, ys, U32.to_nat(j)) == Some{y} : Maybe<&2, T>}, SC.update(T, slots(T, t), U32.to_nat(i), v), slots(T, t2), Equal.sym(List<&2, T>, slots(T, t2), SC.update(T, slots(T, t), U32.to_nat(i), v), upd_slots(T, d, t, U32.to_nat(i), v, hi, pf)), Equal.trans(Maybe<&2, T>, SC.nth(T, SC.update(T, slots(T, t), U32.to_nat(i), v), U32.to_nat(j)), SC.nth(T, slots(T, t), U32.to_nat(j)), Some{y}, LL.nth_update_other(T, slots(T, t), U32.to_nat(i), U32.to_nat(j), v, ne), hy)),
347 upd_perfect(T, d, t, U32.to_nat(i), v, pf))