§7. Principles and invariants
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Principles
- The healer is not the patient. The repair core is outside the blast radius of anything it changes; no generation or proposal can modify it.
- The model proposes; machinery disposes. Model output is a typed proposal, never a command.
- Machinery before model. Deterministic code handles everything it can; the model is a fallback.
- Desired, observed, and healthy are three different things. Never collapse them.
- Every change is a transaction. Journaled before, probed after, reverted on failure, recoverable if the daemon dies.
- Authority is derived, never supplied. The executor computes what a change touches and how risky it is from the evaluated configuration; no field of a proposal or of any other request carries authority or identity.
- Sensor input is data, never instructions.
- Degrade to a working machine. Without the model, the console, or the network, the system boots, runs, repairs simple faults, and reverts.
- Don’t fight the user. A deliberate stop, disable, unmount, or disconnect is an override of desired state, not a fault, provided it reaches the journal with the actor’s identity before it takes effect (§11).
- Disruption is a cost. Prefer the least disruptive repair; surface disruption before acting.
- The oracle is protected. Nothing a proposal can do may weaken a canonical probe.
- Grow into the hardware.
- The executor is a reference monitor. It is always invoked, tamperproof, and small enough to verify. Everything above the verified core is a principal with an authenticated identity, a set of capabilities, and a reputation; authority is derived below that line and never held above it. The rule is species-blind: it applies the same way to users, root acting through Planarian, apps, the on-device model, and remote agents.
- Invisible under normal use. Planarian’s overhead, notifications, and effect on foreground work are measured and may not get worse; non-urgent work waits while the user is absorbed in something.
- The response to the monitor failing cannot depend on the monitor. Failure posture is declared in the generation and enforced by systemd and the initrd.
- Name every way around. A guarantee is stated only as widely as it holds; each route around it is a row in
docs/bypasses.mdwith its phase, and no gate passes with an open High row.
Invariants (checked by txn and policy; each is a test in gym and, where marked, a proof)
| ID | Invariant | Proof |
|---|---|---|
| I1 | A boot-confirmed known-good generation always exists, is bootable, and is in the boot menu; an accepted_baseline never replaces it there. It may lag the security floor until the floor generation is boot-confirmed (§12e); it is then a manual fallback, never an automatic one. | D |
| I2 | The installed core package’s hash equals the hash recorded in its signature. In A–D the reference hash is recorded by the build and covers every Planarian binary and script (§12d); it detects a swapped file, not a rebuilt generation. | E |
| I3 | Garbage collection never removes known-good, the previous generation, the current generation, an in-flight candidate, or the boot model. | A (test), D (proof) |
| I4 | Running means desired-Running under the current conditions, observed-active, and every applicable Readiness probe passed with fresh evidence. Diagnostic probes never determine Running. | A |
| I5 | Forbidden actions are unrepresentable as transitions; Decision::Reject is never converted to any tier by any setting. | A (proof) |
| I6 | At most one generation-changing transaction is active (a generation transaction waiting in Built for an activation window, or in AwaitingBoot, counts as active); no transition executes while a transaction is in any mutating or checking state: Activating, Checking, Publishing, Published, Promoted, or Reverting. Unit and device repairs may execute during Built and AwaitingBoot, and during a boot-only Promoted (admitted at boot, awaiting its confirmation; owner decision, 31 Oct): that change is already fully in place. (This list is the one the ledger enforces; v4.5’s omitted Checking.) | A (proof) |
| I7 | Every executed transition is logged with proposal, source, pre- and post-state, derived facts, policy version, probe evidence (per probe: id, result, time), decision, and outcome; an approved transition’s log and journal records name the approver’s principal and the token’s bound_to. | A |
| I8 | A tier-3 transition executes only with an approval token bound to the concrete candidate (§12), re-validated immediately before execution. “Immediately before execution” includes the moment a transaction leaves Built after waiting for an activation window: facts are re-derived, decide re-run and the stale check repeated there too, not only at approval. | A, C (proof) |
| I9 | The model process holds exactly one write capability: submit a proposal. | B (by the sandbox, §20, and a gym case), E (proof) |
| I10 | No change that removes or alters a canonical probe executes below AskFirst, and canonical probes are evaluated from the installed core package regardless of the active generation. | A |
| I11 | A session’s cumulative effect is classified at least as high as any single transition producing it. | A (proof) |
| I12 | Under the progress assumptions of §17a, every transaction in the journal reaches a terminal state (Committed, Reverted, Rejected, Cancelled, or RecoveryFailed); RecoveryFailed always alerts and sets the recovery interlock. Two states wait on events outside the system’s control and are bounded separately (§12f): a transaction in Built waiting for an activation window is Cancelled(Daemon) after the parking limit; one in AwaitingBoot waits for the reboot it was published for and is reported as waiting, never as a recovery failure. | A (proof, conditional) |
| I13 | A unit under an override is never a repair target while the override holds. | A, C (proof) |
| I14 | Policy facts (sensitivity, affected units, manifest-touching, caller identity) are derived by the executor from the evaluated generation and the authenticated peer, never read from a proposal or from any other request field. | A (proof of the decide half; the request half by test) |
| I15 | Exactly one owner (lease) per transaction; a mutating call with a stale epoch is refused; only the lease holder advances the journal. | A (proof) |
| I16 | No automatic revert, rollback, or boot fallback selects a generation below the security floor; going below it requires administrator approval (§12e). The floor is derived from the whole system closure (§12e); a fix outside the inspected set does not move it. | A (proof of the decide and target-selection parts; the bootloader part by test) |
| I17 | The set of principals holding administrator capability is never empty. | A (proof, given root exists) |
| I18 | Every journal record commits to the hash of its predecessor; a broken chain is detected on read and treated as an integrity failure (§12c, §12d). This holds against damage and against anyone who cannot rewrite the whole journal and checkpoint consistently; root can, until the head is anchored off the disk (§12c). | A (proof, trusting SHA-256) |
| I19 | No principal approves its own proposal, and no principal grants itself, or a principal it controls, a capability it does not hold. | A (proof), C |
| I20 | No agent (the on-device model, a remote relay, or any agent started by planarian agent run) starts while planarian-ready.target is not reached, and every running agent is stopped when a failure posture engages, in every posture (§12d). Agents the launcher creates are inside this rule exactly as the units declared in services.planarian.agentUnits (the model service and any relay) are. | A |
| I21 | No transition that cannot be reversed, or that may lose a session, user data or connectivity, executes below AskFirst, unless the loss falls only on the caller’s own session (and, for connectivity, the caller has a seat); a loss reaching another user’s session requires administrator approval (§11 floors). Garbage collection of generations outside the protected set is Runtime by §12b, not irreversible loss in this sense (owner decision, 2026-10-30); gc.retainAllGenerations keeps every generation. | A (proof) |
| I22 | Changing the generation, collecting garbage, binding drivers, resolving the recovery interlock and overriding a Security-sensitive unit are administrator operations; a Security-sensitive unit is changed without approval only to restore its declared state (§11); the unattributed actor holds no authority, and an agent holds exactly its user’s (§11). | A (proof) |
| I23 | A generation transaction commits only after its boot entry is written and promoted; a runtime transaction never publishes, promotes or reverts; the override file is replaced only under the daemon’s exclusive lock on its directory and only when its content hash is the one recorded at Prepared (§9 step 4). A writer that does not take the lock is outside this guarantee (docs/bypasses.md, X-12). | A (proof) |
| I24 | An agent’s authority is bound to the one AgentStarted record for the unit instance it runs in, identified by that instance (not by name); a second start under the same name neither rebinds a running agent nor is journaled before it has succeeded (§11, §16). | A |
| I25 | Post-commit bookkeeping (security-floor derivation, the committed generation’s override content, session accounting) runs on every path that writes Committed for a generation transaction: the daemon’s, the watchdog’s, the boot-only confirmation’s. A commit whose floor record cannot be appended does not commit (§12, §12e). | A |