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(rustdoc::invalid_rust_codeblocks)]
11#![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
12#![cfg_attr(any(verus_keep_ghost, feature = "allocator"), feature(allocator_api))]
13#![cfg_attr(verus_keep_ghost, feature(step_trait))]
14#![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
15#![cfg_attr(verus_keep_ghost, feature(sized_hierarchy))]
16#![cfg_attr(verus_keep_ghost, feature(freeze))]
17#![cfg_attr(verus_keep_ghost, feature(derive_clone_copy))]
18#![cfg_attr(verus_keep_ghost, feature(derive_eq))]
19#![cfg_attr(verus_keep_ghost, verifier::migrate_postconditions_with_mut_refs(true))]
20#![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(liballoc_internals))]
21#![cfg_attr(verus_keep_ghost, feature(new_range_api))]
22
23#[cfg(feature = "alloc")]
24extern crate alloc;
25
26pub mod arithmetic;
27pub mod array;
28pub mod atomic;
29pub mod atomic_ghost;
30pub mod bits;
31pub mod bytes;
32pub mod calc_macro;
33pub mod cell;
34pub mod compute;
35pub mod contrib;
36pub mod float;
37pub mod function;
38#[cfg(all(feature = "alloc", feature = "std"))]
39pub mod hash_map;
40#[cfg(all(feature = "alloc", feature = "std"))]
41pub mod hash_set;
42pub mod invariant;
43#[cfg(verus_keep_ghost)]
44pub mod laws_cmp;
45#[cfg(verus_keep_ghost)]
46pub mod laws_eq;
47pub mod layout;
48pub mod logatom;
49pub mod map;
50pub mod map_lib;
51pub mod math;
52pub mod modes;
53pub mod multiset;
54pub mod multiset_lib;
55pub mod pcm;
56pub mod pcm_lib;
57pub mod pervasive;
58pub mod predicate;
59pub mod proph;
60pub mod raw_ptr;
61pub mod relations;
62pub mod rwlock;
63pub mod seq;
64pub mod seq_lib;
65pub mod set;
66pub mod set_lib;
67pub mod shared;
68#[cfg(feature = "alloc")]
69pub mod simple_pptr;
70pub mod slice;
71pub mod state_machine_internal;
72pub mod storage_protocol;
73pub mod string;
74#[cfg(feature = "std")]
75pub mod thread;
76pub mod tokens;
77pub mod view;
78
79#[cfg(verus_keep_ghost)]
80pub mod std_specs;
81
82// Re-exports all vstd types, traits, and functions that are commonly used or replace
83// regular `core` or `std` definitions.
84pub mod prelude;
85
86use prelude::*;
87
88verus! {
89
90#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
91pub broadcast group group_vstd_default {
92    //
93    // basic Verus math, types, and features
94    //
95    seq::group_seq_axioms,
96    seq_lib::group_seq_lib_default,
97    map::group_map_axioms,
98    set::group_set_axioms,
99    set_lib::group_set_lib_default,
100    multiset::group_multiset_axioms,
101    compute::all_spec_ensures,
102    function::group_function_axioms,
103    laws_eq::group_laws_eq,
104    laws_cmp::group_laws_cmp,
105    //
106    // Rust types
107    //
108    slice::group_slice_axioms,
109    array::group_array_axioms,
110    string::group_string_axioms,
111    raw_ptr::group_raw_ptr_axioms,
112    layout::group_layout_axioms,
113    //
114    // core std_specs
115    //
116    std_specs::range::group_range_axioms,
117    std_specs::bits::group_bits_axioms,
118    std_specs::control_flow::group_control_flow_axioms,
119    std_specs::slice::group_slice_axioms,
120    std_specs::manually_drop::group_manually_drop_axioms,
121    //
122    // std_specs for alloc (with or without std)
123    //
124    #[cfg(feature = "alloc")]
125    std_specs::vec::group_vec_axioms,
126    #[cfg(feature = "alloc")]
127    std_specs::vecdeque::group_vec_dequeue_axioms,
128    //
129    // std_specs for alloc + std
130    //
131    #[cfg(all(feature = "alloc", feature = "std"))]
132    std_specs::hash::group_hash_axioms,
133}
134
135} // verus!
136// This allows us to use `$crate::vstd` or `crate::vstd` to refer to vstd
137// both in verus_verify_core mode (vstd is a module) and out (vstd is a crate)
138#[cfg(not(verus_verify_core))]
139#[doc(hidden)]
140pub use crate as vstd;
vstd/vstd.rs

vstd/
vstd.rs
