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#![feature(sized_hierarchy)]
5#![feature(proc_macro_hygiene)]
6#![allow(non_snake_case)]
7#![allow(unused_parens)]
8#![allow(unused_braces)]
9#![allow(rustdoc::invalid_rust_codeblocks)]
10#![allow(rustdoc::invalid_html_tags)]
11#![allow(rustdoc::broken_intra_doc_links)]
12
13extern crate alloc;
14
15pub mod arithmetic;
16pub mod array_ptr;
17pub mod auxiliary;
18pub mod bit_mapping;
19pub mod cast_ptr;
20pub mod extern_const;
21pub mod external;
22pub mod function_properties;
23pub mod ghost_tree;
24pub mod ownership;
25pub mod resource;
26pub mod undroppable;
27
28#[macro_use]
29pub mod ptr_extra;
30pub mod map_extra;
31
32pub mod prelude;
33pub mod raw_ptr_extra;
34pub mod seq_extra;
35pub mod set_extra;
36pub mod state_machine;
37pub mod std_extra;
38pub mod temporal_logic;