proof_shift.bend

lawful-bytes@0.1.1.0 · 516 lines · 25 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-bytes@0.1.1.0/proof_seq.bend as Q
5import lawful-bytes@0.1.1.0/proof_core.bend as C
6import lawful-bytes@0.1.1.0/proof_ops.bend as O
7import lawful-bytes@0.1.1.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)