vstd/std_specs/
ops.rs

1/// Defines the specifications for operator traits.
2///
3/// This file specifies the behavior of operator traits for integers when the trait method is invoked.
4/// Preconditions for some operator trait method are required to prevent overflow and underflow.
5///
6/// - For primitive integer types, the expression `lhs $op rhs` is directly handled by the verifier
7///   without relying on trait specifications defined here, avoiding additional trigger costs.
8///   However, calling `lhs.add(rhs)` or T::add(lhs, rhs) will trigger the corresponding trait method
9/// - If an operator is overloaded for a custom type, both `lhs $op rhs` and `lhs.add(rhs)` invoke the
10///   corresponding trait method for verification.
11///   and its preconditions are enforced.
12/// - Since this crate (vstd) defines the extension traits AddSpec, SubSpec, etc.,
13///   this crate is also allowed to implement these extension traits for known std types
14///   like u8, u16, etc.  Rust's coherence rules prevent other crates from implementing
15///   these extension traits for std types.  If this is a problem, as a last-resort workaround,
16///   other crates can assume axioms about the extension traits as an alternative to implementing
17///   them directly.
18use super::super::prelude::*;
19
20macro_rules! def_un_ops_spec {
21    ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident) => {
22        $crate::vstd::prelude::verus! {
23            #[verifier::external_trait_specification]
24            #[verifier::external_trait_extension($spec_trait via $impl_trait)]
25            pub trait $extrait {
26                type ExternalTraitSpecificationFor: $trait;
27
28                type Output;
29
30                spec fn $obeys() -> bool;
31
32                spec fn $req(self) -> bool
33                    where Self: Sized;
34
35                spec fn $spec(self) -> Self::Output
36                    where Self: Sized;
37
38                fn $fun(self) -> (ret: Self::Output)
39                    requires
40                        self.$req(),
41                    ensures
42                        Self::$obeys() ==> ret == self.$spec();
43            }
44        }
45};
46}
47
48macro_rules! def_bin_ops_spec {
49    ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident) => {
50        $crate::vstd::prelude::verus! {
51            #[verifier::external_trait_specification]
52            #[verifier::external_trait_extension($spec_trait via $impl_trait)]
53            pub trait $extrait<Rhs = Self> {
54                type ExternalTraitSpecificationFor: $trait<Rhs>;
55
56                type Output;
57
58                spec fn $obeys() -> bool;
59
60                spec fn $req(self, rhs: Rhs) -> bool
61                    where Self: Sized;
62
63                spec fn $spec(self, rhs: Rhs) -> Self::Output
64                    where Self: Sized;
65
66                fn $fun(self, rhs: Rhs) -> (ret: Self::Output)
67                    requires
68                        self.$req(rhs),
69                    ensures
70                        Self::$obeys() ==> ret == self.$spec(rhs);
71            }
72        }
73};
74}
75
76def_un_ops_spec!(
77    core::ops::Neg,
78    ExNeg,
79    NegSpec,
80    NegSpecImpl,
81    neg,
82    obeys_neg_spec,
83    neg_req,
84    neg_spec
85);
86
87def_un_ops_spec!(
88    core::ops::Not,
89    ExNot,
90    NotSpec,
91    NotSpecImpl,
92    not,
93    obeys_not_spec,
94    not_req,
95    not_spec
96);
97
98def_bin_ops_spec!(
99    core::ops::Add,
100    ExAdd,
101    AddSpec,
102    AddSpecImpl,
103    add,
104    obeys_add_spec,
105    add_req,
106    add_spec
107);
108
109def_bin_ops_spec!(
110    core::ops::Sub,
111    ExSub,
112    SubSpec,
113    SubSpecImpl,
114    sub,
115    obeys_sub_spec,
116    sub_req,
117    sub_spec
118);
119
120def_bin_ops_spec!(
121    core::ops::Mul,
122    ExMul,
123    MulSpec,
124    MulSpecImpl,
125    mul,
126    obeys_mul_spec,
127    mul_req,
128    mul_spec
129);
130
131def_bin_ops_spec!(
132    core::ops::Div,
133    ExDiv,
134    DivSpec,
135    DivSpecImpl,
136    div,
137    obeys_div_spec,
138    div_req,
139    div_spec
140);
141
142def_bin_ops_spec!(
143    core::ops::Rem,
144    ExRem,
145    RemSpec,
146    RemSpecImpl,
147    rem,
148    obeys_rem_spec,
149    rem_req,
150    rem_spec
151);
152
153def_bin_ops_spec!(
154    core::ops::BitAnd,
155    ExBitAnd,
156    BitAndSpec,
157    BitAndSpecImpl,
158    bitand,
159    obeys_bitand_spec,
160    bitand_req,
161    bitand_spec
162);
163
164def_bin_ops_spec!(
165    core::ops::BitOr,
166    ExBitOr,
167    BitOrSpec,
168    BitOrSpecImpl,
169    bitor,
170    obeys_bitor_spec,
171    bitor_req,
172    bitor_spec
173);
174
175def_bin_ops_spec!(
176    core::ops::BitXor,
177    ExBitXor,
178    BitXorSpec,
179    BitXorSpecImpl,
180    bitxor,
181    obeys_bitxor_spec,
182    bitxor_req,
183    bitxor_spec
184);
185
186def_bin_ops_spec!(
187    core::ops::Shl,
188    ExShl,
189    ShlSpec,
190    ShlSpecImpl,
191    shl,
192    obeys_shl_spec,
193    shl_req,
194    shl_spec
195);
196
197def_bin_ops_spec!(
198    core::ops::Shr,
199    ExShr,
200    ShrSpec,
201    ShrSpecImpl,
202    shr,
203    obeys_shr_spec,
204    shr_req,
205    shr_spec
206);
207
208macro_rules! def_uop_impls {
209    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, [$(($typ:ty, $req_expr:expr, $spec_expr:expr))*]) => {
210        $crate::vstd::prelude::verus! {
211            $(
212                impl $impl_trait for $typ {
213                    open spec fn $obeys() -> bool {
214                        true
215                    }
216
217                    open spec fn $req($self) -> bool {
218                        $req_expr
219                    }
220
221                    open spec fn $spec($self) -> Self::Output {
222                        $spec_expr
223                    }
224                }
225
226                pub assume_specification[ <$typ as $trait>::$fun ](x: $typ) -> $typ;
227            )*
228        }
229};
230}
231
232macro_rules! def_bop_impls {
233    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, [$(($typ:ty, $req_expr:expr, $spec_expr:expr))*]) => {
234        $crate::vstd::prelude::verus! {
235            $(
236                impl $impl_trait for $typ {
237                    open spec fn $obeys() -> bool {
238                        true
239                    }
240
241                    open spec fn $req($self, $rhs: $typ) -> bool {
242                        $req_expr
243                    }
244
245                    open spec fn $spec($self, $rhs: $typ) -> Self::Output {
246                        $spec_expr
247                    }
248                }
249
250                pub assume_specification[ <$typ as $trait>::$fun ](x: $typ, y: $typ) -> $typ;
251            )*
252        }
253};
254}
255
256macro_rules! def_uop_impls_no_check {
257    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $op:tt, [$($typ:ty)*]) => {
258        $crate::vstd::prelude::verus! {
259            def_uop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, [
260                $(
261                    (
262                        $typ,
263                        true,
264                        $op $self
265                    )
266                )*
267            ]);
268        }
269};
270}
271
272macro_rules! def_uop_impls_check_overflow {
273    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $op:tt, [$($typ:ty)*]) => {
274        $crate::vstd::prelude::verus! {
275            def_uop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, [
276                $(
277                    (
278                        $typ,
279                        ($op $self) as $typ == ($op $self),
280                        ($op $self) as $typ
281                    )
282                )*
283            ]);
284        }
285};
286}
287
288macro_rules! def_bop_impls_no_check {
289    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
290        $crate::vstd::prelude::verus! {
291            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
292                $(
293                    (
294                        $typ,
295                        true,
296                        $self $op $rhs
297                    )
298                )*
299            ]);
300        }
301};
302}
303
304macro_rules! def_bop_impls_check_overflow {
305    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
306        $crate::vstd::prelude::verus! {
307            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
308                $(
309                    (
310                        $typ,
311                        ($self $op $rhs) as $typ == ($self $op $rhs),
312                        ($self $op $rhs) as $typ
313                    )
314                )*
315            ]);
316        }
317};
318}
319
320macro_rules! def_bop_impls_unsigned_div_rem {
321    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
322        $crate::vstd::prelude::verus! {
323            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
324                $(
325                    (
326                        $typ,
327                        $rhs != 0,
328                        $self $op $rhs
329                    )
330                )*
331            ]);
332        }
333};
334}
335
336// Signed div/rem needs to:
337// - check for overflow (e.g. (-128i8) / (-1im))
338// - express truncating div, rem in terms of euclidean /, %
339macro_rules! def_bop_impls_signed_div_rem {
340    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
341        $crate::vstd::prelude::verus! {
342            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
343                $(
344                    (
345                        $typ,
346                        $rhs != 0 && !($self == $typ::MIN && $rhs == -1),
347                        if $self >= 0 {
348                            ($self $op $rhs) as $typ
349                        } else {
350                            (-((-$self) $op ($rhs as int))) as $typ
351                        }
352                    )
353                )*
354            ]);
355        }
356};
357}
358
359// TODO: there are many more combinations of primitive integer types supported by Shl and Shr,
360// such as (Self = u8, Rhs = u64)
361macro_rules! def_bop_impls_shift {
362    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
363        $crate::vstd::prelude::verus! {
364            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
365                $(
366                    (
367                        $typ,
368                        $rhs < $typ::BITS,
369                        $self $op $rhs
370                    )
371                )*
372            ]);
373        }
374};
375}
376
377def_uop_impls_check_overflow!(core::ops::Neg, NegSpecImpl, neg, obeys_neg_spec, neg_req, neg_spec, self, -, [
378    isize i8 i16 i32 i64 i128
379]);
380
381def_uop_impls_no_check!(core::ops::Not, NotSpecImpl, not, obeys_not_spec, not_req, not_spec, self, !, [
382    bool
383    usize u8 u16 u32 u64 u128
384    isize i8 i16 i32 i64 i128
385]);
386
387def_bop_impls_check_overflow!(core::ops::Add, AddSpecImpl, add, obeys_add_spec, add_req, add_spec, self, rhs, +, [
388    usize u8 u16 u32 u64 u128
389    isize i8 i16 i32 i64 i128
390]);
391
392def_bop_impls_check_overflow!(core::ops::Sub, SubSpecImpl, sub, obeys_sub_spec, sub_req, sub_spec, self, rhs, -, [
393    usize u8 u16 u32 u64 u128
394    isize i8 i16 i32 i64 i128
395]);
396
397def_bop_impls_check_overflow!(core::ops::Mul, MulSpecImpl, mul, obeys_mul_spec, mul_req, mul_spec, self, rhs, *, [
398    usize u8 u16 u32 u64 u128
399    isize i8 i16 i32 i64 i128
400]);
401
402def_bop_impls_unsigned_div_rem!(core::ops::Div, DivSpecImpl, div, obeys_div_spec, div_req, div_spec, self, rhs, /, [
403    usize u8 u16 u32 u64 u128
404]);
405
406def_bop_impls_signed_div_rem!(core::ops::Div, DivSpecImpl, div, obeys_div_spec, div_req, div_spec, self, rhs, /, [
407    isize i8 i16 i32 i64 i128
408]);
409
410def_bop_impls_unsigned_div_rem!(core::ops::Rem, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec, self, rhs, %, [
411    usize u8 u16 u32 u64 u128
412]);
413
414def_bop_impls_signed_div_rem!(core::ops::Rem, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec, self, rhs, %, [
415    isize i8 i16 i32 i64 i128
416]);
417
418def_bop_impls_no_check!(core::ops::BitAnd, BitAndSpecImpl, bitand, obeys_bitand_spec, bitand_req, bitand_spec, self, rhs, &, [
419    usize u8 u16 u32 u64 u128
420    isize i8 i16 i32 i64 i128
421]);
422
423def_bop_impls_no_check!(core::ops::BitOr, BitOrSpecImpl, bitor, obeys_bitor_spec, bitor_req, bitor_spec, self, rhs, |, [
424    usize u8 u16 u32 u64 u128
425    isize i8 i16 i32 i64 i128
426]);
427
428def_bop_impls_no_check!(core::ops::BitXor, BitXorSpecImpl, bitxor, obeys_bitxor_spec, bitxor_req, bitxor_spec, self, rhs, ^, [
429    bool
430    usize u8 u16 u32 u64 u128
431    isize i8 i16 i32 i64 i128
432]);
433
434def_bop_impls_shift!(core::ops::Shl, ShlSpecImpl, shl, obeys_shl_spec, shl_req, shl_spec, self, rhs, <<, [
435    usize u8 u16 u32 u64 u128
436    isize i8 i16 i32 i64 i128
437]);
438
439def_bop_impls_shift!(core::ops::Shr, ShrSpecImpl, shr, obeys_shr_spec, shr_req, shr_spec, self, rhs, >>, [
440    usize u8 u16 u32 u64 u128
441    isize i8 i16 i32 i64 i128
442]);
443
444verus! {
445
446#[verusfmt::skip]
447// Note: we do not assume that floating point types have obeys_*_spec() == true
448// because Rust floating point operations are not guaranteed to be deterministic.
449// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
450// Instead, we ensure an uninterpreted function about the result,
451// which can be used to trigger user-supplied axioms.
452#[verusfmt::skip]
453
454pub uninterp spec fn neg_ensures<A>(x: A, o: A) -> bool;
455
456pub uninterp spec fn add_ensures<A>(x: A, y: A, o: A) -> bool;
457
458pub uninterp spec fn sub_ensures<A>(x: A, y: A, o: A) -> bool;
459
460pub uninterp spec fn mul_ensures<A>(x: A, y: A, o: A) -> bool;
461
462pub uninterp spec fn div_ensures<A>(x: A, y: A, o: A) -> bool;
463
464pub assume_specification[ <f32 as core::ops::Neg>::neg ](x: f32) -> (o: f32)
465    ensures
466        neg_ensures::<f32>(x, o),
467;
468
469pub assume_specification[ <f32 as core::ops::Add>::add ](x: f32, y: f32) -> (o: f32)
470    ensures
471        add_ensures::<f32>(x, y, o),
472;
473
474pub assume_specification[ <f32 as core::ops::Sub>::sub ](x: f32, y: f32) -> (o: f32)
475    ensures
476        sub_ensures::<f32>(x, y, o),
477;
478
479pub assume_specification[ <f32 as core::ops::Mul>::mul ](x: f32, y: f32) -> (o: f32)
480    ensures
481        mul_ensures::<f32>(x, y, o),
482;
483
484pub assume_specification[ <f32 as core::ops::Div>::div ](x: f32, y: f32) -> (o: f32)
485    ensures
486        div_ensures::<f32>(x, y, o),
487;
488
489pub assume_specification[ <f64 as core::ops::Neg>::neg ](x: f64) -> (o: f64)
490    ensures
491        neg_ensures::<f64>(x, o),
492;
493
494pub assume_specification[ <f64 as core::ops::Add>::add ](x: f64, y: f64) -> (o: f64)
495    ensures
496        add_ensures::<f64>(x, y, o),
497;
498
499pub assume_specification[ <f64 as core::ops::Sub>::sub ](x: f64, y: f64) -> (o: f64)
500    ensures
501        sub_ensures::<f64>(x, y, o),
502;
503
504pub assume_specification[ <f64 as core::ops::Mul>::mul ](x: f64, y: f64) -> (o: f64)
505    ensures
506        mul_ensures::<f64>(x, y, o),
507;
508
509pub assume_specification[ <f64 as core::ops::Div>::div ](x: f64, y: f64) -> (o: f64)
510    ensures
511        div_ensures::<f64>(x, y, o),
512;
513
514} // verus!
vstd/std_specs/ops.rs

vstd/std_specs/
ops.rs
