tasm_lib/arithmetic/u128/
overflowing_add.rs

1use std::collections::HashMap;
2
3use triton_vm::prelude::*;
4
5use crate::prelude::*;
6use crate::traits::basic_snippet::Reviewer;
7use crate::traits::basic_snippet::SignOffFingerprint;
8
9/// Mimics [`u128::overflowing_add`].
10///
11/// ### Behavior
12///
13/// ```text
14/// BEFORE: _ [rhs: u128] [lhs: u128]
15/// AFTER:  _ [sum: u128] [is_overflow: bool]
16/// ```
17///
18/// ### Preconditions
19///
20/// - all input arguments are properly [`BFieldCodec`] encoded
21///
22/// ### Postconditions
23///
24/// - the output is properly [`BFieldCodec`] encoded
25#[derive(Debug, Default, Copy, Clone, Eq, PartialEq, Hash)]
26pub struct OverflowingAdd;
27
28impl OverflowingAdd {
29    /// Generate code to perform an addition on `u128`s.
30    ///
31    /// This function is called by both this snippet and
32    /// [`SafeAdd`](super::safe_add::SafeAdd).
33    ///
34    /// ```text
35    /// BEFORE: _ rhs_3 rhs_2 rhs_1 rhs_0 lhs_3 lhs_2 lhs_1 lhs_0
36    /// AFTER:  _ sum_3 sum_2 sum_1 sum_0 is_overflow
37    /// ```
38    /// Don't forget to adapt the signature when using this function elsewhere.
39    pub(crate) fn addition_code() -> Vec<LabelledInstruction> {
40        triton_asm!(
41            pick 4  // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 lhs_0 rhs_0
42            add
43            split   // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 (lhs_0 + rhs_0)_hi (lhs_0 + rhs_0)_lo
44                    // _ rhs_3 rhs_2 rhs_1 lhs_3 lhs_2 lhs_1 carry_1            sum_0
45            swap 5  // _ rhs_3 rhs_2 sum_0 lhs_3 lhs_2 lhs_1 carry_1 rhs_1
46            add
47            add
48            split   // _ rhs_3 rhs_2 sum_0 lhs_3 lhs_2 carry_2 sum_1
49            swap 5  // _ rhs_3 sum_1 sum_0 lhs_3 lhs_2 carry_2 rhs_2
50            add
51            add
52            split   // _ rhs_3 sum_1 sum_0 lhs_3 carry_3 sum_2
53            swap 5  // _ sum_2 sum_1 sum_0 lhs_3 carry_3 rhs_3
54            add
55            add
56            split   // _ sum_2 sum_1 sum_0 carry_4 sum_3
57            place 4 // _ sum_3 sum_2 sum_1 sum_0 carry_4
58                    // _ sum_3 sum_2 sum_1 sum_0 is_overflow
59        )
60    }
61}
62
63impl BasicSnippet for OverflowingAdd {
64    fn inputs(&self) -> Vec<(DataType, String)> {
65        ["lhs", "rhs"]
66            .map(|s| (DataType::U128, s.to_owned()))
67            .to_vec()
68    }
69
70    fn outputs(&self) -> Vec<(DataType, String)> {
71        vec![
72            (DataType::U128, "sum".to_owned()),
73            (DataType::Bool, "overflow".to_owned()),
74        ]
75    }
76
77    fn entrypoint(&self) -> String {
78        "tasmlib_arithmetic_u128_overflowing_add".to_string()
79    }
80
81    fn code(&self, _: &mut Library) -> Vec<LabelledInstruction> {
82        triton_asm! { {self.entrypoint()}: {&Self::addition_code()} return }
83    }
84
85    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
86        let mut sign_offs = HashMap::new();
87        sign_offs.insert(Reviewer("ferdinand"), 0x191e15314c8a5c8e.into());
88        sign_offs
89    }
90}
91
92#[cfg(test)]
93pub(crate) mod tests {
94    use rand::rngs::StdRng;
95
96    use super::*;
97    use crate::test_prelude::*;
98
99    impl OverflowingAdd {
100        fn assert_expected_add_behavior(&self, lhs: u128, rhs: u128) {
101            let initial_stack = self.set_up_test_stack((rhs, lhs));
102
103            let mut expected_stack = initial_stack.clone();
104            self.rust_shadow(&mut expected_stack);
105
106            test_rust_equivalence_given_complete_state(
107                &ShadowedClosure::new(Self),
108                &initial_stack,
109                &[],
110                &NonDeterminism::default(),
111                &None,
112                Some(&expected_stack),
113            );
114        }
115
116        pub fn edge_case_points() -> Vec<u128> {
117            [0, 0x200000002fffffffffff908f8, 1 << 127, u128::MAX]
118                .into_iter()
119                .flat_map(|p| [p.checked_sub(1), Some(p), p.checked_add(1)])
120                .flatten()
121                .collect()
122        }
123    }
124
125    impl Closure for OverflowingAdd {
126        type Args = (u128, u128);
127
128        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) {
129            let (left, right) = pop_encodable::<Self::Args>(stack);
130            let (sum, is_overflow) = left.overflowing_add(right);
131            push_encodable(stack, &sum);
132            push_encodable(stack, &is_overflow);
133        }
134
135        fn pseudorandom_args(&self, seed: [u8; 32], _: Option<BenchmarkCase>) -> Self::Args {
136            StdRng::from_seed(seed).random()
137        }
138
139        fn corner_case_args(&self) -> Vec<Self::Args> {
140            let edge_case_points = Self::edge_case_points();
141
142            edge_case_points
143                .iter()
144                .cartesian_product(&edge_case_points)
145                .map(|(&l, &r)| (l, r))
146                .collect()
147        }
148    }
149
150    #[test]
151    fn rust_shadow() {
152        ShadowedClosure::new(OverflowingAdd).test();
153    }
154
155    #[test]
156    fn unit_test() {
157        let snippet = OverflowingAdd;
158        snippet.assert_expected_add_behavior(1u128 << 67, 1u128 << 67)
159    }
160
161    #[test]
162    fn overflow_test() {
163        let test_overflowing_add = |a, b| {
164            OverflowingAdd.assert_expected_add_behavior(a, b);
165            OverflowingAdd.assert_expected_add_behavior(b, a);
166        };
167
168        test_overflowing_add(1, u128::MAX);
169        test_overflowing_add(2, u128::MAX - 1);
170        test_overflowing_add(1 << 127, 1 << 127);
171        test_overflowing_add(u128::MAX, u128::MAX);
172
173        for a in [31, 32, 33, 63, 64, 65, 95, 96, 97].map(|p| 1 << p) {
174            test_overflowing_add(u128::MAX, a);
175        }
176
177        for i in 0..128 {
178            let a = 1 << i;
179            let b = u128::MAX - a + 1;
180            debug_assert_eq!((0, true), a.overflowing_add(b), "i = {i}; a = {a}, b = {b}");
181
182            test_overflowing_add(a, b);
183        }
184    }
185}
186
187#[cfg(test)]
188mod benches {
189    use super::*;
190    use crate::test_prelude::*;
191
192    #[test]
193    fn benchmark() {
194        ShadowedClosure::new(OverflowingAdd).bench();
195    }
196}