feat: extend Jolt claim protocol formulas#1597
Conversation
18ed880 to
9fba45a
Compare
27f1951 to
8f437ff
Compare
941c1b4 to
4344fe3
Compare
|
Claude code review session started: https://claude.ai/code/session_01FNR82Crof9atPbqeKS2a11 |
|
Stack maintenance — rebased onto #1596 ( 📚 Stack A: #1596 → #1597 (this PR) → #1598 → #1599 → #1600 → #1601 → #1602 → #1603 #1596 and #1597 are shared by both stacks; each PR targets the one before it. Conflict resolution
Follow-up CI fix ( Local validation
|
moodlezoup
left a comment
There was a problem hiding this comment.
Reviewed the Rust changes (specs/*.md skimmed as docs). This is verifier-side claim scaffolding for the prover stack; most new helpers are exercised only by their own tests so far. Opening-point orderings, the proof_commitment_order reorder (now matching the prover's all_committed_polynomials), and the SameEvaluationAs refactor all check out. A few notes below.
Minor / non-blocking:
jolt-poly/src/dense.rs:sumcheck_round_eval_with_orderhas no callers (all 25 sites usesumcheck_round_eval). Fine if a later stack entry needs it; otherwise drop it.field_inline/formulas/dimensions.rs:read_write_opening_point/validate_phase_split/FieldRegistersReadWriteOpeningPointare a near-verbatim copy of the jolt-sideReadWriteDimensionsversions. Consider sharing the phase-split helper.jolt-poly/src/eq.rs:boolean_index_msb'sindex.checked_shl(1)?guards the shift amount (always 1), not value overflow, so it never returnsNoneon >64-var points. Not reachable from current callers, but the guard is misleading.
Generated by Claude Code
| where | ||
| F: Field, | ||
| { | ||
| Polynomial::new(EqPolynomial::<F>::evals(stage1_cycle_binding, None)) |
There was a problem hiding this comment.
hamming_booleanity_eq_cycle_polynomial builds the eq table without reversing its cycle point, unlike every sibling (ra_virtualization_eq_cycle_polynomial here at L363, the instruction version, and eq_address_cycle_polynomial), which all .rev() first. The prover treats RAM hamming-booleanity and RAM ra-virtualization identically (both GruenSplitEqPolynomial::new(¶ms.r_cycle.r, LowToHigh) over a big-endian r_cycle), so the verifier helpers should be symmetric. The only test here is tautological (evals(x) == evals(x)) and there's no live caller yet. Please confirm the intended orientation of stage1_cycle_binding before this is wired up — if the caller passes the same big-endian point the other helpers receive, this table will be bit-reversed relative to the hamming_weight polynomial it multiplies.
Generated by Claude Code
| [ | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldRs1Value), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldRs2Value), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldRdValue), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldProduct), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldInvProduct), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::Add, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::Sub, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::Mul, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::Inv, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::AssertEq, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::LoadFromX, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::StoreToX, | ||
| )), | ||
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | ||
| FieldInlineOpFlag::LoadImm, | ||
| )), | ||
| ] |
There was a problem hiding this comment.
This re-types the exact 13-entry sequence already declared in FIELD_INLINE_SPARTAN_OUTER_R1CS_INPUTS above, and the test just asserts the two are equal via map. Map the const directly:
| [ | |
| outer_opening(FieldInlineVirtualPolynomial::FieldRs1Value), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldRs2Value), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldRdValue), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldProduct), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldInvProduct), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::Add, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::Sub, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::Mul, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::Inv, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::AssertEq, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::LoadFromX, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::StoreToX, | |
| )), | |
| outer_opening(FieldInlineVirtualPolynomial::FieldOpFlag( | |
| FieldInlineOpFlag::LoadImm, | |
| )), | |
| ] | |
| FIELD_INLINE_SPARTAN_OUTER_R1CS_INPUTS.map(outer_opening) |
Generated by Claude Code
| /// | ||
| /// Consumers must enforce these in the same constraint system as the input and output | ||
| /// claims; treating them as metadata can leave alternate opening chains unbound. | ||
| pub consistency: Vec<JoltConsistencyClaim<F>>, |
There was a problem hiding this comment.
This drops the soundness-contract warning that previously documented consistency (consumers must enforce these in the same constraint system; treating them as metadata can leave alternate opening chains unbound). The field's behavior is unchanged, but that's a load-bearing, easy-to-misuse invariant — worth keeping the doc comment.
Generated by Claude Code
Benchmark comparison (crates) |
91dbcf2 to
62aab06
Compare
Part of the draft Jolt prover stack.
Base:
prover-stack/01-field-inline-tracingHead:
prover-stack/02-jolt-claims-protocol-formulasExtends the Jolt claim formulas, including field-inline protocol formulas and supporting specs.
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