From 1f0ce43f283fff39e1c5a83c5f82e1c4f5665e45 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Jul 2026 14:17:10 -0300 Subject: [PATCH 1/3] docs(ecsm): correct stale column-count comment (~427 -> 667) NUM_COLUMNS is 667 after k widened 32 bytes -> 256 bit-columns and xg_sub_p (16 halfwords) was added. Comment-only; no behavior change. --- prover/src/tables/ecsm.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 6c3af31ae..01e506823 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -28,7 +28,7 @@ pub(crate) const CARRY_OFFSET_X2: i64 = 8160; pub(crate) const CARRY_OFFSET_YG: i64 = 16319; // ========================================================================= -// Column indices (~427 columns) +// Column indices (667 columns; keep in sync with NUM_COLUMNS below) // ========================================================================= pub mod cols { From f516c20e69ec602348699217769fd121adfa087f Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Jul 2026 14:17:17 -0300 Subject: [PATCH 2/3] docs(ecdas): note yR relation is also mu-gated The mu-gated R*P term (rq()) is applied in all three relations -- Lambda, Xr, and Yr (ecdas.rs s_i: Lambda/Xr/Yr all call rq()), not just lambda/xR. Comment-only; no behavior change. --- prover/src/tables/ecdas.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index 6b457d226..e2eaed9f3 100644 --- a/prover/src/tables/ecdas.rs +++ b/prover/src/tables/ecdas.rs @@ -8,7 +8,7 @@ //! bus (an add follows). ECSM seeds and drains the bus; interior rows telescope. //! //! 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 +//! 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}; From 5144ddedf3a1cca3e4e94fbdf455869ccdc045a3 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Jul 2026 14:34:39 -0300 Subject: [PATCH 3/3] perf(ecsm): factor mu out of the Yg p^2 convolution sum The mu-gated p^2 term was multiplied by mu once per inner-loop term (up to i+1 times per limb). Accumulate the constant sum first and apply mu once per limb, mirroring ECDAS rq(). Algebraically identical (mu distributes over the sum; p_byte_expr is a constant), degree unchanged; ~Sum(i+1) fewer field muls per Yg limb over the LDE domain. Validated: ecsm_tests::yg_padding_closes_via_mu_gated_p2_and_b, constraints_hold_on_generated_trace, ecsm_constraint_set_folder_capture_agree, and test_prove_elfs_ecsm{,_multi} + forged-mu rejection all pass. --- prover/src/tables/ecsm.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index 01e506823..ab0654c9a 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -741,13 +741,17 @@ impl EcsmConstraints { // Σ (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 + mu.clone() * (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 { let curve_b = b.const_base(B); s = s - mu * curve_b;