creusot_std/std/
num.rs

1use crate::{
2    ghost::Plain,
3    logic::ops::{AddLogic, MulLogic, NegLogic, NthBitLogic, SubLogic},
4    prelude::*,
5};
6
7macro_rules! mach_int {
8    ($t:ty, $ty_nm:expr, $zero:expr, $to_int:literal) => {
9        impl View for $t {
10            type ViewTy = Int;
11            #[logic]
12            #[builtin(concat!($ty_nm, $to_int))]
13            fn view(self) -> Self::ViewTy {
14                dead
15            }
16        }
17
18        impl DeepModel for $t {
19            type DeepModelTy = Int;
20            #[logic(open, inline)]
21            fn deep_model(self) -> Self::DeepModelTy {
22                pearlite! { self@ }
23            }
24        }
25
26        #[trusted]
27        impl Plain for $t {}
28
29        extern_spec! {
30            impl Default for $t {
31                #[check(ghost)]
32                #[ensures(result == $zero)]
33                fn default() -> $t { 0 }
34            }
35
36            impl Clone for $t {
37                #[check(ghost)]
38                #[ensures(result == *self)]
39                fn clone(&self) -> $t {
40                    *self
41                }
42            }
43        }
44
45        impl AddLogic for $t {
46            type Output = Self;
47            #[logic]
48            #[builtin(concat!($ty_nm, ".add"))]
49            #[allow(unused_variables)]
50            fn add(self, other: Self) -> Self {
51                dead
52            }
53        }
54
55        impl SubLogic for $t {
56            type Output = Self;
57            #[logic]
58            #[builtin(concat!($ty_nm, ".sub"))]
59            #[allow(unused_variables)]
60            fn sub(self, other: Self) -> Self {
61                dead
62            }
63        }
64
65        impl MulLogic for $t {
66            type Output = Self;
67            #[logic]
68            #[builtin(concat!($ty_nm, ".mul"))]
69            #[allow(unused_variables)]
70            fn mul(self, other: Self) -> Self {
71                dead
72            }
73        }
74
75        impl NegLogic for $t {
76            type Output = Self;
77            #[logic]
78            #[builtin(concat!($ty_nm, ".neg"))]
79            fn neg(self) -> Self {
80                dead
81            }
82        }
83
84        impl NthBitLogic for $t {
85            #[logic]
86            #[builtin(concat!($ty_nm, ".nth"))]
87            #[allow(unused_variables)]
88            fn nth_bit(self, n: Int) -> bool {
89                dead
90            }
91        }
92    };
93}
94
95mach_int!(u8, "creusot.int.UInt8$BW$", 0u8, ".t'int");
96mach_int!(u16, "creusot.int.UInt16$BW$", 0u16, ".t'int");
97mach_int!(u32, "creusot.int.UInt32$BW$", 0u32, ".t'int");
98mach_int!(u64, "creusot.int.UInt64$BW$", 0u64, ".t'int");
99mach_int!(u128, "creusot.int.UInt128$BW$", 0u128, ".t'int");
100#[cfg(target_pointer_width = "64")]
101mach_int!(usize, "creusot.int.UInt64$BW$", 0usize, ".t'int");
102#[cfg(target_pointer_width = "32")]
103mach_int!(usize, "creusot.int.UInt32$BW$", 0usize, ".t'int");
104#[cfg(target_pointer_width = "16")]
105mach_int!(usize, "creusot.int.UInt16$BW$", 0usize, ".t'int");
106
107mach_int!(i8, "creusot.int.Int8$BW$", 0i8, ".to_int");
108mach_int!(i16, "creusot.int.Int16$BW$", 0i16, ".to_int");
109mach_int!(i32, "creusot.int.Int32$BW$", 0i32, ".to_int");
110mach_int!(i64, "creusot.int.Int64$BW$", 0i64, ".to_int");
111mach_int!(i128, "creusot.int.Int128$BW$", 0i128, ".to_int");
112#[cfg(target_pointer_width = "64")]
113mach_int!(isize, "creusot.int.Int64$BW$", 0isize, ".to_int");
114#[cfg(target_pointer_width = "32")]
115mach_int!(isize, "creusot.int.Int32$BW$", 0isize, ".to_int");
116#[cfg(target_pointer_width = "16")]
117mach_int!(isize, "creusot.int.Int16$BW$", 0isize, ".to_int");
118
119/// Adds specifications for checked, wrapping, saturating, and overflowing operations on the given
120/// integer type
121macro_rules! spec_type {
122    ($type:ty) => {
123        // Specify addition, subtraction and multiplication
124        spec_op_common!($type, +, checked_add, wrapping_add, saturating_add, overflowing_add, unchecked_add);
125        spec_op_common!($type, -, checked_sub, wrapping_sub, saturating_sub, overflowing_sub, unchecked_sub);
126        spec_op_common!($type, *, checked_mul, wrapping_mul, saturating_mul, overflowing_mul, unchecked_mul);
127
128        extern_spec! {
129            impl $type {
130                #[allow(dead_code)]
131                #[check(ghost)]
132                #[ensures(result == -self)]
133                fn wrapping_neg(self) -> $type;
134            }
135        }
136
137        // Specify division separately, because it has the additional precondition that the divisor
138        // is non-zero. Overflow on division can only occur on signed types and only when computing
139        // `$type::MIN / -1`.
140        extern_spec! {
141            impl $type {
142                #[allow(dead_code)]
143                #[check(ghost)]
144                // Returns `None` iff the divisor is zero or the division overflows
145                #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
146                // Else, returns the result of the division
147                #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@)]
148                fn checked_div(self, rhs: $type) -> Option<$type>;
149
150                #[allow(dead_code)]
151                #[check(ghost)]
152                // Panics if the divisor is zero
153                #[requires(rhs@ != 0)]
154                // Returns `self` if the division overflows
155                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == self@)]
156                // Else, returns the result of the division
157                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
158                fn wrapping_div(self, rhs: $type) -> $type;
159
160                #[allow(dead_code)]
161                #[check(ghost)]
162                // Panics if the divisor is zero
163                #[requires(rhs@ != 0)]
164                // Returns `$type::MIN` if the division overflows
165                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == $type::MIN@)]
166                // Else, returns the result of the division
167                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
168                fn saturating_div(self, rhs: $type) -> $type;
169
170                #[allow(dead_code)]
171                #[check(ghost)]
172                // Panics if the divisor is zero
173                #[requires(rhs@ != 0)]
174                // Returns `self` if the division overflows
175                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result.0@ == self@)]
176                // Else, returns the result of the division
177                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result.0@ == self@ / rhs@)]
178                // Overflow only occurs when computing `$type::MIN / -1`
179                #[ensures(result.1 == (self@ == $type::MIN@ && rhs@ == -1))]
180                fn overflowing_div(self, rhs: $type) -> ($type, bool);
181            }
182        }
183    };
184}
185
186macro_rules! spec_unsized {
187    ($type:ty, $zero:expr, $one:expr) => {
188        spec_type!($type);
189
190        extern_spec! {
191            impl $type {
192                    #[check(ghost)]
193                    #[ensures(if self == $zero { result == (self == $zero) } else { result == (self@ % rhs@ == 0) })]
194                    fn is_multiple_of(self, rhs: Self) -> bool;
195
196                    #[check(ghost)]
197                    #[ensures(result == (self != $zero && self & (self - $one) == $zero))]
198                    fn is_power_of_two(self) -> bool;
199            }
200        }
201    };
202}
203
204/// Adds specifications for checked, wrapping, saturating, and overflowing versions of the given
205/// operation on the given type. This only works for operations that have no additional pre- or
206/// postconditions.
207macro_rules! spec_op_common {
208    (
209        $type:ty,
210        $op:tt,
211        $checked:ident,
212        $wrapping:ident,
213        $saturating:ident,
214        $overflowing:ident,
215        $unchecked:ident
216    ) => {
217        extern_spec! {
218            impl $type {
219                // Checked: performs the operation on `Int`, returns `Some` if the result is between
220                // `$type::MIN` and `$type::MAX`, or `None` if the result cannot be represented by
221                // `$type`
222                #[allow(dead_code)]
223                #[check(ghost)]
224                // Returns `None` iff the result is out of range
225                #[ensures(
226                    (result == None)
227                    == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
228                )]
229                // Returns `Some(result)` if the result is in range
230                #[ensures(forall<r: $type> result == Some(r) ==> r@ == (self@ $op rhs@))]
231                fn $checked(self, rhs: $type) -> Option<$type>;
232
233                // Wrapping: performs the operation on `Int` and converts back to `$type`
234                #[allow(dead_code)]
235                #[check(ghost)]
236                #[ensures(result == self $op rhs)]
237                fn $wrapping(self, rhs: $type) -> $type;
238
239                // Saturating: performs the operation on `Int` and clamps the result between
240                // `$type::MIN` and `$type::MAX`
241                #[allow(dead_code)]
242                #[check(ghost)]
243                // Returns the result if it is in range
244                #[ensures(
245                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
246                    ==> result@ == (self@ $op rhs@)
247                )]
248                // Returns the nearest bound if the result is out of range
249                #[ensures((self@ $op rhs@) < $type::MIN@ ==> result@ == $type::MIN@)]
250                #[ensures((self@ $op rhs@) > $type::MAX@ ==> result@ == $type::MAX@)]
251                fn $saturating(self, rhs: $type) -> $type;
252
253                // Overflowing: performs the operation on `Int` and converts back to `$type`, and
254                // indicates whether an overflow occurred
255                #[allow(dead_code)]
256                #[check(ghost)]
257                // Returns the result if it is in range
258                #[ensures(
259                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
260                    ==> result.0@ == (self@ $op rhs@)
261                )]
262                // Returns the result shifted by a multiple of the type's range if it is out of
263                // range. For addition and subtraction, `k` (qualified over below) will always be 1
264                // or -1, but the verifier is able to deduce that.
265                #[ensures(
266                    exists<k: Int> result.0@ == (self@ $op rhs@) + k * ($type::MAX@ - $type::MIN@ + 1)
267                )]
268                // Overflow occurred iff the result is out of range
269                #[ensures(
270                    result.1 == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
271                )]
272                fn $overflowing(self, rhs: $type) -> ($type, bool);
273
274                #[check(ghost)]
275                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
276                #[ensures(result@ == self@ $op rhs@)]
277                unsafe fn $unchecked(self, rhs: $type) -> $type;
278            }
279        }
280    };
281}
282
283/// Adds specifications for the abs_diff operation on the given pair of signed
284/// and unsigned integer types
285macro_rules! spec_abs_diff {
286    ($unsigned:ty, $signed:ty) => {
287        extern_spec! {
288            impl $unsigned {
289                #[allow(dead_code)]
290                #[check(ghost)]
291                #[ensures(result@ == self@.abs_diff(other@))]
292                fn abs_diff(self, other: $unsigned) -> $unsigned;
293            }
294
295            impl $signed {
296                #[allow(dead_code)]
297                #[check(ghost)]
298                #[ensures(result@ == self@.abs_diff(other@))]
299                fn abs_diff(self, other: $signed) -> $unsigned;
300            }
301        }
302    };
303}
304
305spec_unsized!(u8, 0u8, 1u8);
306spec_unsized!(u16, 0u16, 1u16);
307spec_unsized!(u32, 0u32, 1u32);
308spec_unsized!(u64, 0u64, 1u64);
309spec_unsized!(u128, 0u128, 1u128);
310spec_unsized!(usize, 0usize, 1usize);
311
312spec_type!(i8);
313spec_type!(i16);
314spec_type!(i32);
315spec_type!(i64);
316spec_type!(i128);
317spec_type!(isize);
318
319spec_abs_diff!(u8, i8);
320spec_abs_diff!(u16, i16);
321spec_abs_diff!(u32, i32);
322spec_abs_diff!(u64, i64);
323spec_abs_diff!(u128, i128);
324spec_abs_diff!(usize, isize);
creusot_std/std/num.rs

creusot_std/std/
num.rs
