risc0-lean4
⚠️ This repository contains research artifacts. It is a work in progress and should not be used for any purpose.
risc0-lean4 is a formal model of the RISC Zero zkVM, written in the Lean Theorem Prover (version 4). Its long-term goal is to support formal security and soundness proofs for the RISC Zero ecosystem.
Features
We have executable models for:
- ELF file handling
- RV32IM emulation
- SHA2-256
- Merkle tree parsing and inclusion proof verification
- The Baby Bear field (and its degree 4 extension)
- Number Theoretic transform (NTT)
- FRI verification
- Arithmetic circuit parsing and evaluation
- zkVM receipt parsing and verification
We are currently developing the meta-theory of these systems.
Repo Organization
- Main verification logic
- Lean version: Verify.lean
- Rust version: verify/mod.rs
- Merkle verification
- Lean version: Merkle.lean
- Rust version: verify/merkle.rs
- FRI verification
- Lean version: Fri.lean
- Rust version: verify/fri.rs
Compatibility
This repository trails behind the zkVM repository. Precise version information can be found in Cargo.lock.
Building
Getting Lean4
See the Quickstart guide.
Performing the build
First, check to see if lake is in your terminal's search path. If not, you either haven't installed Lean4 yet, or you haven't source'd the elan environment variables.
risc0-lean4$ source ~/.elan/env
Now you can perform the build:
risc0-lean4$ lake build
Running the tools
This repository includes various executables. These executables are currently used for testing, but will eventually be expanded to provide greater utility.
Receipt verifier
Verify a receipt generated by the zkVM:
risc0-lean4$ ./build/bin/zkvm-verify-lean4
zkVM emulator
Run a zkVM guest (without proof):
risc0-lean4$ ./build/bin/zkvm-emu-lean4
Elf dumper
Read the headers of an ELF binary:
risc0-lean4$ ./build/bin/elf-dump-lean4
Building the docs
$ lake -Kdoc=on update
$ lake -Kdoc=on build Zkvm:docs
The docs will be viewable at build/doc/index.html.