I7 · Every executed transition is logged with proposal, source, pre- and post-state, derived …
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
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.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Tested, not proved | A | 0 : 1 (baseline 0 : 1, not degraded) | 0 entries, 0 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 |
|---|---|---|---|
| P4 | Journal fsync is durable and the preallocation is writable | Platform | I6, I12, I15, I18, I24, I25 |
How it is tested
No gym entry exercises it.
Also tested by daemon core 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
| Spec | Change |
|---|---|
| v4 | Restored principles (now 12) and invariants (I1–I14) that v3 referenced but omitted |
| v4.6 | I7: probe evidence per probe and the approver’s identity in the record [C1, C17] |
See also
—