tasm_lib/arithmetic/u64/
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/// Add two `u64`s, indicating whether overflow occurred.
10///
11/// ### Behavior
12///
13/// ```text
14/// BEFORE: _ [right: u64] [left: u64]
15/// AFTER:  _ [sum: u64] [is_overflow: bool]
16/// ```
17///
18/// ### Preconditions
19///
20/// - all input arguments are properly [`BFieldCodec`] encoded
21///
22/// ### Postconditions
23///
24/// - the `sum` is the sum of the input modulo [`u64::MAX`]
25/// - `is_overflow` is `true` if and only if the sum of the input exceeds
26///   [`u64::MAX`]
27/// - the `sum` is properly [`BFieldCodec`] encoded
28/// - `is_overflow` is properly [`BFieldCodec`] encoded
29#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
30pub struct OverflowingAdd;
31
32impl OverflowingAdd {
33    /// (See [`OverflowingAdd`])
34    pub(crate) fn addition_code() -> Vec<LabelledInstruction> {
35        triton_asm! {
36            pick 2
37            // _ rhs_hi lhs_hi lhs_lo rhs_lo
38
39            add
40            split
41            // _ rhs_hi lhs_hi carry sum_lo
42
43            place 3
44            // _ sum_lo rhs_hi lhs_hi carry
45
46            add
47            add
48            // _ sum_lo (lhs_hi+rhs_hi+carry)
49
50            split
51            // _ sum_lo overflow sum_hi
52
53            place 2
54        }
55    }
56}
57
58impl BasicSnippet for OverflowingAdd {
59    fn parameters(&self) -> Vec<(DataType, String)> {
60        ["lhs", "rhs"]
61            .map(|s| (DataType::U64, s.to_string()))
62            .to_vec()
63    }
64
65    fn return_values(&self) -> Vec<(DataType, String)> {
66        vec![
67            (DataType::U64, "wrapped_sum".to_string()),
68            (DataType::Bool, "overflow".to_string()),
69        ]
70    }
71
72    fn entrypoint(&self) -> String {
73        "tasmlib_arithmetic_u64_overflowing_add".to_string()
74    }
75
76    fn code(&self, _: &mut Library) -> Vec<LabelledInstruction> {
77        triton_asm! {
78            {self.entrypoint()}:
79                {&Self::addition_code()}
80                return
81        }
82    }
83
84    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
85        let mut sign_offs = HashMap::new();
86        sign_offs.insert(Reviewer("ferdinand"), 0x77f1dc470c2bb719.into());
87        sign_offs
88    }
89}
90
91#[cfg(test)]
92pub mod tests {
93    use super::*;
94    use crate::test_prelude::*;
95
96    impl OverflowingAdd {
97        pub fn corner_case_points() -> Vec<u64> {
98            [0, 1 << 32, u64::MAX]
99                .into_iter()
100                .flat_map(|p| [p.checked_sub(1), Some(p), p.checked_add(1)])
101                .flatten()
102                .collect()
103        }
104    }
105
106    impl Closure for OverflowingAdd {
107        type Args = (u64, u64);
108
109        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) -> Result<(), RustShadowError> {
110            let right = pop_encodable::<u64>(stack)?;
111            let left = pop_encodable::<u64>(stack)?;
112            let (sum, is_overflow) = left.overflowing_add(right);
113            push_encodable(stack, &sum);
114            push_encodable(stack, &is_overflow);
115            Ok(())
116        }
117
118        fn pseudorandom_args(
119            &self,
120            seed: [u8; 32],
121            bench_case: Option<BenchmarkCase>,
122        ) -> Self::Args {
123            match bench_case {
124                Some(BenchmarkCase::CommonCase) => (1 << 63, (1 << 63) - 1),
125                Some(BenchmarkCase::WorstCase) => (1 << 63, 1 << 50),
126                None => StdRng::from_seed(seed).random(),
127            }
128        }
129
130        fn corner_case_args(&self) -> Vec<Self::Args> {
131            let corner_case_points = Self::corner_case_points();
132
133            corner_case_points
134                .iter()
135                .cartesian_product(&corner_case_points)
136                .map(|(&l, &r)| (l, r))
137                .collect()
138        }
139    }
140
141    #[macro_rules_attr::apply(test)]
142    fn u64_overflowing_add_pbt() {
143        ShadowedClosure::new(OverflowingAdd).test()
144    }
145}
146
147#[cfg(test)]
148mod benches {
149    use super::*;
150    use crate::test_prelude::*;
151
152    #[macro_rules_attr::apply(test)]
153    fn benchmark() {
154        ShadowedClosure::new(OverflowingAdd).bench()
155    }
156}
tasm_lib/arithmetic/u64/overflowing_add.rs

tasm_lib/arithmetic/u64/
overflowing_add.rs
