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