perf(prover): slim MEMW table

[nicole-graus]

Description

This PR Implements the MEMW spec changes introduced in PR #398 ("Losing some MEMW weight"):

• Replace address_add[7] DWordHL columns (28 field elements) with add_limb_overflow[7] Bit columns (7 field elements), making address_add a virtual column computed via BusValue::linear.
• Remove 28 IS_HALFWORD bitwise lookups for address columns.
• Remove 3 LT overflow checks (R1-R3: base_address < base_address + offset): address overflow is now handled implicitly by the carry bit in the virtual formula.
• Replace AddConstraint pairs with IsBitConstraint::unconditional for each overflow bit.

Result: 70 → 49 main columns, 57 → 26 bus interactions.

[github-actions]

Codex Code Review

1. High (Security/Soundness): add_limb_overflow is only constrained as a bit, not as the actual carry

• In the new design, byte addresses are derived from base_address plus a virtual carry bit (add_limb_overflow) in bus expressions (memw.rs:333, memw.rs:410, memw.rs:488).
• But constraints now only enforce overflow ∈ {0,1} (memw.rs:995) and no longer enforce overflow = carry(base_lo + i).
• This allows a malicious witness to choose carry bits arbitrarily and alter effective memory token addresses for bytes 1..7, which is a proof soundness risk.
• Fix: add arithmetic carry constraints (conditioned by width multiplicities) tying each overflow bit to base_address_0 + (i+1); alternatively restore explicit address_add columns + ADD constraints.

2. Medium (Security/Correctness): overflow checks for base_address + offset were removed

• LT overflow checks (R1/R2/R3 style) are no longer emitted; phase 3 now only emits timestamp LT ops (trace_builder.rs:704).
• Correspondingly, MEMW LT bus interactions now cover only timestamp ordering (C4–C7), not address overflow rejection (memw.rs:752).
• If VM semantics require rejecting wrapped accesses near u64::MAX, this PR changes behavior and can admit invalid addresses unless enforced elsewhere.
• Fix: reintroduce explicit overflow rejection constraints or add an equivalent bound constraint ensuring address addition stays within valid 64-bit limb ranges.

[nicole-graus]

/bench

[github-actions]

Benchmark — fib_iterative_2M (median of 3)

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

Metric	main	PR	Δ
Peak heap	122496 MB	116104 MB	-6392 MB (-5.2%) 🟢
Prove time	46.765s	35.116s	-11.649s (-24.9%) 🟢

🎉 Improvement detected — heap or time decreased by more than 5%.

✅ Low variance (time: 2.1%, heap: 0.8%)

Memory Growth

_{Measured with TABLE_PARALLELISM=1 (sequential) · best of 2 samples per point}

Program	Steps	main (MB)	PR (MB)	Δ
fib_iterative_250k	250k	8761	7829	-932 MB (-10.6%)
fib_iterative_500k	500k	13956	10521	-3435 MB (-24.6%)
fib_iterative_1M	1M	20918	16072	-4846 MB (-23.2%)
fib_iterative_2M	2M	32812	26466	-6346 MB (-19.3%)

Growth rate: 10651 MB / 1M steps (main: 13379, Δ: -20.4%)
Fit: R² = 0.9998 (main: 0.9907)

🎉 Memory scaling improvement — growth rate decreased by -20.4%

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

[claude]

Review: Slim MEMW Table

Overall the optimization is clean -- replacing 28 stored DWordHL columns with 7 carry bits and making address_add virtual is a solid structural win. The logic, constraint counting (49 cols, 26 bus interactions, 9 constraints), and trace generation all look correct.

Two issues flagged inline:

Medium -- 64-bit address overflow no longer caught in MEMW

The old R1-R3 LT checks and IS_HALFWORD range checks on address_add columns together prevented proofs where a memory access crossed the 2^64 address boundary. With the virtual formula, addr_add_hi = base_address_1 + overflow[i] can equal 2^32 when base_address_1 = 0xFFFF_FFFF and carry occurs -- a field element distinct from the wrapped address 0. The new design relies entirely on base_address_1 being externally constrained to [0, 2^32). Needs verification or documentation (see inline comment).

Low -- Incomplete test coverage for mixed overflow

test_add_limb_overflow only hits the all-zero and all-one extremes. A case like base_addr_lo = 0xFFFF_FFFE with width=8 would exercise mixed per-byte carry bits (overflow[0]=0, overflow[1..6]=1) and better validate the independent computation.