sp1_recursion_core/air/
builder.rs

1use core::iter::{once, repeat};
2use p3_air::{AirBuilder, AirBuilderWithPublicValues};
3use p3_field::AbstractField;
4use sp1_stark::{
5    air::{AirInteraction, BaseAirBuilder, InteractionScope, MachineAirBuilder},
6    InteractionKind,
7};
8
9use super::{
10    Block, InstructionCols, MemoryAccessTimestampCols, MemoryCols, OpcodeSelectorCols,
11    RangeCheckOpcode,
12};
13
14/// A trait which contains all helper methods for building SP1 recursion machine AIRs.
15pub trait SP1RecursionAirBuilder:
16    MachineAirBuilder + RecursionMemoryAirBuilder + RecursionInteractionAirBuilder
17{
18}
19
20impl<AB: AirBuilderWithPublicValues + RecursionMemoryAirBuilder> SP1RecursionAirBuilder for AB {}
21impl<AB: BaseAirBuilder> RecursionMemoryAirBuilder for AB {}
22impl<AB: BaseAirBuilder> RecursionInteractionAirBuilder for AB {}
23
24pub trait RecursionMemoryAirBuilder: RecursionInteractionAirBuilder {
25    fn recursion_eval_memory_access<E: Into<Self::Expr> + Clone>(
26        &mut self,
27        timestamp: impl Into<Self::Expr>,
28        addr: impl Into<Self::Expr>,
29        memory_access: &impl MemoryCols<E, Block<E>>,
30        is_real: impl Into<Self::Expr>,
31    ) {
32        let is_real: Self::Expr = is_real.into();
33        self.assert_bool(is_real.clone());
34
35        let timestamp: Self::Expr = timestamp.into();
36        let mem_access = memory_access.access();
37
38        self.eval_memory_access_timestamp(timestamp.clone(), mem_access, is_real.clone());
39
40        let addr = addr.into();
41        let prev_timestamp = mem_access.prev_timestamp.clone().into();
42        let prev_values = once(prev_timestamp)
43            .chain(once(addr.clone()))
44            .chain(memory_access.prev_value().clone().map(Into::into))
45            .collect();
46        let current_values = once(timestamp)
47            .chain(once(addr.clone()))
48            .chain(memory_access.value().clone().map(Into::into))
49            .collect();
50
51        self.receive(
52            AirInteraction::new(prev_values, is_real.clone(), InteractionKind::Memory),
53            InteractionScope::Local,
54        );
55        self.send(
56            AirInteraction::new(current_values, is_real, InteractionKind::Memory),
57            InteractionScope::Local,
58        );
59    }
60
61    #[allow(clippy::manual_repeat_n)]
62    fn recursion_eval_memory_access_single<E: Into<Self::Expr> + Clone>(
63        &mut self,
64        timestamp: impl Into<Self::Expr>,
65        addr: impl Into<Self::Expr>,
66        memory_access: &impl MemoryCols<E, E>,
67        is_real: impl Into<Self::Expr>,
68    ) {
69        let is_real: Self::Expr = is_real.into();
70        self.assert_bool(is_real.clone());
71
72        let timestamp: Self::Expr = timestamp.into();
73        let mem_access = memory_access.access();
74
75        self.eval_memory_access_timestamp(timestamp.clone(), mem_access, is_real.clone());
76
77        let addr = addr.into();
78        let prev_timestamp = mem_access.prev_timestamp.clone().into();
79        let prev_values = once(prev_timestamp)
80            .chain(once(addr.clone()))
81            .chain(once(memory_access.prev_value().clone().into()))
82            .chain(repeat(Self::Expr::zero()).take(3))
83            .collect();
84        let current_values = once(timestamp)
85            .chain(once(addr.clone()))
86            .chain(once(memory_access.value().clone().into()))
87            .chain(repeat(Self::Expr::zero()).take(3))
88            .collect();
89
90        self.receive(
91            AirInteraction::new(prev_values, is_real.clone(), InteractionKind::Memory),
92            InteractionScope::Local,
93        );
94        self.send(
95            AirInteraction::new(current_values, is_real, InteractionKind::Memory),
96            InteractionScope::Local,
97        );
98    }
99
100    /// Verifies that the memory access happens after the previous memory access.
101    fn eval_memory_access_timestamp<E: Into<Self::Expr> + Clone>(
102        &mut self,
103        timestamp: impl Into<Self::Expr>,
104        mem_access: &impl MemoryAccessTimestampCols<E>,
105        is_real: impl Into<Self::Expr> + Clone,
106    ) {
107        // We subtract one since a diff of zero is not valid.
108        let diff_minus_one: Self::Expr =
109            timestamp.into() - mem_access.prev_timestamp().clone().into() - Self::Expr::one();
110
111        // Verify that mem_access.ts_diff = mem_access.ts_diff_16bit_limb
112        // + mem_access.ts_diff_12bit_limb * 2^16.
113        self.eval_range_check_28bits(
114            diff_minus_one,
115            mem_access.diff_16bit_limb().clone(),
116            mem_access.diff_12bit_limb().clone(),
117            is_real.clone(),
118        );
119    }
120
121    /// Verifies the inputted value is within 28 bits.
122    ///
123    /// This method verifies that the inputted is less than 2^24 by doing a 16 bit and 12 bit range
124    /// check on it's limbs.  It will also verify that the limbs are correct.  This method is needed
125    /// since the memory access timestamp check (see [Self::eval_memory_access_timestamp]) needs to
126    /// assume the clk is within 28 bits.
127    fn eval_range_check_28bits(
128        &mut self,
129        value: impl Into<Self::Expr>,
130        limb_16: impl Into<Self::Expr> + Clone,
131        limb_12: impl Into<Self::Expr> + Clone,
132        is_real: impl Into<Self::Expr> + Clone,
133    ) {
134        // Verify that value = limb_16 + limb_12 * 2^16.
135        self.when(is_real.clone()).assert_eq(
136            value,
137            limb_16.clone().into() +
138                limb_12.clone().into() * Self::Expr::from_canonical_u32(1 << 16),
139        );
140
141        // Send the range checks for the limbs.
142        self.send_range_check(
143            Self::Expr::from_canonical_u8(RangeCheckOpcode::U16 as u8),
144            limb_16,
145            is_real.clone(),
146        );
147
148        self.send_range_check(
149            Self::Expr::from_canonical_u8(RangeCheckOpcode::U12 as u8),
150            limb_12,
151            is_real,
152        )
153    }
154}
155
156/// Builder trait containing helper functions to send/receive interactions.
157pub trait RecursionInteractionAirBuilder: BaseAirBuilder {
158    /// Sends a range check operation to be processed.
159    fn send_range_check(
160        &mut self,
161        range_check_opcode: impl Into<Self::Expr>,
162        val: impl Into<Self::Expr>,
163        is_real: impl Into<Self::Expr>,
164    ) {
165        self.send(
166            AirInteraction::new(
167                vec![range_check_opcode.into(), val.into()],
168                is_real.into(),
169                InteractionKind::Range,
170            ),
171            InteractionScope::Global,
172        );
173    }
174
175    /// Receives a range check operation to be processed.
176    fn receive_range_check(
177        &mut self,
178        range_check_opcode: impl Into<Self::Expr>,
179        val: impl Into<Self::Expr>,
180        is_real: impl Into<Self::Expr>,
181    ) {
182        self.receive(
183            AirInteraction::new(
184                vec![range_check_opcode.into(), val.into()],
185                is_real.into(),
186                InteractionKind::Range,
187            ),
188            InteractionScope::Global,
189        );
190    }
191
192    fn send_program<E: Into<Self::Expr> + Copy>(
193        &mut self,
194        pc: impl Into<Self::Expr>,
195        instruction: InstructionCols<E>,
196        selectors: OpcodeSelectorCols<E>,
197        is_real: impl Into<Self::Expr>,
198    ) {
199        let program_interaction_vals = once(pc.into())
200            .chain(instruction.into_iter().map(|x| x.into()))
201            .chain(selectors.into_iter().map(|x| x.into()))
202            .collect::<Vec<_>>();
203        self.send(
204            AirInteraction::new(program_interaction_vals, is_real.into(), InteractionKind::Program),
205            InteractionScope::Global,
206        );
207    }
208
209    fn receive_program<E: Into<Self::Expr> + Copy>(
210        &mut self,
211        pc: impl Into<Self::Expr>,
212        instruction: InstructionCols<E>,
213        selectors: OpcodeSelectorCols<E>,
214        is_real: impl Into<Self::Expr>,
215    ) {
216        let program_interaction_vals = once(pc.into())
217            .chain(instruction.into_iter().map(|x| x.into()))
218            .chain(selectors.into_iter().map(|x| x.into()))
219            .collect::<Vec<_>>();
220        self.receive(
221            AirInteraction::new(program_interaction_vals, is_real.into(), InteractionKind::Program),
222            InteractionScope::Global,
223        );
224    }
225
226    fn send_table<E: Into<Self::Expr> + Clone>(
227        &mut self,
228        opcode: impl Into<Self::Expr>,
229        table: &[E],
230        is_real: impl Into<Self::Expr>,
231    ) {
232        let table_interaction_vals = table.iter().map(|x| x.clone().into());
233        let values = once(opcode.into()).chain(table_interaction_vals).collect();
234        self.send(
235            AirInteraction::new(values, is_real.into(), InteractionKind::Syscall),
236            InteractionScope::Local,
237        );
238    }
239
240    fn receive_table<E: Into<Self::Expr> + Clone>(
241        &mut self,
242        opcode: impl Into<Self::Expr>,
243        table: &[E],
244        is_real: impl Into<Self::Expr>,
245    ) {
246        let table_interaction_vals = table.iter().map(|x| x.clone().into());
247        let values = once(opcode.into()).chain(table_interaction_vals).collect();
248        self.receive(
249            AirInteraction::new(values, is_real.into(), InteractionKind::Syscall),
250            InteractionScope::Local,
251        );
252    }
253}
sp1_recursion_core/air/builder.rs

sp1_recursion_core/air/
builder.rs
