BINIUS-255: bind the reduction claim to the committed trace oracle

[tcoratger]

Closes BINIUS-255.

Ties the AND-check + shift reduction to the committed trace, so the data-parallel M4 prover/verifier now run end to end.

The problem

The reduction crunches the whole batch to one number: the witness, folded over instances at r_rho, evaluated at a random point.

But nothing linked that number to the data committed at the very start.

• A cheating prover could reduce one witness and commit a different one.
• The claim was floating free — about some witness, not the committed witness.
• Without the link, the proof proves nothing.

The idea

The verifier must force: the committed trace, read at the reduction's point, equals the reduced number.

Two mismatches make that look hard:

• The number is folded over instances; the commitment still has every instance separately.
• The number is over single bits; the commitment is packed into $\mathbb{F}_{2^{128}}$ elements.

Both vanish with the right point. The trace's bit index is laid out as [bit | instance | wire], and evaluating a multilinear at a coordinate is a weighted sum over it. So:

• Evaluating the trace's instance coordinates at r_rho performs the instance fold — for free.
• The bit-to-packed gap is exactly what the existing ring-switch handles.

So the single-instance ring-switch is reused verbatim, opening the trace at:

r_j  ||  r_rho  ||  r_y
(bit)   (instance)  (wire)

No new gadget, no new assumption — just the right point.

The change

- Prover::prove / Verifier::verify: standalone commit-open at a random point
+ Prover::prove / Verifier::verify: commit trace -> reduction -> ring-switch -> open, on one transcript

• crates/m4-prover/src/prove.rs — Prover::prove runs the whole protocol; setup builds the shift keys once.
• crates/m4-verifier/src/verify.rs — Verifier::verify runs the whole protocol; the verifier now stores the constraint system.
• crates/{m4-prover,m4-verifier}/src/reduction.rs — module docs updated: the trace-oracle tie is done by the protocol layer, not "a later step".

Soundness

• The instance fold equals evaluating the trace at r_rho on the instance axis — a multilinear evaluation is the eq-weighted sum, so this is exact, not an approximation.
• The point r_j || r_rho || r_y matches the trace layout [bit | instance | wire] coordinate for coordinate.
• Dimensions match exactly: the packed trace has log_hidden + log_inst - 1 elements; the point has 6 + log_inst + log_hidden coordinates, which is elements + 7 (the ring-switch packing width).
• The ring-switch is the same gadget the single-instance protocol uses — no new cryptographic assumption.
• The channel's Elem is $\mathbb{F}_{2^{128}}$, and M4 fixes its one oracle spec directly rather than deriving it against a symbolic channel — so the concrete Elem bound is correct and needs no generalization.

Scope

• new: the full-protocol wiring and two end-to-end tests.
• changed: Prover/Verifier now run the whole protocol (were a standalone commit-open).
• left untouched: intmul / MUL constraints stay out of scope (asserted absent) — that is not part of "andcheck and shift".

Verification

• cargo check, clippy -p binius-m4-prover -p binius-m4-verifier, nightly fmt — clean.
• 29 binius-m4-prover + 3 binius-m4-verifier tests pass, including:
  • protocol_round_trips — a full proof over 64 instances verifies end to end (this is what confirms the point is correct).
  • tampered_opening_is_rejected — flipping one bit of the opening fails with exactly MerkleError(InvalidProof).

🤖 Generated with Claude Code