sp1_core_machine/operations/
add.rs

1use sp1_core_executor::events::ByteRecord;
2use sp1_stark::{air::SP1AirBuilder, Word};
3
4use p3_air::AirBuilder;
5use p3_field::{AbstractField, Field};
6use sp1_derive::AlignedBorrow;
7
8use crate::air::WordAirBuilder;
9
10/// A set of columns needed to compute the add of two words.
11#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
12#[repr(C)]
13pub struct AddOperation<T> {
14    /// The result of `a + b`.
15    pub value: Word<T>,
16
17    /// Trace.
18    pub carry: [T; 3],
19}
20
21impl<F: Field> AddOperation<F> {
22    pub fn populate(&mut self, record: &mut impl ByteRecord, a_u32: u32, b_u32: u32) -> u32 {
23        let expected = a_u32.wrapping_add(b_u32);
24        self.value = Word::from(expected);
25        let a = a_u32.to_le_bytes();
26        let b = b_u32.to_le_bytes();
27
28        let mut carry = [0u8, 0u8, 0u8];
29        if (a[0] as u32) + (b[0] as u32) > 255 {
30            carry[0] = 1;
31            self.carry[0] = F::one();
32        }
33        if (a[1] as u32) + (b[1] as u32) + (carry[0] as u32) > 255 {
34            carry[1] = 1;
35            self.carry[1] = F::one();
36        }
37        if (a[2] as u32) + (b[2] as u32) + (carry[1] as u32) > 255 {
38            carry[2] = 1;
39            self.carry[2] = F::one();
40        }
41
42        let base = 256u32;
43        let overflow = a[0].wrapping_add(b[0]).wrapping_sub(expected.to_le_bytes()[0]) as u32;
44        debug_assert_eq!(overflow.wrapping_mul(overflow.wrapping_sub(base)), 0);
45
46        // Range check
47        {
48            record.add_u8_range_checks(&a);
49            record.add_u8_range_checks(&b);
50            record.add_u8_range_checks(&expected.to_le_bytes());
51        }
52        expected
53    }
54
55    pub fn eval<AB: SP1AirBuilder>(
56        builder: &mut AB,
57        a: Word<AB::Var>,
58        b: Word<AB::Var>,
59        cols: AddOperation<AB::Var>,
60        is_real: AB::Expr,
61    ) {
62        let one = AB::Expr::one();
63        let base = AB::F::from_canonical_u32(256);
64
65        let mut builder_is_real = builder.when(is_real.clone());
66
67        // For each limb, assert that difference between the carried result and the non-carried
68        // result is either zero or the base.
69        let overflow_0 = a[0] + b[0] - cols.value[0];
70        let overflow_1 = a[1] + b[1] - cols.value[1] + cols.carry[0];
71        let overflow_2 = a[2] + b[2] - cols.value[2] + cols.carry[1];
72        let overflow_3 = a[3] + b[3] - cols.value[3] + cols.carry[2];
73        builder_is_real.assert_zero(overflow_0.clone() * (overflow_0.clone() - base));
74        builder_is_real.assert_zero(overflow_1.clone() * (overflow_1.clone() - base));
75        builder_is_real.assert_zero(overflow_2.clone() * (overflow_2.clone() - base));
76        builder_is_real.assert_zero(overflow_3.clone() * (overflow_3.clone() - base));
77
78        // If the carry is one, then the overflow must be the base.
79        builder_is_real.assert_zero(cols.carry[0] * (overflow_0.clone() - base));
80        builder_is_real.assert_zero(cols.carry[1] * (overflow_1.clone() - base));
81        builder_is_real.assert_zero(cols.carry[2] * (overflow_2.clone() - base));
82
83        // If the carry is not one, then the overflow must be zero.
84        builder_is_real.assert_zero((cols.carry[0] - one.clone()) * overflow_0.clone());
85        builder_is_real.assert_zero((cols.carry[1] - one.clone()) * overflow_1.clone());
86        builder_is_real.assert_zero((cols.carry[2] - one.clone()) * overflow_2.clone());
87
88        // Assert that the carry is either zero or one.
89        builder_is_real.assert_bool(cols.carry[0]);
90        builder_is_real.assert_bool(cols.carry[1]);
91        builder_is_real.assert_bool(cols.carry[2]);
92        builder_is_real.assert_bool(is_real.clone());
93
94        // Range check each byte.
95        {
96            builder.slice_range_check_u8(&a.0, is_real.clone());
97            builder.slice_range_check_u8(&b.0, is_real.clone());
98            builder.slice_range_check_u8(&cols.value.0, is_real);
99        }
100    }
101}
sp1_core_machine/operations/add.rs

sp1_core_machine/operations/
add.rs
