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/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..258aa23b7 --- /dev/null +++ b/crypto/stark/src/constraint_ir/mod.rs @@ -0,0 +1,33 @@ +//! 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; + +#[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); + } +} 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..cf3921629 100644 --- a/crypto/stark/src/constraints/mod.rs +++ b/crypto/stark/src/constraints/mod.rs @@ -1,3 +1,7 @@ pub mod boundary; +pub mod builder; +#[cfg(test)] +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" + ); + } + } +} 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; 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.