feat: add R1CS extension foundations#1598
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. |
0xAndoroid
force-pushed
the
prover-stack/02-jolt-claims-protocol-formulas
branch
from
941c1b4 to
4344fe3
Compare
0xAndoroid
force-pushed
the
prover-stack/03-r1cs-extensions
branch
from
d736494 to
6ac2f06
Compare
|
Stack maintenance — rebased onto #1597 ( 📚 Stack A: #1596 → #1597 → #1598 (this PR) → #1599 → #1600 → #1601 → #1602 → #1603 #1596 and #1597 are shared by both stacks; each PR targets the one before it. Conflict resolution
|
|
Claude code review session started: https://claude.ai/code/session_01QkiBw7VPFYPPVdBDnKTKAy |
moodlezoup
left a comment
moodlezoup
left a comment
There was a problem hiding this comment.
Reviewed the R1CS foundations across the nonnative-field, EC-gadget, Poseidon-transcript, polynomial, and BlindFold/sumcheck additions. No soundness-critical issues found — the nonnative Fq-in-Fr arithmetic (range checks, carry chains, modular-reduction uniqueness), the Grumpkin EC gadgets, and the Nova-fold/Spartan structure all check out, and the split-eq/Lt/Lagrange/one-hot ports are validated against dense references. The inline comments are mostly latent (these foundations have few or no callers yet), but worth pinning down before they get wired up.
A few smaller notes not worth inline comments:
poseidon.rs: the in-circuit transcript only self-validates against a hand-rolledNativeTranscriptin the same file, not against the actualjolt-corePoseidonTranscriptit's meant to reproduce bit-for-bit. There are two divergent native transcripts in the repo (LE/32-byte/n_roundsvs BE/31-byte/length-prefixed); the gadget matches the former. A pinned known-answer test against the real prover transcript would catch silent desync.split_eq.rs:275-315:e_out_in_for_window/e_active_for_windoware caller-less and untested, with index math guarded only bydebug_assert!. Add tests against a dense reference or defer to the PR that introduces a caller.nonnative.rs:CARRY_BITS = 68is load-bearing for both completeness and the no-wrap soundness argument (honest max carry is 66 bits) — worth a WHY comment.prove.rsBlindFold outer/inner sumcheck accumulation loops are serial in the dominant first rounds (unlike thepar_iterhot sumchecks in jolt-core); fine for a small verifier R1CS but worth revisiting if the circuit grows.
Generated by Claude Code
| pos: Limbs<5>, | ||
| neg: Limbs<5>, | ||
| } |
There was a problem hiding this comment.
pos/neg are only Limbs<5> (320 bits), but fmadd_magnitude adds terms up to value (~254 bits) × scalar (~64 bits) ≈ 2^318, and add_assign_trunc::<5> truncates with no overflow check or debug_assert. Summing only a few full-width terms wraps silently and reduce() returns a wrong value with no signal (confirmed empirically). Nothing calls this yet so it's dormant, but fmadd_u64/add accept arbitrary Fr values, so a caller passing full field elements gets silent corruption. Unlike WideAccumulator/FrSignedProductAccumulator (u128 slots, documented headroom), the capacity here is undocumented. Either widen to u128-based slots or document the small-value precondition on SignedScalarAccumulator and add a debug_assert on the carry-out limb.
Generated by Claude Code
| fn pack_bytes(bytes: &[AssignedScalar<Fr>]) -> AssignedScalar<Fr> { | ||
| assert!( | ||
| bytes.len() <= 32, | ||
| "Poseidon byte chunks must fit in one BN254 scalar" | ||
| ); | ||
| let mut value = zero(); | ||
| let mut lc = LinearCombination::zero(); | ||
| let mut coefficient = Fr::from_u64(1); | ||
| let radix = Fr::from_u64(256); | ||
| for byte in bytes { | ||
| value += byte.value * coefficient; | ||
| lc = lc + byte.lc.clone().scale(coefficient); | ||
| coefficient *= radix; | ||
| } | ||
| AssignedScalar::new(value, lc) | ||
| } |
There was a problem hiding this comment.
pack_bytes computes Σ byte_i · 256^i over the byte witnesses' lc but never range-constrains each byte to [0,256). The native from_le_bytes_mod_order has no such freedom, so for the gadget to bind to a canonical byte string the caller must guarantee each Byte is in range — otherwise a malicious witness (e.g. byte_0 = 256, byte_1 = 0 vs byte_0 = 0, byte_1 = 1) produces the same packed scalar and the same transcript state from different "byte strings", breaking the binding of absorb_bytes. This obligation is currently undocumented on R1csByteTranscript::Byte/absorb_bytes. Either range-check internally or document the [0,256) invariant prominently.
Generated by Claude Code
| append_vector_opening( | ||
| transcript, | ||
| b"bf_witness_opening", | ||
| b"bf_witness_blind", | ||
| &proof.witness_opening, | ||
| ); |
There was a problem hiding this comment.
Transcript asymmetry: the verifier appends bf_witness_opening/bf_witness_blind here, but the prover (prove.rs, after open_rows for the folded witness) never appends it — it only appends bf_error_opening. Harmless today since this is the last transcript op and no challenge is derived afterward, but it's a real prover/verifier divergence. If this BlindFold transcript is ever chained into a larger protocol (the stated direction of this stack), the verifier's transcript state will diverge from the prover's. Either append it on the prover side too, or drop this append.
Generated by Claude Code
| fn constant_mul_terms(lhs: [u64; NUM_LIMBS], rhs: [u64; NUM_LIMBS]) -> [BigUint; MUL_LIMBS] { | ||
| let mut terms = std::array::from_fn(|_| BigUint::zero()); | ||
| for (lhs_index, lhs_limb) in lhs.into_iter().enumerate() { | ||
| for (rhs_index, rhs_limb) in rhs.into_iter().enumerate() { | ||
| terms[lhs_index + rhs_index] += BigUint::from(lhs_limb) * BigUint::from(rhs_limb); | ||
| } | ||
| } | ||
| terms | ||
| } |
There was a problem hiding this comment.
constant_mul_terms is a byte-for-byte copy of convolution_terms above (lines 521-529). Both callers (the product convolution at line 300 and the modulus·quotient reduction at line 314) can share a single helper — drop one.
Generated by Claude Code
| fn fmadd_magnitude(slots: &mut [u128; 8], value: Fr, magnitude: Limbs<4>) { | ||
| let value = value.inner_limbs(); | ||
| for i in 0..4 { | ||
| for j in 0..4 { | ||
| let product = (value.0[i] as u128) * (magnitude.0[j] as u128); | ||
| slots[i + j] += (product as u64) as u128; | ||
| slots[i + j + 1] += ((product >> 64) as u64) as u128; | ||
| } | ||
| } | ||
| } | ||
|
|
||
| #[inline] | ||
| fn normalize(slots: [u128; 8]) -> Limbs<9> { | ||
| let mut out = [0u64; 9]; | ||
| let mut carry = 0u128; | ||
| for (index, slot) in slots.into_iter().enumerate() { | ||
| let (sum, overflow) = slot.overflowing_add(carry); | ||
| out[index] = sum as u64; | ||
| carry = (sum >> 64) + ((overflow as u128) << 64); | ||
| } | ||
| out[8] = carry as u64; | ||
| Limbs(out) | ||
| } |
There was a problem hiding this comment.
The 4×4 u128-slot product loop and the normalize carry-propagation pass here are identical to wide_accumulator.rs (fmadd/normalize), differing only in Limbs<9> vs BigInt<9> return type (which interconvert via arkworks/mod.rs). This signed-product accumulator is essentially two wide accumulators (pos/neg) plus a sign branch in reduce. Extract a shared fmadd_into(slots, a, b) + normalize(slots) so the carry logic lives in one place.
Generated by Claude Code
0xAndoroid
force-pushed
the
prover-stack/02-jolt-claims-protocol-formulas
branch
from
91dbcf2 to
62aab06
Compare
0xAndoroid
force-pushed
the
prover-stack/03-r1cs-extensions
branch
from
0efc262 to
774da69
Compare
3 participants
Part of the draft Jolt prover stack.
Base:
prover-stack/02-jolt-claims-protocol-formulasHead:
prover-stack/03-r1cs-extensionsAdds shared R1CS, transcript, polynomial, field, BlindFold, and crypto foundations used by protocol wrappers.
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