Directive: generate reusable primality certificates and reach Curve25519

Outcome

Extend the existing Mathlib-free primality pipeline so an explicitly requested certificate-generation mode can prove Hex.Nat.Prime (2^255 - 19), offer the exact checked certificate as a Try this: replacement, and make that replacement a deterministic regression fixture.

The ordinary primality tactic already has the right trust boundary: compiled search is untrusted, the result is reified as PrimeCert, and prime_of_checkPrimeAt makes the kernel replay checkPrime. Preserve that architecture. This directive is about search reach, reusable source output, certificate size, and replay cost.

The primary normative owner is HexPrimality/SPEC/hex-primality.md. Amend HexIntFactor/SPEC/hex-int-factor.md as well if its registered factor-search budget or smooth-search contract changes.

Premise and concrete obstruction

Let

p = 2^255 - 19
  = 57896044618658097711785492504343953926634992332820282019728792003956564819949.

The current fixed-base Miller-Rabin screen accepts p, but both the core search and the registered HexIntFactor extension exhaust. The public complete factorizer likewise returns a checked incomplete result.

The relevant first certificate child is exposed by

p - 1 = 2^2 * 3 * 65147 *
  74058212732561358302231226437062788676166966415465897661863160754340907.

Recursively, search must separate the factor

31757755568855353,

whose predecessor has largest prime factor 430751. An independent stage-one Pollard p - 1 diagnostic at base 2 returns this factor at bound 524288 and returns no factor at 262144. Reproduce that boundary with the Lean implementation before relying on it.

Once this factor is available, the accumulated factor product

981609426360740691344999861639072106

exceeds

sqrt(74058212732561358302231226437062788676166966415465897661863160754340907)
= 272136386270857499792158335716642712,

so the search has enough data for square-root Pocklington without factoring the remaining cofactor completely.

The present hard limit is smoothBoundCap = 9999. Pollard p - 1 and ECM obtain their stage primes from the committed table, so merely raising that constant would not implement the requested bound.

1. Verified runtime prime source

Use a verified runtime prime source rather than adding a second unverified sieve or growing the committed primeTable to this search bound.

The existing HexPrimality.Sieve already proves sieve_testBit_iff, and mem_bitsToList plus bitsToList_pairwise_lt provide the readback and ordering facts. Add a convenient compiled wrapper, including the exceptional primes 2 and 3, with a theorem of the shape

n ∈ primesBelow bound ↔ n < bound ∧ Hex.Nat.Prime n

and retain strict ascending order/no duplicates. Choose the final short standard name during the SPEC edit.

This wrapper should:

• execute through the compiled sieve;
• be independent of the fixed committed-table bound;
• supply the stage primes used by Pollard p - 1 and ECM;
• make the requested smoothness bound mean that every prime up to that bound was actually included;
• be benchmarked at least through the Curve25519-required bound;
• avoid forcing kernel replay of a newly generated half-million-entry table.

The final primality and factor results remain protected by their existing checkers. Verification here additionally protects search coverage and creates a reusable exact prime-enumeration API. It should also be considered as the broad-initial-segment implementation behind primesIn, but changing that public implementation is benchmark-dependent rather than required for this directive.

Do not enlarge the committed primeTable merely to feed a search algorithm.

2. Separate construction and ordinary tactic budgets

Keep the ordinary primality policy bounded by its current interactive/release budget unless measurements justify a change independently.

Add an explicitly requested certificate-construction policy with enough bounded work to handle this example. Its resource configuration must state and report at least:

• maximum input bits and recursive certificate depth;
• factor-worklist fuel;
• Pollard p - 1 bounds and bases;
• rho restarts and steps;
• ECM bounds and curve count;
• witness candidates.

The construction route must remain finite and report honest exhaustion. It must not invoke trial division as an effectively unbounded fallback or shell out to PARI, GNU factor, Python, or another external prover.

The initial required smooth route is stage-one Pollard p - 1 through at least 524288. Pollard p - 1 stage 2, ECM stage 2, ECPP, quadratic sieve, and number-field sieve are outside this directive.

Prefer an explicit budget/profile passed through FactorSearchBudget over more hard-coded attempt caps. Preserve exact attempt and Rand accounting on success and exhaustion.

3. Minimize the emitted certificate

Do not recursively certify every factor returned by an untrusted producer and only then discover that a much smaller subset sufficed.

Select and validate a deterministic subset that satisfies either square-root Pocklington or the cube-root criterion. The selection cost should account for recursive child certificates, not only the number or magnitude of factors at the current node. Prefer table leaves and already cheap children when they yield a smaller replay tree.

