sp1_core_machine/operations/
address.rs

1use serde::{Deserialize, Serialize};
2use slop_air::AirBuilder;
3use slop_algebra::{AbstractField, Field, PrimeField32};
4use sp1_derive::{AlignedBorrow, InputExpr, InputParams, IntoShape, SP1OperationBuilder};
5
6use sp1_core_executor::{events::ByteRecord, ByteOpcode};
7use sp1_hypercube::{air::SP1AirBuilder, Word};
8use sp1_primitives::consts::u64_to_u16_limbs;
9use struct_reflection::{StructReflection, StructReflectionHelper};
10
11use crate::air::{SP1Operation, SP1OperationBuilder};
12
13use super::{AddrAddOperation, AddrAddOperationInput};
14
15/// A set of columns needed to validate the address and return the aligned address.
16#[derive(
17    AlignedBorrow,
18    StructReflection,
19    Default,
20    Debug,
21    Clone,
22    Copy,
23    Serialize,
24    Deserialize,
25    IntoShape,
26    SP1OperationBuilder,
27)]
28#[repr(C)]
29pub struct AddressOperation<T> {
30    /// Instance of `AddOperation` for addr.
31    pub addr_operation: AddrAddOperation<T>,
32
33    /// This is used to check if the top two limbs of the address is not both zero.
34    pub top_two_limb_inv: T,
35}
36
37impl<F: PrimeField32> AddressOperation<F> {
38    pub fn populate(&mut self, record: &mut impl ByteRecord, b: u64, c: u64) -> u64 {
39        let memory_addr = b.wrapping_add(c);
40        let addr_limbs = u64_to_u16_limbs(memory_addr);
41        self.addr_operation.populate(record, b, c);
42        let sum_top_two_limb =
43            F::from_canonical_u16(addr_limbs[1]) + F::from_canonical_u16(addr_limbs[2]);
44        self.top_two_limb_inv = sum_top_two_limb.inverse();
45        record.add_bit_range_check(addr_limbs[0] / 8, 13);
46        memory_addr
47    }
48}
49
50impl<F: Field> AddressOperation<F> {
51    /// Given `op_b` and `op_c` in a memory opcode, derive the memory address.
52    /// The memory address is constrained to be `>= 2^16` and less than 2^48.
53    /// Both `is_real` and offset bits are constrained to be boolean and correct.
54    /// The returned value is the aligned memory address used for memory access.
55    #[allow(clippy::too_many_arguments)]
56    pub fn eval<AB>(
57        builder: &mut AB,
58        b: Word<AB::Expr>,
59        c: Word<AB::Expr>,
60        offset_bit0: AB::Expr,
61        offset_bit1: AB::Expr,
62        offset_bit2: AB::Expr,
63        is_real: AB::Expr,
64        cols: AddressOperation<AB::Var>,
65    ) -> [AB::Expr; 3]
66    where
67        AB: SP1AirBuilder + SP1OperationBuilder<AddrAddOperation<<AB as AirBuilder>::F>>,
68    {
69        // Check that `is_real` and offset bits are boolean.
70        builder.assert_bool(is_real.clone());
71        builder.assert_bool(offset_bit0.clone());
72        builder.assert_bool(offset_bit1.clone());
73        builder.assert_bool(offset_bit2.clone());
74
75        // `addr` is computed as `op_b + op_c`, and is range checked to be three u16 limbs.
76        <AddrAddOperation<AB::F> as SP1Operation<AB>>::eval(
77            builder,
78            AddrAddOperationInput::new(b, c, cols.addr_operation, is_real.clone()),
79        );
80        let addr = cols.addr_operation.value;
81
82        let sum_top_two_limb = addr[1] + addr[2];
83
84        // Check that `addr >= 2^16`, so it doesn't touch registers.
85        // This implements a stack guard of size 2^16 bytes = 64KB.
86        // If `is_real = 1`, then `addr[1] + addr[2] != 0`, so `addr >= 2^16`.
87        builder.assert_eq(cols.top_two_limb_inv * sum_top_two_limb.clone(), is_real.clone());
88
89        // Check `0 <= (addr[0] - 4 * bit2 - 2 * bit1 - bit0) / 8 < 2^13`.
90        // This shows `addr[0] - 4 * bit2 - 2 * bit1 - bit0` is a multiple of `8` within `u16`.
91        builder.send_byte(
92            AB::Expr::from_canonical_u32(ByteOpcode::Range as u32),
93            (addr[0]
94                - AB::Expr::from_canonical_u32(4) * offset_bit2.clone()
95                - AB::Expr::from_canonical_u32(2) * offset_bit1.clone()
96                - offset_bit0.clone())
97                * AB::F::from_canonical_u32(8).inverse(),
98            AB::Expr::from_canonical_u32(13),
99            AB::Expr::zero(),
100            is_real.clone(),
101        );
102
103        [
104            addr[0].into()
105                - AB::Expr::from_canonical_u32(4) * offset_bit2
106                - AB::Expr::from_canonical_u32(2) * offset_bit1
107                - offset_bit0,
108            addr[1].into(),
109            addr[2].into(),
110        ]
111    }
112}
113
114#[derive(Debug, Clone, InputExpr, InputParams)]
115pub struct AddressOperationInput<AB: SP1AirBuilder> {
116    pub b: Word<AB::Expr>,
117    pub c: Word<AB::Expr>,
118    pub offset_bit0: AB::Expr,
119    pub offset_bit1: AB::Expr,
120    pub offset_bit2: AB::Expr,
121    pub is_real: AB::Expr,
122    pub cols: AddressOperation<AB::Var>,
123}
124
125impl<AB> SP1Operation<AB> for AddressOperation<AB::F>
126where
127    AB: SP1AirBuilder + SP1OperationBuilder<AddrAddOperation<<AB as AirBuilder>::F>>,
128{
129    type Input = AddressOperationInput<AB>;
130    type Output = [AB::Expr; 3];
131
132    fn lower(builder: &mut AB, input: Self::Input) -> Self::Output {
133        Self::eval(
134            builder,
135            input.b,
136            input.c,
137            input.offset_bit0,
138            input.offset_bit1,
139            input.offset_bit2,
140            input.is_real,
141            input.cols,
142        )
143    }
144}
sp1_core_machine/operations/address.rs

sp1_core_machine/operations/
address.rs
