vstd/
vstd.rs

1//! The "standard library" for [Verus](https://github.com/verus-lang/verus).
2//! Contains various utilities and datatypes for proofs,
3//! as well as runtime functionality with specifications.
4//! For an introduction to Verus, see [the tutorial](https://verus-lang.github.io/verus/guide/).
5#![cfg_attr(not(feature = "std"), no_std)]
6#![allow(unused_parens)]
7#![allow(unused_imports)]
8#![allow(dead_code)]
9#![allow(unused_attributes)]
10#![allow(unused_features)] // silences spurious warnings for features that cause errors when omitted
11#![allow(rustdoc::invalid_rust_codeblocks)]
12#![cfg_attr(verus_keep_ghost, feature(atomic_internals))]
13#![cfg_attr(verus_keep_ghost, feature(generic_atomic))]
14#![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
15#![cfg_attr(any(verus_keep_ghost, feature = "allocator"), feature(allocator_api))]
16#![cfg_attr(verus_keep_ghost, feature(step_trait))]
17#![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
18#![cfg_attr(verus_keep_ghost, feature(sized_hierarchy))]
19#![cfg_attr(verus_keep_ghost, feature(freeze))]
20#![cfg_attr(verus_keep_ghost, feature(derive_clone_copy_internals))]
21#![cfg_attr(verus_keep_ghost, feature(derive_eq_internals))]
22#![cfg_attr(verus_keep_ghost, feature(slice_index_methods))]
23#![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(liballoc_internals))]
24#![cfg_attr(verus_keep_ghost, feature(nonzero_internals))]
25#![cfg_attr(verus_keep_ghost, feature(hint_must_use))]
26#![cfg_attr(verus_keep_ghost, feature(fmt_internals))]
27#![cfg_attr(verus_keep_ghost, feature(fmt_arguments_from_str))]
28#![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(btree_cursors))]
29#![cfg_attr(verus_keep_ghost, feature(panic_internals))]
30
31#[cfg(feature = "alloc")]
32extern crate alloc;
33
34pub mod arithmetic;
35pub mod array;
36pub mod atomic;
37pub mod atomic_ghost;
38pub mod bits;
39pub mod bytes;
40pub mod calc_macro;
41pub mod cell;
42pub mod compute;
43pub mod contrib;
44pub mod endian;
45pub mod float;
46pub mod function;
47#[cfg(feature = "std")]
48pub mod future;
49#[cfg(all(feature = "alloc", feature = "std"))]
50pub mod hash_map;
51#[cfg(all(feature = "alloc", feature = "std"))]
52pub mod hash_set;
53pub mod imap;
54pub mod imap_lib;
55pub mod invariant;
56pub mod iset;
57pub mod iset_lib;
58#[cfg(verus_keep_ghost)]
59pub mod laws_cmp;
60#[cfg(verus_keep_ghost)]
61pub mod laws_eq;
62pub mod layout;
63pub mod logatom;
64pub mod map;
65pub mod map_lib;
66pub mod math;
67pub mod modes;
68pub mod multiset;
69pub mod multiset_lib;
70#[cfg(verus_keep_ghost)]
71pub mod mut_ref;
72pub mod pervasive;
73pub mod predicate;
74pub mod proph;
75pub mod raw_ptr;
76pub mod relations;
77pub mod resource;
78pub mod rwlock;
79pub mod seq;
80pub mod seq_lib;
81pub mod set;
82pub mod set_lib;
83pub mod shared;
84#[cfg(feature = "alloc")]
85pub mod simple_pptr;
86pub mod slice;
87pub mod state_machine_internal;
88pub mod string;
89#[cfg(feature = "std")]
90pub mod thread;
91pub mod tokens;
92pub mod utf8;
93pub mod view;
94pub mod wrapping;
95
96#[cfg(verus_keep_ghost)]
97pub mod std_specs;
98
99// Re-exports all vstd types, traits, and functions that are commonly used or replace
100// regular `core` or `std` definitions.
101pub mod prelude;
102
103use prelude::*;
104
105verus! {
106
107#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
108pub broadcast group group_vstd_default {
109    //
110    // basic Verus math, types, and features
111    //
112    seq::group_seq_lemmas,
113    seq_lib::group_seq_lib_default,
114    map::group_map_lemmas,
115    set::group_set_lemmas,
116    imap::group_imap_lemmas,
117    iset::group_iset_lemmas,
118    set_lib::group_set_lib_default,
119    multiset::group_multiset_axioms,
120    compute::all_spec_ensures,
121    function::group_function_axioms,
122    laws_eq::group_laws_eq,
123    laws_cmp::group_laws_cmp,
124    //
125    // Rust types
126    //
127    slice::group_slice_axioms,
128    array::group_array_axioms,
129    #[cfg(not(verus_verify_core))]
130    string::group_string_axioms,
131    raw_ptr::group_raw_ptr_axioms,
132    layout::group_layout_axioms,
133    mut_ref::group_mut_ref_axioms,
134    //
135    // core std_specs
136    //
137    std_specs::range::group_range_axioms,
138    std_specs::bits::group_bits_axioms,
139    std_specs::control_flow::group_control_flow_axioms,
140    std_specs::fmt::group_fmt_axioms,
141    std_specs::manually_drop::group_manually_drop_axioms,
142    std_specs::iter::group_iter_axioms,
143    //
144    // std_specs for alloc (with or without std)
145    //
146    #[cfg(feature = "alloc")]
147    std_specs::vec::group_vec_axioms,
148    #[cfg(feature = "alloc")]
149    std_specs::vecdeque::group_vec_dequeue_axioms,
150    //
151    // std_specs for alloc + std
152    //
153    #[cfg(all(feature = "alloc", feature = "std"))]
154    std_specs::hash::group_hash_axioms,
155    #[cfg(feature = "alloc")]
156    std_specs::btree::group_btree_axioms,
157    //
158    // std_specs for nonzero_internals
159    //
160    #[cfg(feature = "nonzero_internals")]
161    std_specs::nonzero::group_nonzero_axioms,
162}
163
164} // verus!
165// This allows us to use `$crate::vstd` or `crate::vstd` to refer to vstd
166// both in verus_verify_core mode (vstd is a module) and out (vstd is a crate)
167#[cfg(not(verus_verify_core))]
168#[doc(hidden)]
169pub use crate as vstd;
vstd/vstd.rs

vstd/
vstd.rs
