Plonky3's Field Arithmetic Extraction With Aeneas

✨ 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.

Repository Structure

• 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.sh is the extraction script, which also modifies the extracted code for correctness.

Extraction Targets

We're currently targeting fields.rs and mersenne31.rs, with the corresponding incremental models in src/.

Further Documentation

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.sh file.