Pratt/Lucas prime certificates over fast modular exponentiation

A reusable core for proving Nat.Prime p for large p via the Lucas primality criterion, using a binary (square-and-multiply) modular exponentiation whose result is checkable by kernel decide at cryptographic sizes.

The ZMod p power a ^ (p - 1) is unary npowRec, so it is not directly evaluable for a 256-bit p. powMod computes a ^ k % n in O(log k) multiplications, and powMod_cast transports a fast powMod … = 1 check into the a ^ (p - 1) = 1 hypothesis of lucas_primality.

Main definitions

• powMod a k n — binary modular exponentiation returning a ^ k % n.
• Cert — a Pratt certificate tree; Cert.check — its Boolean checker.
• pratt_prime c — tactic closing Nat.Prime p from an inline certificate c.

Main results

• powMod_eq — powMod a k n = a ^ k % n for 0 < n.
• powMod_cast — ((powMod a k n : ℕ) : ZMod n) = (a : ZMod n) ^ k.
• lucas_of_cover — Nat.Prime p from a witness a, a list qs containing every prime factor of p - 1, and fast powMod checks.
• lucas_of_certificate — the same from a list qs of prime factors with product p - 1.
• Cert.sound — c.check = true → Nat.Prime c.prime.

def CatCrypt.PrattCertificate.powModGo (m : ℕ) : ℕ → ℕ → ℕ → ℕ → ℕ

Square-and-multiply worker for modular exponentiation. fuel bounds the number of squarings; base is the running square, e the remaining exponent bits, and acc the accumulated product, all kept reduced % m. The e = 0 guard halts the loop, so the recursion depth is the bit length of the initial exponent.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.PrattCertificate.powModGo m 0 x✝² x✝¹ x✝ = x✝

def CatCrypt.PrattCertificate.powMod (a k n : ℕ) : ℕ

Binary (square-and-multiply) modular exponentiation: powMod a k n = a ^ k % n (for 0 < n), computed in O(log k) multiplications. The worker powModGo is tail-recursive with fuel k, so kernel decide reduces a fully applied powMod in O(log k) GMP Nat steps at cryptographic sizes without a Lean.ofReduceBool axiom.

Equations

• CatCrypt.PrattCertificate.powMod a k n = CatCrypt.PrattCertificate.powModGo n k (a % n) k (1 % n)

theorem CatCrypt.PrattCertificate.powModGo_cast (m fuel base e acc : ℕ) : e < 2 ^ fuel → ↑(powModGo m fuel base e acc) = ↑acc * ↑base ^ e

The worker invariant: cast into ZMod m, powModGo computes acc * base ^ e, provided the fuel covers the exponent (e < 2 ^ fuel).

theorem CatCrypt.PrattCertificate.powModGo_lt (m : ℕ) (hm : 0 < m) (fuel base e acc : ℕ) : acc < m → powModGo m fuel base e acc < m

The worker stays inside [0, m) when started from a reduced accumulator.

theorem CatCrypt.PrattCertificate.powMod_lt (a k n : ℕ) (hn : 0 < n) : powMod a k n < n

The output is a residue: powMod a k n < n for 0 < n.

theorem CatCrypt.PrattCertificate.powMod_cast (a k n : ℕ) [NeZero n] : ↑(powMod a k n) = ↑a ^ k

The fast powMod result cast into ZMod n equals the abstract power there, so a powMod … = 1 check discharges an a ^ k = 1 hypothesis over ZMod n.

theorem CatCrypt.PrattCertificate.powMod_eq (a k n : ℕ) (hn : 0 < n) : powMod a k n = a ^ k % n

Correctness of binary modular exponentiation.

theorem CatCrypt.PrattCertificate.prime_mem_of_dvd_listProd {q : ℕ} (hq : Nat.Prime q) (l : List ℕ) : (∀ r ∈ l, Nat.Prime r) → q ∣ l.prod → q ∈ l

A prime dividing the product of a list of primes is a member of the list.

