Skip to content

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

Closed
sagar-a16z wants to merge 14 commits into
jolt-v2/equivalencefrom
sagar/modular-sdk
Closed

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

Conversation

@sagar-a16z

Copy link
Copy Markdown
Contributor

Summary

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

  • New jolt-host crate: thin host-side wrapper exposing prove_program / verify_proof / ProofBundle. Drives the modular pipeline end-to-end.
  • #[jolt::provable(backend = \"modular\")] macro arg: legacy backend remains the default; opting in routes through jolt-host instead of jolt-core's Jolt prover.
  • muldiv and fibonacci examples flipped to the modular backend. Both prove + verify cleanly:
    • muldiv: prove 4.4s / verify 0.2s / peak RSS 3.24 GiB
    • fibonacci: prove ~3.5s / verify 0.2s / peak RSS 3.22 GiB

Fixture bumped to (log_t=18, log_k_bytecode=14, log_k_ram=14) — the largest shape supported by jolt-kernels' current Stage 6 RA-virtual sumcheck.

Upstream fixes uncovered along the way

  • fix(commitment): pad non-one-hot oracle data to layout num_vars — required for joint_opening_hint::combine_hints to produce a well-defined aggregate commitment. Was silently broken because the only e2e test that exercises this path (jolt-equivalence) doesn't currently compile on this branch (jolt_profiling API drift).
  • feat(jolt-kernels): fix stage5 padding — single-line is_interleaved_operands default was wrong, producing stage6 relation output claim mismatch on any non-trivial guest after the fixture bump. Surfaced because prove_program is the first real consumer that drives static default_prover_programs() end-to-end on the new fixture.
  • fix(macros): set_std emission in modular compile path — guests using libstd were routing to riscv64imac-unknown-none-elf instead of *-zero-linux-musl, breaking serde/crossbeam-utils compile.

Test plan

  • cargo nextest run -p bolt --test commitment_ir — 53/53 pass
  • cargo nextest run -p jolt-hostmuldiv_modular_prove_smoke passes (un-ignored; jolt CLI must be installed, consistent with existing host::Program::new() tests in jolt-core)
  • cargo run --release -p muldivvalid: true, output 2223173
  • cargo run --release -p fibonaccivalid: true, output fib(50) = 12586269025
  • Reviewer: check that the bolt-emit changes in crates/bolt/src/protocols/jolt/emit/rust/commitment.rs match the regen'd output in crates/jolt-prover/src/stages/commitment.rs

markosg04 and others added 14 commits May 8, 2026 00:28
Introduces jolt-hyperkzg, a pairing-based multilinear polynomial
commitment scheme implementing the jolt-openings trait surface.
Generic over `P: PairingGroup`; BN254 is the production instantiation.

Contents:
- scheme.rs: HyperKZGScheme implementing CommitmentScheme and
  AdditivelyHomomorphic; prove/verify built on KZG univariate openings
- kzg.rs: univariate KZG primitives (commit, evaluate, witness
  polynomial division) used internally by the multilinear protocol
- types.rs: HyperKZGCommitment, HyperKZGProof, HyperKZGProverSetup,
  HyperKZGVerifierSetup
- error.rs: HyperKzgError enum
Adds the jolt-witness crate and the supporting modular crate APIs needed before landing the Bolt and generated-code stack.

The new witness crate centralizes Bolt-facing witness/oracle helpers for commitment trace inputs, one-hot chunk materialization, sparse stage 4/5 trace data, stage 6 bytecode/read-RAF/booleanity inputs, and small deterministic oracle helpers used by generated tests.

This also moves the primitive modular crates onto the semantic surface expected by Bolt-generated code: a simplified jolt-field trait bundle, transcript byte-length accounting and MockTranscript, reusable polynomial/source helpers, R1CS row-dot helpers, trace extraction over CycleRow, canonical lookup-table ordering/names, and sumcheck verifier helper modules.

This intentionally does not include the PCS prover/verifier split, Bolt itself, generated prover/verifier/kernel crates, or jolt-equivalence/CI wiring.

Validation:

