Crate planarian_txn 

Planarian transaction kernel (SPEC §12, §12c).

• machine: which journal state may follow which. Pure; a Verus target.
• ledger: journal records and the live state they establish. Its validate enforces I6, I15 and the recovery interlock on every record.
• journal: the write-ahead, CRC-framed, preallocated log, with checkpoint-then-truncate compaction.
• store: durable storage (in-memory for the fake harness, files on disk).
• kernel: drives one transaction through execution, takeover and the crash-recovery table, over a Host that provides backends and probes.
• fake: in-memory backends for the fake harness.

Modules

chain

The journal’s hash chain as a decision (I18), apart from the I/O in journal.rs. Hashing stays outside: SHA-256 is trusted (P5), so each record enters as a Link carrying the head it claims to follow (prev) and the head after it (next, from journal::chain). What is proved here is everything else: a record follows exactly when its seq is the next one and its prev is the current head; a segment is accepted exactly when every record follows, and otherwise the first that does not is reported; and what the writer appends always follows.

fake

In-memory fake backends for the txn-kernel harness (catalog harness = "fake").

journal

The write-ahead journal (§12, §12c).

kernel

Driving one transaction through the journal (§12 step 7, step 8, the crash-recovery table, ownership and fencing).

ledger

Journal records and the ledger they build (§12, §12c).

machine

The journal state machine: which TxnState may follow which (§12). Pure; a Verus proof target (I12 paths, write-ahead ordering).

store

Durable storage under the journal (§12c): a preallocated log, an atomically replaced checkpoint, a fixed-size RecoveryFailed sentinel, and the per- transaction fence epochs that backends check before mutating.