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    /// Layout policy (Native vs Masm).
42    pub layout: LayoutKind,
43    /// Number of AIRs the circuit is built over. With `1` the layout is the plain
44    /// single-AIR layout; with `num_airs >= 2` the stark-vars region reserves
45    /// additional EF slots for the per-AIR multi-AIR β coefficients (one per AIR)
46    /// and lifted selector triples (one per AIR).
47    pub num_airs: usize,
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, config.num_airs >= 2) {
92        (LayoutKind::Native, false) => InputLayout::new(counts),
93        (LayoutKind::Masm, false) => InputLayout::new_masm(counts),
94        (LayoutKind::Native, true) => InputLayout::new_multi_air(counts, config.num_airs),
95        (LayoutKind::Masm, true) => InputLayout::new_masm_multi_air(counts, config.num_airs),
96    };
97    layout.validate();
98
99    let air_layout = AirLayout {
100        preprocessed_width: 0,
101        main_width: counts.width,
102        num_public_values: counts.num_public,
103        permutation_width: counts.aux_width,
104        num_permutation_challenges: counts.num_randomness,
105        num_permutation_values: air.num_aux_values(),
106        num_periodic_columns: counts.num_periodic,
107    };
108    let mut builder = SymbolicAirBuilder::<F, EF>::new(air_layout);
109    air.eval(&mut builder);
110    let constraint_layout = builder.constraint_layout();
111    let base_constraints = builder.base_constraints();
112    let ext_constraints = builder.extension_constraints();
113
114    let periodic_data = (!periodic_columns.is_empty())
115        .then(|| PeriodicColumnData::from_periodic_columns::<F>(periodic_columns.to_vec()));
116    let dag = build_verifier_dag::<F, EF>(
117        &base_constraints,
118        &ext_constraints,
119        &constraint_layout,
120        &layout,
121        periodic_data.as_ref(),
122    );
123
124    Ok(AceArtifacts { layout, dag })
125}
126
127fn input_counts_for_air<A, F, EF>(air: &A, config: AceConfig, num_periodic: usize) -> InputCounts
128where
129    A: LiftedAir<F, EF>,
130    F: Field,
131    EF: ExtensionField<F>,
132{
133    assert!(config.num_quotient_chunks > 0, "num_quotient_chunks must be > 0");
134    assert!(
135        air.preprocessed_trace().is_none(),
136        "preprocessed trace inputs are not supported"
137    );
138
139    let num_randomness = air.num_randomness();
140    assert!(
141        num_randomness == 2,
142        "AIR must declare exactly 2 randomness challenges (alpha, beta), got {num_randomness}"
143    );
144
145    InputCounts {
146        width: air.width(),
147        aux_width: air.aux_width(),
148        num_aux_boundary: air.num_aux_values(),
149        num_public: air.num_public_values(),
150        num_randomness,
151        num_periodic,
152        num_quotient_chunks: config.num_quotient_chunks,
153    }
154}