proofs/crypto/curve25519/prime.bend

bend-collections-laws-crypto@1.0.0.0 · 32 lines · 5 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/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/word.bend as WD
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
9
10# p = FS.prime(one) = 2^255 - 19 as 1 + pp, the form of the modular lemmas
11# (proofs/math/natural/arith.bend), with (1 + pp) + 19 == 2^255.
12
13def pp_of(+one: Nat) -> Nat:
14  Nat.sub(C.shift(255n, one), 20n)
15
16def p20(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(20n, WD.sc(255n, one)) == True{} : Bool}:
17  +a = L.subst(Nat, o => {Nat.is_le(20n, WD.sc(5n, o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
18  N.le_trans(20n, WD.sc(5n, one), WD.sc(255n, one), a, M.sc_mono(250n, 5n, one))
19
20# 20 + pp == 2^255
21def pp_sum(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(20n, pp_of(one)) == WD.sc(255n, one) : Nat}:
22  N.sub_add(WD.sc(255n, one), 20n, p20(one, h1))
23
24def hP(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(1n+pp_of(one), 19n) == WD.sc(255n, one) : Nat}:
25  +pp = pp_of(one)
26  +e = Equal.cong(Nat, Nat, t => 1n+t, Nat.add(pp, 19n), Nat.add(19n, pp), NA.add_comm(pp, 19n))
27  Equal.trans(Nat, Nat.add(1n+pp, 19n), Nat.add(20n, pp), WD.sc(255n, one), e, pp_sum(one, h1))
28
29def prime_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.prime(one) == 1n+pp_of(one) : Nat}:
30  +pp = pp_of(one)
31  +e = Equal.cong(Nat, Nat, t => Nat.sub(t, 19n), WD.sc(255n, one), Nat.add(20n, pp), Equal.sym(Nat, Nat.add(20n, pp), WD.sc(255n, one), pp_sum(one, h1)))
32  Equal.trans(Nat, Nat.sub(WD.sc(255n, one), 19n), Nat.sub(Nat.add(20n, pp), 19n), 1n+pp, e, N.add_sub_cancel(19n, 1n+pp))