§17a. Verification plan and trusted assumptions
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
Proof targets, in order: Phase A — schema::digest; policy::decide (purity; I5; I11; I14 in the sense that decide has no Proposal input; probe-tamper → AskFirst or Reject; I16 in decide and revert-target selection; I19: no token whose approver is the proposer, no self-grant); txn kernel (I6, including Built-waiting and AwaitingBoot; I12: every journaled transaction reaches a terminal state under the modeled outcomes; write-ahead ordering). Added 2026-10-29: the journal’s hash chain (I18: every record written commits to its predecessor’s hash, and the check on read reports the first break), in txn under Verus in A, trusting only SHA-256; the residue classifier (§11: which unit endings are a person’s stop and which are faults) extracted as a pure function with Kani harnesses in A, Verus with exec in C; I17 (user_authorization gives root the administrator capability, so the set is never empty while root exists) in policy in A. exec orchestration gets Kani harnesses and proptest in A, Verus in C, together with I13 (the incident planner never targets an overridden unit). Diagnoser soundness and scorer in B. Broker in C. Switch/rollback and supervisor in D (store integrity proven only for content-addressed paths; input-addressed paths are verified by signature and NAR hash, not by content). OSTD, model channel, core update path in E.
docs/assumptions.md lists every externally specified behavior the proofs rely on, maintained as Verus external_body/assume sites are added. Phase A entries: backend Outcome is honest (Succeeded means applied; Unknown means the backend cannot say); activate_live(revert_to) restores the activation state of revert_to; publish_boot and the promotion rename are idempotent; the journal’s fsync is durable and the preallocation is writable; systemd reports unit state truthfully over D-Bus and honors X-RestartIfChanged/X-StopIfChanged; fencing is effective (a stale-epoch call is refused before it mutates); the kernel and systemd are correct. Re-observation after a backend call detects divergence from the assumed postcondition; it does not undo an irreversible effect, which is why the NonReversible floor exists.
Progress assumptions for I12 (liveness is conditional on these, stated in the proof): some lease holder (daemon or watchdog) eventually runs; a fenced worker eventually stops issuing calls or its calls are refused; journal writes eventually succeed (guaranteed by the preallocation for recovery records); backend calls terminate. Under those, every transaction reaches a terminal state; with them violated the proof says nothing, and RecoveryFailed plus alerting is the designed fallback.
Verification ratio. The trusted computing base is 𝒱 ∪ 𝒯: 𝒱, the proven base, is what is verified (schema, policy, txn, and later crates as they enter the Verus subset); 𝒯, the trusted base, is what is trusted but unproven (backends, Nix, systemd, the kernel, firmware), with every trust recorded in docs/assumptions.md. 𝒯 is accounted in three parts. Platform trust (P, G): what the machine underneath does. Proof-validity trust (V, plus the specifications the proofs prove against, Verus, Z3, and rustc): what makes a proof mean what it says. Internal unproven code (I-ids: exec::derive, user_authorization and the admin lookup, the residue classifier, journal I/O, the identity resolution of §10): Planarian’s own code that the proven gates take input from. Internal unproven code is not an assumption about the world; it is work not yet proved, so it is reported as its own number, the internal-unproven count, never folded into the trust count, and it must not grow and is expected to fall from C. Every proved invariant also has at least one gym entry written from the spec’s English rather than from its formal specification, since a proof certifies a wrong specification as readily as a right one. Every gate reports three numbers: the trust count (the count of platform and proof-validity entries in assumptions.md, including external_body and assume sites), the internal-unproven count, and the ratio d:a, discharged (d) to assumed (a) obligations, per invariant (“I12 rests on 3 discharged lemmas and 5 assumptions”) and summed globally. GA reports both as the baseline. Every later gate requires that neither the global ratio nor any per-invariant ratio degrades and that the trust count does not grow. The v4.5 re-accounting (proof-validity entries added, internal code moved out of the trust count) sets a new baseline once, recorded with its reason; it is not a regression. D and E are expected to raise the ratio substantially; the gate requires only that it not fall, so that no one improves it with proofs that discharge nothing load-bearing.
The accounting is itself checked. planarian-gym verification rejects a duplicate obligation id; requires every invariant in the baseline to be present in the current accounting (a removed invariant is a failure, not an absence); and ties each discharged obligation to a proof artifact the verifier actually produced (the Verus check’s output, or a reviewed manifest naming the proof function), not to the textual presence of a function name. Gym mutations: delete an invariant, duplicate an obligation, rename a proof function; each fails the gate.
Status of the Phase A proof targets at v4.6. Proved: policy::decide (I5, I11, I14-decide, I16-decide, I19, I21, I22), I17 (policy::i17_administrators_never_empty), the txn kernel (I6, I12 conditional, I15, I23, write-ahead ordering), the hash chain (I18). Checked by Kani harnesses: the residue classifier (a Security unit’s stop is never inferred as intended, a crash is always a fault, residue is inferred only where the posture allows it; crates/exec/src/kani.rs). Property-tested, not proved (deviations): schema::digest. Every target is counted in docs/verification-ratio.toml, and CI fails when a count differs.