Fix/ecsm address bound air executor

executor/programs/asm/test_ecsm_base_cross.s

@@ -0,0 +1,64 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	# xR is written at low limb 0xFFFF_FFFC, so the DERIVED doubleword bases carry into
+	# the high limb: addr[0] = 0x0_FFFF_FFFC, addr[1] = 0x1_0000_0004, addr[2] =
+	# 0x1_0000_000C, addr[3] = 0x1_0000_0014. Only the per-access address columns can
+	# express that — the old `ADDR_*_0 + 8i` derivation would put a non-canonical low
+	# limb on the Memory bus for i = 1..3 and the trace would not balance. Byte carries
+	# inside a doubleword are exercised too: bytes 4..7 of addr[0] land past 2^32.
+	#
+	# Stack layout (96 bytes): xG at sp+0, k at sp+32, read-back buffer at sp+64.
+	addi	sp, sp, -96
+
+	# xG = secp256k1 Gx, little-endian.
+	li	t0, 0x59F2815B16F81798
+	sd	t0, 0(sp)
+	li	t0, 0x029BFCDB2DCE28D9
+	sd	t0, 8(sp)
+	li	t0, 0x55A06295CE870B07
+	sd	t0, 16(sp)
+	li	t0, 0x79BE667EF9DCBBAC
+	sd	t0, 24(sp)
+
+	# k = 5.
+	li	t0, 5
+	sd	t0, 32(sp)
+	sd	zero, 40(sp)
+	sd	zero, 48(sp)
+	sd	zero, 56(sp)
+
+	# t1 = 2^32 - 4 = 0xFFFF_FFFC.
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	t1, t1, -4
+
+	# ECSM ecall: a0 = &xR (bases carry), a1 = &xG, a2 = &k, a7 = -11.
+	addi	a0, t1, 0
+	addi	a1, sp, 0
+	addi	a2, sp, 32
+	li	a7, -11
+	ecall
+
+	# Read xR back and stage it where the commit syscall can reach it.
+	ld	t2, 0(t1)
+	sd	t2, 64(sp)
+	ld	t2, 8(t1)
+	sd	t2, 72(sp)
+	ld	t2, 16(t1)
+	sd	t2, 80(sp)
+	ld	t2, 24(t1)
+	sd	t2, 88(sp)
+
+	li	a0, 1
+	addi	a1, sp, 64
+	li	a2, 32
+	li	a7, 64
+	ecall
+
+	addi	sp, sp, 96
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/programs/asm/test_ecsm_limb_cross.s

@@ -0,0 +1,85 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	# xR is written at low limb 0xFFFF_FFE1 (high limb 0), so its last doubleword
+	# starts at +24 = 0xFFFF_FFF9 and its trailing bytes cross 2^32. Every base the
+	# ECSM AIR derives stays inside the limb; MEMW's carry columns place the crossing
+	# bytes at 0x1_0000_0000. Reading them back proves they landed there.
+	#
+	# Stack layout (96 bytes): xG at sp+0, k at sp+32, read-back buffer at sp+64.
+	addi	sp, sp, -96
+
+	# xG = secp256k1 Gx, little-endian.
+	li	t0, 0x59F2815B16F81798
+	sd	t0, 0(sp)
+	li	t0, 0x029BFCDB2DCE28D9
+	sd	t0, 8(sp)
+	li	t0, 0x55A06295CE870B07
+	sd	t0, 16(sp)
+	li	t0, 0x79BE667EF9DCBBAC
+	sd	t0, 24(sp)
+
+	# k = 5.
+	li	t0, 5
+	sd	t0, 32(sp)
+	sd	zero, 40(sp)
+	sd	zero, 48(sp)
+	sd	zero, 56(sp)
+
+	# t1 = 2^32 - 31 = 0xFFFF_FFE1.
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	t1, t1, -31
+
+	# ECSM ecall: a0 = &xR (crossing), a1 = &xG, a2 = &k, a7 = -11.
+	addi	a0, t1, 0
+	addi	a1, sp, 0
+	addi	a2, sp, 32
+	li	a7, -11
+	ecall
+
+	# Padding so the continuation test's epoch boundary falls between the ECSM write and
+	# the read-back: at epoch_size_log2 = 5 the ecall sits at instruction 48 and without
+	# this the loads land at 49..55, i.e. the same epoch, and the crossing page is never
+	# carried into an epoch that reads it. Sixteen nops push the loads past cycle 64.
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+	nop
+
+	# Read xR back from the crossing address into the stack buffer. The last load
+	# spans 0xFFFF_FFF9..0x1_0000_0000.
+	ld	t2, 0(t1)
+	sd	t2, 64(sp)
+	ld	t2, 8(t1)
+	sd	t2, 72(sp)
+	ld	t2, 16(t1)
+	sd	t2, 80(sp)
+	ld	t2, 24(t1)
+	sd	t2, 88(sp)
+
+	# Commit the read-back bytes so the test can compare them against x(5G).
+	li	a0, 1
+	addi	a1, sp, 64
+	li	a2, 32
+	li	a7, 64
+	ecall
+
+	addi	sp, sp, 96
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/src/tests/ecsm_tests.rs

