Module ledger 

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

The ledger is the live state the journal establishes. A checkpoint is the serialized ledger, so replaying (checkpoint + tail) and replaying the full history produce equal ledgers by construction.

validate runs before a record is written (write-ahead) and again on replay. It enforces I6, I15 and the recovery interlock at the journal itself, so no caller can journal a step that breaks them.

Verified with Verus (docs/verification.md): validate accepts a record only when rules hold, and apply preserves inv (I6 among the live transactions, unique ids, leases naming their transaction). Bookkeeping no invariant reads (the terminal archive, overrides, incidents, tokens) is done by small unverified helpers that cannot reach the verified fields.

Structs

Entry

IdMap

A map from transaction id, stored as a vector sorted by id; vstd specifies BTreeMap only for keys with an ordering spec, which TxnId lacks. Serialized as the JSON object the BTreeMap was.

InterlockEntry

An unresolved RecoveryFailed (§12c). While any exists, autonomous mutation is blocked.

Ledger

LiveTxn

OpRecord

Reconciliation

What a restarted owner found and did (§12 daemon restart reconciliation).

TerminalTxn

What remains of a terminal transaction: enough to refuse stale epochs and to show the outcome. Bounded to the most recent TERMINAL_KEEP.

Enums

HoldBy

Who applied a hold: systemd’s OnFailure= (seen by the daemon) or the daemon itself, for a stop outside Planarian that is not attributed.

LedgerError

Record

Constants

TERMINAL_KEEP

Functions

archive 🔒

compatible_exec 🔒

find 🔒

flying_exec 🔒

is_autonomous 🔒

lift_override 🔒

note_why 🔒

op_eq 🔒

push_tag 🔒

put 🔒

Insert or replace, keeping the entries sorted by id.

record_incident 🔒

recovery_eq 🔒

set_override 🔒

stale 🔒

tag_string 🔒

use_token 🔒