tasm_lib/arithmetic/u64/
overflowing_add.rs

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

tasm_lib/arithmetic/u64/
overflowing_add.rs
