creusot_contracts/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                    //     match rhs {
197                    //         0 => self == 0,
198                    //         _ => self % rhs == 0,
199                    //     }
200                    // }
201
202                    #[check(ghost)]
203                    #[ensures(result == (self != $zero && self & (self - $one) == $zero))]
204                    fn is_power_of_two(self) -> bool;
205            }
206        }
207    };
208}
209
210/// Adds specifications for checked, wrapping, saturating, and overflowing versions of the given
211/// operation on the given type. This only works for operations that have no additional pre- or
212/// postconditions.
213macro_rules! spec_op_common {
214    (
215        $type:ty,
216        $op:tt,
217        $checked:ident,
218        $wrapping:ident,
219        $saturating:ident,
220        $overflowing:ident,
221        $unchecked:ident
222    ) => {
223        extern_spec! {
224            impl $type {
225                // Checked: performs the operation on `Int`, returns `Some` if the result is between
226                // `$type::MIN` and `$type::MAX`, or `None` if the result cannot be represented by
227                // `$type`
228                #[allow(dead_code)]
229                #[check(ghost)]
230                // Returns `None` iff the result is out of range
231                #[ensures(
232                    (result == None)
233                    == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
234                )]
235                // Returns `Some(result)` if the result is in range
236                #[ensures(forall<r: $type> result == Some(r) ==> r@ == (self@ $op rhs@))]
237                fn $checked(self, rhs: $type) -> Option<$type>;
238
239                // Wrapping: performs the operation on `Int` and converts back to `$type`
240                #[allow(dead_code)]
241                #[check(ghost)]
242                #[ensures(result == self $op rhs)]
243                fn $wrapping(self, rhs: $type) -> $type;
244
245                // Saturating: performs the operation on `Int` and clamps the result between
246                // `$type::MIN` and `$type::MAX`
247                #[allow(dead_code)]
248                #[check(ghost)]
249                // Returns the result if it is in range
250                #[ensures(
251                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
252                    ==> result@ == (self@ $op rhs@)
253                )]
254                // Returns the nearest bound if the result is out of range
255                #[ensures((self@ $op rhs@) < $type::MIN@ ==> result@ == $type::MIN@)]
256                #[ensures((self@ $op rhs@) > $type::MAX@ ==> result@ == $type::MAX@)]
257                fn $saturating(self, rhs: $type) -> $type;
258
259                // Overflowing: performs the operation on `Int` and converts back to `$type`, and
260                // indicates whether an overflow occurred
261                #[allow(dead_code)]
262                #[check(ghost)]
263                // Returns the result if it is in range
264                #[ensures(
265                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
266                    ==> result.0@ == (self@ $op rhs@)
267                )]
268                // Returns the result shifted by a multiple of the type's range if it is out of
269                // range. For addition and subtraction, `k` (qualified over below) will always be 1
270                // or -1, but the verifier is able to deduce that.
271                #[ensures(
272                    exists<k: Int> result.0@ == (self@ $op rhs@) + k * ($type::MAX@ - $type::MIN@ + 1)
273                )]
274                // Overflow occurred iff the result is out of range
275                #[ensures(
276                    result.1 == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
277                )]
278                fn $overflowing(self, rhs: $type) -> ($type, bool);
279
280                #[check(ghost)]
281                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
282                #[ensures(result@ == self@ $op rhs@)]
283                unsafe fn $unchecked(self, rhs: $type) -> $type;
284            }
285        }
286    };
287}
288
289/// Adds specifications for the abs_diff operation on the given pair of signed
290/// and unsigned integer types
291macro_rules! spec_abs_diff {
292    ($unsigned:ty, $signed:ty) => {
293        extern_spec! {
294            impl $unsigned {
295                #[allow(dead_code)]
296                #[check(ghost)]
297                #[ensures(result@ == self@.abs_diff(other@))]
298                fn abs_diff(self, other: $unsigned) -> $unsigned;
299            }
300
301            impl $signed {
302                #[allow(dead_code)]
303                #[check(ghost)]
304                #[ensures(result@ == self@.abs_diff(other@))]
305                fn abs_diff(self, other: $signed) -> $unsigned;
306            }
307        }
308    };
309}
310
311spec_unsized!(u8, 0u8, 1u8);
312spec_unsized!(u16, 0u16, 1u16);
313spec_unsized!(u32, 0u32, 1u32);
314spec_unsized!(u64, 0u64, 1u64);
315spec_unsized!(u128, 0u128, 1u128);
316spec_unsized!(usize, 0usize, 1usize);
317
318spec_type!(i8);
319spec_type!(i16);
320spec_type!(i32);
321spec_type!(i64);
322spec_type!(i128);
323spec_type!(isize);
324
325spec_abs_diff!(u8, i8);
326spec_abs_diff!(u16, i16);
327spec_abs_diff!(u32, i32);
328spec_abs_diff!(u64, i64);
329spec_abs_diff!(u128, i128);
330spec_abs_diff!(usize, isize);
creusot_contracts/std/num.rs

creusot_contracts/std/
num.rs
