Fix KoalaBear irreducibility proof replay on upstream Lean 4.33.1 - #2

Closed

yudduy wants to merge 45 commits into

zksecurity:mainfrom

yudduy:fix/sextic-replay-lean-4.33.1

Commits on Aug 17, 2026

feat: make KoalaBear Rabin irreducibility certificates re-checkable by kernel replay (#306)

kobizk
and
claude
authored
32a0c29

Commits on Aug 18, 2026

doc(RabinCertificate): correct the _of_card rationale and signature (#307)

alexanderlhicks
and
claude
authored
7480a69
refactor: relocate and rename the `Multivariate/Wheels.lean` lemmas (#305)

authored
ac87a1b

Commits on Aug 28, 2026

chore: migrate CompPoly to Lean v4.33.1 (#309)
dtumad
authored
a09455a

Commits on Sep 1, 2026

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

kobizk
and
dhsorens
authored
c6b1530
feat(fields): add fast Mersenne31 arithmetic (#257)

varunthakore
and
dhsorens
authored
ba5032e
feat(scripts): kernel-level axiom sweep with committed regression baseline (#300)

authored
bfea0dc

Commits on Sep 2, 2026

feat(fields): fast binary tower fields (up to 128 bits) (#286)

authored
8e84a81
test(fields): extend Mersenne31 regression coverage (#260)

adrienlacombe
and
dhsorens
authored
40ecb64
feat(fields): add fast Goldilocks arithmetic (#311)

dhsorens
and
varunthakore
authored
e66e436
feat(univariate): Shoup and Las Vegas root-search backends (#290)

dhsorens
and
olympichek
authored
19f0794
feat(linalg): order-basis approximant layer over polynomial matrices (#312)

dhsorens
and
olympichek
authored
2ee5257
feat(bivariate): approximant-basis and hybrid GS interpolation (#313)

dhsorens
and
olympichek
authored
9c0f84f
feat(multivariate): add partial evaluation of the first variable (#315)

dhsorens
and
codygunton
authored
e6fb7df
Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta) (#274)

mitschabaude-bot
and
claude
authored
322f12e

Commits on Sep 3, 2026

refactor(fields)!: remove the deprecated CompPoly.Fields.Mersenne module (#316)
dhsorens
authored
8ac9c98

Commits on Sep 4, 2026

feat(multilinear): factor the equality kernel (#318)

alexanderlhicks
and
eliasjudin
authored
2aa5937

Commits on Sep 7, 2026

refactor(fields): make carry-less multiplication width-generic (#320)

scaraven
and
claude
authored
5671e4c
feat(fields): add polynomial-basis GF(2^64) and its cubic extension (#321)

scaraven
and
claude
authored
3468b38

Commits on Sep 8, 2026

fix(algebra): require identity maps in algebra towers (#324)
alexanderlhicks
authored
b082daf

Commits on Sep 9, 2026

Shore up the benchmarking foundations: cheap sinks, sampling, and per-group seeding (#319)
dhsorens
authored
bbc26a0

Commits on Sep 10, 2026

Size benchmarks from a wall-clock budget instead of 228 hand-tuned counts (#337)
dhsorens
authored
4ce69b9

Commits on Sep 15, 2026

Commits on Sep 21, 2026

Fix KoalaBear irreducibility proof replay

yudduy
and
claude
committed
0fdf177