Merge branch 'main' into linda/shape-validation

Author: sai-deng

book/src/SUMMARY.md

@@ -4,6 +4,7 @@
 * [Introduction](introduction.md)
 * [Construction](construction.md)
 * [Circuit building](circuit_building.md)
+* [Trace generation](trace_generation.md)
 * [Handling arbitrary programs](extensions.md)
 * [Debugging](debugging.md)
 * [Benchmarks](benchmark.md)

book/src/trace_generation.md

@@ -0,0 +1,119 @@
+# Trace Generation Pipeline
+
+After building a circuit, the next step is execution: running the program with concrete inputs and generating the execution traces needed for proving. This section describes the complete flow from a static `Circuit` specification to the final `Traces` structure.
+
+## Overview
+
+The trace generation pipeline consists of three distinct phases:
+
+1. **Circuit compilation** — Transform high-level circuit expressions into a fixed intermediate representation.
+2. **Circuit execution** — Populate the witness table by evaluating operations with concrete input values.
+3. **Trace extraction** — Generate operation-specific traces from the populated witness table.
+
+Each phase has a clear responsibility and produces well-defined outputs that feed into the next stage.
+
+## Phase 1: Circuit Compilation
+
+Circuit compilation happens when calling `builder.build()`. This phase translates circuit expressions into a deterministic sequence of primitive and non-primitive operations.
+
+The compilation process is described in detail in the [Circuit Building](./circuit_building.md#building-pipeline) section. In summary, it performs three successive passes to lower expressions to primitives, handle non-primitive operations, and optimize the resulting graph.
+
+The output is a `Circuit<F>` containing the primitive operations in topological order, non-primitive operation specifications, and witness allocation metadata. This circuit is a static, serializable specification that can be executed multiple times with different inputs.
+
+## Phase 2: Circuit Execution
+
+Circuit execution happens when calling `runner.run()`. This phase populates the witness table by evaluating each operation with concrete field element values.
+
+The runner is initialized with a `Circuit<F>` and receives:
+- Public input values via `runner.set_public_inputs()`
+- Private data for non-primitive operations via `runner.set_non_primitive_op_private_data()`
+
+The runner iterates through primitive operations in topological order, executing each one to populate witness slots. Operations can run in **forward mode** (computing outputs from inputs) or **backward mode** (inferring missing inputs from outputs), allowing bidirectional constraint solving.
+
+The output is a fully populated witness table where every slot contains a concrete field element. Any unset witness triggers a `WitnessNotSet` error.
+
+## Phase 3: Trace Extraction
+
+Trace extraction happens internally within `runner.run()` after execution completes. This phase delegates to specialized trace builders that transform the populated witness table into operation-specific trace tables.
+
+Each primitive operation has a dedicated builder that extracts its operations from the IR and produces trace columns:
+
+- **WitnessTraceBuilder** — Generates the central [witness table](./construction.md#witness-table) with sequential `(index, value)` pairs
+- **ConstTraceBuilder** — Extracts constants (both columns preprocessed)
+- **PublicTraceBuilder** — Extracts public inputs (index preprocessed, values at runtime)
+- **AddTraceBuilder** — Extracts additions with six columns: `(lhs_index, lhs_value, rhs_index, rhs_value, result_index, result_value)`
+- **MulTraceBuilder** — Extracts multiplications with the same six-column structure
+
+Non-primitive operations require custom trace builders. For example, **MmcsTraceBuilder** validates and extracts MMCS path verification traces. Custom trace builders follow the same pattern, operating independently in a single pass to produce isolated trace tables. All index columns are preprocessed since the IR is fixed and known to the verifier.
+
+The output is a `Traces<F>` structure containing all execution traces needed by the prover to generate STARK proofs for each [operation-specific chip](./construction.md#operation-specific-stark-chips).
+
+## Example: Fibonacci Circuit
+
+Consider a simple Fibonacci circuit computing `F(5)`:
+
+```rust,ignore
+let mut builder = CircuitBuilder::new();
+
+let expected = builder.add_public_input();
+let mut a = builder.add_const(F::ZERO);
+let mut b = builder.add_const(F::ONE);
+
+for _ in 2..=5 {
+    let next = builder.add(a, b);
+    a = b;
+    b = next;
+}
+
+builder.connect(b, expected);
+let circuit = builder.build()?;
+```
+
+**Phase 1: Compilation** produces:
+```text
+primitive_ops: [
+  Const { out: w0, val: 0 },
+  Const { out: w1, val: 1 },
+  Public { out: w2, public_pos: 0 },
+  Add { a: w0, b: w1, out: w3 },  // F(2) = 0 + 1
+  Add { a: w1, b: w3, out: w4 },  // F(3) = 1 + 1
+  Add { a: w3, b: w4, out: w5 },  // F(4) = 1 + 2
+  Add { a: w4, b: w5, out: w2 },  // F(5) = 2 + 3 (connects to expected)
+]
+witness_count: 6
+```
+
+**Phase 2: Execution** with `runner.set_public_inputs(&[F::from(5)])`:
+```text
+witness[0] = Some(0)
+witness[1] = Some(1)
+witness[2] = Some(5)
+witness[3] = Some(1)
+witness[4] = Some(2)
+witness[5] = Some(3)
+```
+
+**Phase 3: Trace Extraction** produces:
+```text
+const_trace: [(w0, 0), (w1, 1)]
+public_trace: [(w2, 5)]
+add_trace: [
+  (w0, 0, w1, 1, w3, 1),
+  (w1, 1, w3, 1, w4, 2),
+  (w3, 1, w4, 2, w5, 3),
+  (w4, 2, w5, 3, w2, 5),
+]
+mul_trace: []
+```
+
+The witness table acts as the central bus, with each operation table containing [lookups](./construction.md#lookups) into it. The aggregated lookup argument enforces that all these lookups are consistent.
+
+## Key Properties
+
+**Determinism** — Given the same circuit and inputs, trace generation is completely deterministic, ensuring reproducible proofs.
+
+**Separation of concerns** — Each phase has a single responsibility: compilation handles expression lowering, execution populates concrete values, and trace builders format data for proving.
+
+**Builder pattern efficiency** — Trace builders operate in a single pass using only the data they need. No builder depends on another's output, enabling future parallelization.
+
+**Preprocessed columns** — All index columns in operation traces are preprocessed. Since the IR is fixed, the verifier can reconstruct these columns without online commitments, significantly reducing proof size.

circuit/src/alloc_entry.rs

@@ -21,6 +21,7 @@ pub enum AllocationType {
     Mul,
     Div,
     NonPrimitiveOp(NonPrimitiveOpType),
+    WitnessHint,
 }
 
 /// Detailed allocation entry for debugging
@@ -92,6 +93,7 @@ fn dump_internal_log(allocation_log: &[AllocationEntry]) {
     let mut muls = Vec::new();
     let mut divs = Vec::new();
     let mut non_primitives = Vec::new();
+    let mut witness_hints = Vec::new();
 
     fn display_label(label: &str) -> String {
         if label.is_empty() {
@@ -110,6 +112,7 @@ fn dump_internal_log(allocation_log: &[AllocationEntry]) {
             AllocationType::Mul => muls.push(entry),
             AllocationType::Div => divs.push(entry),
             AllocationType::NonPrimitiveOp(_) => non_primitives.push(entry),
+            AllocationType::WitnessHint => witness_hints.push(entry),
         }
     }
 
@@ -255,6 +258,18 @@ fn dump_internal_log(allocation_log: &[AllocationEntry]) {
         }
         tracing::debug!("");
     }
+
+    if !witness_hints.is_empty() {
+        tracing::debug!("--- Witness Hints ({}) ---", witness_hints.len());
+        for entry in witness_hints {
+            tracing::debug!(
+                "  expr_{} (WitnessHint){}",
+                entry.expr_id.0,
+                display_label(entry.label)
+            );
+        }
+        tracing::debug!("");
+    }
 }
 
 /// List all unique scopes present in the allocation log.

circuit/src/builder/circuit_builder.rs

@@ -1,7 +1,8 @@
 use alloc::vec::Vec;
+use core::hash::Hash;
 
 use hashbrown::HashMap;
-use p3_field::PrimeCharacteristicRing;
+use p3_field::{Field, PrimeCharacteristicRing};
 
 use super::compiler::{ExpressionLowerer, NonPrimitiveLowerer, Optimizer};
 use super::{BuilderConfig, ExpressionBuilder, PublicInputTracker};
@@ -115,6 +116,18 @@ where
         self.public_tracker.count()
     }
 
+    /// Allocates a witness hint (uninitialized witness slot set during non-primitive execution).
+    #[must_use]
+    pub fn alloc_witness_hint(&mut self, label: &'static str) -> ExprId {
+        self.expr_builder.add_witness_hint(label)
+    }
+
+    /// Allocates multiple witness hints.
+    #[must_use]
+    pub fn alloc_witness_hints(&mut self, count: usize, label: &'static str) -> Vec<ExprId> {
+        self.expr_builder.add_witness_hints(count, label)
+    }
+
     /// Adds a constant to the circuit (deduplicated).
     ///
     /// If this value was previously added, returns the original ExprId.
@@ -292,7 +305,7 @@ where
 
 impl<F> CircuitBuilder<F>
 where
-    F: Clone + PrimeCharacteristicRing + PartialEq + Eq + core::hash::Hash,
+    F: Field + Clone + PrimeCharacteristicRing + PartialEq + Eq + Hash,
 {
     /// Builds the circuit into a Circuit with separate lowering and IR transformation stages.
     /// Returns an error if lowering fails due to an internal inconsistency.
@@ -326,7 +339,7 @@ where
         let primitive_ops = optimizer.optimize(primitive_ops);
 
         // Stage 4: Generate final circuit
-        let mut circuit = Circuit::new(witness_count);
+        let mut circuit = Circuit::new(witness_count, expr_to_widx);
         circuit.primitive_ops = primitive_ops;
         circuit.non_primitive_ops = lowered_non_primitive_ops;
         circuit.public_rows = public_rows;
@@ -471,7 +484,7 @@ mod tests {
         assert!(circuit.enabled_ops.is_empty());
 
         match &circuit.primitive_ops[0] {
-            crate::op::Prim::Const { out, val } => {
+            crate::op::Op::Const { out, val } => {
                 assert_eq!(*out, WitnessId(0));
                 assert_eq!(*val, BabyBear::ZERO);
             }
@@ -494,23 +507,23 @@ mod tests {
         assert_eq!(circuit.primitive_ops.len(), 3);
 
         match &circuit.primitive_ops[0] {
-            crate::op::Prim::Const { out, val } => {
+            crate::op::Op::Const { out, val } => {
                 assert_eq!(*out, WitnessId(0));
                 assert_eq!(*val, BabyBear::ZERO);
             }
             _ => panic!("Expected Const at index 0"),
         }
 
         match &circuit.primitive_ops[1] {
-            crate::op::Prim::Public { out, public_pos } => {
+            crate::op::Op::Public { out, public_pos } => {
                 assert_eq!(*out, WitnessId(1));
                 assert_eq!(*public_pos, 0);
             }
             _ => panic!("Expected Public at index 1"),
         }
 
         match &circuit.primitive_ops[2] {
-            crate::op::Prim::Public { out, public_pos } => {
+            crate::op::Op::Public { out, public_pos } => {
                 assert_eq!(*out, WitnessId(2));
                 assert_eq!(*public_pos, 1);
             }
@@ -536,23 +549,23 @@ mod tests {
         assert_eq!(circuit.primitive_ops.len(), 3);
 
         match &circuit.primitive_ops[0] {
-            crate::op::Prim::Const { out, val } => {
+            crate::op::Op::Const { out, val } => {
                 assert_eq!(*out, WitnessId(0));
                 assert_eq!(*val, BabyBear::ZERO);
             }
             _ => panic!("Expected Const at index 0"),
         }
 
         match &circuit.primitive_ops[1] {
-            crate::op::Prim::Const { out, val } => {
+            crate::op::Op::Const { out, val } => {
                 assert_eq!(*out, WitnessId(1));
                 assert_eq!(*val, BabyBear::from_u64(1));
             }
             _ => panic!("Expected Const at index 1"),
         }
 
         match &circuit.primitive_ops[2] {
-            crate::op::Prim::Const { out, val } => {
+            crate::op::Op::Const { out, val } => {
                 assert_eq!(*out, WitnessId(2));
                 assert_eq!(*val, BabyBear::from_u64(2));
             }
@@ -574,7 +587,7 @@ mod tests {
         assert_eq!(circuit.primitive_ops.len(), 4);
 
         match &circuit.primitive_ops[3] {
-            crate::op::Prim::Add { out, a, b } => {
+            crate::op::Op::Add { out, a, b } => {
                 assert_eq!(*out, WitnessId(3));
                 assert_eq!(*a, WitnessId(1));
                 assert_eq!(*b, WitnessId(2));