Two bugs in Jolt

Authors

Sunghyeon Jo

Background

Jolt proves execution of RISC-V programs. The program being proven is the guest, while the host compiles the guest, runs the prover, and calls the verifier.

To generate a proof, Jolt’s tracer records VM execution and generates auxiliary witness data used to prove the execution efficiently.

Internally, Jolt encodes trace data, memory, and advice inputs as tables represented by polynomials. The prover commits to those polynomials, and the verifier later checks openings, which are claimed evaluations of committed polynomials at chosen points. Jolt uses sumcheck to reduce large claims about polynomial tables into smaller opening claims that the verifier can check.

The two bugs discussed here occurred in different parts of that pipeline: one in the verifier’s trusted-advice reduction checks, and one in the tracer’s witness generation for a RISC-V instruction.

Soundness Break: TrustedAdvice Binding

The Intended Binding

The first bug involves Jolt’s advice-input mechanism. Unlike a normal public-input proof, where the verifier can fully examine the program input, an advice-input proof can pass data to the guest without revealing it to the verifier.

TrustedAdvice<T> is the wrapper for host-provided advice where the verifier receives a public commitment, a cryptographic binding to that advice data. In Jolt’s own documentation, TrustedAdvice<T> is similar to untrusted advice, except an external party commits to the input. The intended statement is:

I know a value that matches this public trusted-advice commitment,

and running the guest program with that value produces this output.

The guest program reads the value like an ordinary Rust value by dereferencing the wrapper:

#[jolt::provable]
fn trusted_output(rounds: u64, secret: jolt::TrustedAdvice<u64>) -> u64 {
    let mut acc = *secret; // `acc: T`
    for i in 0..rounds {
        acc = acc
            .wrapping_mul(6_364_136_223_846_793_005)
            .wrapping_add(i);
    }
    acc
}

The host side has two different views of that value:

Prover: receives the trusted-advice value and executes the guest with it.
Verifier: receives the trusted-advice commitment.

Again, the relevant property for this bug is binding: VM execution must use the same value committed to by the verifier’s public trusted-advice commitment. If this property is violated, a proof can execute with one value while satisfying verification with a commitment to another.

Claim Reduction

Internally, Jolt verifies trusted advice by making claims about an advice polynomial, which encodes trusted-advice memory. A reduction protocol processes that claim stage by stage, turning a large claim into a smaller opening claim that the verifier can check efficiently.

Conceptually, the opening point is split as (cycle, address). A useful analogy is CPU execution with RAM:

Cycle coordinates: which clock cycle the VM performed the advice read, indexing into the execution trace.
Address coordinates: which trusted-advice memory address the VM read from, indexing into the trusted-advice memory layout.

The Vulnerability: The Stage 7 Skip

In the normal flow, the reduction operates as a three-stage chain. Stage 6 binds the cycle coordinates and outputs an intermediate claim. Stage 7 consumes that intermediate claim, binds the remaining address coordinates, and outputs the final claim. Stage 8 then takes that final claim and checks it against the public commitment.

Stage 7 is conditional, meaning that if Stage 6 already binds every advice coordinate, then no address coordinates remain and the proof validly skips Stage 7. In this case, the chain must shorten to two steps: Stage 6 must output the final claim directly, handing it straight to Stage 8.

When no address rounds remained, the verifier skipped Stage 7:

if params.num_address_phase_rounds() > 0 {
    params.phase = ReductionPhase::AddressVariables;
    instances.push(advice_reduction_verifier_trusted);
}

The verifier stores advice-opening claims in a claim accumulator. In the code, that accumulator is keyed by names such as AdviceClaimReductionCyclePhase and AdviceClaimReduction. The first name represents the intermediate claim from the cycle phase. The second name represents the final advice-opening claim that Stage 8 checks against the public commitment.

The vulnerability arose because the verifier failed to link the accumulator claims correctly when the chain was shortened. Upon Stage 7 being skipped, the vulnerable code still fetched the intermediate opening for Stage 6:

ReductionPhase::CycleVariables => {
    accumulator
        .get_advice_opening(params.kind, SumcheckId::AdviceClaimReductionCyclePhase)
        .expect("Cycle phase intermediate claim not found")
        .1
}

This created a broken chain: the verifier checked Stage 6’s execution reduction against the intermediate claim (AdviceClaimReductionCyclePhase), while Stage 8 checked the public commitment against the final claim (AdviceClaimReduction).

Normally, Stage 7 acts as the bridge connecting those two accumulator keys. Without Stage 7, the intermediate claim and the final claim were left isolated from each other. Because they were disconnected, a malicious prover could satisfy Stage 6 with execution over EXECUTED_SECRET and independently satisfy Stage 8 with an opening against the public commitment to COMMITTED_SECRET. The verifier accepted the forged proof because it never enforced that the Stage 6 claim and the Stage 8 opening came from the same advice polynomial.

