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>) {
83            let (left, right) = pop_encodable::<Self::Args>(stack);
84            let sum = left.checked_add(right).expect("overflow occurred");
85            push_encodable(stack, &sum);
86        }
87
88        fn pseudorandom_args(&self, seed: [u8; 32], _: Option<BenchmarkCase>) -> Self::Args {
89            let mut rng = StdRng::from_seed(seed);
90            let left = rng.random();
91            let right = rng.random_range(0..=u64::MAX - left);
92
93            (left, right)
94        }
95
96        fn corner_case_args(&self) -> Vec<Self::Args> {
97            let corner_case_points = OverflowingAdd::corner_case_points();
98
99            corner_case_points
100                .iter()
101                .cartesian_product(&corner_case_points)
102                .filter(|&(&l, &r)| l.checked_add(r).is_some())
103                .map(|(&l, &r)| (l, r))
104                .collect()
105        }
106    }
107
108    #[test]
109    fn unit_test() {
110        ShadowedClosure::new(Add).test();
111    }
112
113    #[proptest]
114    fn proptest(left: u64, #[strategy(0..u64::MAX - #left)] right: u64) {
115        let initial_state = InitVmState::with_stack(Add.set_up_test_stack((left, right)));
116        test_rust_equivalence_given_execution_state(&ShadowedClosure::new(Add), initial_state);
117    }
118
119    #[proptest]
120    fn triton_vm_crashes_on_overflowing_add(left: u64, #[strategy(u64::MAX - #left..)] right: u64) {
121        prop_assume!(left.checked_add(right).is_none());
122
123        test_assertion_failure(
124            &ShadowedClosure::new(Add),
125            InitVmState::with_stack(Add.set_up_test_stack((left, right))),
126            &[Add::OVERFLOW_ERROR_ID],
127        );
128    }
129}
130
131#[cfg(test)]
132mod benches {
133    use super::*;
134    use crate::test_prelude::*;
135
136    #[test]
137    fn benchmark() {
138        ShadowedClosure::new(Add).bench()
139    }
140}
tasm_lib/arithmetic/u64/add.rs

tasm_lib/arithmetic/u64/
add.rs
