1.
Intro
2.
Usage
2.1.
Quickstart
2.2.
Guests and hosts
2.2.1.
Guests
2.2.2.
Hosts
2.3.
Runtime Advice
2.4.
Profiling
2.4.1.
zkVM profiling
2.4.2.
Guest profiling
2.5.
Troubleshooting
3.
How it works
3.1.
Architecture overview
3.1.1.
RISC-V emulation
3.1.2.
R1CS constraints
3.1.2.1.
Spartan
3.1.3.
Registers
3.1.4.
RAM
3.1.5.
Instruction execution
3.1.6.
Bytecode
3.1.7.
Batched opening proof
3.2.
Twist and Shout
3.3.
Dory
3.4.
Optimizations
3.4.1.
Batched sumcheck
3.4.2.
Batched openings
3.4.3.
Inlines
3.4.4.
Small value optimizations
3.4.5.
EQ optimizations
3.4.6.
Torus compression
3.5.
Formal Verification
3.5.1.
Z3 Verifier
3.6.
Appendix
3.6.1.
Terminology and nomenclature
3.6.2.
Multilinear extensions
3.6.3.
Sumcheck
3.6.4.
Polynomial commitment schemes
3.6.5.
Memory checking and lookup arguments
3.6.6.
RISC-V
3.6.7.
Jolt 0.1.0
3.6.8.
Additional resources
4.
Roadmap
4.1.
Streaming
4.2.
Recursion
4.3.
Zero Knowledge
4.4.
On-chain verifier
4.5.
Precompiles
Light (default)
Rust
Coal
Navy
Ayu
JoltBook
Formal Verification
This section describes formal verification efforts and tooling in the Jolt codebase.
Z3 verifier