Added AutoCorrode submodule, a reasoning framework for Rust and C in Isabelle/HOL#1590

Open

DominicPM wants to merge 11 commits into

pq-code-package:mainfrom

DominicPM:autocorrode-submodule

Commits on Mar 25, 2026

proofs/isabelle: add AutoCorrode submodule
DominicPM
committed
proofs/isabelle: add abstract ML-KEM polynomial specification and refinement
DominicPM
committed
proofs/isabelle: add NTT zeta factor table and properties
DominicPM
committed
proofs/isabelle: add forward and inverse NTT abstract specifications
DominicPM
committed
proofs/isabelle: prove NTT/inverse-NTT are two-sided inverses mod q
DominicPM
committed
proofs/isabelle: add C functional correctness proofs for scalar helpers
DominicPM
committed
proofs/isabelle: add C functional correctness proofs for Montgomery reduction
DominicPM
committed
proofs/isabelle: add C functional correctness proofs for polynomial loops
DominicPM
committed
proofs/isabelle: add C functional correctness proof of forward NTT
DominicPM
committed
proofs/isabelle: add C functional correctness proof of inverse NTT
DominicPM
committed
proofs/isabelle: wire up split theories, add PDF document generation, remove monolithic files
DominicPM
committed