✨ WIP ✨
This repository contains the Lean 4 verification efforts using Aeneas of some field arithmetic crates from Plonky3.
Currently we are testing the capabilities of Aeneas to extract a Rust model of the Mersenne31 crate, with the aim of verifying it against CompPoly.
src/contains the Mersenne31 models (and a draft for KoalaBear) that we are incrementally building.lean/holds the extracted code and verification efforts.extract-aeneas.shis the extraction script, which also modifies the extracted code for correctness.
We're currently targeting fields.rs
and mersenne31.rs,
with the corresponding incremental models in src/.
Documentation for this repository can be devided into the following categories and found in the following places:
- Incremental construction of the Mersenne31 models and description on the encountered challenges:
src/directory. - Fixes to the extracted Lean code: commented in the
extract-aeneas.shfile.