This repository contains a minimalistic and educational Zero-Knowledge Virtual Machine (ZKVM) implemented using Plonky3. The ZKVM is designed to generate STARK proofs of program execution, providing a simple example for understanding how ZKVMs work.
The Useless ZKVM is a toy implementation designed to:
- Execute a stack-based virtual machine program.
- Capture the execution trace for each instruction.
- Generate a STARK proof for the correctness of the execution.
It utilizes Plonky3 libraries to handle the algebraic and cryptographic operations required for proof generation and verification.
The VM is a stack-based execution environment. It executes a program consisting of basic arithmetic instructions like:
Push
: Push a value onto the stack.Add
: Add the top two stack values.Sub
: Subtract the second stack value from the top.Mul
: Multiply the top two stack values.Div
: Divide the second stack value by the top.
The VM maintains:
- A stack (fixed size of 4 elements).
- A program counter (IP) to track the current instruction.
- A trace log of states for every instruction executed.
The AIR defines constraints for the VM's execution trace. It ensures that the transitions between states in the trace adhere to the VM's instruction semantics. Each operation (e.g., addition, subtraction) is modeled using polynomial constraints.
The VM outputs an execution trace, which is a sequence of states. Each state captures:
- The stack values.
- The current instruction being executed.
- Auxiliary data like remainder values for division.
This trace is later extended and padded for compatibility with the STARK proving system.
The prover:
- Accepts the execution trace from the VM.
- Constructs a STARK proof using the Plonky3 library.
- Verifies the proof by checking that the trace satisfies the AIR constraints.
-
Core Operations:
- Executes stack operations using predefined instructions.
- Maintains a state log for each executed instruction.
-
Key Methods:
run
: Executes the program and captures the trace.perform_operation
: Executes binary operations (e.g., Add, Sub).get_trace
: Outputs the full execution trace.
- Constraints ensure correct state transitions for each instruction type.
- Example constraints:
- Addition: The sum of the top two stack values equals the next stack value.
- Push: Ensures the correct value is pushed onto the stack.
- Captures stack values and auxiliary data at each step.
- Pads the trace to ensure compatibility with STARK requirements.
- Uses Plonky3’s STARK libraries to generate and verify proofs.
- Components include:
- FRI Configuration: Specifies parameters for the proof.
- Challenger: Handles cryptographic challenges.
- PCS (Polynomial Commitment Scheme): Verifies constraints efficiently.
-
Program Execution:
- A sequence of instructions is executed in the VM.
- The state of the VM is logged after each instruction.
-
Trace Construction:
- The VM generates a trace capturing each state transition.
- The trace is extended and padded to fit STARK requirements.
-
Proof Generation:
- The AIR defines constraints that the trace must satisfy.
- The prover constructs a STARK proof, ensuring the trace adheres to the AIR constraints.
-
Proof Verification:
- The proof is verified using the same AIR constraints, guaranteeing the execution's correctness.
-
Create a Program:
- Define a sequence of instructions, e.g.:
let program = vec![ Instructions::Push(Mersenne31::from_canonical_u32(10)), Instructions::Push(Mersenne31::from_canonical_u32(20)), Instructions::Add, Instructions::Push(Mersenne31::from_canonical_u32(40)), Instructions::Sub, ];
- Define a sequence of instructions, e.g.:
-
Initialize the VM:
- Pass the program to the
VM
:let mut vm = VM::new(program);
- Pass the program to the
-
Run the VM:
- Execute the program and capture the trace:
vm.run();
- Execute the program and capture the trace:
-
Generate the Proof:
- Use the AIR to construct a proof:
let vmair = VMAir {}; vmair.generate_proof(vm);
- Use the AIR to construct a proof:
-
Verify the Proof:
- Verify the proof using the same AIR:
verify(&config, &vmair, &mut challenger, &proof, &vec![]);
- Verify the proof using the same AIR:
The Useless ZKVM demonstrates the core principles of zero-knowledge virtual machines:
- Trace construction from program execution.
- Constraint satisfaction using AIR.
- Proof generation and verification using STARKs.
This project is an educational tool, not intended for production use, and serves as a stepping stone for understanding the fundamentals of ZKVMs.