Use Case: Program Execution

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 guest program execution. What makes program execution its own distinct use case, then, is a slightly more complicated scenario where the ‘program to be proven’ is instead taken as the input to the guest program, which implements an interpreter that reads in the ‘program to be proven’ and executes it within the zkVM.

So, in guest program code something like:

fn digest(program: &ElfFile) -> Vec<u8> { ... }

fn rv32i_interpret(program: &ElfFile) -> Vec<u8> { ... }

#[nexus_rt::main]
#[nexus_rt::private_input(program_to_be_proven)]
#[nexus_rt::public_input(program_digest)]
fn main(program_to_be_proven: ElfFile, program_digest: Vec<u8>) -> Vec<u8> {
    assert_eq!(digest(&program_to_be_proven), &program_digest);

    nexus_rt::print!("Program digest {} validated, executing program... ", program_digest);

    let output = rv32i_interpret(&program_to_be_proven);

    nexus_rt::println!("completed.");

    output
}

At first glance, this pattern may not seem to provide any value over just using program_to_be_proven as the guest program in the first place. But, we can nonetheless highlight a few applications where adding this level of indirection is a surprisingly powerful tool to enhance the utility of the zkVM.

The first is implicit in the example given above: we can declare the program_to_be_proven to be a private input, meaning we can prove private programs — enabling applications such as private smart contracts on a blockchain. Notice that the ability to compare the private program to a public digest enables a verifier to confirm desirable properties of the program used in such a deployment, for example that the private program remains consistent across a variety of invocations, or that it is consistent with a claim of correctness issued by a trusted third-party auditor.

A second potential use, orthogonal to the first and somewhat more technical in nature, is that with this guest program the zkVM can — with some thoughtful guesswork as to maximum stack, heap, and output sizes — implement numerous functionalities with a single fixed program and memory model. This can greatly simplify public parameter management for non-transparent provers which may require per-program setup (though the Stwo prover integration is transparent), as well as simplify design and deployment of smart contracts intended to verify zkVM proofs on-chain.

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.

To start, we will follow along with the SDK Quick Start. After installing the zkVM, we run:

$ cargo nexus host lambda_calculus

to initialize the host and guest programs. We begin by creating a shared library for the guest and host program, which we’ll locate within the guest program crate.

The first part of the library will define terms in the calculus:

lambda_calculus/src/guest/src/common.rs
#![cfg_attr(no_std)]

extern crate alloc;

use alloc::boxed::Box;
use core::fmt::{Debug, Display};
use serde::{Serialize, Deserialize};

#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[repr(transparent)]
pub struct DeBruijnIndex(usize);

impl From<usize> for DeBruijnIndex {
    fn from(value: usize) -> Self {
        Self(value)
    }
}

impl Display for DeBruijnIndex {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "{}", self.0)
    }
}

#[derive(Clone, Debug, Serialize, Deserialize)]
enum Term<R> {
    Var(DeBruijnIndex),
    Lambda(R),
    Apply(R, R),
}

impl<R: Display> Display for Term<R> {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        match self {
            Term::Var(v) => write!(f, "{v}"),
            Term::Lambda(t) => {
                write!(f, "(\\")?;
                write!(f, "{t}")?;
                write!(f, ")")
            }
            Term::Apply(t1, t2) => {
                write!(f, "(")?;
                write!(f, "{t1}")?;
                write!(f, " ")?;
                write!(f, "{t2}")?;
                write!(f, ")")
            }
        }
    }
}

This code block defines an Enum of the possible Terms 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
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Expr(Term<Box<Self>>);

impl Display for Expr {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "{}", self.0)
    }
}

impl PartialEq for Expr {
    fn eq(&self, other: &Self) -> bool {
        self.clone().eval().structural_eq(&other.clone().eval())
    }
}

impl Eq for Expr {}

impl Expr {
    pub fn var<T: Into<DeBruijnIndex>>(binding: T) -> Self {
        Self(Term::Var(binding.into()))
    }

    pub fn lambda<T: Into<Box<Self>>>(inner: T) -> Self {
        Self(Term::Lambda(inner.into()))
    }

    pub fn apply<T1, T2>(left: T1, right: T2) -> Self
    where
        T1: Into<Box<Self>>,
        T2: Into<Box<Self>>,
    {
        Self(Term::Apply(left.into(), right.into()))
    }

    pub fn identity() -> Self {
        Self::lambda(Self::var(0))
    }

    pub fn omega() -> Self {
        let expr = Self::lambda(Self::apply(Self::var(0), Self::var(0)));
        Self::apply(expr.clone(), expr)
    }