theorem CatCrypt.PrattCertificate.lucas_of_cover (p : ℕ) (hp1 : 1 < p) (a : ℕ) (qs : List ℕ) (hcover : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → q ∈ qs) (hfermat : powMod a (p - 1) p = 1) (hwit : ∀ q ∈ qs, powMod a ((p - 1) / q) p ≠ 1) : Nat.Prime p

Lucas primality from a covering list of prime factors. Given a witness a, a list qs containing every prime factor of p - 1, the Fermat check powMod a (p - 1) p = 1, and for each q ∈ qs the check powMod a ((p - 1) / q) p ≠ 1, conclude Nat.Prime p.

theorem CatCrypt.PrattCertificate.lucas_of_certificate (p : ℕ) (hp1 : 1 < p) (a : ℕ) (qs : List ℕ) (hprod : qs.prod = p - 1) (hqs_prime : ∀ q ∈ qs, Nat.Prime q) (hfermat : powMod a (p - 1) p = 1) (hwit : ∀ q ∈ qs, powMod a ((p - 1) / q) p ≠ 1) : Nat.Prime p

Lucas primality via a certificate. Given a witness a, a list qs of the prime factors of p - 1 whose product is p - 1, the Fermat check powMod a (p - 1) p = 1, and for each factor q the check powMod a ((p - 1) / q) p ≠ 1, conclude Nat.Prime p.

theorem CatCrypt.PrattCertificate.prime_65537 : Nat.Prime 65537

The Fermat prime 2 ^ 16 + 1 = 65537, proved via lucas_of_certificate. Its p - 1 = 2 ^ 16 has the single prime factor 2; 3 is a witness.

Reflective Pratt certificates

A Cert is a Pratt certificate tree. Cert.check is a Boolean checker that reduces in the kernel by GMP-accelerated Nat arithmetic, and Cert.sound turns c.check = true into Nat.Prime c.prime. The tactic pratt_prime c closes a goal Nat.Prime p from an inline certificate c by kernel decide.

def CatCrypt.PrattCertificate.stripFactor (q : ℕ) : ℕ → ℕ → ℕ

stripFactor q fuel n divides n by q as long as q > 1 divides it, at most fuel times.

Equations

• CatCrypt.PrattCertificate.stripFactor q 0 x✝ = x✝
• CatCrypt.PrattCertificate.stripFactor q fuel.succ x✝ = if (decide (1 < q) && x✝ % q == 0 && x✝ != 0) = true then CatCrypt.PrattCertificate.stripFactor q fuel (x✝ / q) else x✝

theorem CatCrypt.PrattCertificate.stripFactor_spec (q fuel n : ℕ) : ∃ (k : ℕ), n = stripFactor q fuel n * q ^ k

stripFactor removes a power of q: n = stripFactor q fuel n * q ^ k.

def CatCrypt.PrattCertificate.stripAll (n : ℕ) : List ℕ → ℕ

stripAll n qs removes every power of every q ∈ qs from n.

Equations

• CatCrypt.PrattCertificate.stripAll n [] = n
• CatCrypt.PrattCertificate.stripAll n (q :: qs) = CatCrypt.PrattCertificate.stripAll (CatCrypt.PrattCertificate.stripFactor q n n) qs

theorem CatCrypt.PrattCertificate.dvd_mem_of_stripAll_eq_one {r : ℕ} (hr : Nat.Prime r) (qs : List ℕ) (n : ℕ) : stripAll n qs = 1 → r ∣ n → ∃ q ∈ qs, r ∣ q

If stripAll n qs = 1, every prime factor of n divides some q ∈ qs.

def CatCrypt.PrattCertificate.trialGo (q : ℕ) : ℕ → ℕ → Bool

Trial division loop: trialGo q fuel d is true when no m with d ≤ m and m * m ≤ q divides q, inspected for at most fuel candidates.

Equations

