spike(stark): symbolic-field capture of transition constraints → flat IR (CPU)

crypto/stark/src/lib.rs

@@ -25,6 +25,7 @@ pub mod prover;
 pub mod r4_denoms;
 #[cfg(feature = "disk-spill")]
 pub mod storage_mode;
+pub mod symbolic;
 pub mod table;
 pub mod trace;
 pub mod traits;

crypto/stark/src/symbolic/capture.rs

@@ -0,0 +1,58 @@
+//! Capture front-end: run a constraint's generic `evaluate` over the symbolic
+//! fields and snapshot the recorded arena into a [`ConstraintProgram`].
+
+use math::field::element::FieldElement;
+use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as GoldilocksExtension;
+use math::field::goldilocks::GoldilocksField;
+
+use crate::constraints::transition::TransitionConstraint;
+use crate::table::TableView;
+
+use super::ir::{ConstraintProgram, Dim, Op};
+use super::sym_field::{SymExt, SymField, leaf_base, record_leaf, with_arena};
+
+/// Capture a single algebraic transition constraint into a flat IR program.
+///
+/// Builds a symbolic `TableView<SymField, SymExt>` whose main cells are
+/// `Var { main: true, offset: 0, row: 0, col }` leaves (1 step, 1 row,
+/// `num_main_cols` columns; aux is empty for the minimal algebraic set), runs
+/// `c.evaluate::<SymField, SymExt>(step)`, and records the returned id as the
+/// single root.
+///
+/// `num_main_cols` must be at least one greater than any column index the
+/// constraint reads.
+pub fn capture_constraint<T>(c: &T, num_main_cols: usize) -> ConstraintProgram
+where
+    T: TransitionConstraint<GoldilocksField, GoldilocksExtension>,
+{
+    let (nodes, dims, root) = with_arena(|| {
+        // Build the symbolic frame's single step: one row of `num_main_cols`
+        // main cells, each a recorded leaf. Aux is empty.
+        let row: Vec<FieldElement<SymField>> = (0..num_main_cols)
+            .map(|col| {
+                let id = record_leaf(
+                    Op::Var {
+                        main: true,
+                        offset: 0,
+                        row: 0,
+                        col: col as u16,
+                    },
+                    Dim::D1,
+                );
+                leaf_base(id)
+            })
+            .collect();
+
+        let step: TableView<SymField, SymExt> = TableView::new(vec![row], vec![Vec::new()]);
+
+        // Run the real constraint body under the symbolic fields.
+        let result = c.evaluate::<SymField, SymExt>(&step);
+        *result.value()
+    });
+
+    ConstraintProgram {
+        nodes,
+        dims,
+        roots: vec![root.id],
+    }
+}

crypto/stark/src/symbolic/interp.rs

@@ -0,0 +1,97 @@
+//! CPU interpreter for a captured [`ConstraintProgram`].
+//!
+//! A single forward pass over the topologically ordered nodes evaluates each
+//! node into a [`Value`] (base `D1` or extension `D3`), reusing the real
+//! `FieldElement` arithmetic so per-op results are bit-identical to the boxed
+//! constraint path. Mixed-dimension ops auto-embed the `D1` operand into `D3`,
+//! mirroring the field tower's `F: IsSubFieldOf<E>` arithmetic.
+
+use math::field::element::FieldElement;
+use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as GoldilocksExtension;
+use math::field::goldilocks::GoldilocksField;
+
+use super::ir::{ConstraintProgram, Dim, Op};
+
+type Fp = FieldElement<GoldilocksField>;
+type Fp3 = FieldElement<GoldilocksExtension>;
+
+/// A node's computed value: base field (`D1`) or degree-3 extension (`D3`).
+#[derive(Clone, Copy, Debug)]
+enum Value {
+    D1(Fp),
+    D3(Fp3),
+}
+
+impl Value {
+    /// Promote to the extension field, embedding a base value if needed.
+    fn to_ext(self) -> Fp3 {
+        match self {
+            Value::D1(x) => x.to_extension::<GoldilocksExtension>(),
+            Value::D3(x) => x,
+        }
+    }
+
+    fn as_base(self) -> Fp {
+        match self {
+            Value::D1(x) => x,
+            Value::D3(_) => {
+                panic!("expected a base (D1) value but found an extension (D3) value")
+            }
+        }
+    }
+}
+
+/// Evaluate the program's single 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 (`D1`) value, so this returns a `FieldElement<F>`.
+pub fn eval_program_base(prog: &ConstraintProgram, main_row: &[Fp]) -> Fp {
+    let mut values: Vec<Value> = Vec::with_capacity(prog.nodes.len());
+
+    for (i, op) in prog.nodes.iter().enumerate() {
+        let v = match *op {
+            Op::Const1(c) => Value::D1(Fp::from(c)),
+            Op::Const3([c0, c1, c2]) => {
+                Value::D3(Fp3::from_raw([Fp::from(c0), Fp::from(c1), Fp::from(c2)]))
+            }
+            Op::Var { main, 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::D1(main_row[col as usize])
+            }
+            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::D1(x), Dim::D1) => Value::D1(-x),
+                (val, Dim::D3) => Value::D3(-val.to_ext()),
+                (Value::D3(x), Dim::D1) => Value::D3(-x), // dim mismatch, keep ext
+            },
+            Op::Embed(a) => Value::D3(values[a as usize].to_ext()),
+        };
+        values.push(v);
+    }
+
+    let root = prog.roots[0];
+    values[root as usize].as_base()
+}
+
+/// Apply a binary op, auto-embedding to the extension field when the result
+/// dimension is `D3` (or either operand is already `D3`).
+#[inline]
+fn binop(
+    values: &[Value],
+    a: u32,
+    b: u32,
+    result_dim: Dim,
+    base_op: impl Fn(Fp, Fp) -> Fp,
+    ext_op: impl Fn(Fp3, Fp3) -> Fp3,
+) -> Value {
+    let va = values[a as usize];
+    let vb = values[b as usize];
+    match (va, vb, result_dim) {
+        (Value::D1(x), Value::D1(y), Dim::D1) => Value::D1(base_op(x, y)),
+        _ => Value::D3(ext_op(va.to_ext(), vb.to_ext())),
+    }
+}

