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>) {
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        }
116
117        fn pseudorandom_args(
118            &self,
119            seed: [u8; 32],
120            bench_case: Option<BenchmarkCase>,
121        ) -> Self::Args {
122            match bench_case {
123                Some(BenchmarkCase::CommonCase) => (1 << 63, (1 << 63) - 1),
124                Some(BenchmarkCase::WorstCase) => (1 << 63, 1 << 50),
125                None => StdRng::from_seed(seed).random(),
126            }
127        }
128
129        fn corner_case_args(&self) -> Vec<Self::Args> {
130            let corner_case_points = Self::corner_case_points();
131
132            corner_case_points
133                .iter()
134                .cartesian_product(&corner_case_points)
135                .map(|(&l, &r)| (l, r))
136                .collect()
137        }
138    }
139
140    #[test]
141    fn u64_overflowing_add_pbt() {
142        ShadowedClosure::new(OverflowingAdd).test()
143    }
144}
145
146#[cfg(test)]
147mod benches {
148    use super::*;
149    use crate::test_prelude::*;
150
151    #[test]
152    fn benchmark() {
153        ShadowedClosure::new(OverflowingAdd).bench()
154    }
155}
tasm_lib/arithmetic/u64/overflowing_add.rs

tasm_lib/arithmetic/u64/
overflowing_add.rs
