sp1_recursion_core/chips/mem/
constant.rs1use core::borrow::Borrow;
2use itertools::Itertools;
3use p3_air::{Air, BaseAir, PairBuilder};
4use p3_field::PrimeField32;
5use p3_matrix::{dense::RowMajorMatrix, Matrix};
6use sp1_core_machine::utils::pad_rows_fixed;
7use sp1_derive::AlignedBorrow;
8use sp1_stark::air::MachineAir;
9use std::{borrow::BorrowMut, iter::zip, marker::PhantomData};
10
11use crate::{builder::SP1RecursionAirBuilder, *};
12
13use super::MemoryAccessCols;
14
15pub const NUM_CONST_MEM_ENTRIES_PER_ROW: usize = 2;
16
17#[derive(Default)]
18pub struct MemoryChip<F> {
19 _marker: PhantomData<F>,
20}
21
22pub const NUM_MEM_INIT_COLS: usize = core::mem::size_of::<MemoryCols<u8>>();
23
24#[derive(AlignedBorrow, Debug, Clone, Copy)]
25#[repr(C)]
26pub struct MemoryCols<F: Copy> {
27 _nothing: F,
29}
30
31pub const NUM_MEM_PREPROCESSED_INIT_COLS: usize =
32 core::mem::size_of::<MemoryPreprocessedCols<u8>>();
33
34#[derive(AlignedBorrow, Debug, Clone, Copy)]
35#[repr(C)]
36pub struct MemoryPreprocessedCols<F: Copy> {
37 values_and_accesses: [(Block<F>, MemoryAccessCols<F>); NUM_CONST_MEM_ENTRIES_PER_ROW],
38}
39impl<F: Send + Sync> BaseAir<F> for MemoryChip<F> {
40 fn width(&self) -> usize {
41 NUM_MEM_INIT_COLS
42 }
43}
44
45impl<F: PrimeField32> MachineAir<F> for MemoryChip<F> {
46 type Record = crate::ExecutionRecord<F>;
47
48 type Program = crate::RecursionProgram<F>;
49
50 fn name(&self) -> String {
51 "MemoryConst".to_string()
52 }
53 fn preprocessed_width(&self) -> usize {
54 NUM_MEM_PREPROCESSED_INIT_COLS
55 }
56
57 fn generate_preprocessed_trace(&self, program: &Self::Program) -> Option<RowMajorMatrix<F>> {
58 let mut rows = program
59 .inner
60 .iter()
61 .filter_map(|instruction| match instruction {
62 Instruction::Mem(MemInstr { addrs, vals, mult, kind }) => {
63 let mult = mult.to_owned();
64 let mult = match kind {
65 MemAccessKind::Read => -mult,
66 MemAccessKind::Write => mult,
67 };
68
69 Some((vals.inner, MemoryAccessCols { addr: addrs.inner, mult }))
70 }
71 _ => None,
72 })
73 .chunks(NUM_CONST_MEM_ENTRIES_PER_ROW)
74 .into_iter()
75 .map(|row_vs_as| {
76 let mut row = [F::zero(); NUM_MEM_PREPROCESSED_INIT_COLS];
77 let cols: &mut MemoryPreprocessedCols<_> = row.as_mut_slice().borrow_mut();
78 for (cell, access) in zip(&mut cols.values_and_accesses, row_vs_as) {
79 *cell = access;
80 }
81 row
82 })
83 .collect::<Vec<_>>();
84
85 pad_rows_fixed(
87 &mut rows,
88 || [F::zero(); NUM_MEM_PREPROCESSED_INIT_COLS],
89 program.fixed_log2_rows(self),
90 );
91
92 let trace = RowMajorMatrix::new(
94 rows.into_iter().flatten().collect::<Vec<_>>(),
95 NUM_MEM_PREPROCESSED_INIT_COLS,
96 );
97
98 Some(trace)
99 }
100
101 fn generate_dependencies(&self, _: &Self::Record, _: &mut Self::Record) {
102 }
104
105 #[allow(clippy::manual_repeat_n)]
106 fn generate_trace(&self, input: &Self::Record, _: &mut Self::Record) -> RowMajorMatrix<F> {
107 let num_rows = input
109 .mem_const_count
110 .checked_sub(1)
111 .map(|x| x / NUM_CONST_MEM_ENTRIES_PER_ROW + 1)
112 .unwrap_or_default();
113 let mut rows =
114 std::iter::repeat([F::zero(); NUM_MEM_INIT_COLS]).take(num_rows).collect::<Vec<_>>();
115
116 pad_rows_fixed(&mut rows, || [F::zero(); NUM_MEM_INIT_COLS], input.fixed_log2_rows(self));
118
119 RowMajorMatrix::new(rows.into_iter().flatten().collect::<Vec<_>>(), NUM_MEM_INIT_COLS)
121 }
122
123 fn included(&self, _record: &Self::Record) -> bool {
124 true
125 }
126
127 fn local_only(&self) -> bool {
128 true
129 }
130}
131
132impl<AB> Air<AB> for MemoryChip<AB::F>
133where
134 AB: SP1RecursionAirBuilder + PairBuilder,
135{
136 fn eval(&self, builder: &mut AB) {
137 let prep = builder.preprocessed();
138 let prep_local = prep.row_slice(0);
139 let prep_local: &MemoryPreprocessedCols<AB::Var> = (*prep_local).borrow();
140
141 for (value, access) in prep_local.values_and_accesses {
142 builder.send_block(access.addr, value, access.mult);
143 }
144 }
145}
146
147#[cfg(test)]
148mod tests {
149 use machine::tests::test_recursion_linear_program;
150
151 use super::*;
152
153 use crate::runtime::instruction as instr;
154
155 #[test]
156 pub fn prove_basic_mem() {
157 test_recursion_linear_program(vec![
158 instr::mem(MemAccessKind::Write, 1, 1, 2),
159 instr::mem(MemAccessKind::Read, 1, 1, 2),
160 ]);
161 }
162
163 #[test]
164 #[should_panic]
165 pub fn basic_mem_bad_mult() {
166 test_recursion_linear_program(vec![
167 instr::mem(MemAccessKind::Write, 1, 1, 2),
168 instr::mem(MemAccessKind::Read, 9, 1, 2),
169 ]);
170 }
171
172 #[test]
173 #[should_panic]
174 pub fn basic_mem_bad_address() {
175 test_recursion_linear_program(vec![
176 instr::mem(MemAccessKind::Write, 1, 1, 2),
177 instr::mem(MemAccessKind::Read, 1, 9, 2),
178 ]);
179 }
180
181 #[test]
182 #[should_panic]
183 pub fn basic_mem_bad_value() {
184 test_recursion_linear_program(vec![
185 instr::mem(MemAccessKind::Write, 1, 1, 2),
186 instr::mem(MemAccessKind::Read, 1, 1, 999),
187 ]);
188 }
189}