crypto/stark/src/symbolic/ir.rs

@@ -0,0 +1,80 @@
+//! 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 symbolic capture front-end
+//! (see [`crate::symbolic::capture`]) and consumed by the CPU interpreter (see
+//! [`crate::symbolic::interp`]).
+//!
+//! The IR is single-field over Goldilocks, with a [`Dim`] tag distinguishing
+//! base (`D1`, one `u64`) from the degree-3 extension (`D3`, three `u64`).
+
+/// Field-arithmetic dimension of a node's value: base Goldilocks (`D1`) or its
+/// degree-3 extension (`D3`).
+#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, Default)]
+pub enum Dim {
+    /// Base field (one Goldilocks `u64`).
+    #[default]
+    D1,
+    /// Degree-3 extension (`[u64; 3]`).
+    D3,
+}
+
+/// 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`.
+#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
+pub enum Op {
+    /// A base-field literal (already reduced mod the Goldilocks prime).
+    Const1(u64),
+    /// An extension-field literal `[c0, c1, c2]` (each component reduced).
+    Const3([u64; 3]),
+    /// A leaf read of a main-trace cell. `main` is always `true` for the
+    /// minimal algebraic set captured by the spike; aux reads would set it
+    /// `false`. `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,
+    },
+    /// `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 `D1` value into `D3` (`<F as IsSubFieldOf<E>>::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.
+#[derive(Clone, Debug)]
+pub struct ConstraintProgram {
+    /// Topologically ordered instruction list.
+    pub nodes: Vec<Op>,
+    /// Per-node result dimension, parallel to `nodes`.
+    pub dims: Vec<Dim>,
+    /// Per-constraint root node ids.
+    pub roots: Vec<u32>,
+}
+
+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()
+    }
+}

crypto/stark/src/symbolic/mod.rs

@@ -0,0 +1,31 @@
+//! Symbolic-field constraint capture spike.
+//!
+//! A proof-of-concept that lambda_vm's algebraic transition constraints can be
+//! captured into a flat, single-field Goldilocks IR by running each
+//! constraint's existing generic `evaluate::<F, E>` over recording field types
+//! ([`SymField`]/[`SymExt`]), and that interpreting that IR on the CPU
+//! reproduces the constraint's real `evaluate` bit-for-bit.
+//!
+//! This is CPU-only and does not touch the prover hot loop, the LogUp
+//! framework, or GPU code. See `thoughts/gpu-constraint-eval/plan-symbolic-field.md`.
+//!
+//! - [`ir`]: the IR data structures ([`ConstraintProgram`], [`Op`], [`Dim`]).
+//! - [`sym_field`]: the recording fields and the thread-local arena.
+//! - [`capture`]: capture a constraint into a [`ConstraintProgram`].
+//! - [`interp`]: a CPU forward-pass interpreter over the IR.
+//!
+//! [`ConstraintProgram`]: ir::ConstraintProgram
+//! [`Op`]: ir::Op
+//! [`Dim`]: ir::Dim
+//! [`SymField`]: sym_field::SymField
+//! [`SymExt`]: sym_field::SymExt
+
+pub mod capture;
+pub mod interp;
+pub mod ir;
+pub mod sym_field;
+
+pub use capture::capture_constraint;
+pub use interp::eval_program_base;
+pub use ir::{ConstraintProgram, Dim, Op};
+pub use sym_field::{SymExt, SymField, SymId};