vstd/
vstd.rs

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

vstd/
vstd.rs
