diff --git a/crypto/stark/src/constraints/builder.rs b/crypto/stark/src/constraints/builder.rs index 56b10efd0..5395c7228 100644 --- a/crypto/stark/src/constraints/builder.rs +++ b/crypto/stark/src/constraints/builder.rs @@ -119,10 +119,25 @@ pub trait ConstraintBuilder { } // ---- sinks ---------------------------------------------------------- - /// Record base-field constraint `constraint_idx`'s value. - fn emit_base(&mut self, constraint_idx: usize, e: Self::Expr); - /// Record extension-field (LogUp) constraint `constraint_idx`'s value. - fn emit_ext(&mut self, constraint_idx: usize, e: Self::ExprE); + /// Record base-field constraint `constraint_idx`'s value over the trace + /// `rows` it applies to (see [`RowDomain`]). Recording it here is what lets + /// [`ConstraintSet::meta`] be *derived* from this single body (via + /// [`MetaBuilder`]) instead of hand-maintained as a parallel list. The + /// constraint's polynomial degree is NOT declared per-constraint — only the + /// per-table max matters, declared once via [`ConstraintSet::max_degree`]. + fn emit_base_rows(&mut self, constraint_idx: usize, rows: RowDomain, e: Self::Expr); + /// Extension-field (LogUp) counterpart of [`Self::emit_base_rows`]. + fn emit_ext_rows(&mut self, constraint_idx: usize, rows: RowDomain, e: Self::ExprE); + /// Record a base-field constraint that applies to every row (common case). + #[inline] + fn emit_base(&mut self, constraint_idx: usize, e: Self::Expr) { + self.emit_base_rows(constraint_idx, RowDomain::ALL, e); + } + /// Record an extension-field (LogUp) constraint that applies to every row. + #[inline] + fn emit_ext(&mut self, constraint_idx: usize, e: Self::ExprE) { + self.emit_ext_rows(constraint_idx, RowDomain::ALL, e); + } // ---- folds ---------------------------------------------------------- /// Fold one α·value term into a running LogUp fingerprint: @@ -159,41 +174,55 @@ pub enum RootKind { Ext, } -/// Per-constraint metadata: plain data replacing the per-constraint trait -/// objects. `Base` entries MUST form a prefix of an idx-ordered, dense list — -/// see [`num_base_from_meta`]. -/// -/// Every constraint applies to every row (up to `end_exemptions` rows at the -/// end of the trace); there is no per-constraint period/offset/periodic -/// exemption machinery. +/// Which trace rows a transition constraint applies to. `ALL` = every row; +/// `except_last(n)` skips the final `n` rows — used by constraints that read +/// `n` rows ahead (the last `n` rows have no valid "next" to check). Passed at +/// the emit site; degree is NOT here (it's a per-table property, see +/// [`ConstraintSet::max_degree`]) — the two are orthogonal. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub struct RowDomain { + /// Number of exempted rows at the end of the trace. + pub end_exemptions: usize, +} + +impl RowDomain { + /// Every row (no exemptions). + pub const ALL: RowDomain = RowDomain { end_exemptions: 0 }; + /// Every row except the last `n`. + pub const fn except_last(n: usize) -> RowDomain { + RowDomain { end_exemptions: n } + } +} + +/// Per-constraint metadata, DERIVED from the body (via [`MetaBuilder`]). `Base` +/// entries MUST form a prefix of an idx-ordered, dense list — see +/// [`num_base_from_meta`]. Degree is intentionally absent: only the per-table +/// max is consumed (by `composition_poly_degree_bound`), declared once via +/// [`ConstraintSet::max_degree`]. #[derive(Clone, Debug)] pub struct ConstraintMeta { pub constraint_idx: usize, /// Base | Ext; Base entries MUST be a prefix. pub kind: RootKind, - /// Declared degree; asserted == tree-measured degree (host-side test). - pub degree: usize, /// Number of exempted rows at the end of the trace (default 0). pub end_exemptions: usize, } impl ConstraintMeta { - /// A base-field constraint with default zerofier shape (every row, no - /// exemptions). - pub fn base(constraint_idx: usize, degree: usize) -> Self { + /// A base-field constraint applying to every row. + pub fn base(constraint_idx: usize) -> Self { Self { constraint_idx, kind: RootKind::Base, - degree, end_exemptions: 0, } } - /// An extension-field (LogUp) constraint with default zerofier shape. - pub fn ext(constraint_idx: usize, degree: usize) -> Self { + /// An extension-field (LogUp) constraint applying to every row. + pub fn ext(constraint_idx: usize) -> Self { Self { kind: RootKind::Ext, - ..Self::base(constraint_idx, degree) + ..Self::base(constraint_idx) } } @@ -225,19 +254,37 @@ pub fn num_base_from_meta(meta: &[ConstraintMeta]) -> usize { num_base } -/// One table's constraints: metadata + THE single body. +/// One table's constraints: THE single body. /// -/// `meta()` and `eval` are parallel index walks that must agree entry for -/// entry: `meta()[i]` describes the constraint `eval` emits at index `i` -/// (kind, declared degree). The differential tests enforce the pairing -/// (exact-once emission, declared == measured degree); keep the two methods -/// side by side when editing a set. +/// `eval` is the sole source of truth — it emits every constraint once, +/// declaring each one's kind (via `emit_base`/`emit_ext`), degree, and +/// end-exemptions at the emit site. `meta()` is DERIVED from it by running the +/// same body through a [`MetaBuilder`], so there is no parallel list to keep in +/// sync. See [`num_base_from_meta`] for the invariants the derived metadata +/// upholds. pub trait ConstraintSet: Send + Sync { - /// Idx-ordered metadata (see [`num_base_from_meta`] for the invariants). - fn meta(&self) -> Vec; - /// The single constraint body: emits every constraint in `meta()` exactly - /// once. + /// The single constraint body: emits every constraint exactly once. fn eval>(&self, b: &mut B); + + /// The maximum multivariate degree over this set's base constraints — the + /// only degree info the proof consumes (via `composition_poly_degree_bound`, + /// which takes the per-table max). Declared once here instead of per + /// constraint; default 2 covers most tables, override to 3 for the few that + /// have a degree-3 constraint. Hand-declared, never auto-measured (that + /// would change the composition bound); the capture path asserts every + /// constraint's measured degree is `<=` this. + fn max_degree(&self) -> usize { + 2 + } + + /// Idx-ordered metadata, derived by running [`Self::eval`] through a + /// [`MetaBuilder`] (which records the `{kind, end_exemptions}` at each + /// `emit_*`). Never overridden — the body is the source. + fn meta(&self) -> Vec { + let mut mb = MetaBuilder::new(); + self.eval(&mut mb); + mb.into_meta() + } } /// A [`ConstraintSet`] with no transition constraints — for tables whose @@ -248,12 +295,114 @@ pub trait ConstraintSet: Send + Sync { pub struct EmptyConstraints; impl ConstraintSet for EmptyConstraints { - fn meta(&self) -> Vec { - Vec::new() - } fn eval>(&self, _b: &mut B) {} } +// ============================================================================= +// MetaBuilder — derive ConstraintMeta by running the body with no arithmetic +// ============================================================================= + +/// No-op expression for [`MetaBuilder`]: every leaf and operator yields `Nil`, +/// so running a constraint body over it does no field work — it only drives the +/// `emit_*` calls, which is all metadata derivation needs. +#[derive(Clone, Copy)] +pub struct Nil; + +impl core::ops::Add for Nil { + type Output = Nil; + fn add(self, _rhs: Nil) -> Nil { + Nil + } +} +impl core::ops::Sub for Nil { + type Output = Nil; + fn sub(self, _rhs: Nil) -> Nil { + Nil + } +} +impl core::ops::Mul for Nil { + type Output = Nil; + fn mul(self, _rhs: Nil) -> Nil { + Nil + } +} +impl core::ops::Neg for Nil { + type Output = Nil; + fn neg(self) -> Nil { + Nil + } +} + +/// Derives [`ConstraintMeta`] from a [`ConstraintSet`] body: a metadata-only +/// [`ConstraintBuilder`] whose leaves/operators are no-ops and whose `emit_*` +/// sinks record `{constraint_idx, kind, degree, end_exemptions}`. Runs once at +/// setup — never on the per-row prover path. +pub struct MetaBuilder { + metas: Vec, +} + +impl MetaBuilder { + pub fn new() -> Self { + Self { metas: Vec::new() } + } + + /// The recorded metadata, sorted by `constraint_idx` (emission order need + /// not match index order; the sort restores the dense idx-ordering + /// [`num_base_from_meta`] expects). + pub fn into_meta(mut self) -> Vec { + self.metas.sort_by_key(|m| m.constraint_idx); + self.metas + } +} + +impl Default for MetaBuilder { + fn default() -> Self { + Self::new() + } +} + +impl ConstraintBuilder for MetaBuilder { + type Expr = Nil; + type ExprE = Nil; + + fn main(&self, _offset: usize, _col: usize) -> Nil { + Nil + } + fn aux(&self, _offset: usize, _col: usize) -> Nil { + Nil + } + fn challenge(&self, _idx: usize) -> Nil { + Nil + } + fn alpha_pow(&self, _idx: usize) -> Nil { + Nil + } + fn table_offset(&self) -> Nil { + Nil + } + fn const_base(&self, _v: u64) -> Nil { + Nil + } + fn const_signed(&self, _v: i64) -> Nil { + Nil + } + + fn emit_base_rows(&mut self, constraint_idx: usize, rows: RowDomain, _e: Nil) { + self.metas.push(ConstraintMeta { + constraint_idx, + kind: RootKind::Base, + end_exemptions: rows.end_exemptions, + }); + } + fn emit_ext_rows(&mut self, constraint_idx: usize, rows: RowDomain, _e: Nil) { + self.metas.push(ConstraintMeta { + constraint_idx, + kind: RootKind::Ext, + end_exemptions: rows.end_exemptions, + }); + } +} + // ============================================================================= // Shared AIR plumbing: run a ConstraintSet through the folders // ============================================================================= @@ -460,11 +609,13 @@ where FieldElement::::from(v) } - fn emit_base(&mut self, constraint_idx: usize, e: FieldElement) { + #[inline] + fn emit_base_rows(&mut self, constraint_idx: usize, _rows: RowDomain, e: FieldElement) { self.tracker.mark(constraint_idx); self.base_out[constraint_idx] = e; } - fn emit_ext(&mut self, constraint_idx: usize, e: FieldElement) { + #[inline] + fn emit_ext_rows(&mut self, constraint_idx: usize, _rows: RowDomain, e: FieldElement) { debug_assert!( constraint_idx >= self.base_out.len(), "emit_ext with a base-prefix index {constraint_idx}" @@ -593,11 +744,11 @@ where FieldElement::::from(v).to_extension::() } - fn emit_base(&mut self, constraint_idx: usize, e: FieldElement) { + fn emit_base_rows(&mut self, constraint_idx: usize, _rows: RowDomain, e: FieldElement) { self.tracker.mark(constraint_idx); self.ext_out[constraint_idx] = e; } - fn emit_ext(&mut self, constraint_idx: usize, e: FieldElement) { + fn emit_ext_rows(&mut self, constraint_idx: usize, _rows: RowDomain, e: FieldElement) { self.tracker.mark(constraint_idx); self.ext_out[constraint_idx] = e; } @@ -814,13 +965,15 @@ impl ConstraintBuilder for CaptureBuilder { IrExpr::leaf(TreeKind::ConstSigned(v), Dim::Base, 0) } - fn emit_base(&mut self, constraint_idx: usize, e: IrExpr) { + fn emit_base_rows(&mut self, constraint_idx: usize, _rows: RowDomain, e: IrExpr) { debug_assert_eq!(e.0.dim, Dim::Base, "emit_base on an extension expression"); let root = self.flatten(&e); self.ir.emit(constraint_idx, root); + // Record the TREE-MEASURED degree so the host-side test can assert + // measured <= the table's declared max_degree(). self.degrees.push((constraint_idx, e.degree())); } - fn emit_ext(&mut self, constraint_idx: usize, e: IrExpr) { + fn emit_ext_rows(&mut self, constraint_idx: usize, _rows: RowDomain, e: IrExpr) { let root = self.flatten(&e); self.ir.emit(constraint_idx, root); self.degrees.push((constraint_idx, e.degree())); diff --git a/crypto/stark/src/constraints/builder_tests.rs b/crypto/stark/src/constraints/builder_tests.rs index 61b494cf2..fa6eba59c 100644 --- a/crypto/stark/src/constraints/builder_tests.rs +++ b/crypto/stark/src/constraints/builder_tests.rs @@ -18,7 +18,7 @@ use math::field::goldilocks::GoldilocksField as Fp; use crate::constraint_ir::{Dim, eval_program, eval_program_verifier}; use crate::constraints::builder::{ CaptureBuilder, ConstraintBuilder, ConstraintMeta, ConstraintSet, ProverEvalFolder, RootKind, - VerifierEvalFolder, num_base_from_meta, + RowDomain, VerifierEvalFolder, num_base_from_meta, }; use crate::frame::Frame; use crate::table::TableView; @@ -78,25 +78,20 @@ fn inv_shift_32() -> u64 { struct SampleSet; impl ConstraintSet for SampleSet { - fn meta(&self) -> Vec { - vec![ - ConstraintMeta::base(0, 2), // EqXor - ConstraintMeta::base(1, 2), // IsBit - ConstraintMeta::base(2, 3), // add carry 0 (cond-gated bit check) - ConstraintMeta::base(3, 3), // add carry 1 - ConstraintMeta::ext(4, 1), // LogUp-shaped - ] + // idx 2,3 are degree-3 carry constraints. + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { - // idx 0 — EqXor: res − (eq + invert − 2·eq·invert). + // idx 0 — EqXor (degree 2): res − (eq + invert − 2·eq·invert). let res = b.main(0, cols::RES); let eq = b.main(0, cols::EQ); let invert = b.main(0, cols::INVERT); let two = b.const_base(2); b.emit_base(0, res - (eq.clone() + invert.clone() - two * eq * invert)); - // idx 1 — IsBit: x·(1 − x). + // idx 1 — IsBit (degree 2): x·(1 − x). let x = b.main(0, cols::BIT); let one = b.one(); b.emit_base(1, x.clone() * (one - x)); @@ -116,10 +111,11 @@ impl ConstraintSet for SampleSet { let one = b.one(); let carry_0 = (lhs_lo + rhs_lo - sum_lo) * inv_2_32.clone(); let carry_1 = (lhs_hi + rhs_hi + carry_0.clone() - sum_hi) * inv_2_32; + // idx 2, 3 — degree 3 (cond·carry·(1−carry)). b.emit_base(2, cond.clone() * carry_0.clone() * (one.clone() - carry_0)); b.emit_base(3, cond * carry_1.clone() * (one - carry_1)); - // idx 4 — LogUp-shaped: (challenge₀ + aux₀)·alpha₀ − L/N. + // idx 4 — LogUp-shaped (degree 1): (challenge₀ + aux₀)·alpha₀ − L/N. let ch = b.challenge(0); let au = b.aux(0, 0); let alpha = b.alpha_pow(0); @@ -288,12 +284,12 @@ fn capture_measured_degrees_match_declared_meta() { let meta = SampleSet.meta(); assert_eq!(degrees.len(), meta.len()); + let max_degree = SampleSet.max_degree(); for (i, &(idx, measured)) in degrees.iter().enumerate() { assert_eq!(idx, i, "emit order != idx order"); - assert_eq!( - measured, meta[idx].degree, - "constraint {idx}: tree-measured degree {measured} != declared {}", - meta[idx].degree + assert!( + measured <= max_degree, + "constraint {idx}: tree-measured degree {measured} EXCEEDS max_degree() {max_degree}" ); } } @@ -303,9 +299,9 @@ fn meta_base_prefix_gives_num_base() { assert_eq!(num_base_from_meta(&SampleSet.meta()), NUM_BASE); // Pure-base and pure-ext lists. - let pure_base = vec![ConstraintMeta::base(0, 1), ConstraintMeta::base(1, 2)]; + let pure_base = vec![ConstraintMeta::base(0), ConstraintMeta::base(1)]; assert_eq!(num_base_from_meta(&pure_base), 2); - let pure_ext = vec![ConstraintMeta::ext(0, 1), ConstraintMeta::ext(1, 1)]; + let pure_ext = vec![ConstraintMeta::ext(0), ConstraintMeta::ext(1)]; assert_eq!(num_base_from_meta(&pure_ext), 0); assert_eq!(num_base_from_meta(&[]), 0); @@ -320,9 +316,9 @@ fn meta_base_prefix_gives_num_base() { #[should_panic(expected = "must form a prefix")] fn meta_base_after_ext_panics() { let bad = vec![ - ConstraintMeta::base(0, 1), - ConstraintMeta::ext(1, 1), - ConstraintMeta::base(2, 1), + ConstraintMeta::base(0), + ConstraintMeta::ext(1), + ConstraintMeta::base(2), ]; num_base_from_meta(&bad); } @@ -331,7 +327,7 @@ fn meta_base_after_ext_panics() { #[test] #[should_panic(expected = "dense and idx-ordered")] fn meta_non_dense_panics() { - let bad = vec![ConstraintMeta::base(0, 1), ConstraintMeta::base(2, 1)]; + let bad = vec![ConstraintMeta::base(0), ConstraintMeta::base(2)]; num_base_from_meta(&bad); } @@ -447,13 +443,13 @@ impl ConstraintBuilder for CountingCapture { fn const_signed(&self, v: i64) -> Self::Expr { self.inner.const_signed(v) } - fn emit_base(&mut self, constraint_idx: usize, e: Self::Expr) { + fn emit_base_rows(&mut self, constraint_idx: usize, rows: RowDomain, e: Self::Expr) { self.base_idxs.push(constraint_idx); - self.inner.emit_base(constraint_idx, e); + self.inner.emit_base_rows(constraint_idx, rows, e); } - fn emit_ext(&mut self, constraint_idx: usize, e: Self::ExprE) { + fn emit_ext_rows(&mut self, constraint_idx: usize, rows: RowDomain, e: Self::ExprE) { self.ext_idxs.push(constraint_idx); - self.inner.emit_ext(constraint_idx, e); + self.inner.emit_ext_rows(constraint_idx, rows, e); } } @@ -524,20 +520,13 @@ mod lcols { } impl ConstraintSet for NextRowLogUpSet { - fn meta(&self) -> Vec { - vec![ - ConstraintMeta::base(0, 1), - ConstraintMeta::ext(1, 1).with_end_exemptions(1), - ] - } - fn eval>(&self, b: &mut B) { - // idx 0 (base): next-row main read — main(1, VAL) − main(0, VAL). + // idx 0 (base, degree 1): next-row main read — main(1, VAL) − main(0, VAL). let cur = b.main(0, lcols::VAL); let next = b.main(1, lcols::VAL); b.emit_base(0, next - cur); - // idx 1 (ext): acc' − acc − (challenge₀·α₀ + term·α₁) + L/N, + // idx 1 (ext, degree 1, 1 end exemption): acc' − acc − (challenge₀·α₀ + term·α₁) + L/N, // with acc' read from the NEXT row (aux offset 1). let acc = b.aux(0, lcols::ACC); let acc_next = b.aux(1, lcols::ACC); @@ -546,7 +535,11 @@ impl ConstraintSet for NextRowLogUpSet { let a0 = b.alpha_pow(0); let a1 = b.alpha_pow(1); let off = b.table_offset(); - b.emit_ext(1, acc_next - acc - (ch * a0 + term * a1) + off); + b.emit_ext_rows( + 1, + RowDomain::except_last(1), + acc_next - acc - (ch * a0 + term * a1) + off, + ); } } @@ -560,8 +553,12 @@ fn next_row_aux_and_multi_alpha_folder_matches_capture() { let mut cb = CaptureBuilder::::new(); NextRowLogUpSet.eval(&mut cb); let (prog, degrees) = cb.finish(num_base); + let max_degree = NextRowLogUpSet.max_degree(); for &(idx, measured) in °rees { - assert_eq!(measured, meta[idx].degree, "constraint {idx} degree"); + assert!( + measured <= max_degree, + "constraint {idx}: tree degree {measured} EXCEEDS max_degree() {max_degree}" + ); } let mut rng = SplitMix64(0x0004_F01D_u64 ^ 0xABCD); for trial in 0..TRIALS { diff --git a/crypto/stark/src/examples/dummy_air.rs b/crypto/stark/src/examples/dummy_air.rs index e898ade9f..9decb9a53 100644 --- a/crypto/stark/src/examples/dummy_air.rs +++ b/crypto/stark/src/examples/dummy_air.rs @@ -2,7 +2,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -22,23 +22,15 @@ type StarkField = GoldilocksField; pub struct DummyConstraints; impl ConstraintSet for DummyConstraints { - fn meta(&self) -> Vec { - vec![ - // idx 0: fibonacci on column 1; reads two next rows ⇒ 2 end exemptions. - ConstraintMeta::base(0, 1).with_end_exemptions(2), - // idx 1: IS_BIT on column 0, every row. - ConstraintMeta::base(1, 2), - ] - } - fn eval>(&self, b: &mut B) { - // a_{i+2} = a_{i+1} + a_i on column 1. + // idx 0: a_{i+2} = a_{i+1} + a_i on column 1; reads two next rows ⇒ 2 + // end exemptions. let a0 = b.main(0, 1); let a1 = b.main(1, 1); let a2 = b.main(2, 1); - b.emit_base(0, a2 - a1 - a0); + b.emit_base_rows(0, RowDomain::except_last(2), a2 - a1 - a0); - // bit * (bit - 1) = 0 on column 0. + // idx 1: IS_BIT on column 0, every row. bit * (bit - 1) = 0. let bit = b.main(0, 0); let one = b.one(); b.emit_base(1, bit.clone() * (bit - one)); diff --git a/crypto/stark/src/examples/fibonacci_2_cols_shifted.rs b/crypto/stark/src/examples/fibonacci_2_cols_shifted.rs index a1b88a586..855469e4b 100644 --- a/crypto/stark/src/examples/fibonacci_2_cols_shifted.rs +++ b/crypto/stark/src/examples/fibonacci_2_cols_shifted.rs @@ -2,7 +2,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -57,25 +57,16 @@ impl ConstraintSet for Fibonacci2ColsShiftedConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - vec![ - // idx 0: Col0_{i+1} = Col1_i; reads the next row ⇒ 1 end exemption. - ConstraintMeta::base(0, 1).with_end_exemptions(1), - // idx 1: Col1_{i+1} = Col0_i + Col1_i; reads the next row ⇒ 1 end exemption. - ConstraintMeta::base(1, 1).with_end_exemptions(1), - ] - } - fn eval>(&self, b: &mut B) { let a0_0 = b.main(0, 0); let a0_1 = b.main(0, 1); let a1_0 = b.main(1, 0); let a1_1 = b.main(1, 1); - // Col0_{i+1} = Col1_i - b.emit_base(0, a1_0 - a0_1.clone()); - // Col1_{i+1} = Col0_i + Col1_i - b.emit_base(1, a1_1 - a0_0 - a0_1); + // idx 0: Col0_{i+1} = Col1_i; reads the next row ⇒ 1 end exemption. + b.emit_base_rows(0, RowDomain::except_last(1), a1_0 - a0_1.clone()); + // idx 1: Col1_{i+1} = Col0_i + Col1_i; reads the next row ⇒ 1 end exemption. + b.emit_base_rows(1, RowDomain::except_last(1), a1_1 - a0_0 - a0_1); } } diff --git a/crypto/stark/src/examples/fibonacci_2_columns.rs b/crypto/stark/src/examples/fibonacci_2_columns.rs index 0e568c1f4..beb9c999f 100644 --- a/crypto/stark/src/examples/fibonacci_2_columns.rs +++ b/crypto/stark/src/examples/fibonacci_2_columns.rs @@ -5,7 +5,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -34,25 +34,20 @@ impl ConstraintSet for Fibonacci2ColsConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - vec![ - // idx 0: s_{0, i+1} = s_{0, i} + s_{1, i}; reads the next row ⇒ 1 end exemption. - ConstraintMeta::base(0, 1).with_end_exemptions(1), - // idx 1: s_{1, i+1} = s_{1, i} + s_{0, i+1}; reads the next row ⇒ 1 end exemption. - ConstraintMeta::base(1, 1).with_end_exemptions(1), - ] - } - fn eval>(&self, b: &mut B) { let s0_0 = b.main(0, 0); let s0_1 = b.main(0, 1); let s1_0 = b.main(1, 0); let s1_1 = b.main(1, 1); - // s_{0, i+1} = s_{0, i} + s_{1, i} - b.emit_base(0, s1_0.clone() - s0_0 - s0_1.clone()); - // s_{1, i+1} = s_{1, i} + s_{0, i+1} - b.emit_base(1, s1_1 - s0_1 - s1_0); + // idx 0: s_{0, i+1} = s_{0, i} + s_{1, i}; reads the next row ⇒ 1 end exemption. + b.emit_base_rows( + 0, + RowDomain::except_last(1), + s1_0.clone() - s0_0 - s0_1.clone(), + ); + // idx 1: s_{1, i+1} = s_{1, i} + s_{0, i+1}; reads the next row ⇒ 1 end exemption. + b.emit_base_rows(1, RowDomain::except_last(1), s1_1 - s0_1 - s1_0); } } diff --git a/crypto/stark/src/examples/fibonacci_multi_column.rs b/crypto/stark/src/examples/fibonacci_multi_column.rs index d5824b3a4..ae6e61527 100644 --- a/crypto/stark/src/examples/fibonacci_multi_column.rs +++ b/crypto/stark/src/examples/fibonacci_multi_column.rs @@ -4,7 +4,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -39,21 +39,14 @@ where F: IsSubFieldOf + IsFFTField + Send + Sync, E: IsField + Send + Sync, { - fn meta(&self) -> Vec { - // idx i: column i's a_{j+2} = a_{j+1} + a_j; reads two next rows ⇒ 2 - // end exemptions. - (0..self.num_columns) - .map(|i| ConstraintMeta::base(i, 1).with_end_exemptions(2)) - .collect() - } - fn eval>(&self, b: &mut B) { for col in 0..self.num_columns { let a0 = b.main(0, col); let a1 = b.main(1, col); let a2 = b.main(2, col); - // Constraint: a2 = a1 + a0 => a2 - a1 - a0 = 0 - b.emit_base(col, a2 - a1 - a0); + // idx col: column col's a_{j+2} = a_{j+1} + a_j; reads two next rows + // ⇒ 2 end exemptions. + b.emit_base_rows(col, RowDomain::except_last(2), a2 - a1 - a0); } } } diff --git a/crypto/stark/src/examples/fibonacci_rap.rs b/crypto/stark/src/examples/fibonacci_rap.rs index e32709caf..22003952d 100644 --- a/crypto/stark/src/examples/fibonacci_rap.rs +++ b/crypto/stark/src/examples/fibonacci_rap.rs @@ -4,7 +4,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -39,31 +39,24 @@ impl ConstraintSet for FibonacciRAPConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - vec![ - // idx 0: fibonacci; end exemptions hard-coded for the steps = 16 - // integration tests. - ConstraintMeta::base(0, 1).with_end_exemptions(3 + 32 - 16 - 1), - // idx 1: permutation; reads the next row ⇒ 1 end exemption. - ConstraintMeta::ext(1, 2).with_end_exemptions(1), - ] - } - fn eval>(&self, b: &mut B) { - // a_{i+2} = a_{i+1} + a_i on column 0. + // idx 0: a_{i+2} = a_{i+1} + a_i on column 0. End exemptions hard-coded + // for the steps = 16 integration tests. let a0 = b.main(0, 0); let a1 = b.main(1, 0); let a2 = b.main(2, 0); - b.emit_base(0, a2 - a1 - a0); + b.emit_base_rows(0, RowDomain::except_last(3 + 32 - 16 - 1), a2 - a1 - a0); - // z_{i+1} * (b_i + gamma) = z_i * (a_i + gamma) + // idx 1: permutation; z_{i+1} * (b_i + gamma) = z_i * (a_i + gamma); + // reads the next row ⇒ 1 end exemption. let z_i = b.aux(0, 0); let z_i_plus_one = b.aux(1, 0); let gamma = b.challenge(0); let a_i = b.main(0, 0); let b_i = b.main(0, 1); - b.emit_ext( + b.emit_ext_rows( 1, + RowDomain::except_last(1), z_i_plus_one * (b_i + gamma.clone()) - z_i * (a_i + gamma), ); } diff --git a/crypto/stark/src/examples/quadratic_air.rs b/crypto/stark/src/examples/quadratic_air.rs index 4818baed1..aedaf1d72 100644 --- a/crypto/stark/src/examples/quadratic_air.rs +++ b/crypto/stark/src/examples/quadratic_air.rs @@ -4,7 +4,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -33,15 +33,11 @@ impl ConstraintSet for QuadraticConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - // idx 0: x_{i+1} = x_i²; reads the next row ⇒ 1 end exemption. - vec![ConstraintMeta::base(0, 2).with_end_exemptions(1)] - } - fn eval>(&self, b: &mut B) { let x = b.main(0, 0); let x_squared = b.main(1, 0); - b.emit_base(0, x_squared - x.clone() * x); + // idx 0: x_{i+1} = x_i²; reads the next row ⇒ 1 end exemption. + b.emit_base_rows(0, RowDomain::except_last(1), x_squared - x.clone() * x); } } diff --git a/crypto/stark/src/examples/read_only_memory.rs b/crypto/stark/src/examples/read_only_memory.rs index dd74a1b37..521bd7ca9 100644 --- a/crypto/stark/src/examples/read_only_memory.rs +++ b/crypto/stark/src/examples/read_only_memory.rs @@ -4,7 +4,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -31,15 +31,6 @@ impl ConstraintSet for ReadOnlyRAPConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - // All three read the next row ⇒ 1 end exemption each. - vec![ - ConstraintMeta::base(0, 2).with_end_exemptions(1), // continuity - ConstraintMeta::base(1, 2).with_end_exemptions(1), // single value - ConstraintMeta::ext(2, 2).with_end_exemptions(1), // permutation - ] - } - fn eval>(&self, b: &mut B) { let a_sorted_0 = b.main(0, 2); let a_sorted_1 = b.main(1, 2); @@ -48,10 +39,19 @@ where let one = b.one(); let addr_diff = a_sorted_1 - a_sorted_0; - // (a'_{i+1} - a'_i)(a'_{i+1} - a'_i - 1) = 0 where a' is the sorted address - b.emit_base(0, addr_diff.clone() * (addr_diff.clone() - one.clone())); - // (v'_{i+1} - v'_i) * (a'_{i+1} - a'_i - 1) = 0 - b.emit_base(1, (v_sorted_1 - v_sorted_0) * (addr_diff - one)); + // All three read the next row ⇒ degree 2, 1 end exemption each. + // idx 0 — continuity: (a'_{i+1} - a'_i)(a'_{i+1} - a'_i - 1) = 0 where a' is the sorted address + b.emit_base_rows( + 0, + RowDomain::except_last(1), + addr_diff.clone() * (addr_diff.clone() - one.clone()), + ); + // idx 1 — single value: (v'_{i+1} - v'_i) * (a'_{i+1} - a'_i - 1) = 0 + b.emit_base_rows( + 1, + RowDomain::except_last(1), + (v_sorted_1 - v_sorted_0) * (addr_diff - one), + ); // (z - (a'_{i+1} + α * v'_{i+1})) * p_{i+1} = (z - (a_{i+1} + α * v_{i+1})) * p_i let p0 = b.aux(0, 0); @@ -64,7 +64,12 @@ where let v_sorted_1 = b.main(1, 3); let sorted_fp = z.clone() - (a_sorted_1 + v_sorted_1 * alpha.clone()); let unsorted_fp = z - (a1 + v1 * alpha); - b.emit_ext(2, sorted_fp * p1 - unsorted_fp * p0); + // idx 2 — permutation (degree 2, 1 end exemption). + b.emit_ext_rows( + 2, + RowDomain::except_last(1), + sorted_fp * p1 - unsorted_fp * p0, + ); } } diff --git a/crypto/stark/src/examples/read_only_memory_logup.rs b/crypto/stark/src/examples/read_only_memory_logup.rs index 2ad9a28c3..5090098bd 100644 --- a/crypto/stark/src/examples/read_only_memory_logup.rs +++ b/crypto/stark/src/examples/read_only_memory_logup.rs @@ -8,7 +8,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -39,15 +39,6 @@ where F: IsFFTField + IsSubFieldOf + Send + Sync, E: IsField + Send + Sync, { - fn meta(&self) -> Vec { - // All three read the next row ⇒ 1 end exemption each. - vec![ - ConstraintMeta::base(0, 2).with_end_exemptions(1), // continuity - ConstraintMeta::base(1, 2).with_end_exemptions(1), // single value - ConstraintMeta::ext(2, 3).with_end_exemptions(1), // LogUp permutation - ] - } - fn eval>(&self, b: &mut B) { let a_sorted_0 = b.main(0, 2); let a_sorted_1 = b.main(1, 2); @@ -56,10 +47,19 @@ where let one = b.one(); let addr_diff = a_sorted_1 - a_sorted_0; - // (a'_{i+1} - a'_i)(a'_{i+1} - a'_i - 1) = 0 where a' is the sorted address - b.emit_base(0, addr_diff.clone() * (addr_diff.clone() - one.clone())); - // (v'_{i+1} - v'_i) * (a'_{i+1} - a'_i - 1) = 0 - b.emit_base(1, (v_sorted_1 - v_sorted_0) * (addr_diff - one)); + // All three read the next row ⇒ 1 end exemption each. + // idx 0 — continuity (degree 2): (a'_{i+1} - a'_i)(a'_{i+1} - a'_i - 1) = 0 where a' is the sorted address + b.emit_base_rows( + 0, + RowDomain::except_last(1), + addr_diff.clone() * (addr_diff.clone() - one.clone()), + ); + // idx 1 — single value (degree 2): (v'_{i+1} - v'_i) * (a'_{i+1} - a'_i - 1) = 0 + b.emit_base_rows( + 1, + RowDomain::except_last(1), + (v_sorted_1 - v_sorted_0) * (addr_diff - one), + ); // We are using the following LogUp equation: // s1 = s0 + m / sorted_term - 1/unsorted_term. @@ -76,8 +76,10 @@ where let m = b.main(1, 4); let unsorted_term = -(a1 + v1 * alpha.clone()) + z.clone(); let sorted_term = -(a_sorted_1 + v_sorted_1 * alpha) + z; - b.emit_ext( + // idx 2 — LogUp permutation (degree 3, 1 end exemption). + b.emit_ext_rows( 2, + RowDomain::except_last(1), s0 * unsorted_term.clone() * sorted_term.clone() + m * unsorted_term.clone() - sorted_term.clone() - s1 * unsorted_term * sorted_term, diff --git a/crypto/stark/src/examples/simple_addition.rs b/crypto/stark/src/examples/simple_addition.rs index c9eb019ff..d064acd55 100644 --- a/crypto/stark/src/examples/simple_addition.rs +++ b/crypto/stark/src/examples/simple_addition.rs @@ -36,16 +36,11 @@ impl ConstraintSet for SimpleAdditionConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - // idx 0: col0 + col1 = col2, applied at every row (no exemptions). - vec![ConstraintMeta::base(0, 1)] - } - fn eval>(&self, b: &mut B) { let col0 = b.main(0, 0); let col1 = b.main(0, 1); let col2 = b.main(0, 2); - // Constraint: col0 + col1 - col2 = 0 + // idx 0: col0 + col1 - col2 = 0, applied at every row (degree 1, no exemptions). b.emit_base(0, col0 + col1 - col2); } } diff --git a/crypto/stark/src/examples/simple_fibonacci.rs b/crypto/stark/src/examples/simple_fibonacci.rs index bcb5ff5b6..db84ab439 100644 --- a/crypto/stark/src/examples/simple_fibonacci.rs +++ b/crypto/stark/src/examples/simple_fibonacci.rs @@ -2,7 +2,7 @@ use crate::{ constraints::{ boundary::{BoundaryConstraint, BoundaryConstraints}, builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, num_base_from_meta, + ConstraintBuilder, ConstraintMeta, ConstraintSet, RowDomain, num_base_from_meta, run_transition_prover, run_transition_verifier, }, }, @@ -32,16 +32,12 @@ impl ConstraintSet for SimpleFibonacciConstraints where F: IsFFTField + Send + Sync, { - fn meta(&self) -> Vec { - // idx 0: a_{i+2} = a_{i+1} + a_i; reads two next rows ⇒ 2 end exemptions. - vec![ConstraintMeta::base(0, 1).with_end_exemptions(2)] - } - fn eval>(&self, b: &mut B) { let a0 = b.main(0, 0); let a1 = b.main(1, 0); let a2 = b.main(2, 0); - b.emit_base(0, a2 - a1 - a0); + // idx 0: a_{i+2} = a_{i+1} + a_i; reads two next rows ⇒ 2 end exemptions. + b.emit_base_rows(0, RowDomain::except_last(2), a2 - a1 - a0); } } diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index f06d45e01..cd41ac15a 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -825,8 +825,9 @@ pub struct AirWithBuses< /// The LogUp layout: the framework generates the LogUp (extension) /// constraints from this and appends them after the `constraint_set` ones. logup: LogUpLayout, - /// Idx-ordered metadata for all transition constraints: - /// `constraint_set.meta()` (base prefix) followed by `logup_meta` (ext). + /// Idx-ordered metadata for all transition constraints, DERIVED at + /// construction: `constraint_set.meta()` (base prefix) followed by the + /// LogUp emission's derived metadata (ext). meta: Vec, /// Number of base-field constraints (the `RootKind::Base` prefix length of /// `meta`) — these use the cheaper F×E accumulation path. @@ -879,12 +880,16 @@ impl< let logup = LogUpLayout::from_interactions(auxiliary_trace_build_data.interactions.clone()); let num_term_columns = logup.num_term_columns; - // meta = constraint_set base-prefix meta + appended LogUp ext meta. + // meta = constraint_set base-prefix meta + appended LogUp ext meta, + // both DERIVED by running the respective bodies through a MetaBuilder + // (the `{degree, end_exemptions}` declared at each emit). let mut meta = constraint_set.meta(); let num_base = num_base_from_meta(&meta); // The set is entirely base-field (its meta is a Base prefix). debug_assert_eq!(num_base, meta.len(), "constraint set meta must be all-base"); - meta.extend(logup_meta(&logup, meta.len())); + let mut logup_mb = crate::constraints::builder::MetaBuilder::new(); + emit_logup_constraints::(&mut logup_mb, &logup, num_base); + meta.extend(logup_mb.into_meta()); // Layout: num_committed_pairs term columns + 1 accumulated = ⌈N/2⌉ let num_aux_columns = if num_interactions > 0 { @@ -1007,7 +1012,14 @@ where } fn composition_poly_degree_bound(&self, trace_length: usize) -> usize { - let max_degree = self.meta.iter().map(|m| m.degree).max().unwrap_or(1); + // Only the per-table MAX degree is consumed. Base constraints declare it + // once via `ConstraintSet::max_degree()`; the framework's LogUp + // constraints contribute their own known max (batched terms degree 3, + // accumulator `1 + absorbed`). + let max_degree = self + .constraint_set + .max_degree() + .max(logup_max_degree(&self.logup)); // The composition polynomial is the constraint QUOTIENT H = Σ βᵢ·Cᵢ/Zᵢ. Its degree is // deg(Cᵢ) − deg(Zᵢ) = (max_degree−1)·N − max_degree + eᵢ, so with the end-exemptions // eᵢ < max_degree (the max-degree LogUp constraints have eᵢ = 0) it fits in @@ -1729,7 +1741,8 @@ where // accumulated); there are no per-constraint objects. // // All LogUp constraints use the default zerofier shape (every row, no -// exemptions), so [`logup_meta`] emits plain [`RootKind::Ext`] entries. +// exemptions) and are [`RootKind::Ext`]; their metadata is derived from this +// same emission (via `MetaBuilder`), not hand-listed. // // The data-dependent "skip the multiply when the row value is zero" // optimization IS reproduced, through the [`ConstraintBuilder::fold_fingerprint_term`] @@ -1744,7 +1757,7 @@ use crate::constraints::builder::ConstraintBuilder; /// computed by [`AirWithBuses::new`] from the interaction list (via /// `split_interactions`). This is the plain-data source for the LogUp /// constraints: [`emit_logup_constraints`] reads it to generate every LogUp -/// constraint, and [`logup_meta`] reads it for the metadata. +/// constraint (its metadata is derived from that same emission). #[derive(Clone)] pub struct LogUpLayout { /// All interactions, in the order they were registered. The first @@ -2042,7 +2055,8 @@ where -term_b }; - // c · fp_a · fp_b: c is aux (ext), so this is ext throughout. + // c · fp_a · fp_b: c is aux (ext), so this is ext throughout (degree 3; + // see `logup_max_degree`). let main = c * fp_a * fp_b; b.emit_ext(idx, main - term_a - term_b); } @@ -2097,9 +2111,28 @@ where _ => unreachable!("absorbed must contain 1 or 2 interactions"), }; + // Degree 1 + absorbed count (2 for one absorbed, 3 for two); folded into + // the composition bound via `logup_max_degree`. b.emit_ext(idx, root); } +/// The maximum degree among a layout's framework-generated LogUp constraints: +/// batched committed terms are degree 3, the accumulator is `1 + absorbed`. +/// Zero when there are no interactions. Folded into +/// `composition_poly_degree_bound` alongside the base constraints' max_degree. +pub fn logup_max_degree(layout: &LogUpLayout) -> usize { + if layout.interactions.is_empty() { + return 0; + } + // Accumulated constraint: 1 + number of absorbed interactions. + let mut m = 1 + layout.absorbed().len(); + // Batched committed terms (if any) are degree 3. + if layout.num_committed_pairs > 0 { + m = m.max(3); + } + m +} + /// Emit every LogUp transition constraint for `layout` through the builder, /// starting at absolute constraint index `idx_base` (the table's base-constraint /// count). Committed batched terms come first (one per committed pair), then the @@ -2121,26 +2154,6 @@ where emit_logup_accumulated::(b, layout, idx); } -/// The idx-ordered [`ConstraintMeta`] for `layout`'s LogUp constraints, starting -/// at `idx_start`: batched terms are degree 3; the accumulated constraint is -/// degree `1 + absorbed.len()` (2 for one absorbed, 3 for two). All are -/// [`RootKind::Ext`] with the default zerofier shape (period 1, offset 0, no -/// exemptions). -pub fn logup_meta(layout: &LogUpLayout, idx_start: usize) -> Vec { - let mut meta = Vec::with_capacity(layout.num_constraints()); - if layout.interactions.is_empty() { - return meta; - } - let mut idx = idx_start; - for _ in 0..layout.num_committed_pairs { - meta.push(ConstraintMeta::ext(idx, 3)); // c · fp_a · fp_b - idx += 1; - } - let absorbed_len = layout.absorbed().len(); - meta.push(ConstraintMeta::ext(idx, 1 + absorbed_len)); - meta -} - /// Run an [`AirWithBuses`] table's transition constraints through the /// [`ProverEvalFolder`] in ONE pass: the constraint set's base-field body /// followed by the appended LogUp constraints (idx offset by `num_base`, the @@ -2277,24 +2290,25 @@ mod logup_single_source_tests { let n_base = 0usize; // LogUp constraints are all extension-rooted. let n = layout.num_constraints(); - // Metadata self-consistency: all-ext, dense, and the batched/accumulated - // degree formula (3 per batched term; 1 + absorbed for the accumulator). - let meta = logup_meta(layout, n_base); + // Metadata self-consistency: derived from the LogUp emission itself + // (MetaBuilder), it must be all-ext, dense, and match the + // batched/accumulated degree formula (3 per batched term; 1 + absorbed + // for the accumulator). + let meta = { + let mut mb = crate::constraints::builder::MetaBuilder::new(); + emit_logup_constraints::(&mut mb, layout, n_base); + mb.into_meta() + }; assert_eq!(meta.len(), n, "[{label}] meta count"); let num_base = num_base_from_meta(&meta); assert_eq!(num_base, 0, "[{label}] LogUp meta is all-ext"); for (i, m) in meta.iter().enumerate() { assert_eq!(m.constraint_idx, i, "[{label}] meta idx {i}"); assert_eq!(m.kind, RootKind::Ext, "[{label}] meta kind {i}"); - let expected_degree = if i < layout.num_committed_pairs { - 3 - } else { - 1 + layout.absorbed().len() - }; - assert_eq!(m.degree, expected_degree, "[{label}] degree {i}"); } - // Capture once; tree-measured degree <= declared. + // Capture once; the tree-measured degree must match the batched/ + // accumulated formula, and `logup_max_degree` must equal their max. let mut cb = CaptureBuilder::::new(); emit_logup_constraints(&mut cb, layout, n_base); let (prog, degrees) = cb.finish(num_base); @@ -2309,12 +2323,18 @@ mod logup_single_source_tests { "[{label}] emitted constraint indices are not exactly 0..{n}: {emitted:?}" ); for &(idx, measured) in °rees { - assert!( - measured <= meta[idx].degree, - "[{label}] constraint {idx}: tree degree {measured} exceeds declared {}", - meta[idx].degree - ); + let expected_degree = if idx < layout.num_committed_pairs { + 3 + } else { + 1 + layout.absorbed().len() + }; + assert_eq!(measured, expected_degree, "[{label}] degree {idx}"); } + assert_eq!( + logup_max_degree(layout), + degrees.iter().map(|&(_, d)| d).max().unwrap_or(0), + "[{label}] logup_max_degree matches max measured degree" + ); let n_aux = num_aux_cols(layout); diff --git a/prover/src/constraints/cpu.rs b/prover/src/constraints/cpu.rs index f27070193..917445b7e 100644 --- a/prover/src/constraints/cpu.rs +++ b/prover/src/constraints/cpu.rs @@ -66,9 +66,9 @@ pub const NUM_CPU_CONSTRAINTS: usize = 12 + 6 + 2 + 2 + 2 + 4 + 2 + 2 + 1 + 2 + // compiled prover folder, the verifier folder and IR capture. All constraints // here use the default zerofier shape (every row, no exemptions). -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; -use super::templates::{INV_SHIFT_32, add_pair_meta, emit_add_pair, emit_is_bit, is_bit_meta}; +use super::templates::{INV_SHIFT_32, emit_add_pair, emit_is_bit}; /// `col_a · col_b = 0`. pub fn emit_product_zero>( @@ -81,11 +81,6 @@ pub fn emit_product_zero ConstraintMeta { - ConstraintMeta::base(idx, 2) -} - /// `(1 − MEMORY − BRANCH) · read_register2 · imm[i] = 0`. pub fn emit_arg2_exclusive>( b: &mut B, @@ -100,11 +95,6 @@ pub fn emit_arg2_exclusive ConstraintMeta { - ConstraintMeta::base(idx, 3) -} - /// `(1 − MEMORY) · mem_flags · (1 − mem_flags) = 0`. pub fn emit_mem_flags_bit>( b: &mut B, @@ -119,11 +109,6 @@ pub fn emit_mem_flags_bit ConstraintMeta { - ConstraintMeta::base(idx, 3) -} - /// `(1 − flag) · value = 0`. pub fn emit_reg_not_read_is_zero>( b: &mut B, @@ -137,11 +122,6 @@ pub fn emit_reg_not_read_is_zero ConstraintMeta { - ConstraintMeta::base(idx, 2) -} - /// `arg2` multiplex for word index `word_idx ∈ {0, 1}`: /// /// ```text @@ -167,15 +147,10 @@ pub fn emit_arg2>( let expected = memory.clone() * imm.clone() + branch.clone() * rv2.clone() + (one - memory - branch) * (rv2 + imm); + // Degree 2 relies on the live `MEMORY·BRANCH = 0` mutex. b.emit_base(idx, arg2 - expected); } -/// Metadata for [`emit_arg2`] (degree 2 relies on the live `MEMORY·BRANCH = 0` -/// mutex). -pub fn arg2_meta(idx: usize) -> ConstraintMeta { - ConstraintMeta::base(idx, 2) -} - /// `cast(res, DWordWL)` word from the four `res` halves (DWordHL). fn res_word_expr>( b: &B, @@ -205,11 +180,6 @@ pub fn emit_rvd_eq_res ConstraintMeta { - ConstraintMeta::base(idx, 2) -} - /// The `pc + instruction_length` carry pair against a destination dword /// (`rvd` or `next_pc`), gated by `gate`; shared body of /// [`emit_branch_rvd_pair`] and [`emit_next_pc_add_pair`]: @@ -236,6 +206,7 @@ fn emit_pc_len_add_pair [ConstraintMeta; 2] { - [ - ConstraintMeta::base(idx, 3), - ConstraintMeta::base(idx + 1, 3), - ] -} - /// `branch_cond − (BRANCH·JALR + BRANCH·(1−JALR)·res[0])`. pub fn emit_branch_cond>( b: &mut B, @@ -278,11 +241,6 @@ pub fn emit_branch_cond ConstraintMeta { - ConstraintMeta::base(idx, 3) -} - /// `(1 − branch_cond) · carry · (1 − carry) = 0` for /// `next_pc = pc + instruction_length` (two instances at `idx`, `idx + 1`). pub fn emit_next_pc_add_pair>( @@ -295,14 +253,6 @@ pub fn emit_next_pc_add_pair [ConstraintMeta; 2] { - [ - ConstraintMeta::base(idx, 3), - ConstraintMeta::base(idx + 1, 3), - ] -} - // ========================================================================= // Single-source constraint set (ConstraintBuilder front-end) // ========================================================================= @@ -326,62 +276,10 @@ pub fn next_pc_add_meta(idx: usize) -> [ConstraintMeta; 2] { pub struct CpuConstraints; impl ConstraintSet for CpuConstraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(NUM_CPU_CONSTRAINTS); - // idx 0..11: IS_BIT on each BIT_FLAG_COLUMNS entry (unconditional). - for i in 0..BIT_FLAG_COLUMNS.len() { - m.push(is_bit_meta(i, false)); - } - let mut idx = BIT_FLAG_COLUMNS.len(); - // idx 12,13: ADD pair (conditional on ADD). - m.extend(add_pair_meta(idx, true)); - idx += 2; - // idx 14,15: SUB pair (conditional on SUB). - m.extend(add_pair_meta(idx, true)); - idx += 2; - // idx 16..21: word_instr mutexes + register-read gates. - for _ in 0..6 { - m.push(product_zero_meta(idx)); - idx += 1; - } - // idx 22,23: arg2 multiplex. - m.push(arg2_meta(idx)); - idx += 1; - m.push(arg2_meta(idx)); - idx += 1; - // idx 24..27: register zero-forcing. - for _ in 0..4 { - m.push(reg_not_read_is_zero_meta(idx)); - idx += 1; - } - // idx 28,29: rvd = cast(res, WL). - m.push(rvd_eq_res_meta(idx)); - idx += 1; - m.push(rvd_eq_res_meta(idx)); - idx += 1; - // idx 30,31: branch rvd = pc + len. - m.extend(branch_rvd_meta(idx)); - idx += 2; - // idx 32: branch_cond. - m.push(branch_cond_meta(idx)); - idx += 1; - // idx 33,34: next_pc = pc + len. - m.extend(next_pc_add_meta(idx)); - idx += 2; - // idx 35: MEMORY · BRANCH = 0. - m.push(product_zero_meta(idx)); - idx += 1; - // idx 36,37: arg2 exclusivity. - m.push(arg2_exclusive_meta(idx)); - idx += 1; - m.push(arg2_exclusive_meta(idx)); - idx += 1; - // idx 38: IS_BIT(mem_flags) on non-MEMORY rows. - m.push(mem_flags_bit_meta(idx)); - idx += 1; - debug_assert_eq!(idx, NUM_CPU_CONSTRAINTS); - debug_assert_eq!(m.len(), NUM_CPU_CONSTRAINTS); - m + // The conditional ADD/SUB carry pairs, arg2 exclusivity, mem-flags bit and + // branch constraints are degree 3. + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/constraints/templates.rs b/prover/src/constraints/templates.rs index f8f0ec0ea..04932eab8 100644 --- a/prover/src/constraints/templates.rs +++ b/prover/src/constraints/templates.rs @@ -252,7 +252,7 @@ impl AddOperand { // zerofier shape — none of these templates override period/offset/ // exemptions). -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta}; +use stark::constraints::builder::ConstraintBuilder; /// IS_BIT: `x·(1−x)`, optionally gated by a condition column: /// `cond·x·(1−x)`. @@ -274,11 +274,6 @@ pub fn emit_is_bit>( b.emit_base(idx, root); } -/// Metadata for [`emit_is_bit`]: degree 3 gated, 2 ungated. -pub fn is_bit_meta(idx: usize, conditional: bool) -> ConstraintMeta { - ConstraintMeta::base(idx, if conditional { 3 } else { 2 }) -} - /// One [`AddLinearTerm`]: `column · coefficient` or a constant. fn add_term_expr>( b: &B, @@ -377,13 +372,3 @@ pub fn emit_add_pair> let root_1 = bit(b, c1, carry_1); b.emit_base(idx + 1, root_1); } - -/// Metadata for [`emit_add_pair`]: two constraints at `idx`, `idx + 1`; -/// degree 3 gated, 2 ungated. -pub fn add_pair_meta(idx: usize, conditional: bool) -> [ConstraintMeta; 2] { - let degree = if conditional { 3 } else { 2 }; - [ - ConstraintMeta::base(idx, degree), - ConstraintMeta::base(idx + 1, degree), - ] -} diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 48f963fac..77092d0e4 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -42,9 +42,7 @@ use executor::vm::execution::Executor; use executor::vm::memory::MAX_PRIVATE_INPUT_SIZE; use math::field::element::FieldElement; use stark::config::Commitment; -use stark::constraints::builder::{ - ConstraintBuilder, ConstraintMeta, ConstraintSet, EmptyConstraints, -}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet, EmptyConstraints}; use stark::lookup::{AirWithBuses, AuxiliaryTraceBuildData, NullBoundaryConstraintBuilder}; use stark::proof::options::ProofOptions; use stark::proof::stark::MultiProof; @@ -115,10 +113,6 @@ fn global_transcript(elf_bytes: &[u8], num_epochs: usize) -> DefaultTranscript for L2gMemoryConstraints { - fn meta(&self) -> Vec { - // IS_BIT(MU), unconditional → degree 2. - vec![ConstraintMeta::base(0, 2)] - } fn eval>(&self, b: &mut B) { crate::constraints::templates::emit_is_bit(b, 0, local_to_global::cols::MU, None); } diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index d45618329..d4baf10c5 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -26,7 +26,7 @@ //! - Sender: IS_HALFWORD (×3 for next_pc_high[0..3]) //! - Receiver: BRANCH (provides branch targets to CPU) -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; @@ -413,14 +413,8 @@ fn carry_1_expr>( pub struct BranchConstraints; impl ConstraintSet for BranchConstraints { - fn meta(&self) -> Vec { - vec![ - ConstraintMeta::base(0, 3), // PcCarry0IsBit - ConstraintMeta::base(1, 3), // PcCarry1IsBit - ConstraintMeta::base(2, 3), // RegCarry0IsBit - ConstraintMeta::base(3, 3), // RegCarry1IsBit - ConstraintMeta::base(4, 2), // JalrIsBit - ] + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/commit.rs b/prover/src/tables/commit.rs index ce27d5d80..cd1ca264b 100644 --- a/prover/src/tables/commit.rs +++ b/prover/src/tables/commit.rs @@ -46,11 +46,9 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; -use crate::constraints::templates::{ - AddOperand, add_pair_meta, emit_add_pair, emit_is_bit, is_bit_meta, -}; +use crate::constraints::templates::{AddOperand, emit_add_pair, emit_is_bit}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; @@ -737,18 +735,6 @@ pub fn bus_interactions() -> Vec { pub struct CommitConstraints; impl ConstraintSet for CommitConstraints { - fn meta(&self) -> Vec { - let mut m = vec![ - is_bit_meta(0, false), // first - is_bit_meta(1, false), // end - is_bit_meta(2, false), // μ - ConstraintMeta::base(3, 2), // (first + end)·(1 − μ) - ]; - m.extend(add_pair_meta(4, false)); // idx 4,5: address + 1 = address_incr - m.extend(add_pair_meta(6, false)); // idx 6,7: count_decr + 1 = count - m - } - fn eval>(&self, b: &mut B) { // idx 0-2: IS_BIT for first, end, mu emit_is_bit(b, 0, cols::FIRST, None); diff --git a/prover/src/tables/cpu32.rs b/prover/src/tables/cpu32.rs index 3786228ae..e0931ff3a 100644 --- a/prover/src/tables/cpu32.rs +++ b/prover/src/tables/cpu32.rs @@ -24,11 +24,9 @@ use super::types::{ BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_16, VmTable, alu_op, packed_decode_shrunk, }; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; -use crate::constraints::templates::{ - AddOperand, add_pair_meta, emit_add_pair, emit_is_bit, is_bit_meta, -}; +use crate::constraints::templates::{AddOperand, emit_add_pair, emit_is_bit}; // ========================================================================= // Column indices for CPU32 table @@ -602,29 +600,8 @@ pub fn bus_interactions() -> Vec { pub struct Cpu32Constraints; impl ConstraintSet for Cpu32Constraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(32); - // idx 0-6: IS_BIT (unconditional, degree 2). - for i in 0..7 { - m.push(is_bit_meta(i, false)); - } - // idx 7,8: ADD pair gated on ADD (conditional, degree 3). - m.extend(add_pair_meta(7, true)); - // idx 9,10: SUB pair gated on SUB (conditional, degree 3). - m.extend(add_pair_meta(9, true)); - // idx 11-16: RegZero (degree 2). - for i in 11..17 { - m.push(ConstraintMeta::base(i, 2)); - } - // idx 17-22: sign-extension arithmetic (linear, degree 1). - for i in 17..23 { - m.push(ConstraintMeta::base(i, 1)); - } - // idx 23-31: sign-zero, arg2-exclusive, flag ⇒ μ (all degree 2). - for i in 23..32 { - m.push(ConstraintMeta::base(i, 2)); - } - m + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/dvrm.rs b/prover/src/tables/dvrm.rs index 4a6f3d75b..032963c82 100644 --- a/prover/src/tables/dvrm.rs +++ b/prover/src/tables/dvrm.rs @@ -976,7 +976,7 @@ pub fn bus_interactions() -> Vec { // One body against the generic `ConstraintBuilder` serves the compiled prover // folder, the verifier folder and IR capture. Constraint indices 0..19. -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// DVRM table constraints as a single-source [`ConstraintSet`]. No column /// configuration is needed (the DVRM layout is fixed via `cols`). @@ -1059,11 +1059,6 @@ impl DvrmConstraints { } impl ConstraintSet for DvrmConstraints { - fn meta(&self) -> Vec { - // All DVRM constraints are declared degree 2. - (0..19).map(|i| ConstraintMeta::base(i, 2)).collect() - } - fn eval>(&self, b: &mut B) { // idx 0: SignedIsBit — signed * (1 - signed) let signed = b.main(0, cols::SIGNED); diff --git a/prover/src/tables/ec_scalar.rs b/prover/src/tables/ec_scalar.rs index da3eecf04..5589a14e5 100644 --- a/prover/src/tables/ec_scalar.rs +++ b/prover/src/tables/ec_scalar.rs @@ -276,18 +276,13 @@ pub fn bus_interactions() -> Vec { // 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, ConstraintMeta, ConstraintSet}; +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 meta(&self) -> Vec { - // 10 unconditional IS_BIT (degree 2) + 10 MulZero (degree 2). - (0..20).map(|i| ConstraintMeta::base(i, 2)).collect() - } - 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 diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index 8b30fbe08..26bbe44e4 100644 --- a/prover/src/tables/ecdas.rs +++ b/prover/src/tables/ecdas.rs @@ -269,7 +269,7 @@ pub enum Relation { // 4 : NEXT_OP · (1 − MU) // then for (Lambda,C0),(Xr,C1),(Yr,C2): 64 ConvCarry (i=0..64) + 1 ColIsZero. -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// ECDAS transition constraints as a single-source [`ConstraintSet`] (200 /// total). No column configuration needed (the layout is fixed via `cols`). @@ -405,31 +405,9 @@ impl EcdasConstraints { } impl ConstraintSet for EcdasConstraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(200); - // idx 0,1,2: IS_BIT(MU/OP/NEXT_OP), degree 2. - for i in 0..3 { - m.push(ConstraintMeta::base(i, 2)); - } - // idx 3: OP·NEXT_OP, idx 4: NEXT_OP·(1−MU) — degree 2. - m.push(ConstraintMeta::base(3, 2)); - m.push(ConstraintMeta::base(4, 2)); - // Per relation: 64 ConvCarry + 1 ColIsZero. - let mut idx = 5; - for relation in [Relation::Lambda, Relation::Xr, Relation::Yr] { - let conv_degree = match relation { - Relation::Lambda => 3, // op · (λ · Δx) - Relation::Xr | Relation::Yr => 2, - }; - for _ in 0..64 { - m.push(ConstraintMeta::base(idx, conv_degree)); - idx += 1; - } - m.push(ConstraintMeta::base(idx, 1)); // ColIsZero c_63 - idx += 1; - } - debug_assert_eq!(m.len(), 200); - m + // The Lambda ConvCarry has the op·(λ·Δx) term, making it degree 3. + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { @@ -464,7 +442,7 @@ impl ConstraintSet for EcdasConstraints { idx += 1; } let c_last = b.main(0, c_base + 63); - b.emit_base(idx, c_last); + b.emit_base(idx, c_last); // ColIsZero c_63 idx += 1; } } diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index cc87224e4..0dba13910 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -641,7 +641,7 @@ impl OverflowKind { // 140..147 : CarryBit(XrLtP, 0..7) // 147 : OverflowRequired(XrLtP) -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// ECSM transition constraints as a single-source [`ConstraintSet`] (148 /// total). No column configuration needed (the layout is fixed via `cols`). @@ -760,54 +760,20 @@ impl EcsmConstraints { } impl ConstraintSet for EcsmConstraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(148); - m.push(ConstraintMeta::base(0, 2)); // IS_BIT(MU) - let mut idx = 1; - // X2 convolution: 64 carries (deg 2) + closing (deg 1). - for _ in 0..64 { - m.push(ConstraintMeta::base(idx, 2)); - idx += 1; - } - m.push(ConstraintMeta::base(idx, 1)); - idx += 1; - // Yg convolution: 64 carries (deg 2) + closing (deg 1). - for _ in 0..64 { - m.push(ConstraintMeta::base(idx, 2)); - idx += 1; - } - m.push(ConstraintMeta::base(idx, 1)); - idx += 1; - // IS_BIT(q1[32]) (deg 2). - m.push(ConstraintMeta::base(idx, 2)); - idx += 1; - // k < N: 7 carry bits (deg 3) + overflow-required (deg 2). - for _ in 0..7 { - m.push(ConstraintMeta::base(idx, 3)); - idx += 1; - } - m.push(ConstraintMeta::base(idx, 2)); - idx += 1; - // xR < p: 7 carry bits (deg 3) + overflow-required (deg 2). - for _ in 0..7 { - m.push(ConstraintMeta::base(idx, 3)); - idx += 1; - } - m.push(ConstraintMeta::base(idx, 2)); - idx += 1; - debug_assert_eq!(idx, 148); - m + // The k usize { + 3 } fn eval>(&self, b: &mut B) { - // idx 0: IS_BIT(MU): mu·(1−mu). + // idx 0: IS_BIT(MU): mu·(1−mu). (deg 2) let mu = b.main(0, cols::MU); let one = b.one(); b.emit_base(0, mu.clone() * (one - mu)); let mut idx = 1; - // X2 convolution: 64 carries + closing c0(63). + // 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); b.emit_base(idx, root); @@ -817,7 +783,7 @@ impl ConstraintSet for EcsmConstraints { b.emit_base(idx, c0_last); idx += 1; - // Yg convolution: 64 carries + closing c1(63). + // Yg convolution: 64 carries (deg 2) + closing c1(63) (deg 1). for i in 0..64 { let root = Self::conv_carry(b, Relation::Yg, i); b.emit_base(idx, root); @@ -827,13 +793,13 @@ impl ConstraintSet for EcsmConstraints { b.emit_base(idx, c1_last); idx += 1; - // idx 131: IS_BIT(q1[32]): x·(1−x). + // idx 131: 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 + overflow-required each. + // k < N and xR < p: 7 carry bits (deg 3) + overflow-required (deg 2) each. for kind in [OverflowKind::KLtN, OverflowKind::XrLtP] { let c = Self::carry_chain(b, kind); for ci in c.iter().take(7) { diff --git a/prover/src/tables/eq.rs b/prover/src/tables/eq.rs index 945dfd094..117d8426b 100644 --- a/prover/src/tables/eq.rs +++ b/prover/src/tables/eq.rs @@ -24,12 +24,10 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; -use crate::constraints::templates::{ - AddOperand, add_pair_meta, emit_add_pair, emit_is_bit, is_bit_meta, -}; +use crate::constraints::templates::{AddOperand, emit_add_pair, emit_is_bit}; // ========================================================================= // Column indices for EQ table @@ -255,13 +253,6 @@ pub fn bus_interactions() -> Vec { pub struct EqConstraints; impl ConstraintSet for EqConstraints { - fn meta(&self) -> Vec { - let mut m = add_pair_meta(0, false).to_vec(); // idx 0,1: b + diff = a - m.push(is_bit_meta(2, false)); // idx 2: IS_BIT(invert) - m.push(ConstraintMeta::base(3, 2)); // idx 3: res = eq XOR invert - m - } - fn eval>(&self, b: &mut B) { // diff = a - b, encoded as b + diff = a (unconditional). emit_add_pair( diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 31cc4b824..832869012 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -19,7 +19,7 @@ use executor::vm::instruction::execution::KECCAK_SYSCALL_NUMBER; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; use crate::constraints::templates::{AddOperand, INV_SHIFT_32}; @@ -464,17 +464,8 @@ pub fn bus_interactions() -> Vec { pub struct KeccakConstraints; impl ConstraintSet for KeccakConstraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(51); - for lane_idx in 0..25 { - // ADD pair is conditional on μ → degree 3. - m.extend(crate::constraints::templates::add_pair_meta( - lane_idx * 2, - true, - )); - } - m.push(ConstraintMeta::base(50, 2)); // μ · carry_1 - m + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index a69acb763..30a50e0b2 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -29,7 +29,7 @@ //! produces a single-bit carry, range-checked via IS_BIT polynomial constraints. use executor::vm::instruction::execution::{KECCAK_RC, KECCAK_RHO}; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; @@ -906,11 +906,9 @@ pub fn bus_interactions() -> Vec { pub struct KeccakRndConstraints; impl ConstraintSet for KeccakRndConstraints { - fn meta(&self) -> Vec { - // 20 conditional IS_BIT constraints → degree 3. - (0..20) - .map(|i| crate::constraints::templates::is_bit_meta(i, true)) - .collect() + // The IS_BIT constraints are gated by μ (cond·x·(1−x)), so degree 3. + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/load.rs b/prover/src/tables/load.rs index 7b2f8e833..c2bf389dc 100644 --- a/prover/src/tables/load.rs +++ b/prover/src/tables/load.rs @@ -481,7 +481,7 @@ pub fn bus_interactions() -> Vec { // 5: ReadImpliesMu 6..10: ExtensionHigh(4..8) // 10..12: ExtensionMid(2..4) 12: ExtensionLow -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// LOAD table constraints as a single-source [`ConstraintSet`]. No column /// configuration is needed (the LOAD layout is fixed via `cols`). @@ -513,22 +513,8 @@ impl LoadConstraints { } impl ConstraintSet for LoadConstraints { - fn meta(&self) -> Vec { - vec![ - ConstraintMeta::base(0, 2), // FlagIsBit(SIGNED) - ConstraintMeta::base(1, 2), // FlagIsBit(READ2) - ConstraintMeta::base(2, 2), // FlagIsBit(READ4) - ConstraintMeta::base(3, 2), // FlagIsBit(READ8) - ConstraintMeta::base(4, 2), // WidthSumIsBit - ConstraintMeta::base(5, 2), // ReadImpliesMu - ConstraintMeta::base(6, 3), // ExtensionHigh(4) - ConstraintMeta::base(7, 3), // ExtensionHigh(5) - ConstraintMeta::base(8, 3), // ExtensionHigh(6) - ConstraintMeta::base(9, 3), // ExtensionHigh(7) - ConstraintMeta::base(10, 3), // ExtensionMid(2) - ConstraintMeta::base(11, 3), // ExtensionMid(3) - ConstraintMeta::base(12, 3), // ExtensionLow (res[1]) - ] + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index b4032b8e2..a68191f37 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -352,7 +352,7 @@ pub fn bus_interactions() -> Vec { // One body against the generic `ConstraintBuilder` serves the compiled prover // folder, the verifier folder and IR capture. Constraint indices 0..6. -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// LT table constraints as a single-source [`ConstraintSet`]. No column /// configuration is needed (the LT layout is fixed via `cols`). @@ -398,15 +398,9 @@ impl LtConstraints { } impl ConstraintSet for LtConstraints { - fn meta(&self) -> Vec { - vec![ - ConstraintMeta::base(0, 2), // Carry0IsBit - ConstraintMeta::base(1, 2), // Carry1IsBit - ConstraintMeta::base(2, 3), // LtFormula - ConstraintMeta::base(3, 2), // OutXorInvert - ConstraintMeta::base(4, 2), // InvertIsBit - ConstraintMeta::base(5, 2), // SignedIsBit - ] + // The LT formula (idx 2) is degree 3; the rest are degree 2. + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/memw.rs b/prover/src/tables/memw.rs index 30e27fb9a..4f775f535 100644 --- a/prover/src/tables/memw.rs +++ b/prover/src/tables/memw.rs @@ -33,7 +33,7 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; use crate::constraints::templates::emit_is_bit; @@ -860,14 +860,6 @@ fn w2_expr>(b: &B) -> pub struct MemwConstraints; impl ConstraintSet for MemwConstraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(15); - for i in 0..15 { - m.push(ConstraintMeta::base(i, 2)); - } - m - } - fn eval>(&self, b: &mut B) { // idx 0: IS_BIT<μ_sum> = μ_sum * (1 - μ_sum) let one = b.one(); diff --git a/prover/src/tables/memw_aligned.rs b/prover/src/tables/memw_aligned.rs index ec8b8832c..b9517ec91 100644 --- a/prover/src/tables/memw_aligned.rs +++ b/prover/src/tables/memw_aligned.rs @@ -39,7 +39,7 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use super::memw::MemwOperation; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; @@ -670,10 +670,6 @@ fn w2_expr>(b: &B) -> pub struct MemwAlignedConstraints; impl ConstraintSet for MemwAlignedConstraints { - fn meta(&self) -> Vec { - (0..8).map(|i| ConstraintMeta::base(i, 2)).collect() - } - fn eval>(&self, b: &mut B) { // idx 0: IS_BIT<μ_sum> = μ_sum * (1 - μ_sum) let one = b.one(); diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs index 5e2e8ba76..c02380c5f 100644 --- a/prover/src/tables/memw_register.rs +++ b/prover/src/tables/memw_register.rs @@ -41,7 +41,7 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use super::memw::MemwOperation; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; @@ -367,10 +367,6 @@ pub fn bus_interactions() -> Vec { pub struct MemwRegisterConstraints; impl ConstraintSet for MemwRegisterConstraints { - fn meta(&self) -> Vec { - (0..3).map(|i| ConstraintMeta::base(i, 2)).collect() - } - fn eval>(&self, b: &mut B) { // idx 0,1: IS_BIT<μ_read>, IS_BIT<μ_write> emit_is_bit(b, 0, cols::MU_READ, None); diff --git a/prover/src/tables/mul.rs b/prover/src/tables/mul.rs index 08f1c749c..2f0fa1d0e 100644 --- a/prover/src/tables/mul.rs +++ b/prover/src/tables/mul.rs @@ -689,7 +689,7 @@ pub fn bus_interactions() -> Vec { // 2: LhsSign 3: RhsSign // 4..8: RawProduct(0..4) -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// MUL table constraints as a single-source [`ConstraintSet`]. No column /// configuration is needed (the MUL layout is fixed via `cols`). @@ -787,19 +787,6 @@ impl MulConstraints { } impl ConstraintSet for MulConstraints { - fn meta(&self) -> Vec { - vec![ - ConstraintMeta::base(0, 2), // SignedIsBit(LHS_SIGNED) - ConstraintMeta::base(1, 2), // SignedIsBit(RHS_SIGNED) - ConstraintMeta::base(2, 2), // LhsSign - ConstraintMeta::base(3, 2), // RhsSign - ConstraintMeta::base(4, 2), // RawProduct(0) - ConstraintMeta::base(5, 2), // RawProduct(1) - ConstraintMeta::base(6, 2), // RawProduct(2) - ConstraintMeta::base(7, 2), // RawProduct(3) - ] - } - fn eval>(&self, b: &mut B) { // idx 0,1: IS_BIT range checks on the sign-flag multiplicities. let is_bit_lhs = Self::signed_is_bit(b, cols::LHS_SIGNED); diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index 202b67033..77a8ae32a 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -735,7 +735,7 @@ pub const NUM_SHIFT_CONSTRAINTS: usize = 19; // One body against the generic `ConstraintBuilder` serves the compiled prover // folder, the verifier folder and IR capture. Constraint indices 0..19. -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; /// SHIFT table constraints as a single-source [`ConstraintSet`]. No column /// configuration is needed (the SHIFT layout is fixed via `cols`). @@ -829,27 +829,8 @@ impl ShiftConstraints { } impl ConstraintSet for ShiftConstraints { - fn meta(&self) -> Vec { - let mut m = Vec::with_capacity(NUM_SHIFT_CONSTRAINTS); - m.push(ConstraintMeta::base(0, 2)); // DirectionImpliesMu - for i in 0..4 { - m.push(ConstraintMeta::base(1 + i, 3)); // ZbsOverrideX - } - m.push(ConstraintMeta::base(5, 2)); // ZbsOverrideX4 - for i in 0..4 { - m.push(ConstraintMeta::base(6 + i, 3)); // ZbsOverrideY - } - for i in 0..4 { - m.push(ConstraintMeta::base(10 + i, 2)); // LimbShiftIsBit - } - for i in 0..2 { - m.push(ConstraintMeta::base(14 + i, 3)); // OutputMatchesShifted - } - for i in 0..3 { - m.push(ConstraintMeta::base(16 + i, 2)); // FlagIsBit - } - debug_assert_eq!(m.len(), NUM_SHIFT_CONSTRAINTS); - m + fn max_degree(&self) -> usize { + 3 } fn eval>(&self, b: &mut B) { diff --git a/prover/src/tables/store.rs b/prover/src/tables/store.rs index 044f97662..c1dfc937a 100644 --- a/prover/src/tables/store.rs +++ b/prover/src/tables/store.rs @@ -22,10 +22,10 @@ use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; -use stark::constraints::builder::{ConstraintBuilder, ConstraintMeta, ConstraintSet}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable}; -use crate::constraints::templates::{emit_is_bit, is_bit_meta}; +use crate::constraints::templates::emit_is_bit; // ========================================================================= // Column indices for STORE table @@ -261,17 +261,6 @@ pub fn bus_interactions() -> Vec { pub struct StoreConstraints; impl ConstraintSet for StoreConstraints { - fn meta(&self) -> Vec { - vec![ - is_bit_meta(0, false), // write2 - is_bit_meta(1, false), // write4 - is_bit_meta(2, false), // write8 - is_bit_meta(3, false), // μ - ConstraintMeta::base(4, 2), // width sum is bit - ConstraintMeta::base(5, 2), // width ⇒ μ - ] - } - fn eval>(&self, b: &mut B) { emit_is_bit(b, 0, cols::WRITE2, None); emit_is_bit(b, 1, cols::WRITE4, None); diff --git a/prover/src/tests/branch_constraints_tests.rs b/prover/src/tests/branch_constraints_tests.rs index 950b21cb9..ed9001ec5 100644 --- a/prover/src/tests/branch_constraints_tests.rs +++ b/prover/src/tests/branch_constraints_tests.rs @@ -22,10 +22,8 @@ fn test_branch_constraint_set_meta() { for (i, m) in meta.iter().enumerate() { assert_eq!(m.constraint_idx, i); } - for m in &meta[..4] { - assert_eq!(m.degree, 3); - } - assert_eq!(meta[4].degree, 2); + // 4 conditional carry IS_BIT constraints are degree 3, so the table max is 3. + assert_eq!(BranchConstraints.max_degree(), 3); } // ========================================================================= diff --git a/prover/src/tests/commit_tests.rs b/prover/src/tests/commit_tests.rs index 876bdc04b..fdaf4d2cd 100644 --- a/prover/src/tests/commit_tests.rs +++ b/prover/src/tests/commit_tests.rs @@ -438,9 +438,10 @@ fn test_constraints_count_and_indices() { use stark::constraints::builder::ConstraintSet; let meta = CommitConstraints.meta(); assert_eq!(meta.len(), 8); - // Dense, idx-ordered, all degree 2 (unconditional). + // Dense, idx-ordered. for (i, m) in meta.iter().enumerate() { assert_eq!(m.constraint_idx, i); - assert_eq!(m.degree, 2); } + // All constraints are degree 2 (unconditional). + assert_eq!(CommitConstraints.max_degree(), 2); } diff --git a/prover/src/tests/constraint_emit_tests.rs b/prover/src/tests/constraint_emit_tests.rs index 21e9e8fb4..64f03da51 100644 --- a/prover/src/tests/constraint_emit_tests.rs +++ b/prover/src/tests/constraint_emit_tests.rs @@ -12,24 +12,18 @@ use math::field::element::FieldElement; use stark::constraint_ir::eval_program_base; use stark::constraints::builder::{ - CaptureBuilder, ConstraintBuilder, ConstraintMeta, ProverEvalFolder, RootKind, - VerifierEvalFolder, num_base_from_meta, + CaptureBuilder, ConstraintBuilder, MetaBuilder, ProverEvalFolder, RootKind, VerifierEvalFolder, + num_base_from_meta, }; use stark::frame::Frame; use stark::table::TableView; use stark::traits::TransitionEvaluationContext; -use crate::constraints::cpu::{ - arg2_exclusive_meta, arg2_meta, branch_cond_meta, branch_rvd_meta, mem_flags_bit_meta, - next_pc_add_meta, product_zero_meta, reg_not_read_is_zero_meta, rvd_eq_res_meta, -}; use crate::constraints::cpu::{ emit_arg2, emit_arg2_exclusive, emit_branch_cond, emit_branch_rvd_pair, emit_mem_flags_bit, emit_next_pc_add_pair, emit_product_zero, emit_reg_not_read_is_zero, emit_rvd_eq_res, }; -use crate::constraints::templates::{ - AddLinearTerm, AddOperand, add_pair_meta, emit_add_pair, emit_is_bit, is_bit_meta, -}; +use crate::constraints::templates::{AddLinearTerm, AddOperand, emit_add_pair, emit_is_bit}; use crate::tables::cpu::cols; use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; @@ -78,18 +72,23 @@ macro_rules! emit_body { /// this pins that capture/interpretation stays faithful to the compiled folder. /// `meta` must be dense, idx-ordered, all-base, with each declared degree equal /// to the tree-measured degree. -fn check_emit(label: &str, body: &T, meta: &[ConstraintMeta]) { +fn check_emit(label: &str, body: &T, max_degree: usize) { let n = body.n(); - assert_eq!(meta.len(), n, "[{label}] meta length"); - // --- meta invariants --- - assert_eq!(num_base_from_meta(meta), n, "[{label}] all-base num_base"); + // --- meta invariants (DERIVED from the body): dense, idx-ordered, all-base --- + let meta = { + let mut mb = MetaBuilder::new(); + body.eval(&mut mb); + mb.into_meta() + }; + assert_eq!(meta.len(), n, "[{label}] meta length"); + assert_eq!(num_base_from_meta(&meta), n, "[{label}] all-base num_base"); for (i, m) in meta.iter().enumerate() { assert_eq!(m.constraint_idx, i, "[{label}] meta idx {i}"); assert_eq!(m.kind, RootKind::Base, "[{label}] meta kind {i}"); } - // --- capture once; tree-measured degree == declared --- + // --- capture once; tree-measured degree matches the declared max --- let mut cb = CaptureBuilder::::new(); body.eval(&mut cb); let (prog, degrees) = cb.finish(n); @@ -104,13 +103,18 @@ fn check_emit(label: &str, body: &T, meta: &[ConstraintMeta]) { emitted.iter().enumerate().all(|(i, &idx)| i == idx), "[{label}] emitted constraint indices are not exactly 0..{n}: {emitted:?}" ); - for &(idx, measured) in °rees { - assert_eq!( - measured, meta[idx].degree, - "[{label}] constraint {idx}: tree degree {measured} != declared {}", - meta[idx].degree + let mut max_measured = 0; + for &(_, measured) in °rees { + assert!( + measured <= max_degree, + "[{label}] tree degree {measured} EXCEEDS declared max {max_degree}" ); + max_measured = max_measured.max(measured); } + assert_eq!( + max_measured, max_degree, + "[{label}] max tree-measured degree {max_measured} != declared {max_degree}" + ); let no_ch: Vec = vec![]; let offset_e = Fp3::zero(); @@ -167,10 +171,10 @@ fn check_emit(label: &str, body: &T, meta: &[ConstraintMeta]) { #[test] fn emit_is_bit_folder_capture_agree() { emit_body!(Uncond, 1, |b| { emit_is_bit(b, 0, 7, None) }); - check_emit("is_bit_unconditional", &Uncond, &[is_bit_meta(0, false)]); + check_emit("is_bit_unconditional", &Uncond, 2); emit_body!(Cond, 1, |b| { emit_is_bit(b, 0, 5, Some(3)) }); - check_emit("is_bit_conditional", &Cond, &[is_bit_meta(0, true)]); + check_emit("is_bit_conditional", &Cond, 3); } // ============================================================================= @@ -179,7 +183,8 @@ fn emit_is_bit_folder_capture_agree() { /// Run the pair check for one `conditional` flag. fn check_add_pair_case(label: &str, body: &T, conditional: bool) { - check_emit(label, body, &add_pair_meta(0, conditional)); + let max_degree = if conditional { 3 } else { 2 }; + check_emit(label, body, max_degree); } #[test] @@ -250,22 +255,22 @@ fn emit_add_pair_multi_cond_bytes() { #[test] fn emit_product_zero_folder_capture_agree() { emit_body!(Body, 1, |b| { emit_product_zero(b, 0, 12, 17) }); - check_emit("product_zero", &Body, &[product_zero_meta(0)]); + check_emit("product_zero", &Body, 2); } #[test] fn emit_arg2_exclusive_folder_capture_agree() { emit_body!(Body0, 1, |b| { emit_arg2_exclusive(b, 0, cols::IMM_0) }); - check_emit("arg2_exclusive_imm0", &Body0, &[arg2_exclusive_meta(0)]); + check_emit("arg2_exclusive_imm0", &Body0, 3); emit_body!(Body1, 1, |b| { emit_arg2_exclusive(b, 0, cols::IMM_1) }); - check_emit("arg2_exclusive_imm1", &Body1, &[arg2_exclusive_meta(0)]); + check_emit("arg2_exclusive_imm1", &Body1, 3); } #[test] fn emit_mem_flags_bit_folder_capture_agree() { emit_body!(Body, 1, |b| { emit_mem_flags_bit(b, 0) }); - check_emit("mem_flags_bit", &Body, &[mem_flags_bit_meta(0)]); + check_emit("mem_flags_bit", &Body, 3); } #[test] @@ -273,20 +278,12 @@ fn emit_reg_not_read_is_zero_folder_capture_agree() { emit_body!(Body, 1, |b| { emit_reg_not_read_is_zero(b, 0, cols::READ_REGISTER1, cols::RV1_0) }); - check_emit( - "reg_not_read_is_zero_rv1", - &Body, - &[reg_not_read_is_zero_meta(0)], - ); + check_emit("reg_not_read_is_zero_rv1", &Body, 2); emit_body!(Body2, 1, |b| { emit_reg_not_read_is_zero(b, 0, cols::READ_REGISTER2, cols::RV2_1) }); - check_emit( - "reg_not_read_is_zero_rv2", - &Body2, - &[reg_not_read_is_zero_meta(0)], - ); + check_emit("reg_not_read_is_zero_rv2", &Body2, 2); } // ============================================================================= @@ -296,33 +293,33 @@ fn emit_reg_not_read_is_zero_folder_capture_agree() { #[test] fn emit_arg2_folder_capture_agree() { emit_body!(Body0, 1, |b| { emit_arg2(b, 0, 0) }); - check_emit("arg2_word0", &Body0, &[arg2_meta(0)]); + check_emit("arg2_word0", &Body0, 2); emit_body!(Body1, 1, |b| { emit_arg2(b, 0, 1) }); - check_emit("arg2_word1", &Body1, &[arg2_meta(0)]); + check_emit("arg2_word1", &Body1, 2); } #[test] fn emit_rvd_eq_res_folder_capture_agree() { emit_body!(Body0, 1, |b| { emit_rvd_eq_res(b, 0, 0) }); - check_emit("rvd_eq_res_word0", &Body0, &[rvd_eq_res_meta(0)]); + check_emit("rvd_eq_res_word0", &Body0, 2); emit_body!(Body1, 1, |b| { emit_rvd_eq_res(b, 0, 1) }); - check_emit("rvd_eq_res_word1", &Body1, &[rvd_eq_res_meta(0)]); + check_emit("rvd_eq_res_word1", &Body1, 2); } #[test] fn emit_branch_rvd_pair_folder_capture_agree() { emit_body!(Body, 2, |b| { emit_branch_rvd_pair(b, 0) }); - check_emit("branch_rvd_pair", &Body, &branch_rvd_meta(0)); + check_emit("branch_rvd_pair", &Body, 3); } #[test] fn emit_branch_cond_folder_capture_agree() { emit_body!(Body, 1, |b| { emit_branch_cond(b, 0) }); - check_emit("branch_cond", &Body, &[branch_cond_meta(0)]); + check_emit("branch_cond", &Body, 3); } #[test] fn emit_next_pc_add_pair_folder_capture_agree() { emit_body!(Body, 2, |b| { emit_next_pc_add_pair(b, 0) }); - check_emit("next_pc_add_pair", &Body, &next_pc_add_meta(0)); + check_emit("next_pc_add_pair", &Body, 3); } diff --git a/prover/src/tests/constraint_set_tests_a.rs b/prover/src/tests/constraint_set_tests_a.rs index fafaedfe9..89a75864a 100644 --- a/prover/src/tests/constraint_set_tests_a.rs +++ b/prover/src/tests/constraint_set_tests_a.rs @@ -63,18 +63,15 @@ where assert_eq!(m.kind, RootKind::Base, "[{label}] meta kind {i}"); } - // --- capture once; tree-measured degree <= declared --- + // --- capture once; tree-measured degree <= the table's declared max --- // - // The declared `meta.degree` is what the engine uses as the composition-poly - // degree bound. For most tables that bound is tight, so tree-measured == - // declared. A few constraints (the ecsm/ecdas convolution TAILS — `ConvCarry` - // at large `i`) legitimately have a lower EXACT degree than their uniform - // declared bound: at limb `i` near the top, every remaining product has a - // zeroed (constant) factor, so the surviving expression is degree 1 while the - // meta declares 2 (resp. 3). The soundness-relevant invariant is therefore - // `measured <= declared` (the real degree must never EXCEED the bound the - // composition polynomial is sized for) — over-declaration is safe, - // under-declaration is not. + // `max_degree()` is what the engine uses as the composition-poly degree + // bound. Most constraints hit it; a few (the ecsm/ecdas convolution TAILS — + // `ConvCarry` at large `i`) legitimately have a lower EXACT degree (a zeroed + // factor drops the surviving product). The soundness-relevant invariant is + // therefore `measured <= max_degree()` — the real degree must never EXCEED + // the bound the composition polynomial is sized for; over-declaration is + // safe, under-declaration is not. let mut cb = CaptureBuilder::::new(); set.eval(&mut cb); let (prog, degrees) = cb.finish(num_base); @@ -89,11 +86,11 @@ where emitted.iter().enumerate().all(|(i, &idx)| i == idx), "[{label}] emitted constraint indices are not exactly 0..{n}: {emitted:?}" ); + let max_degree = set.max_degree(); for &(idx, measured) in °rees { assert!( - measured <= meta[idx].degree, - "[{label}] constraint {idx}: tree degree {measured} EXCEEDS declared {}", - meta[idx].degree + measured <= max_degree, + "[{label}] constraint {idx}: tree degree {measured} EXCEEDS max_degree() {max_degree}" ); } let no_ch: Vec = vec![]; diff --git a/prover/src/tests/constraint_set_tests_b.rs b/prover/src/tests/constraint_set_tests_b.rs index 87f1d3101..0348c2b70 100644 --- a/prover/src/tests/constraint_set_tests_b.rs +++ b/prover/src/tests/constraint_set_tests_b.rs @@ -67,7 +67,7 @@ fn check_table>(label: &str, set: &CS, num_cols: usiz assert_eq!(m.kind, RootKind::Base, "[{label}] meta kind {i}"); } - // --- capture once; tree-measured degree == declared --- + // --- capture once; tree-measured degree <= the table's declared max --- let mut cb = CaptureBuilder::::new(); set.eval(&mut cb); let (prog, degrees) = cb.finish(n); @@ -82,11 +82,11 @@ fn check_table>(label: &str, set: &CS, num_cols: usiz emitted.iter().enumerate().all(|(i, &idx)| i == idx), "[{label}] emitted constraint indices are not exactly 0..{n}: {emitted:?}" ); + let max_degree = set.max_degree(); for &(idx, measured) in °rees { - assert_eq!( - measured, meta[idx].degree, - "[{label}] constraint {idx}: tree degree {measured} != declared {}", - meta[idx].degree + assert!( + measured <= max_degree, + "[{label}] constraint {idx}: tree degree {measured} EXCEEDS max_degree() {max_degree}" ); } let no_ch: Vec = vec![];