planarian_txn/lib.rs
1//! Planarian transaction kernel (SPEC §12, §12c).
2//!
3//! - `machine`: which journal state may follow which. Pure; a Verus target.
4//! - `ledger`: journal records and the live state they establish. Its
5//! `validate` enforces I6, I15 and the recovery interlock on every record.
6//! - `journal`: the write-ahead, CRC-framed, preallocated log, with
7//! checkpoint-then-truncate compaction.
8//! - `store`: durable storage (in-memory for the fake harness, files on disk).
9//! - `kernel`: drives one transaction through execution, takeover and the
10//! crash-recovery table, over a `Host` that provides backends and probes.
11//! - `fake`: in-memory backends for the fake harness.
12
13#![cfg_attr(verus_keep_ghost, verifier::allow(autoderive_clone_without_spec))]
14// Verus idioms: `&Vec` for its `@` view, explicit `match` and nested `if`
15// rather than `matches!` and let-chains.
16#![allow(clippy::ptr_arg, clippy::match_like_matches_macro, clippy::collapsible_if, clippy::single_match)]
17
18pub mod chain;
19pub mod fake;
20pub mod journal;
21pub mod kernel;
22pub mod ledger;
23pub mod machine;
24pub mod store;
25
26#[cfg(kani)]
27mod kani;