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

executor/programs/asm/test_ecsm_limb_24.s

@@ -0,0 +1,31 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	addi	sp, sp, -64
+	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)
+	li	t0, 5
+	sd	t0, 32(sp)
+	sd	zero, 40(sp)
+	sd	zero, 48(sp)
+	sd	zero, 56(sp)
+	# a0 = 2^32 - 24  (low limb of the xR output address, high limb 0)
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	a0, t1, -24
+	addi	a1, sp, 0
+	addi	a2, sp, 32
+	li	a7, -11
+	ecall
+	addi	sp, sp, 64
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/programs/asm/test_ecsm_limb_25.s

@@ -0,0 +1,31 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	addi	sp, sp, -64
+	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)
+	li	t0, 5
+	sd	t0, 32(sp)
+	sd	zero, 40(sp)
+	sd	zero, 48(sp)
+	sd	zero, 56(sp)
+	# a0 = 2^32 - 25  (low limb of the xR output address, high limb 0)
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	a0, t1, -25
+	addi	a1, sp, 0
+	addi	a2, sp, 32
+	li	a7, -11
+	ecall
+	addi	sp, sp, 64
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/programs/asm/test_ecsm_limb_31.s

@@ -0,0 +1,31 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	addi	sp, sp, -64
+	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)
+	li	t0, 5
+	sd	t0, 32(sp)
+	sd	zero, 40(sp)
+	sd	zero, 48(sp)
+	sd	zero, 56(sp)
+	# a0 = 2^32 - 31  (low limb of the xR output address, high limb 0)
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	a0, t1, -31
+	addi	a1, sp, 0
+	addi	a2, sp, 32
+	li	a7, -11
+	ecall
+	addi	sp, sp, 64
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/programs/asm/test_ecsm_limb_32.s

@@ -0,0 +1,30 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	addi	sp, sp, -64
+	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)
+	li	t0, 5
+	sd	t0, 32(sp)
+	sd	zero, 40(sp)
+	sd	zero, 48(sp)
+	sd	zero, 56(sp)
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	a0, t1, -32
+	addi	a1, sp, 0
+	addi	a2, sp, 32
+	li	a7, -11
+	ecall
+	addi	sp, sp, 64
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/programs/asm/test_limb_cross_sd.s

@@ -0,0 +1,14 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	li	t1, 1
+	slli	t1, t1, 32
+	addi	t2, t1, -4        # 0xFFFFFFFC: an 8-byte store here spans into hi=1
+	li	t0, 0x0123456789ABCDEF
+	sd	t0, 0(t2)
+	ld	t3, 0(t2)
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/src/vm/instruction/execution.rs

@@ -429,9 +429,13 @@ 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)
+                        // PoC ONLY (adversarial adjudication): the env var lets a test
+                        // run the reference semantics WITHOUT this guard, to see whether
+                        // the resulting trace still satisfies the AIR.
+                        if std::env::var_os("ECSM_NO_LIMB_GUARD").is_none()
+                            && (!ecsm_addr_ok(addr_xg, 31)
+                                || !ecsm_addr_ok(addr_xr, 31)
+                                || !ecsm_addr_ok(addr_k, 31))
                         {
                             return Err(ExecutionError::EcsmAddressOverflow);
                         }

prover/src/tests/prove_elfs_tests.rs

@@ -3526,3 +3526,135 @@ fn test_epoch_memory_bus_with_l2g_bookend() {
         "epoch Memory bus must balance with L2G bookend + PAGE excluding touched cells"
     );
 }
