proofs/crypto/curve25519/consts.bend

bend-collections-laws-crypto@1.0.0.0 · 128 lines · 12 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/math/natural/arith.bend as NR
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL
14
15# Constant limb lists. The checker keeps closed naturals in unary, so the
16# value of a constant such as 8p is never formed: every constant is read
17# through valo(one, xs) = one * value(xs), which stays open in the symbolic
18# one, and the carries of its digits are proved once, symbolically.
19
20def v(+x: U32) -> Nat:
21  U32.to_nat(x)
22
23# the value of xs times one, digit by digit
24def valo(+one: Nat, xs: List<&2, U32>) -> Nat:
25  match xs:
26    case Nil{}:
27      0n
28    case Con{h, t}:
29      Nat.add(Nat.mul(one, U32.to_nat(h)), C.shift(8n, valo(one, t)))
30
31def valo_value(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>) -> {valo(one, xs) == FS.value(xs) : Nat}:
32  match xs:
33    case Nil{}:
34      {==}
35    case Con{+h, +t}:
36      +e0 = L.subst(Nat, o => {Nat.mul(o, v(h)) == v(h) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), AR.one_mul(v(h)))
37      M.cong_add(Nat.mul(one, v(h)), v(h), C.shift(8n, valo(one, t)), C.shift(8n, FS.value(t)), e0, M.cong_sc(8n, valo(one, t), FS.value(t), valo_value(one, h1, t)))
38
39# n copies of k, then tl
40def rep(n: Nat, +k: U32, tl: List<&2, U32>) -> List<&2, U32>:
41  match n:
42    case 0n:
43      tl
44    case 1n+m:
45      Con{k, rep(m, k, tl)}
46
47# a run of 2040 = 8 * 255 absorbs a carry of 8
48def run8(+one: Nat, +n: Nat, +tl: List<&2, U32>) -> {Nat.add(valo(one, rep(n, 2040, tl)), Nat.mul(one, 8n)) == LM.shn(n, Nat.add(valo(one, tl), Nat.mul(one, 8n))) : Nat}:
49  match n:
50    case 0n:
51      {==}
52    case 1n+ +m:
53      +R = valo(one, rep(m, 2040, tl))
54      +a = Nat.mul(one, v(2040))
55      +b = Nat.mul(one, 8n)
56      +k1 = Equal.trans(Nat, Nat.add(a, b), Nat.mul(one, Nat.add(v(2040), 8n)), Nat.mul(one, WD.sc(8n, 8n)), Equal.sym(Nat, Nat.mul(one, Nat.add(v(2040), 8n)), Nat.add(a, b), NA.mul_add_left(one, v(2040), 8n)), Equal.cong(Nat, Nat, t => Nat.mul(one, t), Nat.add(v(2040), 8n), WD.sc(8n, 8n), {==}))
57      +k2 = Equal.trans(Nat, Nat.add(a, b), Nat.mul(one, WD.sc(8n, 8n)), WD.sc(8n, b), k1, Equal.sym(Nat, WD.sc(8n, b), Nat.mul(one, WD.sc(8n, 8n)), PL.sc_mul_l(8n, one, 8n)))
58      +e1 = Equal.trans(Nat, Nat.add(Nat.add(a, C.shift(8n, R)), b), Nat.add(a, Nat.add(C.shift(8n, R), b)), Nat.add(Nat.add(a, b), C.shift(8n, R)), NA.add_assoc(a, C.shift(8n, R), b),
59        Equal.trans(Nat, Nat.add(a, Nat.add(C.shift(8n, R), b)), Nat.add(a, Nat.add(b, C.shift(8n, R))), Nat.add(Nat.add(a, b), C.shift(8n, R)), M.cong_r(a, Nat.add(C.shift(8n, R), b), Nat.add(b, C.shift(8n, R)), NA.add_comm(C.shift(8n, R), b)), Equal.sym(Nat, Nat.add(Nat.add(a, b), C.shift(8n, R)), Nat.add(a, Nat.add(b, C.shift(8n, R))), NA.add_assoc(a, b, C.shift(8n, R)))))
60      +e2 = M.cong_l(Nat.add(a, b), WD.sc(8n, b), C.shift(8n, R), k2)
61      +e3 = Equal.trans(Nat, Nat.add(WD.sc(8n, b), C.shift(8n, R)), WD.sc(8n, Nat.add(b, R)), WD.sc(8n, Nat.add(R, b)), M.sc_add(8n, b, R), M.cong_sc(8n, Nat.add(b, R), Nat.add(R, b), NA.add_comm(b, R)))
62      +e4 = M.cong_sc(8n, Nat.add(R, b), LM.shn(m, Nat.add(valo(one, tl), b)), run8(one, m, tl))
63      Equal.trans(Nat, Nat.add(Nat.add(a, C.shift(8n, R)), b), Nat.add(Nat.add(a, b), C.shift(8n, R)), C.shift(8n, LM.shn(m, Nat.add(valo(one, tl), b))), e1,
64        Equal.trans(Nat, Nat.add(Nat.add(a, b), C.shift(8n, R)), Nat.add(WD.sc(8n, b), C.shift(8n, R)), C.shift(8n, LM.shn(m, Nat.add(valo(one, tl), b))), e2,
65          Equal.trans(Nat, Nat.add(WD.sc(8n, b), C.shift(8n, R)), WD.sc(8n, Nat.add(R, b)), C.shift(8n, LM.shn(m, Nat.add(valo(one, tl), b))), e3, e4)))
66
67# a run of zeros shifts
68def run0(+one: Nat, +n: Nat, +tl: List<&2, U32>) -> {valo(one, rep(n, 0, tl)) == LM.shn(n, valo(one, tl)) : Nat}:
69  match n:
70    case 0n:
71      {==}
72    case 1n+ +m:
73      +R = valo(one, rep(m, 0, tl))
74      +e1 = M.cong_l(Nat.mul(one, 0n), 0n, C.shift(8n, R), NA.mul_zero(one))
75      Equal.trans(Nat, Nat.add(Nat.mul(one, 0n), C.shift(8n, R)), C.shift(8n, R), C.shift(8n, LM.shn(m, valo(one, tl))), e1, M.cong_sc(8n, R, LM.shn(m, valo(one, tl)), run0(one, m, tl)))
76
77def one_k(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.mul(one, k) == k : Nat}:
78  L.subst(Nat, o => {Nat.mul(o, k) == k : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), AR.one_mul(k))
79
80# 2^258 == 8 p + 152
81def s258(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {WD.sc(258n, one) == Nat.add(Nat.mul(8n, 1n+pp), 152n) : Nat}:
82  +X = WD.sc(255n, one)
83  +P = {1n+pp : Nat}
84  +e1 = Equal.trans(Nat, WD.sc(3n, X), Nat.mul(X, 8n), Nat.mul(8n, X), Equal.sym(Nat, Nat.mul(X, 8n), WD.sc(3n, X), AR.mul_sc(3n, X)), NA.mul_comm(X, 8n))
85  +e2 = Equal.cong(Nat, Nat, t => Nat.mul(8n, t), X, Nat.add(P, 19n), Equal.sym(Nat, Nat.add(P, 19n), X, hP))
86  +e3 = NA.mul_add_left(8n, P, 19n)
87  Equal.trans(Nat, WD.sc(3n, X), Nat.mul(8n, X), Nat.add(Nat.mul(8n, P), 152n), e1, Equal.trans(Nat, Nat.mul(8n, X), Nat.mul(8n, Nat.add(P, 19n)), Nat.add(Nat.mul(8n, P), 152n), e2, e3))
88
89def eight_p_shape() -> {F.eight_p() == Con{1896, rep(30n, 2040, Con{1016, Nil{}})} : List<&2, U32>}:
90  {==}
91
92# value(8p limbs) == 8 p
93def eight_p_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {valo(one, F.eight_p()) == Nat.mul(8n, 1n+pp) : Nat}:
94  %Equal.sym(List<&2, U32>, F.eight_p(), Con{1896, rep(30n, 2040, Con{1016, Nil{}})}, eight_p_shape()) : {valo(one, _) == Nat.mul(8n, 1n+pp) : Nat}
95  +R = valo(one, rep(30n, 2040, Con{1016, Nil{}}))
96  +a = Nat.mul(one, v(1896))
97  +b = Nat.mul(one, 152n)
98  +c8 = Nat.mul(one, 8n)
99  +t = Nat.add(valo(one, Con{1016, Nil{}}), c8)
100  +k1 = Equal.trans(Nat, Nat.add(a, b), Nat.mul(one, Nat.add(v(1896), 152n)), Nat.mul(one, WD.sc(8n, 8n)), Equal.sym(Nat, Nat.mul(one, Nat.add(v(1896), 152n)), Nat.add(a, b), NA.mul_add_left(one, v(1896), 152n)), Equal.cong(Nat, Nat, z => Nat.mul(one, z), Nat.add(v(1896), 152n), WD.sc(8n, 8n), {==}))
101  +k2 = Equal.trans(Nat, Nat.add(a, b), Nat.mul(one, WD.sc(8n, 8n)), WD.sc(8n, c8), k1, Equal.sym(Nat, WD.sc(8n, c8), Nat.mul(one, WD.sc(8n, 8n)), PL.sc_mul_l(8n, one, 8n)))
102  +e1 = Equal.trans(Nat, Nat.add(Nat.add(a, C.shift(8n, R)), b), Nat.add(a, Nat.add(C.shift(8n, R), b)), Nat.add(Nat.add(a, b), C.shift(8n, R)), NA.add_assoc(a, C.shift(8n, R), b),
103    Equal.trans(Nat, Nat.add(a, Nat.add(C.shift(8n, R), b)), Nat.add(a, Nat.add(b, C.shift(8n, R))), Nat.add(Nat.add(a, b), C.shift(8n, R)), M.cong_r(a, Nat.add(C.shift(8n, R), b), Nat.add(b, C.shift(8n, R)), NA.add_comm(C.shift(8n, R), b)), Equal.sym(Nat, Nat.add(Nat.add(a, b), C.shift(8n, R)), Nat.add(a, Nat.add(b, C.shift(8n, R))), NA.add_assoc(a, b, C.shift(8n, R)))))
104  +e2 = M.cong_l(Nat.add(a, b), WD.sc(8n, c8), C.shift(8n, R), k2)
105  +e3 = Equal.trans(Nat, Nat.add(WD.sc(8n, c8), C.shift(8n, R)), WD.sc(8n, Nat.add(c8, R)), WD.sc(8n, Nat.add(R, c8)), M.sc_add(8n, c8, R), M.cong_sc(8n, Nat.add(c8, R), Nat.add(R, c8), NA.add_comm(c8, R)))
106  +e4 = M.cong_sc(8n, Nat.add(R, c8), LM.shn(30n, t), run8(one, 30n, Con{1016, Nil{}}))
107  +k3 = Equal.trans(Nat, t, Nat.add(Nat.mul(one, v(1016)), c8), Nat.mul(one, Nat.add(v(1016), 8n)), M.cong_l(valo(one, Con{1016, Nil{}}), Nat.mul(one, v(1016)), c8, N.add_zero(Nat.mul(one, v(1016)))), Equal.sym(Nat, Nat.mul(one, Nat.add(v(1016), 8n)), Nat.add(Nat.mul(one, v(1016)), c8), NA.mul_add_left(one, v(1016), 8n)))
108  +k4 = L.subst(Nat, o => {Nat.mul(o, Nat.add(v(1016), 8n)) == WD.sc(10n, o) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
109  +e5 = M.cong_sc(8n, LM.shn(30n, t), LM.shn(30n, WD.sc(10n, one)), Equal.cong(Nat, Nat, z => LM.shn(30n, z), t, WD.sc(10n, one), Equal.trans(Nat, t, Nat.mul(one, Nat.add(v(1016), 8n)), WD.sc(10n, one), k3, k4)))
110  +tot = Equal.trans(Nat, Nat.add(Nat.add(a, C.shift(8n, R)), b), Nat.add(Nat.add(a, b), C.shift(8n, R)), WD.sc(258n, one), e1,
111    Equal.trans(Nat, Nat.add(Nat.add(a, b), C.shift(8n, R)), Nat.add(WD.sc(8n, c8), C.shift(8n, R)), WD.sc(258n, one), e2,
112      Equal.trans(Nat, Nat.add(WD.sc(8n, c8), C.shift(8n, R)), WD.sc(8n, Nat.add(R, c8)), WD.sc(258n, one), e3,
113        Equal.trans(Nat, WD.sc(8n, Nat.add(R, c8)), C.shift(8n, LM.shn(30n, t)), WD.sc(258n, one), e4, e5))))
114  +V = valo(one, Con{1896, rep(30n, 2040, Con{1016, Nil{}})})
115  +tot2 = Equal.trans(Nat, Nat.add(V, 152n), Nat.add(V, b), Nat.add(Nat.mul(8n, 1n+pp), 152n), M.cong_r(V, 152n, b, Equal.sym(Nat, b, 152n, one_k(one, h1, 152n))), Equal.trans(Nat, Nat.add(V, b), WD.sc(258n, one), Nat.add(Nat.mul(8n, 1n+pp), 152n), tot, s258(one, h1, pp, hP)))
116  +tot3 = Equal.trans(Nat, Nat.add(152n, V), Nat.add(V, 152n), Nat.add(152n, Nat.mul(8n, 1n+pp)), NA.add_comm(152n, V), Equal.trans(Nat, Nat.add(V, 152n), Nat.add(Nat.mul(8n, 1n+pp), 152n), Nat.add(152n, Nat.mul(8n, 1n+pp)), tot2, NA.add_comm(Nat.mul(8n, 1n+pp), 152n)))
117  NR.add_cancel(152n, V, Nat.mul(8n, 1n+pp), tot3)
118
119# valo guarded on one: kept folded by the checker (see FS.gdigits)
120def vg(+one: Nat, xs: List<&2, U32>) -> Nat:
121  match one:
122    case 0n:
123      0n
124    case 1n+z:
125      valo(1n+z, xs)
126
127def vg_valo(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>) -> {vg(one, xs) == valo(one, xs) : Nat}:
128  L.subst(Nat, o => {vg(o, xs) == valo(o, xs) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})