- cargo clippy -p jolt-witness -p jolt-poly -p jolt-r1cs -p jolt-trace -p jolt-transcript -p jolt-lookup-tables -p jolt-riscv -p jolt-crypto -p jolt-sumcheck -p jolt-openings -p jolt-dory -p jolt-hyperkzg -q --all-targets -- -D warnings

- cargo nextest run -p jolt-witness -p jolt-poly -p jolt-r1cs -p jolt-trace -p jolt-transcript -p jolt-lookup-tables -p jolt-riscv -p jolt-crypto -p jolt-sumcheck -p jolt-openings -p jolt-dory -p jolt-hyperkzg --cargo-quiet
Adds the Bolt compiler/emitter crate and its Jolt protocol lowering, IR, Rust artifact emission, MLIR dialect definitions, templates, and unit tests.

This layer intentionally stops before checking in generated role crates or jolt-equivalence wiring. It depends on the jolt-witness/modular-helper layer below it and prepares the source generator used by the generated-role PR above it.

Validation:

- cargo check -p bolt -q was attempted but is blocked locally by missing llvm-config required by mlir-sys/tblgen.

- Previous downstack modular package validation remains: clippy all-targets and nextest for touched primitive crates.
Add the Bolt-generated kernel, prover, and verifier crates on top of the Bolt emitter branch.

Wire the generated role crates into the workspace and keep their lint suppressions scoped to generated test modules.

Validation: cargo check -p jolt-kernels -p jolt-verifier -p jolt-prover -q; cargo clippy -p jolt-kernels -p jolt-verifier -p jolt-prover -q --all-targets -- -D warnings; cargo nextest run -p jolt-kernels -p jolt-verifier -p jolt-prover --cargo-quiet.
Add the jolt-equivalence crate for comparing the Bolt-generated path against jolt-core, including generated-role parity, real-data/tamper gates, and perf oracle tests.

Wire the crate into the workspace and add focused GitHub workflows plus a local Bolt LLVM/MLIR setup helper.

Validation: cargo check -p jolt-equivalence -q attempted, blocked locally by missing llvm-config / MLIR_SYS_220_PREFIX.
…nd = "modular")]

Adds the modular SDK API surface as a clean overlay on `refactor/crates`,
no protocol changes:

  - New crate `jolt-host` providing `prove_program` + `verify_proof` +
    `ProofBundle`. Drives a guest ELF through the full Bolt stage chain
    (commitment → Stage1..7 → evaluation proof) and rebuilds verifier
    inputs from prover artifacts without re-tracing. Lifted from the
    FR-coprocessor branch (currently `sagar/fr-coprocessor`) with all
    FR-specific plumbing stripped — the architecture is FR-agnostic by
    design; FR is "always on but zero contribution for non-FR guests"
    when it lands.

  - `#[jolt::provable(backend = "modular")]` macro arg. When set, the
    macro emits `compile_<fn>` / `prove_<fn>` / `verify_<fn>` wired to
    `jolt_host::{prove_program, verify_proof}` instead of jolt-core's
    `RV64IMACProver`. `prove_<fn>` returns `(T, ProofBundle)` with the
    guest's typed return value postcard-decoded from `io_device.outputs`.
    Legacy default unchanged.

  - Guardrails in the macro: compile_error when `max_trace_length >
    2^FIXTURE_LOG_T` (currently 2^16 = 65536, matching
    `JoltProtocolParams::fixture() = (16, 10, 16)`), trusted advice, or
    `wasm`. ZK is rejected indirectly — `jolt-sdk` only re-exports
    `jolt_host` / `jolt_trace` when `feature = "zk"` is OFF, so enabling
    zk with the modular backend produces a clean "cannot find `jolt_host`
    in crate `jolt`" build error.

Two enablement changes in `crates/jolt-trace` (same shape as on the FR
branch — these are infrastructure jolt-host needs to exist, not
modular-specific):

  - `BytecodePreprocessing::preprocess_padded(bytecode, entry, min_size)`:
    pads bytecode up to `min_size.next_power_of_two()` so small guests
    reuse a larger goldens-baked fixture without manual regen.
  - `#[macro_export]` on `with_isa_struct!` so jolt-host can use it for
    instruction → lookup-table-index dispatch.

