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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

//! The "standard library" for [Verus](https://github.com/verus-lang/verus).
//! Contains various utilities and datatypes for proofs,
//! as well as runtime functionality with specifications.
//! For an introduction to Verus, see [the tutorial](https://verus-lang.github.io/verus/guide/).
#![cfg_attr(not(feature = "std"), no_std)]
#![allow(unused_parens)]
#![allow(unused_imports)]
#![allow(dead_code)]
#![allow(unused_attributes)]
#![allow(rustdoc::invalid_rust_codeblocks)]
#![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
#![cfg_attr(any(verus_keep_ghost, feature = "allocator"), feature(allocator_api))]
#![cfg_attr(verus_keep_ghost, feature(step_trait))]
#![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
#![cfg_attr(verus_keep_ghost, feature(strict_provenance))]
#![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))]
#![cfg_attr(verus_keep_ghost, feature(freeze))]

#[cfg(feature = "alloc")]
extern crate alloc;

pub mod arithmetic;
pub mod array;
pub mod atomic;
pub mod atomic_ghost;
pub mod bits;
pub mod bytes;
pub mod calc_macro;
pub mod cell;
pub mod compute;
pub mod function;
#[cfg(all(feature = "alloc", feature = "std"))]
pub mod hash_map;
#[cfg(all(feature = "alloc", feature = "std"))]
pub mod hash_set;
pub mod invariant;
pub mod layout;
pub mod logatom;
pub mod map;
pub mod map_lib;
pub mod math;
pub mod modes;
pub mod multiset;
pub mod multiset_lib;
pub mod pcm;
pub mod pcm_lib;
pub mod pervasive;
pub mod proph;
pub mod raw_ptr;
pub mod rwlock;
pub mod seq;
pub mod seq_lib;
pub mod set;
pub mod set_lib;
pub mod shared;
#[cfg(feature = "alloc")]
pub mod simple_pptr;
pub mod slice;
pub mod state_machine_internal;
pub mod storage_protocol;
pub mod string;
#[cfg(feature = "std")]
pub mod thread;
pub mod view;

pub mod relations;
#[cfg(verus_keep_ghost)]
pub mod std_specs;

// Re-exports all vstd types, traits, and functions that are commonly used or replace
// regular `core` or `std` definitions.
pub mod prelude;
pub mod tokens;

use prelude::*;

verus! {

#[cfg(all(feature = "alloc", feature = "std"))]
#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
pub broadcast group group_vstd_default {
    seq::group_seq_axioms,
    seq_lib::group_seq_lib_default,
    map::group_map_axioms,
    set::group_set_axioms,
    set_lib::group_set_lib_default,
    std_specs::bits::group_bits_axioms,
    std_specs::control_flow::group_control_flow_axioms,
    std_specs::vec::group_vec_axioms,
    slice::group_slice_axioms,
    array::group_array_axioms,
    multiset::group_multiset_axioms,
    string::group_string_axioms,
    std_specs::range::group_range_axioms,
    raw_ptr::group_raw_ptr_axioms,
    compute::all_spec_ensures,
    layout::group_layout_axioms,
    function::group_seq_axioms,
    std_specs::hash::group_hash_axioms,
}

#[cfg(feature = "alloc")]
#[cfg(not(feature = "std"))]
#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
pub broadcast group group_vstd_default {
    seq::group_seq_axioms,
    seq_lib::group_seq_lib_default,
    map::group_map_axioms,
    set::group_set_axioms,
    set_lib::group_set_lib_default,
    std_specs::bits::group_bits_axioms,
    std_specs::control_flow::group_control_flow_axioms,
    std_specs::vec::group_vec_axioms,
    slice::group_slice_axioms,
    array::group_array_axioms,
    multiset::group_multiset_axioms,
    string::group_string_axioms,
    std_specs::range::group_range_axioms,
    raw_ptr::group_raw_ptr_axioms,
    compute::all_spec_ensures,
    layout::group_layout_axioms,
    function::group_seq_axioms,
}

#[cfg(not(feature = "alloc"))]
#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
pub broadcast group group_vstd_default {
    seq::group_seq_axioms,
    seq_lib::group_seq_lib_default,
    map::group_map_axioms,
    set::group_set_axioms,
    set_lib::group_set_lib_default,
    std_specs::bits::group_bits_axioms,
    std_specs::control_flow::group_control_flow_axioms,
    slice::group_slice_axioms,
    array::group_array_axioms,
    multiset::group_multiset_axioms,
    string::group_string_axioms,
    std_specs::range::group_range_axioms,
    raw_ptr::group_raw_ptr_axioms,
    compute::all_spec_ensures,
    layout::group_layout_axioms,
    function::group_seq_axioms,
}

} // verus!
// This allows us to use `$crate::vstd` or `crate::vstd` to refer to vstd
// both in verus_verify_core mode (vstd is a module) and out (vstd is a crate)
#[cfg(not(verus_verify_core))]
#[doc(hidden)]
pub use crate as vstd;