perf(primality): accelerate kernel certificate replay - #10284
Merged
Merged
Conversation
added 5 commits
September 15, 2026 15:37
kim-em
force-pushed
the
perf-primality-replay
branch
from
September 15, 2026 15:38
0ee3e54 to
c9e5f27
Compare
kim-em
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Reduce kernel certificate replay with fixed-window powering, checked power-of-two shifts, direct structural folds, and shared Fermat checks. Proved compiler rewrites (
@[csimp]) connect the kernel specifications to the original compiled algorithms. Checker acceptance, search budgets, and the exact Curve25519primality?suggestion are preserved.Hex wins all eight supplied inputs and all 32 adjacent pairs against compact PrimeCert certificates with matching selected factors and its certified sieve for larger table leaves:
These are complete proof-body kernel checks, excluding imports and elaboration, on Hex/Lean 4.34 and unmodified PrimeCert/Lean 4.33. Every sample is retained. Margins range from 1.11× to 3.46× on this shared host. The earlier PrimeCert Pocklington-leaf variant was slightly faster than its sieve variant; Hex won all eight cases against it too. Curve448 is supplied in both systems, and automatic Hex construction still exhausts there. Chart, sources, and reproduction.
Includes updated SPECs/manual, a checker-only Curve448 fixture, overflow and witness-cache regressions, and arithmetic-specific negative controls. Local verification: full build (14,434 jobs), focused conformance, existing HexArith/HexPrimality/HexIntFactor benchmark verification, and all 64 fresh oracle cases.
🤖 Implemented with Codex assistance.