Crate planarian_schema 

Planarian schema (SPEC §8): types, status derivation and the state digest. No I/O. Intended for the Verus subset: no dyn, no unsafe, no floats, integer time.

Re-exports

pub use pathmap::PathMap;

pub use authz::*;

pub use backend::*;

pub use ids::*;

pub use state::*;

pub use transition::*;

pub use txn::*;

pub use unit::*;

Modules

authz

Principals, capabilities and failure posture (§8, §11, §12d).

backend

Backend contracts (§8). Generic parameters only; no dyn (§6).

gc

Garbage-collection planning under the §12b bounds. Pure: the backends measure, this decides.

ids

Identifiers, hashes and time.

pathmap

PathMap: a map keyed by option path, stored as a vector sorted by key.

spec

Per-transition preconditions and predictions (§8 TransitionSpec, the pure half). Shared by the diagnoser, which builds proposals, and the executor, which checks that a proposal’s expected refines predict (§12 step 3). Derivation of facts needs the evaluated generation and lives in exec.

state

Observed state, derived status, and the state digest (§8).

transition

Transitions, decisions, derived facts and proposals (§8).

txn

Transactions, leases, approvals and incidents (§8).

unit

Units, desired state, the graph, risk metadata and probes (§8).