From 20b489b802e9fc4dca7e4b8043ad14d34cc15687 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 1 Jul 2026 21:56:09 -0300 Subject: [PATCH 1/5] stark: add field-generic constraint IR with builder and CPU interpreter New module crypto/stark/src/constraint_ir/ providing a flat, topologically ordered IR for transition constraints, generic over a field tower , E> (defaulting to Goldilocks and its degree-3 extension): - ir.rs: Op/Dim/ConstraintProgram. Constants live in base_consts/ ext_consts side tables referenced by index (Op::ConstBase(u32)/ Op::ConstExt(u32)), keeping Op a plain Copy+Eq+Hash payload with zero bounds on the fields. - builder.rs: IrBuilder with (Op, Dim) hash-consing, by-value constant dedup via linear scan (FieldElement's canonicalizing PartialEq), and the id-0 = base-zero convention. - interp.rs: forward-pass interpreter; eval_program / eval_program_verifier match the AIR compute_transition_prover / compute_transition contracts, eval_program_base is the minimal single-root entry point. Const ops read the side tables directly. Not wired into the prover or verifier; no behavior change. --- crypto/stark/src/constraint_ir/builder.rs | 282 ++++++++++++++++++++++ crypto/stark/src/constraint_ir/interp.rs | 267 ++++++++++++++++++++ crypto/stark/src/constraint_ir/ir.rs | 122 ++++++++++ crypto/stark/src/constraint_ir/mod.rs | 30 +++ crypto/stark/src/lib.rs | 1 + 5 files changed, 702 insertions(+) create mode 100644 crypto/stark/src/constraint_ir/builder.rs create mode 100644 crypto/stark/src/constraint_ir/interp.rs create mode 100644 crypto/stark/src/constraint_ir/ir.rs create mode 100644 crypto/stark/src/constraint_ir/mod.rs diff --git a/crypto/stark/src/constraint_ir/builder.rs b/crypto/stark/src/constraint_ir/builder.rs new file mode 100644 index 000000000..3b9d2d6eb --- /dev/null +++ b/crypto/stark/src/constraint_ir/builder.rs @@ -0,0 +1,282 @@ +//! Explicit-builder capture front-end. +//! +//! Every transition constraint is captured into a flat [`ConstraintProgram`] +//! through an explicit [`IrBuilder`]: each constraint translates its algebra +//! into builder calls (`main`, `add`, `sub`, `mul`, ...). No fake field, no +//! thread-local arena. +//! +//! The builder hash-conses every node on `(Op, Dim)` and only emits leaves for +//! columns the constraint actually reads, so captured programs are minimal. +//! Field constants live in the [`ConstraintProgram`]'s `base_consts` / +//! `ext_consts` side tables; the builder deduplicates them by value via a linear +//! scan (`FieldElement`'s canonicalizing `PartialEq`) — the tables are tiny and +//! capture runs once at setup, so no hash map is needed there (and none would be +//! sound: `FieldElement`'s derived `Hash` and manual `Eq` disagree on +//! non-canonical representations). + +use std::collections::HashMap; + +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as GoldilocksExtension; +use math::field::goldilocks::GoldilocksField; +use math::field::traits::IsField; + +use super::ir::{ConstraintProgram, Dim, Op}; + +/// A handle to a node in an [`IrBuilder`]: its arena id and result dimension. +/// +/// `Copy` so constraint bodies read like ordinary field arithmetic. +#[derive(Clone, Copy, Debug)] +pub struct Expr { + id: u32, + dim: Dim, +} + +impl Expr { + /// The node's result dimension. + pub fn dim(self) -> Dim { + self.dim + } +} + +/// Builds a [`ConstraintProgram`] from explicit node-construction calls. +/// +/// Nodes are appended in topological order (id `i` references only `< i`) and +/// hash-consed on `(Op, Dim)`, so structurally identical subexpressions share a +/// single id. Field constants are deduplicated by value in the `base_consts` / +/// `ext_consts` tables (linear scan). Node id `0` is reserved for the base-field +/// zero (`Op::ConstBase(0)`, `base_consts[0] = 0`), matching the interpreter's +/// convention. +pub struct IrBuilder { + nodes: Vec, + dims: Vec, + cse: HashMap<(Op, Dim), u32>, + base_consts: Vec>, + ext_consts: Vec>, + roots: Vec, + /// Set by [`Self::mark_unsupported`] when a constraint couldn't be + /// captured. Propagated to [`ConstraintProgram::complete`] so callers know + /// not to interpret an incomplete program. + complete: bool, +} + +impl Default for IrBuilder { + fn default() -> Self { + Self::new() + } +} + +impl IrBuilder { + /// Create a builder with the reserved base-field zero node at id 0. + pub fn new() -> Self { + let mut b = IrBuilder { + nodes: Vec::new(), + dims: Vec::new(), + cse: HashMap::new(), + base_consts: Vec::new(), + ext_consts: Vec::new(), + roots: Vec::new(), + complete: true, + }; + // Reserve id 0 = ConstBase(0) = base-field zero. `const_base(0)` will + // dedup to this. + let zero = b.const_base(0); + debug_assert_eq!(zero.id, 0); + b + } + + /// Record that the constraint currently being captured has no capture + /// implementation. Does not panic and does not emit a root for it — the + /// resulting program is marked incomplete (see + /// [`ConstraintProgram::complete`]) so callers know not to interpret it. + pub fn mark_unsupported(&mut self) { + self.complete = false; + } + + /// Append (or reuse) a node with the given op and result dimension. + fn push(&mut self, op: Op, dim: Dim) -> Expr { + if let Some(&id) = self.cse.get(&(op, dim)) { + return Expr { id, dim }; + } + let id = self.nodes.len() as u32; + self.nodes.push(op); + self.dims.push(dim); + self.cse.insert((op, dim), id); + Expr { id, dim } + } + + // --------------------------------------------------------------------- + // Leaves + // --------------------------------------------------------------------- + + /// A main-trace column read at the given frame `offset`, row 0. + pub fn main(&mut self, offset: u8, col: usize) -> Expr { + self.push( + Op::Var { + main: true, + offset, + row: 0, + col: col as u16, + }, + Dim::Base, + ) + } + + /// An aux-trace column read at the given frame `offset`, row 0 + /// ([`Dim::Ext`]). + pub fn aux(&mut self, offset: u8, col: usize) -> Expr { + self.push( + Op::Var { + main: false, + offset, + row: 0, + col: col as u16, + }, + Dim::Ext, + ) + } + + /// A periodic column read at the current row ([`Dim::Base`]). + pub fn periodic(&mut self, idx: usize) -> Expr { + self.push(Op::Periodic { idx: idx as u16 }, Dim::Base) + } + + /// A LogUp RAP challenge, uniform per proof ([`Dim::Ext`]). + pub fn challenge(&mut self, idx: usize) -> Expr { + self.push(Op::RapChallenge { idx: idx as u16 }, Dim::Ext) + } + + /// A precomputed LogUp alpha power, uniform per proof ([`Dim::Ext`]). + pub fn alpha_power(&mut self, idx: usize) -> Expr { + self.push(Op::AlphaPow { idx: idx as u16 }, Dim::Ext) + } + + /// The LogUp table offset `L/N`, uniform per proof ([`Dim::Ext`]). + pub fn table_offset(&mut self) -> Expr { + self.push(Op::TableOffset, Dim::Ext) + } + + // --------------------------------------------------------------------- + // Constants + // --------------------------------------------------------------------- + + /// Intern a base-field constant into `base_consts`, deduplicating by value. + fn intern_base(&mut self, fe: FieldElement) -> Expr { + let idx = match self.base_consts.iter().position(|c| c == &fe) { + Some(idx) => idx, + None => { + let idx = self.base_consts.len(); + self.base_consts.push(fe); + idx + } + }; + self.push(Op::ConstBase(idx as u32), Dim::Base) + } + + /// Intern an extension-field constant into `ext_consts`, deduplicating by + /// value. + fn intern_ext(&mut self, fe: FieldElement) -> Expr { + let idx = match self.ext_consts.iter().position(|c| c == &fe) { + Some(idx) => idx, + None => { + let idx = self.ext_consts.len(); + self.ext_consts.push(fe); + idx + } + }; + self.push(Op::ConstExt(idx as u32), Dim::Ext) + } + + /// A base-field constant from a `u64`, reduced and deduplicated by value. + pub fn const_base(&mut self, v: u64) -> Expr { + self.intern_base(FieldElement::::from(v)) + } + + /// A base-field constant from an `i64`; negatives map to `p - |v|`. + pub fn const_signed(&mut self, v: i64) -> Expr { + self.intern_base(FieldElement::::from(v)) + } + + /// An extension-field constant, deduplicated by value. + pub fn const_ext(&mut self, v: FieldElement) -> Expr { + self.intern_ext(v) + } + + /// The base-field constant `1`. + pub fn one(&mut self) -> Expr { + self.const_base(1) + } + + // --------------------------------------------------------------------- + // Arithmetic + // --------------------------------------------------------------------- + + /// `a + b`. Result is [`Dim::Base`] only if both operands are base. + pub fn add(&mut self, a: Expr, b: Expr) -> Expr { + let dim = Self::join(a.dim, b.dim); + self.push(Op::Add(a.id, b.id), dim) + } + + /// `a - b`. Result is [`Dim::Base`] only if both operands are base. + pub fn sub(&mut self, a: Expr, b: Expr) -> Expr { + let dim = Self::join(a.dim, b.dim); + self.push(Op::Sub(a.id, b.id), dim) + } + + /// `a * b`. Result is [`Dim::Base`] only if both operands are base. + pub fn mul(&mut self, a: Expr, b: Expr) -> Expr { + let dim = Self::join(a.dim, b.dim); + self.push(Op::Mul(a.id, b.id), dim) + } + + /// `-a`. Preserves the operand's dimension. + pub fn neg(&mut self, a: Expr) -> Expr { + self.push(Op::Neg(a.id), a.dim) + } + + /// Explicitly embed a base value into the extension ([`Dim::Ext`]). + pub fn embed(&mut self, a: Expr) -> Expr { + self.push(Op::Embed(a.id), Dim::Ext) + } + + /// Typing join: `(Base, Base) -> Base`; any `Ext` operand -> `Ext`. + fn join(a: Dim, b: Dim) -> Dim { + match (a, b) { + (Dim::Base, Dim::Base) => Dim::Base, + _ => Dim::Ext, + } + } + + // --------------------------------------------------------------------- + // Emit / finish + // --------------------------------------------------------------------- + + /// Record `e` as the root for constraint `constraint_idx`. + /// + /// `roots` is indexed by `constraint_idx` (grown/filled with sentinel `0` + /// as needed), so constraints can be captured in any order and a full + /// per-table program ends up with `roots[c]` = constraint `c`'s value. + pub fn emit(&mut self, constraint_idx: usize, e: Expr) { + if self.roots.len() <= constraint_idx { + self.roots.resize(constraint_idx + 1, 0); + } + self.roots[constraint_idx] = e.id; + } + + /// Consume the builder and produce the captured program. + /// + /// `num_base` is the number of leading (by `constraint_idx`) constraints + /// that are base-field ([`Dim::Base`]) rooted, matching + /// `AIR::num_base_transition_constraints()`. + pub fn finish(self, num_base: usize) -> ConstraintProgram { + ConstraintProgram { + nodes: self.nodes, + dims: self.dims, + base_consts: self.base_consts, + ext_consts: self.ext_consts, + roots: self.roots, + num_base, + complete: self.complete, + } + } +} diff --git a/crypto/stark/src/constraint_ir/interp.rs b/crypto/stark/src/constraint_ir/interp.rs new file mode 100644 index 000000000..ee8cb3ba5 --- /dev/null +++ b/crypto/stark/src/constraint_ir/interp.rs @@ -0,0 +1,267 @@ +//! CPU interpreter for a captured [`ConstraintProgram`]. +//! +//! A single forward pass over the topologically ordered nodes evaluates each +//! node into a [`Value`] (base [`Dim::Base`] or extension [`Dim::Ext`]), reusing +//! the real `FieldElement` arithmetic so per-op results are bit-identical to the +//! compiled constraint path. Mixed-dimension ops auto-embed the base operand +//! into the extension, mirroring the field tower's `F: IsSubFieldOf` +//! arithmetic. +//! +//! [`eval_program`] / [`eval_program_verifier`] are the full entry points, +//! matching `AIR::compute_transition_prover` / `AIR::compute_transition` +//! respectively. [`eval_program_base`] is the minimal entry point (single root, +//! main-only, base-field result) kept for the per-constraint diff test. +//! +//! Every entry point is generic over the field tower `, E>`; +//! for the Goldilocks tower these monomorphize to the same arithmetic the +//! compiled folder emits. + +use math::field::element::FieldElement; +use math::field::traits::{IsField, IsSubFieldOf}; + +use super::ir::{ConstraintProgram, Dim, Op}; +use crate::table::TableView; +use crate::traits::TransitionEvaluationContext; + +/// A node's computed value: base field ([`Dim::Base`]) or extension +/// ([`Dim::Ext`]). +/// +/// `Clone`, not `Copy` — `Copy` is not provable for a generic `FieldElement`. +/// For the Goldilocks tower these clones compile to register copies. +#[derive(Clone, Debug)] +enum Value { + Base(FieldElement), + Ext(FieldElement), +} + +impl, E: IsField> Value { + /// Promote to the extension field, embedding a base value if needed. + fn to_ext(&self) -> FieldElement { + match self { + Value::Base(x) => x.clone().to_extension::(), + Value::Ext(x) => x.clone(), + } + } + + fn as_base(&self) -> FieldElement { + match self { + Value::Base(x) => x.clone(), + Value::Ext(_) => { + panic!("expected a base value but found an extension value") + } + } + } +} + +/// Shared forward pass: evaluate every node, then return the value array. +/// `resolve_var` resolves `Op::Var` leaves; `resolve_periodic` resolves +/// `Op::Periodic`; the remaining uniforms are read from field-agnostic closures +/// so prover/verifier share this one walk. +#[allow(clippy::too_many_arguments)] +fn run( + prog: &ConstraintProgram, + resolve_var: FVar, + resolve_periodic: FPeriodic, + resolve_challenge: FChallenge, + resolve_alpha: FAlpha, + resolve_offset: FOffset, +) -> Vec> +where + F: IsSubFieldOf, + E: IsField, + FVar: Fn(bool, u8, u8, u16) -> Value, + FPeriodic: Fn(u16) -> Value, + FChallenge: Fn(u16) -> FieldElement, + FAlpha: Fn(u16) -> FieldElement, + FOffset: Fn() -> FieldElement, +{ + let mut values: Vec> = Vec::with_capacity(prog.nodes.len()); + + for (i, op) in prog.nodes.iter().enumerate() { + let v = match *op { + Op::ConstBase(idx) => Value::Base(prog.base_consts[idx as usize].clone()), + Op::ConstExt(idx) => Value::Ext(prog.ext_consts[idx as usize].clone()), + Op::Var { + main, + offset, + row, + col, + } => resolve_var(main, offset, row, col), + Op::Periodic { idx } => resolve_periodic(idx), + Op::RapChallenge { idx } => Value::Ext(resolve_challenge(idx)), + Op::AlphaPow { idx } => Value::Ext(resolve_alpha(idx)), + Op::TableOffset => Value::Ext(resolve_offset()), + Op::Add(a, b) => binop(&values, a, b, prog.dims[i], |x, y| x + y, |x, y| x + y), + Op::Sub(a, b) => binop(&values, a, b, prog.dims[i], |x, y| x - y, |x, y| x - y), + Op::Mul(a, b) => binop(&values, a, b, prog.dims[i], |x, y| x * y, |x, y| x * y), + Op::Neg(a) => match (&values[a as usize], prog.dims[i]) { + (Value::Base(x), Dim::Base) => Value::Base(-x), + (val, Dim::Ext) => Value::Ext(-val.to_ext()), + // A base value tagged extension (or vice versa) is a dim + // mismatch; keep it in the extension to stay well-typed. + (Value::Ext(x), Dim::Base) => Value::Ext(-x.clone()), + }, + Op::Embed(a) => Value::Ext(values[a as usize].to_ext()), + }; + values.push(v); + } + + values +} + +/// Apply a binary op, auto-embedding to the extension field when the result +/// dimension is [`Dim::Ext`] (or either operand is already extension). +#[inline] +fn binop( + values: &[Value], + a: u32, + b: u32, + result_dim: Dim, + base_op: impl Fn(FieldElement, FieldElement) -> FieldElement, + ext_op: impl Fn(FieldElement, FieldElement) -> FieldElement, +) -> Value +where + F: IsSubFieldOf, + E: IsField, +{ + let va = &values[a as usize]; + let vb = &values[b as usize]; + match (va, vb, result_dim) { + (Value::Base(x), Value::Base(y), Dim::Base) => Value::Base(base_op(x.clone(), y.clone())), + _ => Value::Ext(ext_op(va.to_ext(), vb.to_ext())), + } +} + +/// Evaluate one constraint's root over a base-field main row. +/// +/// `main_row[col]` resolves `Var { main: true, col, .. }` leaves. The minimal +/// algebraic constraint set only reads main columns at offset 0, row 0 and +/// returns a base-field value. `constraint_idx` selects which root to read. +/// +/// Kept for the per-constraint diff test; [`eval_program`] is the full prover +/// entry point. +pub fn eval_program_base( + prog: &ConstraintProgram, + constraint_idx: usize, + main_row: &[FieldElement], +) -> FieldElement +where + F: IsSubFieldOf, + E: IsField, +{ + let values = run( + prog, + |main, _offset, row, col| { + assert!(main, "aux leaves are not part of the minimal algebraic set"); + assert_eq!(row, 0, "minimal set reads row 0 only"); + Value::Base(main_row[col as usize].clone()) + }, + |_idx| panic!("periodic leaves are not part of the minimal algebraic set"), + |_idx| panic!("challenge leaves are not part of the minimal algebraic set"), + |_idx| panic!("alpha_power leaves are not part of the minimal algebraic set"), + || panic!("table_offset leaves are not part of the minimal algebraic set"), + ); + let root = prog.roots[constraint_idx]; + values[root as usize].as_base() +} + +/// Full prover entry point: evaluate every constraint in `prog` against `ctx` +/// (must be [`TransitionEvaluationContext::Prover`]), writing base-field +/// ([`Dim::Base`]-rooted) constraints into `base_evals` and extension-field +/// ([`Dim::Ext`]-rooted) constraints into `ext_evals[prog.num_base..]` — the +/// same contract as `AIR::compute_transition_prover`. +pub fn eval_program( + prog: &ConstraintProgram, + ctx: &TransitionEvaluationContext, + base_evals: &mut [FieldElement], + ext_evals: &mut [FieldElement], +) where + F: IsSubFieldOf, + E: IsField, +{ + let TransitionEvaluationContext::Prover { + frame, + periodic_values, + rap_challenges, + logup_alpha_powers, + logup_table_offset, + .. + } = ctx + else { + unreachable!("eval_program called with a Verifier context"); + }; + + let values = run( + prog, + |main, offset, row, col| { + let step: &TableView = frame.get_evaluation_step(offset as usize); + debug_assert_eq!(row, 0, "tables read row 0 of each frame step"); + if main { + Value::Base(step.get_main_evaluation_element(0, col as usize).clone()) + } else { + Value::Ext(step.get_aux_evaluation_element(0, col as usize).clone()) + } + }, + |idx| Value::Base(periodic_values[idx as usize].clone()), + |idx| rap_challenges[idx as usize].clone(), + |idx| logup_alpha_powers[idx as usize].clone(), + || (*logup_table_offset).clone(), + ); + + for (c, &root) in prog.roots.iter().enumerate() { + let v = &values[root as usize]; + if c < prog.num_base { + base_evals[c] = v.as_base(); + } else { + ext_evals[c] = v.to_ext(); + } + } +} + +/// Full verifier entry point: evaluate every constraint in `prog` against `ctx` +/// (must be [`TransitionEvaluationContext::Verifier`]) at the out-of-domain +/// point, writing every constraint (base or LogUp) into `ext_evals` — the same +/// contract as `AIR::compute_transition`. The verifier frame holds only +/// extension-field elements, so base-rooted constraints are embedded into the +/// extension on write. +pub fn eval_program_verifier( + prog: &ConstraintProgram, + ctx: &TransitionEvaluationContext, + ext_evals: &mut [FieldElement], +) where + F: IsSubFieldOf, + E: IsField, +{ + let TransitionEvaluationContext::Verifier { + frame, + periodic_values, + rap_challenges, + logup_alpha_powers, + logup_table_offset, + .. + } = ctx + else { + unreachable!("eval_program_verifier called with a Prover context"); + }; + + let values = run( + prog, + |main, offset, row, col| { + let step: &TableView = frame.get_evaluation_step(offset as usize); + debug_assert_eq!(row, 0, "tables read row 0 of each frame step"); + if main { + Value::Ext(step.get_main_evaluation_element(0, col as usize).clone()) + } else { + Value::Ext(step.get_aux_evaluation_element(0, col as usize).clone()) + } + }, + |idx| Value::Ext(periodic_values[idx as usize].clone()), + |idx| rap_challenges[idx as usize].clone(), + |idx| logup_alpha_powers[idx as usize].clone(), + || (*logup_table_offset).clone(), + ); + + for (c, &root) in prog.roots.iter().enumerate() { + ext_evals[c] = values[root as usize].to_ext(); + } +} diff --git a/crypto/stark/src/constraint_ir/ir.rs b/crypto/stark/src/constraint_ir/ir.rs new file mode 100644 index 000000000..c4159589a --- /dev/null +++ b/crypto/stark/src/constraint_ir/ir.rs @@ -0,0 +1,122 @@ +//! Flat intermediate representation (IR) for captured transition constraints. +//! +//! A [`ConstraintProgram`] is a topologically ordered list of [`Op`] nodes plus +//! a per-constraint root id. It is produced by the builder capture front-end +//! (see [`crate::constraint_ir::builder`]) and consumed by the CPU interpreter +//! (see [`crate::constraint_ir::interp`]). +//! +//! The IR is generic over a field tower `` (default: the Goldilocks base +//! field and its degree-3 extension). Each node carries a [`Dim`] tag +//! distinguishing base-field values ([`Dim::Base`]) from extension-field values +//! ([`Dim::Ext`]). Field constants live in side tables (`base_consts` / +//! `ext_consts`) referenced by index, so [`Op`] stays a plain `Copy + Eq + Hash` +//! payload of `u32`s with no bounds on `F`/`E` — this keeps the builder's +//! `(Op, Dim)` common-subexpression map cheap and correct regardless of the +//! field (`FieldElement` values would otherwise poison that key type, since +//! non-canonical representations compare equal under `PartialEq` but hash +//! differently). + +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as GoldilocksExtension; +use math::field::goldilocks::GoldilocksField; +use math::field::traits::IsField; + +/// Field-arithmetic dimension of a node's value: base field ([`Dim::Base`]) or +/// its extension ([`Dim::Ext`]). +#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, Default)] +pub enum Dim { + /// Base field. + #[default] + Base, + /// Extension field. + Ext, +} + +/// One IR instruction. Operand fields are `u32` ids into the program's `nodes` +/// arena; a node with id `i` only references nodes with id `< i`. Constant ops +/// carry a `u32` index into the program's `base_consts` / `ext_consts` tables +/// rather than the field value itself, so `Op` is `Copy + Eq + Hash` for any +/// field tower. +#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] +pub enum Op { + /// A base-field literal: `base_consts[idx]`. + ConstBase(u32), + /// An extension-field literal: `ext_consts[idx]`. + ConstExt(u32), + /// A leaf read of a trace cell. `main` selects the main trace (base field) + /// vs the aux trace (extension field); `offset`/`row` select the frame + /// step/row, `col` the column. + Var { + /// `true` for a main-trace column read, `false` for an aux read. + main: bool, + /// Frame step index (0-based). + offset: u8, + /// Row within the step. + row: u8, + /// Column index. + col: u16, + }, + /// A periodic column read: `periodic_values[idx]` at the current row + /// ([`Dim::Base`]). + Periodic { idx: u16 }, + /// A LogUp RAP challenge: `rap_challenges[idx]` ([`Dim::Ext`], uniform per + /// proof). + RapChallenge { idx: u16 }, + /// A precomputed LogUp alpha power: `logup_alpha_powers[idx]` ([`Dim::Ext`], + /// uniform per proof). + AlphaPow { idx: u16 }, + /// The LogUp table offset `L/N` ([`Dim::Ext`], uniform per proof). + TableOffset, + /// `nodes[a] + nodes[b]`. + Add(u32, u32), + /// `nodes[a] - nodes[b]`. + Sub(u32, u32), + /// `nodes[a] * nodes[b]`. + Mul(u32, u32), + /// `-nodes[a]`. + Neg(u32), + /// Embed a base value into the extension (`>::embed`). + Embed(u32), +} + +/// A captured program for one transition constraint (or a set of them). +/// +/// `nodes` is topologically ordered (id `i` references only `< i`). `dims[i]` +/// is the result dimension of `nodes[i]`. `roots[c]` is the node id of +/// constraint `c`'s value. `base_consts` / `ext_consts` hold the field literals +/// referenced by `Op::ConstBase` / `Op::ConstExt`. +#[derive(Clone, Debug)] +pub struct ConstraintProgram { + /// Topologically ordered instruction list. + pub nodes: Vec, + /// Per-node result dimension, parallel to `nodes`. + pub dims: Vec, + /// Base-field constant table, indexed by `Op::ConstBase`. + pub base_consts: Vec>, + /// Extension-field constant table, indexed by `Op::ConstExt`. + pub ext_consts: Vec>, + /// Per-constraint root node ids, indexed by `constraint_idx`. + pub roots: Vec, + /// Number of constraints (a prefix of `roots`) that are base-field + /// ([`Dim::Base`]) rooted, matching `AIR::num_base_transition_constraints()`. + /// The prover interpreter writes these into `base_evals`; the rest (LogUp, + /// always [`Dim::Ext`]) go into `ext_evals[num_base..]`. + pub num_base: usize, + /// `false` if any constraint in this program was captured via the + /// default capture body (i.e. it has no real capture impl — see + /// [`crate::constraint_ir::builder::IrBuilder::mark_unsupported`]). + /// Callers must not interpret an incomplete program. + pub complete: bool, +} + +impl ConstraintProgram { + /// Number of nodes in the program (an effectiveness measure for hash-consing). + pub fn len(&self) -> usize { + self.nodes.len() + } + + /// Whether the program has no nodes. + pub fn is_empty(&self) -> bool { + self.nodes.is_empty() + } +} diff --git a/crypto/stark/src/constraint_ir/mod.rs b/crypto/stark/src/constraint_ir/mod.rs new file mode 100644 index 000000000..361dc303b --- /dev/null +++ b/crypto/stark/src/constraint_ir/mod.rs @@ -0,0 +1,30 @@ +//! Field-generic flat IR for transition constraints. +//! +//! A transition constraint's algebra is captured, at AIR-construction time, +//! into a flat intermediate representation ([`ConstraintProgram`]) via an +//! explicit [`IrBuilder`]. Interpreting that IR on the CPU +//! ([`eval_program`] / [`eval_program_verifier`]) reproduces the constraint's +//! real evaluation bit-for-bit, and the same IR is the input to the future GPU +//! constraint-evaluation kernel. +//! +//! The whole module is generic over a field tower `, E>` +//! (defaulting to the Goldilocks base field and its degree-3 extension), so a +//! capture front-end can target it for any field. Constants live in side tables +//! keyed by index, which keeps [`Op`] a plain `Copy + Eq + Hash` payload and the +//! builder's common-subexpression cache sound for every field. +//! +//! - [`ir`]: the IR data structures ([`ConstraintProgram`], [`Op`], [`Dim`]). +//! - [`builder`]: the [`IrBuilder`] and [`Expr`] capture API. +//! - [`interp`]: a CPU forward-pass interpreter over the IR. +//! +//! [`ConstraintProgram`]: ir::ConstraintProgram +//! [`Op`]: ir::Op +//! [`Dim`]: ir::Dim + +pub mod builder; +pub mod interp; +pub mod ir; + +pub use builder::{Expr, IrBuilder}; +pub use interp::{eval_program, eval_program_base, eval_program_verifier}; +pub use ir::{ConstraintProgram, Dim, Op}; diff --git a/crypto/stark/src/lib.rs b/crypto/stark/src/lib.rs index 87236c5f9..e2280f65b 100644 --- a/crypto/stark/src/lib.rs +++ b/crypto/stark/src/lib.rs @@ -6,6 +6,7 @@ compile_error!("the `disk-spill` feature requires memmap2, which does not compil #[cfg(feature = "debug-checks")] pub mod bus_debug; pub mod commitment; +pub mod constraint_ir; pub mod constraints; pub mod context; pub mod debug; From ad15768335d032e160c61693eb9c0b258c3f5d57 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 1 Jul 2026 21:56:32 -0300 Subject: [PATCH 2/5] stark: unit tests for the constraint IR, incl. a non-Goldilocks tower Hand-built IrBuilder programs checked against direct FieldElement arithmetic: every Op variant and leaf kind, mixed base/ext arithmetic with auto-embed, constant dedup (base, signed, ext), the id-0 zero convention, CSE sharing, out-of-order emit() root indexing, the complete-flag plumbing, and 1000-row randomized differential checks. The prover and verifier entry points are exercised against hand-constructed TransitionEvaluationContext values (both variants), including the base-root promotion on the verifier side and next-row (offset 1) frame reads. A reflexive-tower test (E = F over the u32 test field, which has a different modulus and BaseType than Goldilocks) proves the module is genuinely field-generic; math's test-utils feature is enabled as a dev-dependency for it. --- crypto/stark/Cargo.toml | 1 + crypto/stark/src/constraint_ir/mod.rs | 3 + crypto/stark/src/constraint_ir/tests.rs | 560 ++++++++++++++++++++++++ 3 files changed, 564 insertions(+) create mode 100644 crypto/stark/src/constraint_ir/tests.rs diff --git a/crypto/stark/Cargo.toml b/crypto/stark/Cargo.toml index d0f6a51ef..8060b80f3 100644 --- a/crypto/stark/Cargo.toml +++ b/crypto/stark/Cargo.toml @@ -37,6 +37,7 @@ web-sys = { version = "0.3.64", features = ['console'], optional = true } serde_cbor = { version = "0.11.1" } [dev-dependencies] +math = { path = "../math", features = ["test-utils"] } criterion = { version = "0.4", default-features = false } env_logger = "*" test-log = { version = "0.2.11", features = ["log"] } diff --git a/crypto/stark/src/constraint_ir/mod.rs b/crypto/stark/src/constraint_ir/mod.rs index 361dc303b..258aa23b7 100644 --- a/crypto/stark/src/constraint_ir/mod.rs +++ b/crypto/stark/src/constraint_ir/mod.rs @@ -25,6 +25,9 @@ pub mod builder; pub mod interp; pub mod ir; +#[cfg(test)] +mod tests; + pub use builder::{Expr, IrBuilder}; pub use interp::{eval_program, eval_program_base, eval_program_verifier}; pub use ir::{ConstraintProgram, Dim, Op}; diff --git a/crypto/stark/src/constraint_ir/tests.rs b/crypto/stark/src/constraint_ir/tests.rs new file mode 100644 index 000000000..61e3d8dbb --- /dev/null +++ b/crypto/stark/src/constraint_ir/tests.rs @@ -0,0 +1,560 @@ +//! Unit tests for the field-generic constraint IR: hand-built programs checked +//! against direct `FieldElement` arithmetic, the prover/verifier entry points +//! against hand-constructed contexts, and a non-Goldilocks tower (`E = F`) that +//! exercises the reflexive `IsSubFieldOf` path — the point of the genericity. + +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as Ext; +use math::field::goldilocks::GoldilocksField as Fp; +use math::field::test_fields::u32_test_field::U32TestField; + +use super::builder::IrBuilder; +use super::interp::{eval_program, eval_program_base, eval_program_verifier}; +use super::ir::{ConstraintProgram, Dim, Op}; +use crate::frame::Frame; +use crate::lookup::PackingShifts; +use crate::table::TableView; +use crate::traits::TransitionEvaluationContext; + +type FpE = FieldElement; +type ExtE = FieldElement; + +fn fp(v: u64) -> FpE { + FpE::from(v) +} + +/// Build a degree-3 Goldilocks extension element from three `u64` components. +fn ext3(a: u64, b: u64, c: u64) -> ExtE { + ExtE::from_raw([fp(a), fp(b), fp(c)]) +} + +// ------------------------------------------------------------------------ +// id-0 convention + const dedup +// ------------------------------------------------------------------------ + +#[test] +fn id_zero_is_base_const_zero() { + let b = IrBuilder::::new(); + let prog = b.finish(0); + // Node 0 is ConstBase(0); base_consts[0] is the base-field zero. + assert_eq!(prog.nodes[0], Op::ConstBase(0)); + assert_eq!(prog.dims[0], Dim::Base); + assert_eq!(prog.base_consts[0], FpE::zero()); + assert_eq!(prog.len(), 1); + assert!(!prog.is_empty()); +} + +#[test] +fn const_base_zero_dedups_to_id_zero() { + let mut b = IrBuilder::::new(); + let z = b.const_base(0); + assert_eq!(z.dim(), Dim::Base); + let prog = b.finish(0); + // No new node or const slot: reuses the reserved id-0 zero. + assert_eq!(prog.nodes.len(), 1); + assert_eq!(prog.base_consts.len(), 1); +} + +#[test] +fn const_dedup_same_value_interned_once() { + let mut b = IrBuilder::::new(); + b.const_base(7); + b.const_base(7); + let prog = b.finish(0); + // base_consts: [0, 7] only; nodes: ConstBase(0), ConstBase(1) only. + assert_eq!(prog.base_consts, vec![fp(0), fp(7)]); + assert_eq!(prog.nodes.len(), 2); +} + +#[test] +fn const_signed_negative_reduces_and_dedups() { + let mut b = IrBuilder::::new(); + let neg = b.const_signed(-1); + assert_eq!(neg.dim(), Dim::Base); + let prog = b.finish(0); + // -1 in the field is p - 1; matches FieldElement::from(-1i64). + assert_eq!(prog.base_consts[1], FpE::from(-1i64)); + + // Interning the same negative twice uses one slot and one node. + let mut b2 = IrBuilder::::new(); + b2.const_signed(-5); + b2.const_signed(-5); + let prog2 = b2.finish(0); + assert_eq!(prog2.base_consts, vec![fp(0), FpE::from(-5i64)]); + assert_eq!(prog2.nodes.len(), 2); + + // A positive i64 dedups against the same value interned via const_base. + let mut b3 = IrBuilder::::new(); + b3.const_base(9); + b3.const_signed(9); + let prog3 = b3.finish(0); + assert_eq!(prog3.base_consts, vec![fp(0), fp(9)]); + assert_eq!(prog3.nodes.len(), 2); +} + +#[test] +fn const_ext_dedups_by_value() { + let mut b = IrBuilder::::new(); + let e1 = b.const_ext(ext3(1, 2, 3)); + b.const_ext(ext3(1, 2, 3)); + b.const_ext(ext3(4, 5, 6)); + assert_eq!(e1.dim(), Dim::Ext); + let prog = b.finish(0); + // ext_consts: two distinct values. + assert_eq!(prog.ext_consts, vec![ext3(1, 2, 3), ext3(4, 5, 6)]); + // nodes: ConstBase(0) [id-0] + ConstExt(0) + ConstExt(1). + assert_eq!(prog.nodes.len(), 3); + assert_eq!(prog.nodes[1], Op::ConstExt(0)); + assert_eq!(prog.nodes[2], Op::ConstExt(1)); +} + +// ------------------------------------------------------------------------ +// CSE on (Op, Dim) still works with side-table constants. +// ------------------------------------------------------------------------ + +#[test] +fn cse_shares_structurally_identical_subexpressions() { + let mut b = IrBuilder::::new(); + let x = b.main(0, 0); + let y = b.main(0, 1); + let s1 = b.add(x, y); + let s2 = b.add(x, y); // structurally identical: no new node + let nodes_so_far = 4; // zero, x, y, add + let m = b.mul(s1, s2); // Mul(add, add): one new node + b.emit(0, m); + let prog = b.finish(1); + assert_eq!(prog.nodes.len(), nodes_so_far + 1); + + let row = vec![fp(3), fp(4)]; + let got = eval_program_base(&prog, 0, &row); + let s = fp(3) + fp(4); + assert_eq!(got, s * s); +} + +// ------------------------------------------------------------------------ +// Every arithmetic Op over base-field leaves, checked against direct math. +// ------------------------------------------------------------------------ + +#[test] +fn base_arithmetic_add_sub_mul_neg() { + // Roots: idx 0 = (x + y) - (x * y); idx 1 = its negation. + let mut b = IrBuilder::::new(); + let x = b.main(0, 0); + let y = b.main(0, 1); + let sum = b.add(x, y); + let prod = b.mul(x, y); + let diff = b.sub(sum, prod); + let negd = b.neg(diff); + assert_eq!(sum.dim(), Dim::Base); + assert_eq!(prod.dim(), Dim::Base); + assert_eq!(diff.dim(), Dim::Base); + assert_eq!(negd.dim(), Dim::Base); + b.emit(0, diff); + b.emit(1, negd); + let prog = b.finish(2); + + for (px, py) in [(3u64, 5u64), (0, 9), (100, 7), (1, 1)] { + let row = vec![fp(px), fp(py)]; + let expected = (fp(px) + fp(py)) - (fp(px) * fp(py)); + assert_eq!(eval_program_base(&prog, 0, &row), expected); + assert_eq!(eval_program_base(&prog, 1, &row), -expected); + } +} + +#[test] +fn base_const_arithmetic() { + // 2 * x - 1 + let mut b = IrBuilder::::new(); + let x = b.main(0, 0); + let two = b.const_base(2); + let one = b.one(); + let twox = b.mul(two, x); + let res = b.sub(twox, one); + b.emit(0, res); + let prog = b.finish(1); + + for xv in [0u64, 1, 2, 42, 1_000_000] { + let got = eval_program_base(&prog, 0, &[fp(xv)]); + assert_eq!(got, fp(2) * fp(xv) - fp(1)); + } +} + +// ------------------------------------------------------------------------ +// Frame offsets: reading the next row (offset 1). +// ------------------------------------------------------------------------ + +#[test] +fn frame_offset_reads_next_step() { + // next - cur over main column 0. + let mut b = IrBuilder::::new(); + let cur = b.main(0, 0); + let next = b.main(1, 0); + let res = b.sub(next, cur); + b.emit(0, res); + let prog = b.finish(1); + + let step0 = TableView::::new(vec![vec![fp(10)]], vec![vec![]]); + let step1 = TableView::::new(vec![vec![fp(17)]], vec![vec![]]); + let frame = Frame::::new(vec![step0, step1]); + let periodic: Vec = vec![]; + let rap: Vec = vec![]; + let alpha: Vec = vec![]; + let offset = ExtE::zero(); + let shifts = PackingShifts::::new(); + let ctx = + TransitionEvaluationContext::new_prover(&frame, &periodic, &rap, &alpha, &offset, &shifts); + + let mut base_evals = vec![FpE::zero()]; + let mut ext_evals: Vec = vec![]; + eval_program(&prog, &ctx, &mut base_evals, &mut ext_evals); + assert_eq!(base_evals[0], fp(17) - fp(10)); +} + +// ------------------------------------------------------------------------ +// Mixed Base×Ext arithmetic with auto-embed, and the explicit Embed op. +// ------------------------------------------------------------------------ + +#[test] +fn mixed_base_ext_auto_embeds() { + // aux (Ext) + main (Base) and main * aux: result Ext, base auto-embedded. + let mut b = IrBuilder::::new(); + let m = b.main(0, 0); // Base + let a = b.aux(0, 0); // Ext + let sum = b.add(a, m); + let prod = b.mul(m, a); + assert_eq!(sum.dim(), Dim::Ext); + assert_eq!(prod.dim(), Dim::Ext); + b.emit(0, sum); + b.emit(1, prod); + let prog = b.finish(0); // both roots are Ext + + let main_val = fp(5); + let aux_val = ext3(2, 3, 4); + let step = TableView::::new(vec![vec![main_val]], vec![vec![aux_val]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let rap: Vec = vec![]; + let alpha: Vec = vec![]; + let offset = ExtE::zero(); + let shifts = PackingShifts::::new(); + let ctx = + TransitionEvaluationContext::new_prover(&frame, &periodic, &rap, &alpha, &offset, &shifts); + + let mut base_evals: Vec = vec![]; + let mut ext_evals = vec![ExtE::zero(), ExtE::zero()]; + eval_program(&prog, &ctx, &mut base_evals, &mut ext_evals); + // Mixed operators put the subfield on the left: F op E -> E. + assert_eq!(ext_evals[0], main_val + aux_val); + assert_eq!(ext_evals[1], main_val * aux_val); +} + +#[test] +fn explicit_embed_and_ext_neg() { + // Embed(main) and Neg over an Ext value: embed(m) + (-aux). + let mut b = IrBuilder::::new(); + let m = b.main(0, 0); + let e = b.embed(m); + assert_eq!(m.dim(), Dim::Base); + assert_eq!(e.dim(), Dim::Ext); + let a = b.aux(0, 0); + let na = b.neg(a); + assert_eq!(na.dim(), Dim::Ext); + let res = b.add(e, na); + b.emit(0, res); + let prog = b.finish(0); + assert!(prog.nodes.iter().any(|op| matches!(op, Op::Embed(_)))); + + let aux_val = ext3(1, 2, 3); + let step = TableView::::new(vec![vec![fp(9)]], vec![vec![aux_val]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let rap: Vec = vec![]; + let alpha: Vec = vec![]; + let offset = ExtE::zero(); + let shifts = PackingShifts::::new(); + let ctx = + TransitionEvaluationContext::new_prover(&frame, &periodic, &rap, &alpha, &offset, &shifts); + + let mut base_evals: Vec = vec![]; + let mut ext_evals = vec![ExtE::zero()]; + eval_program(&prog, &ctx, &mut base_evals, &mut ext_evals); + assert_eq!(ext_evals[0], fp(9).to_extension::() - aux_val); +} + +// ------------------------------------------------------------------------ +// Every leaf kind: periodic, challenge, alpha_power, table_offset, aux. +// ------------------------------------------------------------------------ + +#[test] +fn all_leaf_kinds_logup_shaped() { + // A LogUp-shaped expression touching every leaf variety: + // periodic(0) * challenge(0) + alpha_pow(1) * aux(0,3) - table_offset() + let mut b = IrBuilder::::new(); + let p = b.periodic(0); // Base + let ch = b.challenge(0); // Ext + let ap = b.alpha_power(1); // Ext + let au = b.aux(0, 3); // Ext + let off = b.table_offset(); // Ext + assert_eq!(p.dim(), Dim::Base); + assert_eq!(ch.dim(), Dim::Ext); + assert_eq!(ap.dim(), Dim::Ext); + assert_eq!(au.dim(), Dim::Ext); + assert_eq!(off.dim(), Dim::Ext); + let t1 = b.mul(p, ch); // Base×Ext → Ext + let t2 = b.mul(ap, au); // Ext×Ext → Ext + let s = b.add(t1, t2); + let res = b.sub(s, off); + assert_eq!(res.dim(), Dim::Ext); + b.emit(0, res); + let prog = b.finish(0); + + let periodic = vec![fp(6)]; + let rap = vec![ext3(1, 0, 0), ext3(2, 2, 2)]; + let alpha = vec![ext3(9, 9, 9), ext3(3, 1, 4)]; + let offset = ext3(7, 7, 7); + let aux_row = vec![ext3(0, 0, 0), ext3(0, 0, 0), ext3(0, 0, 0), ext3(5, 5, 5)]; + + let expected = { + let t1 = periodic[0] * rap[0]; // periodic(0) * challenge(0) + let t2 = alpha[1] * aux_row[3]; + (t1 + t2) - offset + }; + + let step = TableView::::new(vec![vec![]], vec![aux_row]); + let frame = Frame::::new(vec![step]); + let shifts = PackingShifts::::new(); + let ctx = + TransitionEvaluationContext::new_prover(&frame, &periodic, &rap, &alpha, &offset, &shifts); + + let mut base_evals: Vec = vec![]; + let mut ext_evals = vec![ExtE::zero()]; + eval_program(&prog, &ctx, &mut base_evals, &mut ext_evals); + assert_eq!(ext_evals[0], expected); +} + +// ------------------------------------------------------------------------ +// Prover & verifier full entry points on hand-built contexts (both variants). +// ------------------------------------------------------------------------ + +/// One base constraint (idx 0: `a - b`) and one ext constraint +/// (idx 1: `aux0 * alpha0`); `num_base = 1`. +fn two_constraint_program() -> ConstraintProgram { + let mut b = IrBuilder::::new(); + let a = b.main(0, 0); + let bb = b.main(0, 1); + let base_c = b.sub(a, bb); + b.emit(0, base_c); + let au = b.aux(0, 0); + let al = b.alpha_power(0); + let ext_c = b.mul(au, al); + b.emit(1, ext_c); + b.finish(1) +} + +#[test] +fn prover_entry_point_splits_base_and_ext() { + let prog = two_constraint_program(); + let aux_val = ext3(2, 0, 1); + let step = TableView::::new(vec![vec![fp(30), fp(12)]], vec![vec![aux_val]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let rap: Vec = vec![]; + let alpha = vec![ext3(3, 3, 3)]; + let offset = ExtE::zero(); + let shifts = PackingShifts::::new(); + let ctx = + TransitionEvaluationContext::new_prover(&frame, &periodic, &rap, &alpha, &offset, &shifts); + + let mut base_evals = vec![FpE::zero()]; + let mut ext_evals = vec![ExtE::zero(), ExtE::zero()]; + eval_program(&prog, &ctx, &mut base_evals, &mut ext_evals); + + // Base root lands in base_evals[0]; ext root in ext_evals[1] (absolute idx). + assert_eq!(base_evals[0], fp(30) - fp(12)); + assert_eq!(ext_evals[1], aux_val * alpha[0]); +} + +#[test] +fn verifier_entry_point_promotes_base_roots() { + let prog = two_constraint_program(); + // Verifier frame holds extension elements only (Frame). + let aux_val = ext3(2, 0, 1); + let step = TableView::::new( + vec![vec![ext3(30, 0, 0), ext3(12, 0, 0)]], + vec![vec![aux_val]], + ); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let rap: Vec = vec![]; + let alpha = vec![ext3(3, 3, 3)]; + let offset = ExtE::zero(); + let shifts = PackingShifts::::new(); + let ctx = TransitionEvaluationContext::::new_verifier( + &frame, &periodic, &rap, &alpha, &offset, &shifts, + ); + + let mut ext_evals = vec![ExtE::zero(), ExtE::zero()]; + eval_program_verifier(&prog, &ctx, &mut ext_evals); + + // The base-rooted constraint is promoted into the extension on write. + assert_eq!(ext_evals[0], ext3(30, 0, 0) - ext3(12, 0, 0)); + assert_eq!(ext_evals[1], aux_val * alpha[0]); +} + +// ------------------------------------------------------------------------ +// roots indexed by emit(constraint_idx), in any emission order. +// ------------------------------------------------------------------------ + +#[test] +fn roots_indexed_by_constraint_idx_any_order() { + let mut b = IrBuilder::::new(); + let x = b.main(0, 0); + // Emit idx 2 before idx 0 — roots must still land in the right slots. + let x2 = b.mul(x, x); + b.emit(2, x2); + b.emit(0, x); + let one = b.one(); + let xp1 = b.add(x, one); + b.emit(1, xp1); + let prog = b.finish(3); + assert_eq!(prog.roots.len(), 3); + + let row = vec![fp(4)]; + assert_eq!(eval_program_base(&prog, 0, &row), fp(4)); + assert_eq!(eval_program_base(&prog, 1, &row), fp(4) + fp(1)); + assert_eq!(eval_program_base(&prog, 2, &row), fp(4) * fp(4)); +} + +// ------------------------------------------------------------------------ +// complete flag plumbing. +// ------------------------------------------------------------------------ + +#[test] +fn complete_flag_defaults_true_and_mark_unsupported_clears_it() { + let b = IrBuilder::::new(); + assert!(b.finish(0).complete); + + let mut b = IrBuilder::::new(); + b.mark_unsupported(); + assert!(!b.finish(0).complete); +} + +// ------------------------------------------------------------------------ +// Non-Goldilocks tower: E = F over the Baby-Bear-prime U32 test field. +// Exercises the reflexive IsSubFieldOf impl and proves the module is +// genuinely field-generic. (This trimmed math crate has no Stark252-style +// big field; U32TestField has a different modulus AND a different BaseType +// (u32), so it is a strict genericity check.) +// ------------------------------------------------------------------------ + +#[test] +fn non_goldilocks_reflexive_tower_builds_and_interprets() { + type G = U32TestField; + type GE = FieldElement; + fn g(v: u64) -> GE { + GE::from(v) + } + + // Base-only program for eval_program_base (which walks every node and + // accepts main leaves only): x * y + 3. + let mut b0 = IrBuilder::::new(); + let x = b0.main(0, 0); + let y = b0.main(0, 1); + let prod = b0.mul(x, y); + let three = b0.const_base(3); + let base_res = b0.add(prod, three); + b0.emit(0, base_res); + let base_prog = b0.finish(1); + let row = vec![g(6), g(7)]; + assert_eq!(eval_program_base(&base_prog, 0, &row), g(6) * g(7) + g(3)); + + // Program: idx 0 (base) = x * y + 3; idx 1 (ext = same field) = aux0 + 10. + let mut b = IrBuilder::::new(); + let x = b.main(0, 0); + let y = b.main(0, 1); + let prod = b.mul(x, y); + let three = b.const_base(3); + let base_res = b.add(prod, three); + b.emit(0, base_res); + + let au = b.aux(0, 0); // "Ext" (= G here) + let ec = b.const_ext(g(10)); + let ext_res = b.add(au, ec); + assert_eq!(ext_res.dim(), Dim::Ext); + b.emit(1, ext_res); + + let prog = b.finish(1); + // Const dedup with a non-u64 BaseType (u32) still works. + assert_eq!(prog.base_consts, vec![g(0), g(3)]); + assert_eq!(prog.ext_consts, vec![g(10)]); + + // Full prover entry point with F = E = G. + let step = TableView::::new(vec![vec![g(6), g(7)]], vec![vec![g(4)]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let rap: Vec = vec![]; + let alpha: Vec = vec![]; + let offset = g(0); + let shifts = PackingShifts::::new(); + let ctx = TransitionEvaluationContext::::new_prover( + &frame, &periodic, &rap, &alpha, &offset, &shifts, + ); + let mut base_evals = vec![GE::zero()]; + let mut ext_evals = vec![GE::zero(), GE::zero()]; + eval_program(&prog, &ctx, &mut base_evals, &mut ext_evals); + assert_eq!(base_evals[0], g(6) * g(7) + g(3)); + assert_eq!(ext_evals[1], g(4) + g(10)); + + // Verifier entry point too (the frame is Frame either way here). + let vctx = TransitionEvaluationContext::::new_verifier( + &frame, &periodic, &rap, &alpha, &offset, &shifts, + ); + let mut v_evals = vec![GE::zero(), GE::zero()]; + eval_program_verifier(&prog, &vctx, &mut v_evals); + assert_eq!(v_evals[0], g(6) * g(7) + g(3)); + assert_eq!(v_evals[1], g(4) + g(10)); +} + +// ------------------------------------------------------------------------ +// Random-row differential fuzz: a nontrivial base program vs direct math. +// ------------------------------------------------------------------------ + +struct SplitMix64(u64); +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } +} + +#[test] +fn random_rows_match_direct_arithmetic() { + // ((a + b) * c - a) * (b - c) + 5 + let mut bld = IrBuilder::::new(); + let a = bld.main(0, 0); + let b = bld.main(0, 1); + let c = bld.main(0, 2); + let ab = bld.add(a, b); + let abc = bld.mul(ab, c); + let abca = bld.sub(abc, a); + let bc = bld.sub(b, c); + let t = bld.mul(abca, bc); + let five = bld.const_base(5); + let res = bld.add(t, five); + bld.emit(0, res); + let prog = bld.finish(1); + + let mut rng = SplitMix64(0xDEAD_BEEF_CAFE_F00D); + for _ in 0..1000 { + let av = fp(rng.next_u64()); + let bv = fp(rng.next_u64()); + let cv = fp(rng.next_u64()); + let row = vec![av, bv, cv]; + let got = eval_program_base(&prog, 0, &row); + let expected = ((av + bv) * cv - av) * (bv - cv) + fp(5); + assert_eq!(got, expected); + } +} From b7da04c77629c065c38965afda62758345c70e55 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 1 Jul 2026 22:13:44 -0300 Subject: [PATCH 3/5] stark: add the ConstraintBuilder single-body constraint framework MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New module crypto/stark/src/constraints/builder.rs: one constraint body, written once against the ConstraintBuilder trait, is interpreted three ways depending on the implementation it runs over: - ProverEvalFolder (Expr = FieldElement): compiled per-row prover evaluation, constructed from the Prover TransitionEvaluationContext variant plus output slices; emit_ext writes ext_evals at the absolute constraint index. - VerifierEvalFolder (Expr = FieldElement): the same body at the OOD point over the all-extension frame; const_base embeds via FieldElement::::from(v).to_extension(). Monomorphized into the guest binary this is the recursion path — no capture, no hashing, no interpretation. - CaptureBuilder (Expr = owned Rc expression tree with eager dim + degree): one setup-time run that flattens into the constraint IR's IrBuilder (hash-consing there = structural CSE) and returns the program plus per-root tree-measured degrees. Also: ExprOps/ExtExprOps operator-bound aliases (mixed base/ext ops keep the base operand on the left, matching the field tower), ConstraintMeta + RootKind plain-data constraint metadata with the dense/idx-ordered/Base-prefix invariants (num_base_from_meta), the ConstraintSet per-table trait, and debug-build emit tracking asserting every constraint index is emitted exactly once. Tests: a sample ConstraintSet (EqXor-, IsBit- and Add-carry-pair-shaped bodies plus a LogUp-shaped extension constraint) checked on 1000 random rows three ways — prover folder vs direct arithmetic, prover folder vs interpreted capture, verifier folder vs interpreted capture — plus measured-vs-declared degrees, meta invariants, and the completeness asserts. Not wired into any production path; no behavior change. --- crypto/stark/src/constraints/builder.rs | 749 ++++++++++++++++++ crypto/stark/src/constraints/builder_tests.rs | 441 +++++++++++ crypto/stark/src/constraints/mod.rs | 3 + 3 files changed, 1193 insertions(+) create mode 100644 crypto/stark/src/constraints/builder.rs create mode 100644 crypto/stark/src/constraints/builder_tests.rs diff --git a/crypto/stark/src/constraints/builder.rs b/crypto/stark/src/constraints/builder.rs new file mode 100644 index 000000000..305a1a3fc --- /dev/null +++ b/crypto/stark/src/constraints/builder.rs @@ -0,0 +1,749 @@ +//! The `ConstraintBuilder` single-body constraint front-end. +//! +//! One constraint body, written once against [`ConstraintBuilder`], is +//! interpreted three ways depending on the implementation it runs over: +//! - [`ProverEvalFolder`]: `Expr = FieldElement` — compiled per-row prover +//! evaluation (the CPU hot path). +//! - [`VerifierEvalFolder`]: `Expr = FieldElement` — the same body at the +//! OOD point (and, monomorphized into the guest binary, the recursion path; +//! no capture, no hashing, no interpretation in-circuit). +//! - [`CaptureBuilder`]: `Expr` = an owned expression tree — one setup-time run +//! that flattens into the flat [`ConstraintProgram`] IR for the CPU +//! interpreter and the GPU, measuring constraint degrees along the way. +//! +//! A table's constraints are packaged as a [`ConstraintSet`]: idx-ordered +//! [`ConstraintMeta`] (plain data: kind, declared degree, zerofier shape) plus +//! THE single `eval` body that emits every constraint. +//! +//! Fixed packing-shift constants (`2^8`/`2^16`/`2^24`) have no dedicated leaf: +//! bodies lower them through `const_base`, like any other structural constant. + +use std::marker::PhantomData; +use std::ops::{Add, Mul, Neg, Sub}; +use std::rc::Rc; + +use math::field::element::FieldElement; +use math::field::traits::{IsField, IsSubFieldOf}; + +use crate::constraint_ir::{ConstraintProgram, Dim, IrBuilder}; +use crate::frame::Frame; +use crate::traits::TransitionEvaluationContext; + +// ============================================================================= +// Operator-bound aliases +// ============================================================================= + +/// Base-field expression operations. `Ext` is the builder's extension +/// expression type; mixed ops keep the base operand on the LEFT (the field +/// tower only implements subfield ∘ superfield, not the reverse — see +/// `math::field::element` operator impls). +pub trait ExprOps: + Sized + + Clone + + Add + + Sub + + Mul + + Neg + + Add + + Sub + + Mul +{ +} +impl ExprOps for T where + T: Sized + + Clone + + Add + + Sub + + Mul + + Neg + + Add + + Sub + + Mul +{ +} + +/// Extension-field expression operations (self ops only; base×ext lives on +/// [`ExprOps`] so the base operand stays on the left). +pub trait ExtExprOps: + Sized + + Clone + + Add + + Sub + + Mul + + Neg +{ +} +impl ExtExprOps for T where + T: Sized + + Clone + + Add + + Sub + + Mul + + Neg +{ +} + +// ============================================================================= +// The trait +// ============================================================================= + +/// The single-body constraint front-end: leaves + emit sinks. Constraint +/// bodies are generic over an implementation of this trait; the associated +/// `Expr`/`ExprE` types decide what a run of the body *means*. +/// +/// `const_base`/`const_signed` are the ONLY constant path — there is no +/// `From>` on `Expr` (it would be wrong for +/// [`VerifierEvalFolder`], where `Expr = FieldElement`). +pub trait ConstraintBuilder { + /// Base-field expression. + type Expr: ExprOps; + /// Extension-field expression. + type ExprE: ExtExprOps; + + // ---- leaves --------------------------------------------------------- + fn main(&self, offset: usize, col: usize) -> Self::Expr; + fn aux(&self, offset: usize, col: usize) -> Self::ExprE; + fn periodic(&self, idx: usize) -> Self::Expr; + /// `rap_challenges[idx]`. + fn challenge(&self, idx: usize) -> Self::ExprE; + /// `logup_alpha_powers[idx]`. + fn alpha_pow(&self, idx: usize) -> Self::ExprE; + /// The LogUp table offset `L/N`. + fn table_offset(&self) -> Self::ExprE; + fn const_base(&self, v: u64) -> Self::Expr; + fn const_signed(&self, v: i64) -> Self::Expr; + fn one(&self) -> Self::Expr { + self.const_base(1) + } + fn zero(&self) -> Self::Expr { + self.const_base(0) + } + + // ---- 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); +} + +// ============================================================================= +// Constraint metadata +// ============================================================================= + +/// Whether a constraint's root value lives in the base field or the extension. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum RootKind { + /// Base-field constraint (algebraic table constraints). + Base, + /// Extension-field constraint (LogUp). + 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`]. +#[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, + /// Periodicity of application over the trace (default 1: every row). + pub period: usize, + /// Offset for periodic application (default 0). + pub offset: usize, + /// Periodicity of rows exempted within the applied rows (default None). + pub exemptions_period: Option, + /// Offset for the periodic exemptions (default None). + pub periodic_exemptions_offset: Option, + /// 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 { + Self { + constraint_idx, + kind: RootKind::Base, + degree, + period: 1, + offset: 0, + exemptions_period: None, + periodic_exemptions_offset: None, + end_exemptions: 0, + } + } + + /// An extension-field (LogUp) constraint with default zerofier shape. + pub fn ext(constraint_idx: usize, degree: usize) -> Self { + Self { + kind: RootKind::Ext, + ..Self::base(constraint_idx, degree) + } + } + + pub fn with_period(mut self, period: usize) -> Self { + self.period = period; + self + } + + pub fn with_offset(mut self, offset: usize) -> Self { + self.offset = offset; + self + } + + pub fn with_exemptions(mut self, exemptions_period: usize, exemptions_offset: usize) -> Self { + self.exemptions_period = Some(exemptions_period); + self.periodic_exemptions_offset = Some(exemptions_offset); + self + } + + pub fn with_end_exemptions(mut self, end_exemptions: usize) -> Self { + self.end_exemptions = end_exemptions; + self + } +} + +/// Compute `num_base` from a table's metadata, debug-asserting the invariants: +/// the list is dense and idx-ordered (`meta[i].constraint_idx == i`) and +/// `RootKind::Base` entries form a prefix — the prefix length IS `num_base`, +/// matching the engine's existing base/ext split convention. +pub fn num_base_from_meta(meta: &[ConstraintMeta]) -> usize { + let num_base = meta.iter().take_while(|m| m.kind == RootKind::Base).count(); + #[cfg(debug_assertions)] + for (i, m) in meta.iter().enumerate() { + assert_eq!( + m.constraint_idx, i, + "constraint meta must be dense and idx-ordered: entry {i} has idx {}", + m.constraint_idx + ); + assert!( + (m.kind == RootKind::Base) == (i < num_base), + "RootKind::Base entries must form a prefix: entry {i} is {:?}", + m.kind + ); + } + num_base +} + +/// One table's constraints: metadata + THE single body. +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. + fn eval>(&self, b: &mut B); +} + +// ============================================================================= +// Debug-build emit tracking (shared by the folders) +// ============================================================================= + +/// Debug-build bitset asserting every constraint index is emitted exactly +/// once. A zero-sized no-op in release builds. +struct EmitTracker { + #[cfg(debug_assertions)] + seen: Vec, +} + +impl EmitTracker { + fn new(_num_constraints: usize) -> Self { + Self { + #[cfg(debug_assertions)] + seen: vec![false; _num_constraints], + } + } + + #[inline] + fn mark(&mut self, _idx: usize) { + #[cfg(debug_assertions)] + { + assert!( + _idx < self.seen.len(), + "constraint idx {_idx} out of range ({} constraints)", + self.seen.len() + ); + assert!(!self.seen[_idx], "constraint {_idx} emitted twice"); + self.seen[_idx] = true; + } + } + + fn assert_complete(&self) { + #[cfg(debug_assertions)] + for (i, emitted) in self.seen.iter().enumerate() { + assert!(emitted, "constraint {i} was never emitted"); + } + } +} + +// ============================================================================= +// 1. ProverEvalFolder — compiled per-row evaluation (base-field frame) +// ============================================================================= + +/// Direct evaluation over one prover row: `Expr = FieldElement`, +/// `ExprE = FieldElement`. Constructed per row from the Prover +/// [`TransitionEvaluationContext`] variant plus the output slices; +/// `emit_base` writes `base_evals[idx]`, `emit_ext` writes `ext_evals[idx]` +/// (ABSOLUTE constraint index — `ext_evals` is sized to the total constraint +/// count). This is the CPU hot path: after inlining, a body run is the same +/// machine code as a hand-written `evaluate`. +pub struct ProverEvalFolder<'a, F, E> +where + F: IsSubFieldOf, + E: IsField, +{ + frame: &'a Frame, + periodic: &'a [FieldElement], + challenges: &'a [FieldElement], + alphas: &'a [FieldElement], + logup_table_offset: &'a FieldElement, + base_out: &'a mut [FieldElement], + ext_out: &'a mut [FieldElement], + tracker: EmitTracker, +} + +impl<'a, F, E> ProverEvalFolder<'a, F, E> +where + F: IsSubFieldOf, + E: IsField, +{ + /// Build a folder from the Prover context variant. `base_out` must be + /// sized `num_base`; `ext_out` must be sized to the total constraint + /// count (matching the engine's `compute_transition_prover` contract). + /// + /// Panics if `ctx` is the Verifier variant. + pub fn new( + ctx: &TransitionEvaluationContext<'a, F, E>, + base_out: &'a mut [FieldElement], + ext_out: &'a mut [FieldElement], + ) -> Self { + let TransitionEvaluationContext::Prover { + frame, + periodic_values, + rap_challenges, + logup_alpha_powers, + logup_table_offset, + .. + } = ctx + else { + unreachable!("ProverEvalFolder::new called with a Verifier context") + }; + let num_constraints = base_out.len().max(ext_out.len()); + Self { + frame, + periodic: periodic_values, + challenges: rap_challenges, + alphas: logup_alpha_powers, + logup_table_offset, + base_out, + ext_out, + tracker: EmitTracker::new(num_constraints), + } + } + + /// Debug-build check that every constraint index was emitted exactly + /// once (no-op in release builds). Call after running a body. + pub fn assert_all_emitted(&self) { + self.tracker.assert_complete(); + } +} + +impl ConstraintBuilder for ProverEvalFolder<'_, F, E> +where + F: IsSubFieldOf, + E: IsField, +{ + type Expr = FieldElement; + type ExprE = FieldElement; + + fn main(&self, offset: usize, col: usize) -> FieldElement { + self.frame + .get_evaluation_step(offset) + .get_main_evaluation_element(0, col) + .clone() + } + fn aux(&self, offset: usize, col: usize) -> FieldElement { + self.frame + .get_evaluation_step(offset) + .get_aux_evaluation_element(0, col) + .clone() + } + fn periodic(&self, idx: usize) -> FieldElement { + self.periodic[idx].clone() + } + fn challenge(&self, idx: usize) -> FieldElement { + self.challenges[idx].clone() + } + fn alpha_pow(&self, idx: usize) -> FieldElement { + self.alphas[idx].clone() + } + fn table_offset(&self) -> FieldElement { + self.logup_table_offset.clone() + } + fn const_base(&self, v: u64) -> FieldElement { + FieldElement::::from(v) + } + fn const_signed(&self, v: i64) -> FieldElement { + FieldElement::::from(v) + } + + fn emit_base(&mut self, constraint_idx: usize, e: FieldElement) { + self.tracker.mark(constraint_idx); + self.base_out[constraint_idx] = e; + } + fn emit_ext(&mut self, constraint_idx: usize, e: FieldElement) { + debug_assert!( + constraint_idx >= self.base_out.len(), + "emit_ext with a base-prefix index {constraint_idx}" + ); + self.tracker.mark(constraint_idx); + self.ext_out[constraint_idx] = e; + } +} + +// ============================================================================= +// 2. VerifierEvalFolder — same body at the OOD point (all-extension frame) +// ============================================================================= + +/// Direct evaluation at the OOD point: the frame holds only extension +/// elements, so `Expr = FieldElement` and base-constraint results are +/// already extension values. `const_base` embeds via +/// `FieldElement::::from(v).to_extension::()`; `emit_base` writes the +/// (already promoted) value into `ext_evals[idx]`, mirroring the old +/// adapter's `evaluate(..).to_extension()` promotion. Runs once per proof at +/// the OOD point; this exact monomorphization, compiled into the guest +/// binary, is the recursion-guest path. +pub struct VerifierEvalFolder<'a, F, E> +where + F: IsSubFieldOf, + E: IsField, +{ + frame: &'a Frame, + periodic: &'a [FieldElement], + challenges: &'a [FieldElement], + alphas: &'a [FieldElement], + logup_table_offset: &'a FieldElement, + ext_out: &'a mut [FieldElement], + tracker: EmitTracker, + _base_field: PhantomData, +} + +impl<'a, F, E> VerifierEvalFolder<'a, F, E> +where + F: IsSubFieldOf, + E: IsField, +{ + /// Build a folder from the Verifier context variant. `ext_out` must be + /// sized to the total constraint count (matching the engine's + /// `compute_transition` contract). + /// + /// Panics if `ctx` is the Prover variant. + pub fn new( + ctx: &TransitionEvaluationContext<'a, F, E>, + ext_out: &'a mut [FieldElement], + ) -> Self { + let TransitionEvaluationContext::Verifier { + frame, + periodic_values, + rap_challenges, + logup_alpha_powers, + logup_table_offset, + .. + } = ctx + else { + unreachable!("VerifierEvalFolder::new called with a Prover context") + }; + let num_constraints = ext_out.len(); + Self { + frame, + periodic: periodic_values, + challenges: rap_challenges, + alphas: logup_alpha_powers, + logup_table_offset, + ext_out, + tracker: EmitTracker::new(num_constraints), + _base_field: PhantomData, + } + } + + /// Debug-build check that every constraint index was emitted exactly + /// once (no-op in release builds). Call after running a body. + pub fn assert_all_emitted(&self) { + self.tracker.assert_complete(); + } +} + +impl ConstraintBuilder for VerifierEvalFolder<'_, F, E> +where + F: IsSubFieldOf, + E: IsField, +{ + type Expr = FieldElement; + type ExprE = FieldElement; + + fn main(&self, offset: usize, col: usize) -> FieldElement { + self.frame + .get_evaluation_step(offset) + .get_main_evaluation_element(0, col) + .clone() + } + fn aux(&self, offset: usize, col: usize) -> FieldElement { + self.frame + .get_evaluation_step(offset) + .get_aux_evaluation_element(0, col) + .clone() + } + fn periodic(&self, idx: usize) -> FieldElement { + self.periodic[idx].clone() + } + fn challenge(&self, idx: usize) -> FieldElement { + self.challenges[idx].clone() + } + fn alpha_pow(&self, idx: usize) -> FieldElement { + self.alphas[idx].clone() + } + fn table_offset(&self) -> FieldElement { + self.logup_table_offset.clone() + } + fn const_base(&self, v: u64) -> FieldElement { + FieldElement::::from(v).to_extension::() + } + fn const_signed(&self, v: i64) -> FieldElement { + FieldElement::::from(v).to_extension::() + } + + fn emit_base(&mut self, constraint_idx: usize, e: FieldElement) { + self.tracker.mark(constraint_idx); + self.ext_out[constraint_idx] = e; + } + fn emit_ext(&mut self, constraint_idx: usize, e: FieldElement) { + self.tracker.mark(constraint_idx); + self.ext_out[constraint_idx] = e; + } +} + +// ============================================================================= +// 3. CaptureBuilder — owned expression tree, flattened into the flat IR +// ============================================================================= + +/// One node of the capture tree. `degree` is eager (leaf var/periodic = 1, +/// constants/uniforms = 0, mul sums, add/sub max, neg passthrough — p3's +/// `degree_multiple`). +struct TreeNode { + kind: TreeKind, + dim: Dim, + degree: usize, +} + +enum TreeKind { + Main { + offset: u8, + col: u16, + }, + Aux { + offset: u8, + col: u16, + }, + Periodic(u16), + Challenge(u16), + AlphaPow(u16), + TableOffset, + /// Raw `u64` base-field constant; canonicalized (and value-deduplicated) + /// by the [`IrBuilder`] at flatten time. + ConstBase(u64), + /// Raw `i64` base-field constant; negatives map to `p - |v|` at flatten + /// time, exactly as `IrBuilder::const_signed`. + ConstSigned(i64), + Add(IrExpr, IrExpr), + Sub(IrExpr, IrExpr), + Mul(IrExpr, IrExpr), + Neg(IrExpr), +} + +/// Owned capture expression: `Rc` tree with operator overloading. Cloning is +/// a pointer bump; operators allocate nodes — no arena, no interior +/// mutability, no hashing (CSE happens at flatten time via [`IrBuilder`]). +/// Constants carry raw integers, so the tree needs no field type parameters. +#[derive(Clone)] +pub struct IrExpr(Rc); + +impl IrExpr { + fn leaf(kind: TreeKind, dim: Dim, degree: usize) -> Self { + IrExpr(Rc::new(TreeNode { kind, dim, degree })) + } + + fn join(a: Dim, b: Dim) -> Dim { + match (a, b) { + (Dim::Base, Dim::Base) => Dim::Base, + _ => Dim::Ext, + } + } + + fn binop(f: fn(IrExpr, IrExpr) -> TreeKind, degree: usize, a: IrExpr, b: IrExpr) -> Self { + let dim = Self::join(a.0.dim, b.0.dim); + IrExpr(Rc::new(TreeNode { + kind: f(a, b), + dim, + degree, + })) + } + + /// The tree-measured constraint degree (multivariate, in trace columns). + pub fn degree(&self) -> usize { + self.0.degree + } +} + +impl Add for IrExpr { + type Output = IrExpr; + fn add(self, rhs: IrExpr) -> IrExpr { + let d = self.0.degree.max(rhs.0.degree); + IrExpr::binop(TreeKind::Add, d, self, rhs) + } +} +impl Sub for IrExpr { + type Output = IrExpr; + fn sub(self, rhs: IrExpr) -> IrExpr { + let d = self.0.degree.max(rhs.0.degree); + IrExpr::binop(TreeKind::Sub, d, self, rhs) + } +} +impl Mul for IrExpr { + type Output = IrExpr; + // The degree of a product is the SUM of the factor degrees. + #[allow(clippy::suspicious_arithmetic_impl)] + fn mul(self, rhs: IrExpr) -> IrExpr { + let d = self.0.degree + rhs.0.degree; + IrExpr::binop(TreeKind::Mul, d, self, rhs) + } +} +impl Neg for IrExpr { + type Output = IrExpr; + fn neg(self) -> IrExpr { + let (dim, degree) = (self.0.dim, self.0.degree); + IrExpr(Rc::new(TreeNode { + kind: TreeKind::Neg(self), + dim, + degree, + })) + } +} + +/// Captures every emitted constraint into a [`ConstraintProgram`] by +/// flattening the finished trees into an [`IrBuilder`] (whose hash-consing +/// provides structural CSE, host-side, once at setup). Also records each +/// root's tree-measured degree — the degree-measurement API backing the +/// declared-vs-measured gate. +pub struct CaptureBuilder { + ir: IrBuilder, + /// `(constraint_idx, tree-measured degree)` per emit. + degrees: Vec<(usize, usize)>, +} + +impl Default for CaptureBuilder { + fn default() -> Self { + Self::new() + } +} + +impl CaptureBuilder { + pub fn new() -> Self { + Self { + ir: IrBuilder::new(), + degrees: Vec::new(), + } + } + + fn flatten(&mut self, e: &IrExpr) -> crate::constraint_ir::Expr { + match &e.0.kind { + TreeKind::Main { offset, col } => self.ir.main(*offset, *col as usize), + TreeKind::Aux { offset, col } => self.ir.aux(*offset, *col as usize), + TreeKind::Periodic(idx) => self.ir.periodic(*idx as usize), + TreeKind::Challenge(idx) => self.ir.challenge(*idx as usize), + TreeKind::AlphaPow(idx) => self.ir.alpha_power(*idx as usize), + TreeKind::TableOffset => self.ir.table_offset(), + TreeKind::ConstBase(v) => self.ir.const_base(*v), + TreeKind::ConstSigned(v) => self.ir.const_signed(*v), + TreeKind::Add(a, b) => { + let (fa, fb) = (self.flatten(a), self.flatten(b)); + self.ir.add(fa, fb) + } + TreeKind::Sub(a, b) => { + let (fa, fb) = (self.flatten(a), self.flatten(b)); + self.ir.sub(fa, fb) + } + TreeKind::Mul(a, b) => { + let (fa, fb) = (self.flatten(a), self.flatten(b)); + self.ir.mul(fa, fb) + } + TreeKind::Neg(a) => { + let fa = self.flatten(a); + self.ir.neg(fa) + } + } + } + + /// Finish capture: `(program, per-emit tree-measured degrees)`. + pub fn finish(self, num_base: usize) -> (ConstraintProgram, Vec<(usize, usize)>) { + (self.ir.finish(num_base), self.degrees) + } +} + +impl ConstraintBuilder for CaptureBuilder { + type Expr = IrExpr; + type ExprE = IrExpr; + + fn main(&self, offset: usize, col: usize) -> IrExpr { + IrExpr::leaf( + TreeKind::Main { + offset: offset as u8, + col: col as u16, + }, + Dim::Base, + 1, + ) + } + fn aux(&self, offset: usize, col: usize) -> IrExpr { + IrExpr::leaf( + TreeKind::Aux { + offset: offset as u8, + col: col as u16, + }, + Dim::Ext, + 1, + ) + } + fn periodic(&self, idx: usize) -> IrExpr { + IrExpr::leaf(TreeKind::Periodic(idx as u16), Dim::Base, 1) + } + fn challenge(&self, idx: usize) -> IrExpr { + IrExpr::leaf(TreeKind::Challenge(idx as u16), Dim::Ext, 0) + } + fn alpha_pow(&self, idx: usize) -> IrExpr { + IrExpr::leaf(TreeKind::AlphaPow(idx as u16), Dim::Ext, 0) + } + fn table_offset(&self) -> IrExpr { + IrExpr::leaf(TreeKind::TableOffset, Dim::Ext, 0) + } + fn const_base(&self, v: u64) -> IrExpr { + IrExpr::leaf(TreeKind::ConstBase(v), Dim::Base, 0) + } + fn const_signed(&self, v: i64) -> IrExpr { + IrExpr::leaf(TreeKind::ConstSigned(v), Dim::Base, 0) + } + + fn emit_base(&mut self, constraint_idx: usize, 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); + self.degrees.push((constraint_idx, e.degree())); + } + fn emit_ext(&mut self, constraint_idx: usize, 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 new file mode 100644 index 000000000..3860a4588 --- /dev/null +++ b/crypto/stark/src/constraints/builder_tests.rs @@ -0,0 +1,441 @@ +//! Tests for the `ConstraintBuilder` framework: one sample [`ConstraintSet`] +//! (EqXor-shaped, IsBit-shaped and Add-carry-pair-shaped bodies, plus a +//! LogUp-shaped extension constraint) checked three ways on random rows: +//! +//! 1. `ProverEvalFolder` output == direct `FieldElement` arithmetic; +//! 2. `ProverEvalFolder` output == `eval_program` over the captured program; +//! 3. `VerifierEvalFolder` output == `eval_program_verifier` over the captured +//! program; +//! +//! plus: capture-measured degrees == declared `meta.degree`, the meta +//! Base-prefix/density invariants, and the folders' debug-build +//! exactly-once/completeness asserts. + +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as Ext; +use math::field::goldilocks::GoldilocksField as Fp; + +use crate::constraint_ir::{eval_program, eval_program_verifier}; +use crate::constraints::builder::{ + CaptureBuilder, ConstraintBuilder, ConstraintMeta, ConstraintSet, ProverEvalFolder, RootKind, + VerifierEvalFolder, num_base_from_meta, +}; +use crate::frame::Frame; +use crate::lookup::PackingShifts; +use crate::table::TableView; +use crate::traits::TransitionEvaluationContext; + +type FpE = FieldElement; +type ExtE = FieldElement; + +const TRIALS: usize = 1000; + +/// Deterministic SplitMix64. +struct SplitMix64(u64); +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + fn fp(&mut self) -> FpE { + FpE::from(self.next_u64()) + } + fn ext(&mut self) -> ExtE { + ExtE::from_raw([self.fp(), self.fp(), self.fp()]) + } +} + +// ============================================================================= +// The sample table: local column layout + single body +// ============================================================================= + +mod cols { + // EqXor: res = eq XOR invert. + pub const RES: usize = 0; + pub const EQ: usize = 1; + pub const INVERT: usize = 2; + // IsBit. + pub const BIT: usize = 3; + // Add carry pair (64-bit add split in 32-bit halves), gated by COND. + pub const COND: usize = 4; + pub const LHS_LO: usize = 5; + pub const LHS_HI: usize = 6; + pub const RHS_LO: usize = 7; + pub const RHS_HI: usize = 8; + pub const SUM_LO: usize = 9; + pub const SUM_HI: usize = 10; + pub const NUM_COLS: usize = 11; +} + +/// `2^-32` as a canonical Goldilocks `u64` (the add-carry repack constant). +fn inv_shift_32() -> u64 { + *FpE::from(1u64 << 32).inv().unwrap().value() +} + +/// Sample table: 4 base constraints + 1 LogUp-shaped extension constraint. +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 + ] + } + + fn eval>(&self, b: &mut B) { + // idx 0 — EqXor: 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). + let x = b.main(0, cols::BIT); + let one = b.one(); + b.emit_base(1, x.clone() * (one - x)); + + // idx 2, 3 — the add carry pair: + // carry_0 = (lhs.lo + rhs.lo − sum.lo)·2⁻³² + // carry_1 = (lhs.hi + rhs.hi + carry_0 − sum.hi)·2⁻³² + // emit cond·carry_i·(1 − carry_i). + let inv_2_32 = b.const_base(inv_shift_32()); + let lhs_lo = b.main(0, cols::LHS_LO); + let lhs_hi = b.main(0, cols::LHS_HI); + let rhs_lo = b.main(0, cols::RHS_LO); + let rhs_hi = b.main(0, cols::RHS_HI); + let sum_lo = b.main(0, cols::SUM_LO); + let sum_hi = b.main(0, cols::SUM_HI); + let cond = b.main(0, cols::COND); + 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; + 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. + let ch = b.challenge(0); + let au = b.aux(0, 0); + let alpha = b.alpha_pow(0); + let off = b.table_offset(); + b.emit_ext(4, (ch + au) * alpha - off); + } +} + +const NUM_BASE: usize = 4; +const NUM_CONSTRAINTS: usize = 5; + +/// Direct `FieldElement` arithmetic reference for the sample set's base +/// constraints on a main row. +fn direct_base(row: &[FpE]) -> [FpE; NUM_BASE] { + let two = FpE::from(2u64); + let one = FpE::one(); + let inv = FpE::from(1u64 << 32).inv().unwrap(); + + let c0 = row[cols::RES] + - (row[cols::EQ] + row[cols::INVERT] - two * row[cols::EQ] * row[cols::INVERT]); + let c1 = row[cols::BIT] * (one - row[cols::BIT]); + let carry_0 = (row[cols::LHS_LO] + row[cols::RHS_LO] - row[cols::SUM_LO]) * inv; + let carry_1 = (row[cols::LHS_HI] + row[cols::RHS_HI] + carry_0 - row[cols::SUM_HI]) * inv; + let c2 = row[cols::COND] * carry_0 * (one - carry_0); + let c3 = row[cols::COND] * carry_1 * (one - carry_1); + [c0, c1, c2, c3] +} + +/// Direct reference for the extension constraint. +fn direct_ext(aux0: &ExtE, challenge0: &ExtE, alpha0: &ExtE, offset: &ExtE) -> ExtE { + (*challenge0 + *aux0) * *alpha0 - *offset +} + +/// One random trial's inputs. +struct TrialData { + row: Vec, + aux0: ExtE, + challenge0: ExtE, + alpha0: ExtE, + offset: ExtE, +} + +fn random_trial(rng: &mut SplitMix64) -> TrialData { + TrialData { + row: (0..cols::NUM_COLS).map(|_| rng.fp()).collect(), + aux0: rng.ext(), + challenge0: rng.ext(), + alpha0: rng.ext(), + offset: rng.ext(), + } +} + +// ============================================================================= +// The three-way differential checks +// ============================================================================= + +#[test] +fn prover_folder_matches_direct_arithmetic() { + let shifts = PackingShifts::::new(); + let mut rng = SplitMix64(0x0001_F01D_u64 ^ 0xABCD); + for trial in 0..TRIALS { + let t = random_trial(&mut rng); + let step = TableView::::new(vec![t.row.clone()], vec![vec![t.aux0]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let challenges = vec![t.challenge0]; + let alphas = vec![t.alpha0]; + let ctx = TransitionEvaluationContext::new_prover( + &frame, + &periodic, + &challenges, + &alphas, + &t.offset, + &shifts, + ); + + let mut base_out = vec![FpE::zero(); NUM_BASE]; + let mut ext_out = vec![ExtE::zero(); NUM_CONSTRAINTS]; + let mut folder = ProverEvalFolder::new(&ctx, &mut base_out, &mut ext_out); + SampleSet.eval(&mut folder); + folder.assert_all_emitted(); + + let expected_base = direct_base(&t.row); + for (i, expected) in expected_base.iter().enumerate() { + assert_eq!(&base_out[i], expected, "base constraint {i}, trial {trial}"); + } + let expected_ext = direct_ext(&t.aux0, &t.challenge0, &t.alpha0, &t.offset); + assert_eq!(ext_out[4], expected_ext, "ext constraint, trial {trial}"); + } +} + +#[test] +fn prover_folder_matches_interpreted_capture() { + // Capture once (setup-time), interpret per row. + let mut cb = CaptureBuilder::::new(); + SampleSet.eval(&mut cb); + let (prog, _degrees) = cb.finish(NUM_BASE); + + let shifts = PackingShifts::::new(); + let mut rng = SplitMix64(0x0002_F01D_u64 ^ 0xABCD); + for trial in 0..TRIALS { + let t = random_trial(&mut rng); + let step = TableView::::new(vec![t.row.clone()], vec![vec![t.aux0]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let challenges = vec![t.challenge0]; + let alphas = vec![t.alpha0]; + let ctx = TransitionEvaluationContext::new_prover( + &frame, + &periodic, + &challenges, + &alphas, + &t.offset, + &shifts, + ); + + let mut folder_base = vec![FpE::zero(); NUM_BASE]; + let mut folder_ext = vec![ExtE::zero(); NUM_CONSTRAINTS]; + let mut folder = ProverEvalFolder::new(&ctx, &mut folder_base, &mut folder_ext); + SampleSet.eval(&mut folder); + folder.assert_all_emitted(); + + let mut interp_base = vec![FpE::zero(); NUM_BASE]; + let mut interp_ext = vec![ExtE::zero(); NUM_CONSTRAINTS]; + eval_program(&prog, &ctx, &mut interp_base, &mut interp_ext); + + assert_eq!(folder_base, interp_base, "base evals, trial {trial}"); + assert_eq!(folder_ext[4], interp_ext[4], "ext eval, trial {trial}"); + } +} + +#[test] +fn verifier_folder_matches_interpreted_capture() { + let mut cb = CaptureBuilder::::new(); + SampleSet.eval(&mut cb); + let (prog, _degrees) = cb.finish(NUM_BASE); + + let shifts = PackingShifts::::new(); + let mut rng = SplitMix64(0x0003_F01D_u64 ^ 0xABCD); + for trial in 0..TRIALS { + let t = random_trial(&mut rng); + // The verifier frame holds only extension elements (OOD evaluations). + let row_e: Vec = t.row.iter().map(|x| x.to_extension()).collect(); + let step = TableView::::new(vec![row_e], vec![vec![t.aux0]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let challenges = vec![t.challenge0]; + let alphas = vec![t.alpha0]; + let ctx = TransitionEvaluationContext::::new_verifier( + &frame, + &periodic, + &challenges, + &alphas, + &t.offset, + &shifts, + ); + + let mut folder_ext = vec![ExtE::zero(); NUM_CONSTRAINTS]; + let mut folder = VerifierEvalFolder::new(&ctx, &mut folder_ext); + SampleSet.eval(&mut folder); + folder.assert_all_emitted(); + + let mut interp_ext = vec![ExtE::zero(); NUM_CONSTRAINTS]; + eval_program_verifier(&prog, &ctx, &mut interp_ext); + + assert_eq!(folder_ext, interp_ext, "ood evals, trial {trial}"); + } +} + +// ============================================================================= +// Degree measurement + meta invariants +// ============================================================================= + +#[test] +fn capture_measured_degrees_match_declared_meta() { + let mut cb = CaptureBuilder::::new(); + SampleSet.eval(&mut cb); + let (prog, degrees) = cb.finish(NUM_BASE); + assert!(prog.complete); + assert_eq!(prog.roots.len(), NUM_CONSTRAINTS); + + let meta = SampleSet.meta(); + assert_eq!(degrees.len(), meta.len()); + 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 + ); + } +} + +#[test] +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)]; + assert_eq!(num_base_from_meta(&pure_base), 2); + let pure_ext = vec![ConstraintMeta::ext(0, 1), ConstraintMeta::ext(1, 1)]; + assert_eq!(num_base_from_meta(&pure_ext), 0); + assert_eq!(num_base_from_meta(&[]), 0); + + // RootKind sanity on the sample. + let meta = SampleSet.meta(); + assert!(meta[..NUM_BASE].iter().all(|m| m.kind == RootKind::Base)); + assert!(meta[NUM_BASE..].iter().all(|m| m.kind == RootKind::Ext)); +} + +#[cfg(debug_assertions)] +#[test] +#[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), + ]; + num_base_from_meta(&bad); +} + +#[cfg(debug_assertions)] +#[test] +#[should_panic(expected = "dense and idx-ordered")] +fn meta_non_dense_panics() { + let bad = vec![ConstraintMeta::base(0, 1), ConstraintMeta::base(2, 1)]; + num_base_from_meta(&bad); +} + +// ============================================================================= +// Folder completeness asserts (debug builds) +// ============================================================================= + +/// Run a body that emits only constraint 0 of 2, then check completeness. +#[cfg(debug_assertions)] +#[test] +#[should_panic(expected = "never emitted")] +fn prover_folder_missing_emit_asserts() { + let shifts = PackingShifts::::new(); + let step = TableView::::new(vec![vec![FpE::zero(); cols::NUM_COLS]], vec![vec![]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let challenges: Vec = vec![]; + let alphas: Vec = vec![]; + let offset = ExtE::zero(); + let ctx = TransitionEvaluationContext::new_prover( + &frame, + &periodic, + &challenges, + &alphas, + &offset, + &shifts, + ); + + let mut base_out = vec![FpE::zero(); 2]; + let mut ext_out = vec![ExtE::zero(); 2]; + let mut folder = ProverEvalFolder::new(&ctx, &mut base_out, &mut ext_out); + let x = folder.main(0, 0); + folder.emit_base(0, x); // constraint 1 never emitted + folder.assert_all_emitted(); +} + +#[cfg(debug_assertions)] +#[test] +#[should_panic(expected = "emitted twice")] +fn prover_folder_double_emit_asserts() { + let shifts = PackingShifts::::new(); + let step = TableView::::new(vec![vec![FpE::zero(); cols::NUM_COLS]], vec![vec![]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let challenges: Vec = vec![]; + let alphas: Vec = vec![]; + let offset = ExtE::zero(); + let ctx = TransitionEvaluationContext::new_prover( + &frame, + &periodic, + &challenges, + &alphas, + &offset, + &shifts, + ); + + let mut base_out = vec![FpE::zero(); 2]; + let mut ext_out = vec![ExtE::zero(); 2]; + let mut folder = ProverEvalFolder::new(&ctx, &mut base_out, &mut ext_out); + let x = folder.main(0, 0); + folder.emit_base(0, x); + let x = folder.main(0, 0); + folder.emit_base(0, x); +} + +#[cfg(debug_assertions)] +#[test] +#[should_panic(expected = "never emitted")] +fn verifier_folder_missing_emit_asserts() { + let shifts = PackingShifts::::new(); + let step = TableView::::new(vec![vec![ExtE::zero(); cols::NUM_COLS]], vec![vec![]]); + let frame = Frame::::new(vec![step]); + let periodic: Vec = vec![]; + let challenges: Vec = vec![]; + let alphas: Vec = vec![]; + let offset = ExtE::zero(); + let ctx = TransitionEvaluationContext::::new_verifier( + &frame, + &periodic, + &challenges, + &alphas, + &offset, + &shifts, + ); + + let mut ext_out = vec![ExtE::zero(); 2]; + let mut folder = VerifierEvalFolder::new(&ctx, &mut ext_out); + let x = folder.main(0, 0); + folder.emit_base(1, x); + folder.assert_all_emitted(); +} diff --git a/crypto/stark/src/constraints/mod.rs b/crypto/stark/src/constraints/mod.rs index 3811523b5..589e726e3 100644 --- a/crypto/stark/src/constraints/mod.rs +++ b/crypto/stark/src/constraints/mod.rs @@ -1,3 +1,6 @@ pub mod boundary; +pub mod builder; +#[cfg(test)] +mod builder_tests; pub mod evaluator; pub mod transition; From 87ddd90b29e68270d36f457dc872ce7a51b429dd Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 1 Jul 2026 22:14:04 -0300 Subject: [PATCH 4/5] stark: zerofier evaluation as free functions of ConstraintMeta MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New module crypto/stark/src/constraints/zerofier.rs: the bodies of the TransitionConstraintEvaluator default methods (end_exemptions_roots, end_exemptions_lde_evaluations, zerofier_evaluations_on_extended_domain, evaluate_zerofier) relocated verbatim to free functions consuming plain ConstraintMeta — they only ever read the metadata getters. The trait defaults remain untouched and stay the production path until tables convert to ConstraintSet. Tests assert the free functions match the trait defaults bit-for-bit on a configurable boxed constraint across every branch: the default shape, end exemptions, period/offset combinations, and periodic exemptions with and without end exemptions, over both the LDE-domain and OOD entry points. --- crypto/stark/src/constraints/mod.rs | 1 + crypto/stark/src/constraints/zerofier.rs | 443 +++++++++++++++++++++++ 2 files changed, 444 insertions(+) create mode 100644 crypto/stark/src/constraints/zerofier.rs diff --git a/crypto/stark/src/constraints/mod.rs b/crypto/stark/src/constraints/mod.rs index 589e726e3..cf3921629 100644 --- a/crypto/stark/src/constraints/mod.rs +++ b/crypto/stark/src/constraints/mod.rs @@ -4,3 +4,4 @@ pub mod builder; mod builder_tests; pub mod evaluator; pub mod transition; +pub mod zerofier; diff --git a/crypto/stark/src/constraints/zerofier.rs b/crypto/stark/src/constraints/zerofier.rs new file mode 100644 index 000000000..debc0c389 --- /dev/null +++ b/crypto/stark/src/constraints/zerofier.rs @@ -0,0 +1,443 @@ +//! Zerofier evaluation as free functions of [`ConstraintMeta`]. +//! +//! These are the bodies of the `TransitionConstraintEvaluator` default +//! methods (`crate::constraints::transition`), relocated verbatim to consume +//! plain constraint metadata instead of trait getters — they only ever read +//! `period` / `offset` / `exemptions_period` / `periodic_exemptions_offset` / +//! `end_exemptions`. The engine's zerofier machinery moves onto these once +//! tables convert to [`ConstraintSet`](crate::constraints::builder::ConstraintSet); +//! until then the trait defaults remain the production path (equivalence is +//! asserted by the tests below). + +use core::ops::Div; + +use math::field::element::FieldElement; +use math::field::traits::{IsFFTField, IsField, IsSubFieldOf}; + +use crate::constraints::builder::ConstraintMeta; +use crate::domain::Domain; + +/// Roots of the end-exemptions polynomial `∏(x - rᵢ)`. +/// +/// The end-exemptions polynomial vanishes on the last `end_exemptions` rows +/// the constraint must skip. This returns its roots `rᵢ` so callers can +/// evaluate the product `∏(x - rᵢ)` directly at the points they need. +pub fn end_exemptions_roots( + meta: &ConstraintMeta, + trace_primitive_root: &FieldElement, + trace_length: usize, +) -> Vec> { + let end_exemptions = meta.end_exemptions; + if end_exemptions == 0 { + return Vec::new(); + } + // Last row in the constraint's evaluation domain is g^(offset + N - period); + // walking backward by g^period gives the remaining end-exemption roots. + let period = meta.period; + let decrement = trace_primitive_root.pow(trace_length - period); + let mut current = trace_primitive_root.pow(meta.offset + trace_length - period); + let mut roots = Vec::with_capacity(end_exemptions); + for _ in 0..end_exemptions { + roots.push(current.clone()); + current = ¤t * &decrement; + } + roots +} + +/// Evaluations of the end-exemptions polynomial `∏(x - rᵢ)` over the LDE +/// domain. +/// +/// The product has degree `end_exemptions` (≤ 2 in practice), so the direct +/// `O(N · end_exemptions)` product over the precomputed LDE coset is cheaper +/// than an `O(N log N)` FFT. With no exemptions this yields all ones. +pub fn end_exemptions_lde_evaluations( + meta: &ConstraintMeta, + domain: &Domain, +) -> Vec> { + let roots = end_exemptions_roots( + meta, + &domain.trace_primitive_root, + domain.trace_roots_of_unity.len(), + ); + domain + .lde_roots_of_unity_coset + .iter() + .map(|x| { + roots + .iter() + .fold(FieldElement::::one(), |acc, r| acc * (x - r)) + }) + .collect() +} + +/// Compute evaluations of the constraint's zerofier over a LDE domain. +/// +/// With no end exemptions the zerofier is cyclic, so a short period-length +/// vector is returned and the consumer cycles it (same contract as the trait +/// default this body was moved from). +#[allow(unstable_name_collisions)] +pub fn zerofier_evaluations_on_extended_domain( + meta: &ConstraintMeta, + domain: &Domain, +) -> Vec> { + let blowup_factor = domain.blowup_factor; + let trace_length = domain.trace_roots_of_unity.len(); + let trace_primitive_root = &domain.trace_primitive_root; + let coset_offset = &domain.coset_offset; + let lde_root_order = u64::from((blowup_factor * trace_length).trailing_zeros()); + let lde_root = F::get_primitive_root_of_unity(lde_root_order).unwrap(); + + // If there is an exemptions period defined for this constraint, the evaluations are calculated directly + // by computing P_exemptions(x) / Zerofier(x) + if let Some(exemptions_period) = meta.exemptions_period { + debug_assert!(exemptions_period.is_multiple_of(meta.period)); + debug_assert!(meta.periodic_exemptions_offset.is_some()); + + // The elements of the domain have order `trace_length * blowup_factor`, so the zerofier evaluations + // without the end exemptions, repeat their values after `blowup_factor * exemptions_period` iterations, + // so we only need to compute those. + let last_exponent = blowup_factor * exemptions_period; + let numerator_power = trace_length / exemptions_period; + let denominator_power = trace_length / meta.period; + let offset_exponent = + trace_length * meta.periodic_exemptions_offset.unwrap() / exemptions_period; + let numerator_offset = trace_primitive_root.pow(offset_exponent); + let denominator_offset = trace_primitive_root.pow(meta.offset * denominator_power); + let numerator_step = lde_root.pow(numerator_power); + let denominator_step = lde_root.pow(denominator_power); + let mut numerator_eval = coset_offset.pow(numerator_power); + let mut denominator_eval = coset_offset.pow(denominator_power); + + let mut numerators = Vec::with_capacity(last_exponent); + let mut denominators = Vec::with_capacity(last_exponent); + for _ in 0..last_exponent { + numerators.push(&numerator_eval - &numerator_offset); + denominators.push(&denominator_eval - &denominator_offset); + numerator_eval = &numerator_eval * &numerator_step; + denominator_eval = &denominator_eval * &denominator_step; + } + + // Batch inversion: O(3N) muls + 1 inversion instead of N individual inversions. + // Denominators are guaranteed non-zero because the sets of powers of + // `offset_times_x` and `trace_primitive_root` are disjoint, provided that the + // offset is neither an element of the interpolation domain nor part of a + // subgroup with order less than n. + FieldElement::inplace_batch_inverse(&mut denominators).unwrap(); + + let evaluations: Vec<_> = numerators + .iter() + .zip(denominators.iter()) + .map(|(num, denom_inv)| num * denom_inv) + .collect(); + + // Mirror the else-branch fast path: with no end exemptions the zerofier stays + // cyclic, so return the short period-length vector and let the consumer cycle. + if meta.end_exemptions == 0 { + return evaluations; + } + + let end_exemption_evaluations = end_exemptions_lde_evaluations(meta, domain); + + let cycled_evaluations = evaluations + .iter() + .cycle() + .take(end_exemption_evaluations.len()); + + core::iter::zip(cycled_evaluations, end_exemption_evaluations) + .map(|(eval, exemption_eval)| eval * exemption_eval) + .collect() + + // In this else branch, the zerofiers are computed as the numerator, then inverted + // using batch inverse and then multiplied by P_exemptions(x). This way we don't do + // useless divisions. + } else { + let last_exponent = blowup_factor * meta.period; + let denominator_power = trace_length / meta.period; + let denominator_offset = trace_primitive_root.pow(meta.offset * denominator_power); + let denominator_step = lde_root.pow(denominator_power); + let mut denominator_eval = coset_offset.pow(denominator_power); + + let mut evaluations = Vec::with_capacity(last_exponent); + for _ in 0..last_exponent { + evaluations.push(&denominator_eval - &denominator_offset); + denominator_eval = &denominator_eval * &denominator_step; + } + + FieldElement::inplace_batch_inverse(&mut evaluations).unwrap(); + + // Fast path: when end_exemptions == 0 there are no exemption roots, so + // the zerofier stays cyclic — return the short period-length vector + // directly instead of expanding it over the full LDE domain. + if meta.end_exemptions == 0 { + return evaluations; + } + + let end_exemption_evaluations = end_exemptions_lde_evaluations(meta, domain); + + let cycled_evaluations = evaluations + .iter() + .cycle() + .take(end_exemption_evaluations.len()); + + core::iter::zip(cycled_evaluations, end_exemption_evaluations) + .map(|(eval, exemption_eval)| eval * exemption_eval) + .collect() + } +} + +/// Evaluation of the constraint's zerofier at some point `z`, which may be in +/// a field extension. +#[allow(unstable_name_collisions)] +pub fn evaluate_zerofier( + meta: &ConstraintMeta, + z: &FieldElement, + trace_primitive_root: &FieldElement, + trace_length: usize, +) -> FieldElement +where + F: IsSubFieldOf, + E: IsField, +{ + let roots = end_exemptions_roots(meta, trace_primitive_root, trace_length); + // Factor `z - rᵢ` written as `-(rᵢ - z)`: the field ops only go + // subfield − superfield, and `rᵢ ∈ F`, `z ∈ E`. + let end_exemptions_eval = roots.iter().fold(FieldElement::::one(), |acc, root| { + acc * -(root.clone() - z.clone()) + }); + + if let Some(exemptions_period) = meta.exemptions_period { + debug_assert!(exemptions_period.is_multiple_of(meta.period)); + debug_assert!(meta.periodic_exemptions_offset.is_some()); + + let periodic_exemptions_offset = meta.periodic_exemptions_offset.unwrap(); + let offset_exponent = trace_length * periodic_exemptions_offset / exemptions_period; + + let numerator = + -trace_primitive_root.pow(offset_exponent) + z.pow(trace_length / exemptions_period); + let denominator = -trace_primitive_root.pow(meta.offset * trace_length / meta.period) + + z.pow(trace_length / meta.period); + // The denominator is non-zero: z is sampled outside the set of primitive roots. + return numerator + .div(denominator) + .expect("zerofier denominator is non-zero: z is sampled out-of-domain") + * &end_exemptions_eval; + } + + (-trace_primitive_root.pow(meta.offset * trace_length / meta.period) + + z.pow(trace_length / meta.period)) + .inv() + .unwrap() + * &end_exemptions_eval +} + +// ============================================================================= +// Equivalence tests: free functions == the trait defaults they were moved from +// ============================================================================= + +#[cfg(test)] +mod tests { + use super::*; + use crate::constraints::transition::TransitionConstraintEvaluator; + use crate::traits::TransitionEvaluationContext; + use math::fft::roots_of_unity::get_powers_of_primitive_root_coset; + use math::field::element::FieldElement; + use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as Ext; + use math::field::goldilocks::GoldilocksField as Fp; + + type FpE = FieldElement; + type ExtE = FieldElement; + + /// A boxed-path constraint whose zerofier shape is configurable — used to + /// run the ORIGINAL trait-default bodies for comparison. + struct DummyConstraint { + period: usize, + offset: usize, + exemptions_period: Option, + periodic_exemptions_offset: Option, + end_exemptions: usize, + } + + impl TransitionConstraintEvaluator for DummyConstraint { + fn degree(&self) -> usize { + 1 + } + fn constraint_idx(&self) -> usize { + 0 + } + fn evaluate_verifier( + &self, + _ctx: &TransitionEvaluationContext, + _evals: &mut [ExtE], + ) { + } + fn period(&self) -> usize { + self.period + } + fn offset(&self) -> usize { + self.offset + } + fn exemptions_period(&self) -> Option { + self.exemptions_period + } + fn periodic_exemptions_offset(&self) -> Option { + self.periodic_exemptions_offset + } + fn end_exemptions(&self) -> usize { + self.end_exemptions + } + } + + impl DummyConstraint { + fn meta(&self) -> ConstraintMeta { + let mut m = ConstraintMeta::base(0, 1) + .with_period(self.period) + .with_offset(self.offset) + .with_end_exemptions(self.end_exemptions); + if let Some(p) = self.exemptions_period { + m = m.with_exemptions(p, self.periodic_exemptions_offset.unwrap()); + } + m + } + } + + /// Hand-built prover Domain: trace length 16, blowup 4, coset offset 7. + fn sample_domain() -> Domain { + let trace_length: usize = 16; + let blowup_factor: usize = 4; + let coset_offset = FpE::from(7u64); + let root_order = trace_length.trailing_zeros(); + let trace_primitive_root = + ::get_primitive_root_of_unity(root_order as u64) + .unwrap(); + let trace_roots_of_unity = get_powers_of_primitive_root_coset( + root_order as u64, + trace_length, + &FieldElement::one(), + ) + .unwrap(); + let lde_root_order = (trace_length * blowup_factor).trailing_zeros(); + let lde_roots_of_unity_coset = get_powers_of_primitive_root_coset( + lde_root_order as u64, + trace_length * blowup_factor, + &coset_offset, + ) + .unwrap(); + Domain { + root_order, + lde_roots_of_unity_coset, + trace_primitive_root, + trace_roots_of_unity, + coset_offset, + blowup_factor, + interpolation_domain_size: trace_length, + } + } + + /// The zerofier configurations exercised: every branch of the moved + /// bodies (default; end exemptions; period/offset; periodic exemptions + /// with and without end exemptions). + fn sample_configs() -> Vec { + vec![ + // Every row, no exemptions (the common case). + DummyConstraint { + period: 1, + offset: 0, + exemptions_period: None, + periodic_exemptions_offset: None, + end_exemptions: 0, + }, + // End exemptions only. + DummyConstraint { + period: 1, + offset: 0, + exemptions_period: None, + periodic_exemptions_offset: None, + end_exemptions: 2, + }, + // Periodic constraint with offset. + DummyConstraint { + period: 2, + offset: 1, + exemptions_period: None, + periodic_exemptions_offset: None, + end_exemptions: 0, + }, + // Periodic constraint with offset and end exemptions. + DummyConstraint { + period: 4, + offset: 3, + exemptions_period: None, + periodic_exemptions_offset: None, + end_exemptions: 1, + }, + // Periodic exemptions (bit_flags-shaped), cyclic fast path. + DummyConstraint { + period: 1, + offset: 0, + exemptions_period: Some(4), + periodic_exemptions_offset: Some(3), + end_exemptions: 0, + }, + // Periodic exemptions + end exemptions. + DummyConstraint { + period: 1, + offset: 0, + exemptions_period: Some(4), + periodic_exemptions_offset: Some(1), + end_exemptions: 2, + }, + ] + } + + #[test] + fn lde_zerofier_evaluations_match_trait_defaults() { + let domain = sample_domain(); + for (i, c) in sample_configs().iter().enumerate() { + let expected = c.zerofier_evaluations_on_extended_domain(&domain); + let got = zerofier_evaluations_on_extended_domain(&c.meta(), &domain); + assert_eq!(got, expected, "config {i} mismatch"); + } + } + + #[test] + fn ood_zerofier_evaluations_match_trait_defaults() { + let domain = sample_domain(); + let trace_length = domain.trace_roots_of_unity.len(); + let root = &domain.trace_primitive_root; + // A few arbitrary OOD points with all three extension components set. + let zs = [ + ExtE::from_raw([FpE::from(123u64), FpE::from(456u64), FpE::from(789u64)]), + ExtE::from_raw([ + FpE::from(0xDEAD_BEEFu64), + FpE::from(0xCAFE_F00Du64), + FpE::from(0x1234_5678u64), + ]), + ]; + for (i, c) in sample_configs().iter().enumerate() { + for z in &zs { + let expected = c.evaluate_zerofier(z, root, trace_length); + let got = evaluate_zerofier(&c.meta(), z, root, trace_length); + assert_eq!(got, expected, "config {i} mismatch at z={z:?}"); + } + } + } + + #[test] + fn end_exemptions_helpers_match_trait_defaults() { + let domain = sample_domain(); + let trace_length = domain.trace_roots_of_unity.len(); + let root = &domain.trace_primitive_root; + for (i, c) in sample_configs().iter().enumerate() { + assert_eq!( + end_exemptions_roots(&c.meta(), root, trace_length), + c.end_exemptions_roots(root, trace_length), + "config {i} roots mismatch" + ); + assert_eq!( + end_exemptions_lde_evaluations(&c.meta(), &domain), + c.end_exemptions_lde_evaluations(&domain), + "config {i} lde evaluations mismatch" + ); + } + } +} From e72e1b3c2f972bd1970f2563c33f3f577612184d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 1 Jul 2026 23:14:40 -0300 Subject: [PATCH 5/5] docs(gpu-constraint-eval): single-source constraints plan + constraint front-end survey --- .../impl-plan-single-source-constraints.md | 503 ++++++++++++++++++ .../survey-constraint-frontends.md | 162 ++++++ 2 files changed, 665 insertions(+) create mode 100644 thoughts/gpu-constraint-eval/impl-plan-single-source-constraints.md create mode 100644 thoughts/gpu-constraint-eval/survey-constraint-frontends.md diff --git a/thoughts/gpu-constraint-eval/impl-plan-single-source-constraints.md b/thoughts/gpu-constraint-eval/impl-plan-single-source-constraints.md new file mode 100644 index 000000000..041690b0a --- /dev/null +++ b/thoughts/gpu-constraint-eval/impl-plan-single-source-constraints.md @@ -0,0 +1,503 @@ +# Implementation plan: single-source constraints (Phase 2.5, PRs A + B) + +**Audience: the implementing agent.** Self-contained: read this + the referenced code +and you can build it without the design discussion that produced it. All file:line +refs verified on branch `spike/constraint-ir-builder-part2` (PR #757, head of the +constraint-IR stack: #739 = Part 1, #757 = Part 2). + +**Companion docs** (context, not required reading to implement): +- `survey-constraint-frontends.md` — how Plonky3/OpenVM/SP1/risc0/zisk/airbender do this. +- `roadmap.md` — the overall GPU-constraint-eval program (this plan = its Phase 2.5). +- `plan-generic-ir-fable.md` — superseded by this file. + +--- + +## 1. Goal and non-goals + +**Goal.** Every transition constraint is defined exactly **once**, and from that +single definition we derive: (a) the compiled CPU prover evaluation, (b) the +verifier evaluation at the OOD point (identical code path in the recursion guest), +(c) the flat IR (`ConstraintProgram`) that the CPU interpreter and the future GPU +kernel consume. Today every constraint is written **twice** (`evaluate` + +`capture`); that duplication is the thing being deleted. + +**Non-goals / hard constraints:** +- The stark engine **stays generic** over `, E>`. Do not + concretize the prover/verifier to Goldilocks. +- **Do not** make the interpreter the CPU proving path. This was measured + (2026-07-01, ABBA on the bench server, ethrex 20-transfer fixture, + `spike/constraint-ir-default-on` vs `spike/constraint-ir-builder-part2`): + interpreted constraint eval costs **~9% total prove time** (pairs: −8.54%, + −9.36%). The compiled folder path is mandatory. +- No DSL, no codegen, no checked-in generated files. +- Protocol semantics are untouchable: same constraints, same zerofier structure + (per-constraint period/offset/exemptions + grouped evaluation), same transcript. + Proofs must be **bit-for-bit identical** before/after (golden-proof gate below). +- The recursion guest (verifier compiled to RISC-V) must never hash and never + interpret: its constraint evaluation is the compiled folder. Capture (which + hash-conses) must not run on the guest path — see §4.6. + +## 2. Settled decisions (do not relitigate) + +| Decision | Choice | Why (evidence) | +|---|---|---| +| Single-source mechanism | One generic body per **table**, `fn eval` | The Plonky3/SP1/OpenVM `Air` pattern (survey §1-3); object-safety handled by monomorphizing inside concrete impls, so `&dyn AIR` keeps working | +| CPU prover path | Compiled `EvalFolder` (re-run body per row) | Bench: interpreter = −9% prove time; p3+SP1 do the same | +| GPU path | Capture → flat `ConstraintProgram` → device interpreter (roadmap Phase 4) | The whole point of the program; OpenVM/zisk-validated | +| Per-constraint objects | **Deleted.** Constraints are expressions emitted by the table body; metadata is plain data (`Vec`) | Simplest model; removes `Vec>`, the adapter, `boxed()`, per-constraint structs | +| Constants in the IR | Side tables (`Op::ConstBase(u32)` → `base_consts: Vec>`) | Keeps `Op` POD `Copy+Eq+Hash` with zero bounds on F; `IsField::BaseType` has no Eq/Hash (`crypto/math/src/field/traits.rs:101`), and `FieldElement`'s derived-Hash/manual-Eq disagree on non-canonical reps (`element.rs:47`, `goldilocks.rs:411`) — inline constants would poison the CSE map's key type | +| "FieldConsts" associated consts (roadmap §2.5 step 1) | **Not needed** | Every residue-using constraint is concretely `` (`prover/src/constraints/templates.rs:81,543`, `cpu.rs:112-749`); field-generic code (lookup.rs) uses only structural u64/i64 constants that `FieldElement::::from` handles for any field | +| `degree()` | Stays **declared**, in `ConstraintMeta`; host-side test asserts declared == measured-from-IR | Measuring requires capture; capture must not run in the guest (verifier needs `composition_poly_degree_bound`, `lookup.rs:1006-1020`) | +| CSE / hashing | Only in the flatten step (existing `IrBuilder` hash-consing), host-side, once per AIR, lazily | p3 doesn't CSE at all; OpenVM only Arc-identity. Guest never flattens | +| Emission order | Explicit `constraint_idx` everywhere (`emit_*` takes idx; meta is idx-ordered) | Order/index alignment is load-bearing in every surveyed system; we keep it explicit + debug-assert completeness | + +## 3. Architecture (end state) + +``` +per table (e.g. eq.rs): + EqConstraints (small struct: nothing or col config) + ├─ fn meta(&self) -> Vec // idx-ordered metadata, plain data + └─ fn eval>(&self, b) // THE single body: emits every constraint + +framework (lookup.rs): LogUp constraints emitted the same way, generated from the + interaction config (single definitions = today's capture helpers, generalized) + +three interpretations of the same body: + ProverEvalFolder Expr = FieldElement → per LDE row, compiled (CPU prover hot path) + VerifierEvalFolder Expr = FieldElement → once at OOD point (verifier + recursion guest) + CaptureBuilder Expr = owned expr tree → once at setup, host (flatten → ConstraintProgram) + ├─ CPU interpreter (tests / GPU parity) + └─ GPU lowering (Phase 4) + +engine (unchanged shape): &dyn AIR; AirWithBuses stores the table's ConstraintSet + + Vec; zerofier machinery reads meta; one virtual call per row per table. +``` + +## 4. PR A — generic IR + +Self-contained first PR. Makes `constraint_ir` generic so `CaptureBuilder` can +target it for any field and the `unsafe` bridge dies. **Behavior identical** — +gates are bit-for-bit. + +### 4A.1 `crypto/stark/src/constraint_ir/ir.rs` +- Rename `Dim::{D1, D3}` → `Dim::{Base, Ext}`. +- Replace `Op::Const1(u64)` / `Op::Const3([u64;3])` with `Op::ConstBase(u32)` / + `Op::ConstExt(u32)` — indices into new fields on the program: + ```rust + pub struct ConstraintProgram { + pub nodes: Vec, // Op stays Copy+Eq+Hash (u32 payloads only) + pub dims: Vec, + pub base_consts: Vec>, + pub ext_consts: Vec>, + pub roots: Vec, + pub num_base: usize, + pub complete: bool, + } + ``` +- Bounds: `F: IsField, E: IsField` only. Default type params = Goldilocks tower so + existing concrete code compiles unchanged during migration. +- Verified: `Const1`/`Const3`/`const_ext` have **zero** users outside + `constraint_ir/` (including tests), so the const redesign is module-contained. + +### 4A.2 `crypto/stark/src/constraint_ir/builder.rs` +- `IrBuilder`; fields gain + `base_consts`/`ext_consts`; delete `const_cache: HashMap`. +- `const_base(v: u64)` / `const_signed(v: i64)`: `FieldElement::::from(v)` + (generic `From` exists, `element.rs:149`), then intern. +- `intern_base(fe)`: linear scan `base_consts.iter().position(|c| c == &fe)` + (PartialEq → `F::eq`, canonicalizing — exact dedup, no Hash needed; tables are + tiny and this runs once at setup), push if absent, then + `push(Op::ConstBase(idx), Dim::Base)` (the `(Op, Dim)` cse map is unchanged — + `Op` is still POD). Same for `intern_ext`. +- `const_ext` signature becomes `const_ext(v: FieldElement)`. +- Keep id-0 convention: `new()` interns zero first → node 0 = `ConstBase(0)`, + `base_consts[0] = 0`. Node ids are assigned in first-use order exactly as + today ⇒ **node counts in `prover/src/tests/constraint_ir_tests.rs` must not + change** (product_zero 4, is_bit_uncond 5, is_bit_cond 7, add_carry_0 14, + add_carry_1 21; full-table: CPU 616 nodes / EQ 142). + +### 4A.3 trait plumbing (temporary — PR B replaces it) +- `Capture` in `constraint_ir/mod.rs:43`; + `TransitionConstraintEvaluator::capture(&self, b: &mut IrBuilder)` + (`constraints/transition.rs:40`) — object-safe (F,E are trait params; precedent: + `evaluate_verifier` already takes `&TransitionEvaluationContext`). + With the default type params, the ~35 concrete `impl Capture for …` in the + prover crate compile **unchanged**. `AIR::constraint_program()` + (`traits.rs:330`) returns `ConstraintProgram`. +- lookup.rs capture helpers (`capture_multiplicity` etc., `lookup.rs:1733-1997`) + and the two LogUp `capture` overrides (`lookup.rs:2130,2336`) gain ``. + +### 4A.4 `crypto/stark/src/constraint_ir/interp.rs` + delete the bridge +- `Value { Base(FieldElement), Ext(FieldElement) }` — `Clone`, not + `Copy` (not provable for generic F); use `.clone()`; for Goldilocks these + compile to register copies. +- `eval_program` / `eval_program_verifier` / `eval_program_base` become generic + `, E: IsField>` (add `IsFFTField`/`'static`/`Send+Sync` only + if call sites force it). Const resolution reads the side tables (no more + per-row `Fp::from` re-reduction). +- **Delete `constraint_ir/bridge.rs`** (99 lines, all the module's `unsafe`). +- `constraints/evaluator.rs`: field becomes + `Option>` (line 30); the hook at + lines 110-125 loses the `ran` fallback boolean — call `eval_program` directly + when the program is `Some`. The `complete:false → None` guard at :239-243 stays. +- `verifier.rs:254-274`: call `eval_program_verifier` directly; keep the + `prog.complete` boxed fallback. + +### 4A.5 PR A gates +- `cargo test -p lambda-vm-prover constraint_ir_tests -- --nocapture` — node + counts + full-table prover/verifier diff gates bit-identical. +- `cargo test --release -p lambda-vm-prover --features stark/constraint-ir` + (incl. `test_prove_elfs_*`) and the default suite; `cargo test -p stark`. +- New test: capture+interpret over a non-Goldilocks tower (Stark252, `E = F`; + reflexive `IsSubFieldOf` impl at `traits.rs:28`) — proves the genericity. +- `grep -rn unsafe crypto/stark/src/constraint_ir/` → empty. +- `cargo fmt` + `cargo clippy` clean (required before every push). + +## 5. PR B — single-source constraints + +### 5.1 Step 0 — readability spike ✅ DONE (2026-07-01) + +**Outcome: operator style wins; the trait surface in §5.2 is PINNED.** Reference +implementation (concrete Goldilocks): branch `spike/constraint-builder-step0`, +commit `57ee832e` — `crypto/stark/src/constraints/builder.rs` + +`prover/src/tests/constraint_builder_spike.rs`. All differential gates passed +first try (EqXor / IsBit / Add-pair: ProverEvalFolder == old `evaluate::`, +VerifierEvalFolder == old `evaluate::`, capture→flatten→interpret == old +evaluate, 1000 rows each; tree-measured degree == declared). Ergonomics: clone +noise 2/1/2 per body (only for genuine reuse; Rc clone = pointer bump), **zero +`.into()`** (leaves return `Expr` directly — no `Var`/`Expr` split, dodging SP1's +noise), zero borrow-checker fights. Converted EqXor body, verbatim: + +```rust +let res = b.main(0, eq_cols::RES); +let eq = b.main(0, eq_cols::EQ); +let invert = b.main(0, eq_cols::INVERT); +let two = b.const_base(2); +b.emit_base(idx, res - (eq.clone() + invert.clone() - two * eq * invert)); +``` + +Bonus finding: emitting the Add lo/hi pair from ONE template function lets the +IrBuilder hash-consing share the whole `carry_0` subtree across the pair — 24 +nodes vs 14+21 for the old separate per-constraint captures. Per-table programs +will therefore be smaller than the sum of the Phase-0 per-constraint node counts; +**PR 2 gates compare folder-vs-interpreter values, never node counts.** + +### 5.2 Trait surface — PINNED by the spike (`crypto/stark/src/constraints/builder.rs`) + +Generic lift of the spike's concrete form (add ``, +`FieldElement`/`` for `Fp`/`Fp3`; the verifier folder's const embed needs +`F: IsSubFieldOf`): + +```rust +pub trait ExprOps: Sized + Clone + + Add + Sub + + Mul + Neg + + Add + Sub + Mul {} +// + blanket impl for any type meeting the bounds + +pub trait ExtExprOps: Sized + Clone + + Add + Sub + + Mul + Neg {} + +pub trait ConstraintBuilder { + type Expr: ExprOps; + type ExprE: ExtExprOps; + fn main(&self, offset: usize, col: usize) -> Self::Expr; + fn aux(&self, offset: usize, col: usize) -> Self::ExprE; + fn periodic(&self, idx: usize) -> Self::Expr; + fn challenge(&self, idx: usize) -> Self::ExprE; // rap_challenges[idx] + fn alpha_pow(&self, idx: usize) -> Self::ExprE; // logup_alpha_powers[idx] + fn table_offset(&self) -> Self::ExprE; // logup L/N + fn const_base(&self, v: u64) -> Self::Expr; // ONLY constant path + fn const_signed(&self, v: i64) -> Self::Expr; + fn one(&self) -> Self::Expr { self.const_base(1) } // keep these defaults + fn zero(&self) -> Self::Expr { self.const_base(0) } + fn emit_base(&mut self, constraint_idx: usize, e: Self::Expr); + fn emit_ext(&mut self, constraint_idx: usize, e: Self::ExprE); +} +``` + +Spike corrections to the original sketch (binding for PR 1b — do not deviate): +- The alias shape is `Expr: ExprOps` — cross-field ops live on the + **base** side with base always the LEFT operand (the field tower only + implements subfield∘superfield); `ExtExprOps` takes **no** type params. +- **No `From>` bound on `Expr`** — wrong for `VerifierEvalFolder` + where `Expr = FieldElement`; `const_base`/`const_signed` are the only + constant path (verifier folder: `FieldElement::::from(v).to_extension()`). +- `CaptureBuilder::finish(num_base)` returns + `(ConstraintProgram, Vec<(usize, usize)>)` — per-root (idx, measured + degree); this IS the degree-measurement API for gate §5.9.2. +- Concrete folder leaves use `*` derefs (clippy `clone_on_copy`); generic folders + use `.clone()` (no lint fires on generics). The capture tree's `Mul` needs + `#[allow(clippy::suspicious_arithmetic_impl)]` (degree = sum of operands). + +```rust +/// One table's constraints: metadata + THE single body. +pub trait ConstraintSet: Send + Sync { + fn meta(&self) -> Vec; // idx-ordered + fn eval>(&self, b: &mut B); // emits every constraint +} + +pub struct ConstraintMeta { + pub constraint_idx: usize, + pub kind: RootKind, // Base | Ext; Base entries MUST be a prefix + pub degree: usize, // declared; asserted == measured (test, §5.8) + pub period: usize, // default 1 + pub offset: usize, // default 0 + pub exemptions_period: Option, + pub periodic_exemptions_offset: Option, + pub end_exemptions: usize, // default 0 +} +``` +Invariants (debug-assert in the folders and at AIR construction): meta is dense +and idx-ordered; `kind == Base` entries form a prefix (this IS `num_base`, matching +the existing convention, `traits.rs:239-243`); `eval` emits **every** idx exactly +once (folders track a seen-bitset in debug builds). + +### 5.3 The three builder implementations (framework, written once) + +1. **`ProverEvalFolder<'a, F, E>`** — `Expr = FieldElement`, + `ExprE = FieldElement`. Constructed per row from the Prover + `TransitionEvaluationContext` (`traits.rs:73-95`) + output slices; leaves read + the frame exactly as `interp.rs:176-192` does today + (`frame.get_evaluation_step(offset).get_main_evaluation_element(0, col)`); + `emit_base` writes `base_evals[idx]`, `emit_ext` writes `ext_evals[idx]`. + All ops are plain `FieldElement` arithmetic — after inlining this is the same + machine code as today's `evaluate` bodies. **This is the CPU hot path.** +2. **`VerifierEvalFolder<'a, F, E>`** — `Expr = FieldElement` (the OOD frame is + `Frame`), `ExprE = FieldElement`; `const_base` embeds via + `FieldElement::::from(v).to_extension::()`; `emit_base` promotes and + writes `ext_evals[idx]` (mirrors `TransitionConstraintAdapter`, + `constraints/transition.rs:459`). Runs once at the OOD point. **This exact + monomorphization, compiled into the guest binary, is the recursion-guest + path — no capture, no hashing, no interpretation in-circuit.** +3. **`CaptureBuilder`** — `Expr`/`ExprE` = small owned tree + (`enum IrExpr { Leaf(...), Add(Rc, Rc), … }`, each node also + storing an eagerly-computed `degree` — leaf var 1, const 0, mul sums, add/sub + max, p3's `degree_multiple`). Operators allocate nodes — **no arena, no + RefCell, no thread-local, no hashing during capture**. `emit_*` flattens the + finished tree into the PR A `IrBuilder` (recursive walk; hash-consing + there = structural CSE, host-side) and records the root + measured degree. + Produces `ConstraintProgram` + measured degrees. + +### 5.4 Table conversion (the bulk — mechanical) + +Per table (17 production tables in `prover/src/tables/*.rs`): replace the +`*_constraints(idx_start) -> (Vec>, usize)` function with a +`XxxConstraints` struct implementing `ConstraintSet`. Recipe, using EQ +(`prover/src/tables/eq.rs:253-345`) as the model: + +```rust +pub struct EqConstraints; // holds col config only if the table needs it + +impl ConstraintSet for EqConstraints { + fn meta(&self) -> Vec { + let mut m = templates::add_pair_meta(0); // idx 0,1: b + diff = a + m.extend(templates::is_bit_meta(2, 1)); // idx 2: IS_BIT(invert) + m.push(ConstraintMeta::base(3, /*degree*/ 2)); // idx 3: res = eq XOR invert + m + } + fn eval>(&self, b: &mut B) { + templates::emit_add_pair(b, 0, vec![], AddOperand::dword(cols::B_0), + AddOperand::from_dword_hl(cols::DIFF_0), AddOperand::dword(cols::A_0)); + templates::emit_is_bit(b, 2, cols::INVERT, None); + let (res, eq, invert) = (b.main(0, cols::RES), b.main(0, cols::EQ), b.main(0, cols::INVERT)); + let two = b.const_base(2); + b.emit_base(3, res - (eq + invert - two * eq * invert)); + } +} +``` + +- **Templates become functions**: `AddConstraint`/`IsBitConstraint`/ + `ProductZeroConstraint`/the cpu.rs constraint structs + (`prover/src/constraints/{templates,cpu}.rs`) turn into `emit_*` + + `*_meta` function pairs in the same files. Their existing `capture` bodies are + the starting point for `emit_*` (they're already builder-call style); their + `evaluate` operator text is the readability reference. Delete both old bodies + and the structs' trait impls when each table converts. +- The multi-kind mega-constraints (Dvrm 11 kinds / Cpu32 8 / Shift 7 / Lt·Load·Mul 6) + convert the same way — their `compute()` loops are statically bounded and + already unrolled in the existing `capture` impls. +- Index bookkeeping: the old `idx_start` threading disappears; each table's meta + is self-contained 0..n. (LogUp indices are appended by the framework — §5.5.) + +### 5.5 LogUp (framework side, `crypto/stark/src/lookup.rs`) + +- Reduce `LookupBatchedTermConstraint` / `LookupAccumulatedConstraint` to plain + config data (a `LogUpLayout`: committed pairs, absorbed interactions, + `term_column_idx`s, `acc_column_idx`, `num_term_columns`) — this is exactly + what `AirWithBuses::new` already computes at `lookup.rs:858-880` + (`split_interactions`, absorbed slice). +- The single definitions are the **existing capture helpers** + (`capture_multiplicity`, `capture_linear_terms`, `capture_packing_fingerprint`, + `capture_fingerprint`, `lookup.rs:1733-1997`) generalized over + `B: ConstraintBuilder`, plus two `emit_logup_batched_term` / + `emit_logup_accumulated` functions transcribed from the current `capture` + overrides (`lookup.rs:2130`, `:2336` — including the 1-absorbed vs 2-absorbed + branches and the `aux(1, col)` next-row reads). +- **Delete** the `evaluate_*` twins (`evaluate_batched_term_constraint`, + `evaluate_accumulated_constraint`) and the two structs' boxed-trait impls + (`lookup.rs:2039-2196`, `:2197+`). +- Framework meta: reproduce the current structs' `period/offset/end_exemptions` + answers exactly (read them off the current impls before deleting). +- The runtime `BusValue::Linear` zero-skip optimization is already intentionally + not reproduced in capture (value-preserving; see the honesty note at + `lookup.rs:1725-1729`) — with one body this asymmetry disappears entirely; + verify the golden-proof gate still passes (it must: the skip is value-neutral). + +### 5.6 Engine rewiring + +- **`AirWithBuses`** (`lookup.rs:805-830`): gains a type param + `CS: ConstraintSet`; field `transition_constraints: Vec>` is + replaced by `constraint_set: CS`, `logup: LogUpLayout`, and + `meta: Vec` (= `cs.meta()` + framework-appended LogUp meta; + compute `num_base` from the Base-prefix). `new` (`lookup.rs:849`) takes the + `CS` value instead of the boxed vec; everything else it computes stays. +- **`AIR` trait** (`crypto/stark/src/traits.rs`): + - `transition_constraints()` (`:315-317`) — **deleted**. + - New: `fn constraints_meta(&self) -> &[ConstraintMeta]`. + - `compute_transition_prover` (`:255`) / `compute_transition` (`:224`) lose + their boxed-loop defaults and become required methods. `AirWithBuses` + implements them as one-liners into free generic helpers: + `run_transition_prover(&self.constraint_set, &self.logup, ctx, base, ext)` + (constructs `ProverEvalFolder`, runs `cs.eval` + `emit_logup_*`); same for + the verifier folder and for `constraint_program()` (capture + flatten, + **lazily, cached in a `OnceLock` — the guest never calls it**, see §5.7). + - `composition_poly_degree_bound` (`lookup.rs:1006-1020`): max over + `meta.degree` instead of `c.degree()`. +- **Zerofier machinery**: `transition_zerofier_evaluations_grouped` + (`traits.rs:343-370`) reads `ZerofierGroupKey` fields from + `constraints_meta()`; the big default methods + `zerofier_evaluations_on_extended_domain` / `evaluate_zerofier` / + `end_exemptions_*` (`constraints/transition.rs:127-337`) become free functions + of `(&ConstraintMeta, &Domain | z)` in a new `constraints/zerofier.rs` — they + only ever consumed the metadata getters (verified). Bodies move verbatim. +- **`ConstraintEvaluator`** (`constraints/evaluator.rs`): unchanged flow; the + `eval_row` hook calls `air.compute_transition_prover(&ctx, base_buf, transition_buf)` + as today (now one virtual call into the monomorphized folder run instead of 33). + The `constraint-ir` feature hook from PR A stays as the interpreter reference + path for tests/GPU parity — **off by default** (bench: −9%). +- **Delete**: `TransitionConstraintEvaluator`, `TransitionConstraintAdapter`, + `TransitionConstraint` (old signature), `Capture`, `boxed()` — + all of `constraints/transition.rs` except what moves to `zerofier.rs`. + +### 5.7 Guest-safety rule (recursion) + +The verifier path must run: AIR construction (no capture — `constraint_program` +is lazy and only the prover/GPU/tests force it) → `VerifierEvalFolder` at the OOD +point. Add a test or debug assertion that the verify path never constructs an +`IrBuilder` (e.g. feature-gate a counter, or simply grep-audit + document). +Degree is read from declared meta, so `composition_poly_degree_bound` needs no +capture. This preserves the no-HashMap-in-guest rule with zero special-casing. + +### 5.8 Examples + tests migration + +- The 13 example AIRs (`crypto/stark/src/examples/*.rs`) and + `tests/transition_tests.rs` implement `TransitionConstraintEvaluator` directly + today; each becomes a `ConstraintSet` impl (bodies are 1-3 trivial constraints) + + the three forwarding one-liners on their `AIR` impls. The + `complete: false` fallback machinery (`ConstraintProgram::complete`, + `IrBuilder::mark_unsupported`) can then be **retired** — every AIR captures. +- `prover/src/tests/constraint_ir_tests.rs`: the per-constraint Phase-0 diff + tests convert to compare `ProverEvalFolder` output vs interpreted program on + random rows (same assertion, derived from one body now). Full-table gates + unchanged in spirit: folder vs interpreter vs (during migration only) the old + boxed path. + +### 5.9 PR B gates — all must pass + +0. **Pre-flight, from the PR 1 fresh-eyes review (do these FIRST, before any + conversion):** + - `num_base` has two independent sources of truth — the interpreter routes by + `c < prog.num_base` (panics via `.as_base()` on mismatch) while the folders + route by which `emit_*` the body calls, and `CaptureBuilder::finish(num_base)` + takes it as a bare argument. Everywhere PR 2 wires these, the value MUST be + `num_base_from_meta(&meta)`, and add a test asserting it equals the captured + base-emit count (release-checked, not debug-only). + - Extend the folder↔capture differential test to cover an `aux(1, col)` + next-row read and a second alpha index — the real 1-/2-absorbed LogUp bodies + use both and the PR 1 sample body covers neither. +1. **Golden proofs** (the transcription safety net — this replaces the oracle + role the duplication accidentally provided): proofs are deterministic given + trace+params. Before starting conversion, record proof-bytes hashes for a + fixed ELF set (e.g. the `test_prove_elfs_*` inputs) on the pre-PR-B commit; + assert identical hashes after. Any slip in any constraint body changes the + composition polynomial and flips the hash. +2. **Degree assert**: for every table, measured degree (CaptureBuilder trees) == + declared `meta.degree`. +3. **Backend consistency**: folder vs interpreted `ConstraintProgram` on 1000 + random rows, every production table (extends the existing gate pattern). +4. Full suite: `cargo test --release -p lambda-vm-prover` (default) and with + `--features stark/constraint-ir`; `cargo test -p stark`. +5. **ABBA sanity** on the bench server (expect ≈ 0, possibly small win from + removing 33 virtual calls/row): + `scripts/bench_abba.sh origin/ origin/spike/constraint-ir-builder-part2 20`. +6. `cargo fmt` + `cargo clippy` before every push. No AI attribution anywhere + (commits, PR bodies) — repo rule. + +## 6. Sequencing, branch mechanics & PR packaging + +**The spike PRs (#737, #739, #757) are NOT merged and get closed** once the new +branches exist — the user wants human reviewers to see only the real design, +never the transitional scaffolding (bridge `unsafe`, `Capture`-alongside- +`evaluate` duplication, boxed adapter). Their branches stay in the remote as +provenance; close each with "superseded by the single-source constraints PRs; +code absorbed". **Work from their code, not their PRs**: develop on a branch cut +from `spike/constraint-ir-builder-part2` (it has the IR/interpreter/capture +bodies to absorb), but the PRs opened against `main` present the end state +fresh. + +Ship as **two PRs against main**, both containing only end-state code: + +- **PR 1 — framework** (≈ §4 + §5.2-5.3): `constraint_ir` module arriving + *already generic* (main never sees a concrete-Goldilocks IR or a bridge) + + `ConstraintBuilder` + `ProverEvalFolder`/`VerifierEvalFolder` + + `CaptureBuilder` + `ConstraintMeta` + zerofier free functions. Not wired into + production paths; fully exercised by its own tests (§4A.5 gates reshaped as + folder-vs-interpreter, the non-Goldilocks-tower test, spike-derived node-count + tests). Zero behavior change. +- **PR 2 — the switch** (≈ §5.4-5.9): all tables + LogUp converted, + `AirWithBuses`/`AIR`/zerofier rewired, old trait machinery deleted, golden + proofs byte-identical. Structure the commits per table group so the diff reads + as old-`evaluate`-deleted next to new-body-added in each file. + +Notes: +- The internal build order within the work branch can still follow §4 then §5 + (the PR A/PR B labels elsewhere in this doc = the work phases; PR 1/PR 2 = the + review packaging). The golden-proof baseline hashes are taken on `main` + immediately before PR 2's conversion starts. +- GPU work (roadmap Phase 4) consumes `ConstraintProgram` — stable after + PR 1 merges; it can proceed in parallel with PR 2. +- Housekeeping: close #737 now; close #739/#757 when PR 1 opens; delete the + bench branch `spike/constraint-ir-default-on` after PR 2 lands (keep it until + then for ABBA re-runs). + +## 7. What NOT to do (guardrails) + +- Do not interpret constraints in the CPU prover default path (−9%, measured). +- Do not put `FieldElement` values inside `Op` (breaks POD/CSE; §2 table). +- Do not introduce hashing, capture, or interpretation into the verifier path + (recursion guest). `VerifierEvalFolder` only. +- Do not change constraint semantics, indexing, zerofier structure, `num_base` + ordering, or anything transcript-visible — golden proofs must hold. +- Do not add a `degree`-measuring pass to the verifier; declared meta + host test. +- Do not build packed/SIMD folders, register allocation, or codec work now — + that's roadmap Phase 6, gated on GPU profiles. + +## 8. Current-code map (for orientation) + +| What | Where (verified) | +|---|---| +| IR + interpreter + builder + bridge | `crypto/stark/src/constraint_ir/{ir,interp,builder,bridge,mod}.rs` (758 lines total) | +| Boxed constraint trait + adapter + zerofier defaults | `crypto/stark/src/constraints/transition.rs` | +| Prover eval loop + IR hook | `crypto/stark/src/constraints/evaluator.rs:89-160` | +| Verifier OOD eval + IR hook | `crypto/stark/src/verifier.rs:241-274` | +| AIR trait (compute_transition*, zerofier grouping, constraint_program) | `crypto/stark/src/traits.rs:224-336,343-370` | +| AirWithBuses (the one production AIR) + LogUp constraints + capture helpers | `crypto/stark/src/lookup.rs:805+,965+,1733-2400` | +| Constraint templates + CPU constraints (evaluate/capture pairs) | `prover/src/constraints/{templates,cpu}.rs` | +| Table constraint builders (eq, lt, mul, dvrm, shift, …) | `prover/src/tables/*.rs` (e.g. `eq.rs:253-345`) | +| Existing diff-test gates | `prover/src/tests/constraint_ir_tests.rs` | +| Goldilocks residue constants | `prover/src/tables/types.rs:387-423` | +| Example AIRs (to migrate) | `crypto/stark/src/examples/*.rs` (13 files) | +| Bench harness | `scripts/bench_abba.sh` (runs on the bench server only) | diff --git a/thoughts/gpu-constraint-eval/survey-constraint-frontends.md b/thoughts/gpu-constraint-eval/survey-constraint-frontends.md new file mode 100644 index 000000000..7089ab8bd --- /dev/null +++ b/thoughts/gpu-constraint-eval/survey-constraint-frontends.md @@ -0,0 +1,162 @@ +# Survey: constraint front-ends across production STARK provers + +How six production systems **define constraints once** and derive CPU-prover eval, +verifier eval, recursion-guest eval, and the GPU form from that single definition. +Compiled 2026-07-01 from the reference clones in `others/` (agent-verified file:line +refs are into those clones). Companion to `plan-generic-ir-fable.md`, which turns +these findings into our design. + +Motivating question: lambda_vm currently hand-writes **two bodies per constraint** +(`evaluate` + `capture`). Is that ever necessary, and what should the single +source of truth look like? + +## The matrix + +| | Source of truth | CPU prover hot path | Verifier @ OOD | Recursion guest | GPU form | Dedup/CSE | +|---|---|---|---|---|---|---| +| **Plonky3** | one `Air::eval` body | re-run body per packed row (compiled folder) | re-run body, all-ext folder | — | — | none (tree = metadata only) | +| **OpenVM** | one `Air::eval` body | **interpret** captured DAG (self-documented as slower; AOT = future work) | interpret DAG | interpret DAG with circuit-var types | transpile DAG → 3-addr `u128` codec | Arc-pointer identity only | +| **SP1** | one `Air::eval` body | re-run body per packed row (compiled folder) | re-run body (folder) | re-run body, `Expr = SymbolicExt` DSL AST → staged straight-line circuit code | closed-source (moongate server) | — | +| **risc0** | Zirgen DSL (external tool) | generated straight-line C++/CUDA/Metal (old) or one shared C++ template (M3) | **interpret** compact SSA op-stream (`PolyExtStepDef`) | verifier compiled to ZKR bytecode on a micro-op VM | generated straight-line CUDA | generator's problem | +| **zisk** | PIL2 DSL | **interpret** bytecode, AVX-packed ×128 rows | interpret same bytecode, `domainSize=1`, all-ext | interpret (verify circuits are PIL airs) | interpret the **identical** bytecode in CUDA | compiler's problem | +| **airbender** | one imperative builder run | **interpret** deg-≤2 term-lists | generated straight-line Rust (checked-in, 9.5k lines) | generated straight-line (compiled) | flatten term-lists → metadata | none | + +## Per-project notes + +### Plonky3 (`others/Plonky3` — a fork; symbolic lives in `air/src/symbolic/`) +- `Air::eval(&mut AB)` is the one body (`air/src/air.rs:199`); associated types + `Expr: Algebra + Algebra`, `Var: Into + Copy` with explicit + `Add/Sub/Mul` bounds give **infix operators** (`air/src/builder.rs:12-43`). +- Folders: `ProverConstraintFolder` (`Expr = PackedVal`, SIMD, per quotient row, + `uni-stark/src/folder.rs:113`), `VerifierConstraintFolder` (`Expr = Challenge`, + once at ζ, Horner accumulate, `folder.rs:185,216`), `SymbolicAirBuilder` + (`Expr = SymbolicExpression`, once at setup, `symbolic/builder.rs:277`), + `DebugConstraintBuilder` (plain `F`, per trace row). +- Symbolic tree: `Arc` children, **no hash-consing, no CSE of any kind** — + used only for constraint count / degree (`degree_multiple` cached per node, + Mul sums, `symbolic/mod.rs:179`) / base-ext layout. Hot path never touches it. +- Selectors are builder methods (`is_first_row`/`is_transition`, `when_*` wraps a + `FilteredAirBuilder` that multiplies the condition in, `filtered.rs:60`) — no + per-constraint period/offset/exemptions metadata (ours is richer; keep ours). +- **Trap they document**: emission order is load-bearing — symbolic pass and + folder pass must agree on constraint indexing (`folder.rs:99`). + +### OpenVM (`others/openvm-stark-backend`) +- One body, run **once at keygen** by `SymbolicRapBuilder`; the captured DAG + (`SymbolicExpressionDag`, `dag.rs:51`) is stored in the proving key. Production + CPU quotient, verifier-at-OOD, and the CUDA transpiler are all **interpreters + of that DAG** — the body never runs in production again (only the debug builder + re-runs it). Their own README (`prover/cpu/quotient/README.md:13-28`) flags + interpreter overhead vs p3's compiled folders; AOT-compile is listed future work. +- Dedup = `Arc::ptr_eq` identity only (`dag.rs:140-208`); structurally identical + but separately built subtrees are NOT merged. +- Verifier folder is generic over `Var/Expr` precisely so a recursive verifier can + interpret the same DAG with circuit types (`verifier/folder.rs:33`); explicit + warning that the naive tree walk is exponential — use the linear DAG walk + (`folder.rs:127`). +- Interactions declared in-body (`push_interaction`); the framework generates the + LogUp constraints into the same constraint list (`interaction/rap.rs:28-43`) — + same architecture as our `BusInteraction` + framework constraints. +- **Gotchas to avoid**: GPU rules are re-transpiled+re-encoded on *every prove* + (`SymbolicRulesOnGpu::new` per call — cache per AIR instead); codec packs + constants as 32-bit (`as_canonical_u32`, `codec.rs:101-139`) — hard-assumes a + 31-bit field, doesn't fit Goldilocks. + +### SP1 (`others/sp1` = v6.2.1 hypercube, `others/sp1_4` = v4.2.1 FRI/quotient — mechanism identical) +- One `Air` body at the scale of hundreds of chips. CPU prover = compiled + packed folder per row-group (`sp1_4/crates/stark/src/quotient.rs:57-160`); + symbolic run happens once at chip construction for metadata only (degree is + **measured**, not declared — `chip.rs:83`). +- **The recursion answer**: `GenericVerifierConstraintFolder` + (`folder.rs:163`) instantiated with DSL types + (`Expr = SymbolicExt` — a 3-variant AST with operator overloading, + `recursion/compiler/src/ir/symbolic.rs:31`) so `chip.eval(&mut folder)` **stages + straight-line circuit code**. Zero hashing, zero interpretation in-circuit + (`recursion/circuit/src/constraints.rs:19-118`). v6 kept the exact pattern. +- **Ergonomics cost, visible at scale**: pervasive `.into()` / `.clone()` noise in + bodies (Expr isn't Copy), and the generic folder's trait bounds are enormous — + every `Add/Sub/Mul` combination spelled out per impl (`folder.rs:197-219`). +- No GPU constraint IR in public code (CUDA prover = closed gRPC server). + +### risc0 (`others/risc0` — Zirgen NOT in repo, only generated artifacts) +- Old style emits the **same constraint DAG four times** (Rust verifier bytecode + `poly_ext.rs` 923 KB + straight-line `poly_fp.cpp` 24.7k lines + `eval_check.cu` + + `.metal`); rv32im's `poly_ext.rs` is 1.05 MB, keccak's is **18.9 MB** — all + checked in; consistency rests on the external generator. M3 style collapses + witgen+eval into one Context-parametrized C++ template body. +- Verifier-side representation worth mirroring: `PolyExtStepDef` — a compact SSA + op-stream (`Const/Get/Add/Sub/Mul/AndEqz/AndCond` + taps metadata) interpreted + at the OOD point (`zkp/src/adapter.rs:156-233`). Recursion runs the verifier as + ZKR bytecode on a tiny micro-op VM (3 ops/cycle). +- Lesson: the codegen route costs an external toolchain, MB-scale generated files, + FFI boundaries, and slow iteration; the compact interpreted op-list for the + verifier is the part that aged well. + +### zisk / pil2-proofman (`others/zisk`, `others/pil2-proofman`) — our exact field (Goldilocks + cubic ext, LogUp) +- One PIL2-compiled `.bin` of expression programs; **three interpreters of the + identical artifact**: CPU (AVX2/AVX512, `NROWS_PACK=128`, + `expressions_pack.hpp:351-483`), CUDA (same `ops/args/numbers` uploaded, + same switch, shared-mem scratch, `expressions_gpu.cu:680-919`), verifier + (`domainSize=1`, all-extension, `stark_verify.hpp:310-351`). Zero codegen, + zero duplication; recursive verify circuits are themselves PIL airs. +- **Instruction encoding (production template for our device IR)**: 1 dim-signature + byte (dest/src dims ∈ {(1,1,1),(3,3,1),(3,3,3)}) + 8 `u16` args + `[arith_op, dest_pos, (type,pos,stride)×2]`, `u64` Goldilocks constant pool; + 4 arith ops (`add/sub/mul/sub_swap`). Rotations = per-operand `stride` index + into the openings table. LogUp compiles to ordinary expressions — no special + opcodes. +- Interpreter overhead is mitigated by 128-lane packing (dispatch amortized). + +### airbender (`others/airbender`) +- One imperative `Circuit`/`BasicAssembly` run authors constraints AND registers + witness resolvers in the same pass; lowered once to `CompiledCircuitArtifact` + (degree-≤2 term-lists — quadratic enforced at authoring, `constraint.rs:513`). + Four consumers derive from it: CPU prover interprets term-lists + (`prover/src/prover_stages/stage3.rs:629-683`), GPU flattener + (`stage_3_kernels.rs:102-172`), verifier **codegen** (checked-in 9,577-line + unrolled `evaluate_quotient`), witness codegen (CPU Rust + GPU `.cuh`). +- Recursion guest = the generated straight-line verifier — compiled, no hashing. +- **Caveat that argues for trait-instantiation over codegen**: the generated + verifier files are checked in and refreshed by a script (`recreate_verifiers.sh`) + — freshness depends on CI discipline, not the compiler. +- Degree-≤2 term-lists don't fit our degree-3 op-DAG (known from the roadmap). + +## Implications for lambda_vm + +1. **Nobody hand-writes two bodies.** Every system has one source of truth; our + `evaluate`+`capture` duplication is an anomaly with no precedent. It must go. +2. **The Rust-native one-body mechanism is the `Air` / builder-trait pattern** + (p3, OpenVM, SP1). The DSL/codegen alternatives (risc0, zisk, airbender's + verifier) buy the same single-source guarantee but cost external toolchains, + MB-scale checked-in artifacts, or CI-enforced freshness. For a Rust codebase, + trait instantiation gives the same guarantee compiler-enforced at every build. +3. **CPU hot path — compile it.** p3 and SP1 re-run the monomorphized body per + (packed) row; OpenVM interprets and self-documents the cost; zisk interprets + but amortizes over 128 SIMD lanes. We chase ~1% prover deltas ⇒ folder-style + compiled eval. (Packed/SIMD folders are a future opportunity our design leaves + open; our current scalar-per-row `evaluate` maps 1:1 onto a scalar folder.) +4. **Recursion guest — compile it too.** SP1 (staged DSL) and airbender (codegen) + both evaluate constraints as straight-line compiled code in-guest; only zisk + interprets. Our guest verifier is ordinary Rust compiled to RISC-V, so the + eval folder instantiated at `FieldElement` IS the compiled guest path — + zero hashing, zero interpretation, no staging machinery needed. +5. **Capture stays out of the hot path and out of the guest.** Symbolic capture + runs once at setup (keygen), host-side (p3, OpenVM, SP1 unanimously). CSE is + *not* done during capture by anyone (p3: none; OpenVM: Arc-identity only); + dedup belongs in the flatten/lowering step, where hashing is host-setup-only. +6. **GPU encoding template = zisk** (same field: 64-bit Goldilocks constants, + 3 dim-combos, stride-indexed rotations), with OpenVM's three-address register + allocation as the alternative; OpenVM's 31-bit constant packing does not fit. + Cache the lowered form per AIR (OpenVM forgets to — re-transpiles every prove). +7. **Emission order / constraint indexing is load-bearing** across every one-body + system (p3 documents it; OpenVM's layout depends on it). Our explicit + `constraint_idx` + indexed `emit` already handles this — keep it. +8. **Metadata**: p3/SP1 measure degree by running the symbolic builder instead of + declaring it (one less hand-maintained number — we can measure per-root degree + from the captured IR). Our per-constraint zerofier metadata + (period/offset/exemptions) is richer than their `is_first/last/transition` + selector trio — keep ours declared. +9. **LogUp architecture confirmed**: OpenVM/SP1 declare interactions in-body and + let the framework generate the LogUp constraints. Our declarative + `BusInteraction` + framework-generated lookup constraints is the same shape; + the LogUp constraint bodies become single builder bodies like everything else.