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

vstd/
vstd.rs
