diff --git a/executor/programs/asm/test_ecsm_base_cross.s b/executor/programs/asm/test_ecsm_base_cross.s new file mode 100644 index 000000000..ca4e0d26d --- /dev/null +++ b/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 diff --git a/executor/programs/asm/test_ecsm_limb_cross.s b/executor/programs/asm/test_ecsm_limb_cross.s new file mode 100644 index 000000000..d7433b324 --- /dev/null +++ b/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 diff --git a/executor/src/tests/ecsm_tests.rs b/executor/src/tests/ecsm_tests.rs index 0fa240a8e..56c2e9dd5 100644 --- a/executor/src/tests/ecsm_tests.rs +++ b/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:?}" + ); } diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index c92c0ab88..8ac2e48f7 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/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 for SyscallNumbers { type Error = (); fn try_from(value: u64) -> Result { @@ -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}")] diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 8f3e68db4..374d27dc4 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -2021,6 +2021,60 @@ mod tests { ); } + // An ECSM operand whose last doubleword's trailing bytes cross `2^32` maps a runtime page + // at `0x1_0000_0000`, so the epoch machinery has to carry a page whose base sits exactly on + // the limb boundary through the per-epoch touched-cell pass and the L2G bookkeeping. The + // monolithic path is covered by `test_prove_ecsm_operand_crossing_limb_boundary`; this is + // the same guest split across epochs. + #[test] + fn test_ecsm_operand_crossing_limb_across_epochs() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_ecsm_limb_cross"); + // The guest pads 16 nops between the ECSM write and the read-back so a 32-cycle epoch + // boundary falls between them; without that the write, all four crossing reads and the + // commit sit in one epoch and the crossing page is never carried into an epoch that + // reads it. Assert the property, not a cycle count: the assembler expands each 64-bit + // `li` into eight instructions, so absolute indices move when a constant changes. + let logs = Executor::new(&Elf::load(&elf_bytes).unwrap(), vec![]) + .unwrap() + .run() + .unwrap() + .logs; + let ecall_idx = logs + .iter() + .position(|l| l.src1_val == executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER) + .expect("the guest must issue the ECSM ecall"); + let first_read_idx = ecall_idx + 17; // 16 nops, then the first `ld` + assert!( + (ecall_idx >> 5) < (first_read_idx >> 5), + "the epoch boundary must fall between the ECSM write (cycle {ecall_idx}) and the \ + read-back (cycle {first_read_idx}); adjust the nop padding in the .s" + ); + + let mut gx = [ + 0x79u8, 0xBE, 0x66, 0x7E, 0xF9, 0xDC, 0xBB, 0xAC, 0x55, 0xA0, 0x62, 0x95, 0xCE, 0x87, + 0x0B, 0x07, 0x02, 0x9B, 0xFC, 0xDB, 0x2D, 0xCE, 0x28, 0xD9, 0x59, 0xF2, 0x81, 0x5B, + 0x16, 0xF8, 0x17, 0x98, + ]; + gx.reverse(); + let mut k = [0u8; 32]; + k[0] = 5; + let expected = ecsm::scalar_mul_x(&k, &gx).unwrap(); + + let out = prove_and_verify_continuation( + &elf_bytes, + &[], + 5, + &ProofOptions::default_test_options(), + ) + .unwrap(); + assert_eq!( + out.as_deref(), + Some(&expected[..]), + "xR read back from across the 2^32 boundary must survive epoch splitting" + ); + } + // Guards that the continuation API takes `epoch_size_log2` directly. A log2 of // 4 produces 16-cycle epochs over the 33-cycle `test_commit_split`, putting its // two commits in different epochs and exercising the cross-epoch x254 carry. diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 746bef91c..5f89e6b41 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -9,18 +9,34 @@ //! See `spec/src/ecsm.toml`. All multi-limb arithmetic uses 8-bit limbs; the witness is built //! by `ecsm::compute_witness`, which reproduces these exact recurrences. //! +//! ## Operand addresses +//! Each of the twelve doubleword accesses carries its own address column, derived from the +//! operand base by a real 64-bit addition and range-checked halfword by halfword — spec +//! `ec:c:range_addr_*` and `ec:c:extrapolate_addr_*`. The table therefore needs no precondition +//! from the caller: an operand whose bytes straddle `2^32` is expressed exactly, and one whose +//! last address would wrap `2^64` is rejected by `µ·carry_1 = 0`. Deriving the bases inline as +//! `ADDR_*_0 + 8i` instead, which is what this table used to do, made the AIR's accepted set +//! depend on the executor's `ecsm_addr_ok` and the two drifted apart (#902). +//! +//! One band is worth naming because this table does not own it: for a base in +//! `[u64::MAX-30, u64::MAX-24]` the additions here are all satisfied, and the trace fails only +//! because MEMW's per-byte `hi = base_1 + carry` is never reduced mod `2^32`, so the last byte's +//! token sits at `2^32` and no PAGE token supplies it. Sound, and in-circuit — but a cross-table +//! argument rather than a constraint of ours, and not reachable through the executor, so no test +//! covers it; forging it needs a hand-built trace. +//! //! ## Padding //! Padding rows have `mu = 0`, all columns zero. The yG carry relation closes because both the //! `µ·p²` and `µ·b` terms vanish when `µ = 0`, leaving the trivial `0 = 0` recurrence. The x² -//! relation has no standalone constant and also closes at all-zero. The range checks / -//! virtual-carry checks remain µ-gated as before. +//! relation has no standalone constant and also closes at all-zero. The range checks, the +//! address additions and the virtual-carry checks are all µ-gated. use executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; -use crate::constraints::templates::INV_SHIFT_32; +use crate::constraints::templates::{AddOperand, INV_SHIFT_32, emit_add_pair}; use ecsm::{B, EcsmWitness, N_BYTES, P_BYTES}; // Bias signed convolution carries into IsHalfword [0, 2^16); see spec ecsm.typ "Carry offset" (@ecsm-limb_carry). @@ -28,9 +44,12 @@ pub(crate) const CARRY_OFFSET_X2: i64 = 8160; pub(crate) const CARRY_OFFSET_YG: i64 = 16319; // ========================================================================= -// Column indices (667 columns; keep in sync with NUM_COLUMNS below) +// Column indices (703 columns; keep in sync with NUM_COLUMNS below) // ========================================================================= +/// Halfword accessor for one operand's per-access address columns. +type AccFn = fn(usize, usize) -> usize; + pub mod cols { pub const TIMESTAMP_0: usize = 0; pub const TIMESTAMP_1: usize = 1; @@ -57,7 +76,52 @@ pub mod cols { pub const XR_SUB_P: usize = 650; // U256HL (16 halfwords) pub const MU: usize = 666; - pub const NUM_COLUMNS: usize = 667; + /// Per-access operand addresses, `addr_*[i]` for `i = 1..=3`, each a `DWordHL` + /// (4 halfwords) — spec `ec:c:extrapolate_addr_{xG,k,xR}`. + /// + /// `addr_*[0]` is the `ADDR_*_0` / `ADDR_*_1` pair above, which the spec allows to stay a + /// `DWordWL` ("`addr_xG[0]`, `addr_k[0]` and `addr_xR[0]` could be `DWordWL`s rather than + /// `HL`s"). It carries no range check of its own, and the reason is NOT that the REGISTER + /// table range-checks register words — it does not; `register.rs` has no constraint set at + /// all and pushes `init`/`fini` raw. What binds it is the `i = 0` MEMW send: it puts the + /// pair straight onto the Memory bus, where the only tokens available come from PAGE and + /// REGISTER at canonical `(lo, hi)` addresses, so a non-canonical limb matches nothing and + /// the bus does not balance. Every other chip that takes an address from a register leans + /// on the same argument (see the note in `memw.rs` about `base_address_1`). + pub const ADDR_XG_ACC: usize = 667; // DWordHL[3] (12) + pub const ADDR_K_ACC: usize = 679; // DWordHL[3] (12) + pub const ADDR_XR_ACC: usize = 691; // DWordHL[3] (12) + + pub const NUM_COLUMNS: usize = 703; + + /// Halfword `hw` of the `i`-th per-access address in the block at `base`. + /// + /// The assert is load-bearing, not defensive: `i = 0` would underflow `i - 1` and, in + /// release, land on `xr_sub_p(13..15)` and `MU`. Access 0 is the `ADDR_*_0`/`ADDR_*_1` + /// pair, which has no halfword columns — the `0..4` loops over the MEMW sends sit right + /// next to the `1..4` loops over these, so the wrong bound is the natural typo here. + #[inline] + const fn acc_hw(base: usize, i: usize, hw: usize) -> usize { + assert!(matches!(i, 1..=3), "per-access address index must be 1..=3"); + assert!(hw < 4, "a DWordHL has four halfwords"); + base + (i - 1) * 4 + hw + } + + /// Halfword `hw` of `addr_xG[i]`, for `i = 1..=3`. + #[inline] + pub const fn addr_xg_acc(i: usize, hw: usize) -> usize { + acc_hw(ADDR_XG_ACC, i, hw) + } + /// Halfword `hw` of `addr_k[i]`, for `i = 1..=3`. + #[inline] + pub const fn addr_k_acc(i: usize, hw: usize) -> usize { + acc_hw(ADDR_K_ACC, i, hw) + } + /// Halfword `hw` of `addr_xR[i]`, for `i = 1..=3`. + #[inline] + pub const fn addr_xr_acc(i: usize, hw: usize) -> usize { + acc_hw(ADDR_XR_ACC, i, hw) + } #[inline] pub const fn xr(i: usize) -> usize { @@ -166,6 +230,24 @@ pub fn generate_ecsm_trace( table.set_dword_wl(row_idx, cols::ADDR_K_0, op.addr_k); table.set_dword_wl(row_idx, cols::ADDR_XR_0, op.addr_xr); + // addr_*[i] = addr_*[0] + 8i, as real 64-bit additions (spec + // `ec:c:extrapolate_addr_*`). `expect` rather than a wrapping add, as `keccak.rs` + // does for its lane pointers: wrapping here would encode the wrap into the columns + // and `collect_bitwise_from_ecsm` would wrap the same way, so the trace stays + // self-consistent — the bus balances and the only symptom is constraint 431/432/433 + // failing, with nothing pointing back at the operand. The executor refuses these, + // so a wrap means a caller built the op some other way. + for i in 1..4 { + let off = (8 * i) as u64; + let derived = |addr: u64| { + addr.checked_add(off) + .expect("ECSM operand address range must be validated by the executor") + }; + table.set_dword_hl(row_idx, cols::addr_xg_acc(i, 0), derived(op.addr_xg)); + table.set_dword_hl(row_idx, cols::addr_k_acc(i, 0), derived(op.addr_k)); + table.set_dword_hl(row_idx, cols::addr_xr_acc(i, 0), derived(op.addr_xr)); + } + table.set_bytes(row_idx, cols::XR, &w.x_r); table.set_bytes(row_idx, cols::YR, &w.y_r); for b in 0..256 { @@ -261,6 +343,36 @@ fn dword_bytes(col: usize, chunk: usize) -> [BusValue; 8] { std::array::from_fn(|b| packed(col + 8 * chunk + b)) } +/// The `(lo, hi)` words of `addr_*[i]`, the address of the operand's `i`-th doubleword. +/// +/// `i = 0` is the `DWordWL` base bound to the register read; `i = 1..=3` are the per-access +/// `DWordHL` columns that `ec:c:extrapolate_addr_*` derives from it, repacked into words. +/// Nothing here adds an offset: the carry lives in the columns, so an address whose bytes +/// cross `2^32` is expressed exactly. +fn access_addr( + base_lo: usize, + base_hi: usize, + acc: fn(usize, usize) -> usize, + i: usize, +) -> (BusValue, BusValue) { + if i == 0 { + return (packed(base_lo), packed(base_hi)); + } + let word = |hw: usize| { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: hw, + }, + LinearTerm::Column { + coefficient: 1 << 16, + column: hw + 1, + }, + ]) + }; + (word(acc(i, 0)), word(acc(i, 2))) +} + /// A register value `[lo, hi, 0, 0, 0, 0, 0, 0]` as MEMW value elements. fn register_value(lo_col: usize, hi_col: usize) -> [BusValue; 8] { let mut v: [BusValue; 8] = std::array::from_fn(|_| BusValue::constant(0)); @@ -330,15 +442,10 @@ pub fn bus_interactions() -> Vec { 0, ), )); - // read xG: 4 doublewords at addr_xG + 8i (ts). + // read xG: 4 doublewords at addr_xG[i] (ts). for i in 0..4 { - let base_lo = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::ADDR_XG_0, - }, - LinearTerm::Constant((8 * i) as i64), - ]); + let (base_lo, base_hi) = + access_addr(cols::ADDR_XG_0, cols::ADDR_XG_1, cols::addr_xg_acc, i); out.push(BusInteraction::sender( BusId::Memw, mu(), @@ -346,7 +453,7 @@ pub fn bus_interactions() -> Vec { dword_bytes(cols::XG, i), 0, base_lo, - packed(cols::ADDR_XG_1), + base_hi, ts_lo(), ts_hi(), 0, @@ -380,15 +487,9 @@ pub fn bus_interactions() -> Vec { 0, ), )); - // read k: 4 doublewords at addr_k + 8i (ts + 1). + // read k: 4 doublewords at addr_k[i] (ts + 1). for i in 0..4 { - let base_lo = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::ADDR_K_0, - }, - LinearTerm::Constant((8 * i) as i64), - ]); + let (base_lo, base_hi) = access_addr(cols::ADDR_K_0, cols::ADDR_K_1, cols::addr_k_acc, i); out.push(BusInteraction::sender( BusId::Memw, mu(), @@ -396,7 +497,7 @@ pub fn bus_interactions() -> Vec { k_dword_busvalues(i), 0, base_lo, - packed(cols::ADDR_K_1), + base_hi, ts_lo_plus(1), ts_hi(), 0, @@ -420,22 +521,17 @@ pub fn bus_interactions() -> Vec { 0, ), )); - // write xR: 4 doublewords at addr_xR + 8i (ts + 2). + // write xR: 4 doublewords at addr_xR[i] (ts + 2). for i in 0..4 { - let base_lo = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::ADDR_XR_0, - }, - LinearTerm::Constant((8 * i) as i64), - ]); + let (base_lo, base_hi) = + access_addr(cols::ADDR_XR_0, cols::ADDR_XR_1, cols::addr_xr_acc, i); out.push(BusInteraction::sender( BusId::Memw, mu(), memw_write( dword_bytes(cols::XR, i), base_lo, - packed(cols::ADDR_XR_1), + base_hi, ts_lo_plus(2), ts_hi(), 1, @@ -443,6 +539,21 @@ pub fn bus_interactions() -> Vec { )); } + // IS_HALF on every halfword of every per-access address (spec `ec:c:range_addr_*`). + // addr_*[0] is excluded: its canonicality comes from the i = 0 MEMW send reaching the + // Memory bus, where only canonical PAGE/REGISTER tokens exist (see the `cols` note). + for acc in [cols::addr_xg_acc, cols::addr_k_acc, cols::addr_xr_acc] { + for i in 1..4 { + for hw in 0..4 { + out.push(BusInteraction::sender( + BusId::IsHalfword, + mu(), + vec![packed(acc(i, hw))], + )); + } + } + } + // IS_BYTE range checks (single byte → AreBytes[x, 0]). let is_byte = |col: usize, len: usize, out: &mut Vec| { for i in 0..len { @@ -671,7 +782,7 @@ impl OverflowKind { // ========================================================================= // // One body against the generic `ConstraintBuilder` serves the compiled prover -// folder, the verifier folder and IR capture. Constraint indices 0..413: +// folder, the verifier folder and IR capture. Constraint indices 0..434: // 0 : IS_BIT(MU) // 1..257 : IS_BIT(k[i]) for the 256 scalar bits // 257 : KBitsZeroOnPadding — (Σ k_bit[i])·(1−µ) @@ -686,10 +797,12 @@ impl OverflowKind { // 404 : OverflowRequired(KLtN) // 405..412 : CarryBit(XrLtP, 0..7) // 412 : OverflowRequired(XrLtP) +// 413..431 : AddCarryPair(addr_*[i] = addr_*[0] + 8i), 3 operands x i in 1..=3 +// 431..434 : µ·carry_1 = 0 on addr_*[3] (the 64-bit addition must not wrap) use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; -/// ECSM transition constraints as a single-source [`ConstraintSet`] (413 +/// ECSM transition constraints as a single-source [`ConstraintSet`] (434 /// total). No column configuration needed (the layout is fixed via `cols`). #[derive(Clone, Copy)] pub struct EcsmConstraints; @@ -897,6 +1010,49 @@ impl ConstraintSet for EcsmConstraints { idx += 1; } - debug_assert_eq!(idx, 413); + // addr_*[i] = addr_*[0] + 8i for i = 1..=3, as real 64-bit additions with the carry + // propagating into the high limb (spec `ec:c:extrapolate_addr_*`). Two carry-bit + // constraints per addition, gated on µ so padding rows close at all-zero. + let operands: [(usize, AccFn); 3] = [ + (cols::ADDR_XG_0, cols::addr_xg_acc), + (cols::ADDR_K_0, cols::addr_k_acc), + (cols::ADDR_XR_0, cols::addr_xr_acc), + ]; + + for (base, acc) in operands { + for i in 1..4 { + emit_add_pair( + b, + idx, + &[cols::MU], + &AddOperand::dword(base), + &AddOperand::constant((8 * i) as i64), + &AddOperand::from_dword_hl(acc(i, 0)), + ); + idx += 2; + } + } + + // µ · carry_1 = 0 on the last address of each operand: the 64-bit addition must not + // wrap. `emit_add_pair` only constrains its carries to be bits, so without this a + // prover could take addr_*[3] = addr_*[0] + 24 − 2^64. Only i = 3 needs it: if + // addr + 24 does not wrap, neither does addr + 8 or addr + 16. Mirrors the top-lane + // constraint in `keccak.rs`. + for (base, acc) in operands { + let c65536 = b.const_base(65536); + let inv_2_32 = b.const_base(INV_SHIFT_32); + let base_lo = b.main(0, base); + let base_hi = b.main(0, base + 1); + let sum_lo = b.main(0, acc(3, 0)) + b.main(0, acc(3, 1)) * c65536.clone(); + let sum_hi = b.main(0, acc(3, 2)) + b.main(0, acc(3, 3)) * c65536; + let c24 = b.const_base(24); + let carry_0 = (base_lo + c24 - sum_lo) * inv_2_32.clone(); + let carry_1 = (base_hi + carry_0 - sum_hi) * inv_2_32; + let mu = b.main(0, cols::MU); + b.emit_base(idx, mu * carry_1); + idx += 1; + } + + debug_assert_eq!(idx, 434); } } diff --git a/prover/src/tables/memw.rs b/prover/src/tables/memw.rs index 282b0c312..730cfea7a 100644 --- a/prover/src/tables/memw.rs +++ b/prover/src/tables/memw.rs @@ -254,14 +254,17 @@ pub fn bus_interactions() -> Vec { // lo = base_address_0 + (i+1) - 2^32 * carry[i] // hi = base_address_1 + carry[i] // - // Safety: `hi` is at most `base_address_1 + 1`. This never reaches 2^32 - // because the CPU table splits addresses into (lo, hi) with both halves - // in [0, 2^32), and the Memw bus ties MEMW's base_address to the CPU's - // value. MEMW only receives accesses where base_address_1 <= 0xFFFF_FFFE - // (addresses near u64::MAX are rejected by the executor before proving). - // Consequently, `carry[i]` is implicitly correct: a wrong carry bit - // produces a memory token at a wrong address that has no matching - // PAGE/REGISTER token, causing multiset imbalance and an invalid proof. + // Safety: `hi` is at most `base_address_1 + 1`, and `base_address_1 == 0xFFFF_FFFF` + // IS receivable — an ECSM operand based at `u64::MAX - 31` is accepted, so do not + // assume the executor keeps such accesses out. `hi` reaching 2^32 is not a soundness + // problem, it is the mechanism: a non-canonical high limb has no matching PAGE or + // REGISTER token, so the multiset does not balance and the proof is invalid. Same + // argument makes `carry[i]` implicitly correct — a wrong carry bit produces a token + // at a wrong address, which nothing supplies. + // + // (Only an unaligned base can carry out of the low limb: a byte offset reaches 2^32 + // only from `base_address_0 >= 2^32 - 7`, which is never a multiple of 8, so the + // aligned MEMW_A path and its own bound are not involved.) // CM8: memory[is_register, base_address, old_timestamp[0], old[0]] with +μ_sum interactions.push(BusInteraction::sender( diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 5ec9fa566..67bd253e8 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2301,6 +2301,21 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec> (16 * hw)) & 0xFFFF) as u16)); + } + } + } // ZERO: assert k != 0 (sum of k's bytes). let sum: u32 = w.k.iter().map(|&b| b as u32).sum(); out.push(BitwiseOperation::zero(sum)); diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index 91956c5ad..200d28dac 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -19,6 +19,13 @@ const IDX_YG_CONV0: usize = 323; // ConvCarry(Yg, 0) const IDX_Q1_BIT32: usize = 388; // IS_BIT(q1[32]) const IDX_XG_CARRY0: usize = 389; // CarryBit(XgLtP, 0) const IDX_XG_OVERFLOW: usize = 396; // OverflowRequired(XgLtP) +const IDX_ADDR_XG_ADD: usize = 413; // AddCarryPair(addr_xG[1]), 2 per address, i = 1..=3 +const IDX_ADDR_XR_ADD: usize = 425; // AddCarryPair(addr_xR[1]) +const IDX_ADDR_XG_NOWRAP: usize = 431; // µ·carry_1 = 0 on addr_xG[3] +const IDX_ADDR_XR_NOWRAP: usize = 433; // µ·carry_1 = 0 on addr_xR[3] + +/// Halfword accessor for one operand's per-access address columns. +type AccFn = fn(usize, usize) -> usize; fn gx_le() -> [u8; 32] { // secp256k1 Gx, little-endian. @@ -94,7 +101,7 @@ fn constraints_hold_on_generated_trace() { #[test] fn constraint_set_count() { - assert_eq!(EcsmConstraints.meta().len(), 413); + assert_eq!(EcsmConstraints.meta().len(), 434); } /// The yG carry recurrence closes on all-zero padding because both the `µ·p²` offset and the @@ -267,3 +274,146 @@ fn constraints_hold_for_k_eq_n_minus_one() { } } } + +/// `ec:c:extrapolate_addr_*`: a per-access address that is not `addr[0] + 8i` breaks the +/// addition. Without these constraints the twelve MEMW accesses could be sent at twelve +/// unrelated addresses, which is the deviation #902 reports. +/// +/// Run over all three operands: the constraint block pairs each operand's base column with its +/// own accessor, and a copy/paste slip there (xG's base against k's columns, say) would satisfy +/// every test that only exercises xG. +#[test] +fn extrapolate_addr_rejects_a_wrong_per_access_address() { + let trace = generate_ecsm_trace(&[op_for(5)]); + let clean = eval_row(&trace, 0); + for (i, v) in clean.iter().enumerate() { + assert_eq!(*v, FE::zero(), "constraint {i} must hold on the clean row"); + } + + // (accessor, first ADD constraint of that operand's block). Blocks are operand-major with + // stride 6: xG 413..418, k 419..424, xR 425..430; within a block, i = 1,2,3 x (carry_0, carry_1). + let operands: [(AccFn, usize, &str); 3] = [ + (cols::addr_xg_acc, IDX_ADDR_XG_ADD, "xG"), + (cols::addr_k_acc, IDX_ADDR_XG_ADD + 6, "k"), + (cols::addr_xr_acc, IDX_ADDR_XR_ADD, "xR"), + ]; + for (acc, block, name) in operands { + for i in 1..4 { + let mut main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(0, c)) + .collect(); + // Move addr_*[i] by one byte. + main[acc(i, 0)] = main[acc(i, 0)] + FE::one(); + let row = eval_main_row(main); + let idx = block + (i - 1) * 2; + assert_ne!( + row[idx], + FE::zero(), + "{name}: a wrong addr[{i}] must break constraint {idx}" + ); + } + } +} + +/// The `µ·carry_1 = 0` addition, which the spec's `ADD` template does not give us: without it +/// `addr[3] = addr[0] + 24 − 2^64` satisfies the carry pair, so an operand could wrap the +/// address space in-circuit while the executor refuses it. The wrapped address is a small, +/// matchable one (`0x10` here), so what this blocks is a collision with legitimate memory, not +/// merely an unsatisfiable trace. Checked on all three operands. +#[test] +fn addr_wrapping_past_u64_is_rejected() { + let operands: [(usize, AccFn, usize, usize, &str); 3] = [ + ( + cols::ADDR_XG_0, + cols::addr_xg_acc, + IDX_ADDR_XG_ADD, + IDX_ADDR_XG_NOWRAP, + "xG", + ), + ( + cols::ADDR_K_0, + cols::addr_k_acc, + IDX_ADDR_XG_ADD + 6, + IDX_ADDR_XG_NOWRAP + 1, + "k", + ), + ( + cols::ADDR_XR_0, + cols::addr_xr_acc, + IDX_ADDR_XR_ADD, + IDX_ADDR_XR_NOWRAP, + "xR", + ), + ]; + for (base_col, acc, add_block, nowrap, name) in operands { + let mut main = vec![FE::zero(); cols::NUM_COLUMNS]; + main[cols::MU] = FE::one(); + // base = u64::MAX - 7, so addr[3] = base + 24 wraps to 0x10. + let base = u64::MAX - 7; + main[base_col] = FE::from(base & 0xFFFF_FFFF); + main[base_col + 1] = FE::from(base >> 32); + for i in 1..4u64 { + let a = base.wrapping_add(8 * i); + for hw in 0..4 { + main[acc(i as usize, hw)] = FE::from((a >> (16 * hw)) & 0xFFFF); + } + } + let row = eval_main_row(main); + // Every carry bit of the three additions is satisfied by the wrapped witness... + for offset in 0..6 { + assert_eq!( + row[add_block + offset], + FE::zero(), + "{name}: the wrapped addition still satisfies carry bit {offset}" + ); + } + // ...so only the no-wrap constraint catches it. + assert_ne!( + row[nowrap], + FE::zero(), + "{name}: an operand whose last address wraps u64 must be rejected" + ); + } +} + +/// Padding rows stay valid: every new constraint is µ-gated, so an all-zero row closes. +#[test] +fn addr_constraints_close_on_padding() { + let main = vec![FE::zero(); cols::NUM_COLUMNS]; + let row = eval_main_row(main); + for (offset, v) in row[IDX_ADDR_XG_ADD..=IDX_ADDR_XR_NOWRAP].iter().enumerate() { + let idx = IDX_ADDR_XG_ADD + offset; + assert_eq!(*v, FE::zero(), "constraint {idx} must close at µ = 0"); + } +} + +/// The invariant the MSB16 bus bug broke, as a fast test instead of only end-to-end proving: +/// every `IsHalfword` interaction the ECSM row sends must have exactly one matching lookup in +/// `collect_bitwise_from_ecsm`, which is what feeds the receive multiplicity. The two live in +/// different files and are written by hand, so nothing but a count keeps them in step. +#[test] +fn is_half_sends_match_the_collector() { + use crate::tables::bitwise::BitwiseOperationType; + + let sends = crate::tables::ecsm::bus_interactions() + .iter() + .filter(|b| b.is_sender && b.bus_id == u64::from(crate::tables::types::BusId::IsHalfword)) + .count(); + + let op = op_for(5); + let collected = crate::tables::trace_builder::collect_bitwise_from_ecsm(&[op]) + .iter() + .filter(|o| o.lookup_type == BitwiseOperationType::IsHalf) + .count(); + + assert_eq!( + sends, collected, + "each IsHalfword send must have one collected lookup: {sends} sends vs {collected} lookups" + ); + // The 36 address halfwords are part of that total; a regression that dropped them would + // still balance if the collector lost them too, so pin the address share explicitly. + assert!( + sends >= 36, + "the per-access address halfwords must be among the sends" + ); +} diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ffe9071b2..cd611e310 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1137,6 +1137,92 @@ fn test_prove_elfs_ecsm() { ); } +/// Byte carries: the operand's last doubleword starts inside the limb and its trailing bytes +/// cross `2^32`, which MEMW's per-byte carry columns place at the arithmetically correct +/// address. The guest reads the bytes back from across the boundary before committing, so the +/// proof witnesses where they landed. +/// +/// This is the case the executor used to refuse while the AIR proved it, so it pins the +/// executor side; its counterpart is `ecsm_syscall_accepts_operands_crossing_the_limb`. It does +/// NOT exercise the per-access address columns — here all four derived bases have `hi = 0` and +/// the sends are identical to the old inline `ADDR_*_0 + 8i` derivation. For that see +/// `test_prove_ecsm_derived_bases_cross_limb`. +#[test] +fn test_prove_ecsm_operand_crossing_limb_boundary() { + let _ = env_logger::builder().is_test(true).try_init(); + + let elf_bytes = crate::test_utils::asm_elf_bytes("test_ecsm_limb_cross"); + let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); + let executor = + executor::vm::execution::Executor::new(&elf, vec![]).expect("Failed to create executor"); + let result = executor + .run() + .expect("an operand whose last doubleword base is in-limb must execute"); + + // Gx little-endian, k = 5. + let mut gx = [ + 0x79u8, 0xBE, 0x66, 0x7E, 0xF9, 0xDC, 0xBB, 0xAC, 0x55, 0xA0, 0x62, 0x95, 0xCE, 0x87, 0x0B, + 0x07, 0x02, 0x9B, 0xFC, 0xDB, 0x2D, 0xCE, 0x28, 0xD9, 0x59, 0xF2, 0x81, 0x5B, 0x16, 0xF8, + 0x17, 0x98, + ]; + gx.reverse(); + let mut k = [0u8; 32]; + k[0] = 5; + let expected_xr = ecsm::scalar_mul_x(&k, &gx).unwrap(); + assert_eq!( + result.return_values.memory_values, + expected_xr.to_vec(), + "xR read back from across the 2^32 boundary must equal x(5G)" + ); + + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "ECSM with an operand crossing the 2^32 limb boundary must prove and verify" + ); +} + +/// The positive case for the per-access address columns: with `xR` at low limb `0xFFFF_FFFC` +/// the DERIVED bases carry into the high limb (`addr[1] = 0x1_0000_0004`, and so on), which only +/// `ec:c:extrapolate_addr_*`'s real 64-bit addition can express. Under the old derivation those +/// sends would carry a non-canonical low limb and the Memory bus would not balance, so this +/// program is unprovable on `main` — and its executor refuses it there too. Byte carries inside +/// a doubleword are covered as well: bytes 4..7 of `addr[0]` land past `2^32`. +#[test] +fn test_prove_ecsm_derived_bases_cross_limb() { + let _ = env_logger::builder().is_test(true).try_init(); + + let elf_bytes = crate::test_utils::asm_elf_bytes("test_ecsm_base_cross"); + let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); + let executor = + executor::vm::execution::Executor::new(&elf, vec![]).expect("Failed to create executor"); + let result = executor + .run() + .expect("an operand whose derived bases carry must execute"); + + let mut gx = [ + 0x79u8, 0xBE, 0x66, 0x7E, 0xF9, 0xDC, 0xBB, 0xAC, 0x55, 0xA0, 0x62, 0x95, 0xCE, 0x87, 0x0B, + 0x07, 0x02, 0x9B, 0xFC, 0xDB, 0x2D, 0xCE, 0x28, 0xD9, 0x59, 0xF2, 0x81, 0x5B, 0x16, 0xF8, + 0x17, 0x98, + ]; + gx.reverse(); + let mut k = [0u8; 32]; + k[0] = 5; + assert_eq!( + result.return_values.memory_values, + ecsm::scalar_mul_x(&k, &gx).unwrap().to_vec(), + "xR read back from addresses whose bases carry must equal x(5G)" + ); + + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "ECSM with derived bases crossing the limb must prove and verify" + ); +} + #[test] fn test_prove_elfs_ecsm_multi() { let _ = env_logger::builder().is_test(true).try_init();