~/jendhub

proofs/crypto/curve25519/reduce.bend

bend-collections-laws-crypto@1.0.0.0 · 156 lines · 15 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/u32.bend as U
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD
17
18# reduce = three passes: from 32 limbs below 2^28 to 32 limbs below 2^8,
19# the value kept mod p. T = 2^(8 * 32) = LM.shn(32n, one).
20
21def v(+x: U32) -> Nat:
22  U32.to_nat(x)
23
24# value(xs) < 2^(8 n) for n limbs below 2^8
25def val_lt(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +e: {LM.okb(n, xs, 255n) == True{} : Bool}) -> {Nat.is_lt(FS.value(xs), LM.shn(n, one)) == True{} : Bool}:
26  match n xs:
27    case 0n Nil{}:
28      L.subst(Nat, o => {Nat.is_lt(0n, o) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
29    case 0n Con{y, yt}:
30      Empty.absurd({Nat.is_lt(FS.value(Con{y, yt}), one) == True{} : Bool}, L.false_true(e))
31    case 1n+m Nil{}:
32      Empty.absurd({Nat.is_lt(0n, LM.shn(1n+m, one)) == True{} : Bool}, L.false_true(e))
33    case 1n+ +m Con{+y, +yt}:
34      +X = FS.value(yt)
35      +ih = val_lt(one, h1, m, yt, LM.okb_tail(m, y, yt, 255n, e))
36      +a = M.le_sc(8n, 1n+X, LM.shn(m, one), N.lt_succ_le_succ(X, LM.shn(m, one), ih))
37      +b = L.subst(Nat, z => {Nat.is_le(z, C.shift(8n, LM.shn(m, one))) == True{} : Bool}, WD.sc(8n, 1n+X), Nat.add(256n, C.shift(8n, X)), A.sc_succ(8n, X), a)
38      +c = N.lt_add_r2(v(y), 256n, C.shift(8n, X), N.le_lt_succ(v(y), 255n, LM.okb_head(m, y, yt, 255n, e)))
39      N.lt_le_trans(Nat.add(v(y), C.shift(8n, X)), Nat.add(256n, C.shift(8n, X)), C.shift(8n, LM.shn(m, one)), c, b)
40
41# a + t < b + t -> a < b
42def lt_cancel_r(+a: Nat, +b: Nat, +t: Nat, +h: {Nat.is_lt(Nat.add(a, t), Nat.add(b, t)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
43  +h1 = N.lt_succ_le_succ(Nat.add(a, t), Nat.add(b, t), h)
44  +h2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(b, t)) == True{} : Bool}, 1n+Nat.add(a, t), Nat.add(1n+a, t), {==}, h1)
45  +h3 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(b, t)) == True{} : Bool}, Nat.add(1n+a, t), Nat.add(t, 1n+a), NA.add_comm(1n+a, t), h2)
46  +h4 = L.subst(Nat, z => {Nat.is_le(Nat.add(t, 1n+a), z) == True{} : Bool}, Nat.add(b, t), Nat.add(t, b), NA.add_comm(b, t), h3)
47  +h5 = L.subst(Bool, z => {z == True{} : Bool}, Nat.is_le(Nat.add(t, 1n+a), Nat.add(t, b)), Nat.is_le(1n+a, b), NR.le_add_cancel(t, 1n+a, b), h4)
48  N.succ_le_lt(a, b, h5)
49
50# 2^256 c >= 2^256 when c >= 1
51def shn_ge(+one: Nat, +c: Nat, +h: {Nat.is_le(one, c) == True{} : Bool}) -> {Nat.is_le(LM.shn(32n, one), LM.shn(32n, c)) == True{} : Bool}:
52  AR.sc_le(256n, one, c, h)
53
54# 2^256 c < 2^256 2 -> c < 2
55def shn_lt_cancel(+c: Nat, +d: Nat, +h: {Nat.is_lt(LM.shn(32n, c), LM.shn(32n, d)) == True{} : Bool}) -> {Nat.is_lt(c, d) == True{} : Bool}:
56  AR.sc_lt_cancel(256n, c, d, h)
57
58# K = 2^27; K + 38 <= 2^256 and K < 2^256
59def k_le_t(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(WD.sc(27n, one), LM.shn(32n, one)) == True{} : Bool}:
60  M.sc_mono(229n, 27n, one)
61
62def k38_le_t(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(WD.sc(27n, one), 38n), LM.shn(32n, one)) == True{} : Bool}:
63  +a = N.le_trans(38n, 255n, WD.sc(27n, one), {==}, FD.le255(one, h1, 19n))
64  +b = M.le_add2(WD.sc(27n, one), 38n, WD.sc(27n, one), WD.sc(27n, one), N.le_refl(WD.sc(27n, one)), a)
65  +c = L.subst(Nat, z => {Nat.is_le(Nat.add(WD.sc(27n, one), 38n), z) == True{} : Bool}, Nat.add(WD.sc(27n, one), WD.sc(27n, one)), WD.sc(28n, one), M.sc_dbl(27n, one), b)
66  N.le_trans(Nat.add(WD.sc(27n, one), 38n), WD.sc(28n, one), LM.shn(32n, one), c, M.sc_mono(228n, 28n, one))
67
68# case c < 1 (so c == 0): a + 38 c == a < T
69def small_zero(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +ha: {Nat.is_lt(a, LM.shn(32n, one)) == True{} : Bool}, +hc: {Nat.is_lt(c, one) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), LM.shn(32n, one)) == True{} : Bool}:
70  +c0 = U.lt_one_zero(c, L.subst(Nat, o => {Nat.is_lt(c, o) == True{} : Bool}, one, 1n, h1, hc))
71  %Equal.cong(Nat, Nat, z => Nat.add(a, Nat.mul(38n, z)), 0n, c, Equal.sym(Nat, c, 0n, c0)) : {Nat.is_lt(_, LM.shn(32n, one)) == True{} : Bool}
72  %Equal.sym(Nat, Nat.add(a, 0n), a, N.add_zero(a)) : {Nat.is_lt(_, LM.shn(32n, one)) == True{} : Bool}
73  ha
74
75# case c >= 1: then a < K and c == 1, so a + 38 < K + 38 <= T
76def small_one(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +V: Nat, +hv: {Nat.add(a, LM.shn(32n, c)) == V : Nat}, +hV: {Nat.is_lt(V, Nat.add(LM.shn(32n, one), WD.sc(27n, one))) == True{} : Bool}, +hc: {Nat.is_le(one, c) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), LM.shn(32n, one)) == True{} : Bool}:
77  +T = LM.shn(32n, one)
78  +K = WD.sc(27n, one)
79  +s = LM.shn(32n, c)
80  +hs = shn_ge(one, c, hc)
81  +v1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(T, K)) == True{} : Bool}, V, Nat.add(a, s), Equal.sym(Nat, Nat.add(a, s), V, hv), hV)
82  +v2 = N.le_lt_trans(Nat.add(a, T), Nat.add(a, s), Nat.add(T, K), N.le_add_left(T, s, a, hs), v1)
83  +v3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(a, T), z) == True{} : Bool}, Nat.add(T, K), Nat.add(K, T), NA.add_comm(T, K), v2)
84  +ak = lt_cancel_r(a, K, T, v3)
85  +w1 = N.le_lt_trans(s, Nat.add(a, s), Nat.add(T, K), PL.le_add_l(a, s), v1)
86  +w2 = N.lt_le_trans(s, Nat.add(T, K), Nat.add(T, T), w1, N.le_add_left(K, T, T, k_le_t(one, h1)))
87  +w3 = L.subst(Nat, z => {Nat.is_lt(s, z) == True{} : Bool}, Nat.add(T, T), LM.shn(32n, Nat.add(one, one)), M.sc_add(256n, one, one), w2)
88  +c2 = shn_lt_cancel(c, Nat.add(one, one), w3)
89  +c2b = L.subst(Nat, o => {Nat.is_lt(c, Nat.add(o, o)) == True{} : Bool}, one, 1n, h1, c2)
90  +cle = L.subst(Nat, o => {Nat.is_le(c, o) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le(c, 1n, c2b))
91  +ce = N.le_antisym(c, one, cle, hc)
92  +m1 = L.subst(Nat, o => {Nat.mul(38n, o) == 38n : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
93  %Equal.cong(Nat, Nat, z => Nat.add(a, Nat.mul(38n, z)), one, c, Equal.sym(Nat, c, one, ce)) : {Nat.is_lt(_, T) == True{} : Bool}
94  %M.cong_r(a, 38n, Nat.mul(38n, one), Equal.sym(Nat, Nat.mul(38n, one), 38n, m1)) : {Nat.is_lt(_, T) == True{} : Bool}
95  N.lt_le_trans(Nat.add(a, 38n), Nat.add(K, 38n), T, N.lt_add_r2(a, K, 38n, ak), k38_le_t(one, h1))
96
97def small_by(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +V: Nat, +b: Bool, +hb: {Nat.is_lt(c, one) == b : Bool}, +ha: {Nat.is_lt(a, LM.shn(32n, one)) == True{} : Bool}, +hv: {Nat.add(a, LM.shn(32n, c)) == V : Nat}, +hV: {Nat.is_lt(V, Nat.add(LM.shn(32n, one), WD.sc(27n, one))) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), LM.shn(32n, one)) == True{} : Bool}:
98  match b:
99    case True{}:
100      small_zero(one, h1, a, c, ha, hb)
101    case False{}:
102      small_one(one, h1, a, c, V, hv, hV, N.not_lt_le(c, one, hb))
103
104# after two passes the value is below 2^256
105def two_lt(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +hx: {LM.okb(32n, xs, WD.sc(28n, one)) == True{} : Bool}) -> {Nat.is_lt(FS.value(F.pass(F.pass(xs))), LM.shn(32n, one)) == True{} : Bool}:
106  +T = LM.shn(32n, one)
107  +K = WD.sc(27n, one)
108  +r1 = F.carry(xs, 0)
109  +a1 = FS.value(LM.cl(r1))
110  +c1 = v(LM.cc(r1))
111  +y1 = F.pass(xs)
112  +hy1 = FD.pass_okb(one, h1, xs, hx)
113  +la = val_lt(one, h1, 32n, LM.cl(r1), FD.cr_okb(one, h1, xs, hx))
114  +lc = N.le_trans(Nat.mul(38n, c1), Nat.mul(38n, WD.sc(21n, one)), WD.sc(6n, WD.sc(21n, one)), M.le_mul2(38n, c1, 38n, WD.sc(21n, one), N.le_refl(38n), FD.cr_cb(one, h1, xs, hx)), FD.m38(WD.sc(21n, one)))
115  +l1 = N.lt_le_trans(Nat.add(a1, Nat.mul(38n, c1)), Nat.add(T, Nat.mul(38n, c1)), Nat.add(T, K), N.lt_add_r2(a1, T, Nat.mul(38n, c1), la), N.le_add_left(Nat.mul(38n, c1), K, T, lc))
116  +hV = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(T, K)) == True{} : Bool}, Nat.add(a1, Nat.mul(38n, c1)), FS.value(y1), Equal.sym(Nat, FS.value(y1), Nat.add(a1, Nat.mul(38n, c1)), FD.pass_val(one, h1, xs, hx)), l1)
117  +r2 = F.carry(y1, 0)
118  +a2 = FS.value(LM.cl(r2))
119  +c2 = v(LM.cc(r2))
120  +la2 = val_lt(one, h1, 32n, LM.cl(r2), FD.cr_okb(one, h1, y1, hy1))
121  +lt2 = small_by(one, h1, a2, c2, FS.value(y1), Nat.is_lt(c2, one), {==}, la2, FD.cr_val(one, h1, y1, hy1), hV)
122  L.subst(Nat, z => {Nat.is_lt(z, T) == True{} : Bool}, Nat.add(a2, Nat.mul(38n, c2)), FS.value(F.pass(y1)), Equal.sym(Nat, FS.value(F.pass(y1)), Nat.add(a2, Nat.mul(38n, c2)), FD.pass_val(one, h1, y1, hy1)), lt2)
123
124# a pass of a value below 2^256 carries out 0: the output is the carry's limbs
125def last_zero(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +V: Nat, +hv: {Nat.add(a, LM.shn(32n, c)) == V : Nat}, +hV: {Nat.is_lt(V, LM.shn(32n, one)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(c, one) == b : Bool}) -> {c == 0n : Nat}:
126  match b:
127    case True{}:
128      U.lt_one_zero(c, L.subst(Nat, o => {Nat.is_lt(c, o) == True{} : Bool}, one, 1n, h1, hb))
129    case False{}:
130      +hs = shn_ge(one, c, N.not_lt_le(c, one, hb))
131      +x = N.le_trans(LM.shn(32n, one), LM.shn(32n, c), V, hs, L.subst(Nat, z => {Nat.is_le(LM.shn(32n, c), z) == True{} : Bool}, Nat.add(a, LM.shn(32n, c)), V, hv, PL.le_add_l(a, LM.shn(32n, c))))
132      Empty.absurd({c == 0n : Nat}, L.true_not_false(Nat.is_lt(V, LM.shn(32n, one)), hV, N.le_not_lt(V, LM.shn(32n, one), x)))
133
134def pass_exact(+r: F.Cr, +hc: {LM.cc(r) == 0 : U32}) -> {F.pass_fin(r) == LM.cl(r) : List<&2, U32>}:
135  %Equal.sym(List<&2, U32>, F.pass_fin(r), F.add0(LM.cl(r), U32.mul(38, LM.cc(r))), FD.pass_fin_eta(r)) : {_ == LM.cl(r) : List<&2, U32>}
136  %Equal.cong(U32, List<&2, U32>, z => F.add0(LM.cl(r), U32.mul(38, z)), 0, LM.cc(r), Equal.sym(U32, LM.cc(r), 0, hc)) : {_ == LM.cl(r) : List<&2, U32>}
137  FD.add0_zero(LM.cl(r))
138
139# reduce gives 32 limbs below 2^8
140def reduce_okb(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +hx: {LM.okb(32n, xs, WD.sc(28n, one)) == True{} : Bool}) -> {LM.okb(32n, F.reduce(xs), 255n) == True{} : Bool}:
141  +y2 = F.pass(F.pass(xs))
142  +hy2 = FD.pass_okb(one, h1, F.pass(xs), FD.pass_okb(one, h1, xs, hx))
143  +r3 = F.carry(y2, 0)
144  +c3 = v(LM.cc(r3))
145  +z = last_zero(one, h1, FS.value(LM.cl(r3)), c3, FS.value(y2), FD.cr_val(one, h1, y2, hy2), two_lt(one, h1, xs, hx), Nat.is_lt(c3, one), {==})
146  +cz = U.injective(LM.cc(r3), 0, z)
147  %Equal.sym(List<&2, U32>, F.pass_fin(r3), LM.cl(r3), pass_exact(r3, cz)) : {LM.okb(32n, _, 255n) == True{} : Bool}
148  FD.cr_okb(one, h1, y2, hy2)
149
150def reduce_mod(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>, +hx: {LM.okb(32n, xs, WD.sc(28n, one)) == True{} : Bool}) -> {Nat.mod(FS.value(F.reduce(xs)), 1n+pp) == Nat.mod(FS.value(xs), 1n+pp) : Nat}:
151  +y1 = F.pass(xs)
152  +hy1 = FD.pass_okb(one, h1, xs, hx)
153  +y2 = F.pass(y1)
154  +hy2 = FD.pass_okb(one, h1, y1, hy1)
155  Equal.trans(Nat, Nat.mod(FS.value(F.pass(y2)), 1n+pp), Nat.mod(FS.value(y2), 1n+pp), Nat.mod(FS.value(xs), 1n+pp), FD.pass_mod(one, h1, pp, hP, y2, hy2),
156    Equal.trans(Nat, Nat.mod(FS.value(y2), 1n+pp), Nat.mod(FS.value(y1), 1n+pp), Nat.mod(FS.value(xs), 1n+pp), FD.pass_mod(one, h1, pp, hP, y1, hy1), FD.pass_mod(one, h1, pp, hP, xs, hx)))