creusot_std/std/
num.rs

1use crate::{
2    ghost::Plain,
3    logic::ops::{
4        AddLogic, BitAndLogic, BitOrLogic, BitXorLogic, MulLogic, NegLogic, NotLogic, ShlLogic,
5        ShrLogic, SubLogic,
6    },
7    prelude::*,
8};
9use core::num::Wrapping;
10// Resolve links like [`i8::add`] in the generated documentation
11#[cfg(creusot)]
12use core::ops::{
13    Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign,
14    Mul, MulAssign, Neg, Rem, RemAssign, Shl, ShlAssign, Shr, ShrAssign, Sub, SubAssign,
15};
16
17/// Trait for the nth bit of a bitvector in logic code.
18pub trait NthBitLogic {
19    /// The nth bit of a bitvector.
20    /// In [`bitwise_proof`] mode, this is translated to [`nth`](https://www.why3.org/stdlib/bv.html#nth_188) in Why3.
21    /// Otherwise this is an abstract function.
22    #[logic]
23    fn nth_bit(self, n: Int) -> bool;
24}
25
26macro_rules! mach_int {
27    ($t:ty, $ty_nm:expr, $zero:expr, $to_int:literal) => {
28        impl View for $t {
29            type ViewTy = Int;
30            #[logic]
31            #[builtin(concat!($ty_nm, $to_int))]
32            fn view(self) -> Self::ViewTy {
33                dead
34            }
35        }
36
37        impl DeepModel for $t {
38            type DeepModelTy = Int;
39            #[logic(open, inline)]
40            fn deep_model(self) -> Self::DeepModelTy {
41                pearlite! { self@ }
42            }
43        }
44
45        impl Plain for $t {
46            #[trusted]
47            #[ensures(*result == *snap)]
48            #[check(ghost)]
49            #[allow(unused_variables)]
50            fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
51                Ghost::conjure()
52            }
53        }
54
55        extern_spec! {
56            impl Default for $t {
57                #[check(ghost)]
58                #[ensures(result == $zero)]
59                fn default() -> $t { 0 }
60            }
61
62            impl Clone for $t {
63                #[check(ghost)]
64                #[ensures(result == *self)]
65                fn clone(&self) -> $t {
66                    *self
67                }
68            }
69
70            #[constant(eval)]
71            const $t::MIN;
72
73            #[constant(eval)]
74            const $t::MAX;
75
76            #[constant(eval)]
77            const $t::BITS;
78
79            #[constant(eval)]
80            const core::$t::MIN;
81
82            #[constant(eval)]
83            const core::$t::MAX;
84        }
85
86        impl AddLogic for $t {
87            type Output = Self;
88            #[logic]
89            #[builtin(concat!($ty_nm, ".add"))]
90            #[allow(unused_variables)]
91            fn add_logic(self, other: Self) -> Self {
92                dead
93            }
94        }
95
96        impl SubLogic for $t {
97            type Output = Self;
98            #[logic]
99            #[builtin(concat!($ty_nm, ".sub"))]
100            #[allow(unused_variables)]
101            fn sub_logic(self, other: Self) -> Self {
102                dead
103            }
104        }
105
106        impl MulLogic for $t {
107            type Output = Self;
108            #[logic]
109            #[builtin(concat!($ty_nm, ".mul"))]
110            #[allow(unused_variables)]
111            fn mul_logic(self, other: Self) -> Self {
112                dead
113            }
114        }
115
116        impl NegLogic for $t {
117            type Output = Self;
118            #[logic]
119            #[builtin(concat!($ty_nm, ".neg"))]
120            fn neg_logic(self) -> Self {
121                dead
122            }
123        }
124
125        impl ShlLogic for $t {
126            type Output = Self;
127            #[logic]
128            #[builtin(concat!($ty_nm, ".shl"))]
129            #[allow(unused_variables)]
130            fn shl_logic(self, other: Self) -> Self {
131                dead
132            }
133        }
134
135        impl ShrLogic for $t {
136            type Output = Self;
137            #[logic]
138            #[builtin(concat!($ty_nm, ".shr"))]
139            #[allow(unused_variables)]
140            fn shr_logic(self, other: Self) -> Self {
141                dead
142            }
143        }
144
145        impl BitAndLogic for $t {
146            type Output = Self;
147            #[logic]
148            #[builtin(concat!($ty_nm, ".bw_and"))]
149            #[allow(unused_variables)]
150            fn bitand_logic(self, other: Self) -> Self {
151                dead
152            }
153        }
154
155        impl BitOrLogic for $t {
156            type Output = Self;
157            #[logic]
158            #[builtin(concat!($ty_nm, ".bw_or"))]
159            #[allow(unused_variables)]
160            fn bitor_logic(self, other: Self) -> Self {
161                dead
162            }
163        }
164
165        impl BitXorLogic for $t {
166            type Output = Self;
167            #[logic]
168            #[builtin(concat!($ty_nm, ".bw_xor"))]
169            #[allow(unused_variables)]
170            fn bitxor_logic(self, other: Self) -> Self {
171                dead
172            }
173        }
174
175        impl NotLogic for $t {
176            type Output = Self;
177            #[logic]
178            #[builtin(concat!($ty_nm, ".bw_not"))]
179            #[allow(unused_variables)]
180            fn not_logic(self) -> Self {
181                dead
182            }
183        }
184
185        impl NthBitLogic for $t {
186            #[logic]
187            #[builtin(concat!($ty_nm, ".nth"))]
188            #[allow(unused_variables)]
189            fn nth_bit(self, n: Int) -> bool {
190                dead
191            }
192        }
193    };
194}
195
196mach_int!(u8, "creusot.int.UInt8$BW$", 0u8, ".t'int");
197mach_int!(u16, "creusot.int.UInt16$BW$", 0u16, ".t'int");
198mach_int!(u32, "creusot.int.UInt32$BW$", 0u32, ".t'int");
199mach_int!(u64, "creusot.int.UInt64$BW$", 0u64, ".t'int");
200mach_int!(u128, "creusot.int.UInt128$BW$", 0u128, ".t'int");
201#[cfg(target_pointer_width = "64")]
202mach_int!(usize, "creusot.int.UInt64$BW$", 0usize, ".t'int");
203#[cfg(target_pointer_width = "32")]
204mach_int!(usize, "creusot.int.UInt32$BW$", 0usize, ".t'int");
205#[cfg(target_pointer_width = "16")]
206mach_int!(usize, "creusot.int.UInt16$BW$", 0usize, ".t'int");
207
208mach_int!(i8, "creusot.int.Int8$BW$", 0i8, ".to_int");
209mach_int!(i16, "creusot.int.Int16$BW$", 0i16, ".to_int");
210mach_int!(i32, "creusot.int.Int32$BW$", 0i32, ".to_int");
211mach_int!(i64, "creusot.int.Int64$BW$", 0i64, ".to_int");
212mach_int!(i128, "creusot.int.Int128$BW$", 0i128, ".to_int");
213#[cfg(target_pointer_width = "64")]
214mach_int!(isize, "creusot.int.Int64$BW$", 0isize, ".to_int");
215#[cfg(target_pointer_width = "32")]
216mach_int!(isize, "creusot.int.Int32$BW$", 0isize, ".to_int");
217#[cfg(target_pointer_width = "16")]
218mach_int!(isize, "creusot.int.Int16$BW$", 0isize, ".to_int");
219
220/// Adds specifications for checked, wrapping, saturating, and overflowing operations on the given
221/// integer type
222macro_rules! spec_type {
223    ($type:ty) => {
224        // Specify addition, subtraction and multiplication
225        spec_op_common! {$type}
226        spec_impl_common! {$type}
227        spec_div_rem! {$type}
228        spec_bits! {$type}
229        spec_shifts! {$type}
230
231        extern_spec! {
232            impl $type {
233                #[allow(dead_code)]
234                #[check(ghost)]
235                #[ensures(result == -self)]
236                fn wrapping_neg(self) -> $type;
237            }
238        }
239
240        // Specify division separately, because it has the additional precondition that the divisor
241        // is non-zero. Overflow on division can only occur on signed types and only when computing
242        // `$type::MIN / -1`.
243        extern_spec! {
244            impl $type {
245                #[allow(dead_code)]
246                #[check(ghost)]
247                // Returns `None` iff the divisor is zero or the division overflows
248                #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
249                // Else, returns the result of the division
250                #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@)]
251                fn checked_div(self, rhs: $type) -> Option<$type>;
252
253                #[allow(dead_code)]
254                #[check(ghost)]
255                // Panics if the divisor is zero
256                #[requires(rhs@ != 0)]
257                // Returns `self` if the division overflows
258                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == self@)]
259                // Else, returns the result of the division
260                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
261                fn wrapping_div(self, rhs: $type) -> $type;
262
263                #[allow(dead_code)]
264                #[check(ghost)]
265                // Panics if the divisor is zero
266                #[requires(rhs@ != 0)]
267                // Returns `$type::MIN` if the division overflows
268                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == $type::MIN@)]
269                // Else, returns the result of the division
270                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
271                fn saturating_div(self, rhs: $type) -> $type;
272
273                #[allow(dead_code)]
274                #[check(ghost)]
275                // Panics if the divisor is zero
276                #[requires(rhs@ != 0)]
277                // Returns `self` if the division overflows
278                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result.0@ == self@)]
279                // Else, returns the result of the division
280                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result.0@ == self@ / rhs@)]
281                // Overflow only occurs when computing `$type::MIN / -1`
282                #[ensures(result.1 == (self@ == $type::MIN@ && rhs@ == -1))]
283                fn overflowing_div(self, rhs: $type) -> ($type, bool);
284            }
285        }
286    };
287}
288
289pub trait NumExt {
290    #[logic]
291    fn leading_zeros_logic(self) -> u32;
292
293    #[logic]
294    fn trailing_zeros_logic(self) -> u32;
295
296    #[logic]
297    fn leading_ones_logic(self) -> u32;
298
299    #[logic]
300    fn trailing_ones_logic(self) -> u32;
301}
302
303macro_rules! spec_unsigned {
304    ($type:ty, $zero:expr, $one:expr) => {
305        spec_type!($type);
306
307        impl NumExt for $type {
308            #[logic(opaque)]
309            #[trusted]
310            #[ensures(result <= $type::BITS)]
311            #[ensures((result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one))]
312            #[ensures((result == $type::BITS) == (self == $zero))]
313            fn leading_zeros_logic(self) -> u32 {
314                dead
315            }
316
317            #[logic(opaque)]
318            #[trusted]
319            #[ensures(result <= $type::BITS)]
320            #[ensures((result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32)))]
321            #[ensures((result == $type::BITS) == (self == $zero))]
322            fn trailing_zeros_logic(self) -> u32 {
323                dead
324            }
325
326            #[logic(opaque)]
327            #[trusted]
328            #[ensures(result <= $type::BITS)]
329            #[ensures((result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero))]
330            #[ensures((result == $type::BITS) == (self == $type::MAX))]
331            fn leading_ones_logic(self) -> u32 {
332                dead
333            }
334
335            #[logic(opaque)]
336            #[trusted]
337            #[ensures(result <= $type::BITS)]
338            #[ensures((result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32)))]
339            #[ensures((result == $type::BITS) == (self == $type::MAX))]
340            fn trailing_ones_logic(self) -> u32 {
341                dead
342            }
343        }
344
345        extern_spec! {
346            impl $type {
347                    #[check(ghost)]
348                    #[ensures(if self == $zero { result == (self == $zero) } else { result == (self@ % rhs@ == 0) })]
349                    fn is_multiple_of(self, rhs: Self) -> bool;
350
351                    #[check(ghost)]
352                    #[ensures(result == (self != $zero && self & (self - $one) == $zero))]
353                    fn is_power_of_two(self) -> bool;
354
355                    #[check(ghost)]
356                    #[logic_alias($type::leading_zeros_logic)]
357                    fn leading_zeros(self) -> u32;
358
359                    #[check(ghost)]
360                    #[logic_alias($type::trailing_zeros_logic)]
361                    fn trailing_zeros(self) -> u32;
362
363                    #[check(ghost)]
364                    #[logic_alias($type::leading_ones_logic)]
365                    fn leading_ones(self) -> u32;
366
367                    #[check(ghost)]
368                    #[logic_alias($type::trailing_ones_logic)]
369                    fn trailing_ones(self) -> u32;
370            }
371        }
372
373        spec_div_rem!{@nz Div, div, /, $type, $type, $type}
374        spec_div_rem!{@nz Rem, rem, %, $type, $type, $type}
375    };
376}
377
378/// Adds specifications for checked, wrapping, saturating, and overflowing versions of the given
379/// operation on the given type. This only works for operations that have no additional pre- or
380/// postconditions.
381macro_rules! spec_op_common {
382    ($type:ty) => {
383        spec_op_common!{$type, +, checked_add, wrapping_add, saturating_add, overflowing_add, unchecked_add}
384        spec_op_common!{$type, -, checked_sub, wrapping_sub, saturating_sub, overflowing_sub, unchecked_sub}
385        spec_op_common!{$type, *, checked_mul, wrapping_mul, saturating_mul, overflowing_mul, unchecked_mul}
386    };
387    (
388        $type:ty,
389        $op:tt,
390        $checked:ident,
391        $wrapping:ident,
392        $saturating:ident,
393        $overflowing:ident,
394        $unchecked:ident
395    ) => {
396        extern_spec! {
397            impl $type {
398                // Checked: performs the operation on `Int`, returns `Some` if the result is between
399                // `$type::MIN` and `$type::MAX`, or `None` if the result cannot be represented by
400                // `$type`
401                #[allow(dead_code)]
402                #[check(ghost)]
403                // Returns `None` iff the result is out of range
404                #[ensures(
405                    (result == None)
406                    == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
407                )]
408                // Returns `Some(result)` if the result is in range
409                #[ensures(forall<r: $type> result == Some(r) ==> r@ == (self@ $op rhs@))]
410                fn $checked(self, rhs: $type) -> Option<$type>;
411
412                // Wrapping: performs the operation on `Int` and converts back to `$type`
413                #[allow(dead_code)]
414                #[check(ghost)]
415                #[ensures(result == self $op rhs)]
416                fn $wrapping(self, rhs: $type) -> $type;
417
418                // Saturating: performs the operation on `Int` and clamps the result between
419                // `$type::MIN` and `$type::MAX`
420                #[allow(dead_code)]
421                #[check(ghost)]
422                // Returns the result if it is in range
423                #[ensures(
424                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
425                    ==> result@ == (self@ $op rhs@)
426                )]
427                // Returns the nearest bound if the result is out of range
428                #[ensures((self@ $op rhs@) < $type::MIN@ ==> result@ == $type::MIN@)]
429                #[ensures((self@ $op rhs@) > $type::MAX@ ==> result@ == $type::MAX@)]
430                fn $saturating(self, rhs: $type) -> $type;
431
432                // Overflowing: performs the operation on `Int` and converts back to `$type`, and
433                // indicates whether an overflow occurred
434                #[allow(dead_code)]
435                #[check(ghost)]
436                // Returns the result if it is in range
437                #[ensures(
438                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
439                    ==> result.0@ == (self@ $op rhs@)
440                )]
441                // Returns the result shifted by a multiple of the type's range if it is out of
442                // range. For addition and subtraction, `k` (qualified over below) will always be 1
443                // or -1, but the verifier is able to deduce that.
444                #[ensures(
445                    exists<k: Int> result.0@ == (self@ $op rhs@) + k * ($type::MAX@ - $type::MIN@ + 1)
446                )]
447                // Overflow occurred iff the result is out of range
448                #[ensures(
449                    result.1 == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
450                )]
451                fn $overflowing(self, rhs: $type) -> ($type, bool);
452
453                #[check(ghost)]
454                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
455                #[ensures(result@ == self@ $op rhs@)]
456                unsafe fn $unchecked(self, rhs: $type) -> $type;
457            }
458        }
459    };
460}
461
462macro_rules! spec_impl_common {
463    ($type:ty) => {
464        spec_impl_common!{Add, add, +, AddAssign, add_assign, +=, $type}
465        spec_impl_common!{Sub, sub, -, SubAssign, sub_assign, -=, $type}
466        spec_impl_common!{Mul, mul, *, MulAssign, mul_assign, *=, $type}
467    };
468    ($op_trait:ident, $op_method:ident, $op:tt, $op_assign_trait:ident, $op_assign_method:ident, $op_assign:tt, $type:ty) => {
469        spec_impl_common!{@ $op_trait, $op_method, $op, $type, $type, $type}
470        spec_impl_common!{@ $op_trait, $op_method, $op, $type, $type, &$type}
471        spec_impl_common!{@ $op_trait, $op_method, $op, $type, &$type, $type}
472        spec_impl_common!{@ $op_trait, $op_method, $op, $type, &$type, &$type}
473        spec_impl_common!{@assign $op_assign_trait, $op_assign_method, $op_assign, $op, $type, $type}
474        spec_impl_common!{@assign $op_assign_trait, $op_assign_method, $op_assign, $op, $type, &$type}
475    };
476    (@ $op_trait:ident, $op_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
477        extern_spec! {
478            impl $op_trait<$rhs> for $lhs {
479                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
480                #[ensures(result@ == self@ $op rhs@)]
481                fn $op_method(self, rhs: $rhs) -> $type {
482                    self $op rhs
483                }
484            }
485        }
486    };
487    (@assign $op_assign_trait:ident, $op_assign_method:ident, $op_assign:tt, $op:tt, $type:ty, $rhs:ty) => {
488        extern_spec! {
489            impl $op_assign_trait<$rhs> for $type {
490                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
491                #[ensures((^self)@ == self@ $op rhs@)]
492                fn $op_assign_method(&mut self, rhs: $rhs) {
493                    *self $op_assign rhs
494                }
495            }
496        }
497    }
498}
499
500macro_rules! spec_div_rem {
501    ($type:ty) => {
502        spec_div_rem!{@ Div, div, /, $type}
503        spec_div_rem!{@ Rem, rem, %, $type}
504        spec_div_rem!{@assign DivAssign, div_assign, /=, /, $type}
505        spec_div_rem!{@assign RemAssign, rem_assign, %=, %, $type}
506    };
507    (@ $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty) => {
508        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, $type, $type}
509        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, $type, &$type}
510        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, &$type, $type}
511        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, &$type, &$type}
512    };
513    (@ $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
514        extern_spec! {
515            impl $divrem_trait<$rhs> for $lhs {
516                #[requires(rhs@ != 0)]
517                #[requires(!(self@ == $type::MIN@ && rhs@ == -1))]
518                #[ensures(result@ == self@ $op rhs@)]
519                fn $divrem_method(self, rhs: $rhs) -> $type {
520                    self $op rhs
521                }
522            }
523        }
524    };
525    (@nz $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
526        extern_spec! {
527            impl $divrem_trait<NonZero<$rhs>> for $lhs {
528                // This has to be trusted because it's implemented by calling into an intrinsic
529                // that only has `Copy` bound which is not sufficient to specify the precondition.
530                #[requires(!(self@ == $type::MIN@ && rhs@ == -1))]
531                #[ensures(result@ == self@ $op rhs@)]
532                fn $divrem_method(self, rhs: NonZero<$rhs>) -> $type;
533            }
534        }
535    };
536    (@assign $divrem_assign_trait:ident, $divrem_assign_method:ident, $op_assign:tt, $op:tt, $type:ty) => {
537        spec_div_rem!{@assign $divrem_assign_trait, $divrem_assign_method, $op_assign, $op, $type, $type}
538        spec_div_rem!{@assign $divrem_assign_trait, $divrem_assign_method, $op_assign, $op, $type, &$type}
539    };
540    (@assign $divrem_assign_trait:ident, $divrem_assign_method:ident, $op_assign:tt, $op:tt, $type:ty, $rhs:ty) => {
541        extern_spec! {
542            impl $divrem_assign_trait<$rhs> for $type {
543                #[requires(rhs@ != 0)]
544                #[requires(!(*self == $type::MIN && rhs@ == -1))]
545                #[ensures((^self)@ == self@ $op rhs@)]
546                fn $divrem_assign_method(&mut self, rhs: $rhs) {
547                    *self $op_assign rhs
548                }
549            }
550        }
551    };
552}
553
554macro_rules! spec_bits {
555    ($type:ty) => {
556        spec_bits! {$type, &, BitAnd, bitand, BitAndAssign, bitand_assign}
557        spec_bits! {$type, |, BitOr, bitor, BitOrAssign, bitor_assign}
558        spec_bits! {$type, ^, BitXor, bitxor, BitXorAssign, bitxor_assign}
559    };
560    ($type:ty, $op:tt, $tr:ident, $f:ident, $tr_assign:ident, $f_assign: ident) => {
561        extern_spec! {
562            impl $tr for $type {
563                #[check(ghost)]
564                #[ensures(result == self $op rhs)]
565                fn $f(self, rhs: $type) -> $type {
566                    self $op rhs
567                }
568            }
569
570            impl $tr for &$type {
571                #[check(ghost)]
572                #[ensures(result == *self $op *rhs)]
573                fn $f(self, rhs: &$type) -> $type {
574                    *self $op *rhs
575                }
576            }
577
578            impl $tr<&$type> for $type {
579                #[check(ghost)]
580                #[ensures(result == self $op *rhs)]
581                fn $f(self, rhs: &$type) -> $type {
582                    self $op *rhs
583                }
584            }
585
586            impl $tr<$type> for &$type {
587                #[check(ghost)]
588                #[ensures(result == *self $op rhs)]
589                fn $f(self, rhs: $type) -> $type {
590                    *self $op rhs
591                }
592            }
593
594            impl $tr_assign for $type {
595                #[check(ghost)]
596                #[ensures(^self == *self $op rhs)]
597                fn $f_assign(&mut self, rhs: $type) {
598                    *self = *self $op rhs
599                }
600            }
601
602            impl $tr_assign<&$type> for $type {
603                #[check(ghost)]
604                #[ensures(^self == *self $op *rhs)]
605                fn $f_assign(&mut self, rhs: &$type) {
606                    *self = *self $op *rhs
607                }
608            }
609        }
610    };
611}
612
613macro_rules! spec_shifts {
614    ($type:ty) => {
615        spec_shifts! {$type, u8 u16 u32 u64 u128 usize i8 i16 i32 i64 i128 isize}
616    };
617    ($type:ty, $($rhs:ty)*) => {
618        $(spec_shifts! {$type, $rhs, >>, Shr, shr, ShrAssign, shr_assign})*
619        $(spec_shifts! {$type, $rhs, <<, Shl, shl, ShlAssign, shl_assign})*
620    };
621    ($type:ty, $rhs:ty, $op:tt, $tr:ident, $f:ident, $tr_assign:ident, $f_assign:ident) => {
622        extern_spec! {
623            impl $tr<$rhs> for $type {
624                #[requires((0usize as $rhs) <= rhs && rhs <= ($type::BITS - 1u32) as $rhs)]
625                #[ensures(result == self $op rhs)]
626                fn $f(self, rhs: $rhs) -> $type {
627                    self $op rhs
628                }
629            }
630
631            impl $tr<&$rhs> for $type {
632                #[requires((0usize as $rhs) <= *rhs && *rhs <= ($type::BITS - 1u32) as $rhs)]
633                #[ensures(result == self $op *rhs)]
634                fn $f(self, rhs: &$rhs) -> $type {
635                    self $op *rhs
636                }
637            }
638
639            impl $tr<$rhs> for &$type {
640                #[requires((0usize as $rhs) <= rhs && rhs <= ($type::BITS - 1u32) as $rhs)]
641                #[ensures(result == *self $op rhs)]
642                fn $f(self, rhs: $rhs) -> $type {
643                    *self $op rhs
644                }
645            }
646
647            impl $tr<&$rhs> for &$type {
648                #[requires((0usize as $rhs) <= *rhs && *rhs <= ($type::BITS - 1u32) as $rhs)]
649                #[ensures(result == *self $op *rhs)]
650                fn $f(self, rhs: &$rhs) -> $type {
651                    *self $op *rhs
652                }
653            }
654
655            impl $tr_assign<$rhs> for $type {
656                #[requires((0usize as $rhs) <= rhs && rhs <= ($type::BITS - 1u32) as $rhs)]
657                #[ensures(^self == *self $op rhs)]
658                fn $f_assign(&mut self, rhs: $rhs) {
659                    *self = *self $op rhs
660                }
661            }
662
663            impl $tr_assign<&$rhs> for $type {
664                #[requires((0usize as $rhs) <= *rhs && *rhs <= ($type::BITS - 1u32) as $rhs)]
665                #[ensures(^self == *self $op *rhs)]
666                fn $f_assign(&mut self, rhs: &$rhs) {
667                    *self = *self $op *rhs
668                }
669            }
670        }
671    };
672}
673
674/// Adds specifications for the abs_diff operation on the given pair of signed
675/// and unsigned integer types
676macro_rules! spec_abs_diff {
677    ($unsigned:ty, $signed:ty) => {
678        extern_spec! {
679            impl $unsigned {
680                #[allow(dead_code)]
681                #[check(ghost)]
682                #[ensures(result@ == self@.abs_diff(other@))]
683                fn abs_diff(self, other: $unsigned) -> $unsigned;
684            }
685
686            impl $signed {
687                #[allow(dead_code)]
688                #[check(ghost)]
689                #[ensures(result@ == self@.abs_diff(other@))]
690                fn abs_diff(self, other: $signed) -> $unsigned;
691
692                #[allow(dead_code)]
693                #[check(ghost)]
694                #[ensures(result == (self@ > 0))]
695                fn is_positive(self) -> bool;
696
697                #[allow(dead_code)]
698                #[check(ghost)]
699                #[ensures(result == (self@ < 0))]
700                fn is_negative(self) -> bool;
701
702                #[allow(dead_code)]
703                #[check(ghost)]
704                #[ensures(self@ >= 0 ==> result@ == self@)]
705                #[ensures(self@ < 0 ==> result@ == -self@)]
706                fn unsigned_abs(self) -> $unsigned;
707
708                #[allow(dead_code)]
709                #[check(ghost)]
710                #[ensures(self@ > 0 ==> result@ == 1)]
711                #[ensures(self@ == 0 ==> result@ == 0)]
712                #[ensures(self@ < 0 ==> result@ == -1)]
713                fn signum(self) -> Self;
714
715                #[allow(dead_code)]
716                #[check(ghost)]
717                #[requires(self@ != Self::MIN@)]
718                #[ensures(self@ >= 0 ==> result@ == self@)]
719                #[ensures(self@ < 0 ==> result@ == -self@)]
720                fn abs(self) -> Self;
721            }
722
723            impl TryFrom<$signed> for $unsigned {
724                #[check(ghost)]
725                #[ensures(match result { Ok(val) => val@ == value@, Err(_) => value@ < 0 })]
726                fn try_from(value: $signed) -> Result<Self, core::num::TryFromIntError>;
727            }
728
729            impl TryFrom<$unsigned> for $signed {
730                #[check(ghost)]
731                #[ensures(match result { Ok(val) => val@ == value@, Err(_) => value@ > Self::MAX@ })]
732                fn try_from(value: $unsigned) -> Result<Self, core::num::TryFromIntError>;
733            }
734        }
735    };
736}
737
738spec_bits!(bool);
739
740spec_unsigned!(u8, 0u8, 1u8);
741spec_unsigned!(u16, 0u16, 1u16);
742spec_unsigned!(u32, 0u32, 1u32);
743spec_unsigned!(u64, 0u64, 1u64);
744spec_unsigned!(u128, 0u128, 1u128);
745spec_unsigned!(usize, 0usize, 1usize);
746
747spec_type!(i8);
748spec_type!(i16);
749spec_type!(i32);
750spec_type!(i64);
751spec_type!(i128);
752spec_type!(isize);
753
754spec_abs_diff!(u8, i8);
755spec_abs_diff!(u16, i16);
756spec_abs_diff!(u32, i32);
757spec_abs_diff!(u64, i64);
758spec_abs_diff!(u128, i128);
759spec_abs_diff!(usize, isize);
760
761macro_rules! spec_shifts_logic {
762    ($lhs:ty | $rhs:ty) => {
763        impl ShlLogic<$rhs> for $lhs {
764            type Output = $lhs;
765
766            #[logic(open, inline)]
767            fn shl_logic(self, rhs: $rhs) -> $lhs {
768                self << rhs as $lhs
769            }
770        }
771
772        impl ShrLogic<$rhs> for $lhs {
773            type Output = $lhs;
774
775            #[logic(open, inline)]
776            fn shr_logic(self, rhs: $rhs) -> $lhs {
777                self >> rhs as $lhs
778            }
779        }
780    };
781    ($($prev:ty,)* | $cur:ty | ) => { $(spec_shifts_logic!($cur | $prev);)* };
782    ($($prev:ty,)* | $cur:ty | $nexth:ty, $($nextq:ty,)*) => {
783        $(spec_shifts_logic!($cur | $prev);)*
784        spec_shifts_logic!($cur | $nexth);
785        $(spec_shifts_logic!($cur | $nextq);)*
786
787        spec_shifts_logic!($($prev,)* $cur, | $nexth | $($nextq,)*);
788    };
789}
790
791spec_shifts_logic!(|u8| u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize,);
792
793#[cfg(creusot)]
794use core::num::{NonZero, ZeroablePrimitive};
795
796#[cfg(creusot)]
797impl<T: ZeroablePrimitive + View> View for NonZero<T> {
798    type ViewTy = T::ViewTy;
799    #[logic(open, inline)]
800    fn view(self) -> Self::ViewTy {
801        self.get_logic().view()
802    }
803}
804
805#[cfg(creusot)]
806impl<T: ZeroablePrimitive + DeepModel> DeepModel for NonZero<T> {
807    type DeepModelTy = T::DeepModelTy;
808    #[logic(open, inline)]
809    fn deep_model(self) -> Self::DeepModelTy {
810        self.get_logic().deep_model()
811    }
812}
813
814#[cfg(creusot)]
815impl<T: ZeroablePrimitive + Plain + View<ViewTy = Int>> Plain for NonZero<T> {
816    #[requires(inv(*snap))]
817    #[ensures(*result == *snap)]
818    #[check(ghost)]
819    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
820        ghost! {
821            unsafe { Self::new_unchecked(*snapshot!(snap.get_logic()).into_ghost()) }
822        }
823    }
824}
825
826#[cfg(creusot)]
827impl<T: ZeroablePrimitive + View<ViewTy = Int>> Invariant for NonZero<T> {
828    #[logic(open, prophetic)]
829    fn invariant(self) -> bool {
830        pearlite! {
831            self@ != 0 &&
832            inv(self.get_logic()) // This is always trivially true, but needed to prove into_ghost generically.
833        }
834    }
835}
836
837#[cfg(creusot)]
838pub trait NonZeroExt {
839    type Inner;
840
841    #[logic]
842    fn get_logic(self) -> Self::Inner;
843}
844
845#[cfg(creusot)]
846impl<T: ZeroablePrimitive> NonZeroExt for NonZero<T> {
847    type Inner = T;
848
849    #[builtin("identity")]
850    #[logic]
851    fn get_logic(self) -> Self::Inner {
852        dead
853    }
854}
855
856#[cfg(creusot)]
857extern_spec! {
858    impl<T: ZeroablePrimitive> NonZero<T> {
859        #[ensures(result == self.get_logic())]
860        #[check(ghost)]
861        fn get(self) -> T;
862    }
863
864    impl<T: ZeroablePrimitive + View<ViewTy = Int>> NonZero<T> {
865        #[ensures(match result {
866            None => n@ == 0,
867            Some(nz) => n@ != 0 && nz.get_logic() == n,
868        })]
869        #[check(ghost)]
870        fn new(n: T) -> Option<Self>;
871
872        #[requires(n@ != 0)]
873        #[ensures(result.get_logic() == n)]
874        #[check(ghost)]
875        unsafe fn new_unchecked(n: T) -> Self;
876    }
877}
878
879impl<T: DeepModel> DeepModel for Wrapping<T> {
880    type DeepModelTy = Wrapping<T::DeepModelTy>;
881
882    #[logic(open, inline)]
883    fn deep_model(self) -> Self::DeepModelTy {
884        pearlite! { Wrapping(self.0.deep_model()) }
885    }
886}
887
888macro_rules! spec_wrapping {
889    ($($type:ty)*) => {$(
890        extern_spec! {
891            impl Add<Wrapping<$type>> for Wrapping<$type> {
892                #[check(ghost)]
893                #[ensures(result.0 == self.0 + rhs.0)]
894                fn add(self, rhs: Wrapping<$type>) -> Wrapping<$type> {
895                    Wrapping(self.0.wrapping_add(rhs.0))
896                }
897            }
898
899            impl Sub<Wrapping<$type>> for Wrapping<$type> {
900                #[ensures(result.0 == self.0 - rhs.0)]
901                fn sub(self, rhs: Wrapping<$type>) -> Wrapping<$type> {
902                    Wrapping(self.0.wrapping_sub(rhs.0))
903                }
904            }
905
906            impl Mul<Wrapping<$type>> for Wrapping<$type> {
907                #[ensures(result.0 == self.0 * rhs.0)]
908                fn mul(self, rhs: Wrapping<$type>) -> Wrapping<$type> {
909                    Wrapping(self.0.wrapping_mul(rhs.0))
910                }
911            }
912
913            impl Neg for Wrapping<$type> {
914                #[check(ghost)]
915                #[ensures(result.0 == -self.0)]
916                fn neg(self) -> Wrapping<$type> {
917                    Wrapping(self.0.wrapping_neg())
918                }
919            }
920        }
921    )*};
922}
923
924spec_wrapping!(u8 u16 u32 u64 u128 usize i8 i16 i32 i64 i128 isize);
925
926impl DeepModel for core::num::ParseIntError {
927    type DeepModelTy = Self;
928
929    #[logic(open, inline)]
930    fn deep_model(self) -> Self::DeepModelTy {
931        self
932    }
933}
creusot_std/std/num.rs

creusot_std/std/
num.rs
