RISC-V
RISC-V is an open-source instruction set architecture (ISA) based on reduced instruction set computer (RISC) principles. Every RISC-V implementation includes a base integer ISA, with optional extensions for additional functionality.
Supported Instructions
Jolt currently supports the RV64IMAC instruction set, comprising the 64-bit integer instruction set (RV64I), the integer multiplication/division extension (RV64M), the atomic memory operations extension (RV64A), and the compressed instruction extension (RV64C).
RV64I (base)
RV64I is the base 64-bit integer instruction set: 32 registers (x0--x31, each 64 bits wide, with x0 hardwired to zero), 32-bit fixed-width instructions, and a load/store architecture (all arithmetic operates on registers; memory is accessed only via dedicated load/store instructions with base-plus-offset addressing). It provides arithmetic, logical, shift, branch, and jump operations.
For detailed instruction formats and encoding, refer to chapter 2 of the specification.
"M" extension (integer multiply/divide)
Adds signed and unsigned multiplication (MUL, MULH, MULHU, MULHSU) and division/remainder (DIV, DIVU, REM, REMU), plus their 32-bit W-type variants. Divide-by-zero produces a well-defined result rather than a trap.
For detailed instruction formats and encoding, refer to chapter 7 of the specification.
"A" extension (atomics)
Adds atomic read-modify-write operations (AMOSWAP, AMOADD, AMOAND, AMOOR, AMOXOR, AMOMIN, AMOMAX) and load-reserved/store-conditional (LR/SC) pairs, each in word (32-bit) and doubleword (64-bit) variants.
Jolt's LR/SC implementation
Jolt implements LR/SC using virtual sequences with a pair of width-specific reservation registers:
reservation_w(virtual register 32) -- used byLR.W/SC.Wfor word (32-bit) reservationsreservation_d(virtual register 33) -- used byLR.D/SC.Dfor doubleword (64-bit) reservations
The two reservation registers enforce width-matched pairing: LR.W sets reservation_w and clears reservation_d; LR.D does the reverse. This cross-clear means SC.W after LR.D (or SC.D after LR.W) will always fail, since the SC checks only its own width's reservation register.
The SC failure path uses prover-supplied VirtualAdvice constrained to . On success, a constraint forces the reservation address to match rs1, and rs2 is stored to memory. On failure, the store is a no-op (the original memory value is written back). The destination register rd receives 0 on success, 1 on failure. Both reservation registers are always cleared at the end of any SC instruction, per the RISC-V specification.
For the constraint design and soundness argument, see RISC-V emulation. For the virtual register layout, see Registers.
For detailed instruction formats and encoding, refer to chapter 8 of the specification.
"C" extension (compressed instructions)
Provides 16-bit encodings for common operations, reducing binary size by ~25--30%. Compressed instructions map directly to their 32-bit RV64I equivalents and can be freely intermixed with them; the Jolt tracer expands them before execution.
For detailed instruction formats and encoding, refer to chapter 16 of the specification.
Compilation via LLVM
Jolt proves execution of RISC-V ELF binaries, which can be produced from any language with an LLVM frontend (Rust, C, C++, etc.). The jolt-sdk crate handles cross-compilation to the RISC-V target automatically via the #[jolt::provable] macro. The compilation pipeline is:
Source (Rust/C/C++) → LLVM IR → RISC-V ELF → Jolt tracer → proof
