1	import Base
2	import ./defs.bend as D
3	import ./bytes.bend as B
4	import ./proof_seq.bend as Q
5	import ./proof_core.bend as C
6	import ./proof_ops.bend as O
7	import ./proof_append.bend as X
8	import lawful-words@0.1.0.0/defs.bend as W
9	import lawful-words@0.1.0.0/proof_nat.bend as N
10	import lawful-words@0.1.0.0/proof_u32.bend as U
11	import lawful-words@0.1.0.0/proof_bytes.bend as Y
12	import lawful-arrays@0.1.0.0/proof_base.bend as AB
13	import lawful-arrays@0.1.0.0/proof_tree.bend as P
14	import 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	
23	law 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	
29	def 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	
38	law 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	
43	def 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).
53	law 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	
60	def 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	
70	law 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	
77	def 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	
89	law 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	
95	def 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	
105	law sub_self:
106	  for +j: Nat
107	  {Nat.sub(j, j) == 0n : Nat}
108	
109	def 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	
119	def 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	
128	law 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	
137	def 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	
153	law 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	
164	def 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.
180	def 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.
184	law 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	
192	def 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	
197	law 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	
205	def 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	
208	law 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	
214	def 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	
223	law 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	
230	def 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.
236	def 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).
240	law 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	
247	def 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.
268	law 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	
278	def 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	
302	law sub_le:
303	  for +a: Nat
304	  for +b: Nat
305	  {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}
306	
307	def 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.
318	law 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	
326	def 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.
335	law 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	
345	def 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).
353	law 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	
368	def 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	
381	law 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	
397	def 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	
450	law sv0:
451	  for +xs: List<&2, U32>
452	  for +kk: Nat
453	  {SV(xs, kk, 0n) == xs : List<&2, U32>}
454	
455	def 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	
460	law 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	
469	def 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	
498	law 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	
507	def 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)