~/jendhub

proofs/crypto/ed25519/scalar3.bend

bend-collections-laws-crypto@1.0.0.0 · 136 lines · 19 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/spec/crypto/ed25519.bend as SE
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
14import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as AD
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend as S2
22
23# The group order L of spec/crypto/ed25519.bend and the scalar clauses:
24# L + (2^256 - L) == 2^256 and 2 L <= 2^256 by certified digit additions,
25# then reduce, mul_add and lt_l of src/crypto/ed25519/scalar.bend.
26
27def v(+x: U32) -> Nat:
28  U32.to_nat(x)
29
30# 2^256 - 2 L
31def dlist() -> List<&2, U32>:
32  [38, 88, 20, 70, 203, 57, 219, 79, 83, 198, 16, 186, 66, 12, 66, 214,
33   255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 223]
34
35def zeros() -> List<&2, U32>:
36  K.rep(32n, 0, Nil{})
37
38def adc1() -> {AD.adc_ok(ESC.ell(), dlist(), ESC.comp_l(), 0n, 0n) == True{} : Bool}:
39  {==}
40
41def adc2() -> {AD.adc_ok(ESC.comp_l(), ESC.ell(), zeros(), 0n, 1n) == True{} : Bool}:
42  {==}
43
44def ell_valo(+one: Nat) -> {K.valo(one, ESC.ell()) == SE.ell(one) : Nat}:
45  AD.valo_u(one, ESC.ell())
46
47def mmL(+one: Nat) -> Nat:
48  Nat.sub(SE.ell(one), 1n)
49
50def ell_ge(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(2n, SE.ell(one)) == True{} : Bool}:
51  +e = Equal.sym(Nat, K.valo(one, ESC.ell()), SE.ell(one), ell_valo(one))
52  +a = L.subst(Nat, o => {Nat.is_le(2n, Nat.mul(o, v(237))) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
53  +b = N.le_trans(2n, Nat.mul(one, v(237)), K.valo(one, ESC.ell()), a, N.le_add_right(Nat.mul(one, v(237)), C.shift(8n, K.valo(one, K.rep(0n, 0, [211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222, 20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16])))))
54  L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, K.valo(one, ESC.ell()), SE.ell(one), Equal.sym(Nat, SE.ell(one), K.valo(one, ESC.ell()), e), b)
55
56def ell_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+mmL(one) == SE.ell(one) : Nat}:
57  N.sub_add(SE.ell(one), 1n, N.le_trans(1n, 2n, SE.ell(one), {==}, ell_ge(one, h1)))
58
59def one_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(1n, 1n+mmL(one)) == True{} : Bool}:
60  L.subst(Nat, z => {Nat.is_lt(1n, z) == True{} : Bool}, SE.ell(one), 1n+mmL(one), Equal.sym(Nat, 1n+mmL(one), SE.ell(one), ell_eq(one, h1)), N.succ_le_lt(1n, SE.ell(one), ell_ge(one, h1)))
61
62def cp_okb() -> {LM.okb(32n, ESC.comp_l(), 255n) == True{} : Bool}:
63  {==}
64
65def zero_vg(+one: Nat, +h1: {one == 1n : Nat}) -> {K.valo(one, zeros()) == 0n : Nat}:
66  Equal.trans(Nat, K.valo(one, zeros()), LM.shn(32n, K.valo(one, Nil{})), 0n, K.run0(one, 32n, Nil{}), {==})
67
68# (2^256 - L) + L == 2^256
69def hvL(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(K.valo(one, ESC.comp_l()), 1n+mmL(one)) == SC.T(one) : Nat}:
70  +cp = ESC.comp_l()
71  +C1 = K.valo(one, cp)
72  +L1 = K.valo(one, ESC.ell())
73  +e = AD.adc_val(one, cp, ESC.ell(), zeros(), 0n, 1n, adc2())
74  +e1 = Equal.trans(Nat, Nat.add(K.valo(one, zeros()), LM.sh(cp, Nat.mul(one, 1n))), Nat.add(0n, LM.shn(32n, Nat.mul(one, 1n))), SC.T(one), M.cong_add(K.valo(one, zeros()), 0n, LM.sh(cp, Nat.mul(one, 1n)), LM.shn(32n, Nat.mul(one, 1n)), zero_vg(one, h1), LM.sh_okb(32n, cp, 255n, Nat.mul(one, 1n), cp_okb())), Equal.cong(Nat, Nat, z => LM.shn(32n, z), Nat.mul(one, 1n), one, NA.mul_one(one)))
75  +e2 = Equal.trans(Nat, Nat.add(Nat.add(C1, L1), Nat.mul(one, 0n)), Nat.add(Nat.add(C1, L1), 0n), Nat.add(C1, L1), M.cong_r(Nat.add(C1, L1), Nat.mul(one, 0n), 0n, NA.mul_zero(one)), N.add_zero(Nat.add(C1, L1)))
76  +e3 = M.cong_r(C1, 1n+mmL(one), L1, Equal.trans(Nat, 1n+mmL(one), SE.ell(one), L1, ell_eq(one, h1), Equal.sym(Nat, L1, SE.ell(one), ell_valo(one))))
77  Equal.trans(Nat, Nat.add(C1, 1n+mmL(one)), Nat.add(C1, L1), SC.T(one), e3, Equal.trans(Nat, Nat.add(C1, L1), Nat.add(Nat.add(C1, L1), Nat.mul(one, 0n)), SC.T(one), Equal.sym(Nat, Nat.add(Nat.add(C1, L1), Nat.mul(one, 0n)), Nat.add(C1, L1), e2), Equal.trans(Nat, Nat.add(Nat.add(C1, L1), Nat.mul(one, 0n)), Nat.add(K.valo(one, zeros()), LM.sh(cp, Nat.mul(one, 1n))), SC.T(one), e, e1)))
78
79# 2 L <= 2^256
80def h2L(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(1n+mmL(one), 1n+mmL(one)), SC.T(one)) == True{} : Bool}:
81  +l = K.valo(one, ESC.ell())
82  +d = K.valo(one, dlist())
83  +c = K.valo(one, ESC.comp_l())
84  +m = {1n+mmL(one) : Nat}
85  +e = AD.adc_val(one, ESC.ell(), dlist(), ESC.comp_l(), 0n, 0n, adc1())
86  +s0 = Equal.trans(Nat, LM.sh(ESC.ell(), Nat.mul(one, 0n)), LM.shn(32n, Nat.mul(one, 0n)), 0n, LM.sh_okb(32n, ESC.ell(), 255n, Nat.mul(one, 0n), {==}), Equal.cong(Nat, Nat, z => LM.shn(32n, z), Nat.mul(one, 0n), 0n, NA.mul_zero(one)))
87  +e1 = Equal.trans(Nat, Nat.add(l, d), Nat.add(Nat.add(l, d), Nat.mul(one, 0n)), c, Equal.trans(Nat, Nat.add(l, d), Nat.add(Nat.add(l, d), 0n), Nat.add(Nat.add(l, d), Nat.mul(one, 0n)), Equal.sym(Nat, Nat.add(Nat.add(l, d), 0n), Nat.add(l, d), N.add_zero(Nat.add(l, d))), M.cong_r(Nat.add(l, d), 0n, Nat.mul(one, 0n), Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)))), Equal.trans(Nat, Nat.add(Nat.add(l, d), Nat.mul(one, 0n)), Nat.add(c, LM.sh(ESC.ell(), Nat.mul(one, 0n))), c, e, Equal.trans(Nat, Nat.add(c, LM.sh(ESC.ell(), Nat.mul(one, 0n))), Nat.add(c, 0n), c, M.cong_r(c, LM.sh(ESC.ell(), Nat.mul(one, 0n)), 0n, s0), N.add_zero(c))))
88  +lm = Equal.trans(Nat, l, SE.ell(one), m, ell_valo(one), Equal.sym(Nat, m, SE.ell(one), ell_eq(one, h1)))
89  +e2 = Equal.trans(Nat, Nat.add(Nat.add(m, m), d), Nat.add(m, Nat.add(l, d)), SC.T(one), Equal.trans(Nat, Nat.add(Nat.add(m, m), d), Nat.add(m, Nat.add(m, d)), Nat.add(m, Nat.add(l, d)), NA.add_assoc(m, m, d), M.cong_r(m, Nat.add(m, d), Nat.add(l, d), M.cong_l(m, l, d, Equal.sym(Nat, l, m, lm)))), Equal.trans(Nat, Nat.add(m, Nat.add(l, d)), Nat.add(m, c), SC.T(one), M.cong_r(m, Nat.add(l, d), c, e1), Equal.trans(Nat, Nat.add(m, c), Nat.add(c, m), SC.T(one), NA.add_comm(m, c), hvL(one, h1))))
90  L.subst(Nat, z => {Nat.is_le(Nat.add(m, m), z) == True{} : Bool}, Nat.add(Nat.add(m, m), d), SC.T(one), e2, N.le_add_right(Nat.add(m, m), d))
91
92# ---- the clauses, for M = 1 + mmL ----
93
94def reduce_m(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {FS.value(ESC.reduce(bs)) == Nat.mod(FS.value(bs), 1n+mmL(one)) : Nat}:
95  +mm = mmL(one)
96  +n = X.bitlen(bs)
97  +V = FS.value(bs)
98  %Equal.sym(List<&2, U32>, ESC.mac(n, bs, F.one(), F.zero()), S2.macg(n, bs, F.one(), F.zero(), ESC.comp_l()), S2.mac_eq(n, bs, F.one(), F.zero())) : {FS.value(_) == Nat.mod(V, 1n+mm) : Nat}
99  +e = S2.mac_val(one, h1, mm, h2L(one, h1), ESC.comp_l(), cp_okb(), hvL(one, h1), n, bs, F.one(), F.zero(), hb, {==}, one_lt(one, h1), {==}, {==})
100  +e2 = Equal.trans(Nat, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, V), 1n)), Nat.add(0n, Nat.mul(C.low(n, V), 1n)), V, M.cong_l(WD.sc(n, 0n), 0n, Nat.mul(C.low(n, V), 1n), A.sc_zero(n)), Equal.trans(Nat, Nat.mul(C.low(n, V), 1n), C.low(n, V), V, NA.mul_one(C.low(n, V)), S2.low_all(bs, hb)))
101  Equal.trans(Nat, FS.value(S2.macg(n, bs, F.one(), F.zero(), ESC.comp_l())), Nat.mod(Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, V), 1n)), 1n+mm), Nat.mod(V, 1n+mm), e, M.cong_mod(1n+mm, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, V), 1n)), V, e2))
102
103def mul_add_m(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +s: List<&2, U32>, +r: List<&2, U32>, +hk: {LM.lea(k, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +hr: {LM.okb(32n, r, 255n) == True{} : Bool}, +ls: {Nat.is_lt(FS.value(s), 1n+mmL(one)) == True{} : Bool}, +lr: {Nat.is_lt(FS.value(r), 1n+mmL(one)) == True{} : Bool}) -> {FS.value(ESC.mul_add(k, s, r)) == Nat.mod(Nat.add(FS.value(r), Nat.mul(FS.value(k), FS.value(s))), 1n+mmL(one)) : Nat}:
104  +mm = mmL(one)
105  +P = {1n+mm : Nat}
106  +n = X.bitlen(k)
107  +K2 = FS.value(k)
108  +S = FS.value(s)
109  +R = FS.value(r)
110  +cp = ESC.comp_l()
111  +hv = hvL(one, h1)
112  +h2 = h2L(one, h1)
113  +mg = S2.macg(n, k, s, F.zero(), cp)
114  +om = S2.mac_okb(one, h1, mm, cp, cp_okb(), hv, n, k, s, F.zero(), hk, hs, {==})
115  +lm = S2.mac_below(one, h1, mm, h2, cp, cp_okb(), hv, n, k, s, F.zero(), hk, hs, ls, {==}, {==})
116  +em = S2.mac_val(one, h1, mm, h2, cp, cp_okb(), hv, n, k, s, F.zero(), hk, hs, ls, {==}, {==})
117  +em2 = Equal.trans(Nat, FS.value(mg), Nat.mod(Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, K2), S)), P), Nat.mod(Nat.mul(K2, S), P), em, M.cong_mod(P, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, K2), S)), Nat.mul(K2, S), Equal.trans(Nat, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, K2), S)), Nat.add(0n, Nat.mul(C.low(n, K2), S)), Nat.mul(K2, S), M.cong_l(WD.sc(n, 0n), 0n, Nat.mul(C.low(n, K2), S), A.sc_zero(n)), Equal.cong(Nat, Nat, z => Nat.mul(z, S), C.low(n, K2), K2, S2.low_all(k, hk)))))
118  %Equal.sym(List<&2, U32>, ESC.mac(n, k, s, F.zero()), mg, S2.mac_eq(n, k, s, F.zero())) : {FS.value(ESC.addm(_, r)) == Nat.mod(Nat.add(R, Nat.mul(K2, S)), P) : Nat}
119  +ea = SC.addg_val(one, h1, mm, h2, cp, cp_okb(), hv, mg, r, om, hr, lm, lr)
120  +eb = Equal.trans(Nat, Nat.mod(Nat.add(FS.value(mg), R), P), Nat.mod(Nat.add(Nat.mod(Nat.mul(K2, S), P), R), P), Nat.mod(Nat.add(R, Nat.mul(K2, S)), P), M.cong_mod(P, Nat.add(FS.value(mg), R), Nat.add(Nat.mod(Nat.mul(K2, S), P), R), M.cong_l(FS.value(mg), Nat.mod(Nat.mul(K2, S), P), R, em2)), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mod(Nat.mul(K2, S), P), R), P), Nat.mod(Nat.add(Nat.mul(K2, S), R), P), Nat.mod(Nat.add(R, Nat.mul(K2, S)), P), NR.mod_add_l(mm, Nat.mul(K2, S), R), M.cong_mod(P, Nat.add(Nat.mul(K2, S), R), Nat.add(R, Nat.mul(K2, S)), NA.add_comm(Nat.mul(K2, S), R))))
121  Equal.trans(Nat, FS.value(SC.addg(mg, r, cp)), Nat.mod(Nat.add(FS.value(mg), R), P), Nat.mod(Nat.add(R, Nat.mul(K2, S)), P), ea, eb)
122
123def mul_add_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +s: List<&2, U32>, +r: List<&2, U32>, +hk: {LM.lea(k, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +hr: {LM.okb(32n, r, 255n) == True{} : Bool}, +ls: {Nat.is_lt(FS.value(s), 1n+mmL(one)) == True{} : Bool}, +lr: {Nat.is_lt(FS.value(r), 1n+mmL(one)) == True{} : Bool}) -> {LM.okb(32n, ESC.mul_add(k, s, r), 255n) == True{} : Bool}:
124  +mm = mmL(one)
125  +cp = ESC.comp_l()
126  +n = X.bitlen(k)
127  +mg = S2.macg(n, k, s, F.zero(), cp)
128  %Equal.sym(List<&2, U32>, ESC.mac(n, k, s, F.zero()), mg, S2.mac_eq(n, k, s, F.zero())) : {LM.okb(32n, ESC.addm(_, r), 255n) == True{} : Bool}
129  SC.addg_okb(one, h1, mm, cp, cp_okb(), hvL(one, h1), mg, r, S2.mac_okb(one, h1, mm, cp, cp_okb(), hvL(one, h1), n, k, s, F.zero(), hk, hs, {==}), hr)
130
131def reduce_okb(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {LM.okb(32n, ESC.reduce(bs), 255n) == True{} : Bool}:
132  %Equal.sym(List<&2, U32>, ESC.mac(X.bitlen(bs), bs, F.one(), F.zero()), S2.macg(X.bitlen(bs), bs, F.one(), F.zero(), ESC.comp_l()), S2.mac_eq(X.bitlen(bs), bs, F.one(), F.zero())) : {LM.okb(32n, _, 255n) == True{} : Bool}
133  S2.mac_okb(one, h1, mmL(one), ESC.comp_l(), cp_okb(), hvL(one, h1), X.bitlen(bs), bs, F.one(), F.zero(), hb, {==}, {==})
134
135def lt_l_m(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {ESC.lt_l(x) == Nat.is_lt(FS.value(x), 1n+mmL(one)) : Bool}:
136  SC.lt_by(one, h1, mmL(one), x, ESC.comp_l(), hx, cp_okb(), hvL(one, h1), Nat.is_lt(v(LM.cc(F.carry(F.addl(x, ESC.comp_l()), 0))), one), {==})