perf(hex-primality): enforce measured elaborator policy

.github/workflows/ci.yml

@@ -167,7 +167,7 @@ jobs:
       # fresh against the restored libs, which is cheap.
       - name: Define the hex-dev cache + build target sets
         run: |
-          echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
+          echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
           echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
       # Shared build. The libraries, bench exes, conformance #guard drivers, and
       # emit-fixture exes are all elaborated here so the two verification tails

HexPrimality/Elab.lean

@@ -28,9 +28,10 @@ numeral `e`; `primality n` adds `this : Hex.Nat.Prime n`;
 `primality h : n` names it `h`.
 
 For reproducible syntax with no seed argument, the elaborator uses
-`Rand.ofSeed n` and `defaultPrimeFuel n`; the lower `primeCert?` API remains
-explicitly seeded, and diagnostics report the seed and fuel if certificate
-search exhausts its budget. The companion library may register an
+`Rand.ofSeed n` and `primalityFuel n`, the measured policy cap over
+`defaultPrimeFuel n`; the lower `primeCert?` API remains explicitly seeded,
+and diagnostics report the seed and fuel if certificate search exhausts its
+budget. The companion library may register an
 additional `@[tactic primalityTac]` handler for `Nat.Prime` goal shapes;
 handlers registered later run first and defer here by throwing
 `unsupportedSyntax`.
@@ -89,11 +90,54 @@ meta def checkClosed (tactic : String) (e : Expr) : MetaM Unit := do
     throwError "{tactic}: the argument{indentExpr e}\
         \nmust not contain free or meta variables"
 
-/-- Bit-length ceiling on tactic inputs: the kernel replay uses
-`O(K log n)` modular and bounded ordinary multiplications plus `O(K)`
-factor-subject comparisons, and beyond this size certificate search itself
-is the bottleneck to fix first. -/
-meta def primalityBitBudget : Nat := 8192
+/-- Supported bit-length ceiling for every elaboration-time certificate route.
+The 512-bit boundary is the largest measured fresh-module rung; changing it
+requires new end-to-end search, reification, and kernel-replay evidence. -/
+meta def primalityBitBudget : Nat := 512
+
+/-- Maximum recursive fuel passed to elaboration-time certificate search.
+At the supported bit ceiling `defaultPrimeFuel` is 1038; the round 1040 cap
+makes the resource bound explicit and prevents later changes to the default
+from silently widening the tactic policy. -/
+meta def primalityFuelBudget : Nat := 1040
+
+/-- Maximum Brent restarts at one partial-factor worklist entry on every
+elaboration-time certificate route. -/
+meta def primalityRhoRestartBudget : Nat := 2
+
+/-- Maximum Brent cycle steps per restart on every elaboration-time
+certificate route. -/
+meta def primalityRhoStepBudget : Nat := 1 <<< 15
+
+/-- The explicit rho allocation shared by every elaboration-time route. -/
+meta def primalitySearchBudget : Hex.Nat.PrimeCertBudget :=
+  ⟨primalityRhoRestartBudget, primalityRhoStepBudget⟩
+
+/-- The fuel selected by every elaboration-time certificate route. -/
+meta def primalityFuel (n : Nat) : Nat :=
+  min (Hex.Nat.defaultPrimeFuel n) primalityFuelBudget
+
+/-- Whether an input is admitted by the common elaboration policy. -/
+meta def withinPrimalityBudget (n : Nat) : Bool :=
+  decide (n.log2 + 1 ≤ primalityBitBudget)
+
+/-- Enforce the common input-size policy before any certificate search. -/
+meta def checkPrimalityPolicy (tactic : String) (n : Nat) : MetaM Unit := do
+  let bits := n.log2 + 1
+  unless withinPrimalityBudget n do
+    throwError "{tactic}: input has {bits} bits; the enforced policy supports \
+        at most {primalityBitBudget} bits; raising the ceiling requires new \
+        end-to-end benchmark evidence"
+
+/-- Report bounded-search exhaustion without inviting an unbounded fallback. -/
+meta def throwPrimalityExhausted {α : Type} (tactic : String) (n attempts fuel : Nat) :
+    MetaM α :=
+  throwError "{tactic}: certificate search for {n} exhausted after {attempts} \
+      attempts (seed {n}, recursive fuel {fuel}; policy maximum \
+      {primalityFuelBudget} fuel at {primalityBitBudget} bits, \
+      {primalityRhoRestartBudget} rho restarts with \
+      {primalityRhoStepBudget} steps each); no total primality decision was \
+      attempted"
 
 /-- Run the certificate search and emit the checked proof term with `head`
 applied to the subject, the reified certificate, and the `Eq.refl true`
@@ -107,10 +151,10 @@ meta def provePrimeWith (head : Name) (tactic : String) (n : Nat)
         \nevaluates to {n} but is not definitionally transparent to the \
         elaborator (an imported definition without `@[expose]`?); the kernel \
         could not check the emitted certificate against it"
