Jolt & Lasso
Read the latest and complete one on my Notion: https://doutv.notion.site/Jolt-Lasso-1591aee049b480b7a44ad7d00e3e9265?pvs=4
Why zkVM?
zkVM VS specialized circuits
✅ Develop zk app without learning zk
✅ Exploit existing compiler infra and tooling
✅ A single circuit can run all programs up to a certain time bound
❌ Much larger Circuit
❌ Any bug in the compiler can render the system insecure
How VM/CPU works?
- Repeatedly execute the fetch-decode-execute logic
- Perform reads and writes to Random Access Memory (RAM)
Watch and understand the animation in RISC-V Simulator
How does Jolt zkVM prove VM execution?
https://excalidraw.com/#json=o6Sc1hlZSN0ZlGQS9aeob,XQusaS02jGZRzzDN0aRAug
Example: Fibonacci
Note: Jolt code tested on 2024.06, some of them maybe outdated
- Rust developer only needs to write this program
#![cfg_attr(feature = "guest", no_std)]
#![no_main]
#[jolt::provable]
fn fib(n: u32) -> u128 {
let mut a: u128 = 0;
let mut b: u128 = 1;
let mut sum: u128;
for _ in 1..n {
sum = a + b;
a = b;
b = sum;
}
b
}let mut program = host::Program::new("fib");
program.set_input(3);- RISC-V Compiler
let (bytecode, memory_init) = program.decode();Decode native RISC-V instructions from ELF file
Even for this simple Fibonacci program, it has 500 instructions
Thus, I use a simple one from an online RISC-V emulator
bytecode: native RISC-V instructions
memory_init:
Jolt Prover
let preprocessing: crate::jolt::vm::JoltPreprocessing<F, PCS> =
RV32IJoltVM::preprocess(bytecode.clone(), memory_init, 1 << 20, 1 << 20, 1 << 22);
let (io_device, trace, circuit_flags) = program.trace();
let (jolt_proof, jolt_commitments) = <RV32IJoltVM as Jolt<_, PCS, C, M>>::prove(
io_device,
trace,
circuit_flags,
preprocessing.clone(),
);RV32IJoltVM::preprocess(bytecode, memory_init)
- Commit to instructions and memory layout
- Generate lookup tables
program.trace()
- simulate execution in RISC-V VM -> get the native execution trace
- Mapping each RISC-V instructions to Jolt instructions -> get the Jolt execution trace
trace io_devicejust like a hard drive
prove()
- Prove the execution trace step-by-step
Jolt Verifier
RV32IJoltVM::verify(preprocessing, jolt_proof, jolt_commitments);Some observations
- Prover and Verifier agree on
preprocessing, which is similar to verification keyvkey - Start from
bytecodeandmemory_init, Jolt doesn’t include a compiler. Typically, we don’t consider compiler bugs.
Visualize Lasso
Lasso Contribution: MLE-structured and Decomposable tables
Jolt Contribution: Design efficient Lasso Lookup tables for RISC-V
Learning Goal: understand Decomposable tables and Offline Memory Checking
https://www.youtube.com/watch?v=iDcXj9Vx3zY
What is Lookup Argument?
Prove \{3, 1, 1\} \subseteq \{1, 2, 3, 4\}
Get Backdoor’s stories in your inbox
Join Medium for free to get updates from this writer.
lookups (possibly repeated) are all contained in the table (distinct values)
Decomposable Tables
Offline Memory Checking
- Online: Merkle hashing that immediately confirm that a memory read was done correctly by insisting that each read includes an authentication path.
- Offline: check the correctness of all read operations “all at once”, after the reads have all occurred
Read-only
Each memory access is conceptually decoupled into a “read” operation and a “write” operation, where the write simply increments the counter.
- Init memory: [5, 9]
$$ I = (address, value, counter)=\{(0,5,0), (1, 9, 0) \} $$
- Read memory[1]
$$ R = \{(1, 9, 0)\} $$
- Write 5 into memory[1], counter+=1
$$ W = \{(1, 5, 1)\} $$
$$ F = \{(0,5,0), (1,5,1)\} $$
$$ I \cup W = R \cup F $$
How about read-write memory checking?
Should we introduce extra constraints?
Read-write
The multiset equality check for read-only memory is not adequate for ensuring the accuracy of read values. It is essential to also verify that each read operation retrieves a value that was written in a previous step (not a future step).
To formalize this, we assert that the timestamp of each read operation, denoted as read_timestamp, must not exceed the global timestamp at that particular step. The global timestamp starts at 0 and is incremented once per step.
The verification of read_timestamp≤global_timestamp is equivalent to confirming that read_timestamp falls within the range [0,TRACE_LENGTH) and that the difference (global_timestamp−read_timestamp) is also within the same range.
MLE: Multi-Linear Extension
MLE: Multi-Linear Extension Motivation: convert Vector -> Polynomial
Before extension: a vector [8, 6, 7, 5, 3, 0, 9] After extension: a multilinear polynomial $q(x_1, x_2, x_3)$ can be evaluated on any points
Univariate index in binary representation -> hypercube index
Design Lookup Tables for RISC-V
Lasso Contribution: MLE-structured and Decomposable tables Jolt Contribution: Design efficient Lasso Lookup tables for RISC-V
Jolt Roadmap
“Jolt-with-curves is what one would want to use when proving statements about elliptic curves (at least, without major advances in proving non-native field arithmetic).”
Jolt-with-Binius-commitment will be much faster as a pure zkVM than alternatives, and will be what people use except when proving statements about curves or proving with very small space (in which case people would use Jolt-with-curves).
On-chain Verifier
Implement on-chain verifier (Solidity, Move, etc.) · Issue #209 · a16z/jolt
- Current verifier is slow and the proof size is huge.
https://github.com/flyq/jolt_verifier_canister
- Verifier on Internet Computer, the JoltPreprocessing is 50MB, proof 500KB+
- Why is JoltPreprocessing large?
- https://jolt.a16zcrypto.com/future/on-chain-verifier.html
- Estimate Solidity verifier cost: >2 million gas
- Groth16 recursion is not easy
Recursion
- No recursion for now
- Today Jolt is a monolithic SNARK. RISC-V traces cannot be broken up, they must be proven monolithically or not at all.
- Require huge memory for large program trace
Questions
- How does Lasso lookup, R1CS, and offline memory checking work together? Why Jolt need R1CS?
- Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?
- How Jolt combined with Binius?
- I tried to verify Schnorr signature using Jolt, it requires 500GB+ memory. why does Jolt consume such a large memory?
Read More
Binius: highly efficient proofs over binary fields
Jolt R1CS — How + why we rewrote Circom in Rust 🦀 | Sam Ragsdale
