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 fn generate_trace(&self, input: &Self::Record, _: &mut Self::Record) -> RowMajorMatrix<F> {
106 let num_rows = input
108 .mem_const_count
109 .checked_sub(1)
110 .map(|x| x / NUM_CONST_MEM_ENTRIES_PER_ROW + 1)
111 .unwrap_or_default();
112 let mut rows =
113 std::iter::repeat([F::zero(); NUM_MEM_INIT_COLS]).take(num_rows).collect::<Vec<_>>();
114
115 pad_rows_fixed(&mut rows, || [F::zero(); NUM_MEM_INIT_COLS], input.fixed_log2_rows(self));
117
118 RowMajorMatrix::new(rows.into_iter().flatten().collect::<Vec<_>>(), NUM_MEM_INIT_COLS)
120 }
121
122 fn included(&self, _record: &Self::Record) -> bool {
123 true
124 }
125
126 fn local_only(&self) -> bool {
127 true
128 }
129}
130
131impl<AB> Air<AB> for MemoryChip<AB::F>
132where
133 AB: SP1RecursionAirBuilder + PairBuilder,
134{
135 fn eval(&self, builder: &mut AB) {
136 let prep = builder.preprocessed();
137 let prep_local = prep.row_slice(0);
138 let prep_local: &MemoryPreprocessedCols<AB::Var> = (*prep_local).borrow();
139
140 for (value, access) in prep_local.values_and_accesses {
141 builder.send_block(access.addr, value, access.mult);
142 }
143 }
144}
145
146#[cfg(test)]
147mod tests {
148 use machine::tests::test_recursion_linear_program;
149
150 use super::*;
151
152 use crate::runtime::instruction as instr;
153
154 #[test]
155 pub fn prove_basic_mem() {
156 test_recursion_linear_program(vec![
157 instr::mem(MemAccessKind::Write, 1, 1, 2),
158 instr::mem(MemAccessKind::Read, 1, 1, 2),
159 ]);
160 }
161
162 #[test]
163 #[should_panic]
164 pub fn basic_mem_bad_mult() {
165 test_recursion_linear_program(vec![
166 instr::mem(MemAccessKind::Write, 1, 1, 2),
167 instr::mem(MemAccessKind::Read, 9, 1, 2),
168 ]);
169 }
170
171 #[test]
172 #[should_panic]
173 pub fn basic_mem_bad_address() {
174 test_recursion_linear_program(vec![
175 instr::mem(MemAccessKind::Write, 1, 1, 2),
176 instr::mem(MemAccessKind::Read, 1, 9, 2),
177 ]);
178 }
179
180 #[test]
181 #[should_panic]
182 pub fn basic_mem_bad_value() {
183 test_recursion_linear_program(vec![
184 instr::mem(MemAccessKind::Write, 1, 1, 2),
185 instr::mem(MemAccessKind::Read, 1, 1, 999),
186 ]);
187 }
188}