proofs/crypto/poly1305/step.bend

bend-collections-laws-crypto@1.0.0.0 · 428 lines · 27 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/src/crypto/poly1305/limbs.bend as Li
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
8import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as SHN
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as FB
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V
15
16# One Poly1305 block on limbs: (h + c) r == block(r, h, c) + K p exactly, for
17# an explicit K, and the block keeps the limb invariant (17 limbs, limbs
18# 0..15 of 8 bits, limb 16 at most 4, so the value is below 5 * 2^128 < 2p).
19# 2^k is C.shift(k, one) for a variable one = 1 (the checker would expand a
20# closed 2^130), and p is pm(one) = 2^130 - 5.
21
22def pm(+one: Nat) -> Nat:
23  Nat.sub(C.shift(130n, one), 5n)
24
25law p5:
26  for +one: Nat
27  for +h1: {one == 1n : Nat}
28  {Nat.add(pm(one), 5n) == C.shift(130n, one) : Nat}
29
30def p5(one, h1):
31  +s = C.shift(130n, one)
32  +h5 = N.le_trans(5n, C.shift(3n, one), s, L.subst(Nat, z => {Nat.is_le(5n, C.shift(3n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(127n, C.shift(3n, one)))
33  A.tr(Nat.add(Nat.sub(s, 5n), 5n), Nat.add(5n, Nat.sub(s, 5n)), s, N.add_comm(Nat.sub(s, 5n), 5n), N.sub_add(s, 5n, h5))
34
35# 2^130 x = x p + 5 x
36law big130:
37  for +one: Nat
38  for +h1: {one == 1n : Nat}
39  for +x: Nat
40  {C.shift(130n, x) == Nat.add(Nat.mul(x, pm(one)), Nat.mul(x, 5n)) : Nat}
41
42def big130(one, h1, x):
43  A.tr(C.shift(130n, x), Nat.mul(x, C.shift(130n, one)), Nat.add(Nat.mul(x, pm(one)), Nat.mul(x, 5n)), WW.shift_mul_one(130n, one, h1, x),
44    A.tr(Nat.mul(x, C.shift(130n, one)), Nat.mul(x, Nat.add(pm(one), 5n)), Nat.add(Nat.mul(x, pm(one)), Nat.mul(x, 5n)),
45      Equal.cong(Nat, Nat, t => Nat.mul(x, t), C.shift(130n, one), Nat.add(pm(one), 5n), A.sy(Nat.add(pm(one), 5n), C.shift(130n, one), p5(one, h1))),
46      NA.mul_add_left(x, pm(one), 5n)))
47
48# a + (b + c) == (a + c) + b
49def rot(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, c), b) : Nat}:
50  A.tr(Nat.add(a, Nat.add(b, c)), Nat.add(a, Nat.add(c, b)), Nat.add(Nat.add(a, c), b), WM.cong_r(a, Nat.add(b, c), Nat.add(c, b), N.add_comm(b, c)), A.sy(Nat.add(Nat.add(a, c), b), Nat.add(a, Nat.add(c, b)), N.add_assoc(a, c, b)))
51
52# ---- the fold 2^136 = 64 p + 320 ----
53
54def s21(+one: Nat) -> Nat:
55  C.shift(21n, one)
56
57# the fold's limb bound: 321 * 2^21 < 2^30
58def dbound(+one: Nat) -> Nat:
59  Nat.add(s21(one), Nat.mul(s21(one), 320n))
60
61law dbound_lt:
62  for +one: Nat
63  for +h1: {one == 1n : Nat}
64  {Nat.is_lt(dbound(one), C.shift(30n, one)) == True{} : Bool}
65
66def dbound_lt(one, h1):
67  +s = s21(one)
68  +l1 = A.lt_mul_l(s, 321n, 512n, A.one_le_shift(21n, one, h1), {==})
69  +l2 = A.lt_subst(Nat.mul(s, 321n), Nat.mul(s, 512n), C.shift(9n, s), A.mul_pow(9n, s), l1)
70  A.lt_substl(Nat.mul(s, 321n), dbound(one), C.shift(9n, s), NA.mul_succ(s, 320n), l2)
71
72law dbound_fits:
73  for +one: Nat
74  for +h1: {one == 1n : Nat}
75  {C.fits(32n, dbound(one)) == True{} : Bool}
76
77def dbound_fits(one, h1):
78  SH.fits_mono(30n, 32n, dbound(one), {==}, WW.fits_one(30n, one, h1, dbound(one), dbound_lt(one, h1)))
79
80law fold_ev:
81  for +one: Nat
82  for +h1: {one == 1n : Nat}
83  for +z: List<&2, U32>
84  for +hz: {V.le_all(z, s21(one)) == True{} : Bool}
85  {V.ev(z) == Nat.add(V.ev(Li.fold(z)), Nat.mul(C.shift(6n, V.ev(Li.skip(17n, z))), pm(one))) : Nat}
86
87def fold_ev(one, h1, z, hz):
88  +s = s21(one)
89  +tk = V.ev(Li.take(17n, z))
90  +e = V.ev(Li.skip(17n, z))
91  +f = C.shift(6n, e)
92  +hs = V.le_skip(17n, z, s, hz)
93  +hf4 = dbound_fits(one, h1)
94  +hf3 = A.fits_add_r(32n, s, Nat.mul(s, 320n), hf4)
95  +esc = V.scale_ev(320, Li.skip(17n, z), s, 320n, hs, {==}, hf3)
96  +ed = V.add_ev(Li.take(17n, z), Li.scale(320, Li.skip(17n, z)), s, Nat.mul(s, 320n), V.le_take(17n, z, s, hz), V.scale_le(320, Li.skip(17n, z), s, 320n, hs, {==}, hf3), hf4)
97  # e * 320 == 2^6 (e * 5)
98  +e320 = A.tr(Nat.mul(e, 320n), Nat.mul(Nat.mul(e, 5n), 64n), Nat.mul(f, 5n), A.sy(Nat.mul(Nat.mul(e, 5n), 64n), Nat.mul(e, 320n), NA.mul_assoc(e, 5n, 64n)),
99    A.tr(Nat.mul(Nat.mul(e, 5n), 64n), C.shift(6n, Nat.mul(e, 5n)), Nat.mul(f, 5n), A.mul_pow(6n, Nat.mul(e, 5n)), A.sy(Nat.mul(f, 5n), C.shift(6n, Nat.mul(e, 5n)), WW.shift_mul_l(6n, e, 5n))))
100  +efold = A.tr(V.ev(Li.fold(z)), Nat.add(tk, V.ev(Li.scale(320, Li.skip(17n, z)))), Nat.add(tk, Nat.mul(f, 5n)), ed, WM.cong_r(tk, V.ev(Li.scale(320, Li.skip(17n, z))), Nat.mul(f, 5n), A.tr(V.ev(Li.scale(320, Li.skip(17n, z))), Nat.mul(e, 320n), Nat.mul(f, 5n), esc, e320)))
101  A.tr(V.ev(z), Nat.add(tk, V.pos(17n, e)), Nat.add(V.ev(Li.fold(z)), Nat.mul(f, pm(one))), V.ts_ev(17n, z),
102    A.tr(Nat.add(tk, V.pos(17n, e)), Nat.add(tk, Nat.add(Nat.mul(f, pm(one)), Nat.mul(f, 5n))), Nat.add(V.ev(Li.fold(z)), Nat.mul(f, pm(one))),
103      WM.cong_r(tk, V.pos(17n, e), Nat.add(Nat.mul(f, pm(one)), Nat.mul(f, 5n)), big130(one, h1, f)),
104      A.tr(Nat.add(tk, Nat.add(Nat.mul(f, pm(one)), Nat.mul(f, 5n))), Nat.add(Nat.add(tk, Nat.mul(f, 5n)), Nat.mul(f, pm(one))), Nat.add(V.ev(Li.fold(z)), Nat.mul(f, pm(one))),
105        rot(tk, Nat.mul(f, pm(one)), Nat.mul(f, 5n)),
106        WM.cong_l(Nat.add(tk, Nat.mul(f, 5n)), V.ev(Li.fold(z)), Nat.mul(f, pm(one)), A.sy(V.ev(Li.fold(z)), Nat.add(tk, Nat.mul(f, 5n)), efold)))))
107
108law fold_fit:
109  for +one: Nat
110  for +h1: {one == 1n : Nat}
111  for +z: List<&2, U32>
112  for +hz: {V.le_all(z, s21(one)) == True{} : Bool}
113  {V.fit_all(Li.fold(z), 30n) == True{} : Bool}
114
115def fold_fit(one, h1, z, hz):
116  +s = s21(one)
117  +hs = V.le_skip(17n, z, s, hz)
118  +hf4 = dbound_fits(one, h1)
119  +hf3 = A.fits_add_r(32n, s, Nat.mul(s, 320n), hf4)
120  V.le_fit(Li.fold(z), dbound(one), 30n, one, h1, dbound_lt(one, h1),
121    V.add_le(Li.take(17n, z), Li.scale(320, Li.skip(17n, z)), s, Nat.mul(s, 320n), V.le_take(17n, z, s, hz), V.scale_le(320, Li.skip(17n, z), s, 320n, hs, {==}, hf3), hf4))
122
123law fold_len:
124  for +z: List<&2, U32>
125  for +hl: {Nat.is_le(V.len(z), 33n) == True{} : Bool}
126  {Nat.is_le(V.len(Li.fold(z)), 17n) == True{} : Bool}
127
128def fold_len(z, hl):
129  V.len_add(Li.take(17n, z), Li.scale(320, Li.skip(17n, z)), 17n, V.len_take(17n, z),
130    A.le_substl(V.len(Li.skip(17n, z)), V.len(Li.scale(320, Li.skip(17n, z))), 17n, A.sy(V.len(Li.scale(320, Li.skip(17n, z))), V.len(Li.skip(17n, z)), V.len_scale(320, Li.skip(17n, z))),
131      N.le_trans(V.len(Li.skip(17n, z)), 16n, 17n, V.len_skip(17n, z, 16n, hl), {==})))
132
133# ---- the partial reduction ----
134
135def pv(+d: List<&2, U32>) -> Nat:
136  V.v(Li.quot(16n, Li.carry(16n, d, 0)))
137
138# the limb invariant: 17 limbs, all of 8 bits, limb 16 at most 4
139def inv(+h: List<&2, U32>) -> Bool:
140  Bool.and(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)))
141
142# v(quot) fits 29 bits: the pass-1 top limb fits 31
143law q29:
144  for +d: List<&2, U32>
145  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
146  {C.fits(29n, pv(d)) == True{} : Bool}
147
148def q29(d, hd):
149  +t = Li.carry(16n, d, 0)
150  +top = Li.hd0(Li.skip(16n, t))
151  +ftop = V.carry_top(16n, d, 0, 22n, {==}, hd, {==})
152  +eq = A.tr(pv(d), V.v(U32.shrn(top, 2n)), C.high(2n, V.v(top)), Equal.cong(U32, Nat, w => V.v(w), Li.quot(16n, t), U32.shrn(top, 2n), V.quot_top(16n, t)), SHN.shrn_high(top, 2n))
153  A.fits_subst(29n, C.high(2n, V.v(top)), pv(d), A.sy(pv(d), C.high(2n, V.v(top)), eq), SH.fits_high(2n, 29n, V.v(top), ftop))
154
155# pass 2 on the split: its value is 5 q + the split
156law pass2_ev:
157  for +d: List<&2, U32>
158  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
159  {V.ev(Li.reduce(d)) == Nat.add(Nat.mul(pv(d), 5n), V.ev(Li.split(16n, Li.carry(16n, d, 0)))) : Nat}
160
161def pass2_ev(d, hd):
162  +t = Li.carry(16n, d, 0)
163  +q = Li.quot(16n, t)
164  +vq = V.v(q)
165  +a5 = U32.mul(q, 5)
166  +t0 = Li.hd0(t)
167  +y0 = U32.add(a5, t0)
168  +s0 = U32.add(0, y0)
169  +u1 = U32.shrn(s0, 8n)
170  +rr = Li.split(15n, Li.tl(t))
171  +hlo = V.carry_lo(16n, d, 0)
172  +hq = q29(d, hd)
173  +ea5 = A.tr(V.v(a5), C.low(32n, Nat.mul(vq, 5n)), Nat.mul(vq, 5n), SH.mul_low(q, 5), WW.low_fit(32n, Nat.mul(vq, 5n), A.fits_mul(29n, 3n, vq, 5n, hq, {==})))
174  +ht0 = L.and_left(C.fits(8n, V.v(t0)), V.fit_all(Li.take(15n, Li.tl(t)), 8n), hlo)
175  +hy0a = A.fits_5q(29n, vq, V.v(t0), hq, SH.fits_mono(8n, 29n, V.v(t0), {==}, ht0))
176  +hy0 = A.fits_subst(32n, Nat.add(Nat.mul(vq, 5n), V.v(t0)), Nat.add(V.v(a5), V.v(t0)), WM.cong_l(Nat.mul(vq, 5n), V.v(a5), V.v(t0), A.sy(V.v(a5), Nat.mul(vq, 5n), ea5)), hy0a)
177  +ey0 = WA.add_exact(1n, {==}, a5, t0, hy0)
178  +hy = A.fits_subst(32n, Nat.add(V.v(a5), V.v(t0)), V.v(y0), A.sy(V.v(y0), Nat.add(V.v(a5), V.v(t0)), ey0), hy0)
179  +es0 = WA.add_exact(1n, {==}, 0, y0, hy)
180  +hs0 = A.fits_subst(32n, V.v(y0), V.v(s0), A.sy(V.v(s0), V.v(y0), es0), hy)
181  +eu1 = SHN.shrn_high(s0, 8n)
182  +hu1 = A.fits_subst(24n, C.high(8n, V.v(s0)), V.v(u1), A.sy(V.v(u1), C.high(8n, V.v(s0)), eu1), SH.fits_high(8n, 24n, V.v(s0), hs0))
183  +hr = V.fit_mono(rr, 8n, 24n, {==}, V.split_fit(15n, Li.tl(t), L.and_right(C.fits(8n, V.v(t0)), V.fit_all(Li.take(15n, Li.tl(t)), 8n), hlo)))
184  +c15 = V.ev(Li.carry(15n, rr, u1))
185  +ce = V.carry_ev(15n, rr, u1, 16n, {==}, hr, hu1)
186  +ec = A.tr(c15, Nat.add(c15, 0n), Nat.add(V.v(u1), V.ev(rr)), A.sy(Nat.add(c15, 0n), c15, N.add_zero(c15)), ce)
187  +lo = V.v(U32.and(s0, 255))
188  +elo = FB.andm(s0, 8n, 255, {==})
189  +e4 = A.tr(Nat.add(lo, C.shift(8n, V.v(u1))), Nat.add(C.low(8n, V.v(s0)), C.shift(8n, C.high(8n, V.v(s0)))), V.v(s0),
190    A.cadd(lo, C.low(8n, V.v(s0)), C.shift(8n, V.v(u1)), C.shift(8n, C.high(8n, V.v(s0))), elo, A.csh(8n, V.v(u1), C.high(8n, V.v(s0)), eu1)),
191    A.sy(V.v(s0), Nat.add(C.low(8n, V.v(s0)), C.shift(8n, C.high(8n, V.v(s0)))), WW.low_high(8n, V.v(s0))))
192  +er = C.shift(8n, V.ev(rr))
193  A.tr(Nat.add(lo, C.shift(8n, c15)), Nat.add(lo, C.shift(8n, Nat.add(V.v(u1), V.ev(rr)))), Nat.add(Nat.mul(vq, 5n), Nat.add(V.v(t0), er)),
194    WM.cong_r(lo, C.shift(8n, c15), C.shift(8n, Nat.add(V.v(u1), V.ev(rr))), A.csh(8n, c15, Nat.add(V.v(u1), V.ev(rr)), ec)),
195    A.tr(Nat.add(lo, C.shift(8n, Nat.add(V.v(u1), V.ev(rr)))), Nat.add(Nat.add(lo, C.shift(8n, V.v(u1))), er), Nat.add(Nat.mul(vq, 5n), Nat.add(V.v(t0), er)),
196      A.sy(Nat.add(Nat.add(lo, C.shift(8n, V.v(u1))), er), Nat.add(lo, C.shift(8n, Nat.add(V.v(u1), V.ev(rr)))), V.sh3(lo, V.v(u1), V.ev(rr))),
197      A.tr(Nat.add(Nat.add(lo, C.shift(8n, V.v(u1))), er), Nat.add(V.v(s0), er), Nat.add(Nat.mul(vq, 5n), Nat.add(V.v(t0), er)),
198        WM.cong_l(Nat.add(lo, C.shift(8n, V.v(u1))), V.v(s0), er, e4),
199        A.tr(Nat.add(V.v(s0), er), Nat.add(Nat.add(V.v(a5), V.v(t0)), er), Nat.add(Nat.mul(vq, 5n), Nat.add(V.v(t0), er)),
200          WM.cong_l(V.v(s0), Nat.add(V.v(a5), V.v(t0)), er, A.tr(V.v(s0), V.v(y0), Nat.add(V.v(a5), V.v(t0)), es0, ey0)),
201          A.tr(Nat.add(Nat.add(V.v(a5), V.v(t0)), er), Nat.add(V.v(a5), Nat.add(V.v(t0), er)), Nat.add(Nat.mul(vq, 5n), Nat.add(V.v(t0), er)),
202            N.add_assoc(V.v(a5), V.v(t0), er),
203            WM.cong_l(V.v(a5), Nat.mul(vq, 5n), Nat.add(V.v(t0), er), ea5))))))
204
205law reduce_ev:
206  for +one: Nat
207  for +h1: {one == 1n : Nat}
208  for +d: List<&2, U32>
209  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
210  for +hl: {Nat.is_le(V.len(d), 17n) == True{} : Bool}
211  {V.ev(d) == Nat.add(V.ev(Li.reduce(d)), Nat.mul(pv(d), pm(one))) : Nat}
212
213def reduce_ev(one, h1, d, hd, hl):
214  +t = Li.carry(16n, d, 0)
215  +vq = pv(d)
216  +esp = V.ev(Li.split(16n, t))
217  +c = V.carry_ev(16n, d, 0, 22n, {==}, hd, {==})
218  +sk = V.skip_long(17n, d, hl)
219  +et = A.tr(V.ev(t), Nat.add(V.ev(t), 0n), V.ev(d), A.sy(Nat.add(V.ev(t), 0n), V.ev(t), N.add_zero(V.ev(t))),
220    A.tr(Nat.add(V.ev(t), 0n), Nat.add(V.ev(t), V.pos(17n, V.ev(Li.skip(17n, d)))), V.ev(d), Equal.cong(List<&2, U32>, Nat, l => Nat.add(V.ev(t), V.pos(17n, V.ev(l))), [], Li.skip(17n, d), Equal.sym(List<&2, U32>, Li.skip(17n, d), [], sk)), c))
221  +sq = V.sq_ev(16n, t)
222  +et2 = A.tr(V.ev(t), Nat.add(Nat.add(esp, C.shift(130n, vq)), 0n), Nat.add(esp, C.shift(130n, vq)), A.sy(Nat.add(Nat.add(esp, C.shift(130n, vq)), 0n), V.ev(t), sq), N.add_zero(Nat.add(esp, C.shift(130n, vq))))
223  +e2 = pass2_ev(d, hd)
224  A.tr(V.ev(d), Nat.add(esp, C.shift(130n, vq)), Nat.add(V.ev(Li.reduce(d)), Nat.mul(vq, pm(one))), A.tr(V.ev(d), V.ev(t), Nat.add(esp, C.shift(130n, vq)), A.sy(V.ev(t), V.ev(d), et), et2),
225    A.tr(Nat.add(esp, C.shift(130n, vq)), Nat.add(esp, Nat.add(Nat.mul(vq, pm(one)), Nat.mul(vq, 5n))), Nat.add(V.ev(Li.reduce(d)), Nat.mul(vq, pm(one))),
226      WM.cong_r(esp, C.shift(130n, vq), Nat.add(Nat.mul(vq, pm(one)), Nat.mul(vq, 5n)), big130(one, h1, vq)),
227      A.tr(Nat.add(esp, Nat.add(Nat.mul(vq, pm(one)), Nat.mul(vq, 5n))), Nat.add(Nat.add(esp, Nat.mul(vq, 5n)), Nat.mul(vq, pm(one))), Nat.add(V.ev(Li.reduce(d)), Nat.mul(vq, pm(one))),
228        rot(esp, Nat.mul(vq, pm(one)), Nat.mul(vq, 5n)),
229        WM.cong_l(Nat.add(esp, Nat.mul(vq, 5n)), V.ev(Li.reduce(d)), Nat.mul(vq, pm(one)),
230          A.tr(Nat.add(esp, Nat.mul(vq, 5n)), Nat.add(Nat.mul(vq, 5n), esp), V.ev(Li.reduce(d)), N.add_comm(esp, Nat.mul(vq, 5n)), A.sy(V.ev(Li.reduce(d)), Nat.add(Nat.mul(vq, 5n), esp), e2))))))
231
232# the top limb after the reduction is at most 4 (its value is below 5 * 2^128)
233law reduce_top:
234  for +one: Nat
235  for +h1: {one == 1n : Nat}
236  for +d: List<&2, U32>
237  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
238  {Nat.is_le(V.v(Li.hd0(Li.skip(16n, Li.reduce(d)))), 4n) == True{} : Bool}
239
240def reduce_top(one, h1, d, hd):
241  +h2 = Li.reduce(d)
242  +t = Li.carry(16n, d, 0)
243  +sp = Li.split(16n, t)
244  +vq5 = Nat.mul(pv(d), 5n)
245  +tp = V.v(Li.hd0(Li.skip(16n, h2)))
246  +tt = Nat.add(tp, 0n)
247  +x16 = V.ev(Li.take(16n, h2))
248  +e16 = V.ev(Li.take(16n, t))
249  +a3 = Nat.add(V.v(U32.and(Li.hd0(Li.skip(16n, t)), 3)), 0n)
250  +p1 = V.pos(16n, one)
251  +ts1 = V.ts_ev(16n, h2)
252  +ts2 = V.ts_ev(16n, sp)
253  +e2 = pass2_ev(d, hd)
254  # ev(h2) = 5q + ev(take16 t) + 2^128 a3
255  +ev2 = A.tr(V.ev(h2), Nat.add(vq5, V.ev(sp)), Nat.add(vq5, Nat.add(e16, V.pos(16n, a3))), e2, WM.cong_r(vq5, V.ev(sp), Nat.add(e16, V.pos(16n, a3)), ts2))
256  +l1 = N.lt_le_trans(vq5, C.shift(32n, one), p1, WW.lt_one(32n, one, h1, vq5, A.fits_mul(29n, 3n, pv(d), 5n, q29(d, hd), {==})), WW.shift_ge(96n, C.shift(32n, one)))
257  +l2 = V.ev_lt(Li.take(16n, t), one, h1, V.carry_lo(16n, d, 0))
258  +b2 = A.lt_add2(vq5, Nat.add(e16, V.pos(16n, a3)), p1, Nat.add(p1, V.pos(16n, a3)), l1, A.lt_le_add(e16, V.pos(16n, a3), p1, V.pos(16n, a3), l2, N.le_refl(V.pos(16n, a3))))
259  +e3 = A.tr(Nat.add(p1, Nat.add(p1, V.pos(16n, a3))), Nat.add(p1, V.pos(16n, Nat.add(one, a3))), V.pos(16n, Nat.add(one, Nat.add(one, a3))),
260    WM.cong_r(p1, Nat.add(p1, V.pos(16n, a3)), V.pos(16n, Nat.add(one, a3)), A.sy(V.pos(16n, Nat.add(one, a3)), Nat.add(p1, V.pos(16n, a3)), V.pos_add(16n, one, a3))),
261    A.sy(V.pos(16n, Nat.add(one, Nat.add(one, a3))), Nat.add(p1, V.pos(16n, Nat.add(one, a3))), V.pos_add(16n, one, Nat.add(one, a3))))
262  +b1 = A.le_subst(V.pos(16n, tt), Nat.add(x16, V.pos(16n, tt)), V.ev(h2), A.sy(V.ev(h2), Nat.add(x16, V.pos(16n, tt)), ts1), A.le_add_l(x16, V.pos(16n, tt)))
263  +b1b = A.le_subst(V.pos(16n, tt), V.ev(h2), Nat.add(vq5, Nat.add(e16, V.pos(16n, a3))), ev2, b1)
264  +lt1 = N.le_lt_trans(V.pos(16n, tt), Nat.add(vq5, Nat.add(e16, V.pos(16n, a3))), V.pos(16n, Nat.add(one, Nat.add(one, a3))), b1b, A.lt_subst(Nat.add(vq5, Nat.add(e16, V.pos(16n, a3))), Nat.add(p1, Nat.add(p1, V.pos(16n, a3))), V.pos(16n, Nat.add(one, Nat.add(one, a3))), e3, b2))
265  +lt2 = A.shift_cancel(128n, tt, Nat.add(one, Nat.add(one, a3)), lt1)
266  +lt3 = L.subst(Nat, z => {Nat.is_lt(tt, Nat.add(z, Nat.add(z, a3))) == True{} : Bool}, one, 1n, h1, lt2)
267  +a3v = V.v(U32.and(Li.hd0(Li.skip(16n, t)), 3))
268  +xt = V.v(Li.hd0(Li.skip(16n, t)))
269  +la = A.lt_substl(C.low(2n, xt), a3v, 4n, A.sy(a3v, C.low(2n, xt), FB.andm(Li.hd0(Li.skip(16n, t)), 2n, 3, {==})), WW.low_lt(2n, xt))
270  +la3 = A.le_substl(a3v, a3, 3n, A.sy(a3, a3v, N.add_zero(a3v)), N.lt_succ_le(a3v, 3n, la))
271  +lt5 = N.lt_le_trans(tt, Nat.add(1n, Nat.add(1n, a3)), 5n, lt3, la3)
272  A.le_substl(tt, tp, 4n, N.add_zero(tp), N.lt_succ_le(tt, 4n, lt5))
273
274law reduce_inv:
275  for +one: Nat
276  for +h1: {one == 1n : Nat}
277  for +d: List<&2, U32>
278  for +hd: {V.fit_all(d, 30n) == True{} : Bool}
279  {inv(Li.reduce(d)) == True{} : Bool}
280
281def reduce_inv(one, h1, d, hd):
282  +h2 = Li.reduce(d)
283  +t = Li.carry(16n, d, 0)
284  +y = Li.add([U32.mul(Li.quot(16n, t), 5)], Li.split(16n, t))
285  +tp = V.v(Li.hd0(Li.skip(16n, h2)))
286  +htop = reduce_top(one, h1, d, hd)
287  +f8 = WW.fits_of_lt(8n, tp, N.le_lt_trans(tp, 4n, C.pow2(8n), htop, {==}))
288  +hf = V.fit_split(16n, h2, 8n, V.carry_lo(16n, y, 0), L.and_intro(C.fits(8n, tp), True{}, f8, {==}))
289  L.and_intro(Nat.is_eq(V.len(h2), 17n), Bool.and(V.fit_all(h2, 8n), Nat.is_le(tp, 4n)), {==}, L.and_intro(V.fit_all(h2, 8n), Nat.is_le(tp, 4n), hf, htop))
290
291# ---- one block ----
292
293def zz(+r: List<&2, U32>, +h: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
294  Li.mul(Li.add(h, c), r)
295
296# the multiple of p dropped by one block
297def bk(+r: List<&2, U32>, +h: List<&2, U32>, +c: List<&2, U32>) -> Nat:
298  Nat.add(C.shift(6n, V.ev(Li.skip(17n, zz(r, h, c)))), pv(Li.fold(zz(r, h, c))))
299
300# the product's limbs are at most 2^21, its length at most 33
301law z_le:
302  for +one: Nat
303  for +h1: {one == 1n : Nat}
304  for +r: List<&2, U32>
305  for +h: List<&2, U32>
306  for +c: List<&2, U32>
307  for +hh: {V.fit_all(h, 8n) == True{} : Bool}
308  for +hcf: {V.fit_all(c, 8n) == True{} : Bool}
309  for +hrl: {V.len(r) == 16n : Nat}
310  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
311  {V.le_all(zz(r, h, c), s21(one)) == True{} : Bool}
312
313def s8fit(+one: Nat, +h1: {one == 1n : Nat}) -> {C.fits(32n, Nat.add(C.shift(8n, one), C.shift(8n, one))) == True{} : Bool}:
314  +s8 = C.shift(8n, one)
315  +f9 = A.fits_le_one(8n, one, h1, s8, N.le_refl(s8))
316  SH.fits_mono(10n, 32n, Nat.add(s8, s8), {==}, A.fits_add(9n, s8, s8, f9, f9))
317
318# len(r) * (2^9 * 2^8) == 2^21
319def mbound(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, U32>, +hrl: {V.len(r) == 16n : Nat}) -> {Nat.mul(V.len(r), Nat.mul(Nat.add(C.shift(8n, one), C.shift(8n, one)), C.shift(8n, one))) == s21(one) : Nat}:
320  +s8 = C.shift(8n, one)
321  +m = Nat.mul(Nat.add(s8, s8), s8)
322  +em = A.tr(m, Nat.mul(C.shift(9n, one), s8), C.shift(17n, one), A.cmul(Nat.add(s8, s8), C.shift(9n, one), s8, s8, A.sy(Nat.double(s8), Nat.add(s8, s8), NA.double_self(s8)), {==}), A.shmul(9n, 8n, one, h1))
323  A.tr(Nat.mul(V.len(r), m), Nat.mul(16n, m), s21(one), Equal.cong(Nat, Nat, t => Nat.mul(t, m), V.len(r), 16n, hrl),
324    A.tr(Nat.mul(16n, m), Nat.mul(m, 16n), s21(one), NA.mul_comm(16n, m),
325      A.tr(Nat.mul(m, 16n), C.shift(4n, m), s21(one), A.mul_pow(4n, m), A.csh(4n, m, C.shift(17n, one), em))))
326
327def z_le(one, h1, r, h, c, hh, hcf, hrl, hrf):
328  +s8 = C.shift(8n, one)
329  +x = Li.add(h, c)
330  +hf1 = s8fit(one, h1)
331  +hx = V.add_le(h, c, s8, s8, V.fit_le(h, 8n, one, h1, hh), V.fit_le(c, 8n, one, h1, hcf), hf1)
332  +eb = mbound(one, h1, r, hrl)
333  +b = Nat.mul(V.len(r), Nat.mul(Nat.add(s8, s8), s8))
334  +hf2 = A.fits_subst(32n, s21(one), b, A.sy(b, s21(one), eb), SH.fits_mono(22n, 32n, s21(one), {==}, A.fits_le_one(21n, one, h1, s21(one), N.le_refl(s21(one)))))
335  V.le_mono(zz(r, h, c), b, s21(one), N.eq_le(b, s21(one), eb), V.mul_le(x, r, Nat.add(s8, s8), s8, hx, V.fit_le(r, 8n, one, h1, hrf), hf2))
336
337law z_ev:
338  for +one: Nat
339  for +h1: {one == 1n : Nat}
340  for +r: List<&2, U32>
341  for +h: List<&2, U32>
342  for +c: List<&2, U32>
343  for +hh: {V.fit_all(h, 8n) == True{} : Bool}
344  for +hcf: {V.fit_all(c, 8n) == True{} : Bool}
345  for +hrl: {V.len(r) == 16n : Nat}
346  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
347  {V.ev(zz(r, h, c)) == Nat.mul(Nat.add(V.ev(h), V.ev(c)), V.ev(r)) : Nat}
348
349def z_ev(one, h1, r, h, c, hh, hcf, hrl, hrf):
350  +s8 = C.shift(8n, one)
351  +x = Li.add(h, c)
352  +hf1 = s8fit(one, h1)
353  +hx = V.add_le(h, c, s8, s8, V.fit_le(h, 8n, one, h1, hh), V.fit_le(c, 8n, one, h1, hcf), hf1)
354  +ex = V.add_ev(h, c, s8, s8, V.fit_le(h, 8n, one, h1, hh), V.fit_le(c, 8n, one, h1, hcf), hf1)
355  +eb = mbound(one, h1, r, hrl)
356  +b = Nat.mul(V.len(r), Nat.mul(Nat.add(s8, s8), s8))
357  +hf2 = A.fits_subst(32n, s21(one), b, A.sy(b, s21(one), eb), SH.fits_mono(22n, 32n, s21(one), {==}, A.fits_le_one(21n, one, h1, s21(one), N.le_refl(s21(one)))))
358  A.tr(V.ev(zz(r, h, c)), Nat.mul(V.ev(x), V.ev(r)), Nat.mul(Nat.add(V.ev(h), V.ev(c)), V.ev(r)),
359    V.mul_ev(x, r, Nat.add(s8, s8), s8, hx, V.fit_le(r, 8n, one, h1, hrf), hf2),
360    Equal.cong(Nat, Nat, t => Nat.mul(t, V.ev(r)), V.ev(x), Nat.add(V.ev(h), V.ev(c)), ex))
361
362law z_len:
363  for +r: List<&2, U32>
364  for +h: List<&2, U32>
365  for +c: List<&2, U32>
366  for +hhl: {Nat.is_le(V.len(h), 17n) == True{} : Bool}
367  for +hcl: {Nat.is_le(V.len(c), 17n) == True{} : Bool}
368  for +hrl: {V.len(r) == 16n : Nat}
369  {Nat.is_le(V.len(zz(r, h, c)), 33n) == True{} : Bool}
370
371def z_len(r, h, c, hhl, hcl, hrl):
372  A.le_subst(V.len(zz(r, h, c)), Nat.add(V.len(r), 17n), 33n, Equal.cong(Nat, Nat, t => Nat.add(t, 17n), V.len(r), 16n, hrl),
373    V.len_mul(Li.add(h, c), r, 17n, V.len_add(h, c, 17n, hhl, hcl)))
374
375# (h + c) r == block(r, h, c) + bk p
376law block_ev:
377  for +one: Nat
378  for +h1: {one == 1n : Nat}
379  for +r: List<&2, U32>
380  for +h: List<&2, U32>
381  for +c: List<&2, U32>
382  for +hh: {inv(h) == True{} : Bool}
383  for +hcl: {Nat.is_le(V.len(c), 17n) == True{} : Bool}
384  for +hcf: {V.fit_all(c, 8n) == True{} : Bool}
385  for +hrl: {V.len(r) == 16n : Nat}
386  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
387  {Nat.mul(Nat.add(V.ev(h), V.ev(c)), V.ev(r)) == Nat.add(V.ev(Li.block(r, h, c)), Nat.mul(bk(r, h, c), pm(one))) : Nat}
388
389def block_ev(one, h1, r, h, c, hh, hcl, hcf, hrl, hrf):
390  +hhl = N.eq_le(V.len(h), 17n, N.eq_from_is_eq(V.len(h), 17n, L.and_left(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh)))
391  +hr2 = L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh)
392  +hhf = L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), hr2)
393  +z = zz(r, h, c)
394  +d = Li.fold(z)
395  +hz = z_le(one, h1, r, h, c, hhf, hcf, hrl, hrf)
396  +hd = fold_fit(one, h1, z, hz)
397  +hdl = fold_len(z, z_len(r, h, c, hhl, hcl, hrl))
398  +f = C.shift(6n, V.ev(Li.skip(17n, z)))
399  +q = pv(d)
400  +p = pm(one)
401  +e1 = A.sy(V.ev(z), Nat.mul(Nat.add(V.ev(h), V.ev(c)), V.ev(r)), z_ev(one, h1, r, h, c, hhf, hcf, hrl, hrf))
402  +e2 = fold_ev(one, h1, z, hz)
403  +e3 = WM.cong_l(V.ev(d), Nat.add(V.ev(Li.reduce(d)), Nat.mul(q, p)), Nat.mul(f, p), reduce_ev(one, h1, d, hd, hdl))
404  +e4 = A.tr(Nat.add(Nat.add(V.ev(Li.reduce(d)), Nat.mul(q, p)), Nat.mul(f, p)), Nat.add(V.ev(Li.reduce(d)), Nat.add(Nat.mul(q, p), Nat.mul(f, p))), Nat.add(V.ev(Li.reduce(d)), Nat.mul(Nat.add(f, q), p)),
405    N.add_assoc(V.ev(Li.reduce(d)), Nat.mul(q, p), Nat.mul(f, p)),
406    WM.cong_r(V.ev(Li.reduce(d)), Nat.add(Nat.mul(q, p), Nat.mul(f, p)), Nat.mul(Nat.add(f, q), p),
407      A.tr(Nat.add(Nat.mul(q, p), Nat.mul(f, p)), Nat.add(Nat.mul(f, p), Nat.mul(q, p)), Nat.mul(Nat.add(f, q), p), N.add_comm(Nat.mul(q, p), Nat.mul(f, p)), A.sy(Nat.mul(Nat.add(f, q), p), Nat.add(Nat.mul(f, p), Nat.mul(q, p)), NA.mul_add_right(f, q, p)))))
408  A.tr(Nat.mul(Nat.add(V.ev(h), V.ev(c)), V.ev(r)), V.ev(z), Nat.add(V.ev(Li.reduce(d)), Nat.mul(Nat.add(f, q), p)), e1,
409    A.tr(V.ev(z), Nat.add(V.ev(d), Nat.mul(f, p)), Nat.add(V.ev(Li.reduce(d)), Nat.mul(Nat.add(f, q), p)), e2,
410      A.tr(Nat.add(V.ev(d), Nat.mul(f, p)), Nat.add(Nat.add(V.ev(Li.reduce(d)), Nat.mul(q, p)), Nat.mul(f, p)), Nat.add(V.ev(Li.reduce(d)), Nat.mul(Nat.add(f, q), p)), e3, e4)))
411
412law block_inv:
413  for +one: Nat
414  for +h1: {one == 1n : Nat}
415  for +r: List<&2, U32>
416  for +h: List<&2, U32>
417  for +c: List<&2, U32>
418  for +hh: {inv(h) == True{} : Bool}
419  for +hcf: {V.fit_all(c, 8n) == True{} : Bool}
420  for +hrl: {V.len(r) == 16n : Nat}
421  for +hrf: {V.fit_all(r, 8n) == True{} : Bool}
422  {inv(Li.block(r, h, c)) == True{} : Bool}
423
424def block_inv(one, h1, r, h, c, hh, hcf, hrl, hrf):
425  +hr2 = L.and_right(Nat.is_eq(V.len(h), 17n), Bool.and(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n)), hh)
426  +hhf = L.and_left(V.fit_all(h, 8n), Nat.is_le(V.v(Li.hd0(Li.skip(16n, h))), 4n), hr2)
427  +z = zz(r, h, c)
428  reduce_inv(one, h1, Li.fold(z), fold_fit(one, h1, z, z_le(one, h1, r, h, c, hhf, hcf, hrl, hrf)))