snarkvm_circuit_types_integers/
sub_checked.rs

1// Copyright (c) 2019-2025 Provable Inc.
2// This file is part of the snarkVM library.
3
4// Licensed under the Apache License, Version 2.0 (the "License");
5// you may not use this file except in compliance with the License.
6// You may obtain a copy of the License at:
7
8// http://www.apache.org/licenses/LICENSE-2.0
9
10// Unless required by applicable law or agreed to in writing, software
11// distributed under the License is distributed on an "AS IS" BASIS,
12// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13// See the License for the specific language governing permissions and
14// limitations under the License.
15
16use super::*;
17
18impl<E: Environment, I: IntegerType> Sub<Integer<E, I>> for Integer<E, I> {
19    type Output = Self;
20
21    fn sub(self, other: Self) -> Self::Output {
22        self - &other
23    }
24}
25
26impl<E: Environment, I: IntegerType> Sub<Integer<E, I>> for &Integer<E, I> {
27    type Output = Integer<E, I>;
28
29    fn sub(self, other: Integer<E, I>) -> Self::Output {
30        self - &other
31    }
32}
33
34impl<E: Environment, I: IntegerType> Sub<&Integer<E, I>> for Integer<E, I> {
35    type Output = Self;
36
37    fn sub(self, other: &Self) -> Self::Output {
38        &self - other
39    }
40}
41
42impl<E: Environment, I: IntegerType> Sub<&Integer<E, I>> for &Integer<E, I> {
43    type Output = Integer<E, I>;
44
45    fn sub(self, other: &Integer<E, I>) -> Self::Output {
46        let mut output = self.clone();
47        output -= other;
48        output
49    }
50}
51
52impl<E: Environment, I: IntegerType> SubAssign<Integer<E, I>> for Integer<E, I> {
53    fn sub_assign(&mut self, other: Integer<E, I>) {
54        *self -= &other;
55    }
56}
57
58impl<E: Environment, I: IntegerType> SubAssign<&Integer<E, I>> for Integer<E, I> {
59    fn sub_assign(&mut self, other: &Integer<E, I>) {
60        // Stores the difference of `self` and `other` in `self`.
61        *self = self.sub_checked(other);
62    }
63}
64
65impl<E: Environment, I: IntegerType> SubChecked<Self> for Integer<E, I> {
66    type Output = Self;
67
68    #[inline]
69    fn sub_checked(&self, other: &Integer<E, I>) -> Self::Output {
70        // Determine the variable mode.
71        if self.is_constant() && other.is_constant() {
72            // Compute the difference and return the new constant.
73            match self.eject_value().checked_sub(&other.eject_value()) {
74                Some(value) => Integer::constant(console::Integer::new(value)),
75                None => E::halt("Integer underflow on subtraction of two constants"),
76            }
77        } else {
78            // Instead of subtracting the bits of `self` and `other` directly, the integers are
79            // converted into a field elements, and subtracted, before converting back to integers.
80            // Note: This is safe as the field is larger than the maximum integer type supported.
81            let difference = self.to_field() + (!other).to_field() + Field::one();
82
83            // Extract the integer bits from the field element, with a carry bit.
84            let (difference, carry) = match difference.to_lower_bits_le(I::BITS as usize + 1).split_last() {
85                Some((carry, bits_le)) => (Integer::from_bits_le(bits_le), carry.clone()),
86                // Note: `E::halt` should never be invoked as `I::BITS as usize + 1` is greater than zero.
87                None => E::halt("Malformed difference detected during integer subtraction"),
88            };
89
90            // Check for underflow.
91            match I::is_signed() {
92                // For signed subtraction, overflow and underflow conditions are:
93                //   - a > 0 && b < 0 && a - b > 0 (Overflow)
94                //   - a < 0 && b > 0 && a - b < 0 (Underflow)
95                //   - Note: if sign(a) == sign(b) then over/underflow is impossible.
96                //   - Note: the result of an overflow and underflow must be negative and positive, respectively.
97                true => {
98                    let is_different_signs = self.msb().is_not_equal(other.msb());
99                    let is_underflow = is_different_signs & difference.msb().is_equal(other.msb());
100                    E::assert_eq(is_underflow, E::zero());
101                }
102                // For unsigned subtraction, ensure the carry bit is one.
103                false => E::assert_eq(carry, E::one()),
104            }
105
106            // Return the difference of `self` and `other`.
107            difference
108        }
109    }
110}
111
112impl<E: Environment, I: IntegerType> Metrics<dyn Sub<Integer<E, I>, Output = Integer<E, I>>> for Integer<E, I> {
113    type Case = (Mode, Mode);
114
115    fn count(case: &Self::Case) -> Count {
116        <Self as Metrics<dyn SubChecked<Integer<E, I>, Output = Integer<E, I>>>>::count(case)
117    }
118}
119
120impl<E: Environment, I: IntegerType> OutputMode<dyn Sub<Integer<E, I>, Output = Integer<E, I>>> for Integer<E, I> {
121    type Case = (Mode, Mode);
122
123    fn output_mode(case: &Self::Case) -> Mode {
124        <Self as OutputMode<dyn SubChecked<Integer<E, I>, Output = Integer<E, I>>>>::output_mode(case)
125    }
126}
127
128impl<E: Environment, I: IntegerType> Metrics<dyn SubChecked<Integer<E, I>, Output = Integer<E, I>>> for Integer<E, I> {
129    type Case = (Mode, Mode);
130
131    fn count(case: &Self::Case) -> Count {
132        match I::is_signed() {
133            true => match (case.0, case.1) {
134                (Mode::Constant, Mode::Constant) => Count::is(I::BITS, 0, 0, 0),
135                (Mode::Constant, _) => Count::is(0, 0, I::BITS + 3, I::BITS + 5),
136                (_, Mode::Constant) => Count::is(0, 0, I::BITS + 2, I::BITS + 4),
137                (_, _) => Count::is(0, 0, I::BITS + 4, I::BITS + 6),
138            },
139            false => match (case.0, case.1) {
140                (Mode::Constant, Mode::Constant) => Count::is(I::BITS, 0, 0, 0),
141                (_, _) => Count::is(0, 0, I::BITS + 1, I::BITS + 3),
142            },
143        }
144    }
145}
146
147impl<E: Environment, I: IntegerType> OutputMode<dyn SubChecked<Integer<E, I>, Output = Integer<E, I>>>
148    for Integer<E, I>
149{
150    type Case = (Mode, Mode);
151
152    fn output_mode(case: &Self::Case) -> Mode {
153        match (case.0, case.1) {
154            (Mode::Constant, Mode::Constant) => Mode::Constant,
155            (_, _) => Mode::Private,
156        }
157    }
158}
159
160#[cfg(test)]
161mod tests {
162    use super::*;
163    use snarkvm_circuit_environment::Circuit;
164
165    use test_utilities::*;
166
167    use core::{ops::RangeInclusive, panic::RefUnwindSafe};
168
169    const ITERATIONS: u64 = 128;
170
171    fn check_sub<I: IntegerType + RefUnwindSafe>(
172        name: &str,
173        first: console::Integer<<Circuit as Environment>::Network, I>,
174        second: console::Integer<<Circuit as Environment>::Network, I>,
175        mode_a: Mode,
176        mode_b: Mode,
177    ) {
178        let a = Integer::<Circuit, I>::new(mode_a, first);
179        let b = Integer::<Circuit, I>::new(mode_b, second);
180        match first.checked_sub(&second) {
181            Some(expected) => Circuit::scope(name, || {
182                let candidate = a.sub_checked(&b);
183                assert_eq!(expected, *candidate.eject_value());
184                assert_eq!(console::Integer::new(expected), candidate.eject_value());
185                assert_count!(Sub(Integer<I>, Integer<I>) => Integer<I>, &(mode_a, mode_b));
186                assert_output_mode!(Sub(Integer<I>, Integer<I>) => Integer<I>, &(mode_a, mode_b), candidate);
187            }),
188            None => match mode_a.is_constant() && mode_b.is_constant() {
189                true => check_operation_halts(&a, &b, Integer::sub_checked),
190                false => Circuit::scope(name, || {
191                    let _candidate = a.sub_checked(&b);
192                    assert_count_fails!(Sub(Integer<I>, Integer<I>) => Integer<I>, &(mode_a, mode_b));
193                }),
194            },
195        }
196        Circuit::reset();
197    }
198
199    fn run_test<I: IntegerType + RefUnwindSafe>(mode_a: Mode, mode_b: Mode) {
200        let mut rng = TestRng::default();
201
202        for i in 0..ITERATIONS {
203            let name = format!("Sub: {mode_a} - {mode_b} {i}");
204            let first = Uniform::rand(&mut rng);
205            let second = Uniform::rand(&mut rng);
206            check_sub::<I>(&name, first, second, mode_a, mode_b);
207        }
208
209        // Overflow
210        if I::is_signed() {
211            check_sub::<I>("MAX - (-1)", console::Integer::MAX, -console::Integer::one(), mode_a, mode_b);
212        }
213        // Underflow
214        check_sub::<I>("MIN - 1", console::Integer::MIN, console::Integer::one(), mode_a, mode_b);
215    }
216
217    fn run_exhaustive_test<I: IntegerType + RefUnwindSafe>(mode_a: Mode, mode_b: Mode)
218    where
219        RangeInclusive<I>: Iterator<Item = I>,
220    {
221        for first in I::MIN..=I::MAX {
222            for second in I::MIN..=I::MAX {
223                let first = console::Integer::<_, I>::new(first);
224                let second = console::Integer::<_, I>::new(second);
225
226                let name = format!("Sub: ({first} - {second})");
227                check_sub::<I>(&name, first, second, mode_a, mode_b);
228            }
229        }
230    }
231
232    test_integer_binary!(run_test, i8, minus);
233    test_integer_binary!(run_test, i16, minus);
234    test_integer_binary!(run_test, i32, minus);
235    test_integer_binary!(run_test, i64, minus);
236    test_integer_binary!(run_test, i128, minus);
237
238    test_integer_binary!(run_test, u8, minus);
239    test_integer_binary!(run_test, u16, minus);
240    test_integer_binary!(run_test, u32, minus);
241    test_integer_binary!(run_test, u64, minus);
242    test_integer_binary!(run_test, u128, minus);
243
244    test_integer_binary!(#[ignore], run_exhaustive_test, u8, minus, exhaustive);
245    test_integer_binary!(#[ignore], run_exhaustive_test, i8, minus, exhaustive);
246}