def Hex.Nat.oddSplitAux : Nat → Nat → Nat × Nat

Split off the factors of two: oddSplitAux fuel m = (s, d) with m = 2 ^ s * d and d odd, provided the fuel bounds the number of factors of two.

Equations

• Hex.Nat.oddSplitAux 0 x✝ = (0, x✝)
• Hex.Nat.oddSplitAux fuel.succ x✝ = if x✝ % 2 = 0 ∧ x✝ ≠ 0 then have sd := Hex.Nat.oddSplitAux fuel (x✝ / 2); (sd.fst + 1, sd.snd) else (0, x✝)

def Hex.Nat.oddSplit (m : Nat) : Nat × Nat

Split m as 2 ^ s * d with d odd, returning (s, d); oddSplit 0 = (0, 0).

Equations

• Hex.Nat.oddSplit m = Hex.Nat.oddSplitAux (m.log2 + 1) m

theorem Hex.Nat.oddSplit_spec (m : Nat) (hm : m ≠ 0) : 2 ^ (oddSplit m).fst * (oddSplit m).snd = m ∧ (oddSplit m).snd % 2 = 1

Correctness of the split: for m ≠ 0, m = 2 ^ s * d with d odd.

def Hex.Nat.mrWitnessLoop (n : Nat) : Nat → Nat → Bool

The squaring loop of the strong test: starting from x = a ^ (2 ^ 1 * d) % n, true iff some square in the next i steps hits n - 1.

Equations

• Hex.Nat.mrWitnessLoop n x✝ 0 = false
• Hex.Nat.mrWitnessLoop n x✝ i.succ = if x✝ = n - 1 then true else Hex.Nat.mrWitnessLoop n (x✝ * x✝ % n) i

def Hex.Nat.mrStrongTestCore (n s x : Nat) : Bool

Core of the strong test on the residue x = a ^ d % n, with n - 1 = 2 ^ s * d.

Equations

• Hex.Nat.mrStrongTestCore n s x = if x = 1 ∨ x = n - 1 then true else Hex.Nat.mrWitnessLoop n (x * x % n) (s - 1)

def Hex.Nat.millerRabin (n a : Nat) : Bool

The Miller-Rabin test at base a. false is a proof of compositeness; true is evidence and nothing more. The branch list is part of the specification: in particular the a % n = 0 branch returns true (inconclusive; such a base carries no information), which is what makes the compositeness theorem true at small n.

Equations

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

def Hex.Nat.defaultBases : List Nat

The first 13 primes: sufficient witnesses for n < 3.3 · 10^24 by Sorenson-Webster, a fact used only to decide what to try and never in a proof.

Equations

• Hex.Nat.defaultBases = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41]

def Hex.Nat.isProbablePrime (n : Nat) (bases : List Nat := defaultBases) : Bool

Run millerRabin over a base list. true proves nothing about n; it is consumed only as a filter ahead of certificate construction.

Equations

• Hex.Nat.isProbablePrime n bases = bases.all (Hex.Nat.millerRabin n)

theorem Hex.Nat.millerRabin_eq_true_of_prime {n a : Nat} (hp : Prime n) : millerRabin n a = true

A prime passes the Miller-Rabin test at every base: the contrapositive of the compositeness theorem, proved branch by branch.

theorem Hex.Nat.not_prime_of_millerRabin_false {n a : Nat} (h : millerRabin n a = false) : ¬Prime n

A Miller-Rabin witness proves compositeness. This is the theorem the whole test exists for; there is deliberately no converse.