openvm_stark_backend/air_builders/debug/
mod.rs

1use std::sync::{Arc, Mutex};
2
3use p3_air::{AirBuilder, AirBuilderWithPublicValues, ExtensionBuilder, PairBuilder};
4use p3_field::PrimeCharacteristicRing;
5use p3_matrix::{dense::RowMajorMatrixView, stack::VerticalPair};
6
7use super::{PartitionedAirBuilder, ViewPair};
8use crate::{
9    config::{StarkProtocolConfig, Val},
10    interaction::{Interaction, InteractionBuilder},
11};
12
13mod check_constraints;
14
15pub use check_constraints::{
16    check_constraints, check_logup, debug_constraints_and_interactions, AirProofRawInput,
17};
18
19use crate::interaction::BusIndex;
20
21thread_local! {
22   pub static USE_DEBUG_BUILDER: Arc<Mutex<bool>> = Arc::new(Mutex::new(true));
23}
24
25/// An `AirBuilder` which asserts that each constraint is zero, allowing any failed constraints to
26/// be detected early.
27pub struct DebugConstraintBuilder<'a, SC: StarkProtocolConfig> {
28    pub air_name: &'a str,
29    pub row_index: usize,
30    pub preprocessed: ViewPair<'a, Val<SC>>,
31    pub partitioned_main: Vec<ViewPair<'a, Val<SC>>>,
32    pub is_first_row: Val<SC>,
33    pub is_last_row: Val<SC>,
34    pub is_transition: Val<SC>,
35    pub public_values: &'a [Val<SC>],
36    pub has_common_main: bool,
37}
38
39impl<'a, SC> AirBuilder for DebugConstraintBuilder<'a, SC>
40where
41    SC: StarkProtocolConfig,
42{
43    type F = Val<SC>;
44    type Expr = Val<SC>;
45    type Var = Val<SC>;
46    type M = VerticalPair<RowMajorMatrixView<'a, Val<SC>>, RowMajorMatrixView<'a, Val<SC>>>;
47
48    /// It is difficult to horizontally concatenate matrices when the main trace is partitioned, so
49    /// we disable this method in that case.
50    fn main(&self) -> Self::M {
51        if self.partitioned_main.len() == 1 {
52            self.partitioned_main[0]
53        } else {
54            panic!("Main trace is either empty or partitioned. This function should not be used.")
55        }
56    }
57
58    fn is_first_row(&self) -> Self::Expr {
59        self.is_first_row
60    }
61
62    fn is_last_row(&self) -> Self::Expr {
63        self.is_last_row
64    }
65
66    fn is_transition_window(&self, size: usize) -> Self::Expr {
67        if size == 2 {
68            self.is_transition
69        } else {
70            panic!("only supports a window size of 2")
71        }
72    }
73
74    fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
75        assert_eq!(
76            x.into(),
77            Val::<SC>::ZERO,
78            "constraints had nonzero value on air {},row {}",
79            self.air_name,
80            self.row_index
81        );
82    }
83
84    fn assert_eq<I1: Into<Self::Expr>, I2: Into<Self::Expr>>(&mut self, x: I1, y: I2) {
85        let x = x.into();
86        let y = y.into();
87        assert_eq!(
88            x, y,
89            "values didn't match on air {}, row {}: {} != {}",
90            self.air_name, self.row_index, x, y
91        );
92    }
93}
94
95impl<SC> PairBuilder for DebugConstraintBuilder<'_, SC>
96where
97    SC: StarkProtocolConfig,
98{
99    fn preprocessed(&self) -> Self::M {
100        self.preprocessed
101    }
102}
103
104impl<SC> ExtensionBuilder for DebugConstraintBuilder<'_, SC>
105where
106    SC: StarkProtocolConfig,
107{
108    type EF = SC::EF;
109    type ExprEF = SC::EF;
110    type VarEF = SC::EF;
111
112    fn assert_zero_ext<I>(&mut self, x: I)
113    where
114        I: Into<Self::ExprEF>,
115    {
116        assert_eq!(
117            x.into(),
118            SC::EF::ZERO,
119            "constraints had nonzero value on row {}",
120            self.row_index
121        );
122    }
123
124    fn assert_eq_ext<I1, I2>(&mut self, x: I1, y: I2)
125    where
126        I1: Into<Self::ExprEF>,
127        I2: Into<Self::ExprEF>,
128    {
129        let x = x.into();
130        let y = y.into();
131        assert_eq!(
132            x, y,
133            "values didn't match on air {}, row {}: {} != {}",
134            self.air_name, self.row_index, x, y
135        );
136    }
137}
138
139impl<SC> AirBuilderWithPublicValues for DebugConstraintBuilder<'_, SC>
140where
141    SC: StarkProtocolConfig,
142{
143    type PublicVar = Val<SC>;
144
145    fn public_values(&self) -> &[Self::F] {
146        self.public_values
147    }
148}
149
150impl<SC> PartitionedAirBuilder for DebugConstraintBuilder<'_, SC>
151where
152    SC: StarkProtocolConfig,
153{
154    fn cached_mains(&self) -> &[Self::M] {
155        let mut num_cached_mains = self.partitioned_main.len();
156        if self.has_common_main {
157            num_cached_mains -= 1;
158        }
159        &self.partitioned_main[..num_cached_mains]
160    }
161    fn common_main(&self) -> &Self::M {
162        assert!(self.has_common_main, "AIR doesn't have a common main trace");
163        self.partitioned_main.last().unwrap()
164    }
165}
166
167// No-op implementation
168impl<SC> InteractionBuilder for DebugConstraintBuilder<'_, SC>
169where
170    SC: StarkProtocolConfig,
171{
172    fn push_interaction<E: Into<Self::Expr>>(
173        &mut self,
174        _bus_index: BusIndex,
175        _fields: impl IntoIterator<Item = E>,
176        _count: impl Into<Self::Expr>,
177        _count_weight: u32,
178    ) {
179        // no-op, interactions are debugged elsewhere
180    }
181
182    fn num_interactions(&self) -> usize {
183        0
184    }
185
186    fn all_interactions(&self) -> &[Interaction<Self::Expr>] {
187        &[]
188    }
189}
openvm_stark_backend/air_builders/debug/mod.rs

openvm_stark_backend/air_builders/debug/
mod.rs