The FR coprocessor work (on `sagar/fr-coprocessor`) is layered on top of
this SDK and will rebase forward after this lands.
…dding

Three coupled changes that together make `prove_program` work for real
example guests (not just fixture-sized ones).

1. **Fixture bump** (`JoltProtocolParams::fixture()` + `jolt_host`):
   (16, 10, 16) → (18, 14, 14). The previous shape only fit guests with
   trace ≤ 2^16, bytecode ≤ 2^10 = 1024 instructions, RAM ≤ 2^16. With
   real-world guests routinely needing 2^13–2^14 bytecode (jolt-sdk
   prelude alone pulls in formatting + allocator code), the old shape
   left `default_prover_programs()` unusable for any meaningful workload.
   New shape matches what bolt was already exercising in its dynamic
   per-test path. Bolt-emitted `jolt-prover` / `jolt-verifier` stages
   regenerated via `JOLT_UPDATE_GOLDENS=1 cargo nextest run -p bolt
   --test commitment_ir generated_jolt_artifacts_have_uniform_crate_layout_and_import_rules`.

2. **Stage 5 padding fix** (`jolt-kernels/src/trace.rs`): pre-existing
   one-line bug — `stage5_lookup_trace`'s missing-cycle branch pushed
   `is_interleaved_operands = false`, but NoOp cycles (the conceptual
   semantics for padding) have `CircuitFlagSet::default()` where
   `is_interleaved_operands()` returns `true`. The divergence flowed
   through Stage 5 lookup-trace witness into Stage 6 bytecode_read_raf's
   round-0 input claim check, producing `stage6 relation output claim
   mismatch` for any guest whose trace is padded. Surfaces on every
   non-trivial guest at the new fixture shape.

3. **Macro cap update** (`jolt-sdk-macros`): `MAX_MODULAR_TRACE_LENGTH`
   bumped from 2^16 to 2^18 to match the new fixture, so users get a
   build-time `compile_error!` if they request `max_trace_length`
   beyond what the shipped goldens support.

One incidental cleanup: removed unused `AdditivelyHomomorphic` import
from regen'd `jolt-prover/src/prover.rs` (bolt-emit produces it
unconditionally even when unused; will fix in bolt-emit later).
…ular")]

Two example guests flipped to the modular SDK, exercising the full
host-side surface: macro-generated `compile_<fn>` / `prove_<fn>` /
`verify_<fn>` driving `jolt_host::prove_program` + `verify_proof`.

  - muldiv: simplest arithmetic guest. prove 2.18s, verify 0.20s,
    output 2223173, valid: true.
  - fibonacci: tiny recursive guest, validates smallest-guest path.
    prove 7.59s, verify 0.20s, output 12586269025 (= fib(50)),
    valid: true.

Host main rewritten to call macro-emitted functions directly — no more
manual preprocessing dance (preprocess_shared / preprocess_prover /
preprocess_verifier / build_prover / build_verifier). The modular path
encapsulates all of that inside `jolt_host`.

Other examples (sha2-ex, stdlib variants, etc.) still ship on the
default legacy backend; flipping them requires either bytecode ≤ 2^14
or a future fixture bump (see Cargo.toml fixture comment).
Two fixes uncovered while investigating libstd guest support on the
modular backend:

1. **6 stale numeric assertions in `bolt::commitment_ir`** — fallout
   from the fixture bump (18, 14, 14). Numeric assertion updates:
   - `trace_length = 65536` → `262144` (log_t 16 → 18)
   - `num_committed = 41` → `42` (bytecode_d 3 → 4 lifts the count)
   - `round_offset = 16` → `14` (stage2 RAM)
   - `round_schedule = [128, 16]` → `[128, 18]` (stage5)
   - `round_schedule = [10, 16]` → `[14, 18]` (stage6 bytecode read raf)
   - `point_zeros.len() = 1` → `2` (stage6)
   - `point_concats` formula extended `+ 1` (stage6)
   Schema rejection message also updated for num_committed = 42.

   Also restored an `AdditivelyHomomorphic` import in
   `crates/jolt-prover/src/prover.rs` that I had pruned manually after
   the regen — but the regen test compares verbatim source against
   what bolt-emit produces, so manual edits break the check. Leaving
   the import (with the cargo unused-import warning) is the right
   choice until bolt-emit gains conditional emission.

