sp1_recursion_machine/chips/
select.rs1use core::borrow::Borrow;
2use slop_air::{Air, BaseAir, PairBuilder};
3use slop_algebra::{Field, PrimeField32};
4use slop_matrix::Matrix;
5use slop_maybe_rayon::prelude::{IndexedParallelIterator, ParallelIterator, ParallelSliceMut};
6use sp1_derive::AlignedBorrow;
7use sp1_hypercube::{air::MachineAir, next_multiple_of_32};
8use sp1_primitives::SP1Field;
9use sp1_recursion_executor::{
10 Address, ExecutionRecord, Instruction, RecursionProgram, SelectInstr, SelectIo,
11};
12use std::{borrow::BorrowMut, mem::MaybeUninit};
13
14use crate::builder::SP1RecursionAirBuilder;
15
16#[derive(Default, Clone)]
17pub struct SelectChip;
18
19pub const SELECT_COLS: usize = core::mem::size_of::<SelectCols<u8>>();
20
21#[derive(AlignedBorrow, Debug, Clone, Copy)]
22#[repr(C)]
23pub struct SelectCols<F: Copy> {
24 pub vals: SelectIo<F>,
25}
26
27pub const SELECT_PREPROCESSED_COLS: usize = core::mem::size_of::<SelectPreprocessedCols<u8>>();
28
29#[derive(AlignedBorrow, Debug, Clone, Copy)]
30#[repr(C)]
31pub struct SelectPreprocessedCols<F: Copy> {
32 pub is_real: F,
33 pub addrs: SelectIo<Address<F>>,
34 pub mult1: F,
35 pub mult2: F,
36}
37
38impl<F: Field> BaseAir<F> for SelectChip {
39 fn width(&self) -> usize {
40 SELECT_COLS
41 }
42}
43
44impl<F: PrimeField32> MachineAir<F> for SelectChip {
45 type Record = ExecutionRecord<F>;
46
47 type Program = RecursionProgram<F>;
48
49 fn name(&self) -> &'static str {
50 "Select"
51 }
52
53 fn preprocessed_width(&self) -> usize {
54 SELECT_PREPROCESSED_COLS
55 }
56
57 fn preprocessed_num_rows(&self, program: &Self::Program) -> Option<usize> {
58 let instrs_len = program
59 .inner
60 .iter()
61 .filter_map(|instruction| match instruction.inner() {
62 Instruction::Select(x) => Some(x),
63 _ => None,
64 })
65 .count();
66 self.preprocessed_num_rows_with_instrs_len(program, instrs_len)
67 }
68
69 fn preprocessed_num_rows_with_instrs_len(
70 &self,
71 program: &Self::Program,
72 instrs_len: usize,
73 ) -> Option<usize> {
74 let height = program.shape.as_ref().and_then(|shape| shape.height(self));
75 Some(next_multiple_of_32(instrs_len, height))
76 }
77
78 fn generate_preprocessed_trace_into(
79 &self,
80 program: &Self::Program,
81 buffer: &mut [MaybeUninit<F>],
82 ) {
83 assert_eq!(
84 std::any::TypeId::of::<F>(),
85 std::any::TypeId::of::<SP1Field>(),
86 "generate_preprocessed_trace only supports SP1Field field"
87 );
88
89 let instrs = program
90 .inner
91 .iter()
92 .filter_map(|instruction| match instruction.inner() {
93 Instruction::Select(x) => Some(x),
94 _ => None,
95 })
96 .collect::<Vec<_>>();
97 let padded_nb_rows =
98 self.preprocessed_num_rows_with_instrs_len(program, instrs.len()).unwrap();
99
100 let buffer_ptr = buffer.as_mut_ptr() as *mut F;
101 let values = unsafe {
102 core::slice::from_raw_parts_mut(buffer_ptr, padded_nb_rows * SELECT_PREPROCESSED_COLS)
103 };
104
105 unsafe {
106 let padding_start = instrs.len() * SELECT_PREPROCESSED_COLS;
107 let padding_size = padded_nb_rows * SELECT_PREPROCESSED_COLS - padding_start;
108 if padding_size > 0 {
109 core::ptr::write_bytes(buffer[padding_start..].as_mut_ptr(), 0, padding_size);
110 }
111 }
112
113 let populate_len = instrs.len() * SELECT_PREPROCESSED_COLS;
115 values[..populate_len].par_chunks_mut(SELECT_PREPROCESSED_COLS).zip_eq(instrs).for_each(
116 |(row, instr)| {
117 let SelectInstr { addrs, mult1, mult2 } = instr;
118 let access: &mut SelectPreprocessedCols<_> = row.borrow_mut();
119 *access = SelectPreprocessedCols {
120 is_real: F::one(),
121 addrs: addrs.to_owned(),
122 mult1: mult1.to_owned(),
123 mult2: mult2.to_owned(),
124 };
125 },
126 );
127 }
128
129 fn generate_dependencies(&self, _: &Self::Record, _: &mut Self::Record) {
130 }
132
133 fn num_rows(&self, input: &Self::Record) -> Option<usize> {
134 let height = input.program.shape.as_ref().and_then(|shape| shape.height(self));
135 let events = &input.select_events;
136 Some(next_multiple_of_32(events.len(), height))
137 }
138
139 fn generate_trace_into(
140 &self,
141 input: &ExecutionRecord<F>,
142 _: &mut ExecutionRecord<F>,
143 buffer: &mut [MaybeUninit<F>],
144 ) {
145 assert_eq!(
146 std::any::TypeId::of::<F>(),
147 std::any::TypeId::of::<SP1Field>(),
148 "generate_trace_into only supports SP1Field"
149 );
150 let padded_nb_rows = <SelectChip as MachineAir<F>>::num_rows(self, input).unwrap();
151 let events = &input.select_events;
152 let num_event_rows = events.len();
153
154 unsafe {
155 let padding_start = num_event_rows * SELECT_COLS;
156 let padding_size = (padded_nb_rows - num_event_rows) * SELECT_COLS;
157 if padding_size > 0 {
158 core::ptr::write_bytes(buffer[padding_start..].as_mut_ptr(), 0, padding_size);
159 }
160 }
161
162 let buffer_ptr = buffer.as_mut_ptr() as *mut F;
163 let values =
164 unsafe { core::slice::from_raw_parts_mut(buffer_ptr, num_event_rows * SELECT_COLS) };
165
166 let populate_len = events.len() * SELECT_COLS;
168 values[..populate_len].par_chunks_mut(SELECT_COLS).zip_eq(events).for_each(
169 |(row, &vals)| {
170 let cols: &mut SelectCols<_> = row.borrow_mut();
171 *cols = SelectCols { vals };
172 },
173 );
174 }
175
176 fn included(&self, _record: &Self::Record) -> bool {
177 true
178 }
179}
180
181impl<AB> Air<AB> for SelectChip
182where
183 AB: SP1RecursionAirBuilder + PairBuilder,
184{
185 fn eval(&self, builder: &mut AB) {
186 let main = builder.main();
187 let local = main.row_slice(0);
188 let local: &SelectCols<AB::Var> = (*local).borrow();
189 let prep = builder.preprocessed();
190 let prep_local = prep.row_slice(0);
191 let prep_local: &SelectPreprocessedCols<AB::Var> = (*prep_local).borrow();
192
193 builder.receive_single(prep_local.addrs.bit, local.vals.bit, prep_local.is_real);
195 builder.receive_single(prep_local.addrs.in1, local.vals.in1, prep_local.is_real);
196 builder.receive_single(prep_local.addrs.in2, local.vals.in2, prep_local.is_real);
197
198 builder.assert_bool(local.vals.bit);
200
201 builder.assert_eq(
203 local.vals.out1,
204 local.vals.in1 + local.vals.bit * (local.vals.in2 - local.vals.in1),
205 );
206 builder.assert_eq(local.vals.out1 + local.vals.out2, local.vals.in1 + local.vals.in2);
208
209 builder.send_single(prep_local.addrs.out1, local.vals.out1, prep_local.mult1);
211 builder.send_single(prep_local.addrs.out2, local.vals.out2, prep_local.mult2);
212 }
213}
214
215#[cfg(test)]
216mod tests {
217 use crate::{chips::test_fixtures, test::test_recursion_linear_program};
218 use rand::{rngs::StdRng, Rng, SeedableRng};
219 use slop_algebra::AbstractField;
220 use slop_challenger::IopCtx;
221 use sp1_primitives::SP1GlobalContext;
222 use sp1_recursion_executor::{instruction as instr, MemAccessKind};
223
224 use super::*;
225
226 #[tokio::test]
227 async fn prove_select() {
228 type F = <SP1GlobalContext as IopCtx>::F;
229
230 let mut rng = StdRng::seed_from_u64(0xDEADBEEF);
231 let mut addr = 0;
232
233 let instructions = (0..1000)
234 .flat_map(|_| {
235 let in1: F = rng.sample(rand::distributions::Standard);
236 let in2: F = rng.sample(rand::distributions::Standard);
237 let bit = F::from_bool(rng.gen_bool(0.5));
238 assert_eq!(bit * (bit - F::one()), F::zero());
239
240 let (out1, out2) = if bit == F::one() { (in2, in1) } else { (in1, in2) };
241 let alloc_size = 5;
242 let a = (0..alloc_size).map(|x| x + addr).collect::<Vec<_>>();
243 addr += alloc_size;
244 [
245 instr::mem_single(MemAccessKind::Write, 1, a[0], bit),
246 instr::mem_single(MemAccessKind::Write, 1, a[3], in1),
247 instr::mem_single(MemAccessKind::Write, 1, a[4], in2),
248 instr::select(1, 1, a[0], a[1], a[2], a[3], a[4]),
249 instr::mem_single(MemAccessKind::Read, 1, a[1], out1),
250 instr::mem_single(MemAccessKind::Read, 1, a[2], out2),
251 ]
252 })
253 .collect::<Vec<Instruction<F>>>();
254
255 test_recursion_linear_program(instructions).await;
256 }
257
258 #[tokio::test]
259 async fn generate_trace() {
260 let shard = test_fixtures::shard().await;
261 let trace = SelectChip.generate_trace(shard, &mut ExecutionRecord::default());
262 assert!(trace.height() > test_fixtures::MIN_ROWS);
263 }
264
265 #[tokio::test]
266 async fn generate_preprocessed_trace() {
267 let program = &test_fixtures::program_with_input().await.0;
268 let trace = SelectChip.generate_preprocessed_trace(program).unwrap();
269 assert!(trace.height() > test_fixtures::MIN_ROWS);
270 }
271}