tasm_lib/arithmetic/u64/
add.rs

1use std::collections::HashMap;
2
3use tasm_lib::prelude::BasicSnippet;
4use triton_vm::prelude::*;
5
6use crate::arithmetic;
7use crate::prelude::*;
8use crate::traits::basic_snippet::Reviewer;
9use crate::traits::basic_snippet::SignOffFingerprint;
10
11/// Add two `u64`s.
12///
13/// ### Behavior
14///
15/// ```text
16/// BEFORE: _ [right: u64] [left: u64]
17/// AFTER:  _ [sum: u64]
18/// ```
19///
20/// ### Preconditions
21///
22/// - all input arguments are properly [`BFieldCodec`] encoded
23/// - the sum of the arguments does not exceed [`u64::MAX`]
24///
25/// ### Postconditions
26///
27/// - the `sum` is the sum of the arguments
28/// - the `sum` is properly [`BFieldCodec`] encoded
29#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
30pub struct Add;
31
32impl Add {
33    pub const OVERFLOW_ERROR_ID: i128 = 310;
34}
35
36impl BasicSnippet for Add {
37    fn parameters(&self) -> Vec<(DataType, String)> {
38        ["rhs", "lhs"]
39            .map(|side| (DataType::U64, side.to_string()))
40            .to_vec()
41    }
42
43    fn return_values(&self) -> Vec<(DataType, String)> {
44        vec![(DataType::U64, "sum".to_string())]
45    }
46
47    fn entrypoint(&self) -> String {
48        "tasmlib_arithmetic_u64_add".to_string()
49    }
50
51    fn code(&self, _: &mut Library) -> Vec<LabelledInstruction> {
52        triton_asm!({self.entrypoint()}:
53            {&arithmetic::u64::overflowing_add::OverflowingAdd::addition_code()}
54            // _ sum_hi sum_lo is_overflow
55
56            push 0
57            eq
58            assert error_id {Self::OVERFLOW_ERROR_ID}
59            // _ sum_hi sum_lo
60
61            return
62        )
63    }
64
65    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
66        let mut sign_offs = HashMap::new();
67        sign_offs.insert(Reviewer("ferdinand"), 0xe275906c3d0c35f3.into());
68        sign_offs
69    }
70}
71
72#[cfg(test)]
73mod tests {
74    use super::*;
75    use crate::arithmetic::u64::overflowing_add::OverflowingAdd;
76    use crate::test_helpers::test_rust_equivalence_given_execution_state;
77    use crate::test_prelude::*;
78
79    impl Closure for Add {
80        type Args = <OverflowingAdd as Closure>::Args;
81
82        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) -> Result<(), RustShadowError> {
83            let (left, right) = pop_encodable::<Self::Args>(stack)?;
84            let sum = left
85                .checked_add(right)
86                .ok_or(RustShadowError::ArithmeticOverflow)?;
87            push_encodable(stack, &sum);
88            Ok(())
89        }
90
91        fn pseudorandom_args(&self, seed: [u8; 32], _: Option<BenchmarkCase>) -> Self::Args {
92            let mut rng = StdRng::from_seed(seed);
93            let left = rng.random();
94            let right = rng.random_range(0..=u64::MAX - left);
95
96            (left, right)
97        }
98
99        fn corner_case_args(&self) -> Vec<Self::Args> {
100            let corner_case_points = OverflowingAdd::corner_case_points();
101
102            corner_case_points
103                .iter()
104                .cartesian_product(&corner_case_points)
105                .filter(|&(&l, &r)| l.checked_add(r).is_some())
106                .map(|(&l, &r)| (l, r))
107                .collect()
108        }
109    }
110
111    #[macro_rules_attr::apply(test)]
112    fn unit_test() {
113        ShadowedClosure::new(Add).test();
114    }
115
116    #[macro_rules_attr::apply(proptest)]
117    fn proptest(left: u64, #[strategy(0..u64::MAX - #left)] right: u64) {
118        let initial_state = InitVmState::with_stack(Add.set_up_test_stack((left, right)));
119        test_rust_equivalence_given_execution_state(&ShadowedClosure::new(Add), initial_state);
120    }
121
122    #[macro_rules_attr::apply(proptest)]
123    fn triton_vm_crashes_on_overflowing_add(left: u64, #[strategy(u64::MAX - #left..)] right: u64) {
124        prop_assume!(left.checked_add(right).is_none());
125
126        test_assertion_failure(
127            &ShadowedClosure::new(Add),
128            InitVmState::with_stack(Add.set_up_test_stack((left, right))),
129            &[Add::OVERFLOW_ERROR_ID],
130        );
131    }
132}
133
134#[cfg(test)]
135mod benches {
136    use super::*;
137    use crate::test_prelude::*;
138
139    #[macro_rules_attr::apply(test)]
140    fn benchmark() {
141        ShadowedClosure::new(Add).bench()
142    }
143}
tasm_lib/arithmetic/u64/add.rs

tasm_lib/arithmetic/u64/
add.rs
