I15 · Exactly one owner (lease) per transaction
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Exactly one owner (lease) per transaction; a mutating call with a stale epoch is refused; only the lease holder advances the journal.
— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof) | 2 : 2 (baseline 2 : 2, not degraded) | 7 entries, 7 must-pass |
How it is proved
2 obligations, in crates/txn/src/kani.rs, crates/txn/src/ledger.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
validate | verified fn | (no doc comment) | ledger.rs:607 |
takeover_fences_out_the_previous_owner | Kani harness | Fencing (I15): a takeover’s epoch is above both the journaled lease and the store’s fence; once the fence holds it, the previous owner’s epoch and every other epoch are refused and the new owner’s admitted; a second takeover fences out the first. Epoch arithmetic never overflows: at the end of the epoch space a takeover backs off instead. | kani.rs:225 |
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, I7, I12, I18, I24, I25 |
| P7 | Fencing is effective: a stale-epoch call is refused before it mutates | Platform | I12 |
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 |
|---|---|---|---|---|
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-simultaneous-takeover | fake, vm | The daemon and the watchdog try to take over at the same moment; exactly one wins the flock and the other backs off. | invariants: I15; journal_agrees: true; lease_epochs_strictly_increasing: true; owners_per_epoch_max: 1 | 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-i15-old-worker-cannot-finish | fake, vm | The daemon is killed mid-activation and stays down; the watchdog takes the generation change over while the old activation worker is still running. From the takeover on, only the watchdog’s lease advances the transaction or journals a call, the old worker’s activation never overlaps the watchdog’s revert, and each epoch has one owner. | journal_owner_after_takeover: watchdog; no_overlap: activate_live(candidate), activate_live(revert_to); owners_per_epoch_max: 1 | 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 |
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-13 | The network hold (§12d Network security fails closed): planariad applies and lifts planarian-hold@<unit> with no Prepared record, no lease and no op tag, mirroring systemd’s OnFailure=; the hold drops connectivity without asking | Accepted | Accepted | A |