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
26#[cfg(feature = "alloc")]
27extern crate alloc;
28
29pub mod arithmetic;
30pub mod array;
31pub mod atomic;
32pub mod atomic_ghost;
33pub mod bits;
34pub mod bytes;
35pub mod calc_macro;
36pub mod cell;
37pub mod compute;
38pub mod contrib;
39pub mod endian;
40pub mod float;
41pub mod function;
42#[cfg(feature = "std")]
43pub mod future;
44#[cfg(all(feature = "alloc", feature = "std"))]
45pub mod hash_map;
46#[cfg(all(feature = "alloc", feature = "std"))]
47pub mod hash_set;
48pub mod imap;
49pub mod imap_lib;
50pub mod invariant;
51pub mod iset;
52pub mod iset_lib;
53#[cfg(verus_keep_ghost)]
54pub mod laws_cmp;
55#[cfg(verus_keep_ghost)]
56pub mod laws_eq;
57pub mod layout;
58pub mod logatom;
59pub mod map;
60pub mod map_lib;
61pub mod math;
62pub mod modes;
63pub mod multiset;
64pub mod multiset_lib;
65pub mod pervasive;
66pub mod predicate;
67pub mod proph;
68pub mod raw_ptr;
69pub mod relations;
70pub mod resource;
71pub mod rwlock;
72pub mod seq;
73pub mod seq_lib;
74pub mod set;
75pub mod set_lib;
76pub mod shared;
77#[cfg(feature = "alloc")]
78pub mod simple_pptr;
79pub mod slice;
80pub mod state_machine_internal;
81pub mod string;
82#[cfg(feature = "std")]
83pub mod thread;
84pub mod tokens;
85pub mod utf8;
86pub mod view;
87pub mod wrapping;
88
89#[cfg(verus_keep_ghost)]
90pub mod std_specs;
91
92// Re-exports all vstd types, traits, and functions that are commonly used or replace
93// regular `core` or `std` definitions.
94pub mod prelude;
95
96use prelude::*;
97
98verus! {
99
100#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
101pub broadcast group group_vstd_default {
102    //
103    // basic Verus math, types, and features
104    //
105    seq::group_seq_lemmas,
106    seq_lib::group_seq_lib_default,
107    map::group_map_lemmas,
108    set::group_set_lemmas,
109    imap::group_imap_lemmas,
110    iset::group_iset_lemmas,
111    set_lib::group_set_lib_default,
112    multiset::group_multiset_axioms,
113    compute::all_spec_ensures,
114    function::group_function_axioms,
115    laws_eq::group_laws_eq,
116    laws_cmp::group_laws_cmp,
117    //
118    // Rust types
119    //
120    slice::group_slice_axioms,
121    array::group_array_axioms,
122    #[cfg(not(verus_verify_core))]
123    string::group_string_axioms,
124    raw_ptr::group_raw_ptr_axioms,
125    layout::group_layout_axioms,
126    //
127    // core std_specs
128    //
129    std_specs::range::group_range_axioms,
130    std_specs::bits::group_bits_axioms,
131    std_specs::control_flow::group_control_flow_axioms,
132    std_specs::slice::group_slice_axioms,
133    std_specs::manually_drop::group_manually_drop_axioms,
134    std_specs::iter::group_iter_axioms,
135    //
136    // std_specs for alloc (with or without std)
137    //
138    #[cfg(feature = "alloc")]
139    std_specs::vec::group_vec_axioms,
140    #[cfg(feature = "alloc")]
141    std_specs::vecdeque::group_vec_dequeue_axioms,
142    //
143    // std_specs for alloc + std
144    //
145    #[cfg(all(feature = "alloc", feature = "std"))]
146    std_specs::hash::group_hash_axioms,
147    #[cfg(feature = "alloc")]
148    std_specs::btree::group_btree_axioms,
149    //
150    // std_specs for nonzero_internals
151    //
152    #[cfg(feature = "nonzero_internals")]
153    std_specs::nonzero::group_nonzero_axioms,
154}
155
156} // verus!
157// This allows us to use `$crate::vstd` or `crate::vstd` to refer to vstd
158// both in verus_verify_core mode (vstd is a module) and out (vstd is a crate)
159#[cfg(not(verus_verify_core))]
160#[doc(hidden)]
161pub use crate as vstd;
vstd/vstd.rs

vstd/
vstd.rs
