I1 · A boot-confirmed known-good generation always exists, is bootable, and is in the boot menu
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
A boot-confirmed known-good generation always exists, is bootable, and is in the boot menu; an
accepted_baselinenever 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.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | D | 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 |
|---|---|---|---|
| P3 | publish_boot and the override promotion rename are idempotent | Platform | I16, I23 |
| P8 | The kernel and systemd are correct | Platform | I2, I3, I9, I17, I20, I22 |
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
boot-only-kernel-boot-fails | fake | The same change, but the one-shot boot fails; the boot loader falls back to the default (the base), and the transaction is Reverted. | boot_default: base; generation: base; txn: ApplyChange | fake: PASS |
desktop-boot-fails-rollback | vm | A committed change that touches only boot (a kernel parameter) becomes live_tested but not known_good. After a reboot the greeter fails; the boot is not confirmed, Rollback goes to known_good, and after a second reboot the desktop works. | boot_default: known_good; generation: known_good; known_good: unchanged; reports: NotBootConfirmed; txn: Committed Rollback; units: service:display-manager Running | VM: not run in this build |
floor-revert-blocked | fake | A security update (gym-vulnlib 1.0 → 1.1, the old build carries knownVulnerabilities) commits and raises the floor. gym-web then crashes and fails every restart. The only rollback target, known_good, is below the floor: no Rollback runs, the incident escalates with RevertBlockedByFloor, and the boot default stays at the floor. | boot_default: candidate; escalation: RevertBlockedByFloor; generation: candidate; incident: service:gym-web; invariants: I1, I16; security_floor: candidate; txn: Committed ApplyChange, Rollback | fake: PASS |
Also tested by exec::tests (vm-generations).
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
| Spec | Change |
|---|---|
| v4 | Restored principles (now 12) and invariants (I1–I14) that v3 referenced but omitted |
| v4.4 | I1 and I6 clarified against the floor and waiting transactions |