• CatCrypt.PrattCertificate.trialGo q 0 x✝ = false
• CatCrypt.PrattCertificate.trialGo q fuel.succ x✝ = if q < x✝ * x✝ then true else if (q % x✝ == 0) = true then false else CatCrypt.PrattCertificate.trialGo q fuel (x✝ + 1)

theorem CatCrypt.PrattCertificate.trialGo_spec (q fuel d : ℕ) : trialGo q fuel d = true → ∀ (m : ℕ), d ≤ m → m * m ≤ q → ¬m ∣ q

Soundness of trialGo.

def CatCrypt.PrattCertificate.trialPrime (q : ℕ) : Bool

Primality by trial division up to √q.

Equations

• CatCrypt.PrattCertificate.trialPrime q = (decide (2 ≤ q) && CatCrypt.PrattCertificate.trialGo q q 2)

theorem CatCrypt.PrattCertificate.trialPrime_sound (q : ℕ) (h : trialPrime q = true) : Nat.Prime q

Soundness of trialPrime.

inductive CatCrypt.PrattCertificate.Cert : Type

A Pratt certificate tree. small p is checked by trial division; node p a fs is a Lucas certificate for p with witness a whose list fs certifies the distinct prime factors of p - 1. A numeral n denotes small n.

• small (p : ℕ) : Cert
• node (p a : ℕ) (fs : List Cert) : Cert

@[instance_reducible]

instance CatCrypt.PrattCertificate.instOfNatCert (n : ℕ) : OfNat Cert n

Equations

• CatCrypt.PrattCertificate.instOfNatCert n = { ofNat := CatCrypt.PrattCertificate.Cert.small n }

def CatCrypt.PrattCertificate.Cert.prime : Cert → ℕ

The prime a certificate is about.

Equations

• (CatCrypt.PrattCertificate.Cert.small p).prime = p
• (CatCrypt.PrattCertificate.Cert.node p a fs).prime = p

def CatCrypt.PrattCertificate.nodeOk (p a : ℕ) (qs : List ℕ) : Bool

The local Lucas checks of one node: 1 < p, the Fermat check, the factors qs cover p - 1 (stripping them leaves 1), and the witness checks.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.PrattCertificate.prime_of_nodeOk (p a : ℕ) (qs : List ℕ) (hqs : ∀ q ∈ qs, Nat.Prime q) (h : nodeOk p a qs = true) : Nat.Prime p

nodeOk and primality of the factors give primality of p.

def CatCrypt.PrattCertificate.Cert.check : Cert → Bool

The Boolean checker of a Pratt certificate tree.

Equations

• (CatCrypt.PrattCertificate.Cert.small p).check = CatCrypt.PrattCertificate.trialPrime p
• (CatCrypt.PrattCertificate.Cert.node p a fs).check = (CatCrypt.PrattCertificate.nodeOk p a (List.map CatCrypt.PrattCertificate.Cert.prime fs) && CatCrypt.PrattCertificate.Cert.checkAll fs)

def CatCrypt.PrattCertificate.Cert.checkAll : List Cert → Bool

Cert.check on every certificate of a list.

Equations

• CatCrypt.PrattCertificate.Cert.checkAll [] = true
• CatCrypt.PrattCertificate.Cert.checkAll (c :: cs) = (c.check && CatCrypt.PrattCertificate.Cert.checkAll cs)

theorem CatCrypt.PrattCertificate.Cert.sound (c : Cert) : c.check = true → Nat.Prime c.prime

Soundness of Cert.check.

theorem CatCrypt.PrattCertificate.Cert.sound_all (cs : List Cert) : checkAll cs = true → ∀ c ∈ cs, Nat.Prime c.prime

Soundness of Cert.checkAll.

def CatCrypt.PrattCertificate.tacticPratt_prime_ : Lean.ParserDescr

pratt_prime c closes a goal Nat.Prime p from a Pratt certificate tree c with c.prime = p, checking c.check = true by kernel reduction.

Equations

• One or more equations did not get rendered due to their size.