I6 · At most one generation-changing transaction is active (a generation transaction waiting …
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
At most one generation-changing transaction is active (a generation transaction waiting in
Builtfor an activation window, or inAwaitingBoot, counts as active); no transition executes while a transaction is in any mutating or checking state:Activating,Checking,Publishing,Published,Promoted, orReverting. Unit and device repairs may execute duringBuiltandAwaitingBoot, and during a boot-onlyPromoted(admitted at boot, awaiting its confirmation; owner decision, 31 Oct): that change is already fully in place. (This list is the one the ledger enforces; v4.5’s omittedChecking.)— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 7 : 5 (baseline 7 : 5, not degraded) | 9 entries, 9 must-pass |
How it is proved
7 obligations, in crates/txn/src/ledger.rs, crates/txn/src/machine.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
validate | verified fn | (no doc comment) | ledger.rs:607 |
apply | verified fn | Validate, then apply. The record is consumed: the ledger keeps its parts. | ledger.rs:915 |
well_formed | verified fn | The ledger invariant, checked: used on a checkpoint read from disk. | ledger.rs:534 |
i6_one_generation_active | proof fn | I6, as SPEC §7 states it, from the invariant: of two live generation transactions at most one is active (in flight, or waiting in Built); and while a generation transaction is in flight other than awaiting a boot, no other transaction is in flight. | ledger.rs:1235 |
compatible_exec | verified fn | (no doc comment) | ledger.rs:460 |
only_generations_publish | proof fn | Only generation operations publish a boot entry (also a one-shot one) or promote overrides. | machine.rs:182 |
boot_only_never_activates | proof fn | A boot-only candidate is never live-activated: Publishing is journaled before any boot mutation (R01), AwaitingBoot is reached only through it, and left only for Promoted or a revert. | machine.rs:194 |
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 |
|---|---|---|---|
| V3 | Serde impls are unverified (external_derive) | Proof-validity | I5, I14 |
| V4 | Expectation, CheckContext, ApprovalToken, Incident are opaque external types | Proof-validity | — |
| V5 | Ledger bookkeeping helpers (push_tag, tag_string, note_why, archive, set_override, lift_override, record_incident, use_token) are external_body with no postcondition: each receives only the field it updates, so the verified fields are untouched by construction; trusted only to terminate | Proof-validity | I12 |
| V6 | vstd’s specifications of Vec::push, insert, remove, is_empty and Box | Proof-validity | — |
| P4 | Journal fsync is durable and the preallocation is writable | Platform | I7, I12, I15, I18, I24, I25 |
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 |
|---|---|---|---|---|
boot-only-admitted-not-confirmed | fake | A boot-only kernel change boots and is admitted (Promoted: the candidate is the default, its override promoted). sshd then crashes; repairs run while the admitted change is unconfirmed, so sshd is restarted at once, but a canonical unit that needed a repair counts against the change: at the 10-minute checkpoint it is withdrawn, never committed: Reverted, the publishing generation is the default again, the base override restored, and a notice names sshd and says a restart completes it. | boot_default: base; notices_count: count 1, match not confirmed (service:sshd needed a repair before the 10-minute checkpoint); txn: Reverted ApplyChange, service:sshd Committed RestartUnit; units: service:sshd Running | fake: PASS |
boot-only-repair-during-confirmation | fake | A boot-only kernel change boots and is admitted. Two minutes later gym-web (not canonical) crashes: it is repaired at once, without waiting for the 10-minute checkpoint, and the change is still confirmed and committed there. | agrees: true; boot_default: candidate; generation: candidate; txn: Committed ApplyChange, service:gym-web Committed RestartUnit; units: service:gym-web Running | fake: PASS |
crash-activating-bad | fake, vm | planariad is killed during Activating of a bad candidate; the watchdog takes the lease, fences, confirms quiescence, and reverts. | boot_default: base; generation: base; invariants: I6, I12, I15; journal_agrees: true; override_source: base; txn: Reverted ApplyChange; units: service:gym-web Running | fake: PASS; VM: not run in this build |
crash-activating-good | fake, vm | planariad is killed during Activating of a good candidate. The watchdog sees the candidate active, goes to Checking, the probes pass, and it runs the entire commit path. | boot_default: candidate; generation: candidate; invariants: I6, I12, I15; journal_agrees: true; override_source: candidate; txn: Committed ApplyChange | fake: PASS; VM: not run in this build |
crash-slow-worker-overlap | fake, vm | The daemon is killed and immediately restarted while a deliberately slow activation worker survives. The new owner fences it, so activation and revert never overlap and the old owner can never commit. | generation: base; invariants: I6, I15; journal_agrees: true; no_overlap: activate_live(candidate), activate_live(revert_to); stale_owner_commit: false | fake: PASS; VM: not run in this build |
crash-withheld-job-reply | fake | The backend accepts an activation job but its reply is withheld, and the owner is killed before the job id is journaled. Recovery must discover the job by its OpId, or fence it, before making any conflicting mutation. | invariants: I6, I15; journal_agrees: true; no_overlap: activate_live(candidate), activate_live(revert_to); quiescence_includes_tagged_jobs: true | fake: PASS |
en-i6-repair-waits-for-activation | fake, vm | While a slow generation change sits in Activating, gym-web crashes. No repair is prepared until the activation leaves the exclusive states; by the end gym-web runs again. | txn: service:gym-web RestartUnit; units: service:gym-web Running | fake: PASS; VM: not run in this build |
fake-assumptions-conformance | fake | The transaction kernel against the fake backend, once per docs/assumptions.md entry and injected outcome. Each run must satisfy the entry’s contract and reach a terminal state (I12). | invariants: I6, I12, I15; reports: AssumptionHeld(<assumption>) | fake: PASS |
quiet-staged-update-foreground | fake | alice changes her font scale while a game holds Foreground in her session. The verified candidate waits in Built; once Foreground ends it activates in that window and commits. | reports: WaitsForWindow; txn: Committed ApplyChange | fake: PASS |
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 |
| v4.6 | I6 and §12 Concurrency carry the same exclusive-state list, now including Checking and Publishing |
| v4.6 | I6, §10, §12 Concurrency (owner decision, Oct 31): unit and device repairs run during a boot-only Promoted, and a canonical unit that needed a repair since admission means the change is not confirmed |
See also
planarian_txn::ledger in rustdoc · planarian_txn::machine in rustdoc