Skip to content

feat(sdk): #[jolt::provable(backend = "modular")] + modular prove/verify entry points#1535

Open
sagar-a16z wants to merge 9 commits into
jolt-v2/equivalencefrom
sagar/modular-sdk
Open

feat(sdk): #[jolt::provable(backend = "modular")] + modular prove/verify entry points#1535
sagar-a16z wants to merge 9 commits into
jolt-v2/equivalencefrom
sagar/modular-sdk

Conversation

@sagar-a16z
Copy link
Copy Markdown
Contributor

@sagar-a16z sagar-a16z commented May 15, 2026

Summary

Adds the SDK entry points needed to write #[jolt::provable(backend = "modular")] and obtain a working prove/verify round-trip through the modular Bolt-emit prover. Stacks on top of #1515 (jolt-v2/equivalence).

  • Backend::{Legacy, Modular} attribute in common::attributes (legacy is the default — existing call sites are unaffected).
  • New jolt-host crate (~810 LOC) bridges jolt::host::Program + tracer + jolt-prover stages + jolt-verifier into a thin prove_program / verify_proof driver.
  • Macro dispatch in jolt-sdk-macros::build(): the legacy backend continues to emit the existing preprocess_* / build_prover_* / build_verifier_* family; the modular backend emits compile_<fn> / prove_<fn> / verify_<fn> wrapping jolt::modular::*.
  • Examples flipped: examples/muldiv and examples/fibonacci now use backend = "modular" and exercise the ProofBundle round-trip.

End-to-end on this branch (fresh build, fixture (log_t=18, log_k_bytecode=14, log_k_ram=14)):

Example Prove (s) Verify (s) Result
muldiv 2.1 0.17 valid: true
fibonacci 2.3 0.21 valid: true

Bugs uncovered and fixed

Driving real guest traces through the modular prover surfaced three latent prover-side bugs that had not been exercised end-to-end before:

  1. Stage 5 padding produced wrong is_interleaved_operands (jolt-kernels::trace::stage5_lookup_trace).
    The padding branch pushed false, but padding cycles are conceptually NoOp whose default CircuitFlagSet has the interleaved-operands bit set. Result: every padded trace failed with stage6 relation output claim mismatch. Fix: push true in the padding branch.

  2. Bolt-emit commit_oracle (and its commit_batch fallback) produced ragged Dory hints.
    Non-one-hot oracles padded data to 2^oracle_num_vars, while one-hot oracles padded to 2^layout_num_vars. When RdInc / RamInc (natural 2^18) shared a batch with one-hot RA polynomials (2^22), joint_opening_hint::combine_hints panicked with mismatched row counts. Fix: pad non-one-hot data to layout_num_vars so every oracle in the batch yields a uniform-row-count Dory hint.

  3. MemoryImage byte-pair representation can't reconstruct the RAM state the verifier expects.
    Initially, the SDK used TracerBackend::trace + MemoryImage to derive initial_ram_state / final_ram_state. The byte-pair format discards information that jolt_core::zkvm::ram::gen_ram_memory_states reads via Memory::get_doubleword, producing a RAM state that diverges from the verifier's view and triggering stage4 relation input claim mismatch. Fix: drive tracer::trace directly (retains Memory) and call the canonical gen_ram_memory_states. This required exposing tracer::trace_row_from_cycle as pub.

Other upstream changes

The remaining upstream-facing changes are additive or refactors required to make a universal-fixture SDK viable on top of the modular stack:

  1. Fixture bump. bolt::JoltProtocolParams::fixture raised from (16, 10, 16) to (18, 14, 14). This sits at the unchanged Stage 6 DENSE_STAGE6_MAX_DEGREE = 5 ceiling (bytecode_d = ram_d = 4 under log_k_chunk = 4). Verified that log_k_bytecode / log_k_ram cannot be raised further without modifying the kernel.

  2. jolt-program::BytecodePreprocessing::preprocess_with_min_size added; existing preprocess is now a thin min=0 wrapper. Lets SDK consumers pad bytecode to 2^log_k_bytecode for a universal fixture without forking the canonical preprocessing path. Existing callers are unaffected.

  3. Trace-row helpers relocated. extract_trace_rows, cycle_input, and r1cs_cycle_witness moved from jolt-equivalence::core_oracle to jolt-kernels::trace as pub. jolt-kernels already has every required dep; jolt-host now consumes the canonical helpers rather than duplicating them.

  4. Six stale assertions updated in crates/bolt/tests/commitment_ir.rs to track the fixture bump (trace_length, num_committed, round_offset, two round_schedule shapes, and point_zeros / point_concats counts).

