From eedbf6860b8b3a5e975a44d2a8e8c68dcfa99661 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 30 Aug 2026 16:16:53 +0000 Subject: [PATCH 1/2] fix(hex-primality): preserve next-prime work accounting --- HexPrimality/SPEC/hex-primality.md | 17 +++++++++--- HexPrimality/Search.lean | 22 ++++++++++------ conformance/HexPrimality/Conformance.lean | 32 ++++++++++++++++++++--- 3 files changed, 55 insertions(+), 16 deletions(-) diff --git a/HexPrimality/SPEC/hex-primality.md b/HexPrimality/SPEC/hex-primality.md index c9bca7a9b..6e4d5a7aa 100644 --- a/HexPrimality/SPEC/hex-primality.md +++ b/HexPrimality/SPEC/hex-primality.md @@ -777,8 +777,9 @@ structure PrimeDecisionFailure where rand : Rand structure NextPrimeFailure where - attempts : Nat - rand : Rand + rejectedCandidates : Nat + certAttempts : Nat + rand : Rand def defaultPrimeFuel (n : Nat) : Nat @@ -878,8 +879,16 @@ this tree has neither Mathlib-free; an earlier draft of this SPEC declared `nextPrime : Nat → Nat` with no account of either. Adding Euclid would make the total form available and is not on any consumer's critical path, so `NextPrimeFailure` reports exhaustion with the attempt -count and advanced state. The theorem records that a success is the -*least* such prime. +counts and advanced state. The units are separate: `rejectedCandidates` +counts only candidates conclusively proved composite, while `certAttempts` +counts randomized certificate-search attempts consumed by the candidate +whose decision exhausted. An undecided candidate is not included in +`rejectedCandidates`. If the candidate window itself is exhausted, +`certAttempts` is zero. In either case `rand` is the exact state after all +reported randomized work, so a caller can replay or resume without losing +work. Deterministic table lookup, trial division, and Miller--Rabin filtering +do not contribute to `certAttempts`. The theorem records that a success is +the *least* such prime. `primeCert?` distinguishes `PrimeCertStop.composite`, justified by the size check, table completeness, or a failed Miller-Rabin base, from `.exhausted`, diff --git a/HexPrimality/Search.lean b/HexPrimality/Search.lean index e03ba2e57..494644ff4 100644 --- a/HexPrimality/Search.lean +++ b/HexPrimality/Search.lean @@ -629,9 +629,13 @@ deriving Repr /-- A resumable next-prime-search failure. -/ structure NextPrimeFailure where - /-- Candidates conclusively rejected before the failure; the candidate - whose decision failed is not counted. -/ - attempts : Nat + /-- Candidates conclusively rejected as composite before exhaustion. An + undecided candidate is not counted. -/ + rejectedCandidates : Nat + /-- Randomized certificate-search attempts consumed by the undecided + candidate. Deterministic table, trial-division, and Miller--Rabin work is + not counted. -/ + certAttempts : Nat /-- The advanced generator state. -/ rand : Rand deriving Repr @@ -1017,12 +1021,13 @@ theorem isPrime_iff {n : Nat} : isPrime n = true ↔ Prime n := by private def nextPrimeGo (certFuel : Nat) : Nat → Nat → Nat → Rand → Except NextPrimeFailure (Nat × Rand) - | 0, _, attempts, r => .error ⟨attempts, r⟩ - | steps + 1, m, attempts, r => + | 0, _, rejectedCandidates, r => .error ⟨rejectedCandidates, 0, r⟩ + | steps + 1, m, rejectedCandidates, r => match isPrime? m r certFuel with - | .error f => .error ⟨attempts, f.rand⟩ + | .error f => .error ⟨rejectedCandidates, f.attempts, f.rand⟩ | .ok (true, r') => .ok (m, r') - | .ok (false, r') => nextPrimeGo certFuel steps (m + 1) (attempts + 1) r' + | .ok (false, r') => + nextPrimeGo certFuel steps (m + 1) (rejectedCandidates + 1) r' private theorem nextPrimeGo_spec (certFuel : Nat) : ∀ (steps m attempts : Nat) (r : Rand) {p : Nat} {r' : Rand}, @@ -1059,7 +1064,8 @@ private theorem nextPrimeGo_spec (certFuel : Nat) : /-- Fuel-bounded least-prime-above search: a total form needs Euclid's theorem, which this tree does not carry Mathlib-free, so exhaustion is -reported with the attempt count and advanced state. -/ +reported with separate counts for conclusively rejected candidates and +randomized certificate-search attempts, plus the exact advanced state. -/ def nextPrime? (n : Nat) (r : Rand) (fuel : Nat) : Except NextPrimeFailure (Nat × Rand) := nextPrimeGo fuel fuel (n + 1) 0 r diff --git a/conformance/HexPrimality/Conformance.lean b/conformance/HexPrimality/Conformance.lean index 2149d987c..a8eda2cad 100644 --- a/conformance/HexPrimality/Conformance.lean +++ b/conformance/HexPrimality/Conformance.lean @@ -282,10 +282,34 @@ private def rhoRecoveryTrace : Hex.Nat.Internal.RhoTrace := #guard (primesIn 99950 100050).toList.all fun p => isTablePrime p == decide (p < 100000) --- Next-prime search across the table edge. -#guard (match nextPrime? 99991 (Hex.Rand.ofSeed 0) 64 with - | .ok (p, _) => p == 100003 - | .error _ => false) +-- Next-prime success returns the least prime across the table, trial, and +-- certificate tiers. +#guard (match nextPrime? 90 (Hex.Rand.ofSeed 0) 8 with + | .ok (p, _) => p == 97 + | .error _ => false) +#guard (match nextPrime? 100000 (Hex.Rand.ofSeed 0) 4 with + | .ok (p, _) => p == 100003 + | .error _ => false) +#guard (match nextPrime? 10000000 (Hex.Rand.ofSeed 0) 32 with + | .ok (p, _) => p == 10000019 + | .error _ => false) + +-- Candidate-window exhaustion counts every proved-composite candidate but no +-- certificate attempts, and deterministic decisions leave the seed unchanged. +#guard (match nextPrime? 90 (Hex.Rand.ofSeed 0) 6 with + | .error failure => + failure.rejectedCandidates == 6 && failure.certAttempts == 0 && + failure.rand == Hex.Rand.ofSeed 0 + | .ok _ => false) + +-- The first candidate is undecided after nonzero randomized work. Its +-- certificate attempts and exact advanced state are retained, but it is not +-- counted as conclusively rejected. +#guard (match nextPrime? 1000000006 (Hex.Rand.ofSeed 3) 2 with + | .error failure => + failure.rejectedCandidates == 0 && failure.certAttempts == 7 && + failure.rand == ((Hex.Rand.ofSeed 3).words 7).2 + | .ok _ => false) -- Sieve representation and a complete small-bound comparison with the -- independent trial-division decision route. From 417624eb7700fd7321cc198e42eb969c64f01cdf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 30 Aug 2026 16:25:59 +0000 Subject: [PATCH 2/2] test(hex-primality): strengthen next-prime accounting guards --- HexPrimality/SPEC/hex-primality.md | 8 +++-- HexPrimality/Search.lean | 8 +++-- conformance/HexPrimality/Conformance.lean | 39 ++++++++++++++++++----- 3 files changed, 42 insertions(+), 13 deletions(-) diff --git a/HexPrimality/SPEC/hex-primality.md b/HexPrimality/SPEC/hex-primality.md index 6e4d5a7aa..5a3a9d79c 100644 --- a/HexPrimality/SPEC/hex-primality.md +++ b/HexPrimality/SPEC/hex-primality.md @@ -887,8 +887,12 @@ whose decision exhausted. An undecided candidate is not included in `certAttempts` is zero. In either case `rand` is the exact state after all reported randomized work, so a caller can replay or resume without losing work. Deterministic table lookup, trial division, and Miller--Rabin filtering -do not contribute to `certAttempts`. The theorem records that a success is -the *least* such prime. +do not contribute to `certAttempts`; in particular, every conclusively rejected +candidate leaves both this count and `rand` unchanged. A failure with +`rejectedCandidates = fuel` exhausted the whole candidate window. Otherwise +the undecided candidate is `n + 1 + rejectedCandidates`, so the two failure +modes and the resumption point are recoverable from the call and its failure. +The theorem records that a success is the *least* such prime. `primeCert?` distinguishes `PrimeCertStop.composite`, justified by the size check, table completeness, or a failed Miller-Rabin base, from `.exhausted`, diff --git a/HexPrimality/Search.lean b/HexPrimality/Search.lean index 494644ff4..d4a67fa5f 100644 --- a/HexPrimality/Search.lean +++ b/HexPrimality/Search.lean @@ -1030,8 +1030,8 @@ private def nextPrimeGo (certFuel : Nat) : nextPrimeGo certFuel steps (m + 1) (rejectedCandidates + 1) r' private theorem nextPrimeGo_spec (certFuel : Nat) : - ∀ (steps m attempts : Nat) (r : Rand) {p : Nat} {r' : Rand}, - nextPrimeGo certFuel steps m attempts r = .ok (p, r') → + ∀ (steps m rejectedCandidates : Nat) (r : Rand) {p : Nat} {r' : Rand}, + nextPrimeGo certFuel steps m rejectedCandidates r = .ok (p, r') → m ≤ p ∧ Prime p ∧ ∀ q, m ≤ q → q < p → ¬ Prime q := by intro steps induction steps with @@ -1065,7 +1065,9 @@ private theorem nextPrimeGo_spec (certFuel : Nat) : /-- Fuel-bounded least-prime-above search: a total form needs Euclid's theorem, which this tree does not carry Mathlib-free, so exhaustion is reported with separate counts for conclusively rejected candidates and -randomized certificate-search attempts, plus the exact advanced state. -/ +randomized certificate-search attempts, plus the exact advanced state. On +failure, `rejectedCandidates = fuel` means the candidate window was exhausted; +otherwise the undecided candidate is `n + 1 + rejectedCandidates`. -/ def nextPrime? (n : Nat) (r : Rand) (fuel : Nat) : Except NextPrimeFailure (Nat × Rand) := nextPrimeGo fuel fuel (n + 1) 0 r diff --git a/conformance/HexPrimality/Conformance.lean b/conformance/HexPrimality/Conformance.lean index a8eda2cad..60933c19c 100644 --- a/conformance/HexPrimality/Conformance.lean +++ b/conformance/HexPrimality/Conformance.lean @@ -30,6 +30,8 @@ Covered operations: Covered properties: - the total decision agrees with trial division on an initial segment - a `.composite` certificate-search verdict never contradicts `isPrime` +- next-prime exhaustion separates rejected candidates from certificate work + and returns the exact advanced random state - accepted certificates replay; each rejection reason rejects - the committed table window and the runtime segment listing agree - the small sieve agrees with trial division on every represented index @@ -287,12 +289,13 @@ private def rhoRecoveryTrace : Hex.Nat.Internal.RhoTrace := #guard (match nextPrime? 90 (Hex.Rand.ofSeed 0) 8 with | .ok (p, _) => p == 97 | .error _ => false) -#guard (match nextPrime? 100000 (Hex.Rand.ofSeed 0) 4 with +#guard (match nextPrime? 99991 (Hex.Rand.ofSeed 0) 16 with | .ok (p, _) => p == 100003 | .error _ => false) -#guard (match nextPrime? 10000000 (Hex.Rand.ofSeed 0) 32 with - | .ok (p, _) => p == 10000019 - | .error _ => false) +#guard (match nextPrime? 10000000 (Hex.Rand.ofSeed 0) 32, + isPrime? 10000019 (Hex.Rand.ofSeed 0) 32 with + | .ok (p, r), .ok (true, directRand) => p == 10000019 && r == directRand + | _, _ => false) -- Candidate-window exhaustion counts every proved-composite candidate but no -- certificate attempts, and deterministic decisions leave the seed unchanged. @@ -302,14 +305,34 @@ private def rhoRecoveryTrace : Hex.Nat.Internal.RhoTrace := failure.rand == Hex.Rand.ofSeed 0 | .ok _ => false) +-- Certificate-tier composite verdicts also consume no randomized work, so +-- exhausting a window of them leaves the seed unchanged. +#guard (match nextPrime? 10000000 (Hex.Rand.ofSeed 0) 4 with + | .error failure => + failure.rejectedCandidates == 4 && failure.certAttempts == 0 && + failure.rand == Hex.Rand.ofSeed 0 + | .ok _ => false) + -- The first candidate is undecided after nonzero randomized work. Its -- certificate attempts and exact advanced state are retained, but it is not -- counted as conclusively rejected. -#guard (match nextPrime? 1000000006 (Hex.Rand.ofSeed 3) 2 with - | .error failure => +#guard (match nextPrime? 1000000006 (Hex.Rand.ofSeed 3) 2, + isPrime? 1000000007 (Hex.Rand.ofSeed 3) 2 with + | .error failure, .error decisionFailure => failure.rejectedCandidates == 0 && failure.certAttempts == 7 && - failure.rand == ((Hex.Rand.ofSeed 3).words 7).2 - | .ok _ => false) + failure.certAttempts == decisionFailure.attempts && + failure.rand == decisionFailure.rand + | _, _ => false) + +-- A preceding deterministic composite and a later undecided candidate retain +-- both nonzero units without counting the undecided candidate as rejected. +#guard (match nextPrime? 1000000005 (Hex.Rand.ofSeed 3) 2, + isPrime? 1000000007 (Hex.Rand.ofSeed 3) 2 with + | .error failure, .error decisionFailure => + failure.rejectedCandidates == 1 && 0 < failure.certAttempts && + failure.certAttempts == decisionFailure.attempts && + failure.rand == decisionFailure.rand + | _, _ => false) -- Sieve representation and a complete small-bound comparison with the -- independent trial-division decision route.