sp1_core_machine/operations/
and_u32.rs

1use crate::operations::U32toU8Operation;
2use slop_algebra::{AbstractField, Field};
3use sp1_core_executor::{
4    events::{ByteLookupEvent, ByteRecord},
5    ByteOpcode,
6};
7use sp1_derive::AlignedBorrow;
8use sp1_hypercube::air::SP1AirBuilder;
9
10/// A set of columns needed to compute the AND operation over two u16 limbs.
11#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
12#[repr(C)]
13pub struct AndU32Operation<T> {
14    /// Lower byte of two limbs of `b`.
15    pub b_low_bytes: U32toU8Operation<T>,
16
17    /// Lower byte of two limbs of `c`.
18    pub c_low_bytes: U32toU8Operation<T>,
19
20    /// The result of the AND operation.
21    pub value: [T; 4],
22}
23
24impl<F: Field> AndU32Operation<F> {
25    pub fn populate_and_u32(
26        &mut self,
27        record: &mut impl ByteRecord,
28        b_u32: u32,
29        c_u32: u32,
30    ) -> u32 {
31        let expected = b_u32 & c_u32;
32        self.b_low_bytes.populate_u32_to_u8_unsafe(b_u32);
33        self.c_low_bytes.populate_u32_to_u8_unsafe(c_u32);
34
35        let b_bytes = b_u32.to_le_bytes();
36        let c_bytes = c_u32.to_le_bytes();
37        for i in 0..4 {
38            let and = b_bytes[i] & c_bytes[i];
39            self.value[i] = F::from_canonical_u8(and);
40
41            let byte_event = ByteLookupEvent {
42                opcode: ByteOpcode::AND,
43                a: and as u16,
44                b: b_bytes[i],
45                c: c_bytes[i],
46            };
47            record.add_byte_lookup_event(byte_event);
48        }
49        expected
50    }
51
52    /// Evaluate the AND operation over two u32s of two u16 limbs.
53    /// Assumes that the two words are valid u32s of two u16 limbs.
54    /// Constrains that `is_real` is boolean.
55    /// If `is_real` is true, the return value is constrained to be correct.
56    pub fn eval_and_u32<AB: SP1AirBuilder>(
57        builder: &mut AB,
58        b: [AB::Expr; 2],
59        c: [AB::Expr; 2],
60        cols: AndU32Operation<AB::Var>,
61        is_real: AB::Var,
62    ) -> [AB::Expr; 2] {
63        // Constrain that `is_real` is boolean.
64        builder.assert_bool(is_real);
65
66        // Convert the two words to bytes using the unsafe API.
67        // SAFETY: This is safe because the byte lookup will range check the bytes.
68        let b_bytes =
69            U32toU8Operation::<AB::F>::eval_u32_to_u8_unsafe(builder, b, cols.b_low_bytes);
70        let c_bytes =
71            U32toU8Operation::<AB::F>::eval_u32_to_u8_unsafe(builder, c, cols.c_low_bytes);
72
73        // Constrain the `AND` operation over bytes via a byte lookup.
74        for i in 0..4 {
75            builder.send_byte(
76                AB::F::from_canonical_u32(ByteOpcode::AND as u32),
77                cols.value[i],
78                b_bytes[i].clone(),
79                c_bytes[i].clone(),
80                is_real,
81            );
82        }
83
84        // Combine the byte results into two u16 limbs.
85        let result_limb0 = cols.value[0] + cols.value[1] * AB::F::from_canonical_u32(1 << 8);
86        let result_limb1 = cols.value[2] + cols.value[3] * AB::F::from_canonical_u32(1 << 8);
87
88        [result_limb0, result_limb1]
89    }
90}
sp1_core_machine/operations/and_u32.rs

sp1_core_machine/operations/
and_u32.rs
