ECSM operand addresses: the AIR accepts 7 addresses the executor rejects (implementation deviates from spec/src/ecsm.toml)

[MauroToscano]

Demonstration only — not for merge. This branch adds a PoC harness and, to run it, gates the
executor's ecsm_addr_ok guard behind an env var. It is here to document a finding and let you
reproduce it, not to be merged.

Summary

The ECSM AIR accepts operand addresses that the executor rejects. A witness whose operand low limb
falls in a 7-value window balances every bus and verifies, while cli execute on the same
input aborts with EcsmAddressOverflow.

The spec got this right — this is an implementation deviation, not a spec gap.
spec/src/ecsm.toml specifies both the address range checks and carry-correct derivation of the
per-access addresses; prover/src/tables/ecsm.rs implements neither. Details in
Root cause below. Nothing needs to be
designed to fix this — the constraints already exist on paper and simply are not built.

The executor's ecsm_addr_ok guard is a compensating control for that deviation, and because the
guard and the AIR constrain different things, their accepted sets drifted apart — which is where
the window comes from.

One caveat on provenance: spec/src/ecsm.toml currently lives on the spec/ecsm branch and has not
been merged into spec/main, so the constraints are specified but not landed. That is worth
resolving alongside the code, since an unlanded spec is easy for a second implementation to miss.

Severity is low: nothing is forged, no address is aliased, and the reachable gain is
halt-vs-continue on an attacker-authored program. Filing it because it is a real
prover/verifier-vs-executor divergence in a shipped table, and because the spec deviation behind it
is worth correcting on its own terms.

The divergence

ecsm_addr_ok(addr, 31) (executor/src/vm/instruction/execution.rs) requires
(addr mod 2^32) + 31 < 2^32, i.e. lo32 <= 0xFFFF_FFE0.

The AIR only needs lo32 <= 0xFFFF_FFE7. ECSM sends its four doubleword accesses as
base_lo = ADDR_*_0 + 8i, base_hi = ADDR_*_1 — a bare field addition on the low limb with no
carry column. Each of those four bases must therefore be a canonical low limb, so the binding
constraint is lo32 + 24 < 2^32. The trailing 7 bytes of the last doubleword are fine, because
general MEMW carries bytes 1..7 correctly (prover/src/tables/memw.rs: byte 0 uses the raw
(BASE_ADDRESS_0, BASE_ADDRESS_1) pair, bytes 1..7 use
base_0 + i - 2^32*carry[i], base_1 + carry[i]).

Gap = lo32 ∈ [0xFFFF_FFE1, 0xFFFF_FFE7], 7 values per operand, plus a mapped page at high
limb hi + 1.

Reproduction

cargo test --release -p lambda-vm-prover poc_ecsm -- --test-threads=1

a0 low limb	reference executor	proof verifies
0xFFFF_FFE0 (off 32)	accepts	✅ positive control
0xFFFF_FFE1 (off 31)	EcsmAddressOverflow	✅ gap
0xFFFF_FFE7 (off 25)	EcsmAddressOverflow	✅ gap
0xFFFF_FFE8 (off 24)	EcsmAddressOverflow	❌ rejected — LogUp bus does not balance

The off=24 / off=25 boundary is the load-bearing detail: it is exactly the ±1 the mechanism
predicts (byte 0 of doubleword 3 sits at ADDR_0 + 24 with no carry), which is what distinguishes a
real mechanism from a harness that accepts everything.

Two supporting tests:

• poc_plain_sd_across_limb_boundary — a plain 8-byte sd at 0xFFFF_FFFC spanning into high
  limb 1 is executor-accepted and provable. The VM supports limb-crossing accesses generally;
  only the ECSM ecall refuses them.
• poc_ecsm_limb_gap_31_shows_pages_above_2p32 — the off=31 proof's declared runtime pages are
  0xFFFC_0000 and 0x1_0000_0000, confirming the write really did spill past 2^32.

Verification goes through the production prove_with_options / verify_with_options path. The
only source change is the env-var gate on ecsm_addr_ok — trace builder, AIR definitions and
verifier are untouched. Bypassing the executor guard is the point: a malicious prover builds traces
with its own tooling and is not bound by the reference executor, so the question that matters is
whether the verifier accepts the trace.

