Implement the spec's ECSM operand-address constraints

[jotabulacios]

Follow-up to the ECSM address-bound fix (branch fix/ecsm-address-bound-air-executor), and the real fix for the divergence reported in #902.

What the spec says

spec/src/ecsm.toml (landed in the spec's main on 2026-07-20) has no assumption about operand addresses. It constrains them:

• ec:c:range_addr_{xG,k,xR} — IS_HALF over iters = [["i",0,3],["j",0,3]], i.e. all four doubleword addresses of each operand, all four halfwords each.
• ec:c:extrapolate_addr_{xG,k,xR} — addr[i] = ADD(addr[0], 8i) for i = 1..3, with the template's carry propagating into the high limb, so each addr[i] is its own DWordWL column.

What we have

prover/src/tables/ecsm.rs implements neither. It has ADDR_*_0 / ADDR_*_1 and builds each access base as a LinearTerm ADDR_*_0 + 8i with the high limb passed through unchanged:

	spec	ours
address columns per operand	4	1 (base only)
range_addr constraints	3	0 — all five IsHalfword sends in ecsm.rs are on carries and sub-limbs, none on an address
extrapolate_addr constraints	3	0

Because of that our AIR needs the last base to be canonical, and the executor has to guarantee it (ecsm_addr_ok). That precondition is what drifted out of sync with the AIR and produced the seven-value window.

What to do

1. Add the per-access address columns (addr_*[1..3] as DWordHL, 12 columns per operand), their IS_HALF sends, and the ADD carry-pair constraints. prover/src/tables/keccak.rs already does exactly this for its 25 lane pointers — same shape, same range checks.
2. Rewire the 12 MEMW senders to use the per-access column instead of ADDR_*_0 + 8i.
3. Populate the columns in collect_ecsm_memw_ops (prover/src/tables/trace_builder.rs).
4. Add a μ · carry_top = 0 constraint. The spec's ADD template constrains its carries only to be bits (add:c:carry), so it accepts an operand wrapping past 2^64, which Memory::{load,store}_doubleword rejects. keccak.rs has the equivalent for its top lane.
5. Delete ecsm_addr_ok and switch load_u256_le / store_u256_le to checked_add, as the KECCAK path already does.

Notes

• NUM_COLUMNS goes from 667 to roughly 720; trace_builder.rs imports it, so the width change is not local to the table.
• With this in place the AIR accepts strictly more than today (a base crossing the limb becomes provable), so the two executor tests that assert rejection at 0xFFFF_FFE8 become accepted cases and need rewriting. The prover-side tests for an operand crossing 2^32, monolithic and under continuations, stay valid.
• Coordinate with Perf/ecsm affine selector #879, which adds a 64-byte affine operand read as two blocks of four doublewords — under this change it needs no bound of its own.