Primality certificates

Elligator 1 is instantiated over concrete finite fields whose cardinality is a large prime, for instance q = 2^251 - 9 for Curve1174 (see [bernstein2013a], Section 4). Such a primality statement is far out of reach for the decision procedures that evaluate a Nat.Prime goal by trial division, so this file provides the infrastructure needed to check a Pratt certificate inside Lean.

Two ingredients are required:

• powMod, a binary modular exponentiation that the kernel can evaluate on numerals of several hundred bits, together with its correctness statement powMod_eq.
• prime_of_pratt, a repackaging of Mathlib's lucas_primality in which the prime divisors of p - 1 are supplied as an explicit list and all modular exponentiations are phrased through powMod, so that every side condition of the certificate is closed by decide.

Main results

• powMod_eq: powMod m f b e = b ^ e % m whenever the fuel bounds the bit length of the exponent, i.e. e < 2 ^ f.
• prime_of_pratt: the Pratt/Lucas primality criterion in a form suited to kernel evaluation.

def Elligator.PrimalityCertificate.powMod (m : ℕ) : ℕ → ℕ → ℕ → ℕ

powMod m f b e computes b ^ e % m by binary exponentiation, with fuel parameter that has to bound the bit length of e; see powMod_eq.

Unlike b ^ e % m this is evaluated by the kernel in time linear in f, which makes it usable inside decide for exponents with hundreds of bits.

Equations

• One or more equations did not get rendered due to their size.
• Elligator.PrimalityCertificate.powMod m 0 x✝¹ x✝ = 1 % m

theorem Elligator.PrimalityCertificate.powMod_eq (m fuel b e : ℕ) : e < 2 ^ fuel → powMod m fuel b e = b ^ e % m

Correctness of binary modular exponentiation: as soon as the fuel bounds the bit length of the exponent, powMod computes the modular power.

theorem Elligator.PrimalityCertificate.natCast_pow_eq_natCast {m : ℕ} (a e b fuel : ℕ) (hfuel : e < 2 ^ fuel) (h : powMod m fuel a e = b % m) : ↑a ^ e = ↑b

Modular powers inside ZMod m computed through powMod: if the binary exponentiation of a^e modulo m returns b % m, then (a : ZMod m)^e = b. This transports a kernel computation with numerals into an equation between residues.

theorem Elligator.PrimalityCertificate.prime_of_pratt {p : ℕ} (a fuel : ℕ) (L : List ℕ) (hfuel : p - 1 < 2 ^ fuel) (hL : ∀ r ∈ L, Nat.Prime r) (hprod : p - 1 = L.prod) (ha : powMod p fuel a (p - 1) = 1 % p) (hchk : ∀ r ∈ L, powMod p fuel a ((p - 1) / r) ≠ 1 % p) : Nat.Prime p

The Pratt (Lucas) primality criterion, phrased for kernel evaluation.

If L is a list of primes whose product is p - 1 and if the base a has order exactly p - 1 modulo p, witnessed by a^(p - 1) ≡ 1 and a^((p - 1) / r) ≢ 1 for every r ∈ L, then p is prime. All modular powers are written through powMod, so the hypotheses are decidable by computation once p, a, F and L are numerals.