sp1_core_machine/operations/
syscall_addr.rs

1use slop_air::AirBuilder;
2use slop_algebra::{AbstractField, Field, PrimeField32};
3use sp1_derive::AlignedBorrow;
4
5use sp1_core_executor::{events::ByteRecord, ByteOpcode};
6use sp1_hypercube::air::SP1AirBuilder;
7use sp1_primitives::consts::u64_to_u16_limbs;
8
9use super::{IsZeroOperation, IsZeroOperationInput};
10use crate::air::{SP1Operation, SP1OperationBuilder};
11
12/// A set of columns needed to validate the address and return the aligned address.
13#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
14#[repr(C)]
15pub struct SyscallAddrOperation<T> {
16    /// The address itself.
17    pub addr: [T; 3],
18
19    /// This is used to check if the top two limbs of the address is not both zero.
20    pub top_two_limb_min: T,
21
22    /// This is used to check if the top two limbs of the address is u16::MAX.
23    pub top_two_limb_max: IsZeroOperation<T>,
24}
25
26impl<F: PrimeField32> SyscallAddrOperation<F> {
27    pub fn populate(&mut self, record: &mut impl ByteRecord, addr: u64, len: u64) {
28        let addr_limbs = u64_to_u16_limbs(addr);
29        let sum_top_two_limb =
30            F::from_canonical_u16(addr_limbs[1]) + F::from_canonical_u16(addr_limbs[2]);
31        self.addr[0] = F::from_canonical_u16(addr_limbs[0]);
32        self.addr[1] = F::from_canonical_u16(addr_limbs[1]);
33        self.addr[2] = F::from_canonical_u16(addr_limbs[2]);
34        self.top_two_limb_min = sum_top_two_limb.inverse();
35        let is_max = self.top_two_limb_max.populate_from_field_element(
36            sum_top_two_limb - F::from_canonical_u16(u16::MAX) * F::two(),
37        );
38        if is_max == 1 {
39            record.add_bit_range_check((addr_limbs[0] + (len as u16)) / 8, 13);
40        } else {
41            record.add_bit_range_check(addr_limbs[0] / 8, 13);
42        }
43    }
44}
45
46impl<F: Field> SyscallAddrOperation<F> {
47    /// The memory address is constrained to be aligned, `>= 2^16` and less than `2^48 - len`.
48    /// The `cols.addr` is assumed to be composed of valid 3 u16 limbs.
49    #[allow(clippy::too_many_arguments)]
50    pub fn eval<AB: SP1AirBuilder + SP1OperationBuilder<IsZeroOperation<<AB as AirBuilder>::F>>>(
51        builder: &mut AB,
52        len: u32,
53        cols: SyscallAddrOperation<AB::Var>,
54        is_real: AB::Expr,
55    ) -> [AB::Var; 3] {
56        // This is not a constraint, but a sanity check
57        assert!(len.is_multiple_of(8));
58
59        // Check that `is_real` and offset bits are boolean.
60        builder.assert_bool(is_real.clone());
61
62        let sum_top_two_limb = cols.addr[1] + cols.addr[2];
63
64        // Check that `addr >= 2^16`, so it doesn't touch registers.
65        // This implements a stack guard of size 2^16 bytes = 64KB.
66        // If `is_real = 1`, then `addr.0[1] + addr.0[2] != 0`, so `addr >= 2^16`.
67        builder.assert_eq(cols.top_two_limb_min * sum_top_two_limb.clone(), is_real.clone());
68
69        IsZeroOperation::<AB::F>::eval(
70            builder,
71            IsZeroOperationInput::new(
72                sum_top_two_limb.clone() - AB::Expr::from_canonical_u16(u16::MAX) * AB::Expr::two(),
73                cols.top_two_limb_max,
74                is_real.clone(),
75            ),
76        );
77
78        // Check `0 <= (addr[0] + len * top_two_limb_max.result) / 8 < 2^13`.
79        // If `addr[1] == addr[2] == u16::MAX`, this shows `addr + len < 2^48`.
80        // This also shows that `addr[0]` is a multiple of 8 in all cases.
81        builder.send_byte(
82            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
83            (cols.addr[0] + cols.top_two_limb_max.result * AB::Expr::from_canonical_u32(len))
84                * AB::F::from_canonical_u32(8).inverse(),
85            AB::Expr::from_canonical_u32(13),
86            AB::Expr::zero(),
87            is_real.clone(),
88        );
89
90        [cols.addr[0], cols.addr[1], cols.addr[2]]
91    }
92}
sp1_core_machine/operations/syscall_addr.rs

sp1_core_machine/operations/
syscall_addr.rs
