BINIUS-255: compose the AND-check and shift reduction into the M4 protocol

[tcoratger]

Part of BINIUS-255. One step toward the M4 protocol; does not close the issue (the trace-oracle tie remains).

Chains the two batched reductions into one reduction on a shared transcript, for prover and verifier. No new cryptography — just the glue.

The problem

The batched AND-check (BatchAndCheckWitness::prove / verify_bitand_reduction) and the shift reduction (shift::prove feeding the single-instance shift::{verify, check_eval}) existed as standalone building blocks, each exercised only by its own test with hand-built inputs. Nothing composed them on one Fiat-Shamir transcript.

The idea

Run them back to back, the AND-check's output feeding the shift reduction:

   all AND rows  (A & B == C over K * n_and rows)
        │  AND-check
        ▼
   claimed A, B, C at a random row point  +  bit challenge r_z
        │  split the row point, fold the witness over instances
        ▼
   shift reduction
        ▼
   one evaluation claim about the instance-folded witness

The batch-specific step: the AND-check's row point is (constraint, instance). Split it — the constraint part r_x (low) feeds the shift reduction; the instance part r_rho (high) says how to fold the K instances into one before the shift runs.

Why this is correct given the codebase

• It is the batched shape of the single-instance protocol (crates/verifier/src/verify.rs), which already threads bitand → shift in this order — so the Fiat-Shamir ordering is unchanged.
• The exact threading (split r_x/r_rho, fold at r_rho, feed r_x to the shift) is precisely the wiring the existing shift.rs round-trip test already validated; the only change is that r_x, r_rho, and the operand claims now come from the shared transcript rather than being sampled by the test.
• The existing reductions are reused unchanged; this PR only adds the glue.

Scope

• new: m4-prover::prove_reduction, m4-verifier::verify_reduction, and their output structs.
• only AND constraints: MUL is rejected up front (there is no batched intmul check yet), rather than silently passing a zero claim that would skip the MUL checks.
• stops at the witness claim: binding it to the committed trace oracle — which binds r_rho and bridges the bit witness to the packed commitment via a batched ring-switch that does not exist yet — is a later step, flagged in both module docs.
• the CRC-64 test fixture moves from shift.rs to a crate-level #[cfg(test)] mod crc64, so the shift and reduction tests share it without one test module reaching into another's.

Verification

• cargo test -p binius-m4-prover (28) and -p binius-m4-verifier (3) — pass
• clippy --all-targets, +nightly fmt -- --check — clean
• reduction_round_trips: prover and verifier agree on r_rho, the challenge point, and the eval; and the reduced claim equals the true instance-folded witness evaluated at the shift point.
• tampered_transcript_is_rejected.

Note

This branch is cut from main, which still has ValueTable2 (the rename in #1770 is open). When #1770 lands, this is a trivial ValueTable2 → ValueTable rename here.

🤖 Generated with Claude Code

[jimpo]

Hell yeah! This looks super clean. A couple comments, and this'll need a rebase because of the ValueTable rename.

[tcoratger]

Hell yeah! This looks super clean. A couple comments, and this'll need a rebase because of the ValueTable rename.

Just fixed the comments and the conflicts with main :)

[jimpo]

follow-up: It would be best to pass this domain into verify_bitand_reduction too (but the pre-isomorphism version). That would ensure it's consistent between andcheck and shift, by construction. On the prover side too.