@@ -2,7 +2,7 @@
 
 use crate::vm::instruction::decoding::Instruction;
 use crate::vm::instruction::execution::{ECSM_SYSCALL_NUMBER, ExecutionError};
-use crate::vm::memory::Memory;
+use crate::vm::memory::{Memory, MemoryError};
 use crate::vm::registers::Registers;
 
 /// secp256k1 generator x-coordinate, little-endian.
@@ -139,8 +139,9 @@ fn run_ecsm_at(addr_xr: u64, addr_xg: u64, addr_k: u64) -> Result<(), ExecutionE
 
 #[test]
 fn ecsm_syscall_rejects_overlapping_xg_k() {
-    // xG and k are read at the same proof timestamp, so overlapping ranges
-    // would make the trace unprovable — the executor must reject them upfront.
+    // A conservative precondition, not a provability requirement: xG is read at T and k
+    // at T+1, so an overlapping cell chains through MEMW like any other pair of accesses
+    // at increasing timestamps. No caller needs it — two live 32-byte objects are disjoint.
     for addr_k in [0x2000u64, 0x2008, 0x2018, 0x1FE8] {
         let err = run_ecsm_at(0x1000, 0x2000, addr_k).unwrap_err();
         assert!(
@@ -157,20 +158,65 @@ fn ecsm_syscall_rejects_overlapping_xg_k() {
 }
 
 #[test]
-fn ecsm_syscall_rejects_address_overflow() {
-    // 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.
-    for (addr_xr, addr_xg, addr_k) in [
-        (0xFFFF_FFE8, 0x2000, 0x3000),
-        (0x1000, 0xFFFF_FFE8, 0x3000),
-        (0x1000, 0x2000, 0xFFFF_FFF0),
-        (0xFFFF_FFE1, 0x1000, 0x2000),
-        (0x1000, 0xFFFF_FFE1, 0x2000),
-    ] {
-        let err = run_ecsm_at(addr_xr, addr_xg, addr_k).unwrap_err();
+fn ecsm_syscall_accepts_operands_crossing_the_limb() {
+    // The ECSM table derives every one of its twelve doubleword addresses as its own
+    // range-checked column, with a real 64-bit addition, so an operand that straddles `2^32`
+    // is proved exactly and the executor must not reject it. That covers the whole top of a
+    // limb, including the seven values a `+31` precondition used to refuse while the AIR
+    // proved them. The prover counterpart is
+    // `test_prove_ecsm_operand_crossing_limb_boundary`.
+    for lo32 in 0xFFFF_FFE1u64..=0xFFFF_FFFF {
+        run_ecsm_at(lo32, 0x1000, 0x2000)
+            .unwrap_or_else(|e| panic!("xR at {lo32:#x} must run, got {e:?}"));
+        run_ecsm_at(0x1000, lo32, 0x2000)
+            .unwrap_or_else(|e| panic!("xG at {lo32:#x} must run, got {e:?}"));
+        run_ecsm_at(0x1000, 0x2000, lo32)
+            .unwrap_or_else(|e| panic!("k at {lo32:#x} must run, got {e:?}"));
+    }
+    // Straddling a high limb boundary too: the carry lands in the high half of the address.
+    run_ecsm_at(0x0000_0001_FFFF_FFF9, 0x1000, 0x2000).expect("xR crossing into hi = 2 must run");
+}
+
+#[test]
+fn ecsm_syscall_rejects_operands_past_the_address_space() {
+    // The one condition left, and it is worth being precise about which table owns it. The
+    // ECSM chip's own `µ·carry_1 = 0` only bounds `addr + 24 < 2^64`; the last byte is bounded
+    // one table over, because MEMW's per-byte `hi = base_1 + carry` is never reduced mod 2^32,
+    // so at high limb 0xFFFF_FFFF it produces a token at 2^32 that no PAGE token supplies.
+    // Composed, the circuit accepts an operand iff `addr + 31 < 2^64` — exactly what
+    // `checked_add` refuses here, which is why ECSM needs no precondition of its own.
+    //
+    // `u64::MAX - 31` is the largest operand that fits; one byte further must fail, and so
+    // must a base that wraps outright.
+    run_ecsm_at(u64::MAX - 31, 0x1000, 0x2000).expect("the last operand that fits must run");
+    for addr in [u64::MAX - 30, u64::MAX - 24, u64::MAX - 7, u64::MAX] {
+        let err = run_ecsm_at(addr, 0x1000, 0x2000).unwrap_err();
         assert!(
-            matches!(err, ExecutionError::EcsmAddressOverflow),
-            "expected address overflow for xR={addr_xr:#x}, xG={addr_xg:#x}, k={addr_k:#x}"
+            matches!(
+                err,
+                ExecutionError::MemoryError(MemoryError::AddressOverflow)
+            ),
+            "xR at {addr:#x} must be rejected, got {err:?}"
         );
     }
+    // Same on an input operand, where the rejection comes from the load rather than the store.
+    // Written out instead of going through `run_ecsm_at`, whose fixture would itself overflow
+    // trying to place `xG` there.
+    let mut pc = 0;
+    let mut registers = Registers::default();
+    let mut memory = Memory::default();
+    registers.write(17, ECSM_SYSCALL_NUMBER).unwrap();
+    registers.write(10, 0x1000).unwrap();
+    registers.write(11, u64::MAX - 30).unwrap();
+    registers.write(12, 0x2000).unwrap();
+    let err = Instruction::EcallEbreak
+        .run(&mut pc, &mut registers, &mut memory)
+        .unwrap_err();
+    assert!(
+        matches!(
+            err,
+            ExecutionError::MemoryError(MemoryError::AddressOverflow)
+        ),
+        "an xG operand past the address space must be rejected by the load, got {err:?}"
+    );
 }

executor/src/vm/instruction/execution.rs

@@ -31,10 +31,6 @@ const KECCAK_STATE_BYTES: u64 = 25 * 8;
 /// bus as `[lo32, hi32] = [2^32 - 11, 2^32 - 1]`.
 pub const ECSM_SYSCALL_NUMBER: u64 = u64::MAX - 10;
 
-/// `2^32`. ECSM memory operands must not overflow their lower 32-bit address limb when the
-/// largest per-access offset is added: the 32-byte operands reach offset +31 (last byte).
-const LOW_LIMB: u64 = 1 << 32;
-
 impl TryFrom<u64> for SyscallNumbers {
     type Error = ();
     fn try_from(value: u64) -> Result<Self, Self::Error> {
@@ -74,30 +70,42 @@ impl SyscallNumbers {
 }
 
 /// Reads a 256-bit little-endian value as four doublewords at `addr + 8i`.
+///
+/// The span is validated up front, which is where the `addr + 31 < 2^64` contract lives: the
+/// per-access checks below would otherwise leave it emerging from `checked_add(8i)` plus
+/// `Memory::load_doubleword`'s aligned/unaligned split, and the aligned path bound-checks
+/// nothing (8-alignment already caps it at `u64::MAX - 7`).
 fn load_u256_le(memory: &Memory, addr: u64) -> Result<[u8; 32], MemoryError> {
+    addr.checked_add(31).ok_or(MemoryError::AddressOverflow)?;
     let mut out = [0u8; 32];
     for i in 0..4 {
-        let dw = memory.load_doubleword(addr + (i as u64) * 8)?;
+        let base = addr
+            .checked_add((i as u64) * 8)
+            .ok_or(MemoryError::AddressOverflow)?;
+        let dw = memory.load_doubleword(base)?;
         out[i * 8..i * 8 + 8].copy_from_slice(&dw.to_le_bytes());
     }
     Ok(out)
 }
 
 /// Writes a 256-bit little-endian value as four doublewords at `addr + 8i`.
+///
+/// The span is validated before the first store: checking per access would commit
+/// doublewords 0..2 and fail on the fourth, leaving 24 bytes of `xR` in a `Memory` the
+/// caller sees next to an `Err`. See [`load_u256_le`] on where the contract lives.
 fn store_u256_le(memory: &mut Memory, addr: u64, bytes: &[u8; 32]) -> Result<(), MemoryError> {
+    addr.checked_add(31).ok_or(MemoryError::AddressOverflow)?;
     for i in 0..4 {
         let mut dw = [0u8; 8];
         dw.copy_from_slice(&bytes[i * 8..i * 8 + 8]);
-        memory.store_doubleword(addr + (i as u64) * 8, u64::from_le_bytes(dw))?;
+        let base = addr
+            .checked_add((i as u64) * 8)
+            .ok_or(MemoryError::AddressOverflow)?;
+        memory.store_doubleword(base, u64::from_le_bytes(dw))?;
     }
     Ok(())
 }
 
-/// Checks the ECSM address-alignment assumption: `(addr mod 2^32) + max_offset < 2^32`.
-fn ecsm_addr_ok(addr: u64, max_offset: u64) -> bool {
-    (addr % LOW_LIMB) + max_offset < LOW_LIMB
-}
-
 impl Instruction {
     /// Runs the given instruction and returns its execution log
     pub fn run(
@@ -429,19 +437,23 @@ impl Instruction {
                         let addr_xr = registers.read(10)?;
                         let addr_xg = registers.read(11)?;
                         let addr_k = registers.read(12)?;
-                        if !ecsm_addr_ok(addr_xg, 31)
-                            || !ecsm_addr_ok(addr_xr, 31)
-                            || !ecsm_addr_ok(addr_k, 31)
-                        {
-                            return Err(ExecutionError::EcsmAddressOverflow);
-                        }
-                        // xG and k must occupy disjoint 32-byte regions. The trace builder
-                        // reads each operand as unaligned doubleword MEMW accesses (xG at T,
-                        // k at T+1); if the regions overlap, the same address is touched at
-                        // both timestamps and the MEMW consistency argument can't prove the
-                        // access chain. The loaded values would still be well-defined — this
-                        // guard is about trace provability, not correctness of the multiply.
-                        // xR may alias either: its accesses are at a later timestamp.
+                        // No address precondition here: every one of the twelve doubleword
+                        // accesses carries its own range-checked address column, derived with a
+                        // real 64-bit addition (spec `ec:c:range_addr_*` /
+                        // `ec:c:extrapolate_addr_*`), so operands crossing `2^32` are proved
+                        // exactly. What is left is a 64-bit overflow: the AIR's `µ·carry_1 = 0`
+                        // and the `checked_add` in `load_u256_le` / `store_u256_le` reject
+                        // exactly `addr + 31 >= 2^64`, so neither side accepts what the other
+                        // refuses.
+                        //
+                        // xG and k must occupy disjoint 32-byte regions. Conservative only:
+                        // the AIR proves overlap fine — xG is read at T and k at T+1, so an
+                        // overlapping cell chains through MEMW like any other pair of accesses
+                        // at increasing timestamps (measured by bypassing this guard in a
+                        // scratch build; no test pins it, since the guard is what stops such a
+                        // trace being built). It stays because nothing enforces disjointness
+                        // in-circuit and no caller needs it: two live 32-byte objects are
+                        // disjoint by construction. xR may alias either — later timestamp.
                         if addr_xg.abs_diff(addr_k) < 32 {
                             return Err(ExecutionError::EcsmOperandOverlap);
                         }
@@ -630,8 +642,6 @@ pub enum ExecutionError {
     UnalignedKeccakStateAddress(u64),
     #[error("Keccak state address range overflows: {0:#018x}")]
     KeccakStateAddressOverflow(u64),
-    #[error("ECSM address range overflows the lower 32-bit limb")]
-    EcsmAddressOverflow,
     #[error("ECSM xG and k operand ranges overlap")]
     EcsmOperandOverlap,
     #[error("ECSM scalar multiplication error: {0}")]