-  if n.log2 + 1 > primalityBitBudget then
-    throwError "{tactic}: {n} has more than {primalityBitBudget} bits; \
-        raising `primalityBitBudget` is a separate, benchmarked change"
-  match Hex.Nat.primeCert? n (Hex.Rand.ofSeed n) (Hex.Nat.defaultPrimeFuel n) with
+  checkPrimalityPolicy tactic n
+  let fuel := primalityFuel n
+  match Hex.Nat.Internal.primeCertCountedWith? primalitySearchBudget n
+      (Hex.Rand.ofSeed n) fuel with
   | .error f =>
       match f.stop with
       | .composite =>
@@ -122,11 +166,9 @@ meta def provePrimeWith (head : Name) (tactic : String) (n : Nat)
           | none =>
               throwError "{tactic}: {n} is not prime"
       | .exhausted =>
-          throwError "{tactic}: certificate search for {n} exhausted its \
-              budget after {f.attempts} attempts (seed {n}, fuel \
-              {Hex.Nat.defaultPrimeFuel n}); the factorization of n - 1 may \
-              be out of reach"
-  | .ok (c, _) =>
+          throwPrimalityExhausted tactic n f.attempts fuel
+  | .ok success =>
+      let c := success.cert
       -- Untrusted-search self-check before emitting anything.
       unless c.raw.subject == n && Hex.Nat.checkPrime c.raw do
         throwError "{tactic}: internal error: the found certificate fails \

HexPrimality/SPEC/hex-primality.md

@@ -782,6 +782,12 @@ structure NextPrimeFailure where
 
 def defaultPrimeFuel (n : Nat) : Nat
 
+structure PrimeCertBudget where
+  rhoRestarts : Nat
+  rhoSteps    : Nat
+
+def defaultPrimeCertBudget : PrimeCertBudget
+
 structure Internal.PrimeCertSuccess (n : Nat) where
   cert     : CheckedPrimeCert n
   attempts : Nat
@@ -790,6 +796,14 @@ structure Internal.PrimeCertSuccess (n : Nat) where
 def Internal.primeCertCounted? (n : Nat) (r : Rand) (fuel : Nat) :
     Except PrimeCertFailure (Internal.PrimeCertSuccess n)
 
+def Internal.primeCertCountedWith? (budget : PrimeCertBudget)
+    (n : Nat) (r : Rand) (fuel : Nat) :
+    Except PrimeCertFailure (Internal.PrimeCertSuccess n)
+
+theorem Internal.primeCertCountedWith?_composite {budget n r fuel f}
+    (hresult : Internal.primeCertCountedWith? budget n r fuel = .error f)
+    (hstop : f.stop = .composite) : ¬ Prime n
+
 theorem Internal.primeCertCounted?_composite {n r fuel f}
     (hresult : Internal.primeCertCounted? n r fuel = .error f)
     (hstop : f.stop = .composite) : ¬ Prime n
@@ -902,18 +916,78 @@ it replays `O(k log n)` modular multiplications on GMP-backed `Nat`, and never
 the search.
 
 For reproducible syntax with no seed argument, the elaborator uses
-`Rand.ofSeed n`; the lower `primeCert?` API remains explicitly seeded,
-and diagnostics report the seed and attempts if certificate search
-exhausts its fuel.
+`Rand.ofSeed n`; the lower `primeCert?` API remains explicitly seeded.
+
+**The supported positive-certificate elaboration policy is at most 512 input
+bits, at most 1040 recursive certificate-search fuel, at most 2 Brent restarts
+per partial-factor worklist entry, and at most 32768 Brent cycle steps per
+restart.** Every elaboration-time certificate route uses
+`primalityFuel n = min (defaultPrimeFuel n) 1040`; at the exact 512-bit boundary
+the default contributes 1038. The recursive fuel bounds certificate-construction
+depth. Partial factorization is bounded separately by `2 * n.log2 + 8` worklist
+steps at each certificate node and the rho restart/cycle allocation above. The
+fixed witness budget remains 32 candidates per factor entry. The exact attempt
+counter includes rho restarts and witness candidates and can therefore exceed
+the recursive fuel used at a node. Inputs above 512 bits are rejected before
+Miller--Rabin or certificate search. Search exhaustion reports the seed,
+selected recursive fuel, exact attempt count, and all enforced search maxima,
+and explicitly says that no total decision was attempted.
+
+The ceiling is the largest rung with both compiled and kernel evidence. The
+exact-boundary prime `100297^22 * 2^146 + 1`, namely
+`9521691625768090263084389838561930764813603239089634545416648725957969250257409112878363599328138633827640729385461401574761860536478435114675541614002177`, is 512 bits. Its table factors alone do not meet the
+Pocklington threshold: the accepted core and companion routes use bounded rho
+work to discover the above-table factor `100297`, finish after 31 counted
+attempts, reify its recursive certificate, and replay it in the kernel. The
+same prepared certificate is checked by `HexPrimalityKernelProbe` and the
+native `runDecision`, `runCertSearch`, and `runChecker` families. The paired
+fresh-module sweep also exercises the non-smooth 512-bit probable-prime input
+`11069588345001798189188705872711741673446310956174776680242876230365522527670481055399138994024099817696810905038323515123654848684366962778647276800762123`,
+which reaches bounded rho work in a recursive child and exhausts after 11
+attempts at fuel 1038, and the 513-bit value `2^512`, which is rejected before
+search. Both core and companion routes have a 10-second absolute fresh-module
+wall-clock budget on the designated benchmark host. The harness compares the
+largest raw candidate wall time in every substantive sample set against that
+budget and makes any failure invalidate `release_quality`; it does not use the
+reference-subtracted tactic delta for this contract. This single end-to-end
+budget includes Lake startup and build-graph traversal, importing, compiled
+search, compiled self-check, reification, and kernel replay. Rejection and
+exhaustion may be indistinguishable from their import-only controls, but their
+absolute wall times remain budget-gated.
+The paired null controls remain in the record to classify those deltas; their
+spread is not a release gate for this absolute-only contract. Per-arm CPU and
+SMT-sibling interference checks remain hard gates for every accepted sample.
+The raw paired samples and host provenance are committed at
+`reports/bench-results/hex-primality-elaborator-policy-issue-9779-chungus2.json`.
+They reproduce with:
+
+```bash
+python3 scripts/bench/primality_elab_sweep.py --samples 6 \
+  --shared-host --expected-host chungus2 --cpu 22 --timeout 30 \
+  --warm-timeout 600 --max-pair-retries 32 \
+  --output reports/bench-results/hex-primality-elaborator-policy-issue-9779-chungus2.json
+```
+
+`lake build HexPrimalityElabProbe` is the untimed build-only reproduction.
+`primality` calls only `primeCertCountedWith?` with the explicit allocation
+above: it never calls the total `isPrime`, whose exact trial fallback is
+intentionally unbounded.
 
 The companion adds `Nat.Prime n` through that correspondence. Bare
 `primality` uses the certificate route directly. Pinned Mathlib's
 `Nat.Prime` `norm_num` extension was registered first, so ordinary imports
 retain Mathlib's trial-division behavior; the later Hex registration cannot
 transparently pre-empt it. A module explicitly opts into the supported Hex
 policy with `use_hex_primality_norm_num`. Under that policy, numerals below
