Merge main into shrink-cpu-byte-alu (resolve #652 conflicts)

[MauroToscano]

What

Merges latest main into feat/shrink-cpu-byte-alu to clear the merge conflicts on #644.

Since this branch diverged, main advanced only by #652 (soundness: underconstrained chips). #652 added IS_HALFWORD range-checks and wired LT/MUL transition constraints on the same chips this branch reworks — hence the conflicts.

Conflicts resolved (3)

File	Resolution
test_utils.rs	Union of imports (store from this branch + BusId from #652, used by is_halfword_sender_columns).
tables/shift.rs (collect_bitwise_from_shift)	Union — kept both this branch's shift-amount range-checks and #652's input-half (VM-3) checks. The merged bus_interactions carries both sender sets, so both lookup sets are required for the IsHalfword bus to balance. Taking only one side would break bus balance and silently drop a soundness check.
tests/mul_tests.rs	Bus-interaction count 24 (#652) with the ALU receiver label (this branch); wiring-test constraint count 6 → 8, because this branch adds the two SignedIsBit(LHS/RHS) constraints that #652's count predated.

Auto-merge handled the rest correctly: #652's MUL input-half senders + trace lookups (→ 24 interactions) and DVRM n/d senders + lookups (→ 20 IS_HALF) both survived intact alongside the ALU-bus rework.

Note: this branch already adds SignedIsBit(LHS_SIGNED/RHS_SIGNED) to MUL — the exact gap an earlier review of #652 had flagged as missing.

Verification

• cargo build (prover test binary) ✓
• mul / shift / dvrm / lt unit + bus-count + wiring + busless-soundness tests ✓
• End-to-end prove+verify: test_shift_8, sllw, srli_one_zero, mul_8 ✓ — confirms the IsHalfword bus balances with the union resolution.

🤖 Generated with Claude Code

[github-actions]

Codex Code Review

No issues found in the PR diff.

I could not complete a local test run: cargo/rustup attempted to write under read-only /home/runner/.rustup or /home/runner/.cargo paths. I did verify the changed wiring and lookup multiplicities by inspection against the diff and surrounding code.

[claude]

Low — silent false confidence if Linear senders are ever used for IS_HALFWORD

This helper silently drops BusValue::Linear senders (the None arm on line 195). Any future IS_HALFWORD sender written as a Linear value will be invisible here, causing presence-check tests to pass while the range check is actually absent.

The doc comment acknowledges this limitation, but the function name doesn't surface it at call sites — callers read is_halfword_sender_columns(…).contains(&c) as "is this column IS_HALF range-checked" without noticing the Packed-only scope. Consider renaming to is_halfword_packed_sender_columns so the restriction is visible everywhere it's called.

[claude]

Code Review

Overall: This PR correctly closes the VM-3 soundness gap (non-canonical half-decomposition attacks) across MUL, DVRM, and SHIFT, and fixes the silent dead-constraint issue in create_lt_air/create_mul_air. The conflict resolution is well-explained and the new regression tests are a good pattern. Two items to flag:

---

Medium — VM-4: is_negative unconstrained on unsigned-shift rows (deferred, but needs a tracking issue)

SHIFT-C14 sends MSB16[in[3]] → is_negative | signed with Multiplicity::Column(SIGNED), which means the bus provides no binding on is_negative when signed = 0. A malicious prover can set is_negative = 1 on an unsigned SRL/SLL row; the extension = 65535 * is_negative term (SHIFT-C3) then forces arithmetic-right-shift semantics for what should be a logical shift. Any unsigned shift of a value with MSB=1 would produce wrong output that the verifier would accept.

The PR acknowledges this and explicitly defers it (shift.toml omits the constraint). Please ensure there is an open tracking issue for VM-4 before this merges so it doesn't get lost.

---

Low — is_halfword_sender_columns name doesn't surface its Packed-only scope

Flagged inline. The function silently drops BusValue::Linear senders; if a future IS_HALFWORD check is written as a Linear value the presence tests pass while the check is missing. See inline comment for a rename suggestion.

---

Correctness notes (no issues found)

• New n/d IS_HALF senders in DVRM use Multiplicity::Sum(MU_Q, MU_R) — consistent with existing r/n_sub_r/q senders; correct.
• New lhs/rhs IS_HALF senders in MUL use Multiplicity::Sum(MU_LO, MU_HI) — consistent with existing lo/hi senders; correct.
• collect_bitwise_from_mul: per-op count is now 8+4+4+4 = 20; capacity hint matches exactly (MSB16 entries live in a separate second loop and over-fill without triggering reallocation).
• collect_bitwise_from_dvrm: per-op count is 8+4+4+4+1+1 = 22; capacity * 24 is a safe over-estimate.
• Fixing create_lt_air/create_mul_air to wire real constraints (instead of vec![]) is an important correctness fix — the new wiring tests guard against regression.