creusot_std/std/
num.rs

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

creusot_std/std/
num.rs
