The Lambda VM proves correct execution of a RISC-V (RV64IM) program against an input stream. The pipeline has five artifacts and four transformations.
- Source code — high-level Rust (using
syscalls/for guest-host I/O) or RISC-V assembly. - ELF binary — the program in the VM's ISA, ready to load.
- Execution record — per-instruction logs emitted by running the ELF on the VM.
- Witness — a set of trace tables (CPU, decode, MEMW, LOAD, bitwise, branch, LT, shift, MUL, DVRM, page, register, halt, commit, keccak, …) derived from the execution record. Each table is an AIR (Algebraic Intermediate Representation); tables are linked by LogUp lookup arguments.
- Proof — a multi-table STARK proof (transparent, hash-based, post-quantum secure) that the witness satisfies all AIR constraints and lookup arguments. Low-degree of the witness polynomials is verified via FRI.
- Compiler —
rustccross-compiles to the custom RISC-V target spec (executor/programs/riscv64im-lambda-vm-elf.json) and produces the ELF. Thelambda-vm-syscallscrate exposes guest-side syscalls (commit,get_private_input,print_string,keccak_permute,sys_halt). - Executor (
executor/) — loads the ELF, runs the program against the VM's memory and register state, handles syscalls and precompiles (e.g. Keccak), and emits the per-instruction logs. - Witness generator (
prover/src/tables/) — turns the logs into trace tables, populates AIR columns, and computes the LogUp auxiliary columns that connect tables. - Proof system (
crypto/stark/) — commits to each table's trace via Merkle trees, samples challenges via Fiat-Shamir, and runs FRI for the low-degree test. Produces aMultiProof; the verifier replays the transcript and checks all AIR and lookup constraints.
For a deeper dive into each component see the proof system overview.