Try deterministic small witness bases before random witnesses. Reusing a witness base is useful because later checker work may share its Fermat leg.

After minimization, run the public checkPrime on the exact certificate that will be emitted. Malformed factor data may only cause exhaustion.

The compact five-node certificate committed in PR #10267 is the current target shape. A different certificate is acceptable only with concrete evidence that it is smaller or replays faster; the chosen output then becomes the pinned fixture.

4. primality? and the reusable suggestion

Add a goal tactic:

example : Hex.Nat.Prime (2 ^ 255 - 19) := by
  primality?

primality? should run the explicit construction policy, close the goal, and use Lean's core TryThis facility to offer source equivalent to

exact Hex.Nat.prime_of_checkPrimeAt
  (c := .pock ...)
  (by decide +kernel)

Applying the suggestion must remove certificate search from future clean builds. It does not remove kernel replay. Certificate minimization and checker improvements own replay performance.

The rendered replacement must:

• contain the certificate literal itself, not another call to primality;
• be valid in the original namespace and import context;
• preserve the original goal expression, including 2 ^ 255 - 19;
• use stable formatting and fully qualified names where context could otherwise change resolution;
• work without Mathlib for Hex.Nat.Prime;
• use the companion bridge for Nat.Prime when HexPrimalityMathlib is imported;
• contain no sorry, axiom, or native_decide.

The existing reifyPrimeCert code should be shared between ordinary proof emission and suggestion rendering rather than maintaining two certificate encoders.

5. Exact suggestion regression

The acceptance test must use #guard_msgs to pin the complete Try this: output, including the full expected certificate literal. A test that only checks that primality? closes the goal is insufficient.

The fixture should have the form

/--
info: Try this:
  exact Hex.Nat.prime_of_checkPrimeAt
    (c := <the complete expected certificate>)
    (by decide +kernel)
-/
#guard_msgs in
example : Hex.Nat.Prime (2 ^ 255 - 19) := by
  primality?

Add a small fast #guard_msgs case for renderer diagnostics as well, but do not replace the Curve25519 fixture with only the small case. Pin failure diagnostics for construction-budget exhaustion separately.

6. Replay performance

Measure before changing the checker. Separate:

1. input elaboration;
2. certificate search;
3. suggestion rendering/literal elaboration;
4. kernel replay of the committed literal;
5. the complete primality? invocation.

Use the repository's adjacent-arm shared-host protocol and retain every completed sample. Add Curve25519 as a fixed, mode-3 target alongside the existing bit-size family. Record certificate node/entry counts and emitted source/olean sizes.

Investigate at least these replay costs:

• checkWitness recomputes a^(n-1) mod n for every factor entry, even when several entries use the same base;
• independent modular exponentiations at one node do not share a power ladder;
• automatically retained factors may add both parent witness work and recursive child replay.

Any checker representation change must keep checkPrime sound for arbitrary accepted certificates and retain kernel-only replay. Profile before choosing between grouped witnesses, cached Fermat legs, or shared exponentiation ladders.

CI work extends the existing single jobs and scripts; do not add jobs, matrices, or workflows.

Acceptance

• The verified runtime prime wrapper has exact membership and ordering theorems and generates through the required bound in compiled code.
• Lean's Pollard p - 1 route reproduces the required factor at the declared bound.
• The construction route finds and self-checks a certificate for 2^255 - 19 from its deterministic seed and declared finite budget.
• primality? closes the Curve25519 goal and emits a clickable certificate-literal suggestion.
• A #guard_msgs fixture pins the complete exact Curve25519 suggestion.
• Applying that suggestion yields a standalone proof importing only the checker-owning library.
• Ordinary primality behavior and its current bounded failure contract remain stable unless separately justified by measurements.
• Search, replay, and end-to-end measurements are recorded separately, with the host-specific observation in PR example(primality): certify the Curve25519 prime #10267 used only as a starting datum.
• Conformance includes sieve endpoints around 2, 3, and the requested bound; exact Pollard p - 1 success/no-factor/whole outcomes; deterministic certificate generation; malformed-certificate rejection; suggestion text; and honest exhaustion.
• lake build, the existing bench verification commands, and the existing oracle/conformance scripts pass.

Trust boundary

Prime generation and factor search may run compiled code, but no generated prime list, factor claim, witness choice, minimized subset, or rendered suggestion is trusted. The proof accepted by Lean remains an application of checker soundness to a kernel-reduced checkPrime result.