Skip to main content

miden_ace_codegen/
pipeline.rs

1//! High-level ACE codegen pipeline helpers.
2//!
3//! This module ties together the major layers:
4//! - build a verifier-style DAG from AIR constraints,
5//! - choose a READ layout for inputs,
6//! - emit a circuit that mirrors verifier evaluation.
7
8use miden_crypto::{
9    field::{Algebra, ExtensionField, Field, TwoAdicField},
10    stark::air::{
11        LiftedAir,
12        symbolic::{AirLayout, SymbolicAirBuilder, SymbolicExpressionExt},
13    },
14};
15
16use crate::{
17    AceError,
18    circuit::{AceCircuit, emit_circuit},
19    dag::{AceDag, PeriodicColumnData, build_verifier_dag},
20    layout::{InputCounts, InputLayout},
21};
22
23/// Layout strategy for arranging ACE inputs.
24///
25/// - `Native`: minimal, no alignment/padding; useful for native (off-VM) evaluation.
26/// - `Masm`: matches the recursive verifier READ layout (alignment, padding, and randomness
27///   ordering).
28#[derive(Debug, Clone, Copy)]
29pub enum LayoutKind {
30    /// Minimal layout used for off-VM evaluation.
31    Native,
32    /// MASM-aligned layout used by the recursive verifier.
33    Masm,
34}
35
36/// Configuration for building an ACE DAG and its input layout.
37#[derive(Debug, Clone, Copy)]
38pub struct AceConfig {
39    /// Number of quotient chunks used by the AIR.
40    pub num_quotient_chunks: usize,
41    /// Number of variable-length public input groups.
42    /// Each group produces one reduced extension field element.
43    /// The layout policy handles alignment (e.g., MASM word-aligns each group to
44    /// 2 EF slots; Native uses 1 EF slot per group).
45    pub num_vlpi_groups: usize,
46    /// Layout policy (Native vs Masm).
47    pub layout: LayoutKind,
48}
49
50/// Output of the ACE codegen pipeline (layout + DAG).
51#[derive(Debug)]
52pub struct AceArtifacts<EF> {
53    /// Input layout describing the READ section order.
54    pub layout: InputLayout,
55    /// DAG that mirrors the verifier evaluation.
56    pub dag: AceDag<EF>,
57}
58
59/// Build a verifier-equivalent ACE circuit for the provided AIR.
60///
61/// This builds the constraint-evaluation DAG, validates layout invariants, and
62/// emits the off-VM circuit representation. The circuit performs the constraint
63/// evaluation check at the out-of-domain point z.
64pub fn build_ace_circuit_for_air<A, F, EF>(
65    air: &A,
66    config: AceConfig,
67) -> Result<AceCircuit<EF>, AceError>
68where
69    A: LiftedAir<F, EF>,
70    F: TwoAdicField,
71    EF: ExtensionField<F>,
72    SymbolicExpressionExt<F, EF>: Algebra<EF>,
73{
74    let artifacts = build_ace_dag_for_air::<A, F, EF>(air, config)?;
75    emit_circuit(&artifacts.dag, artifacts.layout)
76}
77
78/// Build a verifier-equivalent DAG and layout for the provided AIR.
79pub fn build_ace_dag_for_air<A, F, EF>(
80    air: &A,
81    config: AceConfig,
82) -> Result<AceArtifacts<EF>, AceError>
83where
84    A: LiftedAir<F, EF>,
85    F: TwoAdicField,
86    EF: ExtensionField<F>,
87    SymbolicExpressionExt<F, EF>: Algebra<EF>,
88{
89    let periodic_columns = air.periodic_columns();
90    let counts = input_counts_for_air::<A, F, EF>(air, config, periodic_columns.len());
91    let layout = match config.layout {
92        LayoutKind::Native => InputLayout::new(counts),
93        LayoutKind::Masm => InputLayout::new_masm(counts),
94    };
95    layout.validate();
96
97    let air_layout = AirLayout {
98        preprocessed_width: 0,
99        main_width: counts.width,
100        num_public_values: counts.num_public,
101        permutation_width: counts.aux_width,
102        num_permutation_challenges: counts.num_randomness,
103        num_permutation_values: air.num_aux_values(),
104        num_periodic_columns: counts.num_periodic,
105    };
106    let mut builder = SymbolicAirBuilder::<F, EF>::new(air_layout);
107    air.eval(&mut builder);
108    let constraint_layout = builder.constraint_layout();
109    let base_constraints = builder.base_constraints();
110    let ext_constraints = builder.extension_constraints();
111
112    let periodic_data = (!periodic_columns.is_empty())
113        .then(|| PeriodicColumnData::from_periodic_columns::<F>(periodic_columns.to_vec()));
114    let dag = build_verifier_dag::<F, EF>(
115        &base_constraints,
116        &ext_constraints,
117        &constraint_layout,
118        &layout,
119        periodic_data.as_ref(),
120    );
121
122    Ok(AceArtifacts { layout, dag })
123}
124
125fn input_counts_for_air<A, F, EF>(air: &A, config: AceConfig, num_periodic: usize) -> InputCounts
126where
127    A: LiftedAir<F, EF>,
128    F: Field,
129    EF: ExtensionField<F>,
130{
131    assert!(config.num_quotient_chunks > 0, "num_quotient_chunks must be > 0");
132    assert!(
133        air.preprocessed_trace().is_none(),
134        "preprocessed trace inputs are not supported"
135    );
136
137    let num_randomness = air.num_randomness();
138    assert!(
139        num_randomness == 2,
140        "AIR must declare exactly 2 randomness challenges (alpha, beta), got {num_randomness}"
141    );
142
143    // Convert logical VLPI groups to EF slots based on layout policy.
144    // MASM word-aligns each group (4 base felts = 2 EF slots per group).
145    // Native uses 1 EF slot per group (no padding).
146    let num_vlpi = match config.layout {
147        LayoutKind::Masm => config.num_vlpi_groups * 2,
148        LayoutKind::Native => config.num_vlpi_groups,
149    };
150
151    InputCounts {
152        width: air.width(),
153        aux_width: air.aux_width(),
154        num_public: air.num_public_values(),
155        num_vlpi,
156        num_randomness,
157        num_periodic,
158        num_quotient_chunks: config.num_quotient_chunks,
159    }
160}