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.

risc0/risc0-lean4