Skipping Stage 7

Jolt runs Stage 7 only if num_address_phase_rounds() > 0, meaning some address coordinates remain after Stage 6. The default trusted-advice size is 4096 bytes, or 512 64-bit words. Representing 512 advice words as a multilinear polynomial requires 9 opening coordinates, because 512 = 2^9.

With Jolt’s default proof-data layout (CycleMajor with Dory), a padded trace length of at least 4096 lets Stage 6 bind all 9 coordinates from the cycle side. No address coordinates remain, so num_address_phase_rounds() == 0, which puts the verifier on the no-Stage-7 path.

The Fix

The patch makes Stage 6’s output depend on whether an address phase will follow. If address rounds remain, Stage 6 still outputs the intermediate AdviceClaimReductionCyclePhase. If no address rounds remain, Stage 6 outputs the final scaled AdviceClaimReduction relation:

ReductionPhase::CycleVariables if params.num_address_phase_rounds() > 0 => {
    accumulator
        .get_advice_opening(params.kind, SumcheckId::AdviceClaimReductionCyclePhase)
        .expect("Cycle phase intermediate claim not found")
        .1
}
ReductionPhase::CycleVariables | ReductionPhase::AddressVariables => {
    let advice_claim = accumulator
        .get_advice_opening(params.kind, SumcheckId::AdviceClaimReduction)
        .expect("Final advice claim not found")
        .1;

    advice_claim * params.final_advice_output_scale(sumcheck_challenges)
}

This restores the missing check: if Stage 6 is the last advice reduction, the verifier checks it against the same final advice-opening relation that Stage 8 later uses for the public commitment.

Jolt also patched the analogous zk output-constraint path in a16z/jolt#1485.

Bug 2: REMW Trace Completeness

The second bug came from a different component, the RV64 tracer. Specifically, Jolt’s REMW trace sequence was problematic in a mathematical edge case.

The i32::MIN Edge Case

REMW is the RV64 signed 32-bit remainder instruction. It takes the low 32 bits of both operands, computes a signed 32-bit remainder, then sign-extends the 32-bit result back to 64 bits. The RISC-V unprivileged ISA defines division by zero explicitly: the remainder is the dividend.

Concretely:

low32(rs1) = 0x80000000
low32(rs2) = 0
REMW result = sign_extend_32(0x80000000) = -2147483648

The Trace Failure

The tracer failed to correctly accommodate this edge case. While Jolt’s architectural REMW::exec path correctly executed the instruction semantics, the tracer used a different mechanism: instead of directly proving the division result, it introduced helper advice values, including the quotient and absolute remainder, and proved the relation d*q + r == a.

In the i32::MIN % 0 case, the honest advice value for the absolute remainder is r = 2^31, which is a valid u32 whose 31st bit is set. However, the vulnerable REMW trace sequence incorrectly enforced that this value fit within 31 bits:

asm.emit_i::<SRAI>(*t2, *a3, 31); // Sign bit of remainder
asm.emit_b::<VirtualAssertEQ>(*t2, 0, 0);

For a3 = 2^31, the evaluation of SRAI(a3, 31) is 1, causing Jolt’s internal VirtualAssertEQ trace assertion to panic even though the architectural execution itself was valid. As a result, the prover rejected an honest witness for a valid REMW execution, constituting a completeness failure.

a16z/jolt#1473 had already changed the sibling DIVW path to allow the full unsigned 32-bit advice range. REMW still had the old bound, so the REMW i32::MIN % 0 trace case remained incomplete.

The Fix

The fix mirrors the DIVW bound:

asm.emit_i::<SRAI>(*t2, *a3, 31); // Sign bit of remainder
asm.emit_i::<SRAI>(*t2, *a3, 32); // Remainder advice fits in u32

With the merged fix, the tracer accepts the honest 2^31 remainder advice for the i32::MIN division-by-zero case.

Discovery

Interestingly, while the two bugs were found in different subsystems, the reasoning process used to find them was similar.

For the trusted-advice bug, QED followed ownership of verifier claims across optional phases. A skipped phase was dangerous here because it normally connected an intermediate claim to the final verifier check. A related univariate-skip output-claim fix made that branch worth checking.

For the REMW bug, QED started from the nearby DIVW fix and asked whether sibling instructions still had the same edge-case bound. This insight led directly to REMW, where architectural execution and trace generation disagreed on the i32::MIN divide-by-zero case.

Both findings resulted from careful analysis of boundary edge cases. The trusted-advice bug arose when Stage 7 was skipped due to the absence of address-derived advice variables, while the REMW bug arose from the specific i32::MIN % 0 division input. The lesson is the same in both cases: edge-case review must consider not only the local assertion, but also the surrounding protocol state that gives the assertion its meaning.