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

vstd/
vstd.rs
