miden_air/
lib.rs

1#![no_std]
2
3#[macro_use]
4extern crate alloc;
5
6#[cfg(feature = "std")]
7extern crate std;
8
9use alloc::vec::Vec;
10use core::borrow::Borrow;
11
12use miden_core::{
13    field::ExtensionField,
14    precompile::PrecompileTranscriptState,
15    program::{ProgramInfo, StackInputs, StackOutputs},
16};
17use miden_crypto::stark::matrix::{Matrix, RowMajorMatrix};
18
19pub mod config;
20mod constraints;
21
22pub mod trace;
23use trace::{AUX_TRACE_WIDTH, AuxTraceBuilder, MainTraceRow, TRACE_WIDTH};
24
25// RE-EXPORTS
26// ================================================================================================
27mod export {
28    pub use miden_core::{
29        Felt,
30        serde::{ByteReader, ByteWriter, Deserializable, DeserializationError, Serializable},
31        utils::ToElements,
32    };
33    pub use miden_crypto::stark::air::{Air, AirBuilder, BaseAir, MidenAir, MidenAirBuilder};
34}
35
36pub use export::*;
37
38// PUBLIC INPUTS
39// ================================================================================================
40
41#[derive(Debug, Clone)]
42pub struct PublicInputs {
43    program_info: ProgramInfo,
44    stack_inputs: StackInputs,
45    stack_outputs: StackOutputs,
46    pc_transcript_state: PrecompileTranscriptState,
47}
48
49impl PublicInputs {
50    /// Creates a new instance of `PublicInputs` from program information, stack inputs and outputs,
51    /// and the precompile transcript state (capacity of an internal sponge).
52    pub fn new(
53        program_info: ProgramInfo,
54        stack_inputs: StackInputs,
55        stack_outputs: StackOutputs,
56        pc_transcript_state: PrecompileTranscriptState,
57    ) -> Self {
58        Self {
59            program_info,
60            stack_inputs,
61            stack_outputs,
62            pc_transcript_state,
63        }
64    }
65
66    pub fn stack_inputs(&self) -> StackInputs {
67        self.stack_inputs
68    }
69
70    pub fn stack_outputs(&self) -> StackOutputs {
71        self.stack_outputs
72    }
73
74    pub fn program_info(&self) -> ProgramInfo {
75        self.program_info.clone()
76    }
77
78    /// Returns the precompile transcript state.
79    pub fn pc_transcript_state(&self) -> PrecompileTranscriptState {
80        self.pc_transcript_state
81    }
82
83    /// Converts public inputs into a vector of field elements (Felt) in the canonical order:
84    /// - program info elements
85    /// - stack inputs
86    /// - stack outputs
87    /// - precompile transcript state
88    pub fn to_elements(&self) -> Vec<Felt> {
89        let mut result = self.program_info.to_elements();
90        result.extend_from_slice(self.stack_inputs.as_ref());
91        result.extend_from_slice(self.stack_outputs.as_ref());
92        result.extend_from_slice(self.pc_transcript_state.as_ref());
93        result
94    }
95}
96
97// SERIALIZATION
98// ================================================================================================
99
100impl Serializable for PublicInputs {
101    fn write_into<W: ByteWriter>(&self, target: &mut W) {
102        self.program_info.write_into(target);
103        self.stack_inputs.write_into(target);
104        self.stack_outputs.write_into(target);
105        self.pc_transcript_state.write_into(target);
106    }
107}
108
109impl Deserializable for PublicInputs {
110    fn read_from<R: ByteReader>(source: &mut R) -> Result<Self, DeserializationError> {
111        let program_info = ProgramInfo::read_from(source)?;
112        let stack_inputs = StackInputs::read_from(source)?;
113        let stack_outputs = StackOutputs::read_from(source)?;
114        let pc_transcript_state = PrecompileTranscriptState::read_from(source)?;
115
116        Ok(PublicInputs {
117            program_info,
118            stack_inputs,
119            stack_outputs,
120            pc_transcript_state,
121        })
122    }
123}
124
125// PROCESSOR AIR
126// ================================================================================================
127
128/// Miden VM Processor AIR implementation.
129///
130/// This struct defines the constraints for the Miden VM processor.
131/// Generic over aux trace builder to support different extension fields.
132pub struct ProcessorAir<B = ()> {
133    /// Auxiliary trace builder for generating auxiliary columns.
134    aux_builder: Option<B>,
135}
136
137impl Default for ProcessorAir<()> {
138    fn default() -> Self {
139        Self::new()
140    }
141}
142
143impl ProcessorAir<()> {
144    /// Creates a new ProcessorAir without auxiliary trace support.
145    pub fn new() -> Self {
146        Self { aux_builder: None }
147    }
148}
149
150impl<B> ProcessorAir<B> {
151    /// Creates a new ProcessorAir with auxiliary trace support.
152    pub fn with_aux_builder(builder: B) -> Self {
153        Self { aux_builder: Some(builder) }
154    }
155}
156
157impl<EF, B> MidenAir<Felt, EF> for ProcessorAir<B>
158where
159    EF: ExtensionField<Felt>,
160    B: AuxTraceBuilder<EF>,
161{
162    fn width(&self) -> usize {
163        TRACE_WIDTH
164    }
165
166    fn aux_width(&self) -> usize {
167        // Return the number of extension field columns
168        // The prover will interpret the returned base field data as EF columns
169        AUX_TRACE_WIDTH
170    }
171
172    fn num_randomness(&self) -> usize {
173        trace::AUX_TRACE_RAND_ELEMENTS
174    }
175
176    fn build_aux_trace(
177        &self,
178        main: &RowMajorMatrix<Felt>,
179        challenges: &[EF],
180    ) -> Option<RowMajorMatrix<Felt>> {
181        let _span = tracing::info_span!("build_aux_trace").entered();
182
183        let builders = self.aux_builder.as_ref()?;
184
185        Some(builders.build_aux_columns(main, challenges))
186    }
187
188    fn eval<AB: MidenAirBuilder<F = Felt>>(&self, builder: &mut AB) {
189        use crate::constraints;
190
191        let main = builder.main();
192
193        // Access the two rows: current (local) and next
194        let local = main.row_slice(0).expect("Matrix should have at least 1 row");
195        let next = main.row_slice(1).expect("Matrix should have at least 2 rows");
196
197        // Use structured column access via MainTraceCols
198        let local: &MainTraceRow<AB::Var> = (*local).borrow();
199        let next: &MainTraceRow<AB::Var> = (*next).borrow();
200
201        // SYSTEM CONSTRAINTS
202        constraints::enforce_clock_constraint(builder, local, next);
203
204        // RANGE CHECKER CONSTRAINTS
205        constraints::range::enforce_range_boundary_constraints(builder, local);
206        constraints::range::enforce_range_transition_constraint(builder, local, next);
207        constraints::range::enforce_range_bus_constraint(builder, local);
208    }
209}
miden_air/lib.rs

miden_air/
lib.rs
