Add extra constraints to prevent register side effects in CPU32 padding rows

[RobinJadoul]

No description provided.

[github-actions]

Codex Code Review

Findings:

• Low / Potential bug: spec/src/cpu32.toml only gates register read/write side effects on padding rows (μ = 0). A padding row can still set ALU = 1, because the ALU lookup at line 316 is multiplicity-gated by ALU, not μ. If the goal is “no side effects on padding rows,” add !μ => ALU = 0 at minimum. Consider ADD/SUB too if padding rows should be completely inert.

• Low / Documentation bug: spec/cpu32.typ says padding rows have μ = 1, but the chip padding value is μ = 0 and the new constraints use !μ for padding. This should say μ = 0 to avoid contradicting the constraints.

[claude]

Potential gap: ALU interaction multiplicity is not gated on μ

The three new constraints correctly prevent register read/write side effects in padding rows. However, there is a similar interaction in the alu group:

[[constraints.alu]]
kind = "interaction"
tag = "ALU"
...
multiplicity = "ALU"

ALU is constrained to be a bit, but there is no constraint !μ => ALU = 0. A malicious prover could set ALU = 1 in a padding row (μ = 0) and inject a spurious entry into the ALU logup bus. Whether this is exploitable depends on whether the ALU chip has independent constraints preventing it from matching against rows not associated with real instructions.

If the ALU chip is not separately constrained, a !μ => ALU = 0 constraint should be added here alongside the three existing ones.

[RobinJadoul]

ALU should be free of side-effects, and is similarly not gated on word_instr in the CPU chip

[claude]

Review: Add extra constraints to prevent register side effects in CPU32 padding rows

Summary: This PR fixes a real ZK soundness bug — padding rows (μ = 0) could previously be used by a malicious prover to inject spurious register reads/writes into the logup argument via the MEMW interactions. The fix is logically correct.

What's correct

• The three arithmetic constraints (!μ => read_register1 = 0, !μ => read_register2 = 0, !μ => write_register = 0) are correctly expressed. The polynomial (1 - μ) * flag = 0 correctly encodes the implication since both μ and the flags are bits.
• Placement in the logup group is reasonable since these protect the logup argument's soundness.

Issues found

1. Redundant IS_BIT for μ (inline comment on line 290): The PR adds a second IS_BIT constraint for μ in the range group, but one already exists at the top of the same group (~line 205). Harmless to the circuit but creates a duplicate in the rendered spec.

2. Potential soundness gap — ALU interaction (inline comment on lines 358–371): The ALU interaction uses multiplicity = "ALU" which is not gated on μ. Unlike the register-access multiplicities fixed by this PR, a prover could set ALU = 1 in a padding row and send a spurious entry to the ALU logup bus. Whether this is exploitable depends on the ALU chip's own constraints — worth verifying explicitly.