Repository files navigation

⚠️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 theRISC Zero zkVM, written in theLean Theorem Prover (version4). Its long-term goal is to support formal security and soundness proofs for the RISC Zero ecosystem.

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.

• 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

This repository trails behind thezkVM repository. Precise version information can be found inCargo.lock.

See theQuickstart guide.

First, check to see iflake is in your terminal's search path. If not, you either haven't installed Lean4 yet, or you haven'tsource'd theelan environment variables.

risc0-lean4$ source ~/.elan/env

Now you can perform the build:

risc0-lean4$ lake build

This repository includes various executables. These executables are currently used for testing, but will eventually be expanded to provide greater utility.

Verify a receipt generated by the zkVM:

risc0-lean4$ ./build/bin/zkvm-verify-lean4

Run a zkVM guest (without proof):

risc0-lean4$ ./build/bin/zkvm-emu-lean4

Read the headers of an ELF binary:

risc0-lean4$ ./build/bin/elf-dump-lean4

$lake -Kdoc=on update$lake -Kdoc=on build Zkvm:docs

The docs will be viewable atbuild/doc/index.html.