    pub fn step(&self) -> Self {
        fn subst(body: Expr, arg: Expr, depth: usize) -> Expr {
            match body.0 {
                Term::Var(i) => {
                    if i.0 == depth {
                        arg
                    } else {
                        Expr::var(i)
                    }
                }
                Term::Lambda(e) => subst(*e, arg, depth + 1),
                Term::Apply(e1, e2) => {
                    Expr::apply(subst(*e1, arg.clone(), depth), subst(*e2, arg, depth))
                }
            }
        }

        // attempt beta reduction
        if let Term::Apply(e1, e2) = &self.0 {
            if let Term::Lambda(e) = &e1.0 {
                return subst(*e.clone(), *e2.clone(), 0);
            }
        }

        self.clone()
    }

    pub fn structural_eq(&self, other: &Self) -> bool {
        match (&self.0, &other.0) {
            (Term::Var(i), Term::Var(j)) => *i == *j,
            (Term::Lambda(e), Term::Lambda(f)) => e.structural_eq(f),
            (Term::Apply(e1, e2), Term::Apply(f1, f2)) => {
                e1.structural_eq(f1) && e2.structural_eq(f2)
            }
            _ => false,
        }
    }

    pub fn eval(self) -> Self {
        let mut curr = self;
        loop {
            let next = curr.step();
            if next.structural_eq(&curr) {
                return curr.clone();
            } else {
                curr = next;
            }
        }
    }
}

The implementation also includes various trait implementations as well as both individual 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
...

[dependencies]
nexus-rt = { git = "https://github.com/nexus-xyz/nexus-zkvm.git", tag = "0.3.0", version = "0.3.0" }
postcard = { version = "1.1.1", default-features = false, features = ["alloc"] }
serde = { version = "1.0", default-features = false, features = ["derive"] }

...

Next, we need to export the common code as a Rust library.

lambda_calculus/src/guest/src/lib.rs
#![no_std]

pub mod common;
pub use common::*;

And lastly we need to make this library visible to the host program.

lambda_calculus/Cargo.toml
...

[dependencies]
nexus-sdk = { git = "https://github.com/nexus-xyz/nexus-zkvm.git", tag = "0.3.0", version = "0.3.0" }
guest = { path = "./src/guest" }

...

Returning to the guest program, as an Expr 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
#![cfg_attr(target_arch = "riscv32", no_std, no_main)]

use guest::Expr;

#[nexus_rt::main]
#[nexus_rt::private_input(program_to_be_proven)]
fn main(program_to_be_proven: Expr) -> Expr {
    program_to_be_proven.eval()
}

Then, we just need a suitable host program that invokes the guest using the private program:

lambda_calculus/src/main.rs
use nexus_sdk::{
    compile::{cargo::CargoPackager, Compile, Compiler},
    stwo::seq::Stwo,
    ByGuestCompilation, Local, Prover, Viewable,
};

use guest::Expr;

const PACKAGE: &str = "guest";

fn main() {
    println!("Compiling guest program...");
    let mut prover_compiler = Compiler::<CargoPackager>::new(PACKAGE);
    let prover: Stwo<Local> =
        Stwo::compile(&mut prover_compiler).expect("failed to compile guest program");

    let program_to_be_proven = Expr::apply(Expr::identity(), Expr::var(42));

    println!("Proving execution of vm...");
    let (view, proof) = prover.prove_with_input::<Expr, ()>(
        &program_to_be_proven,
        (),
    ).expect("failed to prove program");

    assert_eq!(view.exit_code().expect("failed to retrieve exit code"), nexus_sdk::KnownExitCodes::ExitSuccess as u32);

    let output = view.public_output::<Expr>().expect("failed to retrieve public output");

    println!("Reduced expression: {}", output);
}

Meanwhile, as desired verification does not require any access to the private program:

println!("Verifier recompiling guest program...");
let mut verifier_compiler = Compiler::<CargoPackager>::new(PACKAGE);
let path = verifier_compiler.build().expect("failed to (re)compile guest program");

print!("Verifying execution...");
proof.verify_expected_from_program_path::<&str, (), Expr>(
  &(),                                           // at view.public_input
  nexus_sdk::KnownExitCodes::ExitSuccess as u32, // at view.exit_code
  &output,                                       // at view.public_output
  &path,                                         // path to program binary
  &[]                                            // no associated data,
).expect("failed to verify proof");

In this way, we are able to use the zkVM to prove the correctness of executing a private program.

Nexus zkVM