proof_shift.bend
lawful-bytes@0.1.0.0 · 516 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-bytes@0.1.0.0/bytes.bend as B
4import lawful-bytes@0.1.0.0/proof_seq.bend as Q
5import lawful-bytes@0.1.0.0/proof_core.bend as C
6import lawful-bytes@0.1.0.0/proof_ops.bend as O
7import lawful-bytes@0.1.0.0/proof_append.bend as X
8import lawful-words@0.1.0.0/defs.bend as W
9import lawful-words@0.1.0.0/proof_nat.bend as N
10import lawful-words@0.1.0.0/proof_u32.bend as U
11import lawful-words@0.1.0.0/proof_bytes.bend as Y
12import lawful-arrays@0.1.0.0/proof_base.bend as AB
13import lawful-arrays@0.1.0.0/proof_tree.bend as P
14import lawful-arrays@0.1.0.0/proof_index.bend as I
15
16# shift on the mirror. The loop reads byte p = j + k and writes it at j; it
17# keeps len. SGT computes the tree the loop leaves (shift_go_eq), and the view
18# invariant (sv) is stated on SGT, a Data function, so no Bytes is involved.
19
20# Lists
21# =====
22
23law get_drop:
24 for +xs: List<&2, U32>
25 for +a: Nat
26 for +b: Nat
27 {List.get(&2, U32, List.drop(&2, U32, xs, a), b) == List.get(&2, U32, xs, Nat.add(a, b)) : Maybe<&2, U32>}
28
29def get_drop(xs, a, b):
30 match xs a:
31 case Nil{} _:
32 {==}
33 case Con{x, t} 0n:
34 {==}
35 case Con{x, t} 1n+p:
36 get_drop(t, p, b)
37
38law drop_length:
39 for +xs: List<&2, U32>
40 for +k: Nat
41 {List.length(&2, U32, List.drop(&2, U32, xs, k)) == Nat.sub(List.length(&2, U32, xs), k) : Nat}
42
43def drop_length(xs, k):
44 match xs k:
45 case Nil{} _:
46 {==}
47 case Con{x, t} 0n:
48 {==}
49 case Con{x, t} 1n+p:
50 drop_length(t, p)
51
52# Setting the first element of drop(xs, j).
53law drop_set0:
54 for +xs: List<&2, U32>
55 for +j: Nat
56 for +x: U32
57 for +h: {Nat.is_lt(j, List.length(&2, U32, xs)) == True{} : Bool}
58 {List.set(&2, U32, List.drop(&2, U32, xs, j), 0n, x) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}
59
60def drop_set0(xs, j, x, h):
61 match xs j:
62 case Nil{} _:
63 Empty.absurd({List.set(&2, U32, Nil{}, 0n, x) == x <> Nil{} : List<&2, U32>}, AB.lt_zero_absurd(j, h))
64 case Con{y, t} 0n:
65 %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, X.drop_zero(t)) : {x <> t == x <> _ : List<&2, U32>}
66 {==}
67 case Con{y, t} 1n+p:
68 drop_set0(t, p, x, h)
69
70law take_snoc:
71 for +ys: List<&2, U32>
72 for +j: Nat
73 for +x: U32
74 for +h: {List.get(&2, U32, ys, j) == Some{x} : Maybe<&2, U32>}
75 {List.take(&2, U32, ys, Nat.add(j, 1n)) == List.append(&2, U32, List.take(&2, U32, ys, j), [x]) : List<&2, U32>}
76
77def take_snoc(ys, j, x, h):
78 match ys j:
79 case Nil{} _:
80 Empty.absurd({Nil{} == List.append(&2, U32, Nil{}, [x]) : List<&2, U32>}, X.none_some(x, h))
81 case Con{+y, t} 0n:
82 %X.some_inj(y, x, h) : {y <> List.take(&2, U32, t, 0n) == [_] : List<&2, U32>}
83 %Equal.sym(List<&2, U32>, List.take(&2, U32, t, 0n), Nil{}, Q.take_zero(t)) : {y <> _ == [y] : List<&2, U32>}
84 {==}
85 case Con{+y, t} 1n+p:
86 %take_snoc(t, p, x, h) : {y <> List.take(&2, U32, t, Nat.add(p, 1n)) == y <> _ : List<&2, U32>}
87 {==}
88
89law take_all:
90 for +ys: List<&2, U32>
91 for +n: Nat
92 for +h: {Nat.is_le(List.length(&2, U32, ys), n) == True{} : Bool}
93 {List.take(&2, U32, ys, n) == ys : List<&2, U32>}
94
95def take_all(ys, n, h):
96 match ys n:
97 case Nil{} _:
98 {==}
99 case Con{y, t} 0n:
100 Empty.absurd({Nil{} == y <> t : List<&2, U32>}, AB.false_ne_true(h))
101 case Con{+y, t} 1n+p:
102 %take_all(t, p, h) : {y <> List.take(&2, U32, t, p) == y <> _ : List<&2, U32>}
103 {==}
104
105law sub_self:
106 for +j: Nat
107 {Nat.sub(j, j) == 0n : Nat}
108
109def sub_self(j):
110 match j:
111 case 0n:
112 {==}
113 case 1n+p:
114 sub_self(p)
115
116# The loop as a tree
117# ==================
118
119def SGT(+len: U32, m: Nat, +tb: P.Tree<U32>, +j: U32, +p: U32, +k: U32) -> P.Tree<U32>:
120 match m:
121 case 0n:
122 tb
123 case 1n+n:
124 +x = C.AT(len, tb, p)
125 +j1 = (j + 1 : U32)
126 SGT(len, n, I.set_tree(U32, tb, (j >> 2n : U32), W.put_byte(C.WD(tb, (j >> 2n : U32)), U32.to_nat((j .&. 3 : U32)), x)), j1, (j1 + k : U32), k)
127
128law shift_go_eq:
129 for +m: Nat
130 for +len: U32
131 for +tb: P.Tree<U32>
132 for +j: U32
133 for +p: U32
134 for +k: U32
135 {B.shift.go(m, B.at(C.BT(len, tb), p), j, k) == C.BT(len, SGT(len, m, tb, j, p, k)) : D.Bytes}
136
137def shift_go_eq(m, len, tb, j, p, k):
138 match m:
139 case 0n:
140 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, tb), p), (C.BT(len, tb), C.AT(len, tb, p)), C.at_pair_t(len, tb, p)) :
141 {B.shift.go(0n, _, j, k) == C.BT(len, tb) : D.Bytes}
142 {==}
143 case 1n+n:
144 +x = C.AT(len, tb, p)
145 +j1 = (j + 1 : U32)
146 +tb1 = I.set_tree(U32, tb, (j >> 2n : U32), W.put_byte(C.WD(tb, (j >> 2n : U32)), U32.to_nat((j .&. 3 : U32)), x))
147 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, tb), p), (C.BT(len, tb), x), C.at_pair_t(len, tb, p)) :
148 {B.shift.go(1n+n, _, j, k) == C.BT(len, SGT(len, 1n+n, tb, j, p, k)) : D.Bytes}
149 %Equal.sym(D.Bytes, B.set(C.BT(len, tb), j, x), C.BT(len, tb1), O.set_eq_t(len, tb, j, x)) :
150 {B.shift.go(n, B.at(_, (j1 + k : U32)), j1, k) == C.BT(len, SGT(len, n, tb1, j1, (j1 + k : U32), k)) : D.Bytes}
151 shift_go_eq(n, len, tb1, j1, (j1 + k : U32), k)
152
153law sgt_ok:
154 for +m: Nat
155 for +len: U32
156 for +tb: P.Tree<U32>
157 for +d: Nat
158 for +j: U32
159 for +p: U32
160 for +k: U32
161 for +hb: {D.ok(C.BT(len, tb), d) == True{} : Bool}
162 {D.ok(C.BT(len, SGT(len, m, tb, j, p, k)), d) == True{} : Bool}
163
164def sgt_ok(m, len, tb, d, j, p, k, hb):
165 match m:
166 case 0n:
167 hb
168 case 1n+n:
169 +x = C.AT(len, tb, p)
170 +j1 = (j + 1 : U32)
171 +tb1 = I.set_tree(U32, tb, (j >> 2n : U32), W.put_byte(C.WD(tb, (j >> 2n : U32)), U32.to_nat((j .&. 3 : U32)), x))
172 sgt_ok(n, len, tb1, d, j1, (j1 + k : U32), k,
173 AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.set(C.BT(len, tb), j, x), C.BT(len, tb1), O.set_eq_t(len, tb, j, x),
174 O.set_ok_t(len, tb, d, j, x, hb)))
175
176# The view invariant
177# ==================
178
179# Bytes j onwards are still those of xs; bytes below j are xs from k on.
180def SV(+xs: List<&2, U32>, +kk: Nat, +jj: Nat) -> List<&2, U32>:
181 List.append(&2, U32, List.take(&2, U32, List.drop(&2, U32, xs, kk), jj), List.drop(&2, U32, xs, jj))
182
183# Nat facts for one step: j + k + (1 + n) = L.
184law sv_lt:
185 for +jj: Nat
186 for +kk: Nat
187 for +n: Nat
188 for +ll: Nat
189 for +hm: {Nat.add(Nat.add(jj, kk), 1n+n) == ll : Nat}
190 {Nat.is_lt(Nat.add(jj, kk), ll) == True{} : Bool}
191
192def sv_lt(jj, kk, n, ll, hm):
193 X.le_split(Nat.add(jj, kk), n, ll,
194 AB.subst(Nat, y => {Nat.is_le(Nat.add(Nat.add(jj, kk), 1n+n), y) == True{} : Bool}, Nat.add(Nat.add(jj, kk), 1n+n), ll, hm,
195 N.le_refl(Nat.add(Nat.add(jj, kk), 1n+n))))
196
197law sv_lt_j:
198 for +jj: Nat
199 for +kk: Nat
200 for +n: Nat
201 for +ll: Nat
202 for +hm: {Nat.add(Nat.add(jj, kk), 1n+n) == ll : Nat}
203 {Nat.is_lt(jj, ll) == True{} : Bool}
204
205def sv_lt_j(jj, kk, n, ll, hm):
206 N.le_lt_trans(jj, Nat.add(jj, kk), ll, N.le_add_r(jj, kk), sv_lt(jj, kk, n, ll, hm))
207
208law sv_m:
209 for +jj: Nat
210 for +kk: Nat
211 for +n: Nat
212 {Nat.add(Nat.add(Nat.add(jj, 1n), kk), n) == Nat.add(Nat.add(jj, kk), 1n+n) : Nat}
213
214def sv_m(jj, kk, n):
215 %Equal.sym(Nat, Nat.add(Nat.add(jj, 1n), kk), Nat.add(jj, 1n+kk), N.add_assoc(jj, 1n, kk)) :
216 {Nat.add(_, n) == Nat.add(Nat.add(jj, kk), 1n+n) : Nat}
217 %Equal.sym(Nat, Nat.add(jj, 1n+kk), 1n+Nat.add(jj, kk), N.add_succ(jj, kk)) :
218 {Nat.add(_, n) == Nat.add(Nat.add(jj, kk), 1n+n) : Nat}
219 %Equal.sym(Nat, Nat.add(Nat.add(jj, kk), 1n+n), 1n+Nat.add(Nat.add(jj, kk), n), N.add_succ(Nat.add(jj, kk), n)) :
220 {1n+Nat.add(Nat.add(jj, kk), n) == _ : Nat}
221 {==}
222
223law sv_jk1:
224 for +jj: Nat
225 for +kk: Nat
226 for +ll: Nat
227 for +h: {Nat.is_lt(Nat.add(jj, kk), ll) == True{} : Bool}
228 {Nat.is_le(Nat.add(Nat.add(jj, 1n), kk), ll) == True{} : Bool}
229
230def sv_jk1(jj, kk, ll, h):
231 %Equal.sym(Nat, Nat.add(Nat.add(jj, 1n), kk), Nat.add(jj, 1n+kk), N.add_assoc(jj, 1n, kk)) : {Nat.is_le(_, ll) == True{} : Bool}
232 %Equal.sym(Nat, Nat.add(jj, 1n+kk), 1n+Nat.add(jj, kk), N.add_succ(jj, kk)) : {Nat.is_le(_, ll) == True{} : Bool}
233 Equal.trans(Bool, Nat.is_le(1n+Nat.add(jj, kk), ll), Nat.is_lt(Nat.add(jj, kk), ll), True{}, N.le_succ_lt(Nat.add(jj, kk), ll), h)
234
235# The final view: SV at j = L - k.
236def SF(+xs: List<&2, U32>, +kk: Nat, +ll: Nat) -> List<&2, U32>:
237 SV(xs, kk, Nat.sub(ll, kk))
238
239# The value read at p = j + k is element j of drop(xs, k).
240law sv_read:
241 for +xs: List<&2, U32>
242 for +jj: Nat
243 for +kk: Nat
244 for +hj: {Nat.is_le(jj, List.length(&2, U32, List.drop(&2, U32, xs, kk))) == True{} : Bool}
245 {List.get(&2, U32, SV(xs, kk, jj), Nat.add(jj, kk)) == List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) : Maybe<&2, U32>}
246
247def sv_read(xs, jj, kk, hj):
248 +A = List.take(&2, U32, List.drop(&2, U32, xs, kk), jj)
249 +la = Q.take_length(List.drop(&2, U32, xs, kk), jj, hj)
250 +hn = AB.subst(Nat, y => {Nat.is_lt(Nat.add(jj, kk), y) == False{} : Bool}, jj, List.length(&2, U32, A),
251 Equal.sym(Nat, List.length(&2, U32, A), jj, la), N.le_not_lt(jj, Nat.add(jj, kk), N.le_add_r(jj, kk)))
252 %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, List.append(&2, U32, A, List.drop(&2, U32, xs, jj)), Nat.add(jj, kk)),
253 List.get(&2, U32, List.drop(&2, U32, xs, jj), Nat.sub(Nat.add(jj, kk), List.length(&2, U32, A))),
254 AB.get_append_r(U32, A, List.drop(&2, U32, xs, jj), Nat.add(jj, kk), hn)) :
255 {_ == List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) : Maybe<&2, U32>}
256 %Equal.sym(Nat, List.length(&2, U32, A), jj, la) :
257 {List.get(&2, U32, List.drop(&2, U32, xs, jj), Nat.sub(Nat.add(jj, kk), _)) == List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) : Maybe<&2, U32>}
258 %Equal.sym(Nat, Nat.sub(Nat.add(jj, kk), jj), kk, N.sub_add_l(jj, kk)) :
259 {List.get(&2, U32, List.drop(&2, U32, xs, jj), _) == List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) : Maybe<&2, U32>}
260 %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, xs, jj), kk), List.get(&2, U32, xs, Nat.add(jj, kk)), get_drop(xs, jj, kk)) :
261 {_ == List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) : Maybe<&2, U32>}
262 %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, xs, kk), jj), List.get(&2, U32, xs, Nat.add(kk, jj)), get_drop(xs, kk, jj)) :
263 {List.get(&2, U32, xs, Nat.add(jj, kk)) == _ : Maybe<&2, U32>}
264 %N.add_comm(jj, kk) : {List.get(&2, U32, xs, Nat.add(jj, kk)) == List.get(&2, U32, xs, _) : Maybe<&2, U32>}
265 {==}
266
267# Writing that value at j moves the boundary to j + 1.
268law sv_write:
269 for +xs: List<&2, U32>
270 for +jj: Nat
271 for +kk: Nat
272 for +x: U32
273 for +hj: {Nat.is_le(jj, List.length(&2, U32, List.drop(&2, U32, xs, kk))) == True{} : Bool}
274 for +hjl: {Nat.is_lt(jj, List.length(&2, U32, xs)) == True{} : Bool}
275 for +hx: {List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) == Some{x} : Maybe<&2, U32>}
276 {List.set(&2, U32, SV(xs, kk, jj), jj, x) == SV(xs, kk, Nat.add(jj, 1n)) : List<&2, U32>}
277
278def sv_write(xs, jj, kk, x, hj, hjl, hx):
279 +A = List.take(&2, U32, List.drop(&2, U32, xs, kk), jj)
280 +la = Q.take_length(List.drop(&2, U32, xs, kk), jj, hj)
281 +RHS = SV(xs, kk, Nat.add(jj, 1n))
282 +hn = AB.subst(Nat, y => {Nat.is_lt(jj, y) == False{} : Bool}, jj, List.length(&2, U32, A),
283 Equal.sym(Nat, List.length(&2, U32, A), jj, la), N.lt_irrefl(jj))
284 %Equal.sym(List<&2, U32>, List.set(&2, U32, List.append(&2, U32, A, List.drop(&2, U32, xs, jj)), jj, x),
285 List.append(&2, U32, A, List.set(&2, U32, List.drop(&2, U32, xs, jj), Nat.sub(jj, List.length(&2, U32, A)), x)),
286 AB.set_append_r(U32, A, List.drop(&2, U32, xs, jj), jj, x, hn)) :
287 {_ == RHS : List<&2, U32>}
288 %Equal.sym(Nat, List.length(&2, U32, A), jj, la) :
289 {List.append(&2, U32, A, List.set(&2, U32, List.drop(&2, U32, xs, jj), Nat.sub(jj, _), x)) == RHS : List<&2, U32>}
290 %Equal.sym(Nat, Nat.sub(jj, jj), 0n, sub_self(jj)) :
291 {List.append(&2, U32, A, List.set(&2, U32, List.drop(&2, U32, xs, jj), _, x)) == RHS : List<&2, U32>}
292 %Equal.sym(List<&2, U32>, List.set(&2, U32, List.drop(&2, U32, xs, jj), 0n, x), x <> List.drop(&2, U32, xs, Nat.add(jj, 1n)),
293 drop_set0(xs, jj, x, hjl)) :
294 {List.append(&2, U32, A, _) == RHS : List<&2, U32>}
295 %Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, xs, kk), Nat.add(jj, 1n)), List.append(&2, U32, A, [x]),
296 take_snoc(List.drop(&2, U32, xs, kk), jj, x, hx)) :
297 {List.append(&2, U32, A, x <> List.drop(&2, U32, xs, Nat.add(jj, 1n))) == List.append(&2, U32, _, List.drop(&2, U32, xs, Nat.add(jj, 1n))) : List<&2, U32>}
298 Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, A, [x]), List.drop(&2, U32, xs, Nat.add(jj, 1n))),
299 List.append(&2, U32, A, List.append(&2, U32, [x], List.drop(&2, U32, xs, Nat.add(jj, 1n)))),
300 X.append_assoc(A, [x], List.drop(&2, U32, xs, Nat.add(jj, 1n))))
301
302law sub_le:
303 for +a: Nat
304 for +b: Nat
305 {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}
306
307def sub_le(a, b):
308 match a b:
309 case 0n _:
310 {==}
311 case 1n+p 0n:
312 N.le_refl(1n+p)
313 case 1n+p 1n+q:
314 N.le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), N.lt_to_le(p, 1n+p,
315 Equal.trans(Bool, Nat.is_lt(p, 1n+p), Nat.is_le(p, p), True{}, N.lt_succ_iff(p, p), N.le_refl(p))))
316
317# drop(xs, k) has L - k elements.
318law xl:
319 for +len: U32
320 for +t: P.Tree<U32>
321 for +d: Nat
322 for +kk: Nat
323 for +h0: {D.ok(C.BT(len, t), d) == True{} : Bool}
324 {List.length(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), kk)) == Nat.sub(U32.to_nat(len), kk) : Nat}
325
326def xl(len, t, d, kk, h0):
327 %Equal.sym(Nat, List.length(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), kk)), Nat.sub(List.length(&2, U32, D.view(C.BT(len, t))), kk),
328 drop_length(D.view(C.BT(len, t)), kk)) :
329 {_ == Nat.sub(U32.to_nat(len), kk) : Nat}
330 %Equal.sym(Nat, List.length(&2, U32, D.view(C.BT(len, t))), U32.to_nat(len), O.view_size_t(len, t, d, h0)) :
331 {Nat.sub(_, kk) == Nat.sub(U32.to_nat(len), kk) : Nat}
332 {==}
333
334# j <= L - k from j + k < L.
335law sv_jd:
336 for +len: U32
337 for +t: P.Tree<U32>
338 for +d: Nat
339 for +jj: Nat
340 for +kk: Nat
341 for +h0: {D.ok(C.BT(len, t), d) == True{} : Bool}
342 for +hlt: {Nat.is_lt(Nat.add(jj, kk), U32.to_nat(len)) == True{} : Bool}
343 {Nat.is_le(jj, List.length(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), kk))) == True{} : Bool}
344
345def sv_jd(len, t, d, jj, kk, h0, hlt):
346 %Equal.sym(Nat, List.length(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), kk)), Nat.sub(U32.to_nat(len), kk), xl(len, t, d, kk, h0)) :
347 {Nat.is_le(jj, _) == True{} : Bool}
348 N.le_sub_r(kk, jj, U32.to_nat(len),
349 AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, Nat.add(jj, kk), Nat.add(kk, jj), N.add_comm(jj, kk),
350 N.lt_to_le(Nat.add(jj, kk), U32.to_nat(len), hlt)))
351
352# The byte read at p is element j of drop(xs, k).
353law sv_x:
354 for +len: U32
355 for +t: P.Tree<U32>
356 for +d: Nat
357 for +k: U32
358 for +tb: P.Tree<U32>
359 for +j: U32
360 for +p: U32
361 for +h0: {D.ok(C.BT(len, t), d) == True{} : Bool}
362 for +hb: {D.ok(C.BT(len, tb), d) == True{} : Bool}
363 for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(j), U32.to_nat(k)) : Nat}
364 for +hv: {D.view(C.BT(len, tb)) == SV(D.view(C.BT(len, t)), U32.to_nat(k), U32.to_nat(j)) : List<&2, U32>}
365 for +hlt: {Nat.is_lt(Nat.add(U32.to_nat(j), U32.to_nat(k)), U32.to_nat(len)) == True{} : Bool}
366 {List.get(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), U32.to_nat(k)), U32.to_nat(j)) == Some{C.AT(len, tb, p)} : Maybe<&2, U32>}
367
368def sv_x(len, t, d, k, tb, j, p, h0, hb, hp, hv, hlt):
369 +xs = D.view(C.BT(len, t))
370 +JJ = U32.to_nat(j)
371 +KK = U32.to_nat(k)
372 +hi = AB.subst(Nat, y => {Nat.is_lt(y, U32.to_nat(len)) == True{} : Bool}, Nat.add(JJ, KK), U32.to_nat(p),
373 Equal.sym(Nat, U32.to_nat(p), Nat.add(JJ, KK), hp), hlt)
374 +a1 = C.at_view_t(len, tb, d, p, C.ok_full(len, tb, d, hb), C.ok_d(len, tb, d, hb), C.ok_len(len, tb, d, hb), hi)
375 %sv_read(xs, JJ, KK, sv_jd(len, t, d, JJ, KK, h0, hlt)) :
376 {_ == Some{C.AT(len, tb, p)} : Maybe<&2, U32>}
377 %hp : {List.get(&2, U32, SV(xs, KK, JJ), _) == Some{C.AT(len, tb, p)} : Maybe<&2, U32>}
378 %hv : {List.get(&2, U32, _, U32.to_nat(p)) == Some{C.AT(len, tb, p)} : Maybe<&2, U32>}
379 Equal.sym(Maybe<&2, U32>, Some{C.AT(len, tb, p)}, List.get(&2, U32, D.view(C.BT(len, tb)), U32.to_nat(p)), a1)
380
381law sv:
382 for +m: Nat
383 for +len: U32
384 for +t: P.Tree<U32>
385 for +d: Nat
386 for +k: U32
387 for +tb: P.Tree<U32>
388 for +j: U32
389 for +p: U32
390 for +h0: {D.ok(C.BT(len, t), d) == True{} : Bool}
391 for +hb: {D.ok(C.BT(len, tb), d) == True{} : Bool}
392 for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(j), U32.to_nat(k)) : Nat}
393 for +hm: {Nat.add(Nat.add(U32.to_nat(j), U32.to_nat(k)), m) == U32.to_nat(len) : Nat}
394 for +hv: {D.view(C.BT(len, tb)) == SV(D.view(C.BT(len, t)), U32.to_nat(k), U32.to_nat(j)) : List<&2, U32>}
395 {D.view(C.BT(len, SGT(len, m, tb, j, p, k))) == SF(D.view(C.BT(len, t)), U32.to_nat(k), U32.to_nat(len)) : List<&2, U32>}
396
397def sv(m, len, t, d, k, tb, j, p, h0, hb, hp, hm, hv):
398 match m:
399 case 0n:
400 +xs = D.view(C.BT(len, t))
401 +JJ = U32.to_nat(j)
402 +KK = U32.to_nat(k)
403 +eL = Equal.trans(Nat, Nat.add(JJ, KK), Nat.add(Nat.add(JJ, KK), 0n), U32.to_nat(len),
404 Equal.sym(Nat, Nat.add(Nat.add(JJ, KK), 0n), Nat.add(JJ, KK), N.add_zero(Nat.add(JJ, KK))), hm)
405 %Equal.sym(List<&2, U32>, D.view(C.BT(len, tb)), SV(xs, KK, JJ), hv) : {_ == SF(xs, KK, U32.to_nat(len)) : List<&2, U32>}
406 %eL : {SV(xs, KK, JJ) == SV(xs, KK, Nat.sub(_, KK)) : List<&2, U32>}
407 %Equal.sym(Nat, Nat.sub(Nat.add(JJ, KK), KK), JJ, N.sub_add(JJ, KK)) : {SV(xs, KK, JJ) == SV(xs, KK, _) : List<&2, U32>}
408 {==}
409 case 1n+n:
410 +xs = D.view(C.BT(len, t))
411 +JJ = U32.to_nat(j)
412 +KK = U32.to_nat(k)
413 +LL = U32.to_nat(len)
414 +x = C.AT(len, tb, p)
415 +j1 = (j + 1 : U32)
416 +tb1 = I.set_tree(U32, tb, (j >> 2n : U32), W.put_byte(C.WD(tb, (j >> 2n : U32)), U32.to_nat((j .&. 3 : U32)), x))
417 +M = Nat.mul(4n, Nat.pow(2n, d))
418 +hd = C.ok_d(len, t, d, h0)
419 +hL = C.ok_len(len, t, d, h0)
420 +hlt = sv_lt(JJ, KK, n, LL, hm)
421 +hltj = sv_lt_j(JJ, KK, n, LL, hm)
422 +ej1 = C.inc_fits(j, d, hd, N.lt_le_trans(JJ, LL, M, hltj, hL))
423 +hj1 = AB.subst(Nat, y => {Nat.is_le(Nat.add(y, KK), LL) == True{} : Bool}, Nat.add(JJ, 1n), U32.to_nat(j1),
424 Equal.sym(Nat, U32.to_nat(j1), Nat.add(JJ, 1n), ej1), sv_jk1(JJ, KK, LL, hlt))
425 +hp1 = C.add_fits(j1, k, d, hd, N.le_trans(Nat.add(U32.to_nat(j1), KK), LL, M, hj1, hL))
426 +hm1 = AB.subst(Nat, y => {Nat.add(Nat.add(y, KK), n) == LL : Nat}, Nat.add(JJ, 1n), U32.to_nat(j1),
427 Equal.sym(Nat, U32.to_nat(j1), Nat.add(JJ, 1n), ej1),
428 Equal.trans(Nat, Nat.add(Nat.add(Nat.add(JJ, 1n), KK), n), Nat.add(Nat.add(JJ, KK), 1n+n), LL, sv_m(JJ, KK, n), hm))
429 +hb1 = AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.set(C.BT(len, tb), j, x), C.BT(len, tb1), O.set_eq_t(len, tb, j, x),
430 O.set_ok_t(len, tb, d, j, x, hb))
431 +hx = sv_x(len, t, d, k, tb, j, p, h0, hb, hp, hv, hlt)
432 +hx256 = AB.subst(U32, y => {U32.is_lt(y, 256) == True{} : Bool}, W.byte(C.WD(tb, (p >> 2n : U32)), U32.to_nat((p .&. 3 : U32))), x,
433 Equal.sym(U32, x, W.byte(C.WD(tb, (p >> 2n : U32)), U32.to_nat((p .&. 3 : U32))), C.at_val(len, tb, p)),
434 Y.byte_lt(C.WD(tb, (p >> 2n : U32)), U32.to_nat((p .&. 3 : U32))))
435 +pv = AB.subst(D.Bytes, y => {D.view(y) == List.set(&2, U32, D.view(C.BT(len, tb)), JJ, x) : List<&2, U32>},
436 B.set(C.BT(len, tb), j, x), C.BT(len, tb1), O.set_eq_t(len, tb, j, x), O.set_view_t(len, tb, d, j, x, hb, hltj, hx256))
437 +hjl = AB.subst(Nat, y => {Nat.is_lt(JJ, y) == True{} : Bool}, LL, List.length(&2, U32, xs),
438 Equal.sym(Nat, List.length(&2, U32, xs), LL, O.view_size_t(len, t, d, h0)), hltj)
439 +sw = sv_write(xs, JJ, KK, x, sv_jd(len, t, d, JJ, KK, h0, hlt), hjl, hx)
440 +hv1a = Equal.trans(List<&2, U32>, D.view(C.BT(len, tb1)), List.set(&2, U32, D.view(C.BT(len, tb)), JJ, x), SV(xs, KK, Nat.add(JJ, 1n)), pv,
441 AB.subst(List<&2, U32>, y => {List.set(&2, U32, y, JJ, x) == SV(xs, KK, Nat.add(JJ, 1n)) : List<&2, U32>}, SV(xs, KK, JJ), D.view(C.BT(len, tb)),
442 Equal.sym(List<&2, U32>, D.view(C.BT(len, tb)), SV(xs, KK, JJ), hv), sw))
443 +hv1 = AB.subst(Nat, y => {D.view(C.BT(len, tb1)) == SV(xs, KK, y) : List<&2, U32>}, Nat.add(JJ, 1n), U32.to_nat(j1),
444 Equal.sym(Nat, U32.to_nat(j1), Nat.add(JJ, 1n), ej1), hv1a)
445 sv(n, len, t, d, k, tb1, j1, (j1 + k : U32), h0, hb1, hp1, hm1, hv1)
446
447# The laws
448# ========
449
450law sv0:
451 for +xs: List<&2, U32>
452 for +kk: Nat
453 {SV(xs, kk, 0n) == xs : List<&2, U32>}
454
455def sv0(xs, kk):
456 %Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, xs, kk), 0n), Nil{}, Q.take_zero(List.drop(&2, U32, xs, kk))) :
457 {List.append(&2, U32, _, List.drop(&2, U32, xs, 0n)) == xs : List<&2, U32>}
458 X.drop_zero(xs)
459
460law shift_view_t:
461 for +len: U32
462 for +t: P.Tree<U32>
463 for +d: Nat
464 for +k: U32
465 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
466 for +hk: {Nat.is_le(U32.to_nat(k), D.size(C.BT(len, t))) == True{} : Bool}
467 {D.view(B.shift(C.BT(len, t), k)) == List.drop(&2, U32, D.view(C.BT(len, t)), U32.to_nat(k)) : List<&2, U32>}
468
469def shift_view_t(len, t, d, k, h, hk):
470 +xs = D.view(C.BT(len, t))
471 +KK = U32.to_nat(k)
472 +LL = U32.to_nat(len)
473 +N0 = Nat.sub(LL, KK)
474 +T2 = SGT(len, N0, t, 0, k, k)
475 +ys = List.drop(&2, U32, xs, KK)
476 +eN = U.to_nat_sub_le(len, k, Equal.trans(Bool, U32.is_le(k, len), Nat.is_le(KK, LL), True{}, U.is_le_to_nat(k, len), hk))
477 +hle = AB.subst(Nat, y => {Nat.is_le(y, LL) == True{} : Bool}, N0, U32.to_nat((len - k : U32)), Equal.sym(Nat, U32.to_nat((len - k : U32)), N0, eN), sub_le(LL, KK))
478 +hyl = xl(len, t, d, KK, h)
479 +hN0 = AB.subst(Nat, y => {Nat.is_le(N0, y) == True{} : Bool}, N0, List.length(&2, U32, ys), Equal.sym(Nat, List.length(&2, U32, ys), N0, hyl), N.le_refl(N0))
480 %Equal.sym(D.Bytes, B.shift.go(N0, B.at(C.BT(len, t), k), 0, k), C.BT(len, T2), shift_go_eq(N0, len, t, 0, k, k)) :
481 {D.view(B.truncate(_, (len - k : U32))) == ys : List<&2, U32>}
482 %Equal.sym(List<&2, U32>, D.view(B.truncate(C.BT(len, T2), (len - k : U32))), List.take(&2, U32, D.view(C.BT(len, T2)), U32.to_nat((len - k : U32))),
483 O.truncate_view_t(len, T2, (len - k : U32), hle)) :
484 {_ == ys : List<&2, U32>}
485 %Equal.sym(Nat, U32.to_nat((len - k : U32)), N0, eN) : {List.take(&2, U32, D.view(C.BT(len, T2)), _) == ys : List<&2, U32>}
486 %Equal.sym(List<&2, U32>, D.view(C.BT(len, T2)), SF(xs, KK, LL),
487 sv(N0, len, t, d, k, t, 0, k, h, h, {==}, N.le_sub_add(KK, LL, hk), Equal.sym(List<&2, U32>, SV(xs, KK, 0n), xs, sv0(xs, KK)))) :
488 {List.take(&2, U32, _, N0) == ys : List<&2, U32>}
489 +A = List.take(&2, U32, ys, N0)
490 +la = Q.take_length(ys, N0, hN0)
491 %Equal.sym(List<&2, U32>, List.take(&2, U32, List.append(&2, U32, A, List.drop(&2, U32, xs, N0)), N0), List.take(&2, U32, A, N0),
492 Q.take_append_l(A, List.drop(&2, U32, xs, N0), N0,
493 AB.subst(Nat, y => {Nat.is_le(N0, y) == True{} : Bool}, N0, List.length(&2, U32, A), Equal.sym(Nat, List.length(&2, U32, A), N0, la), N.le_refl(N0)))) :
494 {_ == ys : List<&2, U32>}
495 %Equal.sym(List<&2, U32>, List.take(&2, U32, A, N0), A, Q.take_take(ys, N0, N0, N.le_refl(N0))) : {_ == ys : List<&2, U32>}
496 take_all(ys, N0, AB.subst(Nat, y => {Nat.is_le(y, N0) == True{} : Bool}, N0, List.length(&2, U32, ys), Equal.sym(Nat, List.length(&2, U32, ys), N0, hyl), N.le_refl(N0)))
497
498law shift_ok_t:
499 for +len: U32
500 for +t: P.Tree<U32>
501 for +d: Nat
502 for +k: U32
503 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
504 for +hk: {Nat.is_le(U32.to_nat(k), D.size(C.BT(len, t))) == True{} : Bool}
505 {D.ok(B.shift(C.BT(len, t), k), d) == True{} : Bool}
506
507def shift_ok_t(len, t, d, k, h, hk):
508 +KK = U32.to_nat(k)
509 +LL = U32.to_nat(len)
510 +N0 = Nat.sub(LL, KK)
511 +T2 = SGT(len, N0, t, 0, k, k)
512 +eN = U.to_nat_sub_le(len, k, Equal.trans(Bool, U32.is_le(k, len), Nat.is_le(KK, LL), True{}, U.is_le_to_nat(k, len), hk))
513 +hle = AB.subst(Nat, y => {Nat.is_le(y, LL) == True{} : Bool}, N0, U32.to_nat((len - k : U32)), Equal.sym(Nat, U32.to_nat((len - k : U32)), N0, eN), sub_le(LL, KK))
514 %Equal.sym(D.Bytes, B.shift.go(N0, B.at(C.BT(len, t), k), 0, k), C.BT(len, T2), shift_go_eq(N0, len, t, 0, k, k)) :
515 {D.ok(B.truncate(_, (len - k : U32)), d) == True{} : Bool}
516 O.truncate_ok_t(len, T2, d, (len - k : U32), sgt_ok(N0, len, t, d, 0, k, k, h), hle)