proofs/crypto/curve25519/poly.bend

bend-collections-laws-crypto@1.0.0.0 · 364 lines · 32 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/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
19def v(+x: U32) -> Nat:
20  U32.to_nat(x)
21
22# ---- lengths ----
23
24def 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
39def 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
50def len_le_nil(+n: Nat) -> {len_le(n, Nil{}) == True{} : Bool}:
51  match n:
52    case 0n:
53      {==}
54    case 1n+m:
55      {==}
56
57def 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
68def 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
79def 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
90def 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
101def 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
107def 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
110def 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
126def 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
138def 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
157def 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
168def 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
183def 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
189def 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
192def 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
206def 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
216def 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
230def 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
239def 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
253def 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
260def 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
267def 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
280def 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
303def 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
307def 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
323def 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
339def 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
348def 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
357def 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)