Test plan

  • cargo nextest run -p bolt --test commitment_ir — 53/53 pass at the new fixture
  • cargo run --release -p muldivvalid: true, output 2223173 (correct)
  • cargo run --release -p fibonaccivalid: true, output 12586269025 (= fib(50))
  • Reviewer: confirm the bolt-emit edits in crates/bolt/src/protocols/jolt/emit/rust/commitment.rs:728,1278 are consistent with the regenerated output in crates/jolt-prover/src/stages/commitment.rs
  • Reviewer: confirm jolt-kernels::trace is the desired home for the relocated helpers (vs. keeping a pub shim in jolt-equivalence)

Parses `backend = "legacy" | "modular"` from `#[jolt::provable(...)]`.
Default is Legacy (no behavior change). Macro will dispatch on this in a
subsequent commit.
Four small upstream changes that need to land together so a universal
modular SDK fixture works end-to-end:

1. bolt::JoltProtocolParams::fixture (16, 10, 16) → (18, 14, 14).
   Stage 6 RA-virtual caps bytecode_d=ram_d <= 4 via the unchanged
   DENSE_STAGE6_MAX_DEGREE=5 ceiling; (18, 14, 14) hits that limit and
   raises the universal log_t ceiling to 2^18.

2. jolt-kernels trace: stage5 padding pushes
   is_interleaved_operands=true (was false). Padding cycles are
   conceptually NoOp whose default CircuitFlagSet has no
   operand-combination bit, so the flag is true. The false branch
   caused stage6 relation output claim mismatch on any padded trace.

3. bolt-emit commit_oracle (and commit_batch fallback): pad non-one-hot
   oracle data to layout_num_vars / plan.num_vars, not oracle_num_vars.
   Otherwise joint_opening_hint::combine_hints panics ragged hint
   lengths when oracles in the same batch have different natural sizes
   (RdInc=18 vs InstructionRa=22).

4. jolt-program: add preprocess_with_min_size to BytecodePreprocessing,
   leaving preprocess as a min=0 thin wrapper. Lets SDK consumers pad
   bytecode up to 2^log_k_bytecode for a universal fixture; existing
   callers are unaffected.
- Regen goldens via JOLT_UPDATE_GOLDENS=1 cargo nextest run -p bolt
  --test commitment_ir generated_jolt_artifacts_have_uniform_crate_layout_and_import_rules
- Bump 6 stale numeric assertions in commitment_ir.rs:
  - trace_length = 65536 → 262144
  - num_committed = 41 → 42 (bytecode_d went from 3 to 4)
  - round_offset = 16 → 18 (log_t bumped)
  - round_schedule = [128, 16] → [128, 18]
  - round_schedule = [10, 16] → [14, 18]
  - point_zeros.len() = 1 → 2, point_concats.len() += 1
  (last two: shape-driven by the new bytecode_d/ram_d under fixture
  (18, 14, 14))

All 53 commitment_ir tests pass.
Make extract_trace_rows / cycle_input / r1cs_cycle_witness pub in
jolt-kernels::trace (along with private fill_next_fields and
lookup_operands helpers). Previously private to
jolt-equivalence::core_oracle, but consumed by any host-side prove
driver (jolt-host, future SDK).

Trade-off: adds common as a jolt-kernels dep (needed for MemoryLayout
in cycle_input). The kernels crate already pulls in jolt-r1cs,
jolt-program, jolt-witness, jolt-riscv, jolt-field — everything else
the helpers need.

core_oracle.rs's local copies are deleted; it imports from kernels now.
Adds workspace member crates/jolt-host with a stub lib.rs (fleshed out
in the next commit).
810-LOC host-side driver that bridges `jolt::host::Program` + tracer
+ jolt-prover stages + jolt-verifier through the modular Bolt stack.

Key changes vs the pre-rename version (da05c2b):
- Trace ingestion uses tracer::TracerBackend + Program::trace_with_backend
  (returns TraceOutput { trace, device, final_memory: MemoryImage })
  instead of the legacy Program::trace 4-tuple.
- Trace-row helpers come from jolt-kernels::trace (moved upstream in
  the previous commit) instead of the deleted jolt-trace crate.
