From f7143568cac4cdf6cf29a2492304ee0cbdfb2dea Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 19 Aug 2026 16:07:34 -0300 Subject: [PATCH 01/11] perf(ecsm): echo yR and yG, halving the ecalls per ecrecover MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ecrecover needs the full public key (the address is keccak(X‖Y)), but the ECSM ecall returned only xR. With an x-only k·P oracle that costs FOUR ecalls: one x(k·P) query carries no information about the sign of y, since x(k·P) = x(k·(−P)), so each of the two lincomb terms needs a second query at a shifted scalar to pin it (`solve_y`). Hinting does not help — verifying a sign costs exactly the scalar multiplication it would save. The chip already computes yR (it arrives on the ECDAS bus) and witnesses yG (the yG convolution proves it). Writing both back drops ecrecover to two ecalls, so ~1533 ECDAS rows per signature become ~768 (measured over 2000 random scalars: 383 rows per ecall). yG is echoed, not consumed. The chip may witness EITHER root of xG — the AIR binds only yG² ≡ xG³ + b — so yR alone would be ambiguous: it is ±y(k·P) for the caller's own point. Returning the root used lets the guest resolve it with one comparison, which keeps the root a free choice exactly as spec/ecsm.typ's "Two options for y_G" aside argues, while still handing back a usable y. The alternative (feeding yG IN, as PR #879 does) has to pin the root by a memory read instead, which invalidates that aside, widens the input ABI to 64 bytes and adds an on-curve validation path to the executor. Costs no column: ECSM stays at 667, gaining 8 bus interactions (579 -> 587), i.e. +4 LogUp aux columns. The guest's yR < p check moves from the AIR to the caller's FieldElement::from_bytes, which is free (a CtOption that rejects >= p) and is also what pins yG to a true root: p is odd, so y and p − y differ in parity, but y + p — a second 256-bit representative when y < 2^256 − p ≈ 2^32, and constructible by choosing r — carries the opposite parity. Guest side: solve_y and scalar_near_edge are gone, three batched inversions become one, and k = 1 / k = N−1 stop being degenerate. Operand buffers are now 8-byte aligned so the twelve doubleword accesses take MEMW_A (29 columns + 1 range check) instead of the general path (49 + 8) — the same fix get_hint already carries. Executor: the output buffer is 96 bytes, so its address bound moves from +31 to +95. Reads stay at T and T+1 and writes at T+2 (xR) and T+3 (yR, yG), the free fourth sub-timestamp, so aliasing the output over either input keeps every per-address chain monotone. Verified locally: ECSM AIR constraints hold on generated traces (including k = N−1 and the forged-row rejections), the executor writes and bounds all 96 bytes, and the guest reconstruction matches ProjectivePoint::lincomb under BOTH witnessed roots (an implementation without the fix-up passes the even-root test and fails the odd-root one). The prover suite is unchanged at 390 passed / 167 failed, byte-identical to main: the failures are missing guest ELF artifacts, which this machine cannot build (Apple clang has no RISC-V target). The end-to-end ELF tests and the row-count measurement still need CI / the server. spec/main needs the matching edit: yR and yG become outputs, the write_xR group gains two MEMW groups, and the "Two options for y_G" aside moves from "only x is output" to "the guest resolves the root from the echoed yG". --- crypto/ecsm/src/curve.rs | 11 +- crypto/ecsm/src/lib.rs | 25 ++- crypto/ethrex-crypto/src/lib.rs | 188 ++++++++--------- crypto/ethrex-crypto/src/tests/ecsm_tests.rs | 202 +++++++++++++------ executor/programs/asm/test_ecsm.s | 9 +- executor/programs/asm/test_ecsm_multi.s | 7 +- executor/programs/asm/test_ecsm_split.s | 6 +- executor/programs/bench/ecsm/src/main.rs | 11 +- executor/programs/rust/ecsm/src/main.rs | 10 +- executor/src/tests/ecsm_tests.rs | 78 +++++++ executor/src/vm/instruction/execution.rs | 16 +- prover/src/tables/ecsm.rs | 61 ++++-- prover/src/tables/trace_builder.rs | 38 ++-- syscalls/src/syscalls.rs | 28 ++- 14 files changed, 463 insertions(+), 227 deletions(-) diff --git a/crypto/ecsm/src/curve.rs b/crypto/ecsm/src/curve.rs index c5c9f5714..f1499dd32 100644 --- a/crypto/ecsm/src/curve.rs +++ b/crypto/ecsm/src/curve.rs @@ -149,15 +149,20 @@ fn schedule(k: &BigUint) -> Vec<(u8, u8, u8)> { sched } -/// Executor fast path: the x-coordinate of `k·g`, via k256's optimized scalar +/// Executor fast path: `k·g` in affine coordinates, via k256's optimized scalar /// multiplication. Needs no step list or slopes, so it skips all witness work. /// `k` must be in `[1, N)` (guaranteed by `prepare`). -pub fn scalar_mul_affine_x(k: &BigUint, g: &AffinePoint) -> BigUint { +pub fn scalar_mul_affine(k: &BigUint, g: &AffinePoint) -> AffinePoint { let scalar = Option::::from(Scalar::from_repr(be32(k).into())) .expect("ECSM: scalar k must be < N"); let g_proj = ProjectivePoint::from(to_k256_affine(g)); let r = (g_proj * scalar).to_affine(); - from_k256_affine(&r).x + from_k256_affine(&r) +} + +/// The x-coordinate of `k·g`. Thin wrapper over [`scalar_mul_affine`]. +pub fn scalar_mul_affine_x(k: &BigUint, g: &AffinePoint) -> BigUint { + scalar_mul_affine(k, g).x } /// Jacobian doubling (dbl-2009-l) for `y² = x³ + 7`: on `(X:Y:Z)` with diff --git a/crypto/ecsm/src/lib.rs b/crypto/ecsm/src/lib.rs index e3a5e3a33..e27bbd6e6 100644 --- a/crypto/ecsm/src/lib.rs +++ b/crypto/ecsm/src/lib.rs @@ -120,9 +120,28 @@ pub(crate) fn prepare( } /// Computes the x-coordinate of `k·G` over secp256k1, given `k` and `xG` as little-endian -/// 32-byte values. This is the executor's entry point — it writes the returned bytes back -/// to guest memory at `addr_xR`. +/// 32-byte values. pub fn scalar_mul_x(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result<[u8; 32], EcsmError> { + Ok(scalar_mul_full(k_le, xg_le)?.0) +} + +/// The ECSM ecall's memory image: `(xR, yR, yG)`, three little-endian 32-byte values written +/// back as one contiguous 96-byte buffer. +pub type EcsmOutput = ([u8; 32], [u8; 32], [u8; 32]); + +/// The executor's entry point: `(xR, yR, yG)` as little-endian 32-byte values, written back +/// to guest memory as one contiguous 96-byte buffer at `addr_xR`. +/// +/// `yG` is echoed because the chip is free to witness *either* root of `xG` — the AIR only +/// binds `yG² ≡ xG³ + b`, so nothing pins the sign (see `spec/ecsm.typ`, "Two options for +/// `y_G`"). Returning `yR` alone would therefore be ambiguous: it is the y of `k·(xG, yG)` +/// for whichever root the prover chose, which is `±y(k·P)` for the caller's own point `P`. +/// Echoing `yG` resolves it caller-side at no cost: the caller checks `yG < p` (free — it +/// is the field-element parse) and compares `yG`'s parity against its own base point's, so +/// a flipped root just flips the sign it applies to `yR`. That keeps the root a free choice +/// for the prover, exactly as the spec's aside argues, while still handing back a usable y. +pub fn scalar_mul_full(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result { let (k, g) = prepare(k_le, xg_le)?; - Ok(to_le_32(&curve::scalar_mul_affine_x(&k, &g))) + let r = curve::scalar_mul_affine(&k, &g); + Ok((to_le_32(&r.x), to_le_32(&r.y), to_le_32(&g.y))) } diff --git a/crypto/ethrex-crypto/src/lib.rs b/crypto/ethrex-crypto/src/lib.rs index ec36b0831..7a4632d1b 100644 --- a/crypto/ethrex-crypto/src/lib.rs +++ b/crypto/ethrex-crypto/src/lib.rs @@ -9,9 +9,10 @@ //! - `keccak256`: a sponge over the `keccak_permute` precompile (riscv64; on //! host it falls back to software keccak for tests). //! - `secp256k1_ecrecover`: the ECDSA recovery's 2-term linear combination is -//! evaluated through the ECSM `ecsm_mul` precompile (riscv64), reconstructing -//! the full point from x-only queries; on host / degenerate inputs it falls -//! back to the pure-Rust `ProjectivePoint::lincomb`. +//! evaluated through the ECSM `ecsm_mul` precompile (riscv64), which returns +//! each `k·P` in full together with the base-point root it used — so the two +//! products cost one query each and are combined with a single chord addition. +//! On host / degenerate inputs it falls back to `ProjectivePoint::lincomb`. //! //! Every other `Crypto` method inherits the trait default (vetted pure-Rust //! crates: `ark-bn254`, `bls12_381`, `p256`, `sha2`, `ripemd`, …). @@ -29,7 +30,7 @@ use k256::elliptic_curve::sec1::ToEncodedPoint; use k256::elliptic_curve::PrimeField; use k256::{AffinePoint, FieldBytes, ProjectivePoint, Scalar, U256}; -// Used only by the x-only point reconstruction (riscv accelerated path + the +// Used only by the point reconstruction (riscv accelerated path + the // host unit tests); unused on a non-test host build. #[cfg(any(target_arch = "riscv64", test))] use k256::elliptic_curve::sec1::FromEncodedPoint; @@ -75,17 +76,19 @@ impl Crypto for LambdaVmEcsmCrypto { /// [`scalar_inv`] / [`decompress_r`] for the fallback that closes that hole. #[cfg(target_arch = "riscv64")] fn get_hint(hint_id: usize, x_be: &[u8; 32]) -> [u8; 32] { - // 8-byte-aligned output buffer so the HINT table's four 8-byte writes land on the - // aligned memory path (MEMW_A) instead of the general MEMW path. An `[u8; 32]` on - // the stack is only 1-aligned, which forces the four writes onto the unaligned - // path and inflates the trace. - #[repr(C, align(8))] - struct Aligned32([u8; 32]); - let mut out = Aligned32([0u8; 32]); + let mut out = Align8([0u8; 32]); lambda_vm_syscalls::syscalls::hint(hint_id, &mut out.0, x_be); out.0 } +/// 8-byte-aligned wrapper for an ecall operand buffer, so the table's 8-byte accesses land +/// on the aligned memory path (MEMW_A, 29 columns + 1 range check) instead of the general +/// one (49 + 8). A bare `[u8; N]` on the stack is only 1-aligned, which forces every access +/// onto the unaligned path and inflates the trace. +#[cfg(target_arch = "riscv64")] +#[repr(C, align(8))] +struct Align8([u8; N]); + /// Scalar-field inverse `x⁻¹ mod n`. /// /// On riscv64 the inverse is first requested from the untrusted `hint` ecall and @@ -288,10 +291,11 @@ fn ecsm_ecrecover(sig: &[u8; 64], recid: u8, msg: &[u8; 32]) -> Result<[u8; 64], /// ECSM-accelerated 2-term linear combination `k1·P1 + k2·P2`. /// -/// On riscv64 this reconstructs the full affine result from four x-only ECSM -/// queries (see [`lincomb2_with_oracle`]); on other targets, and whenever a -/// guard trips (degenerate input or oracle inconsistency), it returns `None` -/// so the caller uses the pure-Rust `ProjectivePoint::lincomb`. +/// On riscv64 this uses two ECSM queries (the precompile returns the full `k·P` plus +/// the root it used, see [`lincomb2_with_oracle`]) instead of four x-only queries plus +/// chord-law y-reconstruction; on other targets, and whenever a guard trips (degenerate +/// input or an unusable oracle result), it returns `None` so the caller uses the +/// pure-Rust `ProjectivePoint::lincomb`. #[cfg(target_arch = "riscv64")] fn ecsm_lincomb2( a1: &AffinePoint, @@ -312,27 +316,41 @@ fn ecsm_lincomb2( None } -/// x-only scalar-mul oracle backed by the ECSM precompile: computes `x(k·P)` -/// for the curve point P whose x-coordinate is passed in. `x` must be the -/// x-coordinate of a curve point and `k` in `(0, N)` (N = curve order) — -/// guaranteed by the guards in [`lincomb2_with_oracle`]. Values cross the ABI -/// as 32-byte little-endian; `x_le` and `k_le` are distinct stack arrays so -/// the executor's `|addr_x_le − addr_k_le| ≥ 32` assumption holds by -/// construction. +/// Scalar-mul oracle backed by the ECSM precompile: for the curve point `P` whose +/// x-coordinate is passed in, returns `(x(k·P̂), y(k·P̂), ŷ)`, where `P̂ = (x, ŷ)` is the root +/// of `x` the chip actually witnessed. The chip is free to pick either root — the AIR binds +/// only `ŷ² ≡ x³ + b` — so the caller resolves the sign from `ŷ` (see +/// [`lincomb2_with_oracle`]). `x` must be the x-coordinate of a curve point and `k` in +/// `(0, N)` (N = curve order), guaranteed by the guards there. +/// +/// Values cross the ABI as 32-byte little-endian; `x_le` and `k_le` are distinct stack +/// arrays so the executor's `|addr_x_le − addr_k_le| ≥ 32` assumption holds by construction. +/// +/// `None` on any coordinate that is not a canonical field element. That parse is load-bearing +/// for `ŷ`, not just hygiene: `p` is odd, so `y` and `p − y` differ in parity, but a value +/// `y + p` (a second 256-bit representative of `y`, possible when `y < 2^256 − p ≈ 2^32`) +/// would carry the *opposite* parity. Rejecting `≥ p` here is what pins `ŷ` to exactly one +/// of the two true roots, and it costs nothing — it is the field-element parse. #[cfg(target_arch = "riscv64")] -fn ecsm_oracle(x: &FieldElement, k: &Scalar) -> Option { +fn ecsm_oracle(x: &FieldElement, k: &Scalar) -> Option<(FieldElement, FieldElement, FieldElement)> { let x_be = x.to_bytes(); let k_be = k.to_bytes(); - let mut x_le = [0u8; 32]; - let mut k_le = [0u8; 32]; + let mut x_le = Align8([0u8; 32]); + let mut k_le = Align8([0u8; 32]); for i in 0..32 { - x_le[i] = x_be[31 - i]; - k_le[i] = k_be[31 - i]; + x_le.0[i] = x_be[31 - i]; + k_le.0[i] = k_be[31 - i]; } - let mut xr_le = [0u8; 32]; - lambda_vm_syscalls::syscalls::ecsm_mul(&mut xr_le, &x_le, &k_le); - xr_le.reverse(); - Option::from(FieldElement::from_bytes(&xr_le.into())) + let mut out = Align8([0u8; 96]); + lambda_vm_syscalls::syscalls::ecsm_mul(&mut out.0, &x_le.0, &k_le.0); + let load = |chunk: usize| -> Option { + let mut be = [0u8; 32]; + for i in 0..32 { + be[i] = out.0[chunk * 32 + 31 - i]; + } + Option::from(FieldElement::from_bytes(&be.into())) + }; + Some((load(0)?, load(1)?, load(2)?)) } /// Base-field inverse `x⁻¹ mod p`. @@ -384,18 +402,20 @@ where Option::from(x.invert()) } -/// Computes `k1·P1 + k2·P2` from four x-only oracle queries, or `None` if any -/// degenerate-configuration guard trips. +/// Computes `k1·P1 + k2·P2` from two oracle queries, or `None` if a degenerate +/// configuration or an unusable oracle result trips a guard. /// -/// The lambda-vm ECSM precompile returns only `x(k·P)`. For `A = k1·P1` with -/// `P1 = (xp, yp)` fully known, query `xa = x(k1·P1)` and `xc = x((k1+1)·P1)`. -/// The chord-addition law gives `λ² = xc + xa + xp =: t` and `ya = yp + λ·dx` -/// with `dx = xa − xp`; substituting into `ya² = xa³ + b` makes λ *linear*: -/// `λ = (xa³ − xp³ − t·dx²) / (2·yp·dx)`. The wrong sign `−ya` would force -/// `x((k1−1)·P1) = xc`, i.e. `k1 ≡ 0` or `2·k1 ≡ 0 (mod n)`, excluded by the -/// scalar guards. x-only queries are parity-invariant (`x(k·P) = x(k·(−P))`), -/// so the precompile's canonical-y lift never matters. Same for `B = k2·P2`, -/// then `Q = A + B` is one affine addition. All three inversions are batched. +/// The ECSM ecall returns the full point `k·P̂` together with the root `ŷ` it used, and the +/// chip may pick either root of `x(P)` — the AIR binds only `ŷ² ≡ x³ + b`. So `k·P̂ = ±(k·P)`: +/// comparing `ŷ` against the caller's own `y` says which, and one conditional negation +/// recovers `k·P`. `Q = A + B` is then a single chord addition with a single field inversion. +/// +/// The x-only predecessor needed a second query `x((k+1)·P)` per point plus the chord-law +/// y-reconstruction, which is what made `k1 = 1` and `k1 = N−1` degenerate; with `y` in hand +/// those scalars are ordinary. secp256k1 has cofactor 1 and prime `N`, so `k·P ≠ O` for every +/// `k ∈ (0, N)` and no further scalar guard is needed. `dx = 0` still covers both remaining +/// degenerate cases at once (two curve points share an x only when they are equal or +/// negatives), and the caller falls back to the software `lincomb` there. /// /// Generic over the oracle so unit tests can substitute a software stand-in. #[cfg(any(target_arch = "riscv64", test))] @@ -407,45 +427,30 @@ fn lincomb2_with_oracle( oracle: O, ) -> Option where - O: Fn(&FieldElement, &Scalar) -> Option, + O: Fn(&FieldElement, &Scalar) -> Option<(FieldElement, FieldElement, FieldElement)>, { // Inputs are affine already (the ecrecover path lifts them from known Z=1 // points), so no projective→affine inversion is needed here. if bool::from(a1.is_identity()) || bool::from(a2.is_identity()) { return None; } - if scalar_near_edge(k1) || scalar_near_edge(k2) { + if bool::from(k1.is_zero()) || bool::from(k2.is_zero()) { return None; } let (x1, y1) = affine_xy(a1)?; let (x2, y2) = affine_xy(a2)?; - let xa = oracle(&x1, k1)?; - let xc1 = oracle(&x1, &(*k1 + Scalar::ONE))?; - let xb = oracle(&x2, k2)?; - let xc2 = oracle(&x2, &(*k2 + Scalar::ONE))?; + let (xa, ya) = oracle_point(&x1, &y1, k1, &oracle)?; + let (xb, yb) = oracle_point(&x2, &y2, k2, &oracle)?; - let dx1 = (xa - x1).normalize(); - let dx2 = (xb - x2).normalize(); + // Q = A + B via one chord addition (A ≠ ±B ⇒ dxq ≠ 0). One field inversion. let dxq = (xb - xa).normalize(); - if bool::from(dx1.is_zero()) || bool::from(dx2.is_zero()) || bool::from(dxq.is_zero()) { + if bool::from(dxq.is_zero()) { return None; } - - // One shared inversion for the two λ denominators and the final chord. - let den1 = y1.double() * dx1; - let den2 = y2.double() * dx2; - let inv = field_inv(&(den1 * den2 * dxq))?; - let inv_den1 = inv * den2 * dxq; - let inv_den2 = inv * den1 * dxq; - let inv_dxq = inv * den1 * den2; - - let ya = solve_y(&x1, &y1, &xa, &xc1, &dx1, &inv_den1)?; - let yb = solve_y(&x2, &y2, &xb, &xc2, &dx2, &inv_den2)?; - - // Q = A + B, with A ≠ ±B ensured by dxq ≠ 0. - let lq = (yb - ya) * inv_dxq; + let inv_dxq = field_inv(&dxq)?; + let lq = ((yb - ya) * inv_dxq).normalize(); let xq = (lq.square() - xa - xb).normalize(); let yq = (lq * (xa - xq) - ya).normalize(); @@ -456,36 +461,37 @@ where point_from_xy(&xq, &yq) } -/// Recovers `y(k·P)` from `xa = x(k·P)` and `xc = x((k+1)·P)`. -/// Returns `None` if `xc` is inconsistent with the computed `lambda` -/// (oracle misbehavior); degeneracy guards are in [`lincomb2_with_oracle`]. +/// One oracle query plus the root fix-up: `k·(xp, yp)` in affine coordinates. +/// +/// The oracle multiplied `(xp, ŷ)` for whichever root `ŷ` the chip witnessed, so the result +/// is `k·(xp, yp)` when `ŷ = yp` and `−k·(xp, yp)` when `ŷ = −yp`. Since `ŷ` is canonical +/// (the oracle's field-element parse rejected `≥ p`) and satisfies `ŷ² ≡ xp³ + b`, those are +/// the only two cases; anything else means the oracle did not multiply *this* point, so we +/// return `None` and the caller falls back to software. +/// +/// Compared by value rather than `ct_eq`: k256 compares raw limbs *and* the magnitude and +/// `normalized` tags, so a subtraction result never compares equal to a normalized constant +/// whatever its value. Both operands are `from_bytes` outputs (magnitude 1), which keeps +/// `Sub`'s internal `negate(1)` within its contract; the negated `yr` is re-normalized so +/// the caller's later subtraction stays within it too. #[cfg(any(target_arch = "riscv64", test))] -fn solve_y( +fn oracle_point( xp: &FieldElement, yp: &FieldElement, - xa: &FieldElement, - xc: &FieldElement, - dx: &FieldElement, - inv_den: &FieldElement, -) -> Option { - let t = *xc + xa + xp; - let xa3 = xa.square() * xa; - let xp3 = xp.square() * xp; - let lambda = (xa3 - xp3 - t * dx.square()) * inv_den; - if lambda.square().normalize() != t.normalize() { - return None; + k: &Scalar, + oracle: &O, +) -> Option<(FieldElement, FieldElement)> +where + O: Fn(&FieldElement, &Scalar) -> Option<(FieldElement, FieldElement, FieldElement)>, +{ + let (xr, yr, yg) = oracle(xp, k)?; + if bool::from((*yp - yg).normalizes_to_zero()) { + return Some((xr, yr)); } - Some((*yp + lambda * dx).normalize()) -} - -/// `k ∈ {0, 1, n−1}`: fast early-exit before oracle calls. -/// k=0: invalid ecall scalar. k=1: dx=0. k=n-1: k+1 wraps to 0 mod n. -#[cfg(any(target_arch = "riscv64", test))] -fn scalar_near_edge(k: &Scalar) -> bool { - use k256::elliptic_curve::subtle::ConstantTimeEq; - bool::from(k.is_zero()) - || bool::from(k.ct_eq(&Scalar::ONE)) - || bool::from(k.ct_eq(&(-Scalar::ONE))) + if bool::from((*yp + yg).normalizes_to_zero()) { + return Some((xr, (-yr).normalize())); + } + None } /// Affine `(x, y)` of a non-identity point as field elements, via its SEC1 diff --git a/crypto/ethrex-crypto/src/tests/ecsm_tests.rs b/crypto/ethrex-crypto/src/tests/ecsm_tests.rs index 42e80224b..f884de8e6 100644 --- a/crypto/ethrex-crypto/src/tests/ecsm_tests.rs +++ b/crypto/ethrex-crypto/src/tests/ecsm_tests.rs @@ -1,6 +1,6 @@ -//! Tests for the x-only ECSM linear-combination reconstruction +//! Tests for the ECSM linear-combination reconstruction //! (`lincomb2_with_oracle`) against the software `ProjectivePoint::lincomb`, -//! plus the degenerate-configuration fallback guards. +//! plus the root fix-up and the degenerate-configuration fallback guards. use crate::*; @@ -11,15 +11,45 @@ fn curve_b() -> FieldElement { FieldElement::from_bytes(&bytes.into()).unwrap() } -/// Software stand-in for the ECSM precompile: lift `x` to a curve point and -/// return `x(k·P)` (parity-invariant, like the real ecall). -fn soft_oracle(x: &FieldElement, k: &Scalar) -> Option { +fn is_odd(y: &FieldElement) -> bool { + y.normalize().to_bytes()[31] & 1 == 1 +} + +/// Software stand-in for the ECSM precompile, parameterised by which root of `x` the chip +/// witnesses. The real chip is free to pick either (the AIR binds only `yG² ≡ xG³ + b`), so +/// both settings are legal traces and the caller must handle them identically. +/// Returns `(x(k·P̂), y(k·P̂), ŷ)` with `P̂ = (x, ŷ)`. +fn soft_oracle_with_root( + x: &FieldElement, + k: &Scalar, + want_odd_root: bool, +) -> Option<(FieldElement, FieldElement, FieldElement)> { let xn = x.normalize(); let y2 = (xn.square() * xn + curve_b()).normalize(); - let y = Option::::from(y2.sqrt())?; - let p = point_from_xy(&xn, &y.normalize())?; + let y = Option::::from(y2.sqrt())?.normalize(); + let yg = if is_odd(&y) == want_odd_root { + y + } else { + (-y).normalize() + }; + let p = point_from_xy(&xn, &yg)?; let prod = (p * k).to_affine(); - Some(affine_xy(&prod)?.0) + let (xr, yr) = affine_xy(&prod)?; + Some((xr, yr, yg)) +} + +/// The canonical (even-root) lift, matching what `ecsm::recover_y_canonical` produces. +fn soft_oracle(x: &FieldElement, k: &Scalar) -> Option<(FieldElement, FieldElement, FieldElement)> { + soft_oracle_with_root(x, k, false) +} + +/// The other legal choice: the odd root. `k·P̂ = −(k·P)` here, so the caller's sign fix-up +/// is what keeps the answer right. +fn soft_oracle_odd( + x: &FieldElement, + k: &Scalar, +) -> Option<(FieldElement, FieldElement, FieldElement)> { + soft_oracle_with_root(x, k, true) } fn g_times(n: u64) -> ProjectivePoint { @@ -55,23 +85,96 @@ fn matches_software_lincomb_on_recovery_shape() { assert_eq!(got, expected.to_affine()); } +/// The property the echoed root buys: whichever root the chip picks, the reconstruction is +/// the same point. With the odd root every `k·P̂` comes back negated, and only the caller's +/// fix-up puts it right — so an unfixed implementation fails this and passes the one above. +#[test] +fn either_witnessed_root_gives_the_same_result() { + let cases = [ + (g_times(3), 123_456_789u64, g_times(7), 987_654_321u64), + ( + ProjectivePoint::GENERATOR, + 0xdead_beefu64, + g_times(0x1234), + 0x0bad_f00du64, + ), + (g_times(11), 2u64.pow(20) + 5, g_times(2), 42u64), + ]; + for (p1, k1, p2, k2) in cases { + let (k1, k2) = (Scalar::from(k1), Scalar::from(k2)); + let expected = ProjectivePoint::lincomb(&p1, &k1, &p2, &k2).to_affine(); + let even = lincomb2_with_oracle(&p1.to_affine(), &k1, &p2.to_affine(), &k2, soft_oracle) + .expect("even-root oracle must reconstruct"); + let odd = lincomb2_with_oracle(&p1.to_affine(), &k1, &p2.to_affine(), &k2, soft_oracle_odd) + .expect("odd-root oracle must reconstruct"); + assert_eq!(even, expected); + assert_eq!( + odd, expected, + "the root fix-up must absorb the chip's choice" + ); + } +} + +/// `ŷ` that is neither `y` nor `−y` means the oracle did not multiply the caller's point. +/// The caller must decline rather than use the result. #[test] -fn edge_scalars_fall_back() { +fn foreign_root_falls_back() { + let bogus = |x: &FieldElement, k: &Scalar| { + let (xr, yr, _) = soft_oracle(x, k)?; + // A valid field element, but not a root of this x. + let mut bytes = [0u8; 32]; + bytes[31] = 9; + Some((xr, yr, FieldElement::from_bytes(&bytes.into()).unwrap())) + }; let p1 = g_times(3); - let p2 = g_times(5); + let p2 = g_times(7); + let k = Scalar::from(12345u64); + assert!( + lincomb2_with_oracle(&p1.to_affine(), &k, &p2.to_affine(), &k, bogus).is_none(), + "a yG that is neither root must be rejected" + ); +} + +/// `k = 1` and `k = N−1` were degenerate for the x-only predecessor (which needed a second +/// `(k+1)·P` query); with `y` returned they are ordinary scalars. +#[test] +fn former_edge_scalars_now_reconstruct() { + let p1 = g_times(3); + let p2 = g_times(7); let ok = Scalar::from(12345u64); - for bad in [Scalar::ZERO, Scalar::ONE, -Scalar::ONE] { - assert!( - lincomb2_with_oracle(&p1.to_affine(), &bad, &p2.to_affine(), &ok, soft_oracle) - .is_none() - ); - assert!( - lincomb2_with_oracle(&p1.to_affine(), &ok, &p2.to_affine(), &bad, soft_oracle) - .is_none() - ); + for k in [Scalar::ONE, -Scalar::ONE] { + for (a, ka, b, kb) in [(p1, k, p2, ok), (p1, ok, p2, k)] { + let expected = ProjectivePoint::lincomb(&a, &ka, &b, &kb); + let got = lincomb2_with_oracle(&a.to_affine(), &ka, &b.to_affine(), &kb, soft_oracle) + .expect("k = 1 / N−1 are ordinary scalars now"); + assert_eq!(got, expected.to_affine()); + } } } +#[test] +fn zero_scalars_fall_back() { + let p1 = g_times(3); + let p2 = g_times(5); + let ok = Scalar::from(12345u64); + assert!(lincomb2_with_oracle( + &p1.to_affine(), + &Scalar::ZERO, + &p2.to_affine(), + &ok, + soft_oracle + ) + .is_none()); + assert!(lincomb2_with_oracle( + &p1.to_affine(), + &ok, + &p2.to_affine(), + &Scalar::ZERO, + soft_oracle + ) + .is_none()); +} + #[test] fn identity_points_fall_back() { let p = g_times(3); @@ -92,10 +195,8 @@ fn cancelling_and_doubling_terms_fall_back() { #[test] fn k_half_n_minus_1_reconstructs_correctly() { - // k = (n-1)/2 satisfies k·P = -(k+1)·P for any P, so the oracle returns - // the same x-coordinate for both the k and k+1 calls (xa = xc). The - // solve_y algebra still holds: lambda² = 2·xa + xp = t, so the check - // passes and the correct ya is recovered. + // k = (n-1)/2 satisfies k·P = -(k+1)·P for any P. It broke nothing before and it + // breaks nothing now; kept as a regression pin on a scalar with structure. let two_inv = Scalar::from(2u64) .invert_vartime() .expect("2 is invertible mod n"); @@ -107,7 +208,7 @@ fn k_half_n_minus_1_reconstructs_correctly() { let expected = ProjectivePoint::lincomb(&p1, &k_half, &p2, &k2); let got = lincomb2_with_oracle(&p1.to_affine(), &k_half, &p2.to_affine(), &k2, soft_oracle) - .expect("k=(n-1)/2 is not near-edge and must reconstruct correctly"); + .expect("k=(n-1)/2 must reconstruct correctly"); assert_eq!(got, expected.to_affine()); } @@ -129,55 +230,28 @@ fn cross_point_cancellation_falls_back() { ); } -#[test] -fn solve_y_rejects_inconsistent_oracle_xc() { - // Directly test that solve_y's lambda² == t check fires when xc is wrong. - // This is the oracle-misbehavior guard: it cannot easily be reached via - // lincomb2_with_oracle because the oracle is Fn (no mutable state to - // return xa correct and xc wrong in separate calls). - let (xp, yp) = affine_xy(&g_times(3).to_affine()).unwrap(); - let k = Scalar::from(12345u64); - - let xa = soft_oracle(&xp, &k).unwrap(); - let xc_correct = soft_oracle(&xp, &(k + Scalar::ONE)).unwrap(); - // xc from k+100 is inconsistent with xa from k — lambda²=t must reject it. - let xc_wrong = soft_oracle(&xp, &(k + Scalar::from(100u64))).unwrap(); - - let dx = (xa - xp).normalize(); - let inv_den = Option::::from((yp.double() * dx).invert()) - .expect("dx is nonzero for k=12345"); - - assert!( - solve_y(&xp, &yp, &xa, &xc_correct, &dx, &inv_den).is_some(), - "correct xc must pass the lambda² check" - ); - assert!( - solve_y(&xp, &yp, &xa, &xc_wrong, &dx, &inv_den).is_none(), - "inconsistent xc (oracle misbehavior) must be rejected by the lambda² check" - ); -} - #[test] fn odd_y_base_point_reconstructs_correctly() { - // Validates the solve_y sign-selection argument: when P1 has odd y the - // reconstruction must still match ProjectivePoint::lincomb. - let (p1, _k_gen) = (2u64..200) + // A base point with odd y exercises the fix-up from the other side: the caller's own y + // is the odd root, so the canonical-lift oracle is the one that comes back negated. + let p1 = (2u64..200) .find_map(|n| { let p = g_times(n); let (_, y) = affine_xy(&p.to_affine())?; - if y.normalize().to_bytes()[31] & 1 == 1 { - Some((p, n)) - } else { - None - } + is_odd(&y).then_some(p) }) .expect("at least one of the first 200 multiples of G has odd y"); let p2 = g_times(13); let k1 = Scalar::from(54321u64); let k2 = Scalar::from(11111u64); - let expected = ProjectivePoint::lincomb(&p1, &k1, &p2, &k2); - let got = lincomb2_with_oracle(&p1.to_affine(), &k1, &p2.to_affine(), &k2, soft_oracle) - .expect("odd-y base point is non-degenerate and must reconstruct correctly"); - assert_eq!(got, expected.to_affine()); + let expected = ProjectivePoint::lincomb(&p1, &k1, &p2, &k2).to_affine(); + for oracle in [ + soft_oracle as fn(&FieldElement, &Scalar) -> _, + soft_oracle_odd as fn(&FieldElement, &Scalar) -> _, + ] { + let got = lincomb2_with_oracle(&p1.to_affine(), &k1, &p2.to_affine(), &k2, oracle) + .expect("odd-y base point is non-degenerate and must reconstruct correctly"); + assert_eq!(got, expected); + } } diff --git a/executor/programs/asm/test_ecsm.s b/executor/programs/asm/test_ecsm.s index 67298f810..13968dfb1 100644 --- a/executor/programs/asm/test_ecsm.s +++ b/executor/programs/asm/test_ecsm.s @@ -1,8 +1,9 @@ .attribute 5, "rv64i2p1_m2p0_zmmul1p0" .globl main main: - # Stack layout (96 bytes): xG at sp+0, k at sp+32, xR at sp+64. - addi sp, sp, -96 + # Stack layout (160 bytes): xG at sp+0, k at sp+32, and the ECSM output buffer + # [xR ‖ yR ‖ yG] at sp+64..sp+160. Only xR is committed. + addi sp, sp, -160 # xG = secp256k1 Gx, little-endian (4 doublewords). li t0, 0x59F2815B16F81798 @@ -21,7 +22,7 @@ main: sd zero, 48(sp) sd zero, 56(sp) - # ECSM ecall: a0 = &xR, a1 = &xG, a2 = &k, a7 = -11. + # ECSM ecall: a0 = &out (96 bytes), a1 = &xG, a2 = &k, a7 = -11. addi a0, sp, 64 addi a1, sp, 0 addi a2, sp, 32 @@ -37,7 +38,7 @@ main: ecall # Restore stack and halt. - addi sp, sp, 96 + addi sp, sp, 160 li a0, 0 li a7, 93 ecall diff --git a/executor/programs/asm/test_ecsm_multi.s b/executor/programs/asm/test_ecsm_multi.s index bc0fcfd23..4885b4aff 100644 --- a/executor/programs/asm/test_ecsm_multi.s +++ b/executor/programs/asm/test_ecsm_multi.s @@ -1,8 +1,9 @@ .attribute 5, "rv64i2p1_m2p0_zmmul1p0" .globl main main: - # Stack layout (96 bytes): xG at sp+0, k at sp+32, xR at sp+64. - addi sp, sp, -96 + # Stack layout (160 bytes): xG at sp+0, k at sp+32, and the ECSM output buffer + # [xR ‖ yR ‖ yG] at sp+64..sp+160. Only xR is committed. + addi sp, sp, -160 # xG = secp256k1 Gx, little-endian (written once; reused by all calls). li t0, 0x59F2815B16F81798 @@ -62,7 +63,7 @@ main: ecall # Restore stack and halt. - addi sp, sp, 96 + addi sp, sp, 160 li a0, 0 li a7, 93 ecall diff --git a/executor/programs/asm/test_ecsm_split.s b/executor/programs/asm/test_ecsm_split.s index e0e1666ae..4df68155b 100644 --- a/executor/programs/asm/test_ecsm_split.s +++ b/executor/programs/asm/test_ecsm_split.s @@ -1,12 +1,12 @@ .attribute 5, "rv64i2p1_m2p0_zmmul1p0" .globl main main: - # Like test_ecsm.s, but the ECSM pointer registers (a0=&xR, a1=&xG, a2=&k) + # Like test_ecsm.s, but the ECSM pointer registers (a0=&out, a1=&xG, a2=&k) # are set at the very START and never rewritten before the ecall. With a small # continuation epoch size the ecall lands in a LATER epoch than the one that set # the pointers, so the per-epoch touched-cell pass must carry registers across # the boundary to compute the right addresses. - addi sp, sp, -96 + addi sp, sp, -160 addi a0, sp, 64 addi a1, sp, 0 addi a2, sp, 32 @@ -41,7 +41,7 @@ main: ecall # Restore stack and halt. - addi sp, sp, 96 + addi sp, sp, 160 li a0, 0 li a7, 93 ecall diff --git a/executor/programs/bench/ecsm/src/main.rs b/executor/programs/bench/ecsm/src/main.rs index 78549d35b..4d311d05b 100644 --- a/executor/programs/bench/ecsm/src/main.rs +++ b/executor/programs/bench/ecsm/src/main.rs @@ -22,10 +22,13 @@ pub fn main() { ]; k.reverse(); - let mut xr = [0u8; 32]; + // The precompile writes [xR ‖ yR ‖ yG]; the chain feeds xR back as the next base point. + #[repr(C, align(8))] + struct Align8([u8; N]); + let mut out = Align8([0u8; 96]); for _ in 0..ITERATIONS { - syscalls::syscalls::ecsm_mul(&mut xr, &xg, &k); - xg = xr; + syscalls::syscalls::ecsm_mul(&mut out.0, &xg, &k); + xg.copy_from_slice(&out.0[..32]); } - syscalls::syscalls::commit(&xr); + syscalls::syscalls::commit(&out.0[..32]); } diff --git a/executor/programs/rust/ecsm/src/main.rs b/executor/programs/rust/ecsm/src/main.rs index 709d4a4ae..ea553c6d9 100644 --- a/executor/programs/rust/ecsm/src/main.rs +++ b/executor/programs/rust/ecsm/src/main.rs @@ -14,7 +14,11 @@ pub fn main() { let mut k = [0u8; 32]; k[0] = 5; - let mut xr = [0u8; 32]; - syscalls::syscalls::ecsm_mul(&mut xr, &xg, &k); - syscalls::syscalls::commit(&xr); + // The precompile writes [xR ‖ yR ‖ yG]; only xR is committed. 8-byte aligned so the + // twelve doubleword accesses take the aligned memory path (MEMW_A). + #[repr(C, align(8))] + struct Align8([u8; N]); + let mut out = Align8([0u8; 96]); + syscalls::syscalls::ecsm_mul(&mut out.0, &xg, &k); + syscalls::syscalls::commit(&out.0[..32]); } diff --git a/executor/src/tests/ecsm_tests.rs b/executor/src/tests/ecsm_tests.rs index 0fa240a8e..2b2d2d220 100644 --- a/executor/src/tests/ecsm_tests.rs +++ b/executor/src/tests/ecsm_tests.rs @@ -174,3 +174,81 @@ fn ecsm_syscall_rejects_address_overflow() { ); } } + +/// Runs the ECSM syscall and returns the whole 96-byte output buffer as +/// `(xR, yR, yG)`, all little-endian. +fn run_ecsm_full( + k_bytes: &[u8; 32], + xg_le: &[u8; 32], +) -> Result<([u8; 32], [u8; 32], [u8; 32]), ExecutionError> { + let mut pc = 0; + let mut registers = Registers::default(); + let mut memory = Memory::default(); + + let addr_out = 0x1000u64; + let addr_xg = 0x2000u64; + let addr_k = 0x3000u64; + write_u256_le(&mut memory, addr_xg, xg_le); + write_u256_le(&mut memory, addr_k, k_bytes); + + registers.write(17, ECSM_SYSCALL_NUMBER).unwrap(); + registers.write(10, addr_out).unwrap(); + registers.write(11, addr_xg).unwrap(); + registers.write(12, addr_k).unwrap(); + + Instruction::EcallEbreak.run(&mut pc, &mut registers, &mut memory)?; + Ok(( + read_u256_le(&memory, addr_out), + read_u256_le(&memory, addr_out + 32), + read_u256_le(&memory, addr_out + 64), + )) +} + +/// `y² ≡ x³ + 7 (mod p)` for little-endian 32-byte coordinates. +fn on_curve(x_le: &[u8; 32], y_le: &[u8; 32]) -> bool { + let fe = |le: &[u8; 32]| { + let mut be = *le; + be.reverse(); + Option::::from(k256::FieldElement::from_bytes(&be.into())) + }; + let (Some(x), Some(y)) = (fe(x_le), fe(y_le)) else { + return false; + }; + let mut seven = [0u8; 32]; + seven[31] = 7; + let b = k256::FieldElement::from_bytes(&seven.into()).unwrap(); + // Negate `y²` (magnitude 1), not the RHS: the RHS is a sum carrying magnitude 2, and + // k256's `negate(1)` asserts its operand's magnitude is <= 1 in debug builds. + ((x.square() * x + b) + y.square().negate(1)) + .normalizes_to_zero() + .into() +} + +#[test] +fn ecsm_syscall_writes_the_full_96_byte_output() { + let xg = gx_le(); + for v in [1u64, 2, 5, 0xFFFF, 1_000_003] { + let k = k_le(v); + let got = run_ecsm_full(&k, &xg).unwrap(); + assert_eq!(got, ecsm::scalar_mul_full(&k, &xg).unwrap()); + let (xr, yr, yg) = got; + // yG is the root of xG the chip used, and the executor lifts to the even one. + assert!(on_curve(&xg, &yg), "yG must satisfy yG² = xG³ + 7"); + assert_eq!(yg[0] & 1, 0, "the executor lifts xG to its even root"); + // yR is the y of k·(xG, yG), so the result is a curve point too. + assert!(on_curve(&xr, &yr), "yR must satisfy yR² = xR³ + 7"); + } +} + +#[test] +fn ecsm_syscall_output_bound_covers_all_96_bytes() { + // The output spans +0..+95, so its low limb must stay under 2^32 - 95. One past the + // last accepted base is where the 96th byte would cross the limb boundary. + let last_ok = 0x1_0000_0000u64 - 96; + run_ecsm_at(last_ok, 0x2000, 0x3000).expect("+95 lands on the last byte of the limb"); + let err = run_ecsm_at(last_ok + 1, 0x2000, 0x3000).unwrap_err(); + assert!( + matches!(err, ExecutionError::EcsmAddressOverflow), + "an output whose 96th byte crosses the limb must be rejected" + ); +} diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 592af95e8..33026f6ee 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -519,14 +519,16 @@ impl Instruction { } SyscallNumbers::Ecsm => { // ECSM(-11): k×G on secp256k1. - // x10 = addr to write xR, x11 = addr of xG, x12 = addr of k. - // xG, k, xR are 32-byte little-endian values; xG and xR must be + // x10 = addr of the 96-byte output buffer [xR ‖ yR ‖ yG], + // x11 = addr of xG, x12 = addr of k. + // All six values are 32-byte little-endian; xG and xR must be // canonical field elements and k must be in [1, N). let addr_xr = registers.read(10)?; let addr_xg = registers.read(11)?; let addr_k = registers.read(12)?; + // The output spans +0..+95, so its bound is 95, not 31. if !addr_limb_ok(addr_xg, 31) - || !addr_limb_ok(addr_xr, 31) + || !addr_limb_ok(addr_xr, 95) || !addr_limb_ok(addr_k, 31) { return Err(ExecutionError::EcsmAddressOverflow); @@ -537,14 +539,18 @@ impl Instruction { // 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. + // The output may alias either (even though it now spans 96 bytes and + // so can cover both): its accesses are at T+2 and T+3, strictly after + // both reads, so every per-address chain stays monotone. if addr_xg.abs_diff(addr_k) < 32 { return Err(ExecutionError::EcsmOperandOverlap); } let xg = load_u256_le(memory, addr_xg)?; let k = load_u256_le(memory, addr_k)?; - let xr = ecsm::scalar_mul_x(&k, &xg)?; + let (xr, yr, yg) = ecsm::scalar_mul_full(&k, &xg)?; store_u256_le(memory, addr_xr, &xr)?; + store_u256_le(memory, addr_xr + 32, &yr)?; + store_u256_le(memory, addr_xr + 64, &yg)?; // Carry addr_xG/addr_k in the CPU log; addr_xR is recovered from x10 // by the ECSM register-read path in the trace builder. src2_val = addr_xg; diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 746bef91c..84603c09c 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -420,27 +420,46 @@ pub fn bus_interactions() -> Vec { 0, ), )); - // write xR: 4 doublewords at addr_xR + 8i (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), - ]); - out.push(BusInteraction::sender( - BusId::Memw, - mu(), - memw_write( - dword_bytes(cols::XR, i), - base_lo, - packed(cols::ADDR_XR_1), - ts_lo_plus(2), - ts_hi(), - 1, - ), - )); + // Write the 96-byte output buffer [xR ‖ yR ‖ yG] as 12 doublewords at addr_xR + off + 8i. + // + // `yG` is echoed because the chip may witness EITHER root of xG — the AIR binds only + // `yG² ≡ xG³ + b`, so nothing here pins the sign (see the "Two options for y_G" aside in + // `spec/ecsm.typ`). `yR` alone would therefore be ambiguous: it is `±y(k·P)` for the + // caller's own point P. Handing back the root the chip used lets the guest resolve it + // with one comparison, which keeps the root a free choice exactly as the aside argues + // while still exposing a usable y — and costs no column, since `YR` and `YG` are already + // witnessed (YR arrives on the ECDAS bus, YG is proved by the yG convolution). + // + // xR keeps ts + 2 (grouped with the x10 register read); yR and yG take ts + 3, the free + // fourth sub-timestamp of the instruction's stride-4 window. Several doubleword accesses + // may share a timestamp as long as their addresses differ, which they do — the three + // chunks are disjoint 32-byte ranges of one buffer. + for (col, off, ts) in [ + (cols::XR, 0i64, ts_lo_plus(2)), + (cols::YR, 32, ts_lo_plus(3)), + (cols::YG, 64, ts_lo_plus(3)), + ] { + for i in 0..4 { + let base_lo = BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::ADDR_XR_0, + }, + LinearTerm::Constant(off + (8 * i) as i64), + ]); + out.push(BusInteraction::sender( + BusId::Memw, + mu(), + memw_write( + dword_bytes(col, i), + base_lo, + packed(cols::ADDR_XR_1), + ts.clone(), + ts_hi(), + 1, + ), + )); + } } // IS_BYTE range checks (single byte → AreBytes[x, 0]). diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 29874caef..9ab202144 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -862,7 +862,7 @@ fn collect_ecsm_ops( let witness = ::ecsm::compute_witness(&k, &xg) .expect("ECSM witness: executor validates 0 < k < N and xG on curve"); - let mut memw_ops = Vec::with_capacity(15); + let mut memw_ops = Vec::with_capacity(23); // x11 -> addr_xG (register read at T), x12 -> addr_k (register read at T+1). { @@ -926,20 +926,30 @@ fn collect_ecsm_ops( register_state.write(10, val, t + 2); } - // xR writes at T + 2 (4 doublewords). - for i in 0..4 { - let addr = addr_xr.wrapping_add((8 * i) as u64); - let mut value = [0u32; 8]; - let mut dword = 0u64; - for j in 0..8 { - value[j] = witness.x_r[8 * i + j] as u32; - dword |= (witness.x_r[8 * i + j] as u64) << (8 * j); + // Output buffer [xR ‖ yR ‖ yG] — 12 doubleword writes at addr_xR + off + 8i. + // xR at T + 2 (grouped with the x10 register read), yR and yG at T + 3, the free fourth + // sub-timestamp of the stride-4 window. The three chunks are disjoint 32-byte ranges, so + // sharing T + 3 between the last two never touches an address twice. `yG` is echoed so + // the guest can tell which root of xG the chip witnessed; see `ecsm::bus_interactions`. + for (bytes, off, ts) in [ + (&witness.x_r, 0u64, t + 2), + (&witness.y_r, 32, t + 3), + (&witness.y_g, 64, t + 3), + ] { + for i in 0..4 { + let addr = addr_xr.wrapping_add(off).wrapping_add((8 * i) as u64); + let mut value = [0u32; 8]; + let mut dword = 0u64; + for j in 0..8 { + value[j] = bytes[8 * i + j] as u32; + dword |= (bytes[8 * i + j] as u64) << (8 * j); + } + let (old_vals, old_ts) = memory_state.read_bytes(addr, 8); + memw_ops.push( + MemwOperation::new(false, addr, value, ts, 8, false).with_old(old_vals, old_ts), + ); + memory_state.write_bytes(addr, dword, 8, ts); } - let (old_vals, old_ts) = memory_state.read_bytes(addr, 8); - memw_ops.push( - MemwOperation::new(false, addr, value, t + 2, 8, false).with_old(old_vals, old_ts), - ); - memory_state.write_bytes(addr, dword, 8, t + 2); } let ecdas_ops = witness diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 5228455ea..3b3592b08 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -176,24 +176,34 @@ pub fn keccak_permute(_state: &mut [u64; 25]) { } #[cfg(target_arch = "riscv64")] -/// Compute `xR = (k·G)_x` on secp256k1 via the ECSM accelerator. All values are 32-byte -/// little-endian. Requires `0 < k < N` and a canonical valid `xG` curve coordinate. -/// `xG` and `k` must not overlap; `xR` may alias either input. -pub fn ecsm_mul(xr: &mut [u8; 32], xg: &[u8; 32], k: &[u8; 32]) { +/// Compute `k·G` on secp256k1 via the ECSM accelerator, writing `[xR ‖ yR ‖ yG]` as three +/// contiguous 32-byte little-endian values into `out`. Requires `0 < k < N` and a canonical +/// valid `xG` curve coordinate. `xG` and `k` must not overlap; `out` may alias either input. +/// +/// `yG` is the root of `xG` the chip actually used, and the chip is free to pick either one +/// (the AIR binds only `yG² ≡ xG³ + b`). So `yR` is the y of `k·(xG, yG)`, which is `±y(k·P)` +/// for the caller's point `P`. Compare `yG` against your own base point's y and negate `yR` +/// when they differ; that also validates `yG`, since a value that is neither root means the +/// output is unusable and the caller should fall back. +/// +/// `out` should be 8-byte aligned so the twelve doubleword accesses land on the aligned +/// memory path (MEMW_A) instead of the general one; the same goes for `xg` and `k`. +pub fn ecsm_mul(out: &mut [u8; 96], xg: &[u8; 32], k: &[u8; 32]) { unsafe { asm!( "ecall", - in("a0") xr.as_mut_ptr(), // x10 = address to write xR - in("a1") xg.as_ptr(), // x11 = address of xG - in("a2") k.as_ptr(), // x12 = address of k + in("a0") out.as_mut_ptr(), // x10 = address to write [xR ‖ yR ‖ yG] + in("a1") xg.as_ptr(), // x11 = address of xG + in("a2") k.as_ptr(), // x12 = address of k in("a7") ECSM_SYSCALL_NUMBER, ) } } #[cfg(not(target_arch = "riscv64"))] -/// Compute `xR = (k·G)_x` on secp256k1 via the ECSM accelerator (32-byte little-endian values). -pub fn ecsm_mul(_xr: &mut [u8; 32], _xg: &[u8; 32], _k: &[u8; 32]) { +/// Compute `k·G` on secp256k1 via the ECSM accelerator, writing `[xR ‖ yR ‖ yG]` +/// (three 32-byte little-endian values) into `out`. +pub fn ecsm_mul(_out: &mut [u8; 96], _xg: &[u8; 32], _k: &[u8; 32]) { unimplemented!("syscalls are only implemented for riscv64 targets"); } From 2b15c92946bcc4d8c40c9b9d6c4204948782bfae Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 19 Aug 2026 16:26:29 -0300 Subject: [PATCH 02/11] fix(ci): satisfy the lint gate on the new ECSM executor test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `make lint` (the required check) runs `cargo fmt --check --all` and four clippy passes with `-D warnings`. The new `run_ecsm_full` helper tripped both: clippy::type_complexity on its `Result<([u8; 32], [u8; 32], [u8; 32]), _>` return, and then rustfmt on the one-line form the fix produced. Reuse the `ecsm::EcsmOutput` alias the crate already exports for exactly this shape, and re-run rustfmt. `make lint` now exits 0. Also type-checked the riscv64-gated `ecsm_oracle` body on host with a stub ecall (that code is behind `#[cfg(target_arch = "riscv64")]`, so neither `make lint` nor the host tests ever compile it): it builds, both `Align8` buffers come out 8-aligned, and the three 32-byte chunks are extracted in [xR ‖ yR ‖ yG] order. `commit` takes `&[u8]`, so the guest program's `commit(&out.0[..32])` is well-typed. `make test-ethrex-crypto` runs both profiles deliberately (k256 swaps its FieldElement implementation and only asserts magnitudes in debug); 26/26 in each. --- executor/src/tests/ecsm_tests.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/executor/src/tests/ecsm_tests.rs b/executor/src/tests/ecsm_tests.rs index 2b2d2d220..ce4e3c11b 100644 --- a/executor/src/tests/ecsm_tests.rs +++ b/executor/src/tests/ecsm_tests.rs @@ -177,10 +177,7 @@ fn ecsm_syscall_rejects_address_overflow() { /// Runs the ECSM syscall and returns the whole 96-byte output buffer as /// `(xR, yR, yG)`, all little-endian. -fn run_ecsm_full( - k_bytes: &[u8; 32], - xg_le: &[u8; 32], -) -> Result<([u8; 32], [u8; 32], [u8; 32]), ExecutionError> { +fn run_ecsm_full(k_bytes: &[u8; 32], xg_le: &[u8; 32]) -> Result { let mut pc = 0; let mut registers = Registers::default(); let mut memory = Memory::default(); From 33ef45c8f6f971bf90148b297ec1f9da439b34a2 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 25 Aug 2026 10:33:52 -0300 Subject: [PATCH 03/11] Cover ECSM's echoed writes and aliased output --- executor/programs/asm/test_ecsm_alias.s | 52 ++++++++ prover/src/tests/prove_elfs_tests.rs | 152 ++++++++++++++++++++++++ 2 files changed, 204 insertions(+) create mode 100644 executor/programs/asm/test_ecsm_alias.s diff --git a/executor/programs/asm/test_ecsm_alias.s b/executor/programs/asm/test_ecsm_alias.s new file mode 100644 index 000000000..3e064948c --- /dev/null +++ b/executor/programs/asm/test_ecsm_alias.s @@ -0,0 +1,52 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + # Same 5·G computation as `test_ecsm`, but the 96-byte output buffer is + # pointed AT the inputs: out = sp+0 covers xG (sp+0..32) and k (sp+32..64). + # The ecall reads both operands before it writes anything (reads at T and + # T+1, xR at T+2, yR and yG at T+3), so the result must be the same as the + # disjoint case even though every input byte is overwritten. That ordering + # is what keeps each per-address chain monotone, and it is only proven if a + # proof of this program verifies. + addi sp, sp, -160 + + # xG = secp256k1 Gx, little-endian (4 doublewords). + 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 (little-endian). + li t0, 5 + sd t0, 32(sp) + sd zero, 40(sp) + sd zero, 48(sp) + sd zero, 56(sp) + + # ECSM ecall: a0 = &out (96 bytes, aliasing both inputs), a1 = &xG, + # a2 = &k, a7 = -11. + addi a0, sp, 0 + addi a1, sp, 0 + addi a2, sp, 32 + li a7, -11 + ecall + + # Commit xR, which now sits where xG used to be. + # Commit syscall: a0 = fd(1), a1 = buf_addr, a2 = count, a7 = 64. + li a0, 1 + addi a1, sp, 0 + li a2, 32 + li a7, 64 + ecall + + # Restore stack and halt. + addi sp, sp, 160 + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index e45c7b927..d4b10a175 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -19,11 +19,14 @@ use stark::constraints::builder::EmptyConstraints; use stark::lookup::{AirWithBuses, AuxiliaryTraceBuildData}; use stark::proof::options::ProofOptions; use stark::proof::view::{MultiProofView, StarkProofView}; +use stark::trace::TraceTable; use stark::traits::AIR; use stark::verifier::{IsStarkVerifier, Verifier}; use crate::VmProof; use crate::tables::MaxRowsConfig; +use crate::tables::memw::cols as memw_cols; +use crate::tables::memw_aligned::cols as memw_aligned_cols; use crate::tables::trace_builder::Traces; use crate::tables::types::{GoldilocksExtension, GoldilocksField}; @@ -1602,6 +1605,155 @@ fn test_prove_elfs_ecsm_forged_ecdas_mu_rejected() { ); } +/// Runs an ECSM asm guest and returns its ELF plus the minimal traces, the shape +/// the three tests below share. +fn ecsm_traces(program: &str) -> (Elf, Traces) { + let elf_bytes = crate::test_utils::asm_elf_bytes(program); + let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); + let result = executor::vm::execution::Executor::new(&elf, vec![]) + .expect("Failed to create executor") + .run() + .expect("Failed to run program"); + let traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + (elf, traces) +} + +/// Where a memory table keeps the three cells these tests read. The general and +/// the aligned MEMW tables lay their rows out differently, and an ECSM write goes +/// to whichever one the caller's buffer alignment selects, so neither layout can +/// be assumed. +struct MemwLayout { + is_register: usize, + timestamp_lo: usize, + timestamp_hi: usize, + first_value: usize, +} + +const MEMW: MemwLayout = MemwLayout { + is_register: memw_cols::IS_REGISTER, + timestamp_lo: memw_cols::TIMESTAMP_0, + timestamp_hi: memw_cols::TIMESTAMP_1, + first_value: memw_cols::VALUE[0], +}; + +const MEMW_ALIGNED: MemwLayout = MemwLayout { + is_register: memw_aligned_cols::IS_REGISTER, + timestamp_lo: memw_aligned_cols::TIMESTAMP_0, + timestamp_hi: memw_aligned_cols::TIMESTAMP_1, + first_value: memw_aligned_cols::VALUE[0], +}; + +/// The timestamp of the single real ECSM row (row 0; these guests make one call). +fn ecsm_timestamp(traces: &Traces) -> u64 { + dword_wl( + &traces.ecsm, + 0, + crate::tables::ecsm::cols::TIMESTAMP_0, + crate::tables::ecsm::cols::TIMESTAMP_1, + ) +} + +/// A `DWordWL` pair read back as one number. +fn dword_wl( + table: &TraceTable, + row: usize, + lo: usize, + hi: usize, +) -> u64 { + table.main_table.get(row, lo).to_raw() + (table.main_table.get(row, hi).to_raw() << 32) +} + +/// Rows of memory (not register) writes/reads at `timestamp`, as +/// `(table index in its own vector, row)`, keyed by which table they came from. +fn memory_rows_at_timestamp(traces: &Traces, timestamp: u64) -> Vec<(bool, usize, usize)> { + let mut out = Vec::new(); + for (aligned, tables) in [(false, &traces.memws), (true, &traces.memw_aligneds)] { + let layout = if aligned { &MEMW_ALIGNED } else { &MEMW }; + for (index, table) in tables.iter().enumerate() { + for row in 0..table.num_rows() { + let is_register = table.main_table.get(row, layout.is_register).to_raw(); + let ts = dword_wl(table, row, layout.timestamp_lo, layout.timestamp_hi); + if is_register == 0 && ts == timestamp { + out.push((aligned, index, row)); + } + } + } + } + out +} + +/// The echoed outputs are only worth anything if the memory they land in is +/// authenticated, so this pins the shape of the writes #941 adds: `yR` and `yG` +/// are written at the ECSM ecall's FOURTH sub-timestamp (reads at T and T+1, +/// the register read and `xR` at T+2), four doublewords each. Eight non-register +/// memory rows at `ts + 3` is what "the free fourth sub-timestamp" means +/// concretely, and it is the window the design says is now full. +#[test] +fn test_ecsm_echoes_yr_and_yg_at_the_fourth_subtimestamp() { + let _ = env_logger::builder().is_test(true).try_init(); + + let (_elf, traces) = ecsm_traces("test_ecsm"); + let writes = memory_rows_at_timestamp(&traces, ecsm_timestamp(&traces) + 3); + + assert_eq!( + writes.len(), + 8, + "yR and yG are four doublewords each, all at the ecall's fourth \ + sub-timestamp; a different count means the write schedule moved" + ); +} + +/// Verifier REJECTS a forged value on one of the echoed writes. `yR` arrives on +/// the ECDAS bus and `yG` is the witnessed root, so both were already in the +/// trace before #941 — what is new is that they are WRITTEN, and a write is only +/// trustworthy if the memory argument ties it to the chip's own witness. Forge +/// the payload of one of those rows and the memory bus must not balance. +#[test] +fn test_prove_elfs_ecsm_forged_echoed_write_rejected() { + let _ = env_logger::builder().is_test(true).try_init(); + + let (elf, mut traces) = ecsm_traces("test_ecsm"); + let target = ecsm_timestamp(&traces) + 3; + + let rows = memory_rows_at_timestamp(&traces, target); + let &(aligned, index, row) = rows + .first() + .expect("no echoed write found at the fourth sub-timestamp — the tamper would be vacuous"); + let layout = if aligned { &MEMW_ALIGNED } else { &MEMW }; + let table = if aligned { + &mut traces.memw_aligneds[index] + } else { + &mut traces.memws[index] + }; + let value = table.main_table.get(row, layout.first_value); + table.main_table.set( + row, + layout.first_value, + value + FieldElement::::one(), + ); + + assert!( + !prove_and_verify_vm_minimal(&elf, &mut traces), + "Verifier must reject a forged payload on an echoed yR/yG write" + ); +} + +/// The 96-byte output buffer is allowed to alias either input, which the design +/// justifies by the read/write timestamp split. The executor covers that the +/// bytes come out right; this covers that the TRACE of it verifies — the claim +/// is about per-address chains staying monotone, and only a proof exercises them. +#[test] +fn test_prove_elfs_ecsm_output_aliases_inputs() { + let _ = env_logger::builder().is_test(true).try_init(); + + let (elf, mut traces) = ecsm_traces("test_ecsm_alias"); + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "a proof of an ECSM call whose output aliases its inputs must verify" + ); +} + /// Verifier REJECTS a forged trace where an addr byte cell is set to a /// non-byte field element. /// From 38d182cd5d5c30c444ea313635a4bfd5b7e92650 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Mon, 24 Aug 2026 18:07:41 -0300 Subject: [PATCH 04/11] Reject a forged yR or yG, and pin the write group This PR turns yR and yG into values the guest reads and trusts: it reconstructs k*P from yR and resolves the root by comparing the echoed yG against its own y. Both were unforgeable already -- yR through the ECDAS final-receiver tuple, yG through the yG convolution -- but only xR had a test saying so, and the argument that yR is not a free witness lives entirely in a bus tuple's column offsets. Two end-to-end forgery tests, the same shape as the xR one: move the low byte of yR, and of yG, on the single real ECSM row, and the verifier must reject. Two structural tests, because the rest is offsets nothing else checks: - the twelve MEMW writes of [xR || yR || yG], their address offsets (0/32/64 + 8i off ADDR_XR) and their timestamps (xR at T+2, yR and yG at T+3). The aliasing argument is exactly this layout -- the operands are read at T and T+1, so a write moving back onto a read's timestamp would touch one address twice and the memory argument could not prove the chain. T+3 is also the last sub-timestamp of the stride-4 window, so a fourth group has nowhere to go. - the ECDAS tuples: the final receiver's accumulator is (xR, yR), the start sender's is (xG, yG). That is what makes yR the constrained double-and-add output rather than a witness the prover picks. Also fixes collect_ecsm_ops's header comment, which still described the write group as xR at T+2 with no mention of yR/yG at T+3, and adds the cols::yr accessor the xr/xg/yg ones already had. --- prover/src/tables/ecsm.rs | 4 + prover/src/tables/trace_builder.rs | 9 +- prover/src/tests/ecsm_tests.rs | 129 ++++++++++++++++++++++++++- prover/src/tests/prove_elfs_tests.rs | 62 +++++++++++++ 4 files changed, 199 insertions(+), 5 deletions(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 84603c09c..bb5d8d05e 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -63,6 +63,10 @@ pub mod cols { pub const fn xr(i: usize) -> usize { XR + i } + #[inline] + pub const fn yr(i: usize) -> usize { + YR + i + } /// Bit `i` of the scalar `k` (0 = LSB, 255 = MSB). #[inline] pub const fn k_bit(i: usize) -> usize { diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index d44d6b9e7..00c8e6d4a 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -832,10 +832,13 @@ fn collect_store_op_from_cpu(op: &CpuOperation, memory_state: &mut MemoryState) /// Collects all MEMW ops and the ECSM / ECDAS table ops for one ECSM ecall. /// /// Timestamp scheme: `x11` register read and `xG` memory reads at `T`; -/// `x12` register read and `k` memory reads at `T + 1`; `x10` register read and -/// `xR` memory writes at `T + 2`. Every read advances +/// `x12` register read and `k` memory reads at `T + 1`; `x10` register read and the four +/// `xR` memory writes at `T + 2`; the `yR` and `yG` writes at `T + 3`, the fourth and last +/// sub-timestamp of the instruction's stride-4 window. Every read advances /// `memory_state` / `register_state` (the offline read-old + write-new model), so later -/// accesses always observe a strictly smaller old timestamp. +/// accesses always observe a strictly smaller old timestamp — and every write of the +/// 96-byte output lands strictly after both operand reads, which is what lets the output +/// buffer alias `xG` or `k` even though it can now cover both. #[allow(clippy::needless_range_loop)] fn collect_ecsm_ops( op: &CpuOperation, diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index 91956c5ad..f5791992b 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -2,12 +2,15 @@ //! the single-source constraint count, and isolated negative checks for the //! padding closure, the scalar-bit padding guard and the `xG < p` overflow. -use crate::tables::ecsm::{EcsmConstraints, EcsmOperation, cols, generate_ecsm_trace}; -use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; +use crate::tables::ecsm::{ + EcsmConstraints, EcsmOperation, bus_interactions, cols, generate_ecsm_trace, +}; +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; use ecsm::{N_BYTES, P_BYTES, compute_witness}; use math::field::element::FieldElement; use stark::constraints::builder::{ConstraintSet, ProverEvalFolder}; use stark::frame::Frame; +use stark::lookup::{BusValue, LinearTerm}; use stark::table::TableView; use stark::trace::TraceTable; use stark::traits::TransitionEvaluationContext; @@ -267,3 +270,125 @@ fn constraints_hold_for_k_eq_n_minus_one() { } } } + +// ========================================================================= +// Structural: the 96-byte output buffer and its ECDAS backing +// ========================================================================= + +/// The single column of a `Packed` bus value. +fn packed_col(v: &BusValue) -> Option { + match v { + BusValue::Packed { start_column, .. } => Some(*start_column), + _ => None, + } +} + +/// `(column, constant)` of a `Linear` bus value shaped `1·col + k`. +fn linear_col_plus(v: &BusValue) -> Option<(usize, i64)> { + let BusValue::Linear(terms) = v else { + return None; + }; + let mut col = None; + let mut constant = 0i64; + for t in terms { + match t { + LinearTerm::Column { + coefficient: 1, + column, + } => col = Some(*column), + LinearTerm::Constant(k) => constant += k, + _ => return None, + } + } + col.map(|c| (c, constant)) +} + +/// The chip publishes `[xR ‖ yR ‖ yG]` as twelve doubleword MEMW writes, and the aliasing +/// argument rests on WHEN they happen: the operands are read at `T` and `T + 1`, so every +/// write must land strictly later, or an output buffer overlapping `xG`/`k` would touch one +/// address twice at the same timestamp. `yR` and `yG` share `T + 3`, which is legal only +/// because their address ranges are disjoint — and `T + 3` is the last sub-timestamp of the +/// instruction's stride-4 window, so there is no room for a fourth group. +/// +/// Pin the layout: nothing else fails loudly if a write moves back onto a read's timestamp +/// or one of the two new coordinates stops being published. +#[test] +fn output_buffer_memw_writes_are_twelve_at_the_expected_offsets() { + let want: Vec<(usize, i64, i64)> = + [(cols::XR, 0i64, 2i64), (cols::YR, 32, 3), (cols::YG, 64, 3)] + .iter() + .flat_map(|&(col, off, ts)| (0..4).map(move |i| (col + 8 * i, off + 8 * i as i64, ts))) + .collect(); + + // MEMW write tuple: [is_register, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]. + let got: Vec<(usize, i64, i64)> = bus_interactions() + .iter() + .filter(|b| b.is_sender && b.bus_id == BusId::Memw as u64 && b.values.len() == 16) + .filter_map(|b| { + // Every other MEMW access this chip makes is a read, and the length filter + // already dropped those (24-element tuple), so these twelve are the buffer. + let (addr_col, addr_off) = linear_col_plus(&b.values[1])?; + assert_eq!(addr_col, cols::ADDR_XR_0); + assert_eq!(packed_col(&b.values[2]), Some(cols::ADDR_XR_1)); + let (ts_col, ts_off) = linear_col_plus(&b.values[11])?; + assert_eq!(ts_col, cols::TIMESTAMP_0); + Some((packed_col(&b.values[3])?, addr_off, ts_off)) + }) + .collect(); + + assert_eq!( + got, want, + "the [xR ‖ yR ‖ yG] write group changed shape (column, address offset, ts offset)" + ); +} + +/// `yR` is not a free column, and neither is `yG`. +/// +/// The ECDAS final receiver carries `[id, ts, xR, yR, xG, yG, −1, 0]`, so the published `yR` +/// has to match the constrained double-and-add output; the start sender carries the same +/// `(xG, yG)` the `Relation::Yg` convolution binds to the curve. The caller-side sign fix-up +/// (`ŷ = ±y` ⇒ negate or not) is sound only while both hold, so pin the tuple offsets. +#[test] +fn ecdas_tuples_carry_the_published_coordinates() { + // ECDAS tuple: [id, ts_lo, ts_hi, accX(32), accY(32), genX(32), genY(32), round, op]. + const ACC_X: usize = 3; + const ACC_Y: usize = ACC_X + 32; + const GEN_X: usize = ACC_Y + 32; + const GEN_Y: usize = GEN_X + 32; + + let coord_is = |values: &[BusValue], at: usize, base: usize| { + (0..32).all(|b| packed_col(&values[at + b]) == Some(base + b)) + }; + + let ecdas: Vec<_> = bus_interactions() + .into_iter() + .filter(|b| b.bus_id == BusId::Ecdas as u64) + .collect(); + assert_eq!( + ecdas.len(), + 2, + "ECSM sends the start tuple and receives the result" + ); + + let start = ecdas + .iter() + .find(|b| b.is_sender) + .expect("ECDAS start sender"); + assert!(coord_is(&start.values, ACC_X, cols::XG)); + assert!(coord_is(&start.values, ACC_Y, cols::YG)); + + let result = ecdas + .iter() + .find(|b| !b.is_sender) + .expect("ECDAS final receiver"); + assert!( + coord_is(&result.values, ACC_X, cols::XR), + "xR must come from the ECDAS accumulator" + ); + assert!( + coord_is(&result.values, ACC_Y, cols::YR), + "yR must come from the ECDAS accumulator, not be a free witness" + ); + assert!(coord_is(&result.values, GEN_X, cols::XG)); + assert!(coord_is(&result.values, GEN_Y, cols::YG)); +} diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index d4b10a175..ddaf2a2fa 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1575,6 +1575,68 @@ fn test_prove_elfs_ecsm_forged_result_rejected() { ); } +/// Soundness: `yR` is published to guest memory now, so it must be as unforgeable as `xR`. +/// +/// It is what the guest reconstructs `k·P` from — move it and you move the recovered public +/// key, i.e. the address `ecrecover` returns. Two things pin it: the ECDAS final-receiver +/// tuple `[ts, xR, yR, xG, yG, -1, 0]` ties the column to the constrained double-and-add +/// output, and the MEMW senders publish that same column to memory. +#[test] +fn test_prove_elfs_ecsm_forged_yr_rejected() { + use crate::tables::ecsm::cols as ecsm_cols; + + let _ = env_logger::builder().is_test(true).try_init(); + + let elf_bytes = crate::test_utils::asm_elf_bytes("test_ecsm"); + 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("Failed to run program"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + + // Forge the low byte of yR on the (single) real ECSM row. + let orig = *traces.ecsm.main_table.get(0, ecsm_cols::yr(0)); + let forged = orig + FieldElement::::one(); + traces.ecsm.main_table.set(0, ecsm_cols::yr(0), forged); + + assert!( + !prove_and_verify_vm_minimal(&elf, &mut traces), + "Verifier must reject a forged ECSM result yR" + ); +} + +/// Soundness: the prover may choose EITHER root of `xG`, but not a non-root. +/// +/// The AIR binds only `yG² ≡ xG³ + b`, and that freedom is deliberate — the guest resolves +/// the sign by comparing the echoed `yG` against its own base point's y. A `yG` free of the +/// curve relation would therefore be a free sign on `k·P`. The `Relation::Yg` convolution is +/// what forbids it; the ECDAS start tuple and the MEMW senders carry the same column. +#[test] +fn test_prove_elfs_ecsm_forged_yg_rejected() { + use crate::tables::ecsm::cols as ecsm_cols; + + let _ = env_logger::builder().is_test(true).try_init(); + + let elf_bytes = crate::test_utils::asm_elf_bytes("test_ecsm"); + 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("Failed to run program"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + + // Forge the low byte of the witnessed root yG on the (single) real ECSM row. + let orig = *traces.ecsm.main_table.get(0, ecsm_cols::yg(0)); + let forged = orig + FieldElement::::one(); + traces.ecsm.main_table.set(0, ecsm_cols::yg(0), forged); + + assert!( + !prove_and_verify_vm_minimal(&elf, &mut traces), + "Verifier must reject a yG that is not a root of xG" + ); +} + /// Regression test: `µ` is the multiplicity of every ECDAS bus interaction, so it must remain /// boolean. Forge a non-boolean `µ` on a real ECDAS row and assert the verifier rejects. /// (k=5 produces 3 ECDAS rows.) From 4e4ac27a384d7b4c4865a081ba38754797d38b63 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Mon, 24 Aug 2026 18:07:42 -0300 Subject: [PATCH 05/11] Take the ECSM operand buffers as an aligned type The doc said "out should be 8-byte aligned so the twelve doubleword accesses land on the aligned memory path (MEMW_A) instead of the general one; the same goes for xg and k". Nothing enforced it, and missing it fails silently -- 49+8 columns per access instead of 29+1, a bigger trace and no other symptom -- which is the worst failure mode to leave to a comment. The wrapper was also copied three times, in ethrex-crypto and in both guest programs. Align8 moves to lambda-vm-syscalls next to the ecall it exists for, and ecsm_mul takes &mut Align8<96> / &Align8<32> / &Align8<32>, so the alignment is a type-level guarantee. The three copies collapse into the shared one, and both guest programs now align their xG and k too, which they did not before -- their eight operand reads move to MEMW_A as well. --- crypto/ethrex-crypto/src/lib.rs | 16 ++++++------ executor/programs/bench/ecsm/src/main.rs | 21 ++++++++-------- executor/programs/rust/ecsm/src/main.rs | 20 +++++++-------- syscalls/src/syscalls.rs | 32 ++++++++++++++++++------ 4 files changed, 51 insertions(+), 38 deletions(-) diff --git a/crypto/ethrex-crypto/src/lib.rs b/crypto/ethrex-crypto/src/lib.rs index 7a4632d1b..ae3a37f3d 100644 --- a/crypto/ethrex-crypto/src/lib.rs +++ b/crypto/ethrex-crypto/src/lib.rs @@ -34,6 +34,12 @@ use k256::{AffinePoint, FieldBytes, ProjectivePoint, Scalar, U256}; // host unit tests); unused on a non-test host build. #[cfg(any(target_arch = "riscv64", test))] use k256::elliptic_curve::sec1::FromEncodedPoint; + +// 8-byte-aligned ecall operand buffers (`ecsm_mul` takes them by type; `hint` wants the +// same alignment for its four 8-byte writes). +#[cfg(target_arch = "riscv64")] +use lambda_vm_syscalls::syscalls::Align8; + #[cfg(any(target_arch = "riscv64", test))] use k256::{EncodedPoint, FieldElement}; @@ -81,14 +87,6 @@ fn get_hint(hint_id: usize, x_be: &[u8; 32]) -> [u8; 32] { out.0 } -/// 8-byte-aligned wrapper for an ecall operand buffer, so the table's 8-byte accesses land -/// on the aligned memory path (MEMW_A, 29 columns + 1 range check) instead of the general -/// one (49 + 8). A bare `[u8; N]` on the stack is only 1-aligned, which forces every access -/// onto the unaligned path and inflates the trace. -#[cfg(target_arch = "riscv64")] -#[repr(C, align(8))] -struct Align8([u8; N]); - /// Scalar-field inverse `x⁻¹ mod n`. /// /// On riscv64 the inverse is first requested from the untrusted `hint` ecall and @@ -342,7 +340,7 @@ fn ecsm_oracle(x: &FieldElement, k: &Scalar) -> Option<(FieldElement, FieldEleme k_le.0[i] = k_be[31 - i]; } let mut out = Align8([0u8; 96]); - lambda_vm_syscalls::syscalls::ecsm_mul(&mut out.0, &x_le.0, &k_le.0); + lambda_vm_syscalls::syscalls::ecsm_mul(&mut out, &x_le, &k_le); let load = |chunk: usize| -> Option { let mut be = [0u8; 32]; for i in 0..32 { diff --git a/executor/programs/bench/ecsm/src/main.rs b/executor/programs/bench/ecsm/src/main.rs index 4d311d05b..316ed55b1 100644 --- a/executor/programs/bench/ecsm/src/main.rs +++ b/executor/programs/bench/ecsm/src/main.rs @@ -7,28 +7,27 @@ const ITERATIONS: usize = 10; pub fn main() { // secp256k1 Gx, big-endian then reversed to little-endian. - let mut xg: [u8; 32] = [ + // `Align8` keeps every operand on the aligned memory path (MEMW_A). + let mut xg = syscalls::syscalls::Align8([ 0x79, 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, - ]; - xg.reverse(); + ]); + xg.0.reverse(); // k = N - 1 (largest valid scalar), big-endian then reversed to little-endian. - let mut k: [u8; 32] = [ + let mut k = syscalls::syscalls::Align8([ 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFE, 0xBA, 0xAE, 0xDC, 0xE6, 0xAF, 0x48, 0xA0, 0x3B, 0xBF, 0xD2, 0x5E, 0x8C, 0xD0, 0x36, 0x41, 0x40, - ]; - k.reverse(); + ]); + k.0.reverse(); // The precompile writes [xR ‖ yR ‖ yG]; the chain feeds xR back as the next base point. - #[repr(C, align(8))] - struct Align8([u8; N]); - let mut out = Align8([0u8; 96]); + let mut out = syscalls::syscalls::Align8::<96>::zeroed(); for _ in 0..ITERATIONS { - syscalls::syscalls::ecsm_mul(&mut out.0, &xg, &k); - xg.copy_from_slice(&out.0[..32]); + syscalls::syscalls::ecsm_mul(&mut out, &xg, &k); + xg.0.copy_from_slice(&out.0[..32]); } syscalls::syscalls::commit(&out.0[..32]); } diff --git a/executor/programs/rust/ecsm/src/main.rs b/executor/programs/rust/ecsm/src/main.rs index ea553c6d9..b6ca81971 100644 --- a/executor/programs/rust/ecsm/src/main.rs +++ b/executor/programs/rust/ecsm/src/main.rs @@ -4,21 +4,19 @@ use lambda_vm_syscalls as syscalls; /// 32-byte x-coordinate as public output. pub fn main() { // secp256k1 Gx, given big-endian then reversed to little-endian for the precompile. - let mut xg: [u8; 32] = [ + // `Align8` keeps every operand on the aligned memory path (MEMW_A). + let mut xg = syscalls::syscalls::Align8([ 0x79, 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, - ]; - xg.reverse(); + ]); + xg.0.reverse(); - let mut k = [0u8; 32]; - k[0] = 5; + let mut k = syscalls::syscalls::Align8::<32>::zeroed(); + k.0[0] = 5; - // The precompile writes [xR ‖ yR ‖ yG]; only xR is committed. 8-byte aligned so the - // twelve doubleword accesses take the aligned memory path (MEMW_A). - #[repr(C, align(8))] - struct Align8([u8; N]); - let mut out = Align8([0u8; 96]); - syscalls::syscalls::ecsm_mul(&mut out.0, &xg, &k); + // The precompile writes [xR ‖ yR ‖ yG]; only xR is committed. + let mut out = syscalls::syscalls::Align8::<96>::zeroed(); + syscalls::syscalls::ecsm_mul(&mut out, &xg, &k); syscalls::syscalls::commit(&out.0[..32]); } diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 3b3592b08..acaa7161b 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -1,6 +1,24 @@ #[cfg(target_arch = "riscv64")] use core::arch::asm; +/// 8-byte-aligned wrapper for an ecall operand buffer. +/// +/// The accelerator tables read and write their operands as doublewords. On an 8-byte-aligned +/// buffer those take the aligned memory path (`MEMW_A`, 29 columns + 1 range check); a bare +/// `[u8; N]` on the stack is only 1-aligned, which forces every access onto the general path +/// (49 + 8) and inflates the trace. Taking `&Align8` in the ecall wrappers makes that a +/// type-level guarantee rather than a comment a caller can miss — and missing it fails +/// silently, as a bigger trace and nothing else. +#[repr(C, align(8))] +pub struct Align8(pub [u8; N]); + +impl Align8 { + /// A zeroed, 8-byte-aligned buffer. + pub const fn zeroed() -> Self { + Self([0u8; N]) + } +} + /// Memory-mapped private input region start address. /// Layout: 4-byte LE length prefix at this address, data at +4. /// The host pre-loads the input; the guest reads directly (no ecall). @@ -186,15 +204,15 @@ pub fn keccak_permute(_state: &mut [u64; 25]) { /// when they differ; that also validates `yG`, since a value that is neither root means the /// output is unusable and the caller should fall back. /// -/// `out` should be 8-byte aligned so the twelve doubleword accesses land on the aligned -/// memory path (MEMW_A) instead of the general one; the same goes for `xg` and `k`. -pub fn ecsm_mul(out: &mut [u8; 96], xg: &[u8; 32], k: &[u8; 32]) { +/// All three buffers are [`Align8`], so the twenty doubleword accesses land on the aligned +/// memory path (`MEMW_A`) instead of the general one. +pub fn ecsm_mul(out: &mut Align8<96>, xg: &Align8<32>, k: &Align8<32>) { unsafe { asm!( "ecall", - in("a0") out.as_mut_ptr(), // x10 = address to write [xR ‖ yR ‖ yG] - in("a1") xg.as_ptr(), // x11 = address of xG - in("a2") k.as_ptr(), // x12 = address of k + in("a0") out.0.as_mut_ptr(), // x10 = address to write [xR ‖ yR ‖ yG] + in("a1") xg.0.as_ptr(), // x11 = address of xG + in("a2") k.0.as_ptr(), // x12 = address of k in("a7") ECSM_SYSCALL_NUMBER, ) } @@ -203,7 +221,7 @@ pub fn ecsm_mul(out: &mut [u8; 96], xg: &[u8; 32], k: &[u8; 32]) { #[cfg(not(target_arch = "riscv64"))] /// Compute `k·G` on secp256k1 via the ECSM accelerator, writing `[xR ‖ yR ‖ yG]` /// (three 32-byte little-endian values) into `out`. -pub fn ecsm_mul(_out: &mut [u8; 96], _xg: &[u8; 32], _k: &[u8; 32]) { +pub fn ecsm_mul(_out: &mut Align8<96>, _xg: &Align8<32>, _k: &Align8<32>) { unimplemented!("syscalls are only implemented for riscv64 targets"); } From e297d65837eb12b82947ee7df33be9e5f7e9ca18 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Mon, 24 Aug 2026 18:07:42 -0300 Subject: [PATCH 06/11] Pin the witness against the executor output image The executor writes scalar_mul_full's bytes into guest memory and the prover writes the witness columns; the MEMW bus asserts the two are the same claim. Publishing yR and yG put two more values under that coupling, and the two sides compute them differently -- the executor through k256's affine scalar multiplication, the witness through its own double-and-add replay. A disagreement on a sign or a representative would surface only as an unbalanced bus, on whichever scalar happened to hit it. Assert the equality directly over k = 1, 5, 0xABCDEF, (N-1)/2 and N-1, including that both sides lift xG to its even root. --- crypto/ecsm/src/tests/witness_tests.rs | 29 +++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/crypto/ecsm/src/tests/witness_tests.rs b/crypto/ecsm/src/tests/witness_tests.rs index f083a1536..88c0770e1 100644 --- a/crypto/ecsm/src/tests/witness_tests.rs +++ b/crypto/ecsm/src/tests/witness_tests.rs @@ -3,7 +3,7 @@ use num_bigint::BigUint; use crate::witness::compute_witness; -use crate::{n, scalar_mul_x, to_le_32}; +use crate::{n, scalar_mul_full, scalar_mul_x, to_le_32}; fn gx_le() -> [u8; 32] { let gx = BigUint::parse_bytes( @@ -59,3 +59,30 @@ fn witness_works_near_curve_order() { assert_eq!(w.x_r, gx); // (N-1)·G = -G shares x with G assert_eq!(w.len_k, 255); } + +/// The executor writes `scalar_mul_full`'s bytes into guest memory while the prover writes the +/// witness columns, and the MEMW bus asserts the two images are the same claim. Publishing +/// `yR` and `yG` put two more values under that coupling — the executor takes them from k256's +/// affine scalar multiplication, the witness from its own double-and-add replay — so the two +/// disagreeing anywhere (a sign, a representative) would surface only as an unbalanced bus on +/// whichever scalar hit it. Pin the agreement directly instead. +#[test] +fn witness_matches_the_executor_output_image() { + let gx = gx_le(); + let scalars = [ + BigUint::from(1u8), + BigUint::from(5u8), + BigUint::from(0xABCDEFu64), + (n() - BigUint::from(1u8)) / BigUint::from(2u8), + n() - BigUint::from(1u8), + ]; + for k_big in scalars { + let k = to_le_32(&k_big); + let w = compute_witness(&k, &gx).expect("witness"); + let (x_r, y_r, y_g) = scalar_mul_full(&k, &gx).expect("executor output"); + assert_eq!(w.x_r, x_r, "xR disagrees for k = {k_big}"); + assert_eq!(w.y_r, y_r, "yR disagrees for k = {k_big}"); + assert_eq!(w.y_g, y_g, "yG disagrees for k = {k_big}"); + assert_eq!(y_g[0] & 1, 0, "xG is lifted to its even root on both sides"); + } +} From 41dcfdb619a77ff7a908498230ad0e742a71c4b1 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Mon, 24 Aug 2026 18:07:42 -0300 Subject: [PATCH 07/11] Range-check yR and yG to < p in the ECSM AIR yR and yG are published to guest memory now, and the guest resolves the root by comparing the echoed yG against the y of its own base point. The byte range checks bound them only by 2^256, and the quotient columns absorb a multiple of p, so a prover could publish y + p: a second 256-bit representative, available whenever y < 2^256 - p (about 2^32). It agrees mod p and carries the OPPOSITE parity -- which is the bit the caller reads. Such points are constructible rather than hypothetical: p = 1 mod 3, so cubing is 3-to-1 and about a third of small y have a curve x. The PR closed this caller-side, with the CtOption from k256's FieldElement::from_bytes rejecting >= p inside ecsm_oracle. That works, but it puts the guarantee in a function that is #[cfg(target_arch = "riscv64")] -- no host test compiles it, and the unit tests cannot reach it, since FieldElement cannot represent a non-canonical value to feed it. Two chip-side range checks give the same guarantee where the rest of the chip's guarantees live, and the parse stays as a free second line. xR already had exactly this (XR_SUB_P / OverflowKind::XrLtP), so yR and yG reuse the machinery unchanged: - YR_SUB_P and YG_SUB_P, 16 halfwords each. 667 -> 699 columns - OverflowKind::YrLtP / YgLtP, 7 carry bits + overflow-required each. 413 -> 429 constraints - 32 IsHalfword sends, with the matching receives in collect_bitwise_from_ecsm -- the multiplicity has to move with the sends or the bus does not balance - y_r_sub_p / y_g_sub_p on the witness Cost is one row per ecall, so this is 32 cells and 16 constraint evaluations per ECSM call, against ECDAS's ~383 rows for the same call. What it buys, beyond not depending on an untested parse: the two caller assumptions the spec branch introduces mostly go away. ECSM-A2 ("reduce yR modulo p before use") is gone -- the chip does it. The load-bearing half of ECSM-A1 is gone too: the comparison no longer has to be made modulo p, because there is only one representative. What remains of A1 is the design's own requirement, that the caller compare the root and decline when it matches neither y nor -y. spec/ecsm-echo-yg (d4e6c123) needs the matching edit: two constraint groups in spec/src/ecsm.toml, and the "No such check is made on yR, deliberately" paragraph plus the assumptions table rewritten to match. --- crypto/ecsm/src/lib.rs | 10 +-- crypto/ecsm/src/witness.rs | 15 +++++ crypto/ethrex-crypto/src/lib.rs | 18 +++--- prover/src/tables/ecsm.rs | 97 ++++++++++++++++++++++++------ prover/src/tables/trace_builder.rs | 13 +++- prover/src/tests/ecsm_tests.rs | 31 +++++++++- syscalls/src/syscalls.rs | 3 +- 7 files changed, 154 insertions(+), 33 deletions(-) diff --git a/crypto/ecsm/src/lib.rs b/crypto/ecsm/src/lib.rs index e27bbd6e6..6de5c59bf 100644 --- a/crypto/ecsm/src/lib.rs +++ b/crypto/ecsm/src/lib.rs @@ -136,10 +136,12 @@ pub type EcsmOutput = ([u8; 32], [u8; 32], [u8; 32]); /// binds `yG² ≡ xG³ + b`, so nothing pins the sign (see `spec/ecsm.typ`, "Two options for /// `y_G`"). Returning `yR` alone would therefore be ambiguous: it is the y of `k·(xG, yG)` /// for whichever root the prover chose, which is `±y(k·P)` for the caller's own point `P`. -/// Echoing `yG` resolves it caller-side at no cost: the caller checks `yG < p` (free — it -/// is the field-element parse) and compares `yG`'s parity against its own base point's, so -/// a flipped root just flips the sign it applies to `yR`. That keeps the root a free choice -/// for the prover, exactly as the spec's aside argues, while still handing back a usable y. +/// Echoing `yG` resolves it caller-side at no cost: the caller compares `yG` against its own +/// base point's `y`, so a flipped root just flips the sign it applies to `yR`. That keeps the +/// root a free choice for the prover, exactly as the spec's aside argues, while still handing +/// back a usable y. The comparison is safe on bytes because the chip range-checks `yG < p` +/// and `yR < p` (`OverflowKind::YgLtP` / `YrLtP`): without those the prover could publish the +/// second representative `y + p`, which agrees mod `p` but carries the opposite parity. pub fn scalar_mul_full(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result { let (k, g) = prepare(k_le, xg_le)?; let r = curve::scalar_mul_affine(&k, &g); diff --git a/crypto/ecsm/src/witness.rs b/crypto/ecsm/src/witness.rs index 28b971383..c4939749d 100644 --- a/crypto/ecsm/src/witness.rs +++ b/crypto/ecsm/src/witness.rs @@ -47,6 +47,17 @@ pub struct EcsmWitness { pub k_sub_n: [u8; 32], /// `(xR - p) mod 2^256` pub x_r_sub_p: [u8; 32], + /// `(yR - p) mod 2^256`, the addend that forces `yR < p`. + pub y_r_sub_p: [u8; 32], + /// `(yG - p) mod 2^256`, the addend that forces `yG < p`. + /// + /// Both are needed because `yR` and `yG` are published to guest memory. The byte range + /// checks alone bound them by `2^256`, and the quotient columns absorb a multiple of `p`, + /// so a witness could publish `y + p` for any `y < 2^256 - p` (~2^32) — and such points + /// are constructible, since `3 | p-1` makes cubing 3-to-1, so a third of small `y` have a + /// curve `x`. `y + p` carries the opposite parity, which is exactly what the caller reads + /// to resolve the root. + pub y_g_sub_p: [u8; 32], /// position of the most significant set bit of `k` pub len_k: u8, pub x_r: [u8; 32], @@ -328,6 +339,8 @@ pub fn compute_witness(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result Result Option<(FieldElement, FieldElement, FieldElement)> { let x_be = x.to_bytes(); @@ -463,9 +464,10 @@ where /// /// The oracle multiplied `(xp, ŷ)` for whichever root `ŷ` the chip witnessed, so the result /// is `k·(xp, yp)` when `ŷ = yp` and `−k·(xp, yp)` when `ŷ = −yp`. Since `ŷ` is canonical -/// (the oracle's field-element parse rejected `≥ p`) and satisfies `ŷ² ≡ xp³ + b`, those are -/// the only two cases; anything else means the oracle did not multiply *this* point, so we -/// return `None` and the caller falls back to software. +/// (the chip's `yG < p` range check, re-checked by the oracle's parse) and satisfies +/// `ŷ² ≡ xp³ + b` (the yG convolution), those are the only two cases; anything else means the +/// oracle did not multiply *this* point, so we return `None` and the caller falls back to +/// software. /// /// Compared by value rather than `ct_eq`: k256 compares raw limbs *and* the magnitude and /// `normalized` tags, so a subtraction result never compares equal to a normalized constant diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index bb5d8d05e..63dad633d 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -28,7 +28,7 @@ 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 (699 columns; keep in sync with NUM_COLUMNS below) // ========================================================================= pub mod cols { @@ -56,8 +56,12 @@ pub mod cols { pub const K_SUB_N: usize = 634; // U256HL (16 halfwords) pub const XR_SUB_P: usize = 650; // U256HL (16 halfwords) pub const MU: usize = 666; + /// `(yR - p) mod 2^256`, the addend that forces `yR < p` (see `OverflowKind::YrLtP`). + pub const YR_SUB_P: usize = 667; // U256HL (16 halfwords) + /// `(yG - p) mod 2^256`, the addend that forces `yG < p` (see `OverflowKind::YgLtP`). + pub const YG_SUB_P: usize = 683; // U256HL (16 halfwords) - pub const NUM_COLUMNS: usize = 667; + pub const NUM_COLUMNS: usize = 699; #[inline] pub const fn xr(i: usize) -> usize { @@ -112,6 +116,14 @@ pub mod cols { pub const fn xr_sub_p(i: usize) -> usize { XR_SUB_P + i } + #[inline] + pub const fn yr_sub_p(i: usize) -> usize { + YR_SUB_P + i + } + #[inline] + pub const fn yg_sub_p(i: usize) -> usize { + YG_SUB_P + i + } } // ========================================================================= @@ -185,6 +197,8 @@ pub fn generate_ecsm_trace( write_halfwords(table, row_idx, cols::XG_SUB_P, &w.x_g_sub_p); write_halfwords(table, row_idx, cols::K_SUB_N, &w.k_sub_n); write_halfwords(table, row_idx, cols::XR_SUB_P, &w.x_r_sub_p); + write_halfwords(table, row_idx, cols::YR_SUB_P, &w.y_r_sub_p); + write_halfwords(table, row_idx, cols::YG_SUB_P, &w.y_g_sub_p); for i in 0..64 { debug_assert!((0..1 << 16).contains(&(w.c0[i] + CARRY_OFFSET_X2))); @@ -431,8 +445,13 @@ pub fn bus_interactions() -> Vec { // `spec/ecsm.typ`). `yR` alone would therefore be ambiguous: it is `±y(k·P)` for the // caller's own point P. Handing back the root the chip used lets the guest resolve it // with one comparison, which keeps the root a free choice exactly as the aside argues - // while still exposing a usable y — and costs no column, since `YR` and `YG` are already - // witnessed (YR arrives on the ECDAS bus, YG is proved by the yG convolution). + // while still exposing a usable y — and the echo itself costs no column, since `YR` and + // `YG` are already witnessed (YR arrives on the ECDAS bus, YG is proved by the yG + // convolution). The `< p` checks below are a separate choice, and those do cost columns. + // + // Both are range-checked to `< p` here (`OverflowKind::YrLtP` / `YgLtP`), so the guest + // compares the echoed root against its own `y` on canonical bytes: nothing lets the prover + // publish the second 256-bit representative `y + p`, whose parity is the opposite one. // // xR keeps ts + 2 (grouped with the x10 register read); yR and yG take ts + 3, the free // fourth sub-timestamp of the instruction's stride-4 window. Several doubleword accesses @@ -527,6 +546,26 @@ pub fn bus_interactions() -> Vec { vec![packed(cols::xr_sub_p(i))], )); } + // yR < p and yG < p. Unlike xR these are not read as numbers by this chip — they go from + // the ECDAS result / the yG witness straight to memory — but both are published to the + // guest, which resolves the root by comparing yG against its own y and then uses yR as a + // field element. Bounding them here is what lets the caller do that on bytes: without it + // the prover could publish `y + p` (possible for y < 2^256 - p ≈ 2^32, and such points + // are constructible), a second representative that agrees mod p but flips the parity. + for i in 0..16 { + out.push(BusInteraction::sender( + BusId::IsHalfword, + mu(), + vec![packed(cols::yr_sub_p(i))], + )); + } + for i in 0..16 { + out.push(BusInteraction::sender( + BusId::IsHalfword, + mu(), + vec![packed(cols::yg_sub_p(i))], + )); + } // ZERO bus: assert k != 0 (sum of byte_k[0..31] is nonzero). // byte_k[i] = Σ_{j=0}^{7} 2^j · k[8i+j], so Σ byte_k = Σ_{b=0}^{255} 2^(b%8) · k[b]. @@ -641,25 +680,30 @@ pub enum Relation { Yg, } -/// The addition-overflow range checks (`xG < p`, `k < N`, `xR < p`), whose 8 word-carries -/// `c` are virtual. Each `c_i = 2^-32·(addend0_i + addend1_i + c_{i-1} − sum_i)`. The addition -/// must overflow `2^256` (carry-out `c_7 = 1`), which proves the strict inequality: +/// The addition-overflow range checks (`xG < p`, `k < N`, `xR < p`, `yR < p`, `yG < p`), +/// whose 8 word-carries `c` are virtual. Each +/// `c_i = 2^-32·(addend0_i + addend1_i + c_{i-1} − sum_i)`. The addition must overflow +/// `2^256` (carry-out `c_7 = 1`), which proves the strict inequality: /// `xG < p` is `p + xg_sub_p = xG + 2^256`; `k < N` is `N + k_sub_N = k + 2^256`; -/// `xR < p` is `p + xR_sub_p = xR + 2^256`. +/// `xR < p` is `p + xR_sub_p = xR + 2^256`; and likewise `yR < p` / `yG < p` against `p`. #[derive(Clone, Copy)] pub enum OverflowKind { XgLtP, KLtN, XrLtP, + YrLtP, + YgLtP, } impl OverflowKind { - /// The constant addend's 32-bit word `i` (`p` for `xG u64 { let bytes = match self { - OverflowKind::XgLtP => &P_BYTES, OverflowKind::KLtN => &N_BYTES, - OverflowKind::XrLtP => &P_BYTES, + OverflowKind::XgLtP + | OverflowKind::XrLtP + | OverflowKind::YrLtP + | OverflowKind::YgLtP => &P_BYTES, }; let mut w = 0u64; for b in 0..4 { @@ -667,12 +711,15 @@ impl OverflowKind { } w } - /// Column base of the witnessed halfword addend (`xg_sub_p` / `k_sub_N` / `xR_sub_p`). + /// Column base of the witnessed halfword addend (`xg_sub_p` / `k_sub_N` / `xR_sub_p` / + /// `yR_sub_p` / `yG_sub_p`). fn addend_hl_base(self) -> usize { match self { OverflowKind::XgLtP => cols::XG_SUB_P, OverflowKind::KLtN => cols::K_SUB_N, OverflowKind::XrLtP => cols::XR_SUB_P, + OverflowKind::YrLtP => cols::YR_SUB_P, + OverflowKind::YgLtP => cols::YG_SUB_P, } } /// Column base of the sum. @@ -681,9 +728,11 @@ impl OverflowKind { OverflowKind::XgLtP => cols::XG, OverflowKind::KLtN => cols::K, OverflowKind::XrLtP => cols::XR, + OverflowKind::YrLtP => cols::YR, + OverflowKind::YgLtP => cols::YG, } } - /// Whether the sum is stored as individual bits (k) rather than bytes (xG/xR). + /// Whether the sum is stored as individual bits (k) rather than bytes (xG/xR/yR/yG). fn sum_is_bits(self) -> bool { matches!(self, OverflowKind::KLtN) } @@ -694,7 +743,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..429: // 0 : IS_BIT(MU) // 1..257 : IS_BIT(k[i]) for the 256 scalar bits // 257 : KBitsZeroOnPadding — (Σ k_bit[i])·(1−µ) @@ -709,10 +758,14 @@ impl OverflowKind { // 404 : OverflowRequired(KLtN) // 405..412 : CarryBit(XrLtP, 0..7) // 412 : OverflowRequired(XrLtP) +// 413..420 : CarryBit(YrLtP, 0..7) +// 420 : OverflowRequired(YrLtP) +// 421..428 : CarryBit(YgLtP, 0..7) +// 428 : OverflowRequired(YgLtP) use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; -/// ECSM transition constraints as a single-source [`ConstraintSet`] (413 +/// ECSM transition constraints as a single-source [`ConstraintSet`] (429 /// total). No column configuration needed (the layout is fixed via `cols`). #[derive(Clone, Copy)] pub struct EcsmConstraints; @@ -903,8 +956,16 @@ impl ConstraintSet for EcsmConstraints { b.emit_base(idx, q1_32.clone() * (one - q1_32)); idx += 1; - // xG < p, k < N and xR < p: 7 carry bits (deg 3) + overflow-required (deg 2) each. - for kind in [OverflowKind::XgLtP, OverflowKind::KLtN, OverflowKind::XrLtP] { + // xG < p, k < N, xR < p, yR < p, yG < p: 7 carry bits (deg 3) + overflow-required + // (deg 2) each. The last two bound the values this chip publishes to guest memory + // alongside xR, so the caller can compare them as bytes. + for kind in [ + OverflowKind::XgLtP, + OverflowKind::KLtN, + OverflowKind::XrLtP, + OverflowKind::YrLtP, + OverflowKind::YgLtP, + ] { let c = Self::carry_chain(b, kind); for ci in c.iter().take(7) { // µ · c_i · (1 − c_i) @@ -920,6 +981,6 @@ impl ConstraintSet for EcsmConstraints { idx += 1; } - debug_assert_eq!(idx, 413); + debug_assert_eq!(idx, 429); } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 00c8e6d4a..0b222315d 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2405,7 +2405,8 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec Vec [u8; 32] { // secp256k1 Gx, little-endian. @@ -97,7 +99,7 @@ fn constraints_hold_on_generated_trace() { #[test] fn constraint_set_count() { - assert_eq!(EcsmConstraints.meta().len(), 413); + assert_eq!(EcsmConstraints.meta().len(), 429); } /// The yG carry recurrence closes on all-zero padding because both the `µ·p²` offset and the @@ -208,6 +210,33 @@ fn xg_ge_p_overflow_required_fires() { ); } +/// `yR` and `yG` are published to guest memory, and the caller resolves the root by comparing +/// the echoed `yG` against its own `y`. A non-canonical representative would break that: `p` +/// is odd, so `y` and `p − y` differ in parity, but `y + p` — a second 256-bit representative +/// whenever `y < 2^256 − p ≈ 2^32`, and reachable, since `3 | p−1` leaves a third of the small +/// `y` with a curve `x` — carries the opposite parity. `OverflowRequired` is what forbids it; +/// `y = p` is the boundary where the addition stops overflowing. +#[test] +fn yr_and_yg_ge_p_overflow_required_fires() { + for (coord, idx, name) in [ + (cols::YR, IDX_YR_OVERFLOW, "yR"), + (cols::YG, IDX_YG_OVERFLOW, "yG"), + ] { + let mut main = vec![FE::zero(); cols::NUM_COLUMNS]; + main[cols::MU] = FE::one(); + // y = p, y_sub_p = 0 (invalid subtraction witness — fine for this isolation test). + for (i, &b) in P_BYTES.iter().enumerate() { + main[coord + i] = FE::from(b as u64); + } + let row = eval_main_row(main); + assert_ne!( + row[idx], + FE::zero(), + "OverflowRequired must fire when {name} = p" + ); + } +} + fn five_g_x_le() -> [u8; 32] { // x-coordinate of 5·G (secp256k1), little-endian. // 0x2f8bde4d1a07209355b4a7250a5c5128e88b84bddc619ab7cba8d569b240efe4 diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index acaa7161b..9115a0d73 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -202,7 +202,8 @@ pub fn keccak_permute(_state: &mut [u64; 25]) { /// (the AIR binds only `yG² ≡ xG³ + b`). So `yR` is the y of `k·(xG, yG)`, which is `±y(k·P)` /// for the caller's point `P`. Compare `yG` against your own base point's y and negate `yR` /// when they differ; that also validates `yG`, since a value that is neither root means the -/// output is unusable and the caller should fall back. +/// output is unusable and the caller should fall back. Both `yG` and `yR` come back reduced +/// mod `p` (the chip range-checks them), so the comparison is safe on the raw bytes. /// /// All three buffers are [`Align8`], so the twenty doubleword accesses land on the aligned /// memory path (`MEMW_A`) instead of the general one. From 5d0b9aae8330c46da6117600097f6f8ab431adb5 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 25 Aug 2026 10:50:30 -0300 Subject: [PATCH 08/11] Drop the weaker of the two write-schedule tests --- prover/src/tests/prove_elfs_tests.rs | 27 +++++---------------------- 1 file changed, 5 insertions(+), 22 deletions(-) diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ddaf2a2fa..ae3443282 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1745,28 +1745,11 @@ fn memory_rows_at_timestamp(traces: &Traces, timestamp: u64) -> Vec<(bool, usize out } -/// The echoed outputs are only worth anything if the memory they land in is -/// authenticated, so this pins the shape of the writes #941 adds: `yR` and `yG` -/// are written at the ECSM ecall's FOURTH sub-timestamp (reads at T and T+1, -/// the register read and `xR` at T+2), four doublewords each. Eight non-register -/// memory rows at `ts + 3` is what "the free fourth sub-timestamp" means -/// concretely, and it is the window the design says is now full. -#[test] -fn test_ecsm_echoes_yr_and_yg_at_the_fourth_subtimestamp() { - let _ = env_logger::builder().is_test(true).try_init(); - - let (_elf, traces) = ecsm_traces("test_ecsm"); - let writes = memory_rows_at_timestamp(&traces, ecsm_timestamp(&traces) + 3); - - assert_eq!( - writes.len(), - 8, - "yR and yG are four doublewords each, all at the ecall's fourth \ - sub-timestamp; a different count means the write schedule moved" - ); -} - -/// Verifier REJECTS a forged value on one of the echoed writes. `yR` arrives on +/// Verifier REJECTS a forged value on one of the echoed writes. Which rows those +/// are — twelve writes, `xR` at T+2 and `yR`/`yG` at T+3 — is pinned structurally +/// by `output_buffer_memw_writes_are_twelve_at_the_expected_offsets`; this covers +/// the live edge that structural test cannot: that the payload actually written is +/// tied to the chip's witness. `yR` arrives on /// the ECDAS bus and `yG` is the witnessed root, so both were already in the /// trace before #941 — what is new is that they are WRITTEN, and a write is only /// trustworthy if the memory argument ties it to the chip's own witness. Forge From a6b48b05aac40d6dbecb06a5bfe5abaa31c19aae Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 25 Aug 2026 10:50:53 -0300 Subject: [PATCH 09/11] Pin the sizing pass against an ECSM trace --- .../tests/count_table_lengths_drift_tests.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/prover/src/tests/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index 7337f0790..a14dc8312 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -126,3 +126,21 @@ fn count_table_lengths_matches_nonempty_hint_trace() { ); assert_count_table_lengths_matches(&elf, &result.logs); } + +/// ECSM routes three register reads, four `k`/`xG` memory reads and now TWELVE +/// output writes through the memory argument, plus the IsHalfword receives its +/// range checks add. `count_table_lengths` has no `ecall_ecsm` branch, so this +/// asserts what that omission costs: MEMW and MEMW_A are exact-match tables in +/// the helper above, so a missing replay shows up here rather than as a +/// mis-sized trace under Disk storage. +#[test] +fn count_table_lengths_matches_nonempty_ecsm_trace() { + let (elf, logs, _) = run_asm_elf("test_ecsm"); + assert!( + logs.iter().any(|log| { + log.src1_val == executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER + }), + "fixture must contain an ECSM ecall" + ); + assert_count_table_lengths_matches(&elf, &logs); +} From 69d96b1c953fb736a0cc517efd89491e3e388d70 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 25 Aug 2026 17:18:08 -0300 Subject: [PATCH 10/11] Fix the ECSM sizing gap and stale ECSM docs --- crypto/ecsm/src/witness.rs | 5 +- crypto/ethrex-crypto/src/lib.rs | 13 +++-- prover/src/tables/ecsm.rs | 10 ++-- prover/src/tables/trace_builder.rs | 18 +++++++ .../tests/count_table_lengths_drift_tests.rs | 34 +++++++++---- prover/src/tests/prove_elfs_tests.rs | 49 +++++++++++++++---- syscalls/src/syscalls.rs | 13 +++-- 7 files changed, 109 insertions(+), 33 deletions(-) diff --git a/crypto/ecsm/src/witness.rs b/crypto/ecsm/src/witness.rs index c4939749d..788df37fe 100644 --- a/crypto/ecsm/src/witness.rs +++ b/crypto/ecsm/src/witness.rs @@ -55,8 +55,9 @@ pub struct EcsmWitness { /// checks alone bound them by `2^256`, and the quotient columns absorb a multiple of `p`, /// so a witness could publish `y + p` for any `y < 2^256 - p` (~2^32) — and such points /// are constructible, since `3 | p-1` makes cubing 3-to-1, so a third of small `y` have a - /// curve `x`. `y + p` carries the opposite parity, which is exactly what the caller reads - /// to resolve the root. + /// curve `x`. Ruling it out is what makes the published bytes canonical, so a caller may + /// resolve the root by comparing them — or their parity, since `p` is odd and `y + p` + /// flips it. pub y_g_sub_p: [u8; 32], /// position of the most significant set bit of `k` pub len_k: u8, diff --git a/crypto/ethrex-crypto/src/lib.rs b/crypto/ethrex-crypto/src/lib.rs index dffdadda5..b0b1014bd 100644 --- a/crypto/ethrex-crypto/src/lib.rs +++ b/crypto/ethrex-crypto/src/lib.rs @@ -325,11 +325,14 @@ fn ecsm_lincomb2( /// arrays so the executor's `|addr_x_le − addr_k_le| ≥ 32` assumption holds by construction. /// /// `None` on any coordinate that is not a canonical field element. The chip already range- -/// checks all three to `< p` (`OverflowKind::XrLtP` / `YrLtP` / `YgLtP`), so this parse is a -/// free second line rather than the guarantee: it is what the caller would otherwise have to -/// rely on, since `p` is odd — `y` and `p − y` differ in parity, but `y + p`, a second 256-bit -/// representative when `y < 2^256 − p ≈ 2^32`, carries the *opposite* parity, which is exactly -/// what [`oracle_point`] reads to resolve the root. +/// checks all three to `< p` (`OverflowKind::XrLtP` / `YrLtP` / `YgLtP`); this parse is the +/// free second line, and together they make the ecall's output a canonical byte string. +/// +/// That canonicity is an ABI guarantee, not something this caller leans on. `y + p` — a second +/// 256-bit representative whenever `y < 2^256 − p ≈ 2^32` — agrees mod `p` but is a different +/// byte string, and flips parity because `p` is odd, so a caller that resolved the root by +/// comparing bytes or their parity would need it ruled out. [`oracle_point`] compares field +/// elements instead, so it would be right either way. #[cfg(target_arch = "riscv64")] fn ecsm_oracle(x: &FieldElement, k: &Scalar) -> Option<(FieldElement, FieldElement, FieldElement)> { let x_be = x.to_bytes(); diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 63dad633d..aa0e89a26 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -2,9 +2,10 @@ //! //! One row per `ECALL(-11)`. It reads `xG` and `k` from memory, witnesses `yG` and proves //! `yG² ≡ xG³ + b mod p` (via two byte-limb convolution relations with quotients `q0,q1` -//! and 64-entry carry arrays `c0,c1`), enforces `0 < k < N` and `xR < p`, writes `xR` back, -//! serves the scalar bits directly via the `Bit` bus, and delegates the double-and-add to ECDAS -//! over the `Ecdas`/`Bit` buses. +//! and 64-entry carry arrays `c0,c1`), enforces `0 < k < N` and `xR, yR, yG < p`, writes the +//! 96-byte output `[xR ‖ yR ‖ yG]` back (`yG` is echoed so the guest can tell which root of +//! `xG` the chip witnessed), serves the scalar bits directly via the `Bit` bus, and delegates +//! the double-and-add to ECDAS over the `Ecdas`/`Bit` buses. //! //! 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. @@ -501,7 +502,8 @@ pub fn bus_interactions() -> Vec { is_byte(cols::Q1, 33, &mut out); // q1[0..=32] (all 33 bytes) // xG and k are byte-checked at memory write time (store.rs AreBytes), not re-checked here. - // IS_HALF range checks on shifted carries, then k_sub_N / xR_sub_p. + // IS_HALF range checks on shifted carries, then xG_sub_p / k_sub_N / xR_sub_p, and + // (since the chip publishes them) yR_sub_p / yG_sub_p. let half_offset = |col: usize, off: i64| { BusValue::linear(vec![ LinearTerm::Column { diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 0b222315d..9df574b69 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -3917,6 +3917,24 @@ pub fn count_table_lengths( .ok_or_else(|| Error::Execution("commit index exceeds u32 range".into()))?; } + if cpu_op.ecall_ecsm { + // Mirror `collect_ecsm_ops`: three register reads (a0/a1/a2), four `xG` and four + // `k` doubleword reads, and the twelve writes of the `[xR ‖ yR ‖ yG]` output all + // go through the memory argument. Replaying it here keeps memory/register state + // in sync with generation, exactly like commit/hint. The LT rows those accesses + // derive are added by the `lt_from_memw + memw_aligned_count` closing below. + let (ecsm_memw, _ecsm_op, _ecdas_ops) = + collect_ecsm_ops(&cpu_op, &mut memory_state, &mut register_state); + for memw_op in &ecsm_memw { + partition_memw( + memw_op, + &mut memw_by_width, + &mut memw_aligned_count, + &mut memw_register_count, + ); + } + } + if cpu_op.ecall_hint { // Mirror `collect_hint_ops`: three register reads (a0/a1/a2) and four // 8-byte output writes go through the memory argument, plus the three LT diff --git a/prover/src/tests/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index a14dc8312..161891863 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -127,20 +127,36 @@ fn count_table_lengths_matches_nonempty_hint_trace() { assert_count_table_lengths_matches(&elf, &result.logs); } -/// ECSM routes three register reads, four `k`/`xG` memory reads and now TWELVE -/// output writes through the memory argument, plus the IsHalfword receives its -/// range checks add. `count_table_lengths` has no `ecall_ecsm` branch, so this -/// asserts what that omission costs: MEMW and MEMW_A are exact-match tables in -/// the helper above, so a missing replay shows up here rather than as a -/// mis-sized trace under Disk storage. +/// ECSM routes twenty-three MEMW ops through the memory argument per ecall: three +/// register reads (`a0`/`a1`/`a2`), four `xG` and four `k` doubleword reads, and the +/// twelve writes of the `[xR ‖ yR ‖ yG]` output. `count_table_lengths` must replay all +/// of it, or MEMW / MEMW_A (exact-match tables in the helper above) drift. +/// +/// Uses the **Rust** guest, not `test_ecsm.s`, and that choice is the whole test. The asm +/// fixtures put every operand on an 8-aligned stack slot, so all twenty memory accesses +/// take the MEMW_A route and `padded_chunked_rows` rounds both sides to the same power of +/// two — a missing replay stays invisible there. The Rust guest spreads accesses across +/// both routes, and dropping the `ecall_ecsm` branch moves the general MEMW table from 16 +/// rows to 8, which this assertion catches. #[test] fn count_table_lengths_matches_nonempty_ecsm_trace() { - let (elf, logs, _) = run_asm_elf("test_ecsm"); + let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent() + .expect("workspace root") + .to_path_buf(); + let elf_bytes = std::fs::read(workspace_root.join("executor/program_artifacts/rust/ecsm.elf")) + .expect("ecsm.elf not found — run `make compile-programs-rust`"); + let elf = Elf::load(&elf_bytes).expect("valid ECSM guest ELF"); + let result = Executor::new(&elf, vec![]) + .expect("executor") + .run() + .expect("ECSM guest execution"); + assert!( - logs.iter().any(|log| { + result.logs.iter().any(|log| { log.src1_val == executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER }), "fixture must contain an ECSM ecall" ); - assert_count_table_lengths_matches(&elf, &logs); + assert_count_table_lengths_matches(&elf, &result.logs); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ae3443282..6441bc198 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1667,9 +1667,12 @@ fn test_prove_elfs_ecsm_forged_ecdas_mu_rejected() { ); } -/// Runs an ECSM asm guest and returns its ELF plus the minimal traces, the shape -/// the three tests below share. -fn ecsm_traces(program: &str) -> (Elf, Traces) { +/// Runs an ECSM asm guest and returns its ELF, the minimal traces, and what the +/// EXECUTOR committed — the shape the tests below share. The committed bytes come +/// from the executor's own memory, not from `traces`, so a caller can check the two +/// views agree: the prover rebuilds the ECSM output from its own replay, so a guest +/// whose two images diverged would still produce a self-consistent, verifying proof. +fn ecsm_traces(program: &str) -> (Elf, Traces, Vec) { let elf_bytes = crate::test_utils::asm_elf_bytes(program); let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); let result = executor::vm::execution::Executor::new(&elf, vec![]) @@ -1678,7 +1681,7 @@ fn ecsm_traces(program: &str) -> (Elf, Traces) { .expect("Failed to run program"); let traces = Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); - (elf, traces) + (elf, traces, result.return_values.memory_values) } /// Where a memory table keeps the three cells these tests read. The general and @@ -1758,7 +1761,7 @@ fn memory_rows_at_timestamp(traces: &Traces, timestamp: u64) -> Vec<(bool, usize fn test_prove_elfs_ecsm_forged_echoed_write_rejected() { let _ = env_logger::builder().is_test(true).try_init(); - let (elf, mut traces) = ecsm_traces("test_ecsm"); + let (elf, mut traces, _committed) = ecsm_traces("test_ecsm"); let target = ecsm_timestamp(&traces) + 3; let rows = memory_rows_at_timestamp(&traces, target); @@ -1785,14 +1788,42 @@ fn test_prove_elfs_ecsm_forged_echoed_write_rejected() { } /// The 96-byte output buffer is allowed to alias either input, which the design -/// justifies by the read/write timestamp split. The executor covers that the -/// bytes come out right; this covers that the TRACE of it verifies — the claim -/// is about per-address chains staying monotone, and only a proof exercises them. +/// justifies by the read/write timestamp split. This covers both halves of that +/// claim: the ANSWER is still right when every operand byte gets overwritten, and +/// the TRACE of it verifies — the per-address chains stay monotone, which only a +/// proof exercises. +/// +/// Checking the value is not redundant with the executor's own aliasing test. The +/// prover rebuilds the ECSM output from its own memory replay rather than from the +/// executor's image, so a load/store ordering regression on either side would leave +/// both self-consistent and the proof would still verify; comparing the executor's +/// committed bytes against the expected `x(5·G)`, and the prover's view against the +/// executor's, is what ties the two together. #[test] fn test_prove_elfs_ecsm_output_aliases_inputs() { let _ = env_logger::builder().is_test(true).try_init(); - let (elf, mut traces) = ecsm_traces("test_ecsm_alias"); + let (elf, mut traces, committed) = ecsm_traces("test_ecsm_alias"); + + // The guest commits xR, which by then sits where xG used to be. + 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!( + committed, + ecsm::scalar_mul_x(&k, &gx).unwrap(), + "an output aliasing both operands must still commit x(5·G)" + ); + assert_eq!( + traces.public_output_bytes, committed, + "the prover's replay of an aliased ECSM must match the executor's memory image" + ); + assert!( prove_and_verify_vm_minimal(&elf, &mut traces), "a proof of an ECSM call whose output aliases its inputs must verify" diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 9115a0d73..a0917b99d 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -4,11 +4,16 @@ use core::arch::asm; /// 8-byte-aligned wrapper for an ecall operand buffer. /// /// The accelerator tables read and write their operands as doublewords. On an 8-byte-aligned -/// buffer those take the aligned memory path (`MEMW_A`, 29 columns + 1 range check); a bare -/// `[u8; N]` on the stack is only 1-aligned, which forces every access onto the general path -/// (49 + 8) and inflates the trace. Taking `&Align8` in the ecall wrappers makes that a -/// type-level guarantee rather than a comment a caller can miss — and missing it fails +/// buffer those can take the aligned memory path (`MEMW_A`, 29 columns + 1 range check); a +/// bare `[u8; N]` on the stack is only 1-aligned, which forces every access onto the general +/// path (49 + 8) and inflates the trace. Taking `&Align8` in the ecall wrappers puts the +/// alignment in the type rather than in a comment a caller can miss — and missing it fails /// silently, as a bigger trace and nothing else. +/// +/// Alignment is necessary, not sufficient: `MEMW_A` also requires all eight bytes of a +/// doubleword to carry the same previous timestamp, which a buffer spanning regions last +/// written at different times does not — an output aliasing an operand, say. Those accesses +/// still fall back to the general path. #[repr(C, align(8))] pub struct Align8(pub [u8; N]); From c3d0168a9e0fa83c6faa2623a47cb34c4f831d0c Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 27 Aug 2026 15:19:24 -0300 Subject: [PATCH 11/11] Make the ECSM 96-byte output hard to misuse --- crypto/ecsm/src/lib.rs | 27 +++++++++--- crypto/ecsm/src/tests/witness_tests.rs | 3 +- executor/src/tests/ecsm_tests.rs | 54 +++++++++++++++++++++--- executor/src/vm/instruction/execution.rs | 16 +++++-- 4 files changed, 84 insertions(+), 16 deletions(-) diff --git a/crypto/ecsm/src/lib.rs b/crypto/ecsm/src/lib.rs index 6de5c59bf..ed8f3c2b1 100644 --- a/crypto/ecsm/src/lib.rs +++ b/crypto/ecsm/src/lib.rs @@ -122,12 +122,25 @@ pub(crate) fn prepare( /// Computes the x-coordinate of `k·G` over secp256k1, given `k` and `xG` as little-endian /// 32-byte values. pub fn scalar_mul_x(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result<[u8; 32], EcsmError> { - Ok(scalar_mul_full(k_le, xg_le)?.0) + Ok(scalar_mul_full(k_le, xg_le)?.x_r) } -/// The ECSM ecall's memory image: `(xR, yR, yG)`, three little-endian 32-byte values written -/// back as one contiguous 96-byte buffer. -pub type EcsmOutput = ([u8; 32], [u8; 32], [u8; 32]); +/// The ECSM ecall's memory image: `xR ‖ yR ‖ yG`, three little-endian 32-byte values +/// written back as one contiguous 96-byte buffer. +/// +/// Named fields rather than a positional tuple: all three are `[u8; 32]`, so a tuple lets any +/// producer or consumer transpose `y_r` and `y_g` with nothing for the compiler to catch. The +/// two mean different things — the product's y versus the root of the *base* point — so a swap +/// does not fail loudly; it yields a wrong recovered public key. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct EcsmOutput { + /// x of `k·(xG, yG)`. + pub x_r: [u8; 32], + /// y of `k·(xG, yG)`. + pub y_r: [u8; 32], + /// The root of `xG` the multiplication actually used. + pub y_g: [u8; 32], +} /// The executor's entry point: `(xR, yR, yG)` as little-endian 32-byte values, written back /// to guest memory as one contiguous 96-byte buffer at `addr_xR`. @@ -145,5 +158,9 @@ pub type EcsmOutput = ([u8; 32], [u8; 32], [u8; 32]); pub fn scalar_mul_full(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result { let (k, g) = prepare(k_le, xg_le)?; let r = curve::scalar_mul_affine(&k, &g); - Ok((to_le_32(&r.x), to_le_32(&r.y), to_le_32(&g.y))) + Ok(EcsmOutput { + x_r: to_le_32(&r.x), + y_r: to_le_32(&r.y), + y_g: to_le_32(&g.y), + }) } diff --git a/crypto/ecsm/src/tests/witness_tests.rs b/crypto/ecsm/src/tests/witness_tests.rs index 88c0770e1..2a8867ba8 100644 --- a/crypto/ecsm/src/tests/witness_tests.rs +++ b/crypto/ecsm/src/tests/witness_tests.rs @@ -79,7 +79,8 @@ fn witness_matches_the_executor_output_image() { for k_big in scalars { let k = to_le_32(&k_big); let w = compute_witness(&k, &gx).expect("witness"); - let (x_r, y_r, y_g) = scalar_mul_full(&k, &gx).expect("executor output"); + let out = scalar_mul_full(&k, &gx).expect("executor output"); + let (x_r, y_r, y_g) = (out.x_r, out.y_r, out.y_g); assert_eq!(w.x_r, x_r, "xR disagrees for k = {k_big}"); assert_eq!(w.y_r, y_r, "yR disagrees for k = {k_big}"); assert_eq!(w.y_g, y_g, "yG disagrees for k = {k_big}"); diff --git a/executor/src/tests/ecsm_tests.rs b/executor/src/tests/ecsm_tests.rs index ce4e3c11b..e1279199f 100644 --- a/executor/src/tests/ecsm_tests.rs +++ b/executor/src/tests/ecsm_tests.rs @@ -156,6 +156,44 @@ fn ecsm_syscall_rejects_overlapping_xg_k() { run_ecsm_at(0x3000, 0x2000, 0x3000).expect("xR aliasing k is allowed"); } +/// The output spans 96 bytes, so it can cover **both** 32-byte operands at once. The syscall +/// allows that on the grounds that the reads land at T and T+1 and the writes at T+2/T+3 — +/// i.e. both operands are loaded before the first output byte is stored. The cases above only +/// ever alias one operand at a time, and the two-at-once shape was covered solely by the +/// prover-side `test_ecsm_alias.s`; the load-before-store ordering it rests on lives here. +#[test] +fn ecsm_syscall_output_may_span_both_operands() { + let xg = gx_le(); + let k = k_le(0xABCDEF); + + // xG at 0x2000..0x2020 and k at 0x2020..0x2040 are disjoint at the exact boundary the + // overlap guard permits (|diff| = 32). The output at 0x2000 runs to 0x2060 and so covers + // both of them. + let addr_out = 0x2000u64; + let addr_xg = 0x2000u64; + let addr_k = 0x2020u64; + + let mut pc = 0; + let mut registers = Registers::default(); + let mut memory = Memory::default(); + write_u256_le(&mut memory, addr_xg, &xg); + write_u256_le(&mut memory, addr_k, &k); + registers.write(17, ECSM_SYSCALL_NUMBER).unwrap(); + registers.write(10, addr_out).unwrap(); + registers.write(11, addr_xg).unwrap(); + registers.write(12, addr_k).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, &mut memory) + .expect("an output covering both operands must run"); + + // Had either operand been read after the output began overwriting it, the multiply would + // have consumed clobbered bytes and this would not match the pure computation. + let expected = ecsm::scalar_mul_full(&k, &xg).unwrap(); + assert_eq!(read_u256_le(&memory, addr_out), expected.x_r, "xR"); + assert_eq!(read_u256_le(&memory, addr_out + 32), expected.y_r, "yR"); + assert_eq!(read_u256_le(&memory, addr_out + 64), expected.y_g, "yG"); +} + #[test] fn ecsm_syscall_rejects_address_overflow() { // Every operand's last accessed byte must stay in the limb (+31); the 0xFFFF_FFE1 @@ -194,11 +232,11 @@ fn run_ecsm_full(k_bytes: &[u8; 32], xg_le: &[u8; 32]) -> Result