sp1_core_machine/syscall/precompiles/mprotect/
air.rs

1use crate::{
2    air::{SP1CoreAirBuilder, SP1Operation},
3    memory::PageProtAccessCols,
4    operations::{LtOperationUnsigned, LtOperationUnsignedInput},
5    utils::next_multiple_of_32,
6};
7use core::borrow::Borrow;
8use slop_air::{Air, AirBuilder, BaseAir};
9use slop_algebra::{AbstractField, PrimeField32};
10use slop_matrix::Matrix;
11use sp1_core_executor::{
12    events::{ByteLookupEvent, ByteRecord, PrecompileEvent},
13    ByteOpcode, ExecutionRecord, Program, SyscallCode,
14};
15use sp1_derive::AlignedBorrow;
16#[cfg(feature = "mprotect")]
17use sp1_hypercube::{addr_to_limbs, air::BaseAirBuilder};
18use sp1_hypercube::{
19    air::{InteractionScope, MachineAir},
20    Word,
21};
22use sp1_primitives::consts::{PROT_EXEC, PROT_READ, PROT_WRITE};
23use std::{borrow::BorrowMut, mem::MaybeUninit};
24
25/// The number of columns in the MProtectCols.
26const NUM_COLS: usize = size_of::<MProtectCols<u8>>();
27
28#[derive(Default)]
29pub struct MProtectChip;
30
31impl MProtectChip {
32    pub const fn new() -> Self {
33        Self
34    }
35}
36
37/// A set of columns for the MProtect operation.
38#[derive(Debug, Clone, AlignedBorrow)]
39#[repr(C)]
40pub struct MProtectCols<T> {
41    /// Clock cycle of the syscall (split into high and low parts)
42    pub clk_high: T,
43    pub clk_low: T,
44
45    /// Address being protected (page-aligned) - 48 bits split into 3x16-bit limbs
46    pub addr: [T; 3],
47
48    /// Split the least significant limb: 4 MSBs and 12 LSBs for page alignment
49    pub addr_4_bits: T,
50    pub addr_12_bits: T,
51
52    /// Protection flags (8 bits)
53    pub prot: T,
54
55    /// Individual protection flag bits
56    pub prot_read: T,
57    pub prot_write: T,
58    pub prot_exec: T,
59
60    /// Whether this row is real
61    pub is_real: T,
62
63    /// Interaction with page protection table
64    pub page_prot_access: PageProtAccessCols<T>,
65
66    /// The untrusted memory region from public values.
67    pub untrusted_memory: [[T; 3]; 2],
68
69    /// Comparison with untrusted memory.
70    pub addr_range_check: [LtOperationUnsigned<T>; 2],
71}
72
73impl<F> BaseAir<F> for MProtectChip {
74    fn width(&self) -> usize {
75        NUM_COLS
76    }
77}
78
79impl<F: PrimeField32> MachineAir<F> for MProtectChip {
80    type Record = ExecutionRecord;
81    type Program = Program;
82
83    fn name(&self) -> &'static str {
84        "Mprotect"
85    }
86
87    fn num_rows(&self, input: &Self::Record) -> Option<usize> {
88        let nb_rows = input.get_precompile_events(SyscallCode::MPROTECT).len();
89        let size_log2 = input.fixed_log2_rows::<F, _>(self);
90        let padded_nb_rows = next_multiple_of_32(nb_rows, size_log2);
91        Some(padded_nb_rows)
92    }
93
94    fn generate_trace_into(
95        &self,
96        input: &ExecutionRecord,
97        output: &mut ExecutionRecord,
98        buffer: &mut [MaybeUninit<F>],
99    ) {
100        let padded_nb_rows = <MProtectChip as MachineAir<F>>::num_rows(self, input).unwrap();
101        let mut blu_events = Vec::new();
102
103        let mprotect_events = input.get_precompile_events(SyscallCode::MPROTECT);
104        let num_event_rows = mprotect_events.len();
105        if input.public_values.is_untrusted_programs_enabled == 0 {
106            assert!(
107                mprotect_events.is_empty(),
108                "Page protect is disabled, but mprotect events are present"
109            );
110        }
111
112        unsafe {
113            let padding_start = num_event_rows * NUM_COLS;
114            let padding_size = (padded_nb_rows - num_event_rows) * NUM_COLS;
115            if padding_size > 0 {
116                core::ptr::write_bytes(buffer[padding_start..].as_mut_ptr(), 0, padding_size);
117            }
118        }
119
120        let buffer_ptr = buffer.as_mut_ptr() as *mut F;
121        let values =
122            unsafe { core::slice::from_raw_parts_mut(buffer_ptr, num_event_rows * NUM_COLS) };
123
124        values.chunks_mut(NUM_COLS).enumerate().for_each(|(idx, row)| {
125            let event = &mprotect_events[idx].1;
126            let event =
127                if let PrecompileEvent::Mprotect(event) = event { event } else { unreachable!() };
128
129            let cols: &mut MProtectCols<F> = row.borrow_mut();
130            // Set clock
131            assert!(event.local_page_prot_access.len() == 1);
132            let clk = event.local_page_prot_access[0].final_page_prot_access.timestamp;
133            cols.clk_high = F::from_canonical_u32((clk >> 24) as u32);
134            cols.clk_low = F::from_canonical_u32((clk & 0xFFFFFF) as u32);
135
136            // Set address (split into 3x16-bit limbs)
137            cols.addr[0] = F::from_canonical_u32((event.addr & 0xFFFF) as u32);
138            cols.addr[1] = F::from_canonical_u32(((event.addr >> 16) & 0xFFFF) as u32);
139            cols.addr[2] = F::from_canonical_u32(((event.addr >> 32) & 0xFFFF) as u32);
140
141            // Split least significant limb: 4 MSBs and 12 LSBs
142            let addr_12_bits = (event.addr & 0xFFF) as u16; // bits [11:0]
143            let addr_4_bits = ((event.addr >> 12) & 0xF) as u16; // bits [15:12]
144
145            cols.addr_12_bits = F::from_canonical_u16(addr_12_bits);
146            cols.addr_4_bits = F::from_canonical_u16(addr_4_bits);
147
148            // Add range check events for addr_4_bits (log₂(16)=4) and addr_12_bits (log₂(4096)=12)
149            blu_events.push(ByteLookupEvent {
150                opcode: ByteOpcode::Range,
151                a: addr_4_bits,
152                b: 4,
153                c: 0,
154            });
155
156            blu_events.push(ByteLookupEvent {
157                opcode: ByteOpcode::Range,
158                a: addr_12_bits,
159                b: 12, // log₂(4096) = 12
160                c: 0,
161            });
162
163            // Set protection flags
164            let page_prot = event.local_page_prot_access[0].final_page_prot_access.page_prot;
165            cols.prot = F::from_canonical_u8(page_prot);
166            cols.prot_read = if page_prot & PROT_READ != 0 { F::one() } else { F::zero() };
167            cols.prot_write = if page_prot & PROT_WRITE != 0 { F::one() } else { F::zero() };
168            cols.prot_exec = if page_prot & PROT_EXEC != 0 { F::one() } else { F::zero() };
169
170            cols.page_prot_access.populate(
171                &event.local_page_prot_access[0].initial_page_prot_access,
172                clk,
173                &mut blu_events,
174            );
175
176            cols.is_real = F::one();
177            #[cfg(feature = "mprotect")]
178            {
179                cols.untrusted_memory[0] = addr_to_limbs(input.public_values.untrusted_memory[0]);
180                cols.untrusted_memory[1] = addr_to_limbs(input.public_values.untrusted_memory[1]);
181
182                // Check that `addr < mem[0]` is false.
183                cols.addr_range_check[0].populate_unsigned(
184                    &mut blu_events,
185                    0,
186                    event.addr,
187                    input.public_values.untrusted_memory[0],
188                );
189                // Check that `addr < mem[1]` is true.
190                cols.addr_range_check[1].populate_unsigned(
191                    &mut blu_events,
192                    1,
193                    event.addr,
194                    input.public_values.untrusted_memory[1],
195                );
196            }
197        });
198
199        // Add byte lookup events to output
200        output.add_byte_lookup_events(blu_events);
201    }
202
203    fn included(&self, shard: &Self::Record) -> bool {
204        if let Some(shape) = shard.shape.as_ref() {
205            shape.included::<F, _>(self)
206        } else {
207            !shard.get_precompile_events(SyscallCode::MPROTECT).is_empty()
208        }
209    }
210}
211
212impl<AB> Air<AB> for MProtectChip
213where
214    AB: SP1CoreAirBuilder,
215{
216    fn eval(&self, builder: &mut AB) {
217        let main = builder.main();
218        let local = main.row_slice(0);
219        let local: &MProtectCols<AB::Var> = (*local).borrow();
220
221        let public_values = builder.extract_public_values();
222
223        builder.assert_bool(local.is_real);
224        builder.assert_eq(public_values.is_untrusted_programs_enabled, AB::Expr::one());
225        #[cfg(feature = "mprotect")]
226        {
227            builder
228                .when(local.is_real)
229                .assert_all_eq(public_values.untrusted_memory[0], local.untrusted_memory[0]);
230            builder
231                .when(local.is_real)
232                .assert_all_eq(public_values.untrusted_memory[1], local.untrusted_memory[1]);
233        }
234        #[cfg(not(feature = "mprotect"))]
235        builder.assert_zero(local.is_real);
236
237        // Check that `addr < untrusted_memory[0]` is false, so `addr >= untrusted_memory[0]`.
238        <LtOperationUnsigned<AB::F> as SP1Operation<AB>>::eval(
239            builder,
240            LtOperationUnsignedInput::<AB>::new(
241                Word([
242                    local.addr[0].into(),
243                    local.addr[1].into(),
244                    local.addr[2].into(),
245                    AB::Expr::zero(),
246                ]),
247                Word([
248                    local.untrusted_memory[0][0].into(),
249                    local.untrusted_memory[0][1].into(),
250                    local.untrusted_memory[0][2].into(),
251                    AB::Expr::zero(),
252                ]),
253                local.addr_range_check[0],
254                local.is_real.into(),
255            ),
256        );
257        builder
258            .when(local.is_real)
259            .assert_zero(local.addr_range_check[0].u16_compare_operation.bit);
260
261        // Check that `addr < untrusted_memory[1]` is true.
262        <LtOperationUnsigned<AB::F> as SP1Operation<AB>>::eval(
263            builder,
264            LtOperationUnsignedInput::<AB>::new(
265                Word([
266                    local.addr[0].into(),
267                    local.addr[1].into(),
268                    local.addr[2].into(),
269                    AB::Expr::zero(),
270                ]),
271                Word([
272                    local.untrusted_memory[1][0].into(),
273                    local.untrusted_memory[1][1].into(),
274                    local.untrusted_memory[1][2].into(),
275                    AB::Expr::zero(),
276                ]),
277                local.addr_range_check[1],
278                local.is_real.into(),
279            ),
280        );
281        builder.when(local.is_real).assert_one(local.addr_range_check[1].u16_compare_operation.bit);
282
283        // Constrain address decomposition - addr[0] should equal addr_12_bits + addr_4_bits * 4096
284        builder.when(local.is_real).assert_eq(
285            local.addr[0],
286            local.addr_12_bits + local.addr_4_bits * AB::Expr::from_canonical_u32(4096),
287        );
288
289        // Range check addr_4_bits and addr_12_bits using byte interactions
290        builder.send_byte(
291            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
292            local.addr_4_bits.into(),
293            AB::Expr::from_canonical_u32(4), // log₂(16) = 4
294            AB::Expr::zero(),
295            local.is_real,
296        );
297
298        builder.send_byte(
299            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
300            local.addr_12_bits.into(),
301            AB::Expr::from_canonical_u32(12), // log₂(4096) = 12
302            AB::Expr::zero(),
303            local.is_real,
304        );
305
306        // Address must be page-aligned (addr_12_bits should be 0 since PAGE_SIZE = 4096)
307        builder.when(local.is_real).assert_zero(local.addr_12_bits);
308
309        // Constrain protection flag decomposition
310        builder.assert_bool(local.prot_read);
311        builder.assert_bool(local.prot_write);
312        builder.assert_bool(local.prot_exec);
313
314        // Create expected bitmap from individual flag bits
315        let expected_prot = local.prot_read * AB::Expr::from_canonical_u8(PROT_READ)
316            + local.prot_write * AB::Expr::from_canonical_u8(PROT_WRITE)
317            + local.prot_exec * AB::Expr::from_canonical_u8(PROT_EXEC);
318
319        // Ensure the reconstructed prot matches the original
320        builder.when(local.is_real).assert_eq(local.prot, expected_prot.clone());
321
322        // Receive the syscall interaction
323        builder.receive_syscall(
324            local.clk_high,
325            local.clk_low,
326            AB::F::from_canonical_u32(SyscallCode::MPROTECT.syscall_id()),
327            AB::Expr::zero(),
328            local.addr.map(Into::into),
329            [local.prot.into(), AB::Expr::zero(), AB::Expr::zero()],
330            local.is_real,
331            InteractionScope::Local,
332        );
333
334        // Update page protection using the write function
335        builder.eval_page_prot_access_write(
336            local.clk_high,
337            local.clk_low,
338            &[local.addr_4_bits, local.addr[1], local.addr[2]],
339            local.page_prot_access,
340            expected_prot,
341            local.is_real,
342        );
343    }
344}
sp1_core_machine/syscall/precompiles/mprotect/air.rs

sp1_core_machine/syscall/precompiles/mprotect/
air.rs
