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 inputs(&self) -> Vec<(DataType, String)> {
38        ["subtrahend", "minuend"]
39            .map(|s| (DataType::U128, s.to_string()))
40            .to_vec()
41    }
42
43    fn outputs(&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"), 0xcfbc5c77452584fd.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>) {
125            let (subtrahend, minuend) = pop_encodable::<Self::Args>(stack);
126            let difference = minuend.checked_sub(subtrahend).unwrap();
127            push_encodable(stack, &difference);
128        }
129
130        fn pseudorandom_args(
131            &self,
132            seed: [u8; 32],
133            bench_case: Option<BenchmarkCase>,
134        ) -> Self::Args {
135            let Some(bench_case) = bench_case else {
136                let mut rng = StdRng::from_seed(seed);
137                let subtrahend = rng.random();
138                let minuend = rng.random_range(subtrahend..=u128::MAX);
139                return (subtrahend, minuend);
140            };
141
142            match bench_case {
143                BenchmarkCase::CommonCase => (1 << 126, 1 << 127),
144                BenchmarkCase::WorstCase => ((1 << 126) + (1 << 56), (1 << 127) + (1 << 64)),
145            }
146        }
147
148        fn corner_case_args(&self) -> Vec<Self::Args> {
149            vec![
150                (0, 0),
151                (0, 1),
152                (1, 1),
153                (1, 0xffff_ffff_ffff_ffff_ffff_ffff_0000_0000),
154                (2, 0xffff_ffff_ffff_ffff_0000_0000_0000_0001),
155                (3, 0xffff_ffff_0000_0000_0000_0000_0000_0002),
156                (4, 1 << 127),
157                (u32::MAX.into(), u32::MAX.into()),
158                (u64::MAX.into(), u64::MAX.into()),
159                (u128::MAX, u128::MAX),
160            ]
161        }
162    }
163
164    #[test]
165    fn rust_shadow() {
166        ShadowedClosure::new(Sub).test();
167    }
168
169    #[proptest]
170    fn overflow_crashes_vm(
171        #[strategy(1_u128..)] subtrahend: u128,
172        #[strategy(..#subtrahend)] minuend: u128,
173    ) {
174        test_assertion_failure(
175            &ShadowedClosure::new(Sub),
176            InitVmState::with_stack(Sub.set_up_test_stack((subtrahend, minuend))),
177            &[Sub::OVERFLOW_ERROR_ID],
178        );
179    }
180}
181
182#[cfg(test)]
183mod benches {
184    use super::*;
185    use crate::test_prelude::*;
186
187    #[test]
188    fn benchmark() {
189        ShadowedClosure::new(Sub).bench();
190    }
191}
tasm_lib/arithmetic/u128/sub.rs

tasm_lib/arithmetic/u128/
sub.rs
