creusot_contracts/std/
num.rs

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

creusot_contracts/std/
num.rs
