Skip to main content

planarian_schema/
lib.rs

1//! Planarian schema (SPEC ยง8): types, status derivation and the state digest.
2//! No I/O. Intended for the Verus subset: no `dyn`, no `unsafe`, no floats,
3//! integer time.
4
5#![cfg_attr(verus_keep_ghost, verifier::allow(autoderive_clone_without_spec))]
6// Verus idioms: `&Vec` for its `@` view, explicit `match` and nested `if`
7// rather than `matches!` and let-chains.
8#![allow(clippy::ptr_arg, clippy::match_like_matches_macro, clippy::collapsible_if)]
9
10pub mod authz;
11pub mod backend;
12#[cfg(any(test, feature = "fixtures"))]
13pub mod fixtures;
14pub mod gc;
15pub mod ids;
16pub mod pathmap;
17pub mod spec;
18pub mod state;
19pub mod transition;
20pub mod txn;
21pub mod unit;
22
23pub use authz::*;
24pub use backend::*;
25pub use ids::*;
26pub use pathmap::PathMap;
27pub use state::*;
28pub use transition::*;
29pub use txn::*;
30pub use unit::*;