Crate planarian_exec

Expand description

The executor (SPEC §12): the one path by which anything changes.

A Proposal from the diagnoser, the intent matcher or a user goes through the steps below, in this order:

digest check (Stale);
caller identity from the socket, overwriting any actor in the proposal;
for ApplyChange: catalog handler → stage → evaluate → build (read-only);
facts derived from the evaluated generation (I14);
refinement check of expected against predict;
policy::decide;
stale check of the owner’s source, then Prepared (durable);
AskFirst parks with a token bound to the concrete candidate, and approval re-derives everything and compares the binding. Otherwise the kernel runs it to a terminal state.

Modules§

derive: Deriving policy facts (I14): from the evaluated generations and the unit definitions, never from a proposal.
host: The real txn::Host: the kernel’s view of the backends, plus the probe check and re-observation the protocol needs (§9 executor-owned requirements, §12 step 7). The daemon and the watchdog both use it, so the watchdog can verify a candidate on its own from the journaled CheckContext.
residue: The residue classifier (§11, owner decision Q5; U3 in docs/assumptions.md): which unit endings Planarian did not cause are a person’s stop, taken as intended until the next boot, and which are faults or alarms. Pure, so its rules are checked by Kani (kani.rs) in Phase A and by Verus in C.

Candidate: What stage, evaluate and build produced for a catalog change.
Config
Executor
Parked
Plan 🔒: Everything decided before a transaction exists.
PrebuildJob: The slow, pre-journal part of planning a catalog change (§9 steps 1–3: stage, evaluate, build), detached from the executor so the daemon can run it on another thread while its core keeps observing and repairing. It touches no journal: a candidate is only a store path and a GC root until a transaction is prepared for it.
Prebuilt: A PrebuildJob’s result.

Submitted: Parked carries the derived facts for display; results are rare and short-lived, so the size difference between variants doesn’t matter.

build_candidate 🔒
outcome_msg 🔒
reject 🔒
token_expired
unmet: An approval token issued at issued has expired by now, both on the boot clock (§12h; §12 step 4: 24 hours). Saturating: a token issued near the end of time never expires early, and no clock value makes this panic. Why t’s precondition does not hold for by (§12 step 5), if it does not. An attested override is replaced only by its holder; anyone else gets its holder named (C3).