tasm_lib/arithmetic/u64/
sub.rs

1use std::collections::HashMap;
2
3use triton_vm::prelude::*;
4
5use crate::arithmetic::u64::overflowing_sub::OverflowingSub;
6use crate::prelude::*;
7use crate::traits::basic_snippet::Reviewer;
8use crate::traits::basic_snippet::SignOffFingerprint;
9
10/// [Subtraction][sub] for unsigned 64-bit integers.
11///
12/// # Behavior
13///
14/// ```text
15/// BEFORE: _ [subtrahend: u64] [minuend: u64]
16/// AFTER:  _ [difference: u64]
17/// ```
18///
19/// # Preconditions
20///
21/// - the `minuend` is greater than or equal to the `subtrahend`
22/// - all input arguments are properly [`BFieldCodec`] encoded
23///
24/// # Postconditions
25///
26/// - the output is the `minuend` minus the `subtrahend`
27/// - the output is properly [`BFieldCodec`] encoded
28///
29/// [sub]: core::ops::Sub
30#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
31pub struct Sub;
32
33impl Sub {
34    pub const OVERFLOW_ERROR_ID: i128 = 340;
35}
36
37impl BasicSnippet for Sub {
38    fn parameters(&self) -> Vec<(DataType, String)> {
39        OverflowingSub.parameters()
40    }
41
42    fn return_values(&self) -> Vec<(DataType, String)> {
43        vec![(DataType::U64, "difference".to_string())]
44    }
45
46    fn entrypoint(&self) -> String {
47        "tasmlib_arithmetic_u64_sub".to_string()
48    }
49
50    fn code(&self, _: &mut Library) -> Vec<LabelledInstruction> {
51        triton_asm!(
52            // BEFORE: _ subtrahend_hi subtrahend_lo minuend_hi minuend_lo
53            // AFTER:  _ difference_hi difference_lo
54            {self.entrypoint()}:
55                {&OverflowingSub::common_subtraction_code()}
56                // _ difference_lo (minuend_hi - subtrahend_hi - carry)
57
58                split
59                place 2
60                // _ difference_hi difference_lo only_0_if_no_overflow
61
62                push 0
63                eq
64                assert error_id {Self::OVERFLOW_ERROR_ID}
65                // _ difference_hi difference_lo
66
67                return
68        )
69    }
70
71    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
72        let mut sign_offs = HashMap::new();
73        sign_offs.insert(Reviewer("ferdinand"), 0x8dad59997cb49bd9.into());
74        sign_offs
75    }
76}
77
78#[cfg(test)]
79mod tests {
80    use super::*;
81    use crate::test_prelude::*;
82
83    impl Sub {
84        pub fn assert_expected_behavior(&self, subtrahend: u64, minuend: u64) {
85            let mut expected_stack = self.set_up_test_stack((subtrahend, minuend));
86            self.rust_shadow(&mut expected_stack).unwrap();
87
88            test_rust_equivalence_given_complete_state(
89                &ShadowedClosure::new(Self),
90                &self.set_up_test_stack((subtrahend, minuend)),
91                &[],
92                &NonDeterminism::default(),
93                &None,
94                Some(&expected_stack),
95            );
96        }
97    }
98
99    impl Closure for Sub {
100        type Args = <OverflowingSub as Closure>::Args;
101
102        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) -> Result<(), RustShadowError> {
103            let (subtrahend, minuend) = pop_encodable::<Self::Args>(stack)?;
104            let difference = minuend
105                .checked_sub(subtrahend)
106                .ok_or(RustShadowError::ArithmeticOverflow)?;
107            push_encodable(stack, &difference);
108            Ok(())
109        }
110
111        fn pseudorandom_args(
112            &self,
113            seed: [u8; 32],
114            bench_case: Option<BenchmarkCase>,
115        ) -> Self::Args {
116            let Some(bench_case) = bench_case else {
117                let mut rng = StdRng::from_seed(seed);
118                let subtrahend = rng.random();
119                let minuend = rng.random_range(subtrahend..=u64::MAX);
120                return (subtrahend, minuend);
121            };
122
123            match bench_case {
124                BenchmarkCase::CommonCase => (0x3ff, 0x7fff_ffff),
125                BenchmarkCase::WorstCase => (0x1_7fff_ffff, 0x64_0000_03ff),
126            }
127        }
128
129        fn corner_case_args(&self) -> Vec<Self::Args> {
130            let edge_case_values = OverflowingSub::edge_case_values();
131
132            edge_case_values
133                .iter()
134                .cartesian_product(&edge_case_values)
135                .filter(|&(&subtrahend, &minuend)| minuend.checked_sub(subtrahend).is_some())
136                .map(|(&subtrahend, &minuend)| (subtrahend, minuend))
137                .collect()
138        }
139    }
140
141    #[macro_rules_attr::apply(test)]
142    fn rust_shadow() {
143        ShadowedClosure::new(Sub).test();
144    }
145
146    #[macro_rules_attr::apply(test)]
147    fn unit_test() {
148        Sub.assert_expected_behavior(129, 256);
149        Sub.assert_expected_behavior(1, 1 << 32);
150    }
151
152    #[macro_rules_attr::apply(proptest)]
153    fn property_test(subtrahend: u64, #[strategy(#subtrahend..)] minuend: u64) {
154        Sub.assert_expected_behavior(subtrahend, minuend);
155    }
156
157    #[macro_rules_attr::apply(proptest)]
158    fn negative_property_test(
159        #[strategy(1_u64..)] subtrahend: u64,
160        #[strategy(..#subtrahend)] minuend: u64,
161    ) {
162        test_assertion_failure(
163            &ShadowedClosure::new(Sub),
164            InitVmState::with_stack(Sub.set_up_test_stack((subtrahend, minuend))),
165            &[Sub::OVERFLOW_ERROR_ID],
166        );
167    }
168}
169
170#[cfg(test)]
171mod benches {
172    use super::*;
173    use crate::test_prelude::*;
174
175    #[macro_rules_attr::apply(test)]
176    fn benchmark() {
177        ShadowedClosure::new(Sub).bench();
178    }
179}
tasm_lib/arithmetic/u64/sub.rs

tasm_lib/arithmetic/u64/
sub.rs