-`2^24` use a guarded alias of Mathlib's trial extension and larger numerals
-use bounded Hex certificate search. The opt-in erasure is local to the
+`2^24` use a guarded alias of Mathlib's trial extension and larger positive
+proofs use the same 512-bit/1040-fuel/2-restart/32768-step Hex certificate
+policy as `primality`. After a fixed-tier composite verdict, negative proofs
+use a separate finite factor search of 16 restarts, each bounded by
+`rhoInnerFuel n`; a found factor is dynamically revalidated before proof
+emission, and exhaustion only declines the goal. It never starts total trial
+division. Above 512 bits the opt-in extension declines both positive and
+negative goals; `norm_num` reports an unsolved goal rather than silently
+restoring Mathlib's total trial decision. The opt-in erasure is local to the
 module and does not persist when that module is imported.
 
 The `2^24` boundary comes from fresh one-goal modules on the pinned
@@ -999,7 +1073,7 @@ in the part of a certificate tree replayed before acceptance or rejection.
 | `isPrime` worst case | `O(√n)` remainder tests | exact fallback after default search exhaustion |
 | `checkPrime`, one Pocklington level | `O(k b)` modular multiplications; `O(k b)` bounded ordinary multiplications; `O(k)` subject comparisons, divisions, and gcds | canonical subject preflight is linear on accepted and rejected lists |
 | `checkPrime`, full tree | `O(Σᵥ kᵥ bᵥ)` modular and bounded ordinary multiplications; `O(K)` subject comparisons, divisions, and gcds | `kᵥ`, `bᵥ` are the entry count and subject bit bound at each visited node; arithmetic preflight bounds each replayed child's subject below its parent, so the sum is `O(K b)` for root bit length `b` |
-| `primeCert?` | dominated by `partialFactor` | unbounded; fuel-limited |
+| `primeCert?` | dominated by `partialFactor` | bounded by recursive fuel, per-node worklist fuel, and `defaultPrimeCertBudget` rho restarts/cycle steps |
 | sieve to `N` | `O(√N + π(√N) · 32)` loop/doubling rounds | each marking round is a bit operation on an `N/3`-bit `Nat` |
 
 These are operation counts, not bit complexity; subject comparisons,
@@ -1112,8 +1186,9 @@ Policy-selection evidence, retained as input to but not a claim about Phase 4:
 
 Families:
 - **Kernel replay**, `checkPrime` on certificates for primes of `31`,
-  `61`, `123`, `256`, and `511` bits (the table-smooth ladder). Decides
-  the `powModNat`-versus-Montgomery question under "Kernel exposure".
+  `61`, `123`, `256`, `511`, and `512` bits. The lower rungs are table-smooth;
+  the 512-bit rung includes the above-table factor `100297`. Decides the
+  `powModNat`-versus-Montgomery question under "Kernel exposure".
 - **Native decision**, bounded `isPrime?` across the same bit lengths.
   The total `isPrime` gets no separate row: it differs only on the
   exhausted-search path, where its exact trial-division fallback is