- BytecodePreprocessing::preprocess_with_min_size replaces the
  preprocess_padded shim.
- with_isa_struct! dispatch macro is gone; instruction → modular
  lookup-table index now goes via jolt-core's InstructionLookup +
  a verbatim copy of core_lookup_table_to_modular_index.
- Lookup-table count via <LookupTableKind<XLEN> as EnumCount>::COUNT
  (modular side) — was hardcoded 40 before.
- build_ram_states rewritten for MemoryImage byte-pairs (vs old
  tracer::Memory doubleword API).

Public surface mirrors the original:
  prove_program(program, inputs, untrusted, trusted) -> ProofBundle
  verify_proof(&bundle, program) -> Result<(), VerifyProgramError>
- jolt-sdk gains a `host`-feature dep on jolt-host and re-exports its
  surface as `jolt::modular::{prove_program, verify_proof, ProofBundle,
  ProveProgramError, VerifyProgramError}`.
- jolt-sdk-macros: parses the `Backend` attribute (legacy default vs
  modular) and dispatches in `build()`. New helpers
  `make_modular_compile_func`, `make_modular_prove_func`,
  `make_modular_verify_func`, and `make_modular_guard` emit the modular
  surface (single Program, ProofBundle round-trip) instead of the
  legacy preprocess/build_prover/build_verifier triple.
- tracer: expose `trace_row_from_cycle` as pub so jolt-host can drive
  `tracer::trace` directly (retaining `Memory` for
  `gen_ram_memory_states`) without losing the byte-level memory
  structure that `MemoryImage` discards.
- jolt-host: use `Program::trace` + `gen_ram_memory_states::<ark_bn254::Fr>`
  for RAM state — earlier MemoryImage-based path produced different
  init/final cells than the verifier expects and triggered "stage4
  relation input claim mismatch".
- examples/muldiv + examples/fibonacci flipped to
  `#[jolt::provable(backend = "modular")]`; main.rs rewritten for the
  ProofBundle round-trip.

Validated end-to-end: muldiv prove 2.1s / verify 0.17s / valid:true;
fibonacci prove 2.3s / verify 0.21s / valid:true.
@github-actions
Copy link
Copy Markdown
Contributor

Warning

This PR has more than 500 changed lines and does not include a spec.

Large features and architectural changes benefit from a spec-driven workflow.
See CONTRIBUTING.md for details on how to create a spec.

If this PR is a bug fix, refactor, or doesn't warrant a spec, feel free to ignore this message.

@github-actions github-actions Bot added the no-spec PR has no spec file label May 15, 2026
- jolt-host: drop unused `tracing` workspace dep
- jolt-equivalence: drop `jolt-riscv` dep (its uses were eliminated when
  trace-row helpers moved to jolt-kernels::trace earlier in the stack)
- Apply `cargo fmt` to touched files
1. bolt::verifier_cleanup LOC budget: bump GENERATED_VERIFIER_TARGET_LOC
   from 6_000 to 6_050. The fixture shape change (16, 10, 16) →
   (18, 14, 14) grew the regenerated verifier surface by 9 LOC (larger
   round-schedule arrays and more descriptor entries at the new log_t /
   log_k_bytecode). Re-tighten when the surface drops back below.

2. jolt-sdk verifier_api test: revert examples/fibonacci to the legacy
   backend so `cargo run -p fibonacci -- --save` regenerates the
   tests/fixtures/{fib_proof.bin, fib_io_device.bin,
   jolt_verifier_preprocessing.dat} that `verify_proof` loads. The
   modular ProofBundle is a different serialization shape;
   RV64IMACProof::from_file can't decode it.

3. WASM Verifier E2E: target-gate jolt-host away from wasm32 in
   jolt-sdk's Cargo.toml. The `host` feature was pulling jolt-host into
   the wasm verifier build, which transitively required jolt-dory; the
   dory-pcs `ArkworksProverSetup::new_from_urs` ctor is gated on
   `cfg(not(target_arch = "wasm32"))`, so the wasm build broke. jolt-host
   is the modular prover driver — it's never used at verify time and
   never compiled for wasm. Same target gate on the
   `jolt::modular` re-export in host_utils.rs.

To keep a modular-backend example in the tree after reverting fibonacci,
flip examples/alloc to `backend = "modular"`. Validated locally:
prove 2.1s / verify 0.17s / valid:true.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

no-spec PR has no spec file

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant