Skip to main content

vstd_extra/
lib.rs

1//! The "extra standard library" for [Verus](https://github.com/verus-lang/verus).
2//! Contains various utilities and general datatypes for proofs useful in Asterinas verification,
3//! as well as extending [Verus standard library(vstd)](https://verus-lang.github.io/verus/verusdoc/vstd) with additional functionality.
4#![no_std]
5#![feature(nonzero_internals)]
6#![feature(sized_hierarchy)]
7#![feature(btree_cursors)]
8#![feature(proc_macro_hygiene)]
9#![cfg_attr(verus_keep_ghost, feature(allocator_api))]
10#![allow(non_snake_case)]
11#![allow(unused_parens)]
12#![allow(unused_braces)]
13#![allow(rustdoc::invalid_rust_codeblocks)]
14#![allow(rustdoc::invalid_html_tags)]
15#![allow(rustdoc::broken_intra_doc_links)]
16
17extern crate alloc;
18
19pub mod arithmetic;
20pub mod array_ptr;
21pub mod atomic_data;
22#[cfg(feature = "irc11")]
23pub mod atomic_irc11;
24pub mod auxiliary;
25pub mod bits;
26pub mod cast_ptr;
27pub mod drop_tracking;
28pub mod external;
29pub mod function_properties;
30pub mod ghost_tree;
31pub mod once;
32pub mod ownership;
33pub mod panic;
34pub mod resource;
35#[cfg(feature = "irc11")]
36pub mod scheduler_thread_view;
37
38#[macro_use]
39pub mod trans_macros;
40pub mod map_extra;
41
42pub mod prelude;
43pub mod range;
44pub mod raw_ptr_extra;
45pub mod rcu_objects;
46pub mod rcu_read_lease;
47pub mod resource_invariant;
48pub mod seq_extra;
49pub mod set_extra;
50pub mod spec_operators;
51pub mod state_machine;
52pub mod sum;
53pub mod temporal_logic;