Update MEMW and MEMW_A to match spec

[nicole-graus]

Description:

Implements the spec changes from PRs #434 and #459:

MEMW:

• Rename add_limb_overflow → carry.
• Add IS_BIT[μ_read] and IS_BIT[μ_write] constraints.

MEMW_A:

• Consolidate base_address_high/mid/low (4 cols) into base_address[3]: DWordWHH (3 cols). 29 cols total, down from 30.
• Replace AND_BYTE alignment check with IS_HALF[base_address[0] + mask].
• Add IS_BIT[μ_read] and IS_BIT[μ_write] constraints.
• Fix u16 overflow in collect_bitwise_from_memw_aligned introduced by the IS_HALF change.

[github-actions]

Codex Code Review

1. High | Security/VM soundness: Alignment constraint was weakened and no longer enforces actual alignment bits.

• In memw_aligned.rs:155, the old AND_BYTE(low_byte, mask) == 0 check was replaced with IS_HALF(base_address[0] + mask).
• In trace_builder.rs:871, bitwise lookup generation was changed to match this new rule.
• This only checks that low_half + mask < 2^16, not that low address bits are zero. Example: address ending in ...0001 with width=2 passes IS_HALF(2) but is misaligned.
• Impact: misaligned accesses can enter MEMW_A, violating its assumptions (aligned fast path, no carry handling), which risks incorrect memory semantics and proof unsoundness.
• Fix: restore an explicit alignment-bit check (e.g. low_byte & mask == 0, or equivalent constraints on low bits). If desired, keep the halfword-overflow check as an additional constraint, not a replacement.

No other significant security/bug/performance issues stood out in the PR diff.

[nicole-graus]

/bench

[github-actions]

Benchmark — fib_iterative_8M (median of 3)

_{Table parallelism: 32 (auto = cores / 3)}

Metric	main	PR	Δ
Peak heap	250570 MB	250074 MB	-496 MB (-0.2%) ⚪
Prove time	81.704s	79.482s	-2.222s (-2.7%) ⚪

✅ No significant change.

✅ Low variance (time: 4.3%, heap: 0.4%)

_{Commit: 0ceaeef · Baseline: cached · Runner: self-hosted bench}

[diegokingston]

Code review

No issues found. Checked for bugs and CLAUDE.md compliance.

🤖 Generated with Claude Code

[claude]

Review: Update MEMW and MEMW_A to match spec

Security Fix (High) — IS_BIT constraints on μ_read / μ_write ✓

The new IS_BIT<μ_read> and IS_BIT<μ_write> constraints in both MEMW and MEMW_A fix a real soundness gap. Previously only IS_BIT<μ_sum> was enforced. In Goldilocks, a malicious prover could set μ_read = p−1 and μ_write = 2: their sum is p+1 ≡ 1 (mod p), so IS_BIT<μ_sum> passed. But the individual multiplicity columns held non-bit field values, corrupting the memory multiset argument. These additions are correct and necessary.

Low — debug_assert! stripped in release builds

In collect_bitwise_from_memw_aligned (trace_builder.rs):

let value = low_half + mask;
debug_assert!(value <= 0xFFFF, "misaligned: ...");
let x = (value & 0xFF) as u8;
let y = ((value >> 8) & 0xFF) as u8;

In release builds this assert is elided. If a misaligned op somehow reaches here (value > 0xFFFF), x and y are silently computed from truncated bits, the IS_HALF lookup entry is wrong, and the proof fails in a non-obvious way. Since alignment is now the CPU's responsibility this is unlikely in practice, but assert! (or returning an Err) would make failures loud regardless of build profile.

Note — Alignment check responsibility shift

The AND_BYTE alignment constraint is removed from MEMW_A; IS_HALF[base_address[0] + mask] now only range-checks that the byte span fits in 16 bits. Alignment enforcement moves entirely to the CPU sender. The spec PRs (#434, #459) back this up, but worth verifying the CPU table's constraint set explicitly rejects unaligned accesses for all widths, since MEMW_A will silently accept them if the CPU doesn't.

---

The rename add_limb_overflow → carry, the 4→3 column consolidation for base_address, and all count updates look correct. No other issues found.