Fix/ecsm address bound air executor

[jotabulacios]

Give every ECSM operand access its own address column

Closes the divergence reported in #902 by fixing its root cause, so ecsm_addr_ok disappears rather than moving.

What

The AIR built each operand's four doubleword bases as ADDR_*_0 + 8i — a bare field addition on
the low address limb, high limb passed through, no per-access column, no carry, no range check. So
the circuit only needed the last base canonical (+24) while the executor guarded +31, and the
seven low limbs in between were provable executions the reference VM aborts:

operand low limb	reference executor	proof verifies
0xFFFF_FFE0 (last base 0xFFFF_FFF8)	accepts	yes
0xFFFF_FFE1 … 0xFFFF_FFE7	EcsmAddressOverflow	yes
0xFFFF_FFE8 (last base 2^32)	EcsmAddressOverflow	no — LogUp bus does not balance

Third column = the same trace with the guard bypassed, through the production prove/verify path; an
aborted execution yields nothing to prove. Low severity — the bytes land at the arithmetically
correct addresses, it needs an attacker-authored ELF, and the shipped guest sits at high limb
0xFFFF_FFFF where both sides reject — but the accepted set was maintained in two places.

Now every access carries its own address, derived and range-checked in-circuit:

• +36 columns, addr_{xG,k,xR}[1..=3] as DWordHL; the 12 MEMW senders read them instead of
  adding 8i. NUM_COLUMNS 667 → 703
• +21 constraints: nine emit_add_pair additions, two carries each, plus µ·carry_1 = 0 per
  operand. 413 → 434
• +36 IsHalfword sends, with matching lookups in collect_bitwise_from_ecsm — the receive
  multiplicity has to move with the sends or the bus does not balance
• ecsm_addr_ok and ExecutionError::EcsmAddressOverflow are gone. load_u256_le /
  store_u256_le use checked_add, and that is the whole contract: the circuit accepts an
  operand iff addr + 31 < 2^64 and the memory path refuses exactly the complement —
  u64::MAX - 31 runs, u64::MAX - 30 does not. Worth being precise about which table owns
  which half: ECSM's µ·carry_1 bounds addr + 24, and the last byte is bounded one table over,
  where MEMW's per-byte hi = base_1 + carry is never reduced mod 2^32 and lands at 2^32 for
  a base in [u64::MAX-30, u64::MAX-24], which no PAGE token supplies. In-circuit, but a
  cross-table argument, and not reachable through the executor so no test covers it
• Cost is noise: one row per ecall, ~128 rows on a real block, against ECDAS's up to 256 steps per
  call. No prove-time number claimed

The xG/k disjointness guard stays, with its comment corrected: overlap does not make the
trace unprovable — xG is read at T and k at T+1, so an overlapping cell chains through
MEMW normally, and bypassing the guard in a scratch build produced a fully-aliased trace that
verifies. No test here pins that, because the guard is what stops one being built.

Spec

ec:c:range_addr_* and ec:c:extrapolate_addr_* on spec/main (c75966ee, #655) specify exactly
this, and KECCAK already implements the shape for its 25 lane pointers. Two deliberate deviations:

• µ·carry_1 = 0 is ours. The ADD template constrains its carries only to be bits, so
  addr[3] = addr[0] + 24 − 2^64 satisfies the spec as written. Test below.
• range_addr_* covers i = 0..3; we skip i = 0, whose DWordWL form the spec sanctions
  ("could be DWordWLs rather than HLs"). What makes that safe is not the REGISTER table
  range-checking register words — it does not, register.rs has no constraint set at all. It is
  the i = 0 MEMW send putting the pair straight on the Memory bus, where the only tokens come
  from PAGE and REGISTER at canonical (lo, hi) addresses. Every chip taking an address from a
  register leans on the same argument. Worth a second opinion.

Tests

The AIR side of these addresses had no coverage; every existing test was executor-side.

• test_prove_ecsm_derived_bases_cross_limb — the positive case for the new columns: xR at
  0xFFFF_FFFC, so the derived bases carry into the high limb (addr[1] = 0x1_0000_0004). The
  old inline derivation would put a non-canonical low limb on the bus, so this guest is
  unprovable on main. Guest reads the bytes back and commits them; must equal x(5·G)
• extrapolate_addr_rejects_a_wrong_per_access_address — moving addr_*[i] one byte breaks the
  ADD carry, over all three operands and all three i
• addr_wrapping_past_u64_is_rejected — a wrapped last address satisfies all six carry bits and
  is caught only by µ·carry_1; the wrapped address is small and matchable, so what this blocks
  is a collision with live memory. All three operands
• addr_constraints_close_on_padding — every new constraint is µ-gated
• is_half_sends_match_the_collector — the send count against the collector that feeds the
  receive multiplicity. That invariant is what the MSB16 bus bug broke, and only end-to-end
  proving covered it before
• test_prove_ecsm_operand_crossing_limb_boundary — byte carries: xR at 0xFFFF_FFE1, bytes
  read back from across 2^32. This pins the executor relaxation, not the new columns — here all
  four derived bases have hi = 0 and the sends match the old derivation. Same guest under
  continuations, padded so the epoch boundary falls between the write and the read-back
• Executor: the whole top of a limb accepted per operand, only 64-bit overflow refused — from the
  store and from the load

[jotabulacios]

/bench

[github-actions]

Benchmark — real block (ethrex_mainnet_25368371.bin) (median of 3)

_{continuations · epoch 2^22 · 12 epochs}

Metric	main	PR	Δ
Peak heap	47024 MB	46860 MB	-164 MB (-0.3%) ⚪
Prove time	157.521s	156.874s	-0.647s (-0.4%) ⚪

✅ No significant change.

_{Prove-time spread 0.8% (156.749s / 157.939s / 156.874s)}

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

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

No actionable issues found in the PR diff. The executor and ECSM proving changes appear consistent.

[github-actions]

AI Review

PR #913 · 9 changed files

Findings

Status	Sev	Location	Finding	Found by
confirmed	medium	executor/src/vm/instruction/execution.rs:86	Partial write on address overflow in store_u256_le	nemotron openrouter/nvidia/nemotron-3-ultra-550b-a55b

Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro).

