I21 · No transition that cannot be reversed, or that may lose a session, user data or connecti…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
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.retainAllGenerationskeeps every generation.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 2 : 4 (baseline 2 : 4, not degraded) | 4 entries, 4 must-pass |
How it is proved
2 obligations, in crates/policy/src/proofs.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
global_floors | proof fn | The global floors (§11), for every transition kind. | proofs.rs:129 |
own_session_is_per_session | proof fn | “Own session” is per session: a user whose other session (or no session) would be disrupted gets the floor, and so does a disruption whose sessions are not known. | proofs.rs:143 |
What it rests on
If any of these is false, the proof no longer describes the real machine.
| Id | Assumption | Kind | Also relied on by |
|---|---|---|---|
| V1 | vstd’s specifications of Vec, String::as_str, str::unicode_len, str::get_char | Proof-validity | I5, I10, I11, I16, I19, I22 |
| V2 | Value is an opaque external type (external_type_specification); nothing about it is assumed | Proof-validity | I5, I11, I16 |
| U1 | exec::derive: DerivedFacts from the evaluated generation, never from a proposal (I14’s other half; property-tested) | Internal unproven | I10, I14, I22 |
| U5 | Identity resolution (§10): peer credentials and pidfd to logind session, seat, terminal | Internal unproven | I19, I24 |
Every proof also rests on V7 (The specifications the proofs prove against (decide_spec, step_spec, inv, chained, the lemma statements) say what the SPEC’s English means), V8 (Verus is sound: what it reports verified holds of the code), V9 (Z3, the solver Verus calls, is sound), V10 (rustc compiles the verified code to a program with the semantics Verus checked).
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
en-i21-irreversible-asks-even-for-root | fake | Root, at maximum autonomy, asks to restore a snapshot over user data: it cannot be reversed. It is held at AskFirst, whoever asks and whatever the setting. | txn: RestoreSnapshot | fake: PASS |
gc-retain-all-generations | fake | With services.planarian.gc.retainAllGenerations set and the generation budget far below what the generations use, four display-scale changes leave old generations behind; garbage collection then collects none of them (the full history stays), and reports the budget as unsatisfiable rather than enforcing it. | collected_none: true; reports: BudgetUnsatisfiable; txn: Committed CollectGarbage | fake: PASS |
identity-peer-exited | vm | alice, logged in at the seat, sends a stop of her own pipewire and exits before the daemon resolves her. With no process behind the connection, the daemon attributes the request to uid 1000 with no session: never to a session it cannot read from that process. | txn: StopAndSuppress | VM: not run in this build |
override-stopped-equals-stop | fake, vm | An administrator with no session here (over SSH) asks, in turn, for an override that stops the display manager and for a plain stop of it. Both end the seated user’s session: both derive SessionLoss over the same units and both are held at AskFirst, since it is not the caller’s own session. | txn: SetOverride, StopAndSuppress; units: service:display-manager Running | fake: PASS; VM: not run in this build |
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| B-4 | decide is proved, but its inputs (DerivedFacts, Authorization) are computed by unproven code | Medium | Open (v4.5 §17a) | A accounting; C proof |
| X-1 | Root edits the store, /boot, the binaries, the journal or the posture state | Accepted | Accepted | E |
| X-2 | A nixos-rebuild outside Planarian | Accepted | Accepted | C |
| X-4 | Physical access | Accepted | Accepted | E |
| X-6 | The supply chain: nixpkgs content, cache signatures, input-addressed store paths | Accepted | Accepted | — |
| X-7 | Backends report success falsely; systemd or the kernel misbehave (P1, P6, P8) | Accepted | Accepted | D, E |
| X-13 | The network hold (§12d Network security fails closed): planariad applies and lifts planarian-hold@<unit> with no Prepared record, no lease and no op tag, mirroring systemd’s OnFailure=; the hold drops connectivity without asking | Accepted | Accepted | A |
History
No changes section names it.