Refactor of accumulation & more precise R1CS evaluation

[quangvdao]

I don't refactor univariate skip in this PR, instead will wait for the generic sumcheck prover interface to hit first (compute_message and ingest_challenge).

PR Description generated by GPT-5:

Title

R1CS refactor: explicit product-virtual constraints and LHS/RHS swap in final uniform constraint

Summary

• Make product-virtual constraints explicit in r1cs::constraints (previously implicit in spartan/product.rs).
• Swap LHS/RHS for the last uniform R1CS constraint to give Bz a boolean shape.
• Separate compile-time constraint metadata from runtime evaluators; constraints.rs is data-only, runtime logic lives under r1cs::evaluation.
• Align spartan/product.rs with the new API (consume metadata; use typed evaluators; minor API cleanups).

Why

• Explicit product-virtual metadata makes the wiring auditable and shared (no duplication in product.rs), and simplifies verifier/prover agreement.
• LHS/RHS swap for the last constraint changes Bz from flag − 1 to 1 − flag, keeping Bz boolean-sized and consistent with the first-group shape.
• Cleaner separation of concerns improves maintainability and reduces coupling.

Key Changes

• R1CS final constraint “MustStartSequenceFromBeginning”:
  • Upstream: DoNotUpdateUnexpandedPC == 1.
  • This branch: 1 == DoNotUpdateUnexpandedPC (LHS/RHS swapped to keep Bz boolean-shaped).
• Product-virtual constraints:
  • Now defined explicitly as (Az · Bz = output) in r1cs::constraints.
  • ShouldJump is modeled as Jump · (1 − NextIsNoop) on the right factor.
  • spartan/product.rs consumes this metadata and uses a typed product-virtual evaluator; it no longer hardcodes the term list.

Additional small diffs (non-R1CS)

• Field/accumulator APIs (new traits and impls):

/// Unified fused-multiply-add trait for accumulators.
/// Perform: acc += left * right.
pub trait FMAdd<Left, Right>: Sized {
    fn fmadd(&mut self, left: &Left, right: &Right);
}

/// Trait for accumulators that finish with Barrett reduction to a field element
pub trait BarrettReduce<F: JoltField> {
    fn barrett_reduce(&self) -> F;
}

/// Trait for accumulators that finish with Montgomery reduction to a field element
pub trait MontgomeryReduce<F: JoltField> {
    fn montgomery_reduce(&self) -> F;
}

### Design Notes
- `r1cs::constraints` holds only:
  - Uniform constraint names and the ordered table.
  - Grouping for univariate-skip (outer).
  - Product-virtual metadata (names, factor forms, outputs).
- `r1cs::evaluation` holds all runtime evaluators (Az/Bz, folding, product-virtual fused eval).
- `spartan/product.rs`:
  - Univariate-skip first round now uses metadata-provided outputs for base claims.
  - Streaming pass computes endpoints once, then binds remaining rounds; mirrors outer’s delayed-reduction pattern.
  - Inner check remains zero-round but now leverages the explicit factor mapping.

### Correctness
- The LHS/RHS swap is algebraically equivalent; only Bz’s sign/shape changes to a canonical boolean form, consistent with first-group invariants.
- Product-virtual semantics are unchanged; we made the factorization explicit and centralized.

### Compatibility
- Naming aligned to “outer” terminology and explicit product-virtual metadata:
  - Uniform constraints table and names exposed under `R1CS_*` identifiers.
  - Product-virtual term list removed from `product.rs`; use `PRODUCT_CONSTRAINTS`.
- No expected changes to public behavior or proof format; prover and verifier still open the same virtuals at the same points.

### Testing
- Constraint-order invariants checked (enum vs table).
- Product-virtual order preserved; verifier still computes `L(τ_high, r0) * Eq(τ_low, r_tail^rev) * fused_left * fused_right`.

### Follow-ups
- Consider unifying Spartan outer/inner and product-virtual paths further now that factorization and grouping are standardized.

[markosg04]

thanks a lot! just nits/questions

[quangvdao]

@markosg04 Thanks so much for the review! I believe I have addressed all of them (some are put as TODOs for the future).

Once the binary check thing gets fixed then I think this is ready to be merged.