feat: add field-inline tracing support - #1596
Conversation
|
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. If this PR is a bug fix, refactor, or doesn't warrant a spec, feel free to ignore this message. |
Benchmark comparison (crates) |
0xAndoroid
left a comment
0xAndoroid
left a comment
There was a problem hiding this comment.
This slice doesn't build: the #[cfg] attributes added to jolt-riscv's instruction-list macros break the un-updated impl_inline_instruction! callback in jolt-program, the removed JoltTraceRow re-exports break tracer's trace_row.rs, and the SDK macro calls a JoltSharedPreprocessing::new signature that doesn't exist in this slice's jolt-core (details inline — this accounts for every red build job, plus machete; taplo also wants crates/jolt-lookup-tables/Cargo.toml, jolt-core/Cargo.toml, and tracer/Cargo.toml reformatted).
On the soundness side: I diffed all ~45 ported prefix prefix_mle/update_prefix_checkpoint implementations against the jolt-core originals — zero semantic divergences — and required_prefixes() matches every table's combine() usage. The remaining comments are mostly trace/preprocess strictness mismatches and witness-format ambiguities worth settling before the prover PRs consume these artifacts.
| UnsupportedXlen { xlen: usize }, | ||
| } | ||
|
|
||
| pub fn instruction_lookup_index<const XLEN: usize>( |
There was a problem hiding this comment.
Neither instruction_lookup_index nor JoltLookupQuery has a production caller in this PR, and the per-call validate_xlen Result diverges from jolt-core's infallible LookupQuery::to_lookup_index pattern on what will be a hot path. If this is staging for the next PR, consider landing it with its consumer; either way the XLEN guard can be a const assertion instead of a runtime check.
| cpu: &mut Cpu, | ||
| ) -> FieldInlineTraceData { | ||
| let rd_register = operands.rd.unwrap_or(0); | ||
| let value = u64::try_from(operands.imm) |
There was a problem hiding this comment.
A negative imm silently becomes zero here, while the preprocess-side encoded_immediate rejects it with InvalidImmediate. Unreachable today (both decoders zero-extend a 12-bit field), but the two sides should agree on the failure mode before a non-decode construction path appears.
|
|
||
| impl From<super::SourceInstructionRow> for $name { | ||
| fn from(row: super::SourceInstructionRow) -> Self { | ||
| let mut operands = FormatFieldInline::from(row.operands); |
There was a problem hiding this comment.
This sets operands.op on the SourceInstructionRow path, but the From<JoltInstructionRow> conversion generated by impl_final_jolt_row_data!(@from_row ...) leaves op: None. Execution still works (the macro passes $op directly), but x_register_role() returns None, so x-register state capture silently disappears for LoadFromX/StoreToX if instructions are ever materialized from final bytecode rows. Currently unreachable for field ops, but worth setting op in both conversions to kill the asymmetry.
0xAndoroid
left a comment
0xAndoroid
left a comment
There was a problem hiding this comment.
A few design-direction notes on the lookup-tables port, follow-up to the earlier review.
| j: usize, | ||
| suffix_len: usize, | ||
| ) -> PrefixCheckpoint<F> { | ||
| let _ = (checkpoints, r_x, r_y, j, suffix_len); |
There was a problem hiding this comment.
Forward-looking note: I want to redesign the prefix-suffix mechanism to materialize the entire small 2^16 prefix table up front, which would eliminate update_prefix_checkpoint entirely and shrink this code surface. Not blocking for this port, but worth keeping the checkpoint machinery thin — it may not survive the redesign.
| #[cfg_attr( | ||
| feature = "serialization", | ||
| derive( | ||
| CanonicalSerialize, |
There was a problem hiding this comment.
Why are we still deriving CanonicalSerialize/CanonicalDeserialize here — I thought we were moving off ark serialization in the new stack? It does match the existing serialization-feature pattern in jolt-riscv/jolt-program (kind.rs, row.rs, preprocess/*), so it's consistent with what's landed; flagging the direction question.
4e43270 to
393e9cb
Compare
18ed880 to
9fba45a
Compare
|
Stack maintenance — #1596 is the base of the prover stack and targets Pika validates it against the latest 📚 Stack A: #1596 (this PR) → #1597 → #1598 → #1599 → #1600 → #1601 → #1602 → #1603 #1596 and #1597 are shared by both stacks; each PR targets the one before it. |
- impl_inline_instruction: accept cfg attrs from for_each_instruction_kind - jolt-riscv: restore trace_row module/exports, from_bits, thiserror dep (accidentally dropped while rebasing onto JoltTraceRow foundation) - jolt-riscv: drop dead test-utils feature and unused rand dep (machete) - jolt-sdk/macros: restore committed-bytecode preprocessing from main, re-apply field-inline hook additively - tracer/cpu: restore interrupt_enabled match from main - guests: declare field-inline feature (silences unexpected_cfgs) - jolt-lookup-tables prefixes: lint-clean ported prefix_mle code (unwrap_or defaults, let-else, redundant else, unreachable!) - taplo fmt
Remove prefix_mle and update_prefix_checkpoint from SparseDensePrefix,
the Prefixes dispatch, and all 40 prefix implementations, along with the
Option-based PrefixCheckpoint alias. Prefixes are now computed solely via
per-phase materialization: evaluate() at binary points builds a dense
table at phase start, the table is bound during the phase's sumcheck
rounds, and the fully bound value becomes the next phase's checkpoint.
Rewrite prefix_suffix_test to exercise that flow end-to-end: materialize,
bind HighToLow with random challenges, check combine(prefixes, suffixes)
against the table MLE every round at c in {0,2}, chain checkpoints from
bound values, and compare the final claim against evaluate_mle over the
full 128-variable point, for both RPP=16 and RPP=8 prover configs.
- Decode FIELD_ASSERT_EQ with rd:None to match the tracer shape and avoid the rd=x0 virtual-register rewrite (bytecode/trace operand divergence). - Add FIELD_STORE_TO_X to field_inline_handles_rd_zero so store-to-x0 stays a legal no-op instead of producing an out-of-range x-register. - Reject out-of-range field-register indices in the emulator (was silently clamping, hiding fr16-31 misuse until proving). - Deduplicate the operand-shape match: expose field_inline_operand_shape_for_op in jolt-riscv; jolt-program and the tracer x_register_role delegate to it. - Replace the duplicated &TraceRow JoltCycle impl with a blanket impl for &T. - Delete the orphaned tracer inline_helpers.rs (undeclared, dead InstrAssembler). - Drop the unused centralized LookupTables::required_prefixes table. - Document the inv(0) and store-to-x truncation trace contracts. - Enforce the FieldRegister bound on deserialize via a real Valid::check and re-run FieldInlineBytecodeMetadata::validate() on the deserialize path. - Fix OwnedTrace::next_row so the field-inline feature actually compiles (TraceRow is not Copy under field-inline).
The field-inline feature is not part of host/zk/default, so no existing CI job compiled or tested it — the feature could regress while CI stayed green. Add an explicit clippy invocation and a nextest run over the crates that define it (tracer, jolt-program, jolt-riscv, jolt-lookup-tables).
27f1951 to
8f437ff
Compare
The prover layer re-introduced the streaming prefix_mle / PrefixCheckpoint mechanism into jolt-lookup-tables to satisfy the CPU backend's instruction read-RAF address-phase sumcheck, which reverted the layer-01 refactor 9d4807b (#1596) that dropped it in favor of per-phase materialization. Restore the post-refactor jolt-lookup-tables prefix API (drop prefix_mle, update_prefix_checkpoint, and the Option-based PrefixCheckpoint alias) and migrate the backend to compute prefixes via materialization instead: - materialize each active prefix as a dense MLE per phase via Prefixes::evaluate over the phase's log_m address bits; - bind the prefix polynomials HighToLow in lockstep with the suffix polynomials, reading them in read_checking_message via sumcheck_eval_at_0_and_2; - checkpoint the fully-bound value at each phase boundary, replacing the every-two-rounds Prefixes::update_checkpoints. The per-round sumcheck messages are unchanged, so proofs are identical. Validated: muldiv e2e (host + host,zk), jolt-lookup-tables (307 tests), clippy in both modes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The prover layer re-introduced the streaming prefix_mle / PrefixCheckpoint mechanism into jolt-lookup-tables to satisfy the CPU backend's instruction read-RAF address-phase sumcheck, which reverted the layer-01 refactor 9d4807b (#1596) that dropped it in favor of per-phase materialization. Restore the post-refactor jolt-lookup-tables prefix API (drop prefix_mle, update_prefix_checkpoint, and the Option-based PrefixCheckpoint alias) and migrate the backend to compute prefixes via materialization instead: - materialize each active prefix as a dense MLE per phase via Prefixes::evaluate over the phase's log_m address bits; - bind the prefix polynomials HighToLow in lockstep with the suffix polynomials, reading them in read_checking_message via sumcheck_eval_at_0_and_2; - checkpoint the fully-bound value at each phase boundary, replacing the every-two-rounds Prefixes::update_checkpoints. The per-round sumcheck messages are unchanged, so proofs are identical. Validated: muldiv e2e (host + host,zk), jolt-lookup-tables (307 tests), clippy in both modes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2 participants
Part of the draft Jolt prover stack.
Base:
mainHead:
prover-stack/01-field-inline-tracingAdds field-inline guest/tracer/program wiring and the SDK feature hooks needed by later prover work.
Validation before submission:
cargo fmt -q -- --checkcargo metadata --no-deps --format-version 1gh stack pushsimulation against a temporary bare remotehandoffs/, oldSTACK.md,stack/, and old stack workflow