Root cause: the implementation does not follow the spec

spec/src/ecsm.toml (on spec/ecsm) specifies two things the implementation omits.

1. Range-check every address, not just the base — ec:c:range_addr_xG:

kind = "interaction"
tag = "IS_HALF"
input = [["idx", ["idx", "addr_xG", "i"], "j"]]
iters = [["i", 0, 3], ["j", 0, 3]]
multiplicity = "μ"

IS_HALF over i = 0..3: all four doubleword addresses, both halves each.

2. Derive the per-doubleword addresses with real addition — ec:c:extrapolate_addr_xG:

kind = "template"
tag = "ADD"
input = [["cast", ["idx", "addr_xG", 0], "DWordWL"], ["cast", ["*", 8, "i"], "DWordWL"]]
output = ["cast", ["idx", "addr_xG", "i"], "DWordWL"]
iter = ["i", 1, 3]

So in the spec each addr_xG[i] is its own DWordWL column, tied to the base through the ADD
template — full 64-bit addition, carry into the high limb included.

prover/src/tables/ecsm.rs has no addr_xG[i] columns at all. It has ADDR_XG_0/ADDR_XG_1 and
builds each access base as a LinearTerm ADDR_XG_0 + 8i with base_hi = ADDR_XG_1 passed
through unchanged. No per-access column, no ADD, no carry, no IS_HALF. The same applies to
addr_k and addr_xR.

With the spec's constraints in place the window cannot exist: IS_HALF on all four addresses forces
each to be a canonical 32-bit-limbed value, and ADD propagates the carry, so the AIR's accepted
set is the executor's.

For contrast, KECCAK does implement this shape — it carry-propagates its lane addresses with real
carry pairs and needs no executor precondition.

Impact

• Not an arbitrary write, value forgery, or address aliasing. Within the window MEMW's carry
  columns compute the arithmetically correct 64-bit addresses, so the bytes land where a correct
  RV64 machine would put them.
• The only false statement provable is "this program did not halt". Exploiting it needs an
  attacker-authored ELF that places such an address in an operand register, and the deployed guest
  is pinned by the DECODE commitment.
• Unreachable for the shipped guests: ecsm_oracle uses [u8; 32] stack arrays, and
  STACK_TOP = 0xFFFF_FFFF_FFFF_FFF0 puts them at high limb 0xFFFF_FFFF, where hi + 1 = 2^32
  is not representable by any page — so the stack case is blocked outright, independent of the low
  limb.

Suggested direction

Implement ec:c:range_addr_* and ec:c:extrapolate_addr_* as written: per-access address columns
derived via ADD, with IS_HALF on each. That makes the AIR self-contained and lets
ecsm_addr_ok be relaxed or dropped.

Do not "fix" this by relaxing the executor guard from +31 to +24. The two guards accept
incomparable sets, not nested ones. The AIR is more permissive on the low limb but strictly
less permissive on the high limb: whenever lo32 >= 0xFFFF_FFE1 the tail bytes carry, so the
AIR needs hi <= 0xFFFF_FFFE. Relaxing the executor to +24 would accept
hi = 0xFFFF_FFFF operands the AIR cannot prove, converting a low-severity soundness gap into
a liveness bug on honest executions. +31 is the unique offset-only bound that is hi-independent:
it guarantees no byte of the 32-byte operand ever crosses 2^32, so no carry is needed anywhere.

Relatedly, addr_limb_ok's doc comment states that a straddling operand "makes the trace
unprovable". That is true of the +8i base derivation but false of MEMW's within-row bytes, and
it is the assumption the 7-value window lives in.

Note on scope

The HINT table added in #876 reproduces the same ADDR_OUT_0 + 8i shape and has the same window;
that instance is addressed separately. This PR is only about ECSM on main.

[MauroToscano]

Adjudication finished. Two additions, one of which settles the fix-direction question with evidence I did not have when I opened this.

The +31 guard was a deliberate tightening from +24 — this window is already a known, tested case

executor/src/tests/ecsm_tests.rs:159-176:

// Every operand's last accessed byte must stay in the limb (+31); the 0xFFFF_FFE1
// cases are the off-by-7 window the old +24 bound for xR/xG let through.

