diff --git a/crypto/ecsm/src/lib.rs b/crypto/ecsm/src/lib.rs index 3a0a44dff..e3a5e3a33 100644 --- a/crypto/ecsm/src/lib.rs +++ b/crypto/ecsm/src/lib.rs @@ -2,7 +2,7 @@ //! //! This crate is shared by the executor (which needs `k·G`'s x-coordinate to write back //! to guest memory) and the prover (which replays the full double-and-add sequence to -//! fill the ECSM / ECDAS / EC_SCALAR trace witnesses). Both entry points compute the same +//! fill the ECSM / ECDAS trace witnesses). Both entry points compute the same //! `k·G` over the audited `k256` curve arithmetic — the executor via `k256`'s scalar //! multiplication, the prover via a projective double-and-add replay — so the x-coordinate //! they write/prove agrees. It is also independent of the `yG` root: both recover the same diff --git a/crypto/ecsm/src/witness.rs b/crypto/ecsm/src/witness.rs index 9322cba7e..acfd820f2 100644 --- a/crypto/ecsm/src/witness.rs +++ b/crypto/ecsm/src/witness.rs @@ -38,6 +38,8 @@ pub struct EcsmWitness { pub q1: [u8; 33], /// carries for the `yG` relation pub c1: [i64; 64], + /// `(xG - p) mod 2^256` + pub x_g_sub_p: [u8; 32], /// `(k - N) mod 2^256` pub k_sub_n: [u8; 32], /// `(xR - p) mod 2^256` @@ -314,6 +316,7 @@ pub fn compute_witness(k_le: &[u8; 32], xg_le: &[u8; 32]) -> Result Result, @@ -285,7 +284,6 @@ impl VmAirs { (self.keccak_rnd.as_ref(), &mut traces.keccak_rnd, &()), (self.keccak_rc.as_ref(), &mut traces.keccak_rc, &()), (self.ecsm.as_ref(), &mut traces.ecsm, &()), - (self.ec_scalar.as_ref(), &mut traces.ec_scalar, &()), (self.ecdas.as_ref(), &mut traces.ecdas, &()), (self.register.as_ref(), &mut traces.register, &()), ]; @@ -360,7 +358,6 @@ impl VmAirs { self.keccak_rnd.as_ref(), self.keccak_rc.as_ref(), self.ecsm.as_ref(), - self.ec_scalar.as_ref(), self.ecdas.as_ref(), self.register.as_ref(), ]; @@ -534,7 +531,6 @@ impl VmAirs { tables::keccak_rc::NUM_PRECOMPUTED_COLS, )); let ecsm: VmAir = Box::new(create_ecsm_air(proof_options)); - let ec_scalar: VmAir = Box::new(create_ec_scalar_air(proof_options)); let ecdas: VmAir = Box::new(create_ecdas_air(proof_options)); let register: VmAir = if let Some((commitment, num_preprocessed_cols)) = register_preprocessed { @@ -641,7 +637,6 @@ impl VmAirs { keccak_rnd, keccak_rc, ecsm, - ec_scalar, ecdas, register, pages, diff --git a/prover/src/tables/ec_scalar.rs b/prover/src/tables/ec_scalar.rs deleted file mode 100644 index 08f797f47..000000000 --- a/prover/src/tables/ec_scalar.rs +++ /dev/null @@ -1,318 +0,0 @@ -//! EC_SCALAR chip — serves the scalar `k` bit-by-bit to the ECDAS chip. -//! -//! One row per scalar byte (32 rows per ECSM ecall, `offset` counting down 31→0). Each row -//! receives a `ServeK[timestamp, ptr, offset]` token, reads byte `k[offset]` from memory, -//! decomposes it into 8 bits, and sends one `Bit[timestamp, 8*offset + i]` token per set bit -//! (the multiplicity is the bit itself). Unless `last_limb` (offset 0) it recurses by sending -//! `ServeK[timestamp, ptr, offset-1]` — a self-referential bus, like COMMIT's `CommitNextByte`. -//! -//! ## Columns (15 total) -//! - `timestamp`: DWordWL (2) — the ECALL timestamp -//! - `ptr`: DWordWL (2) — address of `k` (= `addr_k`) -//! - `offset`: Byte (1) — index of the scalar byte served by this row -//! - `limb_bits`: Bit[8] (8) — bit decomposition of `k[offset]` -//! - `last_limb`: Bit (1) — whether `offset == 0` (terminates the recursion) -//! - `mu`: Bit (1) — multiplicity (1 for real rows, 0 for padding) -//! -//! `limb = Σ 2^i · limb_bits[i]` is virtual (a linear combination, never stored). - -use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; -use stark::trace::TraceTable; - -use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; - -// ========================================================================= -// Column indices -// ========================================================================= - -pub mod cols { - pub const TIMESTAMP_0: usize = 0; - pub const TIMESTAMP_1: usize = 1; - pub const PTR_0: usize = 2; - pub const PTR_1: usize = 3; - pub const OFFSET: usize = 4; - /// limb_bits[0..8] - pub const LIMB_BITS: usize = 5; - pub const LAST_LIMB: usize = 13; - pub const MU: usize = 14; - - pub const NUM_COLUMNS: usize = 15; - - #[inline] - pub const fn limb_bit(i: usize) -> usize { - LIMB_BITS + i - } -} - -// ========================================================================= -// Operation struct -// ========================================================================= - -/// One EC_SCALAR row: serving byte `offset` of the scalar at `ptr`. -#[derive(Debug, Clone)] -pub struct EcScalarOperation { - pub timestamp: u64, - pub ptr: u64, - pub offset: u8, - pub limb: u8, - pub last_limb: bool, -} - -/// Expands a scalar `k` (little-endian bytes) and its ECALL timestamp / address into the -/// 32 EC_SCALAR rows (offsets 31 down to 0). -pub fn rows_for_scalar(timestamp: u64, addr_k: u64, k: &[u8; 32]) -> Vec { - (0..32) - .rev() - .map(|offset| EcScalarOperation { - timestamp, - ptr: addr_k, - offset: offset as u8, - limb: k[offset], - last_limb: offset == 0, - }) - .collect() -} - -// ========================================================================= -// Trace generation -// ========================================================================= - -pub fn generate_ec_scalar_trace( - ops: &[EcScalarOperation], -) -> TraceTable { - let n = ops.len(); - let num_rows = n.next_power_of_two().max(4); - let mut trace = TraceTable::new_main( - crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), - cols::NUM_COLUMNS, - 1, - ); - let table = &mut trace.main_table; - - for (row_idx, op) in ops.iter().enumerate() { - table.set_dword_wl(row_idx, cols::TIMESTAMP_0, op.timestamp); - table.set_dword_wl(row_idx, cols::PTR_0, op.ptr); - table.set_byte(row_idx, cols::OFFSET, op.offset); - for i in 0..8 { - table.set_bool(row_idx, cols::limb_bit(i), ((op.limb >> i) & 1) != 0); - } - table.set_bool(row_idx, cols::LAST_LIMB, op.last_limb); - table.set_fe(row_idx, cols::MU, FE::one()); - } - - // Padding rows keep every field 0: all IS_BIT constraints hold (0 is a bit) and the - // implication constraints (a·b = 0) hold trivially. - trace -} - -// ========================================================================= -// Bus interactions -// ========================================================================= - -/// `limb = Σ 2^i · limb_bits[i]` as a single bus element (used as the byte value in MEMW). -fn limb_value() -> BusValue { - BusValue::linear( - (0..8) - .map(|i| LinearTerm::Column { - coefficient: 1i64 << i, - column: cols::limb_bit(i), - }) - .collect(), - ) -} - -pub fn bus_interactions() -> Vec { - let ts = || { - [ - BusValue::Packed { - start_column: cols::TIMESTAMP_0, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::TIMESTAMP_1, - packing: Packing::Direct, - }, - ] - }; - let ptr = || { - [ - BusValue::Packed { - start_column: cols::PTR_0, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::PTR_1, - packing: Packing::Direct, - }, - ] - }; - - let mut interactions = Vec::with_capacity(11); - - // 1. Receive ServeK[timestamp, ptr, offset] (mult = mu). - { - let [t0, t1] = ts(); - let [p0, p1] = ptr(); - interactions.push(BusInteraction::receiver( - BusId::ServeK, - Multiplicity::Column(cols::MU), - vec![ - t0, - t1, - p0, - p1, - BusValue::Packed { - start_column: cols::OFFSET, - packing: Packing::Direct, - }, - ], - )); - } - - // 2. MEMW: read byte k[offset] at ptr+offset, timestamp+1, width 1 (mult = mu). - // CO24 layout: [old[8], is_register, base[2], value[8], ts[2], w2, w4, w8]. - { - let base_lo = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::PTR_0, - }, - LinearTerm::Column { - coefficient: 1, - column: cols::OFFSET, - }, - ]); - let base_hi = BusValue::Packed { - start_column: cols::PTR_1, - packing: Packing::Direct, - }; - let ts_lo_plus_1 = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::TIMESTAMP_0, - }, - LinearTerm::Constant(1), - ]); - let ts_hi = BusValue::Packed { - start_column: cols::TIMESTAMP_1, - packing: Packing::Direct, - }; - let mut values = Vec::with_capacity(24); - // old[0..8]: read value = limb, rest 0 - values.push(limb_value()); - for _ in 1..8 { - values.push(BusValue::constant(0)); - } - values.push(BusValue::constant(0)); // is_register = 0 - values.push(base_lo); - values.push(base_hi); - // value[0..8]: same as old (read) - values.push(limb_value()); - for _ in 1..8 { - values.push(BusValue::constant(0)); - } - values.push(ts_lo_plus_1); - values.push(ts_hi); - values.push(BusValue::constant(0)); // w2 - values.push(BusValue::constant(0)); // w4 - values.push(BusValue::constant(0)); // w8 (width 1 byte) - interactions.push(BusInteraction::sender( - BusId::Memw, - Multiplicity::Column(cols::MU), - values, - )); - } - - // 3. Receive Bit[timestamp, 8*offset + i] for each set bit (mult = limb_bits[i]). - for i in 0..8 { - let [t0, t1] = ts(); - interactions.push(BusInteraction::receiver( - BusId::Bit, - Multiplicity::Column(cols::limb_bit(i)), - vec![ - t0, - t1, - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 8, - column: cols::OFFSET, - }, - LinearTerm::Constant(i as i64), - ]), - ], - )); - } - - // 4. Recurse: send ServeK[timestamp, ptr, offset-1] (mult = mu - last_limb). - { - let [t0, t1] = ts(); - let [p0, p1] = ptr(); - interactions.push(BusInteraction::sender( - BusId::ServeK, - Multiplicity::Diff(cols::MU, cols::LAST_LIMB), - vec![ - t0, - t1, - p0, - p1, - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::OFFSET, - }, - LinearTerm::Constant(-1), - ]), - ], - )); - } - - interactions -} - -// ========================================================================= -// Single-body constraint set (ConstraintSet front-end) -// ========================================================================= -// -// One body against the generic `ConstraintBuilder` serves the compiled prover -// folder, the verifier folder and IR capture. Constraint indices 0..20. - -use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; - -/// EC_SCALAR transition constraints as a single-source [`ConstraintSet`] (20 -/// total). No column configuration needed (the layout is fixed via `cols`). -pub struct EcScalarConstraints; - -impl ConstraintSet for EcScalarConstraints { - fn eval>(&self, b: &mut B) { - // idx 0..10: unconditional IS_BIT `x·(1−x)` for - // [mu, limb_bit(0..8), last_limb], in that column order. Iterator - // chain, not a Vec: eval runs once per LDE row. - let bit_cols = core::iter::once(cols::MU) - .chain((0..8).map(cols::limb_bit)) - .chain(core::iter::once(cols::LAST_LIMB)); - for (i, col) in bit_cols.enumerate() { - let x = b.main(0, col); - let one = b.one(); - b.emit_base(i, x.clone() * (one - x)); - } - - // idx 10..18: limb_bit(i) · (1 − mu) = 0. - for i in 0..8 { - let a = b.main(0, cols::limb_bit(i)); - let mu = b.main(0, cols::MU); - let one = b.one(); - b.emit_base(10 + i, a * (one - mu)); - } - - // idx 18: last_limb · (1 − mu) = 0. - let last_limb = b.main(0, cols::LAST_LIMB); - let mu = b.main(0, cols::MU); - let one = b.one(); - b.emit_base(18, last_limb * (one - mu)); - - // idx 19: last_limb · offset = 0. - let last_limb = b.main(0, cols::LAST_LIMB); - let offset = b.main(0, cols::OFFSET); - b.emit_base(19, last_limb * offset); - } -} diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index 2ffde164d..ff0c41f84 100644 --- a/prover/src/tables/ecdas.rs +++ b/prover/src/tables/ecdas.rs @@ -7,8 +7,9 @@ //! and `next_op`. When `next_op = 1` it consumes the scalar bit at `round` on the `Bit` //! bus (an add follows). ECSM seeds and drains the bus; interior rows telescope. //! -//! See `spec/src/ecdas.toml`. Constraints are **unconditional**; padding rows set the quotients -//! to `r` and `op = 0`, which makes every relation hold with zero carries. +//! See `spec/src/ecdas.toml`. Constraints are **unconditional**; padding rows set quotients +//! to 0 and `op = 1`. The `R·P` term in the λ, xR, and yR relations is gated with `μ`, so it +//! vanishes on padding rows (μ=0) and all relations hold with zero carries. use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; @@ -128,12 +129,10 @@ pub fn generate_ecdas_trace( table.set_fe(row_idx, cols::MU, FE::one()); } - // Padding rows: q0 = q1 = q2 = r, op = 0, everything else 0. This makes every - // (unconditional) convolution relation hold with zero carries. + // Padding rows: q0 = q1 = q2 = 0, op = 1 (add), everything else 0. The μ-gated R·P + // term vanishes (μ=0), so all convolution relations hold with zero carries. for row_idx in n..num_rows { - table.set_bytes(row_idx, cols::Q0, &R_BYTES); - table.set_bytes(row_idx, cols::Q1, &R_BYTES); - table.set_bytes(row_idx, cols::Q2, &R_BYTES); + table.set_byte(row_idx, cols::OP, 1); } trace @@ -156,7 +155,7 @@ pub fn bus_interactions() -> Vec { let ts_hi = || packed(cols::TIMESTAMP_1); let mut out = Vec::new(); - // Receive [ts, xA, yA, xG, yG, round, op]. + // Receive [id, ts, xA, yA, xG, yG, round, op]. out.push(BusInteraction::receiver( BusId::Ecdas, mu(), @@ -221,7 +220,7 @@ pub fn bus_interactions() -> Vec { vec![ts_lo(), ts_hi(), packed(cols::ROUND)], )); - // Send the updated accumulator: [ts, xR, yR, xG, yG, round - 1 + next_op, next_op]. + // Send the updated accumulator: [id, ts, xR, yR, xG, yG, round - 1 + next_op, next_op]. out.push(BusInteraction::sender( BusId::Ecdas, mu(), @@ -314,20 +313,24 @@ impl EcdasConstraints { } } - /// The r·P − q·P convolution term `Σ_{j=0..=i} (r_byte(j) − q[j])·p_byte(i−j)` - /// (shared structure across all three relations). + /// The `μ·R·P − q·P` convolution term + /// `μ·Σ_{j=0..=i} r_byte(j)·p_byte(i−j) − Σ_{j=0..=i} q[j]·p_byte(i−j)` + /// (shared structure across all three relations). R and P are constants, so + /// `μ·R·P` is degree 1. The `μ`-gate makes the term vanish on padding rows + /// (`μ=0`, `q=0`), keeping all relations at zero carries. fn rq>( b: &B, i: usize, qbase: usize, ) -> B::Expr { - let mut s = b.zero(); + let mu = b.main(0, cols::MU); + let mut r_p = b.zero(); + let mut q_p = b.zero(); for j in 0..=i { - let term = (Self::r_byte_expr(b, j) - Self::byte_at(b, qbase, 33, j)) - * Self::p_byte_expr(b, i - j); - s = s + term; + r_p = r_p + Self::r_byte_expr(b, j) * Self::p_byte_expr(b, i - j); + q_p = q_p + Self::byte_at(b, qbase, 33, j) * Self::p_byte_expr(b, i - j); } - s + mu * r_p - q_p } /// `S_i` for `relation` at limb `i`. diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 846c31812..5d0a9477f 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -3,18 +3,16 @@ //! 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, -//! triggers EC_SCALAR to serve `k` bit-by-bit, and delegates the double-and-add to ECDAS over -//! the `Ecdas`/`ServeK`/`Bit` buses. +//! 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. //! //! ## Padding -//! Padding rows have `mu = 0`, all columns zero **except `q1`, which pads to `p`**. This makes -//! both carry relations close on padding without gating the whole recurrence: the x² relation -//! has no standalone constant (closes at all-zero), and the yG relation closes because the -//! `p² − q1·p` offset cancels (`q1 = p`) and the curve constant `b` is multiplied by `µ` (so it -//! drops when `µ = 0`). Only that single `µ·b` term is µ-gated. The range checks / +//! Padding rows have `mu = 0`, all columns zero. The yG carry relation closes because both the +//! `µ·p²` and `µ·b` terms vanish when `µ = 0`, leaving the trivial `0 = 0` recurrence. The x² +//! relation has no standalone constant and also closes at all-zero. The range checks / //! virtual-carry checks remain µ-gated as before. use executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER; @@ -30,7 +28,7 @@ pub(crate) const CARRY_OFFSET_X2: i64 = 8160; pub(crate) const CARRY_OFFSET_YG: i64 = 16319; // ========================================================================= -// Column indices (~427 columns) +// Column indices (667 columns; keep in sync with NUM_COLUMNS below) // ========================================================================= pub mod cols { @@ -45,27 +43,29 @@ pub mod cols { pub const XR: usize = 8; // U256BL (32) pub const YR: usize = 40; // U256BL (32) - pub const K: usize = 72; // U256BL (32) - pub const LEN_K: usize = 104; // Byte - pub const XG: usize = 105; // U256BL (32) - pub const YG: usize = 137; // U256BL (32) - pub const X2: usize = 169; // U256BL (32) - pub const Q0: usize = 201; // U256BL (32) - pub const C0: usize = 233; // BaseField[64] - pub const Q1: usize = 297; // Byte[33] - pub const C1: usize = 330; // BaseField[64] - pub const K_SUB_N: usize = 394; // U256HL (16 halfwords) - pub const XR_SUB_P: usize = 410; // U256HL (16 halfwords) - pub const MU: usize = 426; - - pub const NUM_COLUMNS: usize = 427; + pub const K: usize = 72; // Bit[256] — scalar bits, k[0] is LSB + pub const LEN_K: usize = 328; // Byte + pub const XG: usize = 329; // U256BL (32) + pub const YG: usize = 361; // U256BL (32) + pub const X2: usize = 393; // U256BL (32) + pub const Q0: usize = 425; // U256BL (32) + pub const C0: usize = 457; // BaseField[64] + pub const Q1: usize = 521; // Byte[33] + pub const C1: usize = 554; // BaseField[64] + pub const XG_SUB_P: usize = 618; // U256HL (16 halfwords) + 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; + + pub const NUM_COLUMNS: usize = 667; #[inline] pub const fn xr(i: usize) -> usize { XR + i } + /// Bit `i` of the scalar `k` (0 = LSB, 255 = MSB). #[inline] - pub const fn k(i: usize) -> usize { + pub const fn k_bit(i: usize) -> usize { K + i } #[inline] @@ -97,6 +97,10 @@ pub mod cols { C1 + i } #[inline] + pub const fn xg_sub_p(i: usize) -> usize { + XG_SUB_P + i + } + #[inline] pub const fn k_sub_n(i: usize) -> usize { K_SUB_N + i } @@ -164,13 +168,17 @@ pub fn generate_ecsm_trace( table.set_bytes(row_idx, cols::XR, &w.x_r); table.set_bytes(row_idx, cols::YR, &w.y_r); - table.set_bytes(row_idx, cols::K, &w.k); + for b in 0..256 { + let bit = (w.k[b / 8] >> (b % 8)) & 1; + table.set_fe(row_idx, cols::k_bit(b), FE::from(bit as u64)); + } table.set_u64(row_idx, cols::LEN_K, w.len_k as u64); table.set_bytes(row_idx, cols::XG, &w.x_g); table.set_bytes(row_idx, cols::YG, &w.y_g); table.set_bytes(row_idx, cols::X2, &w.x2); table.set_bytes(row_idx, cols::Q0, &w.q0); table.set_bytes(row_idx, cols::Q1, &w.q1); + 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); @@ -184,13 +192,6 @@ pub fn generate_ecsm_trace( table.set_fe(row_idx, cols::MU, FE::one()); } - // Padding rows (`mu = 0`) must carry `q1 = p` so the yG carry relation closes: the - // `p² − q1·p` offset cancels and the µ-gated `b` term drops. Bytes 0..31 hold p; byte 32 - // stays 0 (a valid IS_BIT value). - for row_idx in n..num_rows { - table.set_bytes(row_idx, cols::Q1, &P_BYTES); - } - trace } @@ -274,6 +275,24 @@ pub fn point_coord_busvalues(col: usize) -> Vec { (0..32).map(|b| packed(col + b)).collect() } +/// `byte_k[byte_idx]` as a MEMW bus value: linear combination of 8 bit columns +/// `k_bit[8*byte_idx .. 8*byte_idx+7]` with coefficients 2^0..2^7. +fn k_byte_busvalue(byte_idx: usize) -> BusValue { + BusValue::linear( + (0..8) + .map(|j| LinearTerm::Column { + coefficient: 1i64 << j, + column: cols::k_bit(8 * byte_idx + j), + }) + .collect(), + ) +} + +/// One 8-byte MEMW dword chunk of k (bytes `8*dword_idx .. 8*dword_idx+7`). +fn k_dword_busvalues(dword_idx: usize) -> [BusValue; 8] { + std::array::from_fn(|b| k_byte_busvalue(8 * dword_idx + b)) +} + // ========================================================================= // Bus interactions // ========================================================================= @@ -336,7 +355,17 @@ pub fn bus_interactions() -> Vec { )); } - // read x12 -> addr_k (register read at ts). + let ts_lo_plus = |d: i64| { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::TIMESTAMP_0, + }, + LinearTerm::Constant(d), + ]) + }; + + // read x12 -> addr_k (register read at ts + 1). out.push(BusInteraction::sender( BusId::Memw, mu(), @@ -345,13 +374,13 @@ pub fn bus_interactions() -> Vec { 1, BusValue::constant(2 * 12), BusValue::constant(0), - ts_lo(), + ts_lo_plus(1), ts_hi(), 1, 0, ), )); - // read k: 4 doublewords at addr_k + 8i (ts). + // read k: 4 doublewords at addr_k + 8i (ts + 1). for i in 0..4 { let base_lo = BusValue::linear(vec![ LinearTerm::Column { @@ -364,11 +393,11 @@ pub fn bus_interactions() -> Vec { BusId::Memw, mu(), memw_read( - dword_bytes(cols::K, i), + k_dword_busvalues(i), 0, base_lo, packed(cols::ADDR_K_1), - ts_lo(), + ts_lo_plus(1), ts_hi(), 0, 1, @@ -376,16 +405,7 @@ pub fn bus_interactions() -> Vec { )); } - // read x10 -> addr_xR (register read at ts + 1). - let ts_lo_plus = |d: i64| { - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::TIMESTAMP_0, - }, - LinearTerm::Constant(d), - ]) - }; + // read x10 -> addr_xR (register read at ts + 2, grouped with xR writes). out.push(BusInteraction::sender( BusId::Memw, mu(), @@ -394,7 +414,7 @@ pub fn bus_interactions() -> Vec { 1, BusValue::constant(2 * 10), BusValue::constant(0), - ts_lo_plus(1), + ts_lo_plus(2), ts_hi(), 1, 0, @@ -436,7 +456,7 @@ pub fn bus_interactions() -> Vec { is_byte(cols::X2, 32, &mut out); is_byte(cols::Q0, 32, &mut out); is_byte(cols::YG, 32, &mut out); - is_byte(cols::Q1, 32, &mut out); // q1[0..31]; q1[32] is an IS_BIT constraint + 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. @@ -463,6 +483,13 @@ pub fn bus_interactions() -> Vec { vec![half_offset(cols::c1(i), CARRY_OFFSET_YG)], )); } + for i in 0..16 { + out.push(BusInteraction::sender( + BusId::IsHalfword, + mu(), + vec![packed(cols::xg_sub_p(i))], + )); + } for i in 0..16 { out.push(BusInteraction::sender( BusId::IsHalfword, @@ -478,16 +505,17 @@ pub fn bus_interactions() -> Vec { )); } - // ZERO bus: assert k != 0 (sum of k's 32 bytes is nonzero). + // 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]. out.push(BusInteraction::sender( BusId::Zero, mu(), vec![ BusValue::linear( - (0..32) - .map(|i| LinearTerm::Column { - coefficient: 1, - column: cols::k(i), + (0..256) + .map(|b| LinearTerm::Column { + coefficient: 1i64 << (b % 8), + column: cols::k_bit(b), }) .collect(), ), @@ -496,19 +524,15 @@ pub fn bus_interactions() -> Vec { )); // Delegation buses. - // SERVE_K send: [ts, addr_k, 31]. - out.push(BusInteraction::sender( - BusId::ServeK, - mu(), - vec![ - ts_lo(), - ts_hi(), - packed(cols::ADDR_K_0), - packed(cols::ADDR_K_1), - BusValue::constant(31), - ], - )); - // BIT sender: the MSB at position len_k. + // BIT receivers: receive Bit[ts, i] from ECDAS for each scalar bit i=0..255. + for i in 0..256 { + out.push(BusInteraction::receiver( + BusId::Bit, + Multiplicity::Column(cols::k_bit(i)), + vec![ts_lo(), ts_hi(), BusValue::constant(i as u64)], + )); + } + // BIT sender: the MSB at position len_k (always 1). out.push(BusInteraction::sender( BusId::Bit, mu(), @@ -554,8 +578,9 @@ pub fn bus_interactions() -> Vec { out } -/// Builds the ECDAS bus tuple `[ts_lo, ts_hi, accX(32), accY(32), genX(32), genY(32), -/// round, op]`. Shared so the ECSM sender and the ECDAS receiver/sender pack it identically. +/// Builds the ECDAS bus tuple `[id, ts_lo, ts_hi, accX(32), accY(32), genX(32), genY(32), +/// round, op]`. `id` is the curve identifier (0 = secp256k1). Shared so the ECSM sender and +/// the ECDAS receiver/sender pack it identically. #[allow(clippy::too_many_arguments)] pub fn ecdas_tuple( acc_x: usize, @@ -567,7 +592,8 @@ pub fn ecdas_tuple( ts_lo: BusValue, ts_hi: BusValue, ) -> Vec { - let mut v = Vec::with_capacity(2 + 4 * 32 + 2); + let mut v = Vec::with_capacity(1 + 2 + 4 * 32 + 2); + v.push(BusValue::constant(0)); // id = 0 (secp256k1) v.push(ts_lo); v.push(ts_hi); v.extend(point_coord_busvalues(acc_x)); @@ -579,26 +605,36 @@ pub fn ecdas_tuple( v } +// ========================================================================= +// Constraints +// ========================================================================= + /// Which convolution relation a carry constraint enforces. #[derive(Clone, Copy)] pub enum Relation { /// `xG² − x2 − q0·p = 0` X2, - /// `yG² + p² − xG·x2 − b − q1·p = 0` + /// `yG² + µ·p² − xG·x2 − µ·b − q1·p = 0` Yg, } -/// A range-check overflow addition: `p + xR_sub_p = xR + 2^256` (`k u64 { let bytes = match self { + OverflowKind::XgLtP => &P_BYTES, OverflowKind::KLtN => &N_BYTES, OverflowKind::XrLtP => &P_BYTES, }; @@ -608,20 +644,26 @@ impl OverflowKind { } w } - /// Column base of the witnessed halfword addend (`k_sub_N` / `xR_sub_p`). + /// Column base of the witnessed halfword addend (`xg_sub_p` / `k_sub_N` / `xR_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, } } - /// Column base of the byte sum (`k` / `xR`). - fn sum_bl_base(self) -> usize { + /// Column base of the sum. + fn sum_col_base(self) -> usize { match self { + OverflowKind::XgLtP => cols::XG, OverflowKind::KLtN => cols::K, OverflowKind::XrLtP => cols::XR, } } + /// Whether the sum is stored as individual bits (k) rather than bytes (xG/xR). + fn sum_is_bits(self) -> bool { + matches!(self, OverflowKind::KLtN) + } } // ========================================================================= @@ -629,26 +671,30 @@ impl OverflowKind { // ========================================================================= // // One body against the generic `ConstraintBuilder` serves the compiled prover -// folder, the verifier folder and IR capture. Constraint indices 0..148: +// folder, the verifier folder and IR capture. Constraint indices 0..413: // 0 : IS_BIT(MU) -// 1..65 : ConvCarry(X2, 0..64) -// 65 : ColIsZero(c0(63)) -// 66..130 : ConvCarry(Yg, 0..64) -// 130 : ColIsZero(c1(63)) -// 131 : IS_BIT(q1(32)) -// 132..139 : CarryBit(KLtN, 0..7) -// 139 : OverflowRequired(KLtN) -// 140..147 : CarryBit(XrLtP, 0..7) -// 147 : OverflowRequired(XrLtP) +// 1..257 : IS_BIT(k[i]) for the 256 scalar bits +// 257 : KBitsZeroOnPadding — (Σ k_bit[i])·(1−µ) +// 258..322 : ConvCarry(X2, 0..64) +// 322 : ColIsZero(c0(63)) +// 323..387 : ConvCarry(Yg, 0..64) +// 387 : ColIsZero(c1(63)) +// 388 : IS_BIT(q1(32)) +// 389..396 : CarryBit(XgLtP, 0..7) +// 396 : OverflowRequired(XgLtP) +// 397..404 : CarryBit(KLtN, 0..7) +// 404 : OverflowRequired(KLtN) +// 405..412 : CarryBit(XrLtP, 0..7) +// 412 : OverflowRequired(XrLtP) use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; -/// ECSM transition constraints as a single-source [`ConstraintSet`] (148 +/// ECSM transition constraints as a single-source [`ConstraintSet`] (413 /// total). No column configuration needed (the layout is fixed via `cols`). pub struct EcsmConstraints; impl EcsmConstraints { - /// Byte `m` of the base-point order `P` (zero beyond 32 bytes). + /// Byte `m` of the field prime `P` (zero beyond 32 bytes). fn p_byte_expr>( b: &B, m: usize, @@ -692,16 +738,21 @@ impl EcsmConstraints { s = s - byte(cols::X2, 32, i); } Relation::Yg => { - // Σ (yG_j·yG_{i-j} + P_j·P_{i-j} − x2_j·xG_{i-j} − q1_j·P_{i-j}) − b_i + // Σ (yG_j·yG_{i-j} + µ·P_j·P_{i-j} − x2_j·xG_{i-j} − q1_j·P_{i-j}) − µ·b_i + // Both the p² offset and the curve constant b are µ-gated: they vanish on + // padding rows (µ=0), so all columns (including q1) can pad to zero. + // Factor µ out of the p² sum (µ·ΣP_j·P_{i-j}) as ECDAS `rq()` does, so µ + // is applied once per limb instead of once per term. + let mu = b.main(0, cols::MU); + let mut p2 = b.zero(); for j in 0..=i { s = s + byte(cols::YG, 32, j) * byte(cols::YG, 32, i - j); - s = s + Self::p_byte_expr(b, j) * Self::p_byte_expr(b, i - j); + p2 = p2 + Self::p_byte_expr(b, j) * Self::p_byte_expr(b, i - j); s = s - byte(cols::X2, 32, j) * byte(cols::XG, 32, i - j); s = s - byte(cols::Q1, 33, j) * Self::p_byte_expr(b, i - j); } + s = s + mu.clone() * p2; if i == 0 { - // Only the curve constant `b` is µ-gated (µ·B); B_i = 0 for i ≥ 1. - let mu = b.main(0, cols::MU); let curve_b = b.const_base(B); s = s - mu * curve_b; } @@ -730,24 +781,34 @@ impl EcsmConstraints { two_pow_8 * c_i - c_prev - Self::s_i(b, relation, i) } - /// The 8 word-carries of the `kind` addition. + /// The 8 word-carries of the `kind` addition. `k` is summed from its 256 individual + /// bit columns; `xG`/`xR` from their 32 byte columns. fn carry_chain>( b: &B, kind: OverflowKind, ) -> [B::Expr; 8] { let hl = kind.addend_hl_base(); - let bl = kind.sum_bl_base(); + let base = kind.sum_col_base(); let mut c: [B::Expr; 8] = std::array::from_fn(|_| b.zero()); let mut prev = b.zero(); for (i, slot) in c.iter_mut().enumerate() { // addend1 word i (from halfwords): hl[2i] + 2^16·hl[2i+1] let shift_16 = b.const_base(1u64 << 16); let addend1 = b.main(0, hl + 2 * i) + b.main(0, hl + 2 * i + 1) * shift_16; - // sum word i (from bytes): Σ bl[4i+b]·2^{8b} + // sum word i: from individual bits (k) or bytes (xG/xR). let mut sum = b.zero(); - for byte in 0..4 { - let shift = b.const_base(1u64 << (8 * byte)); - sum = sum + b.main(0, bl + 4 * i + byte) * shift; + if kind.sum_is_bits() { + // k is stored as 256 individual bits; word i = bits 32i..32i+31. + for bit in 0..32 { + let shift = b.const_base(1u64 << bit); + sum = sum + b.main(0, base + 32 * i + bit) * shift; + } + } else { + // xG/xR stored as 32 bytes; word i = bytes 4i..4i+3. + for byte in 0..4 { + let shift = b.const_base(1u64 << (8 * byte)); + sum = sum + b.main(0, base + 4 * i + byte) * shift; + } } let addend0 = b.const_base(kind.const_word(i)); let inv = b.const_base(INV_SHIFT_32); @@ -760,7 +821,7 @@ impl EcsmConstraints { } impl ConstraintSet for EcsmConstraints { - // The k usize { 3 } @@ -773,6 +834,25 @@ impl ConstraintSet for EcsmConstraints { let mut idx = 1; + // idx 1..257: IS_BIT(k[i]) for the 256 scalar bits: k·(1−k). (deg 2) + for i in 0..256 { + let k = b.main(0, cols::k_bit(i)); + let one = b.one(); + b.emit_base(idx, k.clone() * (one - k)); + idx += 1; + } + + // idx 257: KBitsZeroOnPadding: (Σ k_bit[i])·(1−µ). All scalar bits must be zero on + // padding rows (µ=0), else a prover could fire phantom `Bit` bus receives. (deg 2) + let mut k_sum = b.zero(); + for i in 0..256 { + k_sum = k_sum + b.main(0, cols::k_bit(i)); + } + let mu = b.main(0, cols::MU); + let one = b.one(); + b.emit_base(idx, k_sum * (one - mu)); + idx += 1; + // X2 convolution: 64 carries (deg 2) + closing c0(63) (deg 1). for i in 0..64 { let root = Self::conv_carry(b, Relation::X2, i); @@ -793,14 +873,14 @@ impl ConstraintSet for EcsmConstraints { b.emit_base(idx, c1_last); idx += 1; - // idx 131: IS_BIT(q1[32]): x·(1−x). (deg 2) + // idx 388: IS_BIT(q1[32]): x·(1−x). (deg 2) let q1_32 = b.main(0, cols::q1(32)); let one = b.one(); b.emit_base(idx, q1_32.clone() * (one - q1_32)); idx += 1; - // k < N and xR < p: 7 carry bits (deg 3) + overflow-required (deg 2) each. - for kind in [OverflowKind::KLtN, OverflowKind::XrLtP] { + // 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] { let c = Self::carry_chain(b, kind); for ci in c.iter().take(7) { // µ · c_i · (1 − c_i) @@ -816,6 +896,6 @@ impl ConstraintSet for EcsmConstraints { idx += 1; } - debug_assert_eq!(idx, 148); + debug_assert_eq!(idx, 413); } } diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 78d5f9a6a..0a86e4149 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -29,7 +29,6 @@ pub mod cpu; pub mod cpu32; pub mod decode; pub mod dvrm; -pub mod ec_scalar; pub mod ecdas; pub mod ecsm; pub mod eq; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 36fd107c3..5c6b3085e 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -47,7 +47,6 @@ use super::cpu::{self, CpuOperation}; use super::cpu32; use super::decode; use super::dvrm::{self, DvrmOperation}; -use super::ec_scalar; use super::ecdas; use super::ecsm; use super::eq; @@ -533,7 +532,7 @@ fn build_reg_fallback( /// MEMW and LOAD collection requires sequential processing with state tracking. /// /// Returns: (memw_buckets, load_ops, lt_ops, shift_ops, bitwise_ops, commit_ops, -/// keccak_ops, cpu32_ops, ecsm_ops, ec_scalar_ops, ecdas_ops) +/// keccak_ops, cpu32_ops, ecsm_ops, ecdas_ops) #[allow(clippy::type_complexity)] fn collect_ops_from_cpu( cpu_ops: &[CpuOperation], @@ -549,7 +548,6 @@ fn collect_ops_from_cpu( Vec, Vec, Vec, - Vec, Vec, ) { let mut memw = MemwBuckets::with_register_capacity(cpu_ops.len() * 3); @@ -561,7 +559,6 @@ fn collect_ops_from_cpu( let mut keccak_ops = Vec::new(); let mut cpu32_ops = Vec::new(); let mut ecsm_ops = Vec::new(); - let mut ec_scalar_ops = Vec::new(); let mut ecdas_ops = Vec::new(); // Seed from the carried x254 (0 for a monolithic run or the first epoch) so a // continuation epoch indexes its commits globally, matching the x254 the @@ -648,13 +645,12 @@ fn collect_ops_from_cpu( }); } - // Collect ECSM ecall operations (memory I/O + the three table row sets) + // Collect ECSM ecall operations (memory I/O + the two table row sets) if op.ecall_ecsm { - let (ecsm_memw, ecsm_op, ec_scalar_rows, ecdas_rows) = + let (ecsm_memw, ecsm_op, ecdas_rows) = collect_ecsm_ops(op, memory_state, register_state); memw.extend_ops(ecsm_memw); ecsm_ops.push(ecsm_op); - ec_scalar_ops.extend(ec_scalar_rows); ecdas_ops.extend(ecdas_rows); } @@ -712,7 +708,6 @@ fn collect_ops_from_cpu( keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, ) } @@ -823,11 +818,11 @@ fn collect_store_op_from_cpu(op: &CpuOperation, memory_state: &mut MemoryState) memw_op } -/// Collects all MEMW ops and the ECSM / EC_SCALAR / ECDAS table ops for one ECSM ecall. +/// Collects all MEMW ops and the ECSM / ECDAS table ops for one ECSM ecall. /// -/// Timestamp scheme (within the instruction's 4-wide budget): the `x11`/`x12` register reads -/// and the `xG`/`k` memory reads happen at `T`; the `x10` register read and the EC_SCALAR -/// byte reads at `T + 1`; the `xR` memory writes at `T + 2`. Every read advances +/// 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 /// `memory_state` / `register_state` (the offline read-old + write-new model), so later /// accesses always observe a strictly smaller old timestamp. #[allow(clippy::needless_range_loop)] @@ -838,7 +833,6 @@ fn collect_ecsm_ops( ) -> ( Vec, ecsm::EcsmOperation, - Vec, Vec, ) { let t = op.timestamp; @@ -857,58 +851,68 @@ 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(47); + let mut memw_ops = Vec::with_capacity(15); - // x11 -> addr_xG, x12 -> addr_k (register reads at T). - for reg in [11u8, 12u8] { - let (val, old_ts) = register_state.read(reg); + // x11 -> addr_xG (register read at T), x12 -> addr_k (register read at T+1). + { + let (val, old_ts) = register_state.read(11); let value = pack_register_value(val); memw_ops.push( - MemwOperation::new(true, 2 * reg as u64, value, t, 2, true) + MemwOperation::new(true, 2 * 11, value, t, 2, true) .with_old(value, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]), ); - register_state.write(reg, val, t); + register_state.write(11, val, t); } - // xG and k: 4 doubleword reads each at T. - for (base, bytes) in [(addr_xg, &witness.x_g), (addr_k, &witness.k)] { - for i in 0..4 { - let addr = base.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, old_ts) = memory_state.read_bytes(addr, 8); - memw_ops - .push(MemwOperation::new(false, addr, value, t, 8, true).with_old(value, old_ts)); - memory_state.write_bytes(addr, dword, 8, t); + // xG: 4 doubleword reads at T. + for i in 0..4 { + let addr = addr_xg.wrapping_add((8 * i) as u64); + let mut value = [0u32; 8]; + let mut dword = 0u64; + for j in 0..8 { + value[j] = witness.x_g[8 * i + j] as u32; + dword |= (witness.x_g[8 * i + j] as u64) << (8 * j); } + let (_old, old_ts) = memory_state.read_bytes(addr, 8); + memw_ops.push(MemwOperation::new(false, addr, value, t, 8, true).with_old(value, old_ts)); + memory_state.write_bytes(addr, dword, 8, t); } - // x10 -> addr_xR (register read at T + 1). + // x12 -> addr_k (register read at T+1). { - let (val, old_ts) = register_state.read(10); + let (val, old_ts) = register_state.read(12); let value = pack_register_value(val); memw_ops.push( - MemwOperation::new(true, 2 * 10, value, t + 1, 2, true) + MemwOperation::new(true, 2 * 12, value, t + 1, 2, true) .with_old(value, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]), ); - register_state.write(10, val, t + 1); + register_state.write(12, val, t + 1); + } + + // k: 4 doubleword reads at T+1. + for i in 0..4 { + let addr = addr_k.wrapping_add((8 * i) as u64); + let mut value = [0u32; 8]; + let mut dword = 0u64; + for j in 0..8 { + value[j] = witness.k[8 * i + j] as u32; + dword |= (witness.k[8 * i + j] as u64) << (8 * j); + } + let (_old, old_ts) = memory_state.read_bytes(addr, 8); + memw_ops + .push(MemwOperation::new(false, addr, value, t + 1, 8, true).with_old(value, old_ts)); + memory_state.write_bytes(addr, dword, 8, t + 1); } - // EC_SCALAR byte reads of k at T + 1 (one per scalar byte). - for offset in 0..32u64 { - let addr = addr_k.wrapping_add(offset); - let byte = k[offset as usize]; - let value = [byte as u32, 0, 0, 0, 0, 0, 0, 0]; - let (_v, old_ts) = memory_state.read_byte(addr); + // x10 -> addr_xR (register read at T + 2, grouped with xR writes per spec ecsm.toml:658). + { + let (val, old_ts) = register_state.read(10); + let value = pack_register_value(val); memw_ops.push( - MemwOperation::new(false, addr, value, t + 1, 1, true) - .with_old(value, [old_ts, 0, 0, 0, 0, 0, 0, 0]), + MemwOperation::new(true, 2 * 10, value, t + 2, 2, true) + .with_old(value, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]), ); - memory_state.write_byte(addr, byte, t + 1); + register_state.write(10, val, t + 2); } // xR writes at T + 2 (4 doublewords). @@ -927,7 +931,6 @@ fn collect_ecsm_ops( memory_state.write_bytes(addr, dword, 8, t + 2); } - let ec_scalar_ops = ec_scalar::rows_for_scalar(t, addr_k, &witness.k); let ecdas_ops = witness .steps .iter() @@ -942,7 +945,7 @@ fn collect_ecsm_ops( witness, }; - (memw_ops, ecsm_op, ec_scalar_ops, ecdas_ops) + (memw_ops, ecsm_op, ecdas_ops) } /// Collects register read/write operations (M1, M3, M5) from CpuOperation, @@ -2277,20 +2280,27 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec, - /// EC_SCALAR table (32 rows per ecall) - pub ec_scalar: TraceTable, - /// ECDAS double/add table (variable rows per ecall) pub ecdas: TraceTable, @@ -2757,7 +2764,6 @@ struct CollectedOps { cpu32_ops: Vec, // EC scalar-multiplication accelerator chips. ecsm_ops: Vec, - ec_scalar_ops: Vec, ecdas_ops: Vec, } @@ -2812,7 +2818,6 @@ fn collect_all_ops( keccak_ops: Vec, cpu32_ops: Vec, ecsm_ops: Vec, - ec_scalar_ops: Vec, ecdas_ops: Vec, register_state: &mut RegisterState, is_final: bool, @@ -2955,7 +2960,6 @@ fn collect_all_ops( store_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, } } @@ -2999,7 +3003,6 @@ fn build_traces( store_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, } = ops; @@ -3361,7 +3364,6 @@ fn build_traces( let gen_halt = || halt::generate_halt_trace(halt_timestamp, halt_next_pc); // ECSM accelerator traces (empty/all-padding for programs that do not use ECSM). let gen_ecsm = || ecsm::generate_ecsm_trace(&ecsm_ops); - let gen_ec_scalar = || ec_scalar::generate_ec_scalar_trace(&ec_scalar_ops); let gen_ecdas = || ecdas::generate_ecdas_trace(&ecdas_ops); let (mut cpus_slot, mut memws_slot, mut memw_aligneds_slot, mut memw_registers_slot) = @@ -3374,7 +3376,7 @@ fn build_traces( let (mut pages_slot, mut register_slot, mut halt_slot) = (None, None, None); let (mut eqs_slot, mut bytewises_slot, mut stores_slot, mut cpu32s_slot) = (None, None, None, None); - let (mut ecsm_slot, mut ec_scalar_slot, mut ecdas_slot) = (None, None, None); + let (mut ecsm_slot, mut ecdas_slot) = (None, None); #[cfg(feature = "disk-spill")] let sequential = storage_mode == StorageMode::Disk || cfg!(not(feature = "parallel")); @@ -3415,7 +3417,6 @@ fn build_traces( spawn_into!(stores_slot, gen_stores); spawn_into!(cpu32s_slot, gen_cpu32s); spawn_into!(ecsm_slot, gen_ecsm); - spawn_into!(ec_scalar_slot, gen_ec_scalar); spawn_into!(ecdas_slot, gen_ecdas); }); } else { @@ -3443,7 +3444,6 @@ fn build_traces( stores_slot = Some(gen_stores()); cpu32s_slot = Some(gen_cpu32s()); ecsm_slot = Some(gen_ecsm()); - ec_scalar_slot = Some(gen_ec_scalar()); ecdas_slot = Some(gen_ecdas()); } @@ -3478,7 +3478,6 @@ fn build_traces( #[allow(unused_mut)] let mut halt_trace = halt_slot.expect(PHASE5_RAN); let ecsm_trace = ecsm_slot.expect(PHASE5_RAN); - let ec_scalar_trace = ec_scalar_slot.expect(PHASE5_RAN); let ecdas_trace = ecdas_slot.expect(PHASE5_RAN); // Fixed-size and per-page tables aren't built through `chunk_and_generate`, @@ -3546,7 +3545,6 @@ fn build_traces( keccak_rnd: keccak_rnd_trace, keccak_rc: keccak_rc_trace, ecsm: ecsm_trace, - ec_scalar: ec_scalar_trace, ecdas: ecdas_trace, memw_registers, local_to_global, @@ -3806,7 +3804,6 @@ impl Traces { use super::decode::NUM_PRECOMPUTED_COLS as DECODE_PRECOMPUTED; use super::decode::cols::NUM_COLUMNS as DECODE_COLS; use super::dvrm::cols::NUM_COLUMNS as DVRM_COLS; - use super::ec_scalar::cols::NUM_COLUMNS as EC_SCALAR_COLS; use super::ecdas::cols::NUM_COLUMNS as ECDAS_COLS; use super::ecsm::cols::NUM_COLUMNS as ECSM_COLS; use super::eq::cols::NUM_COLUMNS as EQ_COLS; @@ -3848,7 +3845,6 @@ impl Traces { keccak_rnd, keccak_rc, ecsm, - ec_scalar, ecdas, memw_registers, eqs, @@ -3916,7 +3912,6 @@ impl Traces { total += (t.num_rows() * CPU32_COLS) as u64; } total += (ecsm.num_rows() * ECSM_COLS) as u64; - total += (ec_scalar.num_rows() * EC_SCALAR_COLS) as u64; total += (ecdas.num_rows() * ECDAS_COLS) as u64; total } @@ -3958,7 +3953,6 @@ impl Traces { let n_store = aux_cols(super::store::bus_interactions().len()); let n_cpu32 = aux_cols(super::cpu32::bus_interactions().len()); let n_ecsm = aux_cols(super::ecsm::bus_interactions().len()); - let n_ec_scalar = aux_cols(super::ec_scalar::bus_interactions().len()); let n_ecdas = aux_cols(super::ecdas::bus_interactions().len()); let Traces { @@ -3981,7 +3975,6 @@ impl Traces { keccak_rnd, keccak_rc, ecsm, - ec_scalar, ecdas, memw_registers, eqs, @@ -4049,7 +4042,6 @@ impl Traces { total += (t.num_rows() * n_cpu32) as u64; } total += (ecsm.num_rows() * n_ecsm) as u64; - total += (ec_scalar.num_rows() * n_ec_scalar) as u64; total += (ecdas.num_rows() * n_ecdas) as u64; total } @@ -4272,7 +4264,6 @@ impl Traces { keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); #[cfg(feature = "instruments")] @@ -4291,7 +4282,6 @@ impl Traces { keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, &mut register_state, is_final, @@ -4351,7 +4341,6 @@ impl Traces { keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); @@ -4366,7 +4355,6 @@ impl Traces { keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, &mut register_state, true, diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index 85eaca17a..fab4aabff 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -343,15 +343,14 @@ pub enum BusId { Cpu32 = 27, // ========================================================================= - // EC scalar multiplication accelerator (ECSM / ECDAS / EC_SCALAR) + // EC scalar multiplication accelerator (ECSM / ECDAS) // ========================================================================= /// ECDAS self-referential double/add sequence bus: /// (timestamp, xA, yA, xG, yG, round, op). ECSM seeds and drains it. Ecdas = 28, - /// EC_SCALAR self-referential scalar-byte server bus: (timestamp, ptr, offset). - ServeK = 29, - /// Scalar-bit bus: EC_SCALAR sends one per set bit (timestamp, bit_index); - /// ECDAS receives one per add, ECSM receives the MSB. + /// Scalar-bit bus: ECDAS sends Bit[ts, round] per step (mult = next_op); + /// ECSM receives Bit[ts, i] for each of the 256 k bits (mult = k[i]), + /// and sends Bit[ts, idx_k] for the MSB (mult = μ). Bit = 30, // ========================================================================= @@ -387,7 +386,6 @@ impl BusId { BusId::MemoryOp => "MemoryOp", BusId::Cpu32 => "Cpu32", BusId::Ecdas => "Ecdas", - BusId::ServeK => "ServeK", BusId::Bit => "Bit", BusId::GlobalMemory => "GlobalMemory", } @@ -420,7 +418,6 @@ impl TryFrom for BusId { 26 => Ok(BusId::MemoryOp), 27 => Ok(BusId::Cpu32), 28 => Ok(BusId::Ecdas), - 29 => Ok(BusId::ServeK), 30 => Ok(BusId::Bit), 31 => Ok(BusId::GlobalMemory), other => Err(other), diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 8ed5fdca2..6dd28ce71 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -57,9 +57,6 @@ use crate::tables::decode::{bus_interactions as decode_bus_interactions, cols as use crate::tables::dvrm::{ DvrmConstraints, bus_interactions as dvrm_bus_interactions, cols as dvrm_cols, }; -use crate::tables::ec_scalar::{ - EcScalarConstraints, bus_interactions as ec_scalar_bus_interactions, cols as ec_scalar_cols, -}; use crate::tables::ecdas::{ EcdasConstraints, bus_interactions as ecdas_bus_interactions, cols as ecdas_cols, }; @@ -939,18 +936,6 @@ pub fn create_ecsm_air(proof_options: &ProofOptions) -> ConcreteVmAir ConcreteVmAir { - build_air( - ec_scalar_cols::NUM_COLUMNS, - ec_scalar_bus_interactions(), - proof_options, - 1, - EcScalarConstraints, - "EC_SCALAR", - ) -} - /// Create ECDAS AIR (per-step double/add of the scalar-multiplication sequence). pub fn create_ecdas_air(proof_options: &ProofOptions) -> ConcreteVmAir { build_air( diff --git a/prover/src/tests/constraint_program_tests.rs b/prover/src/tests/constraint_program_tests.rs index 5de95a446..3ae46494d 100644 --- a/prover/src/tests/constraint_program_tests.rs +++ b/prover/src/tests/constraint_program_tests.rs @@ -178,6 +178,5 @@ fn all_table_programs_match_folders() { check_air(&create_keccak_rnd_air(&opts), "KECCAK_RND"); check_air(&create_keccak_rc_air(&opts), "KECCAK_RC"); check_air(&create_ecsm_air(&opts), "ECSM"); - check_air(&create_ec_scalar_air(&opts), "EC_SCALAR"); check_air(&create_ecdas_air(&opts), "ECDAS"); } diff --git a/prover/src/tests/constraint_set_tests_a.rs b/prover/src/tests/constraint_set_tests_a.rs index 89a75864a..571ae2da3 100644 --- a/prover/src/tests/constraint_set_tests_a.rs +++ b/prover/src/tests/constraint_set_tests_a.rs @@ -1,6 +1,6 @@ //! Folder-vs-capture-interpret regression tests for the single-source //! `ConstraintSet` table bodies (group A: dvrm, shift, mul, lt, load, ecsm, -//! ecdas, ec_scalar). +//! ecdas). //! //! Each table's single `eval` body is run three ways — the `ProverEvalFolder` //! (base), the `VerifierEvalFolder` (extension), and the `CaptureBuilder` → flat @@ -243,17 +243,3 @@ mod ecdas { check_set("ecdas", &EcdasConstraints, cols::NUM_COLUMNS); } } - -// ============================================================================= -// ec_scalar.rs -// ============================================================================= - -mod ec_scalar { - use super::*; - use crate::tables::ec_scalar::{EcScalarConstraints, cols}; - - #[test] - fn ec_scalar_constraint_set_folder_capture_agree() { - check_set("ec_scalar", &EcScalarConstraints, cols::NUM_COLUMNS); - } -} diff --git a/prover/src/tests/ec_scalar_tests.rs b/prover/src/tests/ec_scalar_tests.rs deleted file mode 100644 index f8a19cf79..000000000 --- a/prover/src/tests/ec_scalar_tests.rs +++ /dev/null @@ -1,71 +0,0 @@ -//! Tests for the EC_SCALAR table — constraint satisfaction on generated traces, -//! the `last_limb` schedule, and the single-source constraint count. - -use crate::tables::ec_scalar::{ - EcScalarConstraints, cols, generate_ec_scalar_trace, rows_for_scalar, -}; -use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; -use math::field::element::FieldElement; -use stark::constraints::builder::{ConstraintSet, ProverEvalFolder}; -use stark::frame::Frame; -use stark::table::TableView; -use stark::trace::TraceTable; -use stark::traits::TransitionEvaluationContext; - -/// Evaluate the EC_SCALAR [`ConstraintSet`] on one trace row (the compiled -/// prover folder path), returning every base-field constraint value. -fn eval_row(trace: &TraceTable, row: usize) -> Vec { - let main: Vec = (0..cols::NUM_COLUMNS) - .map(|c| *trace.main_table.get(row, c)) - .collect(); - let n = EcScalarConstraints.meta().len(); - let frame = Frame::::new(vec![TableView::new( - vec![main], - vec![vec![]], - )]); - let no_e: Vec> = vec![]; - let offset_e = FieldElement::::zero(); - let ctx = - TransitionEvaluationContext::new_prover(frame.as_row_frame(), &no_e, &no_e, &offset_e); - let mut base = vec![FE::zero(); n]; - let mut ext = vec![FieldElement::::zero(); n]; - let mut folder = ProverEvalFolder::new(&ctx, &mut base, &mut ext); - EcScalarConstraints.eval(&mut folder); - base -} - -#[test] -fn constraints_hold_on_generated_trace() { - let mut k = [0u8; 32]; - // a scalar with assorted bit patterns across several bytes - k[0] = 0b1010_0101; - k[1] = 0xFF; - k[15] = 0x80; - k[31] = 0x01; - let ops = rows_for_scalar(444, 0x3000, &k); - let trace = generate_ec_scalar_trace(&ops); - - for row in 0..trace.num_rows() { - for (i, v) in eval_row(&trace, row).iter().enumerate() { - assert_eq!(*v, FE::zero(), "constraint {i} must hold at row {row}"); - } - } -} - -#[test] -fn last_limb_set_only_at_offset_zero() { - let k = [7u8; 32]; - let ops = rows_for_scalar(4, 0x100, &k); - assert_eq!(ops.len(), 32); - for op in &ops { - assert_eq!(op.last_limb, op.offset == 0); - } - // 32 distinct offsets 31..0 - assert_eq!(ops[0].offset, 31); - assert_eq!(ops[31].offset, 0); -} - -#[test] -fn constraint_set_count() { - assert_eq!(EcScalarConstraints.meta().len(), 20); -} diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index 9b98f8934..91956c5ad 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -1,9 +1,10 @@ -//! Tests for the ECSM core table — constraint satisfaction on generated traces -//! and the single-source constraint count. +//! Tests for the ECSM core table — constraint satisfaction on generated traces, +//! 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 ecsm::compute_witness; +use ecsm::{N_BYTES, P_BYTES, compute_witness}; use math::field::element::FieldElement; use stark::constraints::builder::{ConstraintSet, ProverEvalFolder}; use stark::frame::Frame; @@ -11,6 +12,14 @@ use stark::table::TableView; use stark::trace::TraceTable; use stark::traits::TransitionEvaluationContext; +// Constraint indices in the single `EcsmConstraints::eval` body (see the index map there). +const IDX_KBITS_ZERO: usize = 257; // KBitsZeroOnPadding +const IDX_X2_CONV0: usize = 258; // ConvCarry(X2, 0) +const IDX_YG_CONV0: usize = 323; // ConvCarry(Yg, 0) +const IDX_Q1_BIT32: usize = 388; // IS_BIT(q1[32]) +const IDX_XG_CARRY0: usize = 389; // CarryBit(XgLtP, 0) +const IDX_XG_OVERFLOW: usize = 396; // OverflowRequired(XgLtP) + fn gx_le() -> [u8; 32] { // secp256k1 Gx, little-endian. let mut be = [ @@ -39,12 +48,9 @@ fn op_for(k: u64) -> EcsmOperation { } } -/// Evaluate the ECSM [`ConstraintSet`] on one trace row (the compiled prover -/// folder path), returning every base-field constraint value. -fn eval_row(trace: &TraceTable, row: usize) -> Vec { - let main: Vec = (0..cols::NUM_COLUMNS) - .map(|c| *trace.main_table.get(row, c)) - .collect(); +/// Evaluate the ECSM [`ConstraintSet`] on a single main-trace row (the compiled +/// prover folder path), returning every base-field constraint value. +fn eval_main_row(main: Vec) -> Vec { let n = EcsmConstraints.meta().len(); let frame = Frame::::new(vec![TableView::new( vec![main], @@ -61,8 +67,16 @@ fn eval_row(trace: &TraceTable, row: usize base } +/// Evaluate the constraint set on trace row `row`. +fn eval_row(trace: &TraceTable, row: usize) -> Vec { + let main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(row, c)) + .collect(); + eval_main_row(main) +} + /// Every ECSM constraint evaluates to zero on a generated trace (real + padding -/// rows). This exercises the padding closure (`q1 = p`, µ-gated `b`) end to end. +/// rows). Exercises the all-zero padding closure (µ-gated `p²` and `b`) end to end. #[test] fn constraints_hold_on_generated_trace() { let ops: Vec = [1u64, 2, 5, 0xFFFF, 1_000_003] @@ -80,5 +94,176 @@ fn constraints_hold_on_generated_trace() { #[test] fn constraint_set_count() { - assert_eq!(EcsmConstraints.meta().len(), 148); + assert_eq!(EcsmConstraints.meta().len(), 413); +} + +/// The yG carry recurrence closes on all-zero padding because both the `µ·p²` offset and the +/// curve constant `µ·b` are multiplied by `µ`, so they vanish when `µ = 0`. This checks the +/// closing argument (Yg limb-0 ConvCarry = constraint `IDX_YG_CONV0`) and its two ingredients. +#[test] +fn yg_padding_closes_via_mu_gated_p2_and_b() { + // yG limb-0 ConvCarry residual on a one-off row with the given `µ` and `q1`. + let yg_residual = |mu: u64, q1_is_p: bool| { + let mut main = vec![FE::zero(); cols::NUM_COLUMNS]; + main[cols::MU] = FE::from(mu); + if q1_is_p { + for (i, &b) in P_BYTES.iter().enumerate() { + main[cols::Q1 + i] = FE::from(b as u64); + } + } + eval_main_row(main)[IDX_YG_CONV0] + }; + + // Padding row (µ=0, q1=0): µ gates away both p² and b → closes trivially. + assert_eq!( + yg_residual(0, false), + FE::zero(), + "padding row (µ=0, q1=0) must close" + ); + + // µ=0 but q1=p: µ·p² is gated away, so q1·p is unmatched → residual = +P_0² = +47² = 2209. + assert_eq!( + yg_residual(0, true), + FE::from(2209u64), + "µ=0 with q1=p leaves +P_0² = +47² residual" + ); + + // µ=1, q1=0: s_i = µ·P_0² − µ·b = 2209 − 7 = 2202 → residual (256·c − c_prev − s_i) = −2202. + assert_eq!( + yg_residual(1, false), + FE::zero() - FE::from(2202u64), + "µ=1, q1=0: residual = −(P_0² − b) = −2202" + ); + + // x² has no standalone constant → closes on an all-zero padding row regardless. + let mut zero = vec![FE::zero(); cols::NUM_COLUMNS]; + zero[cols::MU] = FE::zero(); + assert_eq!( + eval_main_row(zero)[IDX_X2_CONV0], + FE::zero(), + "x² closes on all-zero padding (no standalone constant)" + ); +} + +/// A µ=0 padding row with any k_bit set must violate KBitsZeroOnPadding. +/// Guards against a prover injecting phantom `Bit` bus receives on padding rows. +#[test] +fn k_bits_zero_on_padding_rejects_forged_row() { + // Single forged bit on padding row: sum=1, (1−µ)=1 → 1. + let mut main = vec![FE::zero(); cols::NUM_COLUMNS]; + main[cols::k_bit(0)] = FE::one(); + assert_eq!( + eval_main_row(main.clone())[IDX_KBITS_ZERO], + FE::one(), + "k_bit[0]=1 on µ=0 must fire (residual=1)" + ); + + // Same bit on an active row (µ=1): constraint holds. + main[cols::MU] = FE::one(); + assert_eq!( + eval_main_row(main)[IDX_KBITS_ZERO], + FE::zero(), + "k_bit[0]=1 on µ=1 must not fire" + ); + + // Multiple forged bits: sum=3, residual=3. + let mut main_multi = vec![FE::zero(); cols::NUM_COLUMNS]; + main_multi[cols::k_bit(0)] = FE::one(); + main_multi[cols::k_bit(7)] = FE::one(); + main_multi[cols::k_bit(255)] = FE::one(); + assert_eq!( + eval_main_row(main_multi)[IDX_KBITS_ZERO], + FE::from(3u64), + "3 forged k_bits → residual=3" + ); +} + +/// OverflowRequired for XgLtP evaluates non-zero when xG = p (no valid xg_sub_p exists). +/// All CarryBit constraints still hold (c_i=0 is a valid bit), but the carry chain never +/// reaches c_7=1, so OverflowRequired = µ·(1−c_7) = 1 fires. +#[test] +fn xg_ge_p_overflow_required_fires() { + let mut main = vec![FE::zero(); cols::NUM_COLUMNS]; + main[cols::MU] = FE::one(); + // xG = p, xg_sub_p = 0 (invalid subtraction witness — fine for this isolation test). + for (i, &b) in P_BYTES.iter().enumerate() { + main[cols::xg(i)] = FE::from(b as u64); + } + let row = eval_main_row(main); + + for i in 0..7 { + assert_eq!( + row[IDX_XG_CARRY0 + i], + FE::zero(), + "carry bit {i}: c_i=0 is a valid bit" + ); + } + assert_ne!( + row[IDX_XG_OVERFLOW], + FE::zero(), + "OverflowRequired must fire when xG = p" + ); +} + +fn five_g_x_le() -> [u8; 32] { + // x-coordinate of 5·G (secp256k1), little-endian. + // 0x2f8bde4d1a07209355b4a7250a5c5128e88b84bddc619ab7cba8d569b240efe4 + [ + 0xe4, 0xef, 0x40, 0xb2, 0x69, 0xd5, 0xa8, 0xcb, 0xb7, 0x9a, 0x61, 0xdc, 0xbd, 0x84, 0x8b, + 0xe8, 0x28, 0x51, 0x5c, 0x0a, 0x25, 0xa7, 0xb4, 0x55, 0x93, 0x20, 0x07, 0x1a, 0x4d, 0xde, + 0x8b, 0x2f, + ] +} + +/// Exercises the q1[32]=1 path by using x(5·G) as the base point, which produces a yG +/// quotient whose high byte (index 32) equals 1. IS_BIT(q1[32]) must still hold. +#[test] +fn q1_bit32_equals_one_path() { + let witness = + compute_witness(&k_le(1), &five_g_x_le()).expect("k=1, xG=x(5·G) is a valid ECSM input"); + assert_eq!( + witness.q1[32], 1, + "sanity: q1[32] should be 1 for x(5·G) as base point" + ); + + let op = EcsmOperation { + timestamp: 100, + addr_xg: 0x2000, + addr_k: 0x3000, + addr_xr: 0x1000, + witness, + }; + let trace = generate_ecsm_trace(&[op]); + + for row in 0..trace.num_rows() { + assert_eq!( + eval_row(&trace, row)[IDX_Q1_BIT32], + FE::zero(), + "IS_BIT(q1[32]) must hold (value=1) at row {row}" + ); + } +} + +/// End-to-end constraint check for k = N−1, the maximum valid scalar (len_k = 255). +#[test] +fn constraints_hold_for_k_eq_n_minus_one() { + let mut k_bytes = N_BYTES; + k_bytes[0] -= 1; // N is odd, so N_BYTES[0] >= 1; this gives N-1 in little-endian. + let witness = compute_witness(&k_bytes, &gx_le()).expect("N-1 is a valid scalar"); + assert_eq!(witness.len_k, 255, "N-1 has MSB at bit 255"); + + let op = EcsmOperation { + timestamp: 999, + addr_xg: 0x2000, + addr_k: 0x3000, + addr_xr: 0x1000, + witness, + }; + let trace = generate_ecsm_trace(&[op]); + + for row in 0..trace.num_rows() { + for (i, v) in eval_row(&trace, row).iter().enumerate() { + assert_eq!(*v, FE::zero(), "constraint {i} must hold at row {row}"); + } + } } diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 2c06d7fcf..c3600c359 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -39,8 +39,6 @@ pub mod disk_spill_tests; #[cfg(test)] pub mod dvrm_tests; #[cfg(test)] -pub mod ec_scalar_tests; -#[cfg(test)] pub mod ecdas_tests; #[cfg(test)] pub mod ecsm_tests;