+
+// =============================================================================
+// PoC (adversarial adjudication): ECSM low-limb window
+// =============================================================================
+
+/// Shared body: `name` is an asm ELF whose ECSM output address (`a0`) has low
+/// limb `2^32 - off`. Returns `(executor_rejects_unpatched, prove_verify_ok)`.
+fn ecsm_limb_poc(name: &str) -> (bool, bool) {
+    let _ = env_logger::builder().is_test(true).try_init();
+    let elf_bytes = crate::test_utils::asm_elf_bytes(name);
+    let elf = Elf::load(&elf_bytes).expect("Failed to load ELF");
+
+    // (1) Reference semantics: the unpatched executor must reject.
+    unsafe { std::env::remove_var("ECSM_NO_LIMB_GUARD") };
+    let ex = Executor::new(&elf, vec![]).expect("Failed to create executor");
+    let rejects = match ex.run() {
+        Err(e) => {
+            println!("[poc {name}] reference executor: {e:?}");
+            format!("{e:?}").contains("EcsmAddressOverflow")
+        }
+        Ok(_) => {
+            println!("[poc {name}] reference executor: COMPLETED (no guard hit)");
+            false
+        }
+    };
+
+    // (2) Same program, guard bypassed: does the resulting proof verify?
+    unsafe { std::env::set_var("ECSM_NO_LIMB_GUARD", "1") };
+    let opts = ProofOptions::default_test_options();
+    let ok = match crate::prove_with_options(&elf_bytes, &opts, &MaxRowsConfig::default()) {
+        Ok(proof) => match crate::verify_with_options(&proof, &elf_bytes, &opts, None, None) {
+            Ok(v) => {
+                println!("[poc {name}] prove OK, verify = {v}");
+                v
+            }
+            Err(e) => {
+                println!("[poc {name}] verify ERROR: {e:?}");
+                false
+            }
+        },
+        Err(e) => {
+            println!("[poc {name}] prove ERROR: {e:?}");
+            false
+        }
+    };
+    unsafe { std::env::remove_var("ECSM_NO_LIMB_GUARD") };
+    (rejects, ok)
+}
+
+#[test]
+fn poc_ecsm_limb_gap_31() {
+    // addr_xr low limb = 2^32 - 31 = 0xFFFF_FFE1. Executor: reject. AIR: ?
+    let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_31");
+    println!("RESULT off=31 executor_rejects={rejects} proof_verifies={ok}");
+    assert!(rejects, "executor should reject 0xFFFF_FFE1");
+    assert!(
+        ok,
+        "SOUNDNESS GAP: proof verified for an execution the executor halts on"
+    );
+}
+
+#[test]
+fn poc_ecsm_limb_gap_25() {
+    // addr_xr low limb = 2^32 - 25 = 0xFFFF_FFE7 — the last value in the window.
+    let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_25");
+    println!("RESULT off=25 executor_rejects={rejects} proof_verifies={ok}");
+    assert!(rejects);
+    assert!(ok);
+}
+
+#[test]
+fn poc_ecsm_limb_gap_24_negative_control() {
+    // addr_xr low limb = 2^32 - 24 = 0xFFFF_FFE8: dword base +24 leaves the limb,
+    // so the AIR's byte-0 token is non-canonical. Expect prove/verify to FAIL.
+    let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_24");
+    println!("RESULT off=24 executor_rejects={rejects} proof_verifies={ok}");
+    assert!(rejects);
+    assert!(!ok, "negative control: 0xFFFF_FFE8 should NOT be provable");
+}
+
+#[test]
+fn poc_ecsm_limb_gap_32_positive_control() {
+    // addr_xr low limb = 2^32 - 32 = 0xFFFF_FFE0: the largest value the EXECUTOR
+    // allows. Executor accepts AND the proof verifies — so the only thing that
+    // differs between this and off=31 is the guard, not the harness.
+    let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_32");
+    println!("RESULT off=32 executor_rejects={rejects} proof_verifies={ok}");
+    assert!(!rejects, "executor should ACCEPT 0xFFFF_FFE0");
+    assert!(ok);
+}
+
+#[test]
+fn poc_plain_sd_across_limb_boundary() {
+    // A plain 8-byte store at 0xFFFF_FFFC (spanning into high limb 1) is accepted
+    // by the executor AND provable: the VM's general MEMW path carries correctly
+    // across the 2^32 limb boundary. Only the ECSM ecall refuses it.
+    let _ = env_logger::builder().is_test(true).try_init();
+    let elf_bytes = crate::test_utils::asm_elf_bytes("test_limb_cross_sd");
+    let elf = Elf::load(&elf_bytes).expect("Failed to load ELF");
+    let ex = Executor::new(&elf, vec![]).expect("Failed to create executor");
+    let res = ex.run();
+    println!("[poc plain-sd] executor: {:?}", res.as_ref().err());
+    assert!(res.is_ok(), "plain limb-crossing sd must execute");
+    let opts = ProofOptions::default_test_options();
+    let proof = crate::prove_with_options(&elf_bytes, &opts, &MaxRowsConfig::default())
+        .expect("prove failed");
+    let ok = crate::verify_with_options(&proof, &elf_bytes, &opts, None, None).expect("verify err");
+    println!("RESULT plain-sd-across-limb proof_verifies={ok}");
+    assert!(ok, "limb-crossing plain store should be provable");
+}
+
+#[test]
+fn poc_ecsm_limb_gap_31_shows_pages_above_2p32() {
+    let _ = env_logger::builder().is_test(true).try_init();
+    let elf_bytes = crate::test_utils::asm_elf_bytes("test_ecsm_limb_31");
+    unsafe { std::env::set_var("ECSM_NO_LIMB_GUARD", "1") };
+    let opts = ProofOptions::default_test_options();
+    let proof = crate::prove_with_options(&elf_bytes, &opts, &MaxRowsConfig::default()).unwrap();
+    unsafe { std::env::remove_var("ECSM_NO_LIMB_GUARD") };
+    for r in &proof.runtime_page_ranges {
+        println!("RUNTIME PAGE base=0x{:016X} count={}", r.base, r.count);
+    }
+    let above = proof
+        .runtime_page_ranges
+        .iter()
+        .any(|r| (0..r.count).any(|i| r.base + i * (1u64 << 18) >= (1u64 << 32)));
+    println!("RESULT has_page_at_or_above_2^32={above}");
+    assert!(
+        above,
+        "the xR write must have spilled past the 2^32 limb boundary"
+    );
+}