It then asserts EcsmAddressOverflow at 0xFFFF_FFE1 for both xR and xG. Guard and test landed together in abfb0cbd (#657).

So +24 is not merely a weaker bound — it is the bound this repo already reviewed and rejected, naming this precise 7-value window. That independently confirms the recommendation in the description above: the AIR moves, the executor stays at +31. Relaxing it would revert a reviewed hardening and invalidate an existing passing test.

A second reason beyond that: +24 is an artifact of MEMW's dword-granular carry apparatus, so adopting it would make ECSM's validity depend on a MEMW implementation detail that could silently shift. +31 — "the whole 32-byte operand lies within one 32-bit limb" — is the legible contract.

Recommended fix, unchanged: three BusId::Alu LT senders on ADDR_XG_0/ADDR_K_0/ADDR_XR_0 against 2^32 − 32, plus three LtOperations in the trace builder. ~15 lines, and it is the shape #876 already uses for in_addr. The keccak-style carry-column approach is the principled long-term form (and confirms ECSM is the in-repo outlier) but costs ~9 carry pairs on an already 667-column table for no reachable benefit.

Blast radius is nil by construction — stronger than stated above

Two independent ceilings, both verified:

• the guest heap runs from _end to MAX_MEMORY_SIZE = 0xC000_0000 (syscalls/src/allocator.rs:10,19), strictly below 0xFFFF_FFE1;
• the stack sits at STACK_TOP = 0xFFFF_FFFF_FFFF_FFF0, giving ADDR_1 = 0xFFFF_FFFF, which the carry condition excludes (the last dword's carry puts hi+1 on the bus, so ADDR_1 ≤ 0xFFFF_FFFE is also required).

Note ECSM does not get the 8-alignment immunity its HINT sibling has — ecsm_mul(&mut [u8;32], …) is 1-aligned — so the allocator ceiling is the load-bearing one.

Severity stays LOW; this is a small standalone fix, not urgent and not a merge blocker for anything.

Two notes on the PoC, for the record

The 6 tests were re-run at --test-threads=1 and are 6/6 green. That matters: they mutate a process-global env var, so at default parallelism the off=24 case could in principle "fail" for the wrong reason (guard re-enabled by a sibling test → prove error rather than verify rejection). Single-threaded it still fails specifically with LogUp bus does not balance from stark::verifier, after prove OK. Worth pinning the thread count if these are ever kept.

And one fair critique of the control: 0xFFFF_FFE0 (off=32) is 8-aligned, so its dwords route to MEMW_A — which has no carry columns — while off=24/25/31 are unaligned and route to general MEMW. The positive control therefore exercises a different table than the gap cases. The load-bearing discrimination is off=24 ↔ off=25, same path, ±1, which is clean; but the record should say so.

[MauroToscano]

Converted to draft — this branch is a demonstration and must not merge as-is (it env-gates the executor's ecsm_addr_ok guard so the PoC can run).

To be clear about what is and is not fixed: this finding has no fix PR. It is unrelated to #909, which closes a different class (trace-opening widths, in the STARK verifier). This one is ECSM's operand base addresses in the VM prover, and it is still open on main.

Keeping the branch as the executable record of the finding. The fix, when someone picks it up, is small and fully specified:

• three BusId::Alu LT senders on ADDR_XG_0 / ADDR_K_0 / ADDR_XR_0 against 2^32 − 32, in prover/src/tables/ecsm.rs::bus_interactions;
• three matching LtOperations in the trace builder, and the lt_count bump in count_table_lengths;
• the shape to copy is the in_addr sender already in prover/src/tables/hint.rs.

+31 stays; the AIR moves. That is settled by executor/src/tests/ecsm_tests.rs:159-176, which already names this exact window as "the off-by-7 window the old +24 bound for xR/xG let through".

Severity remains LOW and it is nobody's blocker: the guest heap tops out at MAX_MEMORY_SIZE = 0xC000_0000, strictly below the window, and the stack's ADDR_1 = 0xFFFF_FFFF is excluded by the carry condition. Nothing reachable by an honest guest can enter it. Worth fixing as hygiene — an AIR whose correctness rests entirely on a prover-side guard is a latent hazard — but at low priority.

Happy to open the fix as its own PR against main and link it here.