sp1_recursion_core/air/
builder.rs

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

sp1_recursion_core/air/
builder.rs
