//! 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(unused_features)] // silences spurious warnings for features that cause errors when omitted #![allow(rustdoc::invalid_rust_codeblocks)] #![cfg_attr(verus_keep_ghost, feature(atomic_internals))] #![cfg_attr(verus_keep_ghost, feature(generic_atomic))] #![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(sized_hierarchy))] #![cfg_attr(verus_keep_ghost, feature(freeze))] #![cfg_attr(verus_keep_ghost, feature(derive_clone_copy_internals))] #![cfg_attr(verus_keep_ghost, feature(derive_eq_internals))] #![cfg_attr(verus_keep_ghost, feature(slice_index_methods))] #![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(liballoc_internals))] #![cfg_attr(verus_keep_ghost, feature(nonzero_internals))] #![cfg_attr(verus_keep_ghost, feature(hint_must_use))] #![cfg_attr(verus_keep_ghost, feature(fmt_internals))] #![cfg_attr(verus_keep_ghost, feature(fmt_arguments_from_str))] #![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(btree_cursors))] #![cfg_attr(verus_keep_ghost, feature(panic_internals))] #[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 endian; pub mod float; pub mod function; #[cfg(feature = "std")] pub mod future; #[cfg(all(feature = "alloc", feature = "std"))] pub mod hash_map; #[cfg(all(feature = "alloc", feature = "std"))] pub mod hash_set; pub mod imap; pub mod imap_lib; pub mod invariant; pub mod iset; pub mod iset_lib; #[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; #[cfg(verus_keep_ghost)] pub mod mut_ref; pub mod pervasive; pub mod predicate; pub mod proph; pub mod raw_ptr; pub mod relations; pub mod resource; 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 string; #[cfg(feature = "std")] pub mod thread; pub mod tokens; pub mod utf8; pub mod view; pub mod wrapping; #[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_lemmas, seq_lib::group_seq_lib_default, map::group_map_lemmas, set::group_set_lemmas, imap::group_imap_lemmas, iset::group_iset_lemmas, 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, #[cfg(not(verus_verify_core))] string::group_string_axioms, raw_ptr::group_raw_ptr_axioms, layout::group_layout_axioms, mut_ref::group_mut_ref_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::fmt::group_fmt_axioms, std_specs::manually_drop::group_manually_drop_axioms, std_specs::iter::group_iter_axioms, std_specs::nonzero::group_nonzero_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, #[cfg(feature = "alloc")] std_specs::btree::group_btree_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;