I3 · Garbage collection never removes known-good, the previous generation, the current genera…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Garbage collection never removes known-good, the previous generation, the current generation, an in-flight candidate, or the boot model.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | A (test), D (proof) | 0 : 2 (baseline 0 : 2, not degraded) | 3 entries, 2 must-pass |
How it is proved
No obligation discharges it: nothing about it is proved.
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 |
|---|---|---|---|
| P1 | Backend Outcome is honest: Succeeded means applied; Unknown means the backend cannot say | Platform | I12, I25 |
| P8 | The kernel and systemd are correct | Platform | I1, I2, I9, I17, I20, I22 |
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
gc-during-approval | fake, vm | Garbage collection runs while an AskFirst change waits for approval. The candidate survives (its build root is protected), and after approval verify_candidate passes. | gc_protected: candidate, known_good, base; generation: candidate; txn: Committed ApplyChange | fake: PASS; VM: not run in this build |
storage-budget-unsatisfiable | fake, vm | The generation budget is set below the size of the protected set. GC collects everything unprotected, reports BudgetUnsatisfiable with the shortfall, and never touches the protected set. | gc_protected: known_good, base, previous; reports: BudgetUnsatisfiable | fake: PASS; VM: not run in this build |
storage-nix-full-gc | fake, vm | The Nix store filesystem drops below max(2 GB, 5%) while old generations exist. CollectGarbage runs first, and the protected set is untouched. | gc_protected: known_good, base, previous; txn: Committed CollectGarbage; units: device:fs-nix Running | fake: PASS; VM: not run in this build |
Also tested by schema::gc tests.
Known limits
| Bypass | Route | Severity | Status | Closes in |
|---|---|---|---|---|
| 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 |
History
See also
—