From 84c52d7a6ed32b7baf230008f3d84a7454c0bc0d Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 30 Jun 2026 14:58:14 -0300 Subject: [PATCH 01/12] inline ec_scalar chip into ecsm --- prover/src/lib.rs | 15 +- prover/src/tables/ec_scalar.rs | 376 ---------------------------- prover/src/tables/ecsm.rs | 136 ++++++---- prover/src/tables/mod.rs | 1 - prover/src/tables/trace_builder.rs | 54 +--- prover/src/tables/types.rs | 11 +- prover/src/test_utils.rs | 19 -- prover/src/tests/ec_scalar_tests.rs | 91 ------- prover/src/tests/ecsm_tests.rs | 4 +- prover/src/tests/mod.rs | 2 - 10 files changed, 107 insertions(+), 602 deletions(-) delete mode 100644 prover/src/tables/ec_scalar.rs delete mode 100644 prover/src/tests/ec_scalar_tests.rs diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 143d1ead6..97f74423e 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -51,9 +51,9 @@ use crate::tables::trace_builder::count_table_lengths; use crate::tables::types::BusId; use crate::test_utils::{ E, F, VmAir, create_bitwise_air, create_branch_air, create_bytewise_air, create_commit_air, - create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_ec_scalar_air, - create_ecdas_air, create_ecsm_air, create_eq_air, create_halt_air, create_keccak_air, - create_keccak_rc_air, create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air, + create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_ecdas_air, + create_ecsm_air, create_eq_air, create_halt_air, create_keccak_air, create_keccak_rc_air, + create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air, create_page_air, create_register_air, create_shift_air, create_store_air, }; @@ -75,8 +75,8 @@ pub struct RuntimePageRange { /// Number of tables that always contribute exactly one sub-proof, regardless /// of `TableCounts`: bitwise, decode, halt, commit, keccak, keccak_rnd, -/// keccak_rc, register, ecsm, ec_scalar, ecdas. -pub const FIXED_TABLE_COUNT: usize = 11; +/// keccak_rc, register, ecsm, ecdas. +pub const FIXED_TABLE_COUNT: usize = 10; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -250,7 +250,6 @@ pub(crate) struct VmAirs { pub keccak_rnd: VmAir, pub keccak_rc: VmAir, pub ecsm: VmAir, - pub ec_scalar: VmAir, pub ecdas: VmAir, pub register: VmAir, pub pages: Vec, @@ -276,7 +275,6 @@ impl VmAirs { (&self.keccak_rnd, &mut traces.keccak_rnd, &()), (&self.keccak_rc, &mut traces.keccak_rc, &()), (&self.ecsm, &mut traces.ecsm, &()), - (&self.ec_scalar, &mut traces.ec_scalar, &()), (&self.ecdas, &mut traces.ecdas, &()), (&self.register, &mut traces.register, &()), ]; @@ -351,7 +349,6 @@ impl VmAirs { &self.keccak_rnd, &self.keccak_rc, &self.ecsm, - &self.ec_scalar, &self.ecdas, &self.register, ]; @@ -501,7 +498,6 @@ impl VmAirs { tables::keccak_rc::NUM_PRECOMPUTED_COLS, ); let ecsm = create_ecsm_air(proof_options); - let ec_scalar = create_ec_scalar_air(proof_options); let ecdas = create_ecdas_air(proof_options); let register = if let Some((commitment, num_preprocessed_cols)) = register_preprocessed { create_register_air(proof_options).with_preprocessed(commitment, num_preprocessed_cols) @@ -587,7 +583,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 dd8d483a2..000000000 --- a/prover/src/tables/ec_scalar.rs +++ /dev/null @@ -1,376 +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 math::field::element::FieldElement; -use math::field::traits::{IsField, IsSubFieldOf}; -use stark::constraints::transition::{TransitionConstraint, TransitionConstraintEvaluator}; -use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; -use stark::table::TableView; -use stark::trace::TraceTable; - -use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; -use crate::constraints::templates::new_is_bit_constraints; - -// ========================================================================= -// 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( - vec![FE::zero(); 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 -} - -// ========================================================================= -// Constraints -// ========================================================================= - -/// `a · b = 0` or `a · (1 - b) = 0` (degree 2), used for the spec's implication -/// constraints (`limb_bits_i = 1 ⇒ μ = 1`, `last_limb ⇒ μ`, `last_limb ⇒ offset = 0`). -pub struct MulZeroConstraint { - pub a: usize, - pub b: usize, - /// when true, the second factor is `(1 - b)` instead of `b` - pub b_complement: bool, - pub constraint_idx: usize, -} - -impl TransitionConstraint for MulZeroConstraint { - fn degree(&self) -> usize { - 2 - } - - fn constraint_idx(&self) -> usize { - self.constraint_idx - } - - fn evaluate(&self, step: &TableView) -> FieldElement - where - F: IsSubFieldOf, - E: IsField, - { - let a = step.get_main_evaluation_element(0, self.a).clone(); - let b = step.get_main_evaluation_element(0, self.b).clone(); - if self.b_complement { - a * (FieldElement::::one() - b) - } else { - a * b - } - } -} - -/// Creates all EC_SCALAR transition constraints (20 total). -pub fn create_constraints( - constraint_idx_start: usize, -) -> ( - Vec>>, - usize, -) { - let mut constraints: Vec< - Box>, - > = Vec::with_capacity(20); - let mut idx = constraint_idx_start; - - // IS_BIT for mu, limb_bits[0..8], last_limb. - let mut bit_cols = vec![cols::MU]; - bit_cols.extend((0..8).map(cols::limb_bit)); - bit_cols.push(cols::LAST_LIMB); - let (bit_constraints, next) = new_is_bit_constraints(&bit_cols, idx); - for c in bit_constraints { - constraints.push(c.boxed()); - } - idx = next; - - // limb_bits[i] = 1 ⇒ mu = 1 : limb_bits[i] · (1 - mu) = 0 - for i in 0..8 { - constraints.push( - MulZeroConstraint { - a: cols::limb_bit(i), - b: cols::MU, - b_complement: true, - constraint_idx: idx, - } - .boxed(), - ); - idx += 1; - } - - // last_limb = 1 ⇒ mu = 1 : last_limb · (1 - mu) = 0 - constraints.push( - MulZeroConstraint { - a: cols::LAST_LIMB, - b: cols::MU, - b_complement: true, - constraint_idx: idx, - } - .boxed(), - ); - idx += 1; - - // last_limb = 1 ⇒ offset = 0 : last_limb · offset = 0 - constraints.push( - MulZeroConstraint { - a: cols::LAST_LIMB, - b: cols::OFFSET, - b_complement: false, - constraint_idx: idx, - } - .boxed(), - ); - idx += 1; - - (constraints, idx) -} diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index f8ec0859d..a28670752 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -3,8 +3,8 @@ //! 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. @@ -26,7 +26,7 @@ use stark::table::TableView; use stark::trace::TraceTable; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; -use crate::constraints::templates::{INV_SHIFT_32, IsBitConstraint}; +use crate::constraints::templates::{INV_SHIFT_32, IsBitConstraint, new_is_bit_constraints}; use ecsm::{B, EcsmWitness, N_BYTES, P_BYTES}; // Bias signed convolution carries into IsHalfword [0, 2^16); see spec ecsm.typ "Carry offset" (@ecsm-limb_carry). @@ -49,27 +49,28 @@ 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 K_SUB_N: usize = 618; // U256HL (16 halfwords) + pub const XR_SUB_P: usize = 634; // U256HL (16 halfwords) + pub const MU: usize = 650; + + pub const NUM_COLUMNS: usize = 651; #[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] @@ -168,7 +169,10 @@ 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); @@ -278,6 +282,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 // ========================================================================= @@ -368,7 +390,7 @@ 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), @@ -482,16 +504,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(), ), @@ -500,19 +523,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(), @@ -742,13 +761,17 @@ impl OverflowKind { 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::KLtN => cols::K, OverflowKind::XrLtP => cols::XR, } } + /// Whether the sum is stored as individual bits (k) rather than bytes (xR). + fn sum_is_bits(self) -> bool { + matches!(self, OverflowKind::KLtN) + } } /// Computes the 8 word-carries of the addition for `kind`. @@ -759,7 +782,7 @@ where { let inv = FieldElement::::from(INV_SHIFT_32); let hl = kind.addend_hl_base(); - let bl = kind.sum_bl_base(); + let base = kind.sum_col_base(); let mut c: [FieldElement; 8] = std::array::from_fn(|_| FieldElement::zero()); let mut prev = FieldElement::::zero(); for (i, slot) in c.iter_mut().enumerate() { @@ -767,11 +790,24 @@ where let addend1 = step.get_main_evaluation_element(0, hl + 2 * i).clone() + step.get_main_evaluation_element(0, hl + 2 * i + 1).clone() * FieldElement::::from(1u64 << 16); - // sum word i (from bytes): Σ bl[4i+b]·2^{8b} + // sum word i: computed from individual bits (k) or bytes (xR). let mut sum = FieldElement::::zero(); - for b in 0..4 { - sum += step.get_main_evaluation_element(0, bl + 4 * i + b).clone() - * FieldElement::::from(1u64 << (8 * b)); + if kind.sum_is_bits() { + // k is stored as 256 individual bits; word i = bits 32i..32i+31. + for bit in 0..32 { + sum += step + .get_main_evaluation_element(0, base + 32 * i + bit) + .clone() + * FieldElement::::from(1u64 << bit); + } + } else { + // xR is stored as 32 bytes; word i = bytes 4i..4i+3. + for b in 0..4 { + sum += step + .get_main_evaluation_element(0, base + 4 * i + b) + .clone() + * FieldElement::::from(1u64 << (8 * b)); + } } let addend0 = FieldElement::::from(kind.const_word(i)); let ci = (addend0 + addend1 + prev.clone() - sum) * inv.clone(); @@ -831,7 +867,7 @@ impl TransitionConstraint for OverflowRequ } } -/// Creates all ECSM transition constraints (148 total). +/// Creates all ECSM transition constraints (405 total: 1 mu + 256 k bits + 148 others). pub fn create_constraints( constraint_idx_start: usize, ) -> ( @@ -847,6 +883,14 @@ pub fn create_constraints( constraints.push(IsBitConstraint::unconditional(cols::MU, idx).boxed()); idx += 1; + // IS_BIT(k[i]) for all 256 scalar bits. + let k_bit_cols: Vec = (0..256).map(cols::k_bit).collect(); + let (k_bit_constraints, next_idx) = new_is_bit_constraints(&k_bit_cols, idx); + for c in k_bit_constraints { + constraints.push(c.boxed()); + } + idx = next_idx; + // x2 convolution: 64 carries + closing. for i in 0..64 { constraints.push( 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 f3ca090d7..8fbd80704 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; @@ -363,7 +362,7 @@ fn collect_cpu_ops( /// MEMW and LOAD collection requires sequential processing with state tracking. /// /// Returns: (memw_ops, load_ops, lt_ops, shift_ops, bitwise_ops, commit_ops, keccak_ops, -/// cpu32_ops, ecsm_ops, ec_scalar_ops, ecdas_ops) +/// cpu32_ops, ecsm_ops, ecdas_ops) #[allow(clippy::type_complexity)] fn collect_ops_from_cpu( cpu_ops: &[CpuOperation], @@ -379,7 +378,6 @@ fn collect_ops_from_cpu( Vec, Vec, Vec, - Vec, Vec, ) { let mut memw_ops = Vec::with_capacity(cpu_ops.len() * 3); @@ -391,7 +389,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 @@ -478,13 +475,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_ops.extend(ecsm_memw); ecsm_ops.push(ecsm_op); - ec_scalar_ops.extend(ec_scalar_rows); ecdas_ops.extend(ecdas_rows); } @@ -540,7 +536,6 @@ fn collect_ops_from_cpu( keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, ) } @@ -664,7 +659,6 @@ fn collect_ecsm_ops( ) -> ( Vec, ecsm::EcsmOperation, - Vec, Vec, ) { let t = op.timestamp; @@ -683,7 +677,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(47); + let mut memw_ops = Vec::with_capacity(15); // x11 -> addr_xG, x12 -> addr_k (register reads at T). for reg in [11u8, 12u8] { @@ -724,19 +718,6 @@ fn collect_ecsm_ops( register_state.write(10, val, 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 u64, 0, 0, 0, 0, 0, 0, 0]; - let (_v, old_ts) = memory_state.read_byte(addr); - memw_ops.push( - MemwOperation::new(false, addr, value, t + 1, 1, true) - .with_old(value, [old_ts, 0, 0, 0, 0, 0, 0, 0]), - ); - memory_state.write_byte(addr, byte, t + 1); - } - // xR writes at T + 2 (4 doublewords). for i in 0..4 { let addr = addr_xr.wrapping_add((8 * i) as u64); @@ -753,7 +734,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() @@ -768,7 +748,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, @@ -2555,9 +2535,6 @@ pub struct Traces { /// ECSM core table (one row per scalar-multiplication ecall) pub ecsm: TraceTable, - /// EC_SCALAR table (32 rows per ecall) - pub ec_scalar: TraceTable, - /// ECDAS double/add table (variable rows per ecall) pub ecdas: TraceTable, @@ -2601,7 +2578,6 @@ struct CollectedOps { cpu32_ops: Vec, // EC scalar-multiplication accelerator chips. ecsm_ops: Vec, - ec_scalar_ops: Vec, ecdas_ops: Vec, } @@ -2656,7 +2632,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, @@ -2795,7 +2770,6 @@ fn collect_all_ops( store_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, } } @@ -2839,7 +2813,6 @@ fn build_traces( store_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, } = ops; @@ -3114,7 +3087,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) = @@ -3127,7 +3099,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")); @@ -3168,7 +3140,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 { @@ -3196,7 +3167,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()); } @@ -3231,7 +3201,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`, @@ -3297,7 +3266,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, @@ -3555,7 +3523,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; @@ -3597,7 +3564,6 @@ impl Traces { keccak_rnd, keccak_rc, ecsm, - ec_scalar, ecdas, memw_registers, eqs, @@ -3665,7 +3631,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 } @@ -3707,7 +3672,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 { @@ -3730,7 +3694,6 @@ impl Traces { keccak_rnd, keccak_rc, ecsm, - ec_scalar, ecdas, memw_registers, eqs, @@ -3798,7 +3761,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 } @@ -4015,7 +3977,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); @@ -4030,7 +3991,6 @@ impl Traces { keccak_ops, cpu32_ops, ecsm_ops, - ec_scalar_ops, ecdas_ops, &mut register_state, is_final, @@ -4083,7 +4043,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); @@ -4098,7 +4057,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 71c83284a..0c91cd6d6 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -297,15 +297,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, // ========================================================================= @@ -341,7 +340,6 @@ impl BusId { BusId::MemoryOp => "MemoryOp", BusId::Cpu32 => "Cpu32", BusId::Ecdas => "Ecdas", - BusId::ServeK => "ServeK", BusId::Bit => "Bit", BusId::GlobalMemory => "GlobalMemory", } @@ -374,7 +372,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 fd9d9d40c..29ad3afe3 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -58,9 +58,6 @@ use crate::tables::decode::{bus_interactions as decode_bus_interactions, cols as use crate::tables::dvrm::{ bus_interactions as dvrm_bus_interactions, cols as dvrm_cols, dvrm_constraints, }; -use crate::tables::ec_scalar::{ - bus_interactions as ec_scalar_bus_interactions, cols as ec_scalar_cols, -}; use crate::tables::ecdas::{bus_interactions as ecdas_bus_interactions, cols as ecdas_cols}; use crate::tables::ecsm::{bus_interactions as ecsm_bus_interactions, cols as ecsm_cols}; use crate::tables::eq::{bus_interactions as eq_bus_interactions, cols as eq_cols, eq_constraints}; @@ -1062,22 +1059,6 @@ pub fn create_ecsm_air(proof_options: &ProofOptions) -> VmAir { .with_name("ECSM") } -/// Create EC_SCALAR AIR (serves the scalar bit-by-bit to ECDAS). -pub fn create_ec_scalar_air(proof_options: &ProofOptions) -> VmAir { - let (transition_constraints, _) = crate::tables::ec_scalar::create_constraints(0); - let auxiliary_trace_build_data = AuxiliaryTraceBuildData { - interactions: ec_scalar_bus_interactions(), - }; - AirWithBuses::new( - ec_scalar_cols::NUM_COLUMNS, - auxiliary_trace_build_data, - proof_options, - 1, - transition_constraints, - ) - .with_name("EC_SCALAR") -} - /// Create ECDAS AIR (per-step double/add of the scalar-multiplication sequence). pub fn create_ecdas_air(proof_options: &ProofOptions) -> VmAir { let (transition_constraints, _) = crate::tables::ecdas::create_constraints(0); diff --git a/prover/src/tests/ec_scalar_tests.rs b/prover/src/tests/ec_scalar_tests.rs deleted file mode 100644 index 462443843..000000000 --- a/prover/src/tests/ec_scalar_tests.rs +++ /dev/null @@ -1,91 +0,0 @@ -//! Tests for the EC_SCALAR table — constraint satisfaction on generated traces, -//! the `last_limb` schedule, and the constraint count. - -use crate::constraints::templates::IsBitConstraint; -use crate::tables::ec_scalar::{ - MulZeroConstraint, cols, create_constraints, generate_ec_scalar_trace, rows_for_scalar, -}; -use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; -use stark::constraints::transition::TransitionConstraint; -use stark::table::TableView; -use stark::trace::TraceTable; - -/// Builds a one-row `TableView` for `row` of the trace (constraints only read row 0). -fn row_view( - trace: &TraceTable, - row: usize, -) -> TableView { - let main: Vec = (0..cols::NUM_COLUMNS) - .map(|c| *trace.main_table.get(row, c)) - .collect(); - TableView::new(vec![main], vec![]) -} - -#[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); - - // IS_BIT columns - let mut bit_cols = vec![cols::MU]; - bit_cols.extend((0..8).map(cols::limb_bit)); - bit_cols.push(cols::LAST_LIMB); - - for row in 0..trace.num_rows() { - let view = row_view(&trace, row); - for &col in &bit_cols { - let v = IsBitConstraint::unconditional(col, 0).evaluate(&view); - assert_eq!(v, FE::zero(), "IS_BIT col {col} row {row}"); - } - // implication constraints - for i in 0..8 { - let c = MulZeroConstraint { - a: cols::limb_bit(i), - b: cols::MU, - b_complement: true, - constraint_idx: 0, - }; - assert_eq!(c.evaluate(&view), FE::zero(), "limb_bit{i}=>mu row {row}"); - } - let c = MulZeroConstraint { - a: cols::LAST_LIMB, - b: cols::MU, - b_complement: true, - constraint_idx: 0, - }; - assert_eq!(c.evaluate(&view), FE::zero(), "last_limb=>mu row {row}"); - let c = MulZeroConstraint { - a: cols::LAST_LIMB, - b: cols::OFFSET, - b_complement: false, - constraint_idx: 0, - }; - assert_eq!(c.evaluate(&view), FE::zero(), "last_limb=>offset 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 create_constraints_count() { - let (constraints, next) = create_constraints(0); - assert_eq!(constraints.len(), 20); - assert_eq!(next, 20); -} diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index bc92c4596..331e52413 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -123,8 +123,8 @@ fn constraints_hold_on_generated_trace() { #[test] fn create_constraints_count() { let (constraints, next) = create_constraints(0); - assert_eq!(constraints.len(), 148); - assert_eq!(next, 148); + assert_eq!(constraints.len(), 404); + assert_eq!(next, 404); } /// The yG carry recurrence is unsatisfiable on a padding row unless two ingredients hold, diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 9b32e3b8c..04aaed5c1 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -31,8 +31,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; From 0547f0836e17e32f7b549252244cb691a76241e0 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 30 Jun 2026 15:48:45 -0300 Subject: [PATCH 02/12] Add xG range check in the ECSM AIR --- crypto/ecsm/src/witness.rs | 4 +++ prover/src/tables/ecsm.rs | 50 ++++++++++++++++++++++++++---- prover/src/tables/trace_builder.rs | 5 ++- prover/src/tests/ecsm_tests.rs | 4 +-- 4 files changed, 54 insertions(+), 9 deletions(-) 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 usize { @@ -102,6 +103,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 } @@ -179,6 +184,7 @@ pub fn generate_ecsm_trace( 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); @@ -489,6 +495,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, @@ -737,6 +750,7 @@ impl TransitionConstraint for ColIsZero { /// `p + xR_sub_p = xR + 2^256` (with `xR_sub_p = xR − p mod 2^256`). #[derive(Clone, Copy)] pub enum OverflowKind { + XgLtP, KLtN, XrLtP, } @@ -745,6 +759,7 @@ impl OverflowKind { /// The constant addend's 32-bit word `i` (`N` for `k u64 { let bytes = match self { + OverflowKind::XgLtP => &P_BYTES, OverflowKind::KLtN => &N_BYTES, OverflowKind::XrLtP => &P_BYTES, }; @@ -757,6 +772,7 @@ impl OverflowKind { /// Column base of the witnessed halfword addend (`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, } @@ -764,11 +780,12 @@ impl OverflowKind { /// 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 (xR). + /// Whether the sum is stored as individual bits (k) rather than bytes (xR/xG). fn sum_is_bits(self) -> bool { matches!(self, OverflowKind::KLtN) } @@ -867,7 +884,7 @@ impl TransitionConstraint for OverflowRequ } } -/// Creates all ECSM transition constraints (405 total: 1 mu + 256 k bits + 148 others). +/// Creates all ECSM transition constraints (412 total: 1 mu + 256 k bits + 8 xG

( @@ -937,6 +954,27 @@ pub fn create_constraints( constraints.push(IsBitConstraint::unconditional(cols::q1(32), idx).boxed()); idx += 1; + // xG < p: 7 carry bits + overflow-required. + for i in 0..7 { + constraints.push( + CarryBit { + kind: OverflowKind::XgLtP, + i, + constraint_idx: idx, + } + .boxed(), + ); + idx += 1; + } + constraints.push( + OverflowRequired { + kind: OverflowKind::XgLtP, + constraint_idx: idx, + } + .boxed(), + ); + idx += 1; + // k < N: 7 carry bits + overflow-required. for i in 0..7 { constraints.push( diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 8fbd80704..bb2b88559 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2107,8 +2107,11 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec Date: Tue, 30 Jun 2026 15:54:37 -0300 Subject: [PATCH 03/12] Make ECSM memory interaction timestamps disjoint --- prover/src/tables/ecsm.rs | 27 ++++++------- prover/src/tables/trace_builder.rs | 61 ++++++++++++++++++++---------- 2 files changed, 56 insertions(+), 32 deletions(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 468e60809..200282b55 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -368,7 +368,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(), @@ -377,13 +387,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 { @@ -400,7 +410,7 @@ pub fn bus_interactions() -> Vec { 0, base_lo, packed(cols::ADDR_K_1), - ts_lo(), + ts_lo_plus(1), ts_hi(), 0, 1, @@ -409,15 +419,6 @@ 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), - ]) - }; out.push(BusInteraction::sender( BusId::Memw, mu(), diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index bb2b88559..874c00134 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -679,32 +679,55 @@ fn collect_ecsm_ops( 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 = [0u64; 8]; - let mut dword = 0u64; - for j in 0..8 { - value[j] = bytes[8 * i + j] as u64; - 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 = [0u64; 8]; + let mut dword = 0u64; + for j in 0..8 { + value[j] = witness.x_g[8 * i + j] as u64; + 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); + } + + // x12 -> addr_k (register read at T+1). + { + let (val, old_ts) = register_state.read(12); + let value = pack_register_value(val); + memw_ops.push( + 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(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 = [0u64; 8]; + let mut dword = 0u64; + for j in 0..8 { + value[j] = witness.k[8 * i + j] as u64; + 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); } // x10 -> addr_xR (register read at T + 1). From 8eca0e7d107d7e77e11dc39af89839924af1355a Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 30 Jun 2026 16:11:50 -0300 Subject: [PATCH 04/12] Extend q1 range check to all 33 bytes --- prover/src/tables/ecsm.rs | 8 ++------ prover/src/tables/trace_builder.rs | 3 ++- prover/src/tests/ecsm_tests.rs | 4 ++-- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 200282b55..1da76ca5e 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -469,7 +469,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. @@ -885,7 +885,7 @@ impl TransitionConstraint for OverflowRequ } } -/// Creates all ECSM transition constraints (412 total: 1 mu + 256 k bits + 8 xG

( @@ -951,10 +951,6 @@ pub fn create_constraints( ); idx += 1; - // IS_BIT(q1[32]) - constraints.push(IsBitConstraint::unconditional(cols::q1(32), idx).boxed()); - idx += 1; - // xG < p: 7 carry bits + overflow-required. for i in 0..7 { constraints.push( diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 874c00134..d92d482db 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2118,13 +2118,14 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec Date: Tue, 30 Jun 2026 16:42:23 -0300 Subject: [PATCH 05/12] =?UTF-8?q?Fix=20ECDAS=20padding=20and=20gate=20R?= =?UTF-8?q?=C2=B7P=20term=20with=20=CE=BC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- prover/src/tables/ecdas.rs | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index 6d508d363..bd60187a2 100644 --- a/prover/src/tables/ecdas.rs +++ b/prover/src/tables/ecdas.rs @@ -133,12 +133,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 @@ -313,15 +311,20 @@ impl ConvCarry { let xr = |j: usize| b(cols::XR, 32, j); let yr = |j: usize| b(cols::YR, 32, j); let op = col(cols::OP); + let mu = col(cols::MU); let one = FieldElement::::one(); - // r·P − q·P convolution (shared structure across all three relations). + // μ·R·P − q·P convolution (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. let rq = |qbase: usize| -> FieldElement { - let mut s = FieldElement::::zero(); + let mut r_p = FieldElement::::zero(); + let mut q_p = FieldElement::::zero(); for j in 0..=i { - s += (r_byte::(j) - b(qbase, 33, j)) * p_byte::(i - j); + r_p += r_byte::(j) * p_byte::(i - j); + q_p += b(qbase, 33, j) * p_byte::(i - j); } - s + mu.clone() * r_p - q_p }; match self.relation { From 270356accd4935f91598bce3578b0663fd1e9bca Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 30 Jun 2026 16:56:51 -0300 Subject: [PATCH 06/12] Add curve identifier to ECDAS bus --- prover/src/tables/ecdas.rs | 4 ++-- prover/src/tables/ecsm.rs | 8 +++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index bd60187a2..a6b809e81 100644 --- a/prover/src/tables/ecdas.rs +++ b/prover/src/tables/ecdas.rs @@ -159,7 +159,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(), @@ -224,7 +224,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(), diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 1da76ca5e..9ecf01b78 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -591,8 +591,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, @@ -604,7 +605,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)); From 53e31bd20c7a40294be482e87c7c0aba0a74b586 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 1 Jul 2026 09:41:52 -0300 Subject: [PATCH 07/12] Restore IS_BIT on q1[32] and fix stale executor comment --- crypto/ecsm/src/lib.rs | 2 +- executor/src/vm/instruction/execution.rs | 9 ++++----- prover/src/tables/ecsm.rs | 8 +++++++- prover/src/tables/trace_builder.rs | 8 ++++---- prover/src/tests/ecsm_tests.rs | 4 ++-- 5 files changed, 18 insertions(+), 13 deletions(-) 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/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 148d7f86c..bc78eb2e5 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -412,11 +412,10 @@ impl Instruction { { return Err(ExecutionError::EcsmAddressOverflow); } - // xG and k are both read at the same proof timestamp, so their - // 32-byte ranges must be disjoint or the trace is unprovable - // (MEMW orders accesses per address by strictly increasing - // timestamp). xR may alias either: its accesses are offset to - // later timestamps. + // xG and k must occupy disjoint 32-byte regions: overlapping + // addresses would cause the same memory byte to serve as both + // an xG limb and a k bit, corrupting the scalar multiplication. + // xR may alias either: its accesses are at a later timestamp. if addr_xg.abs_diff(addr_k) < 32 { return Err(ExecutionError::EcsmOperandOverlap); } diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 9ecf01b78..7b573dbd7 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -887,7 +887,7 @@ impl TransitionConstraint for OverflowRequ } } -/// Creates all ECSM transition constraints (411 total: 1 mu + 256 k bits + 8 xG

( @@ -953,6 +953,12 @@ pub fn create_constraints( ); idx += 1; + // IS_BIT(q1[32]) — the high byte of the 33-byte yG quotient is a single-bit value. + // The spec mandates this unconditionally (ec:c:q1_257); IS_BYTE(0..32) is separate + // (μ-gated bus interaction) and does not replace this polynomial constraint. + constraints.push(IsBitConstraint::unconditional(cols::q1(32), idx).boxed()); + idx += 1; + // xG < p: 7 carry bits + overflow-required. for i in 0..7 { constraints.push( diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index d92d482db..fba6b6659 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -644,11 +644,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 also +/// at `T + 1`; `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)] diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index 3960712eb..e518f4698 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -123,8 +123,8 @@ fn constraints_hold_on_generated_trace() { #[test] fn create_constraints_count() { let (constraints, next) = create_constraints(0); - assert_eq!(constraints.len(), 411); - assert_eq!(next, 411); + assert_eq!(constraints.len(), 412); + assert_eq!(next, 412); } /// The yG carry recurrence is unsatisfiable on a padding row unless two ingredients hold, From cd412172203c1945a2922f2b20221d391b2cf982 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 1 Jul 2026 11:45:08 -0300 Subject: [PATCH 08/12] Include XgLtP in the overflow carry constraint test loop --- prover/src/tests/ecsm_tests.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index e518f4698..ce6b9cf21 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -94,7 +94,7 @@ fn constraints_hold_on_generated_trace() { .evaluate(&view), FE::zero() ); - for kind in [OverflowKind::KLtN, OverflowKind::XrLtP] { + for kind in [OverflowKind::XgLtP, OverflowKind::KLtN, OverflowKind::XrLtP] { for i in 0..7 { assert_eq!( CarryBit { From 932ed3b4ac74eac9d09904bb802b7870577feac9 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 2 Jul 2026 14:55:21 -0300 Subject: [PATCH 09/12] Fix stale docs, q1 loop trap comment, k_bit IS_BIT test gap --- prover/src/tables/ecdas.rs | 5 +++-- prover/src/tables/trace_builder.rs | 7 +++++-- prover/src/tests/ecsm_tests.rs | 7 +++++++ 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index a6b809e81..6572d76a0 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 λ and xR relations is gated with `μ`, so it +//! vanishes on padding rows (μ=0) and all relations hold with zero carries. use math::field::element::FieldElement; use math::field::traits::{IsField, IsSubFieldOf}; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index fba6b6659..59c3b12e4 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2118,14 +2118,17 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec Date: Fri, 3 Jul 2026 11:02:49 -0300 Subject: [PATCH 10/12] Add KBitsZeroOnPadding and extend ECSM tests --- prover/src/tables/ecsm.rs | 40 +++++++++- prover/src/tests/ecsm_tests.rs | 138 +++++++++++++++++++++++++++++++-- 2 files changed, 169 insertions(+), 9 deletions(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 7b573dbd7..29fcf96bf 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -469,7 +469,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, 33, &mut out); // q1[0..32] (all 33 bytes) + 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. @@ -887,7 +887,35 @@ impl TransitionConstraint for OverflowRequ } } -/// Creates all ECSM transition constraints (412 total: 1 mu + 256 k bits + 1 q1[32] + 8 xG

for KBitsZeroOnPadding { + fn degree(&self) -> usize { + 2 + } + fn constraint_idx(&self) -> usize { + self.constraint_idx + } + fn evaluate(&self, step: &TableView) -> FieldElement + where + F: IsSubFieldOf, + E: IsField, + { + let mu = step.get_main_evaluation_element(0, cols::MU).clone(); + let sum = (0..256).fold(FieldElement::::zero(), |acc, i| { + acc + step.get_main_evaluation_element(0, cols::k_bit(i)).clone() + }); + sum * (FieldElement::::one() - mu) + } +} + +/// Creates all ECSM transition constraints (413 total: 1 mu + 256 k bits + 1 k-bits-zero-on-padding + 1 q1[32] + 8 xG

( @@ -911,6 +939,10 @@ pub fn create_constraints( } idx = next_idx; + // (Σ k_bit[i]) · (1 − µ) = 0: all scalar bits must be zero on padding rows. + constraints.push(KBitsZeroOnPadding { constraint_idx: idx }.boxed()); + idx += 1; + // x2 convolution: 64 carries + closing. for i in 0..64 { constraints.push( @@ -954,8 +986,8 @@ pub fn create_constraints( idx += 1; // IS_BIT(q1[32]) — the high byte of the 33-byte yG quotient is a single-bit value. - // The spec mandates this unconditionally (ec:c:q1_257); IS_BYTE(0..32) is separate - // (μ-gated bus interaction) and does not replace this polynomial constraint. + // The spec mandates this unconditionally (ec:c:q1_257); IS_BYTE(0..=32) covers all 33 + // bytes via a μ-gated bus interaction and does not replace this polynomial constraint. constraints.push(IsBitConstraint::unconditional(cols::q1(32), idx).boxed()); idx += 1; diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index cd2a16d89..5e8e912dd 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -3,11 +3,11 @@ use crate::constraints::templates::IsBitConstraint; use crate::tables::ecsm::{ - CarryBit, ColIsZero, ConvCarry, EcsmOperation, OverflowKind, OverflowRequired, Relation, cols, - create_constraints, generate_ecsm_trace, + CarryBit, ColIsZero, ConvCarry, EcsmOperation, KBitsZeroOnPadding, OverflowKind, + OverflowRequired, Relation, cols, create_constraints, generate_ecsm_trace, }; use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; -use ecsm::{P_BYTES, compute_witness}; +use ecsm::{N_BYTES, P_BYTES, compute_witness}; use stark::constraints::transition::TransitionConstraint; use stark::table::TableView; use stark::trace::TraceTable; @@ -74,6 +74,11 @@ fn constraints_hold_on_generated_trace() { "is_bit(k_bit[{i}]) row {row}" ); } + assert_eq!( + KBitsZeroOnPadding { constraint_idx: 0 }.evaluate(&view), + FE::zero(), + "k_bits_zero_on_padding row {row}" + ); for i in 0..64 { for relation in [Relation::X2, Relation::Yg] { let v = ConvCarry { @@ -130,8 +135,8 @@ fn constraints_hold_on_generated_trace() { #[test] fn create_constraints_count() { let (constraints, next) = create_constraints(0); - assert_eq!(constraints.len(), 412); - assert_eq!(next, 412); + assert_eq!(constraints.len(), 413); + assert_eq!(next, 413); } /// The yG carry recurrence is unsatisfiable on a padding row unless two ingredients hold, @@ -199,3 +204,126 @@ fn yg_padding_closes_via_q1_eq_p_and_mu_gated_b() { "x² closes on all-zero padding (no standalone constant)" ); } + +/// A µ=0 padding row with any k_bit set must violate KBitsZeroOnPadding. +/// This guards against a prover injecting phantom BIT bus receives on padding rows. +#[test] +fn k_bits_zero_on_padding_rejects_forged_row() { + let c = KBitsZeroOnPadding { constraint_idx: 0 }; + + // 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(); + let view: TableView = TableView::new(vec![main.clone()], vec![]); + assert_eq!(c.evaluate(&view), 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(); + let view_active: TableView = TableView::new(vec![main.clone()], vec![]); + assert_eq!(c.evaluate(&view_active), 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(); + let view_multi: TableView = TableView::new(vec![main_multi], vec![]); + assert_eq!(c.evaluate(&view_multi), 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 (zero subtraction witness — invalid for a real prover but valid for + // this constraint isolation test). + for (i, &b) in P_BYTES.iter().enumerate() { + main[cols::xg(i)] = FE::from(b as u64); + } + let view: TableView = TableView::new(vec![main], vec![]); + + for i in 0..7 { + assert_eq!( + CarryBit { kind: OverflowKind::XgLtP, i, constraint_idx: 0 }.evaluate(&view), + FE::zero(), + "carry bit {i}: c_i=0 is a valid bit" + ); + } + assert_ne!( + OverflowRequired { kind: OverflowKind::XgLtP, constraint_idx: 0 }.evaluate(&view), + 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() { + let view = row_view(&trace, row); + assert_eq!( + IsBitConstraint::unconditional(cols::q1(32), 0).evaluate(&view), + 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() { + let view = row_view(&trace, row); + assert_eq!(IsBitConstraint::unconditional(cols::MU, 0).evaluate(&view), FE::zero(), "is_bit(mu) row {row}"); + for i in 0..256 { + assert_eq!( + IsBitConstraint::unconditional(cols::k_bit(i), 0).evaluate(&view), + FE::zero(), + "is_bit(k_bit[{i}]) row {row}" + ); + } + assert_eq!(KBitsZeroOnPadding { constraint_idx: 0 }.evaluate(&view), FE::zero(), "k_bits_zero_on_padding row {row}"); + for i in 0..64 { + for relation in [Relation::X2, Relation::Yg] { + assert_eq!(ConvCarry { relation, i, constraint_idx: 0 }.evaluate(&view), FE::zero(), "conv carry i={i} row {row}"); + } + } + assert_eq!(ColIsZero { col: cols::c0(63), constraint_idx: 0 }.evaluate(&view), FE::zero()); + assert_eq!(ColIsZero { col: cols::c1(63), constraint_idx: 0 }.evaluate(&view), FE::zero()); + for kind in [OverflowKind::XgLtP, OverflowKind::KLtN, OverflowKind::XrLtP] { + for i in 0..7 { + assert_eq!(CarryBit { kind, i, constraint_idx: 0 }.evaluate(&view), FE::zero(), "carry bit kind i={i} row {row}"); + } + assert_eq!(OverflowRequired { kind, constraint_idx: 0 }.evaluate(&view), FE::zero(), "overflow required row {row}"); + } + } +} From 0c8dd0b36a7635332d05e22b095ebd417e3ee7e2 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 3 Jul 2026 11:14:24 -0300 Subject: [PATCH 11/12] fix lint --- prover/src/tables/ecsm.rs | 7 +- prover/src/tests/ecsm_tests.rs | 133 +++++++++++++++++++++++++++------ 2 files changed, 116 insertions(+), 24 deletions(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 29fcf96bf..2a7e8800c 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -940,7 +940,12 @@ pub fn create_constraints( idx = next_idx; // (Σ k_bit[i]) · (1 − µ) = 0: all scalar bits must be zero on padding rows. - constraints.push(KBitsZeroOnPadding { constraint_idx: idx }.boxed()); + constraints.push( + KBitsZeroOnPadding { + constraint_idx: idx, + } + .boxed(), + ); idx += 1; // x2 convolution: 64 carries + closing. diff --git a/prover/src/tests/ecsm_tests.rs b/prover/src/tests/ecsm_tests.rs index 5e8e912dd..956c912d9 100644 --- a/prover/src/tests/ecsm_tests.rs +++ b/prover/src/tests/ecsm_tests.rs @@ -214,21 +214,36 @@ 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(); - let view: TableView = TableView::new(vec![main.clone()], vec![]); - assert_eq!(c.evaluate(&view), FE::one(), "k_bit[0]=1 on µ=0 must fire (residual=1)"); + let view: TableView = + TableView::new(vec![main.clone()], vec![]); + assert_eq!( + c.evaluate(&view), + 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(); - let view_active: TableView = TableView::new(vec![main.clone()], vec![]); - assert_eq!(c.evaluate(&view_active), FE::zero(), "k_bit[0]=1 on µ=1 must not fire"); + let view_active: TableView = + TableView::new(vec![main.clone()], vec![]); + assert_eq!( + c.evaluate(&view_active), + 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(); - let view_multi: TableView = TableView::new(vec![main_multi], vec![]); - assert_eq!(c.evaluate(&view_multi), FE::from(3u64), "3 forged k_bits → residual=3"); + let view_multi: TableView = + TableView::new(vec![main_multi], vec![]); + assert_eq!( + c.evaluate(&view_multi), + FE::from(3u64), + "3 forged k_bits → residual=3" + ); } /// OverflowRequired for XgLtP evaluates non-zero when xG = p (no valid xg_sub_p exists). @@ -247,13 +262,22 @@ fn xg_ge_p_overflow_required_fires() { for i in 0..7 { assert_eq!( - CarryBit { kind: OverflowKind::XgLtP, i, constraint_idx: 0 }.evaluate(&view), + CarryBit { + kind: OverflowKind::XgLtP, + i, + constraint_idx: 0 + } + .evaluate(&view), FE::zero(), "carry bit {i}: c_i=0 is a valid bit" ); } assert_ne!( - OverflowRequired { kind: OverflowKind::XgLtP, constraint_idx: 0 }.evaluate(&view), + OverflowRequired { + kind: OverflowKind::XgLtP, + constraint_idx: 0 + } + .evaluate(&view), FE::zero(), "OverflowRequired must fire when xG = p" ); @@ -263,9 +287,9 @@ 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, + 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, ] } @@ -273,11 +297,20 @@ fn five_g_x_le() -> [u8; 32] { /// 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 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 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() { @@ -298,12 +331,22 @@ fn constraints_hold_for_k_eq_n_minus_one() { 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 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() { let view = row_view(&trace, row); - assert_eq!(IsBitConstraint::unconditional(cols::MU, 0).evaluate(&view), FE::zero(), "is_bit(mu) row {row}"); + assert_eq!( + IsBitConstraint::unconditional(cols::MU, 0).evaluate(&view), + FE::zero(), + "is_bit(mu) row {row}" + ); for i in 0..256 { assert_eq!( IsBitConstraint::unconditional(cols::k_bit(i), 0).evaluate(&view), @@ -311,19 +354,63 @@ fn constraints_hold_for_k_eq_n_minus_one() { "is_bit(k_bit[{i}]) row {row}" ); } - assert_eq!(KBitsZeroOnPadding { constraint_idx: 0 }.evaluate(&view), FE::zero(), "k_bits_zero_on_padding row {row}"); + assert_eq!( + KBitsZeroOnPadding { constraint_idx: 0 }.evaluate(&view), + FE::zero(), + "k_bits_zero_on_padding row {row}" + ); for i in 0..64 { for relation in [Relation::X2, Relation::Yg] { - assert_eq!(ConvCarry { relation, i, constraint_idx: 0 }.evaluate(&view), FE::zero(), "conv carry i={i} row {row}"); + assert_eq!( + ConvCarry { + relation, + i, + constraint_idx: 0 + } + .evaluate(&view), + FE::zero(), + "conv carry i={i} row {row}" + ); } } - assert_eq!(ColIsZero { col: cols::c0(63), constraint_idx: 0 }.evaluate(&view), FE::zero()); - assert_eq!(ColIsZero { col: cols::c1(63), constraint_idx: 0 }.evaluate(&view), FE::zero()); + assert_eq!( + ColIsZero { + col: cols::c0(63), + constraint_idx: 0 + } + .evaluate(&view), + FE::zero() + ); + assert_eq!( + ColIsZero { + col: cols::c1(63), + constraint_idx: 0 + } + .evaluate(&view), + FE::zero() + ); for kind in [OverflowKind::XgLtP, OverflowKind::KLtN, OverflowKind::XrLtP] { for i in 0..7 { - assert_eq!(CarryBit { kind, i, constraint_idx: 0 }.evaluate(&view), FE::zero(), "carry bit kind i={i} row {row}"); + assert_eq!( + CarryBit { + kind, + i, + constraint_idx: 0 + } + .evaluate(&view), + FE::zero(), + "carry bit kind i={i} row {row}" + ); } - assert_eq!(OverflowRequired { kind, constraint_idx: 0 }.evaluate(&view), FE::zero(), "overflow required row {row}"); + assert_eq!( + OverflowRequired { + kind, + constraint_idx: 0 + } + .evaluate(&view), + FE::zero(), + "overflow required row {row}" + ); } } } From 9a5619ffcef73f219358411993c1a166e27d15b3 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 3 Jul 2026 13:09:41 -0300 Subject: [PATCH 12/12] =?UTF-8?q?ECSM:=20add=20KBitsZeroOnPadding,=20?= =?UTF-8?q?=C2=B5P=C2=B2=20gate,=20x10=20T+2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- prover/src/tables/ecsm.rs | 37 +++++++++++------------------- prover/src/tables/trace_builder.rs | 12 +++++----- prover/src/tests/ecsm_tests.rs | 36 +++++++++++++---------------- 3 files changed, 35 insertions(+), 50 deletions(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 2a7e8800c..579a930eb 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -10,11 +10,9 @@ //! 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; @@ -198,13 +196,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 } @@ -418,7 +409,7 @@ pub fn bus_interactions() -> Vec { )); } - // read x10 -> addr_xR (register read at ts + 1). + // read x10 -> addr_xR (register read at ts + 2, grouped with xR writes). out.push(BusInteraction::sender( BusId::Memw, mu(), @@ -427,7 +418,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, @@ -640,8 +631,8 @@ fn p_byte(m: usize) -> FieldElement { } /// Convolution carry constraint at limb `i`: `2^8·c_i − c_{i-1} − S_i = 0`, with `c_{-1} = 0`. -/// Unconditional (degree 2); the only µ-gated term is the curve constant `µ·b` inside `S_i` -/// for the yG relation at limb 0 (see [`ConvCarry::s_i`]). +/// Unconditional (degree 2); for the yG relation, both the `µ·p²` offset and the curve +/// constant `µ·b` are µ-gated so that all columns can pad to zero (see [`ConvCarry::s_i`]). pub struct ConvCarry { pub relation: Relation, pub i: usize, @@ -674,19 +665,17 @@ impl ConvCarry { 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 can pad to zero. + let mu = step.get_main_evaluation_element(0, cols::MU).clone(); for j in 0..=i { s += byte(cols::YG, 32, j) * byte(cols::YG, 32, i - j); - s += p_byte::(j) * p_byte::(i - j); + s += mu.clone() * (p_byte::(j) * p_byte::(i - j)); s = s - byte(cols::X2, 32, j) * byte(cols::XG, 32, i - j); s = s - byte(cols::Q1, 33, j) * p_byte::(i - j); } if i == 0 { - // Only the curve constant `b` is gated by `µ`: it vanishes on padding - // (µ=0) and equals `b` on real rows (µ=1). `B` is the zero-extension of - // `b`, so `B_i = 0` for i ≥ 1 — nothing to gate there. The rest of the - // relation stays unconditional. - let mu = step.get_main_evaluation_element(0, cols::MU).clone(); s = s - mu * FieldElement::::from(B); } } @@ -697,7 +686,7 @@ impl ConvCarry { impl TransitionConstraint for ConvCarry { fn degree(&self) -> usize { - 2 // degree-2 convolution; the only µ-gated term (µ·b) is degree 1 + 2 // degree-2 convolution; µ-gated terms (µ·p², µ·b) are degree 1 in columns } fn constraint_idx(&self) -> usize { diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 59c3b12e4..f2dac46f4 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -647,8 +647,8 @@ 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 also -/// at `T + 1`; `xR` memory writes at `T + 2`. Every read advances +/// `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)] @@ -730,15 +730,15 @@ fn collect_ecsm_ops( memory_state.write_bytes(addr, dword, 8, t + 1); } - // x10 -> addr_xR (register read at T + 1). + // 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(true, 2 * 10, value, t + 1, 2, true) + MemwOperation::new(true, 2 * 10, value, t + 2, 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(10, val, t + 2); } // xR writes at T + 2 (4 doublewords). @@ -2118,7 +2118,7 @@ pub(crate) fn collect_bitwise_from_ecsm(ops: &[ecsm::EcsmOperation]) -> Vec