UPDATE: This project uses an old version of Risc0. For a more recent iteration of this project, see this repo.
This repository, based on risc0-rust-starter and rust-metamath, is a ZK-STARKed Metamath checker. It uses RISC Zero to compile a checker for the Metamath formal language to a RISC-V based zkVM.
The prover provides a Metamath file and specifies a theorem name to the guest. The guest then returns a receipt which includes the hash of that theorem's statement, a list of hashes of axioms used by the file, and a zero-knowledge proof that that theorem can indeed be proved from the axioms.
First, make sure rustup is installed. This project uses a nightly version of Rust, rustup will automatically install the correct version.
To build all methods and execute the method within the zkVM, run the following command:
cargo run --release
A zkVM program is composed of a host and a guest. The host code runs like any other rust program and launches a zkVM instance using the Prover interface. The guest code is compiled for riscv32im and runs inside a zkVM. Guest code does not have access to std since the zkVM is similar to an embedded system. Use the env in your zkVM guest code to communicate with the host.
We welcome contributions to documentation and code via PRs and GitHub Issues.