Skip to main content

tasm_lib/arithmetic/u128/
sub.rs

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