Introduction
As this walkthrough describes a more advanced use case for the zkVM, we recommend reviewing both the SDK Quick Start and the simpler Stable Matching walkthrough first. By definition, a zkVM is designed to prove the correctness of a program’s execution. However, a more advanced use case arises when the program to be proven is not the code running directly in the zkVM, but is instead provided as input to the zkVM. In this case, the zkVM executes an interpreter as its guest program, which then reads, interprets, and runs the input program inside the zkVM. This effectively allows the zkVM to generate a proof for the execution of arbitrary, dynamically supplied programs. Consider the following guest program in whichprogram_to_be_proven
is nested inside as input to the zkVM
program_to_be_proven
directly as the guest program? However, this level of indirection unlocks powerful capabilities that significantly expand the utility of the zkVM.
Enabling Private Program Execution
The first benefit, illustrated by the example above, is the ability to treat the program to be proven as a private input. This allows the zkVM to prove the execution of programs without revealing their source, making it possible to build private smart contracts on-chain, among other use cases. By comparing the program’s digest to a public input, verifiers can still check meaningful properties such as:- Consistency of the private program across multiple invocations can be checked.
- Conformance to a known, audited version without exposing implementation details can be verified.
Generalization Across Programs with a Single zkVM Binary
A second, more technical benefit is that this structure enables the zkVM to handle a wide range of programs through a single, fixed guest binary — the interpreter. With careful planning around memory constraints (e.g. stack, heap, and output size bounds), this pattern allows:- The proving key and public parameters can be shared and reused across many programs, which simplifies definitions for non-transparent provers which may require per-program setup.
- Deployment pipelines for applications and smart contracts verifying zkVM proofs on-chain can be simplified significantly.
- Systems using non-transparent proving systems can be managed more easily, even though they often require per-program setup (note: the
Stwo
prover used here is transparent).
The Lambda Calculus Model
Instead of working through this design at the full complexity of the RISC-V32i instruction set, we will work through a simpler example of the core concept using a much more fundamental computational model: the lambda calculus.Implementation
To start, we will follow along with the SDK Quick Start. After installing the zkVM, we run:Shared Library
The first part of the library will define terms in the calculus:lambda_calculus/src/guest/src/common.rs
Enum
of the possible Term
s available: an indexed Var
, a Lambda
function definition, and an Apply
function application, as well as some useful trait implementations for constructing and debugging. In the rest of the library, we’ll define full expressions in the calculus, which amount to programs that are “executed” via reduction.
lambda_calculus/src/guest/src/common.rs
step
and iterative eval
routines that reduce the statement into a stable form.
In order to make our common library work across both the host and guest, we have a few quick steps we need to handle. First, we need to update the guest crate to depend on serde
, which the library uses for serializing and deserializing the Expr
structs to and from the zkVM:
lambda_calculus/src/guest/Cargo.toml
lambda_calculus/src/guest/src/lib.rs
lambda_calculus/Cargo.toml
Guest Program
Returning to the guest program, as anExpr
is a program in the lambda calculus, we can now implement our (dead simple) interpreter — for simplicity, we omit any hash-based consistency checking:
lambda_calculus/src/guest/src/main.rs
Host Program
Here we create a suitable host program that invokes the guest using the private program:lambda_calculus/src/main.rs