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
76macro_rules! def_bin_ops_assign_spec {
77    ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident) => {
78        $crate::vstd::prelude::verus! {
79            #[verifier::external_trait_specification]
80            #[verifier::external_trait_extension($spec_trait via $impl_trait)]
81            pub trait $extrait<Rhs = Self> {
82                type ExternalTraitSpecificationFor: $trait<Rhs>;
83
84                spec fn $obeys() -> bool;
85
86                spec fn $req(&self, rhs: Rhs) -> bool;
87
88                spec fn $spec(&self, rhs: Rhs) -> &Self;
89
90                fn $fun(&mut self, rhs: Rhs)
91                    requires
92                        self.$req(rhs),
93                    ensures
94                        Self::$obeys() ==> &*final(self) == old(self).$spec(rhs);
95            }
96        }
97};
98}
99
100def_un_ops_spec!(
101    core::ops::Neg,
102    ExNeg,
103    NegSpec,
104    NegSpecImpl,
105    neg,
106    obeys_neg_spec,
107    neg_req,
108    neg_spec
109);
110
111def_un_ops_spec!(
112    core::ops::Not,
113    ExNot,
114    NotSpec,
115    NotSpecImpl,
116    not,
117    obeys_not_spec,
118    not_req,
119    not_spec
120);
121
122def_bin_ops_spec!(
123    core::ops::Add,
124    ExAdd,
125    AddSpec,
126    AddSpecImpl,
127    add,
128    obeys_add_spec,
129    add_req,
130    add_spec
131);
132
133def_bin_ops_assign_spec!(
134    core::ops::AddAssign,
135    ExAddAssign,
136    AddAssignSpec,
137    AddAssignSpecImpl,
138    add_assign,
139    obeys_add_assign_spec,
140    add_assign_req,
141    add_assign_spec
142);
143
144def_bin_ops_spec!(
145    core::ops::Sub,
146    ExSub,
147    SubSpec,
148    SubSpecImpl,
149    sub,
150    obeys_sub_spec,
151    sub_req,
152    sub_spec
153);
154
155def_bin_ops_assign_spec!(
156    core::ops::SubAssign,
157    ExSubAssign,
158    SubAssignSpec,
159    SubAssignSpecImpl,
160    sub_assign,
161    obeys_sub_assign_spec,
162    sub_assign_req,
163    sub_assign_spec
164);
165
166def_bin_ops_spec!(
167    core::ops::Mul,
168    ExMul,
169    MulSpec,
170    MulSpecImpl,
171    mul,
172    obeys_mul_spec,
173    mul_req,
174    mul_spec
175);
176
177def_bin_ops_assign_spec!(
178    core::ops::MulAssign,
179    ExMulAssign,
180    MulAssignSpec,
181    MulAssignSpecImpl,
182    mul_assign,
183    obeys_mul_assign_spec,
184    mul_assign_req,
185    mul_assign_spec
186);
187
188def_bin_ops_spec!(
189    core::ops::Div,
190    ExDiv,
191    DivSpec,
192    DivSpecImpl,
193    div,
194    obeys_div_spec,
195    div_req,
196    div_spec
197);
198
199def_bin_ops_assign_spec!(
200    core::ops::DivAssign,
201    ExDivAssign,
202    DivAssignSpec,
203    DivAssignSpecImpl,
204    div_assign,
205    obeys_div_assign_spec,
206    div_assign_req,
207    div_assign_spec
208);
209
210def_bin_ops_spec!(
211    core::ops::Rem,
212    ExRem,
213    RemSpec,
214    RemSpecImpl,
215    rem,
216    obeys_rem_spec,
217    rem_req,
218    rem_spec
219);
220
221def_bin_ops_assign_spec!(
222    core::ops::RemAssign,
223    ExRemAssign,
224    RemAssignSpec,
225    RemAssignSpecImpl,
226    rem_assign,
227    obeys_rem_assign_spec,
228    rem_assign_req,
229    rem_assign_spec
230);
231
232def_bin_ops_spec!(
233    core::ops::BitAnd,
234    ExBitAnd,
235    BitAndSpec,
236    BitAndSpecImpl,
237    bitand,
238    obeys_bitand_spec,
239    bitand_req,
240    bitand_spec
241);
242
243def_bin_ops_assign_spec!(
244    core::ops::BitAndAssign,
245    ExBitAndAssign,
246    BitAndAssignSpec,
247    BitAndAssignSpecImpl,
248    bitand_assign,
249    obeys_bitand_assign_spec,
250    bitand_assign_req,
251    bitand_assign_spec
252);
253
254def_bin_ops_spec!(
255    core::ops::BitOr,
256    ExBitOr,
257    BitOrSpec,
258    BitOrSpecImpl,
259    bitor,
260    obeys_bitor_spec,
261    bitor_req,
262    bitor_spec
263);
264
265def_bin_ops_assign_spec!(
266    core::ops::BitOrAssign,
267    ExBitOrAssign,
268    BitOrAssignSpec,
269    BitOrAssignSpecImpl,
270    bitor_assign,
271    obeys_bitor_assign_spec,
272    bitor_assign_req,
273    bitor_assign_spec
274);
275
276def_bin_ops_spec!(
277    core::ops::BitXor,
278    ExBitXor,
279    BitXorSpec,
280    BitXorSpecImpl,
281    bitxor,
282    obeys_bitxor_spec,
283    bitxor_req,
284    bitxor_spec
285);
286
287def_bin_ops_assign_spec!(
288    core::ops::BitXorAssign,
289    ExBitXorAssign,
290    BitXorAssignSpec,
291    BitXorAssignSpecImpl,
292    bitxor_assign,
293    obeys_bitxor_assign_spec,
294    bitxor_assign_req,
295    bitxor_assign_spec
296);
297
298def_bin_ops_spec!(
299    core::ops::Shl,
300    ExShl,
301    ShlSpec,
302    ShlSpecImpl,
303    shl,
304    obeys_shl_spec,
305    shl_req,
306    shl_spec
307);
308
309def_bin_ops_assign_spec!(
310    core::ops::ShlAssign,
311    ExShlAssign,
312    ShlAssignSpec,
313    ShlAssignSpecImpl,
314    shl_assign,
315    obeys_shl_assign_spec,
316    shl_assign_req,
317    shl_assign_spec
318);
319
320def_bin_ops_spec!(
321    core::ops::Shr,
322    ExShr,
323    ShrSpec,
324    ShrSpecImpl,
325    shr,
326    obeys_shr_spec,
327    shr_req,
328    shr_spec
329);
330
331def_bin_ops_assign_spec!(
332    core::ops::ShrAssign,
333    ExShrAssign,
334    ShrAssignSpec,
335    ShrAssignSpecImpl,
336    shr_assign,
337    obeys_shr_assign_spec,
338    shr_assign_req,
339    shr_assign_spec
340);
341
342macro_rules! def_uop_impls {
343    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, [$(($typ:ty, $req_expr:expr, $spec_expr:expr))*]) => {
344        $crate::vstd::prelude::verus! {
345            $(
346                impl $impl_trait for $typ {
347                    open spec fn $obeys() -> bool {
348                        true
349                    }
350
351                    open spec fn $req($self) -> bool {
352                        $req_expr
353                    }
354
355                    open spec fn $spec($self) -> Self::Output {
356                        $spec_expr
357                    }
358                }
359
360                pub assume_specification[ <$typ as $trait>::$fun ](x: $typ) -> $typ;
361            )*
362        }
363};
364}
365
366macro_rules! def_bop_impls {
367    ($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))*]) => {
368        $crate::vstd::prelude::verus! {
369            $(
370                impl $impl_trait for $typ {
371                    open spec fn $obeys() -> bool {
372                        true
373                    }
374
375                    open spec fn $req($self, $rhs: $typ) -> bool {
376                        $req_expr
377                    }
378
379                    open spec fn $spec($self, $rhs: $typ) -> Self::Output {
380                        $spec_expr
381                    }
382                }
383
384                pub assume_specification[ <$typ as $trait>::$fun ](x: $typ, y: $typ) -> $typ;
385            )*
386        }
387};
388}
389
390macro_rules! def_bop_assign_impls {
391    ($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))*]) => {
392        $crate::vstd::prelude::verus! {
393            $(
394                impl $impl_trait for $typ {
395                    open spec fn $obeys() -> bool {
396                        true
397                    }
398
399                    open spec fn $req(&$self, $rhs: $typ) -> bool {
400                        $req_expr
401                    }
402
403                    open spec fn $spec(&$self, $rhs: $typ) -> &Self {
404                        &$spec_expr
405                    }
406                }
407
408                pub assume_specification[ <$typ as $trait>::$fun ](x: &mut $typ, y: $typ);
409            )*
410        }
411};
412}
413
414macro_rules! def_uop_impls_no_check {
415    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $op:tt, [$($typ:ty)*]) => {
416        $crate::vstd::prelude::verus! {
417            def_uop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, [
418                $(
419                    (
420                        $typ,
421                        true,
422                        $op $self
423                    )
424                )*
425            ]);
426        }
427};
428}
429
430macro_rules! def_uop_impls_check_overflow {
431    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $op:tt, [$($typ:ty)*]) => {
432        $crate::vstd::prelude::verus! {
433            def_uop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, [
434                $(
435                    (
436                        $typ,
437                        ($op $self) as $typ == ($op $self),
438                        ($op $self) as $typ
439                    )
440                )*
441            ]);
442        }
443};
444}
445
446macro_rules! def_bop_impls_no_check {
447    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
448        $crate::vstd::prelude::verus! {
449            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
450                $(
451                    (
452                        $typ,
453                        true,
454                        $self $op $rhs
455                    )
456                )*
457            ]);
458        }
459};
460}
461
462macro_rules! def_bop_assign_impls_no_check {
463    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
464        $crate::vstd::prelude::verus! {
465            def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
466                $(
467                    (
468                        $typ,
469                        true,
470                        $self $op $rhs
471                    )
472                )*
473            ]);
474        }
475};
476}
477
478macro_rules! def_bop_impls_check_overflow {
479    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
480        $crate::vstd::prelude::verus! {
481            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
482                $(
483                    (
484                        $typ,
485                        ($self $op $rhs) as $typ == ($self $op $rhs),
486                        ($self $op $rhs) as $typ
487                    )
488                )*
489            ]);
490        }
491};
492}
493
494macro_rules! def_bop_assign_impls_check_overflow {
495    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
496        $crate::vstd::prelude::verus! {
497            def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
498                $(
499                    (
500                        $typ,
501                        ($self $op $rhs) as $typ == ($self $op $rhs),
502                        ($self $op $rhs) as $typ
503                    )
504                )*
505            ]);
506        }
507};
508}
509
510macro_rules! def_bop_impls_unsigned_div_rem {
511    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
512        $crate::vstd::prelude::verus! {
513            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
514                $(
515                    (
516                        $typ,
517                        $rhs != 0,
518                        $self $op $rhs
519                    )
520                )*
521            ]);
522        }
523};
524}
525
526macro_rules! def_bop_assign_impls_unsigned_div_rem {
527    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
528        $crate::vstd::prelude::verus! {
529            def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
530                $(
531                    (
532                        $typ,
533                        $rhs != 0,
534                        $self $op $rhs
535                    )
536                )*
537            ]);
538        }
539};
540}
541
542// Signed div/rem needs to:
543// - check for overflow (e.g. (-128i8) / (-1im))
544// - express truncating div, rem in terms of euclidean /, %
545macro_rules! def_bop_impls_signed_div_rem {
546    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:path, [$($typ:ty)*]) => {
547        $crate::vstd::prelude::verus! {
548            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
549                $(
550                    (
551                        $typ,
552                        $rhs != 0 && !($self == $typ::MIN && $rhs == -1),
553                        $op($self as int, $rhs as int) as $typ
554                    )
555                )*
556            ]);
557        }
558};
559}
560
561macro_rules! def_bop_assign_impls_signed_div_rem {
562    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:path, [$($typ:ty)*]) => {
563        $crate::vstd::prelude::verus! {
564            def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
565                $(
566                    (
567                        $typ,
568                        $rhs != 0 && !($self == $typ::MIN && $rhs == -1),
569                        $op($self as int, $rhs as int) as $typ
570                    )
571                )*
572            ]);
573        }
574};
575}
576
577// TODO: there are many more combinations of primitive integer types supported by Shl and Shr,
578// such as (Self = u8, Rhs = u64)
579macro_rules! def_bop_impls_shift {
580    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
581        $crate::vstd::prelude::verus! {
582            def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
583                $(
584                    (
585                        $typ,
586                        $rhs < $typ::BITS,
587                        $self $op $rhs
588                    )
589                )*
590            ]);
591        }
592};
593}
594
595macro_rules! def_bop_assign_impls_shift {
596    ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => {
597        $crate::vstd::prelude::verus! {
598            def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [
599                $(
600                    (
601                        $typ,
602                        $rhs < $typ::BITS,
603                        $self $op $rhs
604                    )
605                )*
606            ]);
607        }
608};
609}
610
611def_uop_impls_check_overflow!(core::ops::Neg, NegSpecImpl, neg, obeys_neg_spec, neg_req, neg_spec, self, -, [
612    isize i8 i16 i32 i64 i128
613]);
614
615def_uop_impls_no_check!(core::ops::Not, NotSpecImpl, not, obeys_not_spec, not_req, not_spec, self, !, [
616    bool
617    usize u8 u16 u32 u64 u128
618    isize i8 i16 i32 i64 i128
619]);
620
621def_bop_impls_check_overflow!(core::ops::Add, AddSpecImpl, add, obeys_add_spec, add_req, add_spec, self, rhs, +, [
622    usize u8 u16 u32 u64 u128
623    isize i8 i16 i32 i64 i128
624]);
625
626def_bop_assign_impls_check_overflow!(core::ops::AddAssign, AddAssignSpecImpl, add_assign, obeys_add_assign_spec, add_assign_req, add_assign_spec, self, rhs, +, [
627    usize u8 u16 u32 u64 u128
628    isize i8 i16 i32 i64 i128
629]);
630
631def_bop_impls_check_overflow!(core::ops::Sub, SubSpecImpl, sub, obeys_sub_spec, sub_req, sub_spec, self, rhs, -, [
632    usize u8 u16 u32 u64 u128
633    isize i8 i16 i32 i64 i128
634]);
635
636def_bop_assign_impls_check_overflow!(core::ops::SubAssign, SubAssignSpecImpl, sub_assign, obeys_sub_assign_spec, sub_assign_req, sub_assign_spec, self, rhs, -, [
637    usize u8 u16 u32 u64 u128
638    isize i8 i16 i32 i64 i128
639]);
640
641def_bop_impls_check_overflow!(core::ops::Mul, MulSpecImpl, mul, obeys_mul_spec, mul_req, mul_spec, self, rhs, *, [
642    usize u8 u16 u32 u64 u128
643    isize i8 i16 i32 i64 i128
644]);
645
646def_bop_assign_impls_check_overflow!(core::ops::MulAssign, MulAssignSpecImpl, mul_assign, obeys_mul_assign_spec, mul_assign_req, mul_assign_spec, self, rhs, *, [
647    usize u8 u16 u32 u64 u128
648    isize i8 i16 i32 i64 i128
649]);
650
651def_bop_impls_unsigned_div_rem!(core::ops::Div, DivSpecImpl, div, obeys_div_spec, div_req, div_spec, self, rhs, /, [
652    usize u8 u16 u32 u64 u128
653]);
654
655def_bop_assign_impls_unsigned_div_rem!(core::ops::DivAssign, DivAssignSpecImpl, div_assign, obeys_div_assign_spec, div_assign_req, div_assign_spec, self, rhs, /, [
656    usize u8 u16 u32 u64 u128
657]);
658
659def_bop_impls_signed_div_rem!(core::ops::Div, DivSpecImpl, div, obeys_div_spec, div_req, div_spec, self, rhs, super::super::arithmetic::div_mod::rust_div, [
660    isize i8 i16 i32 i64 i128
661]);
662
663def_bop_assign_impls_signed_div_rem!(core::ops::DivAssign, DivAssignSpecImpl, div_assign, obeys_div_assign_spec, div_assign_req, div_assign_spec, self, rhs, super::super::arithmetic::div_mod::rust_div, [
664    isize i8 i16 i32 i64 i128
665]);
666
667def_bop_impls_unsigned_div_rem!(core::ops::Rem, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec, self, rhs, %, [
668    usize u8 u16 u32 u64 u128
669]);
670
671def_bop_assign_impls_unsigned_div_rem!(core::ops::RemAssign, RemAssignSpecImpl, rem_assign, obeys_rem_assign_spec, rem_assign_req, rem_assign_spec, self, rhs, %, [
672    usize u8 u16 u32 u64 u128
673]);
674
675def_bop_impls_signed_div_rem!(core::ops::Rem, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec, self, rhs, super::super::arithmetic::div_mod::rust_rem, [
676    isize i8 i16 i32 i64 i128
677]);
678
679def_bop_assign_impls_signed_div_rem!(core::ops::RemAssign, RemAssignSpecImpl, rem_assign, obeys_rem_assign_spec, rem_assign_req, rem_assign_spec, self, rhs, super::super::arithmetic::div_mod::rust_rem, [
680    isize i8 i16 i32 i64 i128
681]);
682
683def_bop_impls_no_check!(core::ops::BitAnd, BitAndSpecImpl, bitand, obeys_bitand_spec, bitand_req, bitand_spec, self, rhs, &, [
684    usize u8 u16 u32 u64 u128
685    isize i8 i16 i32 i64 i128
686]);
687
688def_bop_assign_impls_no_check!(core::ops::BitAndAssign, BitAndAssignSpecImpl, bitand_assign, obeys_bitand_assign_spec, bitand_assign_req, bitand_assign_spec, self, rhs, &, [
689    usize u8 u16 u32 u64 u128
690    isize i8 i16 i32 i64 i128
691]);
692
693def_bop_impls_no_check!(core::ops::BitOr, BitOrSpecImpl, bitor, obeys_bitor_spec, bitor_req, bitor_spec, self, rhs, |, [
694    usize u8 u16 u32 u64 u128
695    isize i8 i16 i32 i64 i128
696]);
697
698def_bop_assign_impls_no_check!(core::ops::BitOrAssign, BitOrAssignSpecImpl, bitor_assign, obeys_bitor_assign_spec, bitor_assign_req, bitor_assign_spec, self, rhs, |, [
699    usize u8 u16 u32 u64 u128
700    isize i8 i16 i32 i64 i128
701]);
702
703def_bop_impls_no_check!(core::ops::BitXor, BitXorSpecImpl, bitxor, obeys_bitxor_spec, bitxor_req, bitxor_spec, self, rhs, ^, [
704    bool
705    usize u8 u16 u32 u64 u128
706    isize i8 i16 i32 i64 i128
707]);
708
709def_bop_assign_impls_no_check!(core::ops::BitXorAssign, BitXorAssignSpecImpl, bitxor_assign, obeys_bitxor_assign_spec, bitxor_assign_req, bitxor_assign_spec, self, rhs, ^, [
710    usize u8 u16 u32 u64 u128
711    isize i8 i16 i32 i64 i128
712]);
713
714def_bop_impls_shift!(core::ops::Shl, ShlSpecImpl, shl, obeys_shl_spec, shl_req, shl_spec, self, rhs, <<, [
715    usize u8 u16 u32 u64 u128
716    isize i8 i16 i32 i64 i128
717]);
718
719def_bop_assign_impls_shift!(core::ops::ShlAssign, ShlAssignSpecImpl, shl_assign, obeys_shl_assign_spec, shl_assign_req, shl_assign_spec, self, rhs, <<, [
720    usize u8 u16 u32 u64 u128
721    isize i8 i16 i32 i64 i128
722]);
723
724def_bop_impls_shift!(core::ops::Shr, ShrSpecImpl, shr, obeys_shr_spec, shr_req, shr_spec, self, rhs, >>, [
725    usize u8 u16 u32 u64 u128
726    isize i8 i16 i32 i64 i128
727]);
728
729def_bop_assign_impls_shift!(core::ops::ShrAssign, ShrAssignSpecImpl, shr_assign, obeys_shr_assign_spec, shr_assign_req, shr_assign_spec, self, rhs, >>, [
730    usize u8 u16 u32 u64 u128
731    isize i8 i16 i32 i64 i128
732]);
733
734verus! {
735
736#[verusfmt::skip]
737// Note: we do not assume that floating point types have obeys_*_spec() == true
738// because Rust floating point operations are not guaranteed to be deterministic.
739// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
740// Instead, we ensure an uninterpreted function about the result,
741// which can be used to trigger user-supplied axioms.
742#[verusfmt::skip]
743
744pub uninterp spec fn neg_ensures<A>(x: A, o: A) -> bool;
745
746pub uninterp spec fn add_ensures<A>(x: A, y: A, o: A) -> bool;
747
748pub uninterp spec fn sub_ensures<A>(x: A, y: A, o: A) -> bool;
749
750pub uninterp spec fn mul_ensures<A>(x: A, y: A, o: A) -> bool;
751
752pub uninterp spec fn div_ensures<A>(x: A, y: A, o: A) -> bool;
753
754pub assume_specification[ <f32 as core::ops::Neg>::neg ](x: f32) -> (o: f32)
755    ensures
756        neg_ensures::<f32>(x, o),
757;
758
759pub assume_specification[ <f32 as core::ops::Add>::add ](x: f32, y: f32) -> (o: f32)
760    ensures
761        add_ensures::<f32>(x, y, o),
762;
763
764pub assume_specification[ <f32 as core::ops::Sub>::sub ](x: f32, y: f32) -> (o: f32)
765    ensures
766        sub_ensures::<f32>(x, y, o),
767;
768
769pub assume_specification[ <f32 as core::ops::Mul>::mul ](x: f32, y: f32) -> (o: f32)
770    ensures
771        mul_ensures::<f32>(x, y, o),
772;
773
774pub assume_specification[ <f32 as core::ops::Div>::div ](x: f32, y: f32) -> (o: f32)
775    ensures
776        div_ensures::<f32>(x, y, o),
777;
778
779pub assume_specification[ <f64 as core::ops::Neg>::neg ](x: f64) -> (o: f64)
780    ensures
781        neg_ensures::<f64>(x, o),
782;
783
784pub assume_specification[ <f64 as core::ops::Add>::add ](x: f64, y: f64) -> (o: f64)
785    ensures
786        add_ensures::<f64>(x, y, o),
787;
788
789pub assume_specification[ <f64 as core::ops::Sub>::sub ](x: f64, y: f64) -> (o: f64)
790    ensures
791        sub_ensures::<f64>(x, y, o),
792;
793
794pub assume_specification[ <f64 as core::ops::Mul>::mul ](x: f64, y: f64) -> (o: f64)
795    ensures
796        mul_ensures::<f64>(x, y, o),
797;
798
799pub assume_specification[ <f64 as core::ops::Div>::div ](x: f64, y: f64) -> (o: f64)
800    ensures
801        div_ensures::<f64>(x, y, o),
802;
803
804} // verus!
vstd/std_specs/ops.rs

vstd/std_specs/
ops.rs
