creusot_std/std/
num.rs

1use crate::{
2    ghost::Plain,
3    logic::ops::{AddLogic, MulLogic, NegLogic, NthBitLogic, SubLogic},
4    prelude::*,
5};
6#[cfg(creusot)]
7use core::ops::{
8    Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign,
9    Mul, MulAssign, Rem, RemAssign, Shl, ShlAssign, Shr, ShrAssign, Sub, SubAssign,
10};
11
12macro_rules! mach_int {
13    ($t:ty, $ty_nm:expr, $zero:expr, $to_int:literal) => {
14        impl View for $t {
15            type ViewTy = Int;
16            #[logic]
17            #[builtin(concat!($ty_nm, $to_int))]
18            fn view(self) -> Self::ViewTy {
19                dead
20            }
21        }
22
23        impl DeepModel for $t {
24            type DeepModelTy = Int;
25            #[logic(open, inline)]
26            fn deep_model(self) -> Self::DeepModelTy {
27                pearlite! { self@ }
28            }
29        }
30
31        impl Plain for $t {
32            #[trusted]
33            #[ensures(*result == *snap)]
34            #[check(ghost)]
35            #[allow(unused_variables)]
36            fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
37                Ghost::conjure()
38            }
39        }
40
41        extern_spec! {
42            impl Default for $t {
43                #[check(ghost)]
44                #[ensures(result == $zero)]
45                fn default() -> $t { 0 }
46            }
47
48            impl Clone for $t {
49                #[check(ghost)]
50                #[ensures(result == *self)]
51                fn clone(&self) -> $t {
52                    *self
53                }
54            }
55
56            #[constant(eval)]
57            const $t::MIN;
58
59            #[constant(eval)]
60            const $t::MAX;
61
62            #[constant(eval)]
63            const $t::BITS;
64
65            #[constant(eval)]
66            const core::$t::MIN;
67
68            #[constant(eval)]
69            const core::$t::MAX;
70        }
71
72        impl AddLogic for $t {
73            type Output = Self;
74            #[logic]
75            #[builtin(concat!($ty_nm, ".add"))]
76            #[allow(unused_variables)]
77            fn add_logic(self, other: Self) -> Self {
78                dead
79            }
80        }
81
82        impl SubLogic for $t {
83            type Output = Self;
84            #[logic]
85            #[builtin(concat!($ty_nm, ".sub"))]
86            #[allow(unused_variables)]
87            fn sub_logic(self, other: Self) -> Self {
88                dead
89            }
90        }
91
92        impl MulLogic for $t {
93            type Output = Self;
94            #[logic]
95            #[builtin(concat!($ty_nm, ".mul"))]
96            #[allow(unused_variables)]
97            fn mul_logic(self, other: Self) -> Self {
98                dead
99            }
100        }
101
102        impl NegLogic for $t {
103            type Output = Self;
104            #[logic]
105            #[builtin(concat!($ty_nm, ".neg"))]
106            fn neg_logic(self) -> Self {
107                dead
108            }
109        }
110
111        impl NthBitLogic for $t {
112            #[logic]
113            #[builtin(concat!($ty_nm, ".nth"))]
114            #[allow(unused_variables)]
115            fn nth_bit(self, n: Int) -> bool {
116                dead
117            }
118        }
119    };
120}
121
122mach_int!(u8, "creusot.int.UInt8$BW$", 0u8, ".t'int");
123mach_int!(u16, "creusot.int.UInt16$BW$", 0u16, ".t'int");
124mach_int!(u32, "creusot.int.UInt32$BW$", 0u32, ".t'int");
125mach_int!(u64, "creusot.int.UInt64$BW$", 0u64, ".t'int");
126mach_int!(u128, "creusot.int.UInt128$BW$", 0u128, ".t'int");
127#[cfg(target_pointer_width = "64")]
128mach_int!(usize, "creusot.int.UInt64$BW$", 0usize, ".t'int");
129#[cfg(target_pointer_width = "32")]
130mach_int!(usize, "creusot.int.UInt32$BW$", 0usize, ".t'int");
131#[cfg(target_pointer_width = "16")]
132mach_int!(usize, "creusot.int.UInt16$BW$", 0usize, ".t'int");
133
134mach_int!(i8, "creusot.int.Int8$BW$", 0i8, ".to_int");
135mach_int!(i16, "creusot.int.Int16$BW$", 0i16, ".to_int");
136mach_int!(i32, "creusot.int.Int32$BW$", 0i32, ".to_int");
137mach_int!(i64, "creusot.int.Int64$BW$", 0i64, ".to_int");
138mach_int!(i128, "creusot.int.Int128$BW$", 0i128, ".to_int");
139#[cfg(target_pointer_width = "64")]
140mach_int!(isize, "creusot.int.Int64$BW$", 0isize, ".to_int");
141#[cfg(target_pointer_width = "32")]
142mach_int!(isize, "creusot.int.Int32$BW$", 0isize, ".to_int");
143#[cfg(target_pointer_width = "16")]
144mach_int!(isize, "creusot.int.Int16$BW$", 0isize, ".to_int");
145
146/// Adds specifications for checked, wrapping, saturating, and overflowing operations on the given
147/// integer type
148macro_rules! spec_type {
149    ($type:ty) => {
150        // Specify addition, subtraction and multiplication
151        spec_op_common! {$type}
152        spec_impl_common! {$type}
153        spec_div_rem! {$type}
154        spec_bits! {$type}
155        spec_shifts! {$type}
156
157        extern_spec! {
158            impl $type {
159                #[allow(dead_code)]
160                #[check(ghost)]
161                #[ensures(result == -self)]
162                fn wrapping_neg(self) -> $type;
163            }
164        }
165
166        // Specify division separately, because it has the additional precondition that the divisor
167        // is non-zero. Overflow on division can only occur on signed types and only when computing
168        // `$type::MIN / -1`.
169        extern_spec! {
170            impl $type {
171                #[allow(dead_code)]
172                #[check(ghost)]
173                // Returns `None` iff the divisor is zero or the division overflows
174                #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
175                // Else, returns the result of the division
176                #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@)]
177                fn checked_div(self, rhs: $type) -> Option<$type>;
178
179                #[allow(dead_code)]
180                #[check(ghost)]
181                // Panics if the divisor is zero
182                #[requires(rhs@ != 0)]
183                // Returns `self` if the division overflows
184                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == self@)]
185                // Else, returns the result of the division
186                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
187                fn wrapping_div(self, rhs: $type) -> $type;
188
189                #[allow(dead_code)]
190                #[check(ghost)]
191                // Panics if the divisor is zero
192                #[requires(rhs@ != 0)]
193                // Returns `$type::MIN` if the division overflows
194                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == $type::MIN@)]
195                // Else, returns the result of the division
196                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
197                fn saturating_div(self, rhs: $type) -> $type;
198
199                #[allow(dead_code)]
200                #[check(ghost)]
201                // Panics if the divisor is zero
202                #[requires(rhs@ != 0)]
203                // Returns `self` if the division overflows
204                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result.0@ == self@)]
205                // Else, returns the result of the division
206                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result.0@ == self@ / rhs@)]
207                // Overflow only occurs when computing `$type::MIN / -1`
208                #[ensures(result.1 == (self@ == $type::MIN@ && rhs@ == -1))]
209                fn overflowing_div(self, rhs: $type) -> ($type, bool);
210            }
211        }
212    };
213}
214
215pub trait NumExt {
216    #[logic]
217    fn leading_zeros_logic(self) -> u32;
218
219    #[logic]
220    fn trailing_zeros_logic(self) -> u32;
221
222    #[logic]
223    fn leading_ones_logic(self) -> u32;
224
225    #[logic]
226    fn trailing_ones_logic(self) -> u32;
227}
228
229macro_rules! spec_unsized {
230    ($type:ty, $zero:expr, $one:expr) => {
231        spec_type!($type);
232
233        impl NumExt for $type {
234            #[logic(opaque)]
235            #[trusted]
236            #[ensures(result <= $type::BITS)]
237            #[ensures((result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one))]
238            #[ensures((result == $type::BITS) == (self == $zero))]
239            fn leading_zeros_logic(self) -> u32 {
240                dead
241            }
242
243            #[logic(opaque)]
244            #[trusted]
245            #[ensures(result <= $type::BITS)]
246            #[ensures((result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32)))]
247            #[ensures((result == $type::BITS) == (self == $zero))]
248            fn trailing_zeros_logic(self) -> u32 {
249                dead
250            }
251
252            #[logic(opaque)]
253            #[trusted]
254            #[ensures(result <= $type::BITS)]
255            #[ensures((result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero))]
256            #[ensures((result == $type::BITS) == (self == $type::MAX))]
257            fn leading_ones_logic(self) -> u32 {
258                dead
259            }
260
261            #[logic(opaque)]
262            #[trusted]
263            #[ensures(result <= $type::BITS)]
264            #[ensures((result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32)))]
265            #[ensures((result == $type::BITS) == (self == $type::MAX))]
266            fn trailing_ones_logic(self) -> u32 {
267                dead
268            }
269        }
270
271        extern_spec! {
272            impl $type {
273                    #[check(ghost)]
274                    #[ensures(if self == $zero { result == (self == $zero) } else { result == (self@ % rhs@ == 0) })]
275                    fn is_multiple_of(self, rhs: Self) -> bool;
276
277                    #[check(ghost)]
278                    #[ensures(result == (self != $zero && self & (self - $one) == $zero))]
279                    fn is_power_of_two(self) -> bool;
280
281                    #[check(ghost)]
282                    #[ensures(result == self.leading_zeros_logic())]
283                    fn leading_zeros(self) -> u32;
284
285                    #[check(ghost)]
286                    #[ensures(result == self.trailing_zeros_logic())]
287                    fn trailing_zeros(self) -> u32;
288
289                    #[check(ghost)]
290                    #[ensures(result == self.leading_ones_logic())]
291                    fn leading_ones(self) -> u32;
292
293                    #[check(ghost)]
294                    #[ensures(result == self.trailing_ones_logic())]
295                    fn trailing_ones(self) -> u32;
296            }
297        }
298    };
299}
300
301/// Adds specifications for checked, wrapping, saturating, and overflowing versions of the given
302/// operation on the given type. This only works for operations that have no additional pre- or
303/// postconditions.
304macro_rules! spec_op_common {
305    ($type:ty) => {
306        spec_op_common!{$type, +, checked_add, wrapping_add, saturating_add, overflowing_add, unchecked_add}
307        spec_op_common!{$type, -, checked_sub, wrapping_sub, saturating_sub, overflowing_sub, unchecked_sub}
308        spec_op_common!{$type, *, checked_mul, wrapping_mul, saturating_mul, overflowing_mul, unchecked_mul}
309    };
310    (
311        $type:ty,
312        $op:tt,
313        $checked:ident,
314        $wrapping:ident,
315        $saturating:ident,
316        $overflowing:ident,
317        $unchecked:ident
318    ) => {
319        extern_spec! {
320            impl $type {
321                // Checked: performs the operation on `Int`, returns `Some` if the result is between
322                // `$type::MIN` and `$type::MAX`, or `None` if the result cannot be represented by
323                // `$type`
324                #[allow(dead_code)]
325                #[check(ghost)]
326                // Returns `None` iff the result is out of range
327                #[ensures(
328                    (result == None)
329                    == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
330                )]
331                // Returns `Some(result)` if the result is in range
332                #[ensures(forall<r: $type> result == Some(r) ==> r@ == (self@ $op rhs@))]
333                fn $checked(self, rhs: $type) -> Option<$type>;
334
335                // Wrapping: performs the operation on `Int` and converts back to `$type`
336                #[allow(dead_code)]
337                #[check(ghost)]
338                #[ensures(result == self $op rhs)]
339                fn $wrapping(self, rhs: $type) -> $type;
340
341                // Saturating: performs the operation on `Int` and clamps the result between
342                // `$type::MIN` and `$type::MAX`
343                #[allow(dead_code)]
344                #[check(ghost)]
345                // Returns the result if it is in range
346                #[ensures(
347                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
348                    ==> result@ == (self@ $op rhs@)
349                )]
350                // Returns the nearest bound if the result is out of range
351                #[ensures((self@ $op rhs@) < $type::MIN@ ==> result@ == $type::MIN@)]
352                #[ensures((self@ $op rhs@) > $type::MAX@ ==> result@ == $type::MAX@)]
353                fn $saturating(self, rhs: $type) -> $type;
354
355                // Overflowing: performs the operation on `Int` and converts back to `$type`, and
356                // indicates whether an overflow occurred
357                #[allow(dead_code)]
358                #[check(ghost)]
359                // Returns the result if it is in range
360                #[ensures(
361                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
362                    ==> result.0@ == (self@ $op rhs@)
363                )]
364                // Returns the result shifted by a multiple of the type's range if it is out of
365                // range. For addition and subtraction, `k` (qualified over below) will always be 1
366                // or -1, but the verifier is able to deduce that.
367                #[ensures(
368                    exists<k: Int> result.0@ == (self@ $op rhs@) + k * ($type::MAX@ - $type::MIN@ + 1)
369                )]
370                // Overflow occurred iff the result is out of range
371                #[ensures(
372                    result.1 == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
373                )]
374                fn $overflowing(self, rhs: $type) -> ($type, bool);
375
376                #[check(ghost)]
377                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
378                #[ensures(result@ == self@ $op rhs@)]
379                unsafe fn $unchecked(self, rhs: $type) -> $type;
380            }
381        }
382    };
383}
384
385macro_rules! spec_impl_common {
386    ($type:ty) => {
387        spec_impl_common!{Add, add, +, AddAssign, add_assign, +=, $type}
388        spec_impl_common!{Sub, sub, -, SubAssign, sub_assign, -=, $type}
389        spec_impl_common!{Mul, mul, *, MulAssign, mul_assign, *=, $type}
390    };
391    ($op_trait:ident, $op_method:ident, $op:tt, $op_assign_trait:ident, $op_assign_method:ident, $op_assign:tt, $type:ty) => {
392        spec_impl_common!{@ $op_trait, $op_method, $op, $type, $type, $type}
393        spec_impl_common!{@ $op_trait, $op_method, $op, $type, $type, &$type}
394        spec_impl_common!{@ $op_trait, $op_method, $op, $type, &$type, $type}
395        spec_impl_common!{@ $op_trait, $op_method, $op, $type, &$type, &$type}
396        spec_impl_common!{@assign $op_assign_trait, $op_assign_method, $op_assign, $op, $type, $type}
397        spec_impl_common!{@assign $op_assign_trait, $op_assign_method, $op_assign, $op, $type, &$type}
398    };
399    (@ $op_trait:ident, $op_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
400        extern_spec! {
401            impl $op_trait<$rhs> for $lhs {
402                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
403                #[ensures(result@ == self@ $op rhs@)]
404                fn $op_method(self, rhs: $rhs) -> $type {
405                    self $op rhs
406                }
407            }
408        }
409    };
410    (@assign $op_assign_trait:ident, $op_assign_method:ident, $op_assign:tt, $op:tt, $type:ty, $rhs:ty) => {
411        extern_spec! {
412            impl $op_assign_trait<$rhs> for $type {
413                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
414                #[ensures((^self)@ == self@ $op rhs@)]
415                fn $op_assign_method(&mut self, rhs: $rhs) {
416                    *self $op_assign rhs
417                }
418            }
419        }
420    }
421}
422
423macro_rules! spec_div_rem {
424    ($type:ty) => {
425        spec_div_rem!{@ Div, div, /, $type}
426        spec_div_rem!{@ Rem, rem, %, $type}
427        spec_div_rem!{@assign DivAssign, div_assign, /=, /, $type}
428        spec_div_rem!{@assign RemAssign, rem_assign, %=, %, $type}
429    };
430    (@ $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty) => {
431        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, $type, $type}
432        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, $type, &$type}
433        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, &$type, $type}
434        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, &$type, &$type}
435    };
436    (@ $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
437        extern_spec! {
438            impl $divrem_trait<$rhs> for $lhs {
439                #[requires(rhs@ != 0)]
440                #[requires(!(self@ == $type::MIN@ && rhs@ == -1))]
441                #[ensures(result@ == self@ $op rhs@)]
442                fn $divrem_method(self, rhs: $rhs) -> $type {
443                    self $op rhs
444                }
445            }
446        }
447    };
448    (@assign $divrem_assign_trait:ident, $divrem_assign_method:ident, $op_assign:tt, $op:tt, $type:ty) => {
449        spec_div_rem!{@assign $divrem_assign_trait, $divrem_assign_method, $op_assign, $op, $type, $type}
450        spec_div_rem!{@assign $divrem_assign_trait, $divrem_assign_method, $op_assign, $op, $type, &$type}
451    };
452    (@assign $divrem_assign_trait:ident, $divrem_assign_method:ident, $op_assign:tt, $op:tt, $type:ty, $rhs:ty) => {
453        extern_spec! {
454            impl $divrem_assign_trait<$rhs> for $type {
455                #[requires(rhs@ != 0)]
456                #[requires(!(*self == $type::MIN && rhs@ == -1))]
457                #[ensures((^self)@ == self@ $op rhs@)]
458                fn $divrem_assign_method(&mut self, rhs: $rhs) {
459                    *self $op_assign rhs
460                }
461            }
462        }
463    };
464}
465
466macro_rules! spec_bits {
467    ($type:ty) => {
468        spec_bits! {$type, &, BitAnd, bitand, BitAndAssign, bitand_assign}
469        spec_bits! {$type, |, BitOr, bitor, BitOrAssign, bitor_assign}
470        spec_bits! {$type, ^, BitXor, bitxor, BitXorAssign, bitxor_assign}
471    };
472    ($type:ty, $op:tt, $tr:ident, $f:ident, $tr_assign:ident, $f_assign: ident) => {
473        extern_spec! {
474            impl $tr for $type {
475                #[check(ghost)]
476                #[ensures(result == self $op rhs)]
477                fn $f(self, rhs: $type) -> $type;
478            }
479
480            impl $tr for &$type {
481                #[check(ghost)]
482                #[ensures(result == *self $op *rhs)]
483                fn $f(self, rhs: &$type) -> $type;
484            }
485
486            impl $tr<&$type> for $type {
487                #[check(ghost)]
488                #[ensures(result == self $op *rhs)]
489                fn $f(self, rhs: &$type) -> $type;
490            }
491
492            impl $tr<$type> for &$type {
493                #[check(ghost)]
494                #[ensures(result == *self $op rhs)]
495                fn $f(self, rhs: $type) -> $type;
496            }
497
498            impl $tr_assign for $type {
499                #[check(ghost)]
500                #[ensures(^self == *self $op rhs)]
501                fn $f_assign(&mut self, rhs: $type);
502            }
503
504            impl $tr_assign<&$type> for $type {
505                #[check(ghost)]
506                #[ensures(^self == *self $op *rhs)]
507                fn $f_assign(&mut self, rhs: &$type);
508            }
509        }
510    };
511}
512
513macro_rules! spec_shifts {
514    ($type:ty) => {
515        spec_shifts! {$type, u8 u16 u32 u64 u128 usize i8 i16 i32 i64 i128 isize}
516    };
517    ($type:ty, $($rhs:ty)*) => {
518        $(spec_shifts! {$type, $rhs, >>, Shr, shr, ShrAssign, shr_assign})*
519        $(spec_shifts! {$type, $rhs, <<, Shl, shl, ShlAssign, shl_assign})*
520    };
521    ($type:ty, $rhs:ty, $op:tt, $tr:ident, $f:ident, $tr_assign:ident, $f_assign:ident) => {
522        extern_spec! {
523            impl $tr<$rhs> for $type {
524                #[requires((0usize as $rhs) <= rhs && rhs < $type::BITS as $rhs)]
525                #[ensures(result == self $op rhs)]
526                fn $f(self, rhs: $rhs) -> $type;
527            }
528
529            impl $tr<&$rhs> for $type {
530                #[requires((0usize as $rhs) <= *rhs && *rhs < $type::BITS as $rhs)]
531                #[ensures(result == self $op *rhs)]
532                fn $f(self, rhs: &$rhs) -> $type;
533            }
534
535            impl $tr<$rhs> for &$type {
536                #[requires((0usize as $rhs) <= rhs && rhs < $type::BITS as $rhs)]
537                #[ensures(result == *self $op rhs)]
538                fn $f(self, rhs: $rhs) -> $type;
539            }
540
541            impl $tr<&$rhs> for &$type {
542                #[requires((0usize as $rhs) <= *rhs && *rhs < $type::BITS as $rhs)]
543                #[ensures(result == *self $op *rhs)]
544                fn $f(self, rhs: &$rhs) -> $type;
545            }
546
547            impl $tr_assign<$rhs> for $type {
548                #[requires((0usize as $rhs) <= rhs && rhs < $type::BITS as $rhs)]
549                #[ensures(^self == *self $op rhs)]
550                fn $f_assign(&mut self, rhs: $rhs);
551            }
552
553            impl $tr_assign<&$rhs> for $type {
554                #[requires((0usize as $rhs) <= *rhs && *rhs < $type::BITS as $rhs)]
555                #[ensures(^self == *self $op rhs)]
556                fn $f_assign(&mut self, rhs: &$rhs);
557            }
558        }
559    };
560}
561
562/// Adds specifications for the abs_diff operation on the given pair of signed
563/// and unsigned integer types
564macro_rules! spec_abs_diff {
565    ($unsigned:ty, $signed:ty) => {
566        extern_spec! {
567            impl $unsigned {
568                #[allow(dead_code)]
569                #[check(ghost)]
570                #[ensures(result@ == self@.abs_diff(other@))]
571                fn abs_diff(self, other: $unsigned) -> $unsigned;
572            }
573
574            impl $signed {
575                #[allow(dead_code)]
576                #[check(ghost)]
577                #[ensures(result@ == self@.abs_diff(other@))]
578                fn abs_diff(self, other: $signed) -> $unsigned;
579            }
580        }
581    };
582}
583
584spec_bits!(bool);
585
586spec_unsized!(u8, 0u8, 1u8);
587spec_unsized!(u16, 0u16, 1u16);
588spec_unsized!(u32, 0u32, 1u32);
589spec_unsized!(u64, 0u64, 1u64);
590spec_unsized!(u128, 0u128, 1u128);
591spec_unsized!(usize, 0usize, 1usize);
592
593spec_type!(i8);
594spec_type!(i16);
595spec_type!(i32);
596spec_type!(i64);
597spec_type!(i128);
598spec_type!(isize);
599
600spec_abs_diff!(u8, i8);
601spec_abs_diff!(u16, i16);
602spec_abs_diff!(u32, i32);
603spec_abs_diff!(u64, i64);
604spec_abs_diff!(u128, i128);
605spec_abs_diff!(usize, isize);
creusot_std/std/num.rs

creusot_std/std/
num.rs
