Assumptions
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
| Id | Kind | Assumption | Invariants |
|---|---|---|---|
| G1 | Platform (progress) | Some lease holder eventually runs. | I12 |
| G2 | Platform (progress) | A fenced worker eventually stops issuing calls, or its calls are refused. | I12 |
| G3 | Platform (progress) | Journal writes eventually succeed. | I12 |
| G4 | Platform (progress) | Backend calls terminate. | I12 |
| P1 | Platform | Backend Outcome is honest: Succeeded means applied; Unknown means the backend cannot say | I3, I12, I25 |
| P10 | Platform | A pidfd names one process for as long as it is held, and SO_PEERPIDFD (Linux ≥ 6.5) names the process that connected; so a recycled pid can never be mistaken for the peer (§10, B-6). The gym cannot exercise pid reuse itself: Linux hands out pids in increasing order and wraps only after pid_max (4 194 304 on 64-bit systems, 32 768 on some), so the same pid coming back to another process of the same uid, in another session, inside one request’s lifetime, cannot be arranged reproducibly. identity-peer-exited checks the case the pidfd rule decides (a peer gone before it is resolved). The rarity is not the protection; the pidfd is. | |
| P2 | Platform | activate_live(revert_to) restores the activation state of revert_to | |
| P3 | Platform | publish_boot and the override promotion rename are idempotent | I1, I16, I23 |
| P4 | Platform | Journal fsync is durable and the preallocation is writable | I6, I7, I12, I15, I18, I24, I25 |
| P5 | Platform | SHA-256 is collision-resistant (the journal’s hash chain, I18) | I2, I8, I18 |
| P6 | Platform | systemd reports unit state truthfully over D-Bus and honors X-RestartIfChanged / X-StopIfChanged | I4, I13, I20, I24 |
| P7 | Platform | Fencing is effective: a stale-epoch call is refused before it mutates | I12, I15 |
| P8 | Platform | The kernel and systemd are correct | I1, I2, I3, I9, I17, I20, I22 |
| U1 | Internal unproven | exec::derive: DerivedFacts from the evaluated generation, never from a proposal (I14’s other half; property-tested) | I10, I14, I21, I22 |
| U2 | Internal unproven | user_authorization and the administrator lookup (planarian-admin membership, root) | I17, I19, I22 |
| U3 | Internal unproven | The residue classifier (§11: which unit endings are a person’s stop) | I13 |
| U4 | Internal unproven | Journal I/O around the verified chain: framing, torn-tail truncation, checkpoint replace | I18 |
| U5 | Internal unproven | Identity resolution (§10): peer credentials and pidfd to logind session, seat, terminal | I19, I21, I24 |
| V1 | Proof-validity | vstd’s specifications of Vec, String::as_str, str::unicode_len, str::get_char | I5, I10, I11, I16, I19, I21, I22 |
| V10 | Proof-validity | rustc compiles the verified code to a program with the semantics Verus checked. | every proof |
| V11 | Proof-validity | Kani and its back end CBMC are sound within the stated bounds. | every proof |
| V2 | Proof-validity | Value is an opaque external type (external_type_specification); nothing about it is assumed | I5, I11, I16, I21 |
| V3 | Proof-validity | Serde impls are unverified (external_derive) | I5, I6, I14 |
| V4 | Proof-validity | Expectation, CheckContext, ApprovalToken, Incident are opaque external types | I6 |
| V5 | Proof-validity | 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 | I6, I12 |
| V6 | Proof-validity | vstd’s specifications of Vec::push, insert, remove, is_empty and Box | I6 |
| V7 | Proof-validity | The specifications the proofs prove against (decide_spec, step_spec, inv, chained, the lemma statements) say what the SPEC’s English means. A proof certifies a wrong specification as readily as a right one; each proved invariant has a gym entry written from the English to catch the difference (§17a). | every proof |
| V8 | Proof-validity | Verus is sound: what it reports verified holds of the code. | every proof |
| V9 | Proof-validity | Z3, the solver Verus calls, is sound. | every proof |