Skip to content

doc(RabinCertificate): clarify the cold-replay mechanism #308

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dhsorens merged 2 commits into from
Sep 1, 2026
Merged

doc(RabinCertificate): clarify the cold-replay mechanism #308

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
483b956
doc(RabinCertificate): clarify the cold-replay mechanism
kobizk Aug 18, 2026
fc0ca8f
Merge branch 'main' into docs/rabin-cold-replay-mechanism
dhsorens Sep 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions CompPoly/Data/Polynomial/RabinCertificate.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -405,8 +405,12 @@ caller-supplied `q` with `hcard : Fintype.card F = q`. Same shape as

Identical content to `irreducible_of_rabin_prime_degree`, with the field size supplied as `q` and
`hcard : Fintype.card F = q` rather than read off as `Fintype.card F`. Each Rabin condition is then
discharged by applying its certificate directly, rather than first casting the goal with
`rw [hcard]`. Supply `hcard` as `ZMod.card _`.
discharged by applying its certificate directly, avoiding the concrete caller-side `Eq.mpr`
transports introduced by `rw [hcard]`. Fresh replay checks a serialized and reconstructed expression
graph, so it need not follow the same normalization path as checking the elaborator's in-memory
term. In the observed cold replay, checking one such transport's certificate argument entered
`Polynomial.pow → npowRec → Nat.rec`, unfolding `X ^ (fieldSize ^ 6)` one exponent step at a time
until Lean's deep-recursion guard fired. Supply `hcard` as `ZMod.card _`.

Nothing is weakened: instantiating at `q := Fintype.card F` with `rfl` recovers
`irreducible_of_rabin_prime_degree` verbatim, and `CompPolyTests.RabinCertificate` pins that
Expand Down
Loading