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 inputs(&self) -> Vec<(DataType, String)> {
39        OverflowingSub.inputs()
40    }
41
42    fn outputs(&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"), 0x7d887e69af21cab6.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);
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>) {
103            let (subtrahend, minuend) = pop_encodable::<Self::Args>(stack);
104            push_encodable(stack, &(minuend - subtrahend));
105        }
106
107        fn pseudorandom_args(
108            &self,
109            seed: [u8; 32],
110            bench_case: Option<BenchmarkCase>,
111        ) -> Self::Args {
112            let Some(bench_case) = bench_case else {
113                let mut rng = StdRng::from_seed(seed);
114                let subtrahend = rng.random();
115                let minuend = rng.random_range(subtrahend..=u64::MAX);
116                return (subtrahend, minuend);
117            };
118
119            match bench_case {
120                BenchmarkCase::CommonCase => (0x3ff, 0x7fff_ffff),
121                BenchmarkCase::WorstCase => (0x1_7fff_ffff, 0x64_0000_03ff),
122            }
123        }
124
125        fn corner_case_args(&self) -> Vec<Self::Args> {
126            let edge_case_values = OverflowingSub::edge_case_values();
127
128            edge_case_values
129                .iter()
130                .cartesian_product(&edge_case_values)
131                .filter(|&(&subtrahend, &minuend)| minuend.checked_sub(subtrahend).is_some())
132                .map(|(&subtrahend, &minuend)| (subtrahend, minuend))
133                .collect()
134        }
135    }
136
137    #[test]
138    fn rust_shadow() {
139        ShadowedClosure::new(Sub).test();
140    }
141
142    #[test]
143    fn unit_test() {
144        Sub.assert_expected_behavior(129, 256);
145        Sub.assert_expected_behavior(1, 1 << 32);
146    }
147
148    #[proptest]
149    fn property_test(subtrahend: u64, #[strategy(#subtrahend..)] minuend: u64) {
150        Sub.assert_expected_behavior(subtrahend, minuend);
151    }
152
153    #[proptest]
154    fn negative_property_test(
155        #[strategy(1_u64..)] subtrahend: u64,
156        #[strategy(..#subtrahend)] minuend: u64,
157    ) {
158        test_assertion_failure(
159            &ShadowedClosure::new(Sub),
160            InitVmState::with_stack(Sub.set_up_test_stack((subtrahend, minuend))),
161            &[Sub::OVERFLOW_ERROR_ID],
162        );
163    }
164}
165
166#[cfg(test)]
167mod benches {
168    use super::*;
169    use crate::test_prelude::*;
170
171    #[test]
172    fn benchmark() {
173        ShadowedClosure::new(Sub).bench();
174    }
175}
tasm_lib/arithmetic/u64/sub.rs

tasm_lib/arithmetic/u64/
sub.rs