2. **Macro `set_std` emission on the modular backend** — bug found
   trying to flip stdlib's `int_to_string` to `backend = "modular"`.
   The legacy `compile_<fn>` emits `program.set_std(true)` when the
   guest crate enables `guest-std`; this routes the build through
   `riscv64imac-zero-linux-musl` instead of `*-unknown-none-elf`. My
   `make_modular_compile_func` was missing those `set_std` /
   `set_backtrace` / `set_profile` calls, so libstd-using guests built
   for the wrong target (downstream crossbeam-utils, serde_core etc.
   failing because std types aren't available on `none-elf`).

   With this fix, libstd guests build correctly. Stdlib still can't
   actually prove on the current `(18, 14, 14)` fixture because
   `int_to_string` produces a 2^18-instruction bytecode + 2^18 RAM
   footprint after compilation (std runtime is heavy) — that needs a
   `(18, 18, 18)` fixture, tracked as separate goldens-bump work.
- `JoltProtocolParams::fixture()` — single-line comment naming the
  kernel ceiling (degree_bound > 5 unsupported), drops the longer
  example-coverage prose.
- `jolt-host` fixture constants — drop the multi-line "Matches bolt's
  fixture() / Kept in sync with macro guard" preamble; the in-source
  call-site assertion in the macro guard is the actual source of
  truth.
- `prove_program` doc — drops stale (16, 10, 16) reference; use
  `FIXTURE_LOG_T` etc. as the constant names rather than spelling out
  values that drift.
- `ProveProgramError::UnsupportedShape` doc — same.
- `assemble_and_prove` — remove `Phase 3:` / `Phase 5:` section
  separators and the 6a..6j step labels; the per-stage helper call
  names already describe what each block does.
- Phase 4 PCS-setup math comment — drops stale `log_t + log_k_chunk =
  16 + 4 = 20` (it's 22 at the current fixture, but the value isn't
  what matters; the formula `params.log_t + params.log_k_chunk` is
  self-explanatory).

No behavior change.
Output of `JOLT_UPDATE_GOLDENS=1 cargo nextest run -p bolt --test
commitment_ir generated_jolt_artifacts_have_uniform_crate_layout_and_import_rules`
against jolt-v2/equivalence base (bolt at 68adcb9) with the bumped
fixture from the previous commit.
The batched commitment plan commits all oracles at the same Dory row_len
(derived from layout_num_vars). One-hot oracles already pad to
2^layout_num_vars via AddressMajorOneHotPolynomial; the non-one-hot
branch was padding to 2^oracle_num_vars instead, producing fewer rows
in the Dory hint vector when oracle_num_vars < layout_num_vars
(e.g. RdInc/RamInc at 18 vars in a batch with layout 22).

When `joint_opening_hint` later combines hints homomorphically via
`combine_hints`, the ragged row counts panic. Even past the panic, the
aggregated commitment Σ γᵢ·Cᵢ would not equal the commitment of the
joint polynomial, which is materialized at main_num_vars — verification
would fail.

Both bolt-emit sites (the muldiv-sparse fast path and the generic
commit_batch fallback) now pad to layout_num_vars / plan.num_vars to
match the one-hot side. This surfaced trying to prove muldiv through
the modular SDK; previously masked because the only e2e test that
exercises this path (jolt-equivalence) doesn't currently compile.
Now passes after fix(commitment): the full modular prove+verify
round-trip works in default cargo nextest invocation. Previously
ignored because the path was broken upstream by the ragged-hint bug.
@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
@sagar-a16z sagar-a16z closed this May 15, 2026
@sagar-a16z sagar-a16z deleted the sagar/modular-sdk branch May 15, 2026 17:25
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.

3 participants