AI-001: Partial write on address overflow in store_u256_le

• Status: confirmed
• Severity: medium
• Location: executor/src/vm/instruction/execution.rs:86
• Found by: nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

store_u256_le writes the first 3 doublewords before checking the 4th address; if the 4th overflows, the first 3 have already been committed to memory, violating atomicity of the 32-byte store.

Evidence

Lines 86-95: the function loops i=0..3, does checked_add and store_doubleword for each. If i=3 fails, i=0,1,2 have already executed store_doubleword. The ECSM syscall calls this as the last step (line 453), so a partial xR write could be left in memory on error.

Suggested fix

Check all 4 addresses upfront before any stores: add a pre-loop that validates addr.checked_add(31) (last byte), or check each base with checked_add in a separate loop before the store loop.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	success	1
kimi	openrouter/moonshotai/kimi-k2.7-code	general	success	2
minimax	minimax/MiniMax-M3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
moonmath	zro/minimax-m3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
nemotron	openrouter/nvidia/nemotron-3-ultra-550b-a55b	general	success	3

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	success	1	5	0

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Discarded candidates (5) — rejected by the verifier

• ECSM test helpers still use unchecked address arithmetic (executor/src/tests/ecsm_tests.rs:19, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — The test helpers write_u256_le and read_u256_le at ecsm_tests.rs lines 19-37 are test-only scaffolding called exclusively with small addresses like 0x1000, 0x2000, 0x3000 — they never receive operands near u64::MAX. Test helpers do not need the same defensive checking as production code; they are intentionally simpler. The inconsistency with the production load_u256_le/store_u256_le is a style note, not a bug. No test exercises these helpers at overflow-adjacent addresses, so there is no path to a real failure.
• load_u256_le/store_u256_le doc comments are now incomplete (executor/src/vm/instruction/execution.rs:72, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — The doc comment at execution.rs line 72 says 'Reads a 256-bit little-endian value as four doublewords at addr + 8i' which describes the happy path correctly. The error case (AddressOverflow) is communicated by the return type Result<[u8; 32], MemoryError> — the function signature is self-documenting. The function is private (not pub fn), and Rust idioms don't require every error condition to be documented in prose when the error type already names it. A doc comment addition would be a stylistic nitpick, not a missing piece of information that could cause misuse.
• load_u256_le/store_u256_le checked_add only validates doubleword base, not last byte (executor/src/vm/instruction/execution.rs:73, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The checked_add in load_u256_le/store_u256_le (execution.rs lines 76-78, 90-92) catches base-address wrapping (addr + 8i wrapping u64). Memory::store_doubleword (memory.rs lines 149-164) independently checks address+7 overflow for the bytes within each doubleword access. The two checks have partial overlap — for some addresses store_doubleword's own check would also catch what checked_add catches — but this is not incorrect, it's defense in depth. The redundancy is harmless and ensures validation at the right abstraction level: the caller validates the logical doubleword address, the callee validates the byte-by-byte access. Not an issue.
• Cross-epoch ECSM test relies on assembler li expansion count and ecall landing in second half of a 32-cycle epoch (prover/src/continuation.rs:2056, found by glm:openrouter/z-ai/glm-5.2) — The test at continuation.rs lines 2030-2075 dynamically computes ecall_idx from the actual execution logs (line 2043-2046), then asserts (ecall_idx >> 5) < (first_read_idx >> 5) with a clear error message: 'adjust the nop padding in the .s'. This is NOT a fragile hardcoded assertion — it validates that epoch boundaries fall correctly and tells the developer exactly what to fix if toolchain changes shift the instruction count. The assembly source at test_ecsm_limb_cross.s lines 41-44 documents the design assumption explicitly. The test is consciously designed to fail informatively when its assumptions break. The claim that this is a bug conflates 'documented design constraint' with fragility.
• is_half_sends_match_the_collector only checks count, not value correspondence (prover/src/tests/ecsm_tests.rs:395, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The test at ecsm_tests.rs lines 395-418 is explicitly described (line 390-393) as 'a fast test instead of only end-to-end proving' targeting a specific regression (the MSB16 bus bug). It checks count correspondence between sends and collects. Value-level correctness — that the SAME halfword values are sent and collected — is verified by the end-to-end constraint tests (e.g., constraints_hold_on_generated_trace, test_prove_elfs_ecsm) because mismatched values would unbalance the bus and fail verification. The count check is a targeted sanity test complementing the full suite, not a replacement for it. A per-value comparison at this level would duplicate what the full prover already validates.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.