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

creusot_std/std/
num.rs
