vstd 0.0.0-2025-11-05-1950

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

//! The "standard library" for [Verus](https://github.com/verus-lang/verus).
//! Contains various utilities and datatypes for proofs,
//! as well as runtime functionality with specifications.
//! For an introduction to Verus, see [the tutorial](https://verus-lang.github.io/verus/guide/).
#![cfg_attr(not(feature = "std"), no_std)]
#![allow(unused_parens)]
#![allow(unused_imports)]
#![allow(dead_code)]
#![allow(unused_attributes)]
#![allow(rustdoc::invalid_rust_codeblocks)]
#![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
#![cfg_attr(any(verus_keep_ghost, feature = "allocator"), feature(allocator_api))]
#![cfg_attr(verus_keep_ghost, feature(step_trait))]
#![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
#![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))]
#![cfg_attr(verus_keep_ghost, feature(freeze))]
#![cfg_attr(verus_keep_ghost, feature(derive_clone_copy))]
#![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(liballoc_internals))]
#![cfg_attr(verus_keep_ghost, feature(new_range_api))]

#[cfg(feature = "alloc")]
extern crate alloc;

pub mod arithmetic;
pub mod array;
pub mod atomic;
pub mod atomic_ghost;
pub mod bits;
pub mod bytes;
pub mod calc_macro;
pub mod cell;
pub mod compute;
pub mod contrib;
pub mod float;
pub mod function;
#[cfg(all(feature = "alloc", feature = "std"))]
pub mod hash_map;
#[cfg(all(feature = "alloc", feature = "std"))]
pub mod hash_set;
pub mod invariant;
#[cfg(verus_keep_ghost)]
pub mod laws_cmp;
#[cfg(verus_keep_ghost)]
pub mod laws_eq;
pub mod layout;
pub mod logatom;
pub mod map;
pub mod map_lib;
pub mod math;
pub mod modes;
pub mod multiset;
pub mod multiset_lib;
pub mod pcm;
pub mod pcm_lib;
pub mod pervasive;
pub mod proph;
pub mod raw_ptr;
pub mod relations;
pub mod rwlock;
pub mod seq;
pub mod seq_lib;
pub mod set;
pub mod set_lib;
pub mod shared;
#[cfg(feature = "alloc")]
pub mod simple_pptr;
pub mod slice;
pub mod state_machine_internal;
pub mod storage_protocol;
pub mod string;
#[cfg(feature = "std")]
pub mod thread;
pub mod tokens;
pub mod view;

#[cfg(verus_keep_ghost)]
pub mod std_specs;

// Re-exports all vstd types, traits, and functions that are commonly used or replace
// regular `core` or `std` definitions.
pub mod prelude;

use prelude::*;

verus! {

#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
pub broadcast group group_vstd_default {
    //
    // basic Verus math, types, and features
    //
    seq::group_seq_axioms,
    seq_lib::group_seq_lib_default,
    map::group_map_axioms,
    set::group_set_axioms,
    set_lib::group_set_lib_default,
    multiset::group_multiset_axioms,
    compute::all_spec_ensures,
    function::group_function_axioms,
    laws_eq::group_laws_eq,
    laws_cmp::group_laws_cmp,
    //
    // Rust types
    //
    slice::group_slice_axioms,
    array::group_array_axioms,
    string::group_string_axioms,
    raw_ptr::group_raw_ptr_axioms,
    layout::group_layout_axioms,
    //
    // core std_specs
    //
    std_specs::range::group_range_axioms,
    std_specs::bits::group_bits_axioms,
    std_specs::control_flow::group_control_flow_axioms,
    std_specs::slice::group_slice_axioms,
    //
    // std_specs for alloc (with or without std)
    //
    #[cfg(feature = "alloc")]
    std_specs::vec::group_vec_axioms,
    #[cfg(feature = "alloc")]
    std_specs::vecdeque::group_vec_dequeue_axioms,
    //
    // std_specs for alloc + std
    //
    #[cfg(all(feature = "alloc", feature = "std"))]
    std_specs::hash::group_hash_axioms,
}

} // verus!
// This allows us to use `$crate::vstd` or `crate::vstd` to refer to vstd
// both in verus_verify_core mode (vstd is a module) and out (vstd is a crate)
#[cfg(not(verus_verify_core))]
#[doc(hidden)]
pub use crate as vstd;