I12 · Under the progress assumptions of §17a, every transaction in the journal reaches a termi…
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Under the progress assumptions of §17a, every transaction in the journal reaches a terminal state (
Committed,Reverted,Rejected,Cancelled, orRecoveryFailed);RecoveryFailedalways alerts and sets the recovery interlock. Two states wait on events outside the system’s control and are bounded separately (§12f): a transaction inBuiltwaiting for an activation window isCancelled(Daemon)after the parking limit; one inAwaitingBootwaits for the reboot it was published for and is reported as waiting, never as a recovery failure.— SPEC §7
| Status | Proof phase | d:a | Gym |
|---|---|---|---|
| Proved | A (proof, conditional) | 9 : 8 (baseline 9 : 8, not degraded) | 6 entries, 6 must-pass |
How it is proved
9 obligations, in crates/txn/src/kani.rs, crates/txn/src/ledger.rs, crates/txn/src/machine.rs; every one is checked on every CI run.
| Obligation | Kind | What it guarantees | Source |
|---|---|---|---|
i12_steps_terminate | proof fn | I12, termination: every allowed step lowers the rank, so a transaction takes at most eight steps and never cycles. | machine.rs:130 |
i12_terminal_always_reachable | proof fn | I12, progress: from every state that is not terminal, a step to a terminal state is allowed: Cancelled before any mutation, RecoveryFailed after. So whoever holds the lease can always finish the transaction. | machine.rs:141 |
terminal_is_final | proof fn | Terminal states have no successors. | machine.rs:151 |
refusal_only_before_mutation | proof fn | Rejected and Cancelled happen only before anything was mutated, or (for Rejected) from Publishing, whose all-or-nothing publication armed nothing. | machine.rs:161 |
apply | verified fn | Validate, then apply. The record is consumed: the ledger keeps its parts. | ledger.rs:915 |
recovery_table_follows_the_state_machine | Kani harness | The crash-recovery table agrees with the journal state machine: from every state a live transaction can be left in, under every strategy, every path recovery can take starts at that state, takes only steps machine::step_allowed permits (the Verus-verified rules), and ends in a terminal state. Nothing mutated is ever answered with a refusal, and anything not yet mutated is. | kani.rs:185 |
watchdog_takes_over_only_when_it_should | Kani harness | The watchdog takes a transaction over only inside the mutation window, never from itself, and never from a live owner that is within its deadline or has renewed within the grace period; a dead owner’s transaction in the window is always taken. No clock value makes the rule overflow. | kani.rs:199 |
step_allowed | verified fn | (no doc comment) | machine.rs:61 |
add_interlock | verified fn | Mark a transaction RecoveryFailed from the sentinel, when the journal itself could not take the record (§12c). | ledger.rs:934 |
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 |
|---|---|---|---|
| G1 | Some lease holder eventually runs. | Platform (progress) | — |
| G2 | A fenced worker eventually stops issuing calls, or its calls are refused. | Platform (progress) | — |
| G3 | Journal writes eventually succeed. | Platform (progress) | — |
| G4 | Backend calls terminate. | Platform (progress) | — |
| P1 | Backend Outcome is honest: Succeeded means applied; Unknown means the backend cannot say | Platform | I3, I25 |
| P4 | Journal fsync is durable and the preallocation is writable | Platform | I6, I7, I15, I18, I24, I25 |
| P7 | Fencing is effective: a stale-epoch call is refused before it mutates | Platform | I15 |
| 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 | I6 |
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 |
|---|---|---|---|---|
awaiting-boot-reminds-daily | fake | A kernel parameter change takes the boot-only path and nobody restarts for two and a half days. It stays AwaitingBoot (no limit applies, nothing is cancelled), the ‘restart to finish’ notice is repeated once a day, and at the eventual restart it is confirmed and commits. | generation: candidate; notices_count: count 2, match is still waiting for a restart; reports: RestartToFinish; txn: Committed ApplyChange | fake: PASS |
built-parking-expires | fake | alice changes her font scale while a game holds Foreground in her session, and the game never lets go. After a day in Built the change is Cancelled by the daemon, with one notice naming it and how to issue it again; it never activates, even once the game ends. | notices_count: count 1, match waited a day in Built; reports: WaitsForWindow; txn: Cancelled ApplyChange | 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 |
en-i12-nothing-left-open | fake | A generation change breaks gym-web, and the revert to the base fails too. The daemon is killed while it is reverting and comes back to finish the revert, which fails again. At the end no journaled transaction is left open, the change is RecoveryFailed with its alert, the interlock holds, and gym-web’s next crash gets no autonomous restart. | interlock: set; no_txn_on: service:gym-web; nothing_left_open: true; reports: RecoveryFailed; txn: RecoveryFailed ApplyChange | fake: PASS |
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 |
Also tested by exec crash-point property 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.1 | §17a: progress assumptions stated for I12 |
| v4.3 | I12’s terminal set includes Rejected and Cancelled |
| v4.4 | rule 4’s preserve list extended to I10–I20 |
| v4.6 | I12: parked states bounded or reported [S03] |
See also
§17a · §12f · planarian_txn::ledger in rustdoc · planarian_txn::machine in rustdoc