Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion prover/src/tables/ecdas.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down
8 changes: 6 additions & 2 deletions prover/src/tables/ecsm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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;
Expand Down
Loading