tasm_lib/arithmetic/u64/
add.rs

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

tasm_lib/arithmetic/u64/
add.rs
