I23 · A generation transaction commits only after its boot entry is written and promoted
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
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).— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 3 : 1 (baseline 3 : 1, not degraded) | 2 entries, 2 must-pass |
How it is proved
3 obligations, in crates/txn/src/kani.rs, crates/txn/src/machine.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
generations_commit_after_promotion | proof fn | A generation operation commits only after it was published and promoted. | machine.rs:206 |
runtime_never_reverts | proof fn | Runtime operations never revert a generation and never publish (§12). | machine.rs:171 |
override_swap_never_overwrites_a_third_party | Kani harness | The override swap (§9 step 4) never overwrites a file a third party changed: it swaps only when the live file holds the expected source, and is done exactly when it already holds the target. After a completed swap, the revert direction swaps back. | kani.rs:261 |
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 | I1, I16 |
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), V11 (Kani and its back end CBMC are sound within the stated bounds).
How it is tested
| Entry | Harness | What it does | Expects | Latest verdict |
|---|---|---|---|---|
en-i23-third-party-override-kept | fake, vm | Between a change’s boot entry being published and its override promotion, a third party rewrites the override file. Planarian does not overwrite it: the third party’s file stands, and the change does not commit (it stops at RecoveryFailed for a person to resolve). Before it, a runtime restart of gym-web wrote no boot entry. On the VM the third party is a cooperating writer: it holds the lock on planarian/ across the daemon’s compare-and-swap and replaces the file before letting go, so the swap waits and then sees the edit (R11). | override_file: third-party; txn: RecoveryFailed ApplyChange, service:gym-web Committed RestartUnit; units: service:gym-web Running | fake: PASS; VM: not run in this build |
stale-owner-edit-during-build | fake, vm | During the build, the owner edits a tracked file without committing it. The transaction is Rejected(Stale), never activated, and its GC root is released. | gc_root_released: true; generation: base; override_source: base; txn: Rejected(Stale) ApplyChange | fake: PASS; VM: not run in this build |
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 |
| X-12 | A writer that does not take the daemon’s lock on the override directory (an editor, a script) replaces planarian/overrides.nix between the daemon’s comparison and its rename | Accepted | Accepted | C (writer boundary) |
History
| Spec | Change |
|---|---|
| v4.6 | I23: the override CAS is under the daemon’s lock |