Correct the keccak gate and prove bound necessity - #950

Draft

jotabulacios wants to merge 11 commits into

docs-keccak-formal-verification-baselinefrom

fix/keccak-gate-bound-necessity

Commits on Sep 2, 2026

Cite the keccak gate's constructs by name
jotabulacios
committed
f8c1d28
Drop the README's stale-citation catalogue
jotabulacios
committed
a6f6ce4
Decide which keccak range checks are needed
jotabulacios
committed
3051bbf
Exhibit the rho forgery as a complete round
jotabulacios
committed
fd684a6
Record what each keccak range check is worth
jotabulacios
committed
d193ef8
Pin the KECCAK_RND AIR structure, not its counts
jotabulacios
committed
ea575af

Commits on Sep 3, 2026

Check the rho config-D forgery hits its target
jotabulacios
committed
83aa3a3
Decide each keccak range check by a full sweep
jotabulacios
committed
7bd904d
Control the full-chip witness against FIPS-202
jotabulacios
committed
4a29e2c
Run the solver-free keccak gates in CI
jotabulacios
committed
7804fa9
Record how each keccak necessity cell is decided
jotabulacios
committed
6ddf0ba