1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/crypto/curve25519/field.bend as FS
4	import ../../../src/crypto/curve25519/field.bend as F
5	import ../../lib/nat.bend as N
6	import ../../lib/logic.bend as L
7	import ../../lib/word.bend as WD
8	import ../../lib/arith.bend as AR
9	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
10	import ./num.bend as M
11	import ./limbs.bend as LM
12	
13	# The limb-list polynomial operations of src/crypto/curve25519/field.bend:
14	# addl (limbwise sum), scal (times a limb), conv (the schoolbook product),
15	# take/drop (the split at 2^256) and wide (the fold of the product's high
16	# half). Each keeps its value exactly (Nat, no wrap) under limb bounds whose
17	# sums and products stay below 2^32.
18	
19	def v(+x: U32) -> Nat:
20	  U32.to_nat(x)
21	
22	# ---- lengths ----
23	
24	def len_le(n: Nat, xs: List<&2, U32>) -> Bool:
25	  match n:
26	    case 0n:
27	      match xs:
28	        case Nil{}:
29	          True{}
30	        case Con{x, xt}:
31	          False{}
32	    case 1n+m:
33	      match xs:
34	        case Nil{}:
35	          True{}
36	        case Con{x, xt}:
37	          len_le(m, xt)
38	
39	def len_ge(n: Nat, xs: List<&2, U32>) -> Bool:
40	  match n:
41	    case 0n:
42	      True{}
43	    case 1n+m:
44	      match xs:
45	        case Nil{}:
46	          False{}
47	        case Con{x, xt}:
48	          len_ge(m, xt)
49	
50	def len_le_nil(+n: Nat) -> {len_le(n, Nil{}) == True{} : Bool}:
51	  match n:
52	    case 0n:
53	      {==}
54	    case 1n+m:
55	      {==}
56	
57	def len_le_mono(+k: Nat, +d: Nat, +xs: List<&2, U32>, +e: {len_le(k, xs) == True{} : Bool}) -> {len_le(Nat.add(k, d), xs) == True{} : Bool}:
58	  match k xs:
59	    case 0n Nil{}:
60	      len_le_nil(d)
61	    case 0n Con{y, yt}:
62	      Empty.absurd({len_le(d, Con{y, yt}) == True{} : Bool}, L.false_true(e))
63	    case 1n+m Nil{}:
64	      {==}
65	    case 1n+ +m Con{y, +yt}:
66	      len_le_mono(m, d, yt, e)
67	
68	def okb_len_le(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {len_le(n, xs) == True{} : Bool}:
69	  match n xs:
70	    case 0n Nil{}:
71	      {==}
72	    case 0n Con{y, yt}:
73	      Empty.absurd({len_le(0n, Con{y, yt}) == True{} : Bool}, L.false_true(e))
74	    case 1n+m Nil{}:
75	      {==}
76	    case 1n+ +m Con{+y, +yt}:
77	      okb_len_le(m, yt, b, LM.okb_tail(m, y, yt, b, e))
78	
79	def okb_len_ge(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {len_ge(n, xs) == True{} : Bool}:
80	  match n xs:
81	    case 0n Nil{}:
82	      {==}
83	    case 0n Con{y, yt}:
84	      {==}
85	    case 1n+m Nil{}:
86	      Empty.absurd({len_ge(1n+m, Nil{}) == True{} : Bool}, L.false_true(e))
87	    case 1n+ +m Con{+y, +yt}:
88	      okb_len_ge(m, yt, b, LM.okb_tail(m, y, yt, b, e))
89	
90	def okb_mono(+n: Nat, +xs: List<&2, U32>, +b: Nat, +c: Nat, +hb: {Nat.is_le(b, c) == True{} : Bool}, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {LM.okb(n, xs, c) == True{} : Bool}:
91	  match n xs:
92	    case 0n Nil{}:
93	      {==}
94	    case 0n Con{y, yt}:
95	      Empty.absurd({LM.okb(0n, Con{y, yt}, c) == True{} : Bool}, L.false_true(e))
96	    case 1n+m Nil{}:
97	      Empty.absurd({LM.okb(1n+m, Nil{}, c) == True{} : Bool}, L.false_true(e))
98	    case 1n+ +m Con{+y, +yt}:
99	      L.and_intro(Nat.is_le(v(y), c), LM.okb(m, yt, c), N.le_trans(v(y), b, c, LM.okb_head(m, y, yt, b, e), hb), okb_mono(m, yt, b, c, hb, LM.okb_tail(m, y, yt, b, e)))
100	
101	def le_add_l(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}:
102	  %NA.add_comm(b, a) : {Nat.is_le(b, _) == True{} : Bool}
103	  N.le_add_right(b, a)
104	
105	# ---- addl ----
106	
107	def addl_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {Nat.is_le(v(y), b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:
108	  LM.add_v(one, h1, x, y, N.le_lt_trans(Nat.add(v(x), v(y)), Nat.add(a, b), WD.sc(32n, one), M.le_add2(v(x), v(y), a, b, hx, hy), hab))
109	
110	def addl_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.addl(xs, ys)) == Nat.add(FS.value(xs), FS.value(ys)) : Nat}:
111	  match xs ys:
112	    case Nil{} _:
113	      {==}
114	    case Con{+x, +xt} Nil{}:
115	      Equal.sym(Nat, Nat.add(FS.value(Con{x, xt}), 0n), FS.value(Con{x, xt}), N.add_zero(FS.value(Con{x, xt})))
116	    case Con{+x, +xt} Con{+y, +yt}:
117	      +ev = addl_v(one, h1, x, y, a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy), hab)
118	      +ih = addl_val(one, h1, xt, yt, a, b, LM.lea_tail(x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hab)
119	      +X = FS.value(xt)
120	      +Y = FS.value(yt)
121	      +e1 = M.cong_add(v(U32.add(x, y)), Nat.add(v(x), v(y)), C.shift(8n, FS.value(F.addl(xt, yt))), C.shift(8n, Nat.add(X, Y)), ev, M.cong_sc(8n, FS.value(F.addl(xt, yt)), Nat.add(X, Y), ih))
122	      +e2 = M.cong_r(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y)), Nat.add(C.shift(8n, X), C.shift(8n, Y)), Equal.sym(Nat, Nat.add(C.shift(8n, X), C.shift(8n, Y)), C.shift(8n, Nat.add(X, Y)), M.sc_add(8n, X, Y)))
123	      Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(8n, FS.value(F.addl(xt, yt)))), Nat.add(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(y), C.shift(8n, Y))), e1,
124	        Equal.trans(Nat, Nat.add(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(v(x), v(y)), Nat.add(C.shift(8n, X), C.shift(8n, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(y), C.shift(8n, Y))), e2, M.add4(v(x), v(y), C.shift(8n, X), C.shift(8n, Y))))
125	
126	def addl_lea(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.addl(xs, ys), Nat.add(a, b)) == True{} : Bool}:
127	  match xs ys:
128	    case Nil{} _:
129	      LM.lea_mono(ys, b, Nat.add(a, b), le_add_l(a, b), hy)
130	    case Con{+x, +xt} Nil{}:
131	      LM.lea_mono(Con{x, xt}, a, Nat.add(a, b), N.le_add_right(a, b), hx)
132	    case Con{+x, +xt} Con{+y, +yt}:
133	      +ev = addl_v(one, h1, x, y, a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy), hab)
134	      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.add(a, b)) == True{} : Bool}, Nat.add(v(x), v(y)), v(U32.add(x, y)), Equal.sym(Nat, v(U32.add(x, y)), Nat.add(v(x), v(y)), ev), M.le_add2(v(x), v(y), a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy)))
135	      L.and_intro(Nat.is_le(v(U32.add(x, y)), Nat.add(a, b)), LM.lea(F.addl(xt, yt), Nat.add(a, b)), hd, addl_lea(one, h1, xt, yt, a, b, LM.lea_tail(x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hab))
136	
137	# n limbs and at most n limbs give n limbs
138	def addl_okb(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.okb(n, xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hl: {len_le(n, ys) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.okb(n, F.addl(xs, ys), Nat.add(a, b)) == True{} : Bool}:
139	  match n xs ys:
140	    case 0n Nil{} Nil{}:
141	      {==}
142	    case 0n Nil{} Con{y, yt}:
143	      Empty.absurd({LM.okb(0n, Con{y, yt}, Nat.add(a, b)) == True{} : Bool}, L.false_true(hl))
144	    case 0n Con{x, xt} _:
145	      Empty.absurd({LM.okb(0n, F.addl(Con{x, xt}, ys), Nat.add(a, b)) == True{} : Bool}, L.false_true(hx))
146	    case 1n+m Nil{} _:
147	      Empty.absurd({LM.okb(1n+m, ys, Nat.add(a, b)) == True{} : Bool}, L.false_true(hx))
148	    case 1n+ +m Con{+x, +xt} Nil{}:
149	      okb_mono(1n+m, Con{x, xt}, a, Nat.add(a, b), N.le_add_right(a, b), hx)
150	    case 1n+ +m Con{+x, +xt} Con{+y, +yt}:
151	      +hxh = LM.okb_head(m, x, xt, a, hx)
152	      +hyh = LM.lea_head(y, yt, b, hy)
153	      +ev = addl_v(one, h1, x, y, a, b, hxh, hyh, hab)
154	      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.add(a, b)) == True{} : Bool}, Nat.add(v(x), v(y)), v(U32.add(x, y)), Equal.sym(Nat, v(U32.add(x, y)), Nat.add(v(x), v(y)), ev), M.le_add2(v(x), v(y), a, b, hxh, hyh))
155	      L.and_intro(Nat.is_le(v(U32.add(x, y)), Nat.add(a, b)), LM.okb(m, F.addl(xt, yt), Nat.add(a, b)), hd, addl_okb(one, h1, m, xt, yt, a, b, LM.okb_tail(m, x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hl, hab))
156	
157	def addl_len_ge(+n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +e: {len_ge(n, xs) == True{} : Bool}) -> {len_ge(n, F.addl(xs, ys)) == True{} : Bool}:
158	  match n xs ys:
159	    case 0n _ _:
160	      {==}
161	    case 1n+m Nil{} _:
162	      Empty.absurd({len_ge(1n+m, ys) == True{} : Bool}, L.false_true(e))
163	    case 1n+m Con{x, xt} Nil{}:
164	      e
165	    case 1n+ +m Con{x, +xt} Con{y, +yt}:
166	      addl_len_ge(m, xt, yt, e)
167	
168	def addl_len_le(+n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +ex: {len_le(n, xs) == True{} : Bool}, +ey: {len_le(n, ys) == True{} : Bool}) -> {len_le(n, F.addl(xs, ys)) == True{} : Bool}:
169	  match n xs ys:
170	    case 0n Nil{} _:
171	      ey
172	    case 0n Con{x, xt} _:
173	      Empty.absurd({len_le(0n, F.addl(Con{x, xt}, ys)) == True{} : Bool}, L.false_true(ex))
174	    case 1n+m Nil{} _:
175	      ey
176	    case 1n+m Con{x, xt} Nil{}:
177	      ex
178	    case 1n+ +m Con{x, +xt} Con{y, +yt}:
179	      addl_len_le(m, xt, yt, ex, ey)
180	
181	# ---- scal ----
182	
183	def sc_mul_l(+k: Nat, +a: Nat, +x: Nat) -> {WD.sc(k, Nat.mul(a, x)) == Nat.mul(a, WD.sc(k, x)) : Nat}:
184	  +e1 = M.cong_sc(k, Nat.mul(a, x), Nat.mul(x, a), NA.mul_comm(a, x))
185	  +e2 = AR.sc_mul(k, x, a)
186	  +e3 = NA.mul_comm(WD.sc(k, x), a)
187	  Equal.trans(Nat, WD.sc(k, Nat.mul(a, x)), WD.sc(k, Nat.mul(x, a)), Nat.mul(a, WD.sc(k, x)), e1, Equal.trans(Nat, WD.sc(k, Nat.mul(x, a)), Nat.mul(WD.sc(k, x), a), Nat.mul(a, WD.sc(k, x)), e2, e3))
188	
189	def scal_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {Nat.is_le(v(y), b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}:
190	  LM.mul_v(one, h1, x, y, N.le_lt_trans(Nat.mul(v(x), v(y)), Nat.mul(a, b), WD.sc(32n, one), M.le_mul2(v(x), v(y), a, b, hx, hy), hab))
191	
192	def scal_val(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.scal(x, ys)) == Nat.mul(v(x), FS.value(ys)) : Nat}:
193	  match ys:
194	    case Nil{}:
195	      Equal.sym(Nat, Nat.mul(v(x), 0n), 0n, NA.mul_zero(v(x)))
196	    case Con{+y, +yt}:
197	      +ev = scal_v(one, h1, x, y, a, b, hx, LM.lea_head(y, yt, b, hy), hab)
198	      +ih = scal_val(one, h1, x, yt, a, b, hx, LM.lea_tail(y, yt, b, hy), hab)
199	      +Y = FS.value(yt)
200	      +e1 = M.cong_add(v(U32.mul(x, y)), Nat.mul(v(x), v(y)), C.shift(8n, FS.value(F.scal(x, yt))), C.shift(8n, Nat.mul(v(x), Y)), ev, M.cong_sc(8n, FS.value(F.scal(x, yt)), Nat.mul(v(x), Y), ih))
201	      +e2 = M.cong_r(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y)), Nat.mul(v(x), C.shift(8n, Y)), sc_mul_l(8n, v(x), Y))
202	      +e3 = Equal.sym(Nat, Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), Nat.add(Nat.mul(v(x), v(y)), Nat.mul(v(x), C.shift(8n, Y))), NA.mul_add_left(v(x), v(y), C.shift(8n, Y)))
203	      Equal.trans(Nat, Nat.add(v(U32.mul(x, y)), C.shift(8n, FS.value(F.scal(x, yt)))), Nat.add(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y))), Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), e1,
204	        Equal.trans(Nat, Nat.add(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y))), Nat.add(Nat.mul(v(x), v(y)), Nat.mul(v(x), C.shift(8n, Y))), Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), e2, e3))
205	
206	def scal_lea(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}:
207	  match ys:
208	    case Nil{}:
209	      {==}
210	    case Con{+y, +yt}:
211	      +hyh = LM.lea_head(y, yt, b, hy)
212	      +ev = scal_v(one, h1, x, y, a, b, hx, hyh, hab)
213	      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(v(x), v(y)), v(U32.mul(x, y)), Equal.sym(Nat, v(U32.mul(x, y)), Nat.mul(v(x), v(y)), ev), M.le_mul2(v(x), v(y), a, b, hx, hyh))
214	      L.and_intro(Nat.is_le(v(U32.mul(x, y)), Nat.mul(a, b)), LM.lea(F.scal(x, yt), Nat.mul(a, b)), hd, scal_lea(one, h1, x, yt, a, b, hx, LM.lea_tail(y, yt, b, hy), hab))
215	
216	def scal_okb(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.okb(n, ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.okb(n, F.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}:
217	  match n ys:
218	    case 0n Nil{}:
219	      {==}
220	    case 0n Con{y, yt}:
221	      Empty.absurd({LM.okb(0n, F.scal(x, Con{y, yt}), Nat.mul(a, b)) == True{} : Bool}, L.false_true(hy))
222	    case 1n+m Nil{}:
223	      Empty.absurd({LM.okb(1n+m, Nil{}, Nat.mul(a, b)) == True{} : Bool}, L.false_true(hy))
224	    case 1n+ +m Con{+y, +yt}:
225	      +hyh = LM.okb_head(m, y, yt, b, hy)
226	      +ev = scal_v(one, h1, x, y, a, b, hx, hyh, hab)
227	      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(v(x), v(y)), v(U32.mul(x, y)), Equal.sym(Nat, v(U32.mul(x, y)), Nat.mul(v(x), v(y)), ev), M.le_mul2(v(x), v(y), a, b, hx, hyh))
228	      L.and_intro(Nat.is_le(v(U32.mul(x, y)), Nat.mul(a, b)), LM.okb(m, F.scal(x, yt), Nat.mul(a, b)), hd, scal_okb(one, h1, m, x, yt, a, b, hx, LM.okb_tail(m, y, yt, b, hy), hab))
229	
230	def scal_len_ge(+n: Nat, +x: U32, +ys: List<&2, U32>, +e: {len_ge(n, ys) == True{} : Bool}) -> {len_ge(n, F.scal(x, ys)) == True{} : Bool}:
231	  match n ys:
232	    case 0n _:
233	      {==}
234	    case 1n+m Nil{}:
235	      Empty.absurd({len_ge(1n+m, Nil{}) == True{} : Bool}, L.false_true(e))
236	    case 1n+ +m Con{y, +yt}:
237	      scal_len_ge(m, x, yt, e)
238	
239	def scal_len_le(+n: Nat, +x: U32, +ys: List<&2, U32>, +e: {len_le(n, ys) == True{} : Bool}) -> {len_le(n, F.scal(x, ys)) == True{} : Bool}:
240	  match n ys:
241	    case 0n Nil{}:
242	      {==}
243	    case 0n Con{y, yt}:
244	      Empty.absurd({len_le(0n, F.scal(x, Con{y, yt})) == True{} : Bool}, L.false_true(e))
245	    case 1n+m Nil{}:
246	      {==}
247	    case 1n+ +m Con{y, +yt}:
248	      scal_len_le(m, x, yt, e)
249	
250	# ---- conv ----
251	
252	# len(xs) * k
253	def cb(xs: List<&2, U32>, +k: Nat) -> Nat:
254	  match xs:
255	    case Nil{}:
256	      0n
257	    case Con{x, xt}:
258	      Nat.add(k, cb(xt, k))
259	
260	def cbn(n: Nat, +k: Nat) -> Nat:
261	  match n:
262	    case 0n:
263	      0n
264	    case 1n+m:
265	      Nat.add(k, cbn(m, k))
266	
267	def conv_lea(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hc: {Nat.is_lt(cb(xs, Nat.mul(a, b)), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.conv(xs, ys), cb(xs, Nat.mul(a, b))) == True{} : Bool}:
268	  match xs:
269	    case Nil{}:
270	      {==}
271	    case Con{+x, +xt}:
272	      +ab = Nat.mul(a, b)
273	      +k = cb(xt, ab)
274	      +hab = N.le_lt_trans(ab, Nat.add(ab, k), WD.sc(32n, one), N.le_add_right(ab, k), hc)
275	      +hk = N.le_lt_trans(k, Nat.add(ab, k), WD.sc(32n, one), le_add_l(ab, k), hc)
276	      +hs = scal_lea(one, h1, x, ys, a, b, LM.lea_head(x, xt, a, hx), hy, hab)
277	      +hz = L.and_intro(Nat.is_le(0n, k), LM.lea(F.conv(xt, ys), k), N.zero_le(k), conv_lea(one, h1, xt, ys, a, b, LM.lea_tail(x, xt, a, hx), hy, hk))
278	      addl_lea(one, h1, F.scal(x, ys), Con{0, F.conv(xt, ys)}, ab, k, hs, hz, hc)
279	
280	def conv_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hc: {Nat.is_lt(cb(xs, Nat.mul(a, b)), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.conv(xs, ys)) == Nat.mul(FS.value(xs), FS.value(ys)) : Nat}:
281	  match xs:
282	    case Nil{}:
283	      {==}
284	    case Con{+x, +xt}:
285	      +ab = Nat.mul(a, b)
286	      +k = cb(xt, ab)
287	      +Y = FS.value(ys)
288	      +X = FS.value(xt)
289	      +hab = N.le_lt_trans(ab, Nat.add(ab, k), WD.sc(32n, one), N.le_add_right(ab, k), hc)
290	      +hk = N.le_lt_trans(k, Nat.add(ab, k), WD.sc(32n, one), le_add_l(ab, k), hc)
291	      +hxh = LM.lea_head(x, xt, a, hx)
292	      +hxt = LM.lea_tail(x, xt, a, hx)
293	      +hs = scal_lea(one, h1, x, ys, a, b, hxh, hy, hab)
294	      +hz = L.and_intro(Nat.is_le(0n, k), LM.lea(F.conv(xt, ys), k), N.zero_le(k), conv_lea(one, h1, xt, ys, a, b, hxt, hy, hk))
295	      +e1 = addl_val(one, h1, F.scal(x, ys), Con{0, F.conv(xt, ys)}, ab, k, hs, hz, hc)
296	      +e2 = M.cong_add(FS.value(F.scal(x, ys)), Nat.mul(v(x), Y), FS.value(Con{0, F.conv(xt, ys)}), C.shift(8n, Nat.mul(X, Y)), scal_val(one, h1, x, ys, a, b, hxh, hy, hab), M.cong_sc(8n, FS.value(F.conv(xt, ys)), Nat.mul(X, Y), conv_val(one, h1, xt, ys, a, b, hxt, hy, hk)))
297	      +e3 = M.cong_r(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y)), Nat.mul(C.shift(8n, X), Y), AR.sc_mul(8n, X, Y))
298	      +e4 = Equal.sym(Nat, Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), Nat.add(Nat.mul(v(x), Y), Nat.mul(C.shift(8n, X), Y)), NA.mul_add_right(v(x), C.shift(8n, X), Y))
299	      Equal.trans(Nat, FS.value(F.conv(Con{x, xt}, ys)), Nat.add(FS.value(F.scal(x, ys)), FS.value(Con{0, F.conv(xt, ys)})), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e1,
300	        Equal.trans(Nat, Nat.add(FS.value(F.scal(x, ys)), FS.value(Con{0, F.conv(xt, ys)})), Nat.add(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y))), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e2,
301	          Equal.trans(Nat, Nat.add(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y))), Nat.add(Nat.mul(v(x), Y), Nat.mul(C.shift(8n, X), Y)), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e3, e4)))
302	
303	def conv_len_ge(+n: Nat, +x: U32, +xt: List<&2, U32>, +ys: List<&2, U32>, +e: {len_ge(n, ys) == True{} : Bool}) -> {len_ge(n, F.conv(Con{x, xt}, ys)) == True{} : Bool}:
304	  addl_len_ge(n, F.scal(x, ys), Con{0, F.conv(xt, ys)}, scal_len_ge(n, x, ys, e))
305	
306	# len(conv(xs, ys)) <= j + k when len(xs) <= j and len(ys) <= k
307	def conv_len_le(+j: Nat, +k: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +ex: {len_le(j, xs) == True{} : Bool}, +ey: {len_le(k, ys) == True{} : Bool}) -> {len_le(Nat.add(j, k), F.conv(xs, ys)) == True{} : Bool}:
308	  match j xs:
309	    case 0n Nil{}:
310	      len_le_nil(k)
311	    case 0n Con{x, xt}:
312	      Empty.absurd({len_le(k, F.conv(Con{x, xt}, ys)) == True{} : Bool}, L.false_true(ex))
313	    case 1n+m Nil{}:
314	      {==}
315	    case 1n+ +m Con{+x, +xt}:
316	      +hs0 = len_le_mono(k, 1n+m, F.scal(x, ys), scal_len_le(k, x, ys, ey))
317	      +hs = L.subst(Nat, z => {len_le(z, F.scal(x, ys)) == True{} : Bool}, Nat.add(k, 1n+m), Nat.add(1n+m, k), NA.add_comm(k, 1n+m), hs0)
318	      +hz = conv_len_le(m, k, xt, ys, ex, ey)
319	      addl_len_le(Nat.add(1n+m, k), F.scal(x, ys), Con{0, F.conv(xt, ys)}, hs, hz)
320	
321	# ---- take and drop ----
322	
323	def take_drop_val(+n: Nat, +xs: List<&2, U32>) -> {FS.value(xs) == Nat.add(FS.value(F.take(n, xs)), LM.sh(F.take(n, xs), FS.value(F.drop(n, xs)))) : Nat}:
324	  match n xs:
325	    case 0n _:
326	      {==}
327	    case 1n+m Nil{}:
328	      {==}
329	    case 1n+ +m Con{+x, +xt}:
330	      +T = FS.value(F.take(m, xt))
331	      +D = LM.sh(F.take(m, xt), FS.value(F.drop(m, xt)))
332	      +ih = take_drop_val(m, xt)
333	      +e1 = M.cong_r(v(x), C.shift(8n, FS.value(xt)), C.shift(8n, Nat.add(T, D)), M.cong_sc(8n, FS.value(xt), Nat.add(T, D), ih))
334	      +e2 = M.cong_r(v(x), C.shift(8n, Nat.add(T, D)), Nat.add(C.shift(8n, T), C.shift(8n, D)), Equal.sym(Nat, Nat.add(C.shift(8n, T), C.shift(8n, D)), C.shift(8n, Nat.add(T, D)), M.sc_add(8n, T, D)))
335	      +e3 = Equal.sym(Nat, Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), Nat.add(v(x), Nat.add(C.shift(8n, T), C.shift(8n, D))), NA.add_assoc(v(x), C.shift(8n, T), C.shift(8n, D)))
336	      Equal.trans(Nat, Nat.add(v(x), C.shift(8n, FS.value(xt))), Nat.add(v(x), C.shift(8n, Nat.add(T, D))), Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), e1,
337	        Equal.trans(Nat, Nat.add(v(x), C.shift(8n, Nat.add(T, D))), Nat.add(v(x), Nat.add(C.shift(8n, T), C.shift(8n, D))), Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), e2, e3))
338	
339	def take_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +hl: {len_ge(n, xs) == True{} : Bool}, +hx: {LM.lea(xs, b) == True{} : Bool}) -> {LM.okb(n, F.take(n, xs), b) == True{} : Bool}:
340	  match n xs:
341	    case 0n _:
342	      {==}
343	    case 1n+m Nil{}:
344	      Empty.absurd({LM.okb(1n+m, Nil{}, b) == True{} : Bool}, L.false_true(hl))
345	    case 1n+ +m Con{+x, +xt}:
346	      L.and_intro(Nat.is_le(v(x), b), LM.okb(m, F.take(m, xt), b), LM.lea_head(x, xt, b, hx), take_okb(m, xt, b, hl, LM.lea_tail(x, xt, b, hx)))
347	
348	def drop_lea(+n: Nat, +xs: List<&2, U32>, +b: Nat, +hx: {LM.lea(xs, b) == True{} : Bool}) -> {LM.lea(F.drop(n, xs), b) == True{} : Bool}:
349	  match n xs:
350	    case 0n _:
351	      hx
352	    case 1n+m Nil{}:
353	      {==}
354	    case 1n+ +m Con{+x, +xt}:
355	      drop_lea(m, xt, b, LM.lea_tail(x, xt, b, hx))
356	
357	def drop_len_le(+n: Nat, +k: Nat, +xs: List<&2, U32>, +hl: {len_le(Nat.add(n, k), xs) == True{} : Bool}) -> {len_le(k, F.drop(n, xs)) == True{} : Bool}:
358	  match n xs:
359	    case 0n _:
360	      hl
361	    case 1n+m Nil{}:
362	      len_le_nil(k)
363	    case 1n+ +m Con{x, +xt}:
364	      drop_len_le(m, k, xt, hl)