The goal of the project is to verify cryptographic primitives of arkworks library used in Substrate framework and Polkadot node code.
Verification is performed through translation of code from Rust to Lean4 with the help of Charon + Aeneas. After that, properties and proofs for them are formulated.
The translation of functions and structures can be found in Funs.lean and Types.lean. These files are automatically generated
Manually formulated properties and proofs can be found in Proofs.lean
Work is currently in progress on the BigInt primitive of large numbers.
The main dependencies are charon and aeneas. To get everything up and running without issues you can use the Dockerfile in the root of the repository.
docker build -t psc .
docker run -it -v $(pwd):/workspace psc bashOn VSCode, you can also install the Dev Containers extension and open this project in a container.
To build, simply run make.
The tests can be run with make test.
For code that is reached from the main.rs entry point, charon and aeneas generate provable code in the test/lean/Test folder. Proofs should be written in test/lean/Proofs.lean. You can find a nice tutorial on aeneas proofs here.