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..ed8f3c2b1 100644 --- a/crypto/ecsm/src/lib.rs +++ b/crypto/ecsm/src/lib.rs @@ -120,9 +120,47 @@ 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)?.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. +/// +/// 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`. +/// +/// `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 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)?; - Ok(to_le_32(&curve::scalar_mul_affine_x(&k, &g))) + let r = curve::scalar_mul_affine(&k, &g); + 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 f083a1536..2a8867ba8 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,31 @@ 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 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}"); + assert_eq!(y_g[0] & 1, 0, "xG is lifted to its even root on both sides"); + } +} diff --git a/crypto/ecsm/src/witness.rs b/crypto/ecsm/src/witness.rs index 28b971383..788df37fe 100644 --- a/crypto/ecsm/src/witness.rs +++ b/crypto/ecsm/src/witness.rs @@ -47,6 +47,18 @@ 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`. 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, pub x_r: [u8; 32], @@ -328,6 +340,8 @@ pub fn compute_witness(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result Result [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 } @@ -288,10 +289,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 +314,45 @@ 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. The chip already range- +/// 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 { +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, &x_le, &k_le); + 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 +404,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 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 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 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 +429,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 +463,38 @@ 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 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 +/// 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_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/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..316ed55b1 100644 --- a/executor/programs/bench/ecsm/src/main.rs +++ b/executor/programs/bench/ecsm/src/main.rs @@ -7,25 +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(); - let mut xr = [0u8; 32]; + // The precompile writes [xR ‖ yR ‖ yG]; the chain feeds xR back as the next base point. + let mut out = syscalls::syscalls::Align8::<96>::zeroed(); for _ in 0..ITERATIONS { - syscalls::syscalls::ecsm_mul(&mut xr, &xg, &k); - xg = xr; + syscalls::syscalls::ecsm_mul(&mut out, &xg, &k); + xg.0.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..b6ca81971 100644 --- a/executor/programs/rust/ecsm/src/main.rs +++ b/executor/programs/rust/ecsm/src/main.rs @@ -4,17 +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; - 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. + 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/executor/src/tests/ecsm_tests.rs b/executor/src/tests/ecsm_tests.rs index 0fa240a8e..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 @@ -174,3 +212,82 @@ 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 { + 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(ecsm::EcsmOutput { + x_r: read_u256_le(&memory, addr_out), + y_r: read_u256_le(&memory, addr_out + 32), + y_g: 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 ecsm::EcsmOutput { + x_r: xr, + y_r: yr, + y_g: 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..39ec09047 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,26 @@ 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)?; - store_u256_le(memory, addr_xr, &xr)?; + let out = ecsm::scalar_mul_full(&k, &xg)?; + // `checked_add` rather than `+`, as the keccak lane pointers above do: + // the bound at the top of this arm already forces `addr_xr + 95` to fit, + // but that leaves the argument twenty lines from its use. If the bound is + // ever relaxed or reordered, a wrap here would land the write on an + // unrelated region in release builds instead of erroring. + for (off, value) in [(0u64, &out.x_r), (32, &out.y_r), (64, &out.y_g)] { + let addr = addr_xr + .checked_add(off) + .ok_or(ExecutionError::EcsmAddressOverflow)?; + store_u256_le(memory, addr, value)?; + } // 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..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. @@ -28,7 +29,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,13 +57,21 @@ 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 { 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 { @@ -108,6 +117,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 + } } // ========================================================================= @@ -181,6 +198,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))); @@ -420,27 +439,51 @@ 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 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 + // 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]). @@ -459,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 { @@ -504,6 +548,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]. @@ -618,25 +682,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 { @@ -644,12 +713,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. @@ -658,9 +730,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) } @@ -671,7 +745,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−µ) @@ -686,10 +760,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; @@ -880,8 +958,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) @@ -897,6 +983,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 d3560826a..9df574b69 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, @@ -862,7 +865,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 +929,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 @@ -2392,7 +2405,8 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec Vec [u8; 32] { // secp256k1 Gx, little-endian. @@ -94,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 @@ -205,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 @@ -267,3 +299,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 e45c7b927..6441bc198 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}; @@ -1572,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.) @@ -1602,6 +1667,169 @@ fn test_prove_elfs_ecsm_forged_ecdas_mu_rejected() { ); } +/// 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![]) + .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, result.return_values.memory_values) +} + +/// 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 +} + +/// 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 +/// 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, _committed) = 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. 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, 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" + ); +} + /// Verifier REJECTS a forged trace where an addr byte cell is set to a /// non-byte field element. /// diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 5228455ea..a0917b99d 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -1,6 +1,29 @@ #[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 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]); + +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). @@ -176,24 +199,35 @@ 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. 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. +pub fn ecsm_mul(out: &mut Align8<96>, xg: &Align8<32>, k: &Align8<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.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, ) } } #[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 Align8<96>, _xg: &Align8<32>, _k: &Align8<32>) { unimplemented!("syscalls are only implemented for riscv64 targets"); }