vstd/contrib/exec_spec/
arith.rs

1//! This module contains exec implementations of the fixed-width arithmetic
2//! builtins `add`, `sub`, and `mul`.
3//!
4//! Unlike `a + b` (which has type `int` in spec code), `add(a, b)` stays in
5//! the operand type and wraps on overflow, so it has a direct exec
6//! counterpart. The macros rename a call `add(a, b)` to `exec_add(a, b)`,
7//! which resolves to the [`exec_add`] defined here. For example,
8//!
9//! ```rust
10//! exec_spec_verified! {
11//!     spec fn add_u8(a: u8, b: u8) -> u8 {
12//!         add(a, b)
13//!     }
14//! }
15//! ```
16//!
17//! generates (simplified)
18//!
19//! ```rust
20//! fn exec_add_u8(a: u8, b: u8) -> (res: u8)
21//!     ensures res == add_u8(a, b)
22//! {
23//!     exec_add(a, b)
24//! }
25//! ```
26//!
27//! where `exec_add_u8(200, 100) == 44`. Each operation is computed in
28//! `u128`/`i128` (which cannot overflow for operands of at most 64 bits) and
29//! then truncated back to the operand type.
30use crate::contrib::exec_spec::*;
31use crate::prelude::*;
32
33#[cfg(verus_keep_ghost)]
34macro_rules! truncating_cast {
35    ($e:expr, $t:ty) => {
36        #[verifier::truncate]
37        ($e as $t)
38    };
39}
40
41#[cfg(not(verus_keep_ghost))]
42macro_rules! truncating_cast {
43    ($e:expr, $t:ty) => {
44        ($e as $t)
45    };
46}
47
48verus! {
49
50pub trait ExecSpecFixedWidthArith: Sized {
51    spec fn spec_fixed_add(self, rhs: Self) -> Self;
52
53    spec fn spec_fixed_sub(self, rhs: Self) -> Self;
54
55    spec fn spec_fixed_mul(self, rhs: Self) -> Self;
56
57    fn exec_fixed_add(self, rhs: Self) -> (res: Self)
58        ensures
59            res == self.spec_fixed_add(rhs),
60    ;
61
62    fn exec_fixed_sub(self, rhs: Self) -> (res: Self)
63        ensures
64            res == self.spec_fixed_sub(rhs),
65    ;
66
67    fn exec_fixed_mul(self, rhs: Self) -> (res: Self)
68        ensures
69            res == self.spec_fixed_mul(rhs),
70    ;
71}
72
73macro_rules! impl_unsigned_fixed_width_arith {
74    ($($t:ty),*) => {
75        $(
76            verus! {
77                impl ExecSpecFixedWidthArith for $t {
78                    open spec fn spec_fixed_add(self, rhs: $t) -> $t {
79                        add(self, rhs)
80                    }
81
82                    open spec fn spec_fixed_sub(self, rhs: $t) -> $t {
83                        sub(self, rhs)
84                    }
85
86                    open spec fn spec_fixed_mul(self, rhs: $t) -> $t {
87                        mul(self, rhs)
88                    }
89
90                    #[inline(always)]
91                    fn exec_fixed_add(self, rhs: $t) -> (res: $t) {
92                        truncating_cast!(self as u128 + rhs as u128, $t)
93                    }
94
95                    #[inline(always)]
96                    fn exec_fixed_sub(self, rhs: $t) -> (res: $t) {
97                        truncating_cast!(self as i128 - rhs as i128, $t)
98                    }
99
100                    #[inline(always)]
101                    fn exec_fixed_mul(self, rhs: $t) -> (res: $t) {
102                        assert((self as int) * (rhs as int) <= (u64::MAX as int) * (u64::MAX as int))
103                            by (nonlinear_arith)
104                            requires
105                                0 <= self <= u64::MAX,
106                                0 <= rhs <= u64::MAX,
107                        ;
108                        truncating_cast!(self as u128 * rhs as u128, $t)
109                    }
110                }
111            }
112        )*
113    };
114}
115
116macro_rules! impl_signed_fixed_width_arith {
117    ($($t:ty),*) => {
118        $(
119            verus! {
120                impl ExecSpecFixedWidthArith for $t {
121                    open spec fn spec_fixed_add(self, rhs: $t) -> $t {
122                        add(self, rhs)
123                    }
124
125                    open spec fn spec_fixed_sub(self, rhs: $t) -> $t {
126                        sub(self, rhs)
127                    }
128
129                    open spec fn spec_fixed_mul(self, rhs: $t) -> $t {
130                        mul(self, rhs)
131                    }
132
133                    #[inline(always)]
134                    fn exec_fixed_add(self, rhs: $t) -> (res: $t) {
135                        truncating_cast!(self as i128 + rhs as i128, $t)
136                    }
137
138                    #[inline(always)]
139                    fn exec_fixed_sub(self, rhs: $t) -> (res: $t) {
140                        truncating_cast!(self as i128 - rhs as i128, $t)
141                    }
142
143                    #[inline(always)]
144                    fn exec_fixed_mul(self, rhs: $t) -> (res: $t) {
145                        assert(i64::MIN * i64::MIN >= (self as int) * (rhs as int) >= i64::MIN
146                            * i64::MAX) by (nonlinear_arith)
147                            requires
148                                i64::MIN <= self <= i64::MAX,
149                                i64::MIN <= rhs <= i64::MAX,
150                        ;
151                        truncating_cast!(self as i128 * rhs as i128, $t)
152                    }
153                }
154            }
155        )*
156    };
157}
158
159impl_unsigned_fixed_width_arith!(u8, u16, u32, u64, usize);
160
161impl_signed_fixed_width_arith!(i8, i16, i32, i64, isize);
162
163#[inline(always)]
164pub fn exec_add<T: ExecSpecFixedWidthArith>(a: T, b: T) -> (res: T)
165    ensures
166        res == a.spec_fixed_add(b),
167{
168    a.exec_fixed_add(b)
169}
170
171#[inline(always)]
172pub fn exec_sub<T: ExecSpecFixedWidthArith>(a: T, b: T) -> (res: T)
173    ensures
174        res == a.spec_fixed_sub(b),
175{
176    a.exec_fixed_sub(b)
177}
178
179#[inline(always)]
180pub fn exec_mul<T: ExecSpecFixedWidthArith>(a: T, b: T) -> (res: T)
181    ensures
182        res == a.spec_fixed_mul(b),
183{
184    a.exec_fixed_mul(b)
185}
186
187} // verus!
vstd/contrib/exec_spec/arith.rs

vstd/contrib/exec_spec/
arith.rs
