vstd 0.0.0-2026-04-20-1748

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

#![allow(unused_imports)]
use super::super::prelude::*;
use core::sync::atomic::*;

// Supports the core::sync::atomic functions
// This provides NO support for reasoning about the values inside the atomics.
// If you need to do that, see `vstd::atomic` or `vstd::atomic_ghost` instead.

#[verifier::external_type_specification]
pub struct ExOrdering(Ordering);

macro_rules! atomic_specs_common {
    ($at:ty, $ty:ty) => {
        #[verifier::external_type_specification]
        #[verifier::external_body]
        pub struct ExAtomic($at);

        verus!{

        pub assume_specification [ <$at>::new ](v: $ty) -> $at;

        pub assume_specification [ <$at>::compare_exchange ](
            atomic: &$at,
            current: $ty,
            new: $ty,
            success: Ordering,
            failure: Ordering,
        ) -> Result<$ty, $ty>;

        pub assume_specification [ <$at>::compare_exchange_weak ](
            atomic: &$at,
            current: $ty,
            new: $ty,
            success: Ordering,
            failure: Ordering,
        ) -> Result<$ty, $ty>;

        pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering);

        pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        }
    };
}

macro_rules! atomic_specs_int_specific {
    ($at:ty, $ty:ty) => {
        verus!{

        pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty;

        }
    };
}

macro_rules! atomic_specs_int {
    ($modname:ident, $at:ty, $ty:ty) => {
        mod $modname {
            use super::*;
            atomic_specs_common!($at, $ty);
            atomic_specs_int_specific!($at, $ty);
        }
    };
}

macro_rules! atomic_specs_bool {
    ($modname:ident, $at:ty, $ty:ty) => {
        mod $modname {
            use super::*;
            atomic_specs_common!($at, $ty);
        }
    };
}

atomic_specs_int!(atomic_specs_u8, AtomicU8, u8);
atomic_specs_int!(atomic_specs_u16, AtomicU16, u16);
atomic_specs_int!(atomic_specs_u32, AtomicU32, u32);
#[cfg(target_has_atomic = "64")]
atomic_specs_int!(atomic_specs_u64, AtomicU64, u64);
atomic_specs_int!(atomic_specs_usize, AtomicUsize, usize);

atomic_specs_int!(atomic_specs_i8, AtomicI8, i8);
atomic_specs_int!(atomic_specs_i16, AtomicI16, i16);
atomic_specs_int!(atomic_specs_i32, AtomicI32, i32);
#[cfg(target_has_atomic = "64")]
atomic_specs_int!(atomic_specs_i64, AtomicI64, i64);
atomic_specs_int!(atomic_specs_isize, AtomicIsize, isize);

atomic_specs_bool!(atomic_specs_bool, AtomicBool, bool);