Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166//! 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;