This is an old repository associated with this paper.
This project didn't fully make the transition to Lean 4 at the time the rest of the ecosystem did. With Claude Fable available again, I've used it to restore the project to a building state.
Here are some next steps that I'd like to accomplish if I have time:
- Reengineer all polynomials to use the computable polynomial framework (partially done).
- Reformulate the core soundness proving tactic into a computable non-meta function that analyzes a straightforward Linear PCP SNARK scheme and decides if it is sound, (and/or at least outputs the core ideal membership test problem(s)).
- Hook up Lean-SMT or another tactic to resolve these membership tests.
- This will require bumping Lean-SMT to a new toolchain.
- Formulate the Grobner basis problem instances for all of the SNARKs into a standard SMT format for benchmarking purposes.
- Introduce different models for Type I and Type III groups (Type II as well?) and duplicate SNARKs to prove sound in each model where soundness holds.