planarian_schema/
txn.rs

1//! Transactions, leases, approvals and incidents (§8).
2
3use crate::ids::{
4    GenerationId, Hash, IncidentId, JobId, Millis, PolicyVersion, PrincipalId, SnapshotId, StorePath, Timestamp, TxnId,
5};
6use crate::state::UnitStatus;
7use crate::transition::{
8    ApproverClass, ConfigDiff, DerivedFacts, DriverRef, Expectation, RecoveryStrategy, RejectReason, Transition,
9};
10use crate::unit::{Actor, DesiredStatus, UnitId};
11use serde::{Deserialize, Serialize};
12use vstd::prelude::*;
13
14// The journal state machine's states, visible to the `txn` proofs.
15verus! {
16
17#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
18#[verifier::external_derive]
19pub enum TxnState {
20    Prepared,
21    Staged,
22    Built,
23    Activating,
24    Checking,
25    /// Boot entry written.
26    Published,
27    /// The boot-only path (§12 step 7): journaled before `publish_boot_once`,
28    /// the first boot mutation; the crash table asks the boot loader.
29    Publishing,
30    /// A boot-only candidate published as a one-shot next-boot entry (§12f);
31    /// active for I6, confirmed or reverted at that boot.
32    AwaitingBoot,
33    /// Override source promoted.
34    Promoted,
35    Committed,
36    Reverting,
37    Reverted,
38    RecoveryFailed,
39    /// Refused after Prepared (precondition, expired or invalidated approval, policy).
40    Rejected(RejectReason),
41    /// Withdrawn before any mutation.
42    Cancelled(Actor),
43}
44
45impl TxnState {
46    /// I12's terminal set.
47    pub open spec fn terminal(self) -> bool {
48        match self {
49            TxnState::Committed | TxnState::Reverted | TxnState::RecoveryFailed | TxnState::Rejected(_)
50            | TxnState::Cancelled(_) => true,
51            _ => false,
52        }
53    }
54
55    /// Nothing has been mutated yet.
56    pub open spec fn pre_mutation(self) -> bool {
57        match self {
58            TxnState::Prepared | TxnState::Staged | TxnState::Built => true,
59            _ => false,
60        }
61    }
62
63    /// States in which no other transition may execute (I6, §12 Concurrency):
64    /// one list, which the ledger reads.
65    pub open spec fn exclusive(self) -> bool {
66        match self {
67            TxnState::Activating | TxnState::Checking | TxnState::Publishing | TxnState::Published
68            | TxnState::Promoted | TxnState::Reverting => true,
69            _ => false,
70        }
71    }
72
73    pub fn is_terminal(&self) -> (r: bool)
74        ensures
75            r == self.terminal(),
76    {
77        match self {
78            TxnState::Committed | TxnState::Reverted | TxnState::RecoveryFailed | TxnState::Rejected(_)
79            | TxnState::Cancelled(_) => true,
80            _ => false,
81        }
82    }
83
84    pub fn is_pre_mutation(&self) -> (r: bool)
85        ensures
86            r == self.pre_mutation(),
87    {
88        match self {
89            TxnState::Prepared | TxnState::Staged | TxnState::Built => true,
90            _ => false,
91        }
92    }
93
94    pub fn is_exclusive(&self) -> (r: bool)
95        ensures
96            r == self.exclusive(),
97    {
98        match self {
99            TxnState::Activating | TxnState::Checking | TxnState::Publishing | TxnState::Published
100            | TxnState::Promoted | TxnState::Reverting => true,
101            _ => false,
102        }
103    }
104}
105
106// Payloads no proof reads, opaque to Verus.
107#[verifier::external_type_specification]
108#[verifier::external_body]
109#[allow(dead_code)]
110pub struct ExCheckContext(CheckContext);
111
112#[verifier::external_type_specification]
113#[verifier::external_body]
114#[allow(dead_code)]
115pub struct ExApprovalToken(ApprovalToken);
116
117#[verifier::external_type_specification]
118#[verifier::external_body]
119#[allow(dead_code)]
120pub struct ExIncident(Incident);
121
122#[verifier::external_type_specification]
123#[verifier::external_body]
124#[allow(dead_code)]
125pub struct ExExpectation(Expectation);
126
127#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
128#[verifier::external_derive]
129pub enum OwnerId {
130    Daemon { pid: u32, boot_id: Hash },
131    Watchdog { pid: u32, boot_id: Hash },
132}
133
134/// Exclusive ownership of a transaction (§12). `txn` is not in §8; the
135/// backend fences on (txn, epoch), so the lease has to name its transaction.
136#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
137#[verifier::external_derive]
138pub struct Lease {
139    pub txn: TxnId,
140    pub owner: OwnerId,
141    pub epoch: u64,
142    pub worker_pid: Option<u32>,
143    pub renewed: Timestamp,
144    /// Supervisor jobs this owner submitted.
145    pub jobs: Vec<JobId>,
146}
147
148#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
149#[verifier::external_derive]
150pub struct Transaction {
151    pub id: TxnId,
152    pub state: TxnState,
153    pub lease: Lease,
154    /// NAR hash of the owner's source with the BASE override, at Prepared (§9).
155    pub base_source: Option<Hash>,
156    /// NAR hash of the candidate tree actually evaluated and built (§9).
157    pub staged_source: Option<Hash>,
158    /// The candidate store path's NAR hash, as the store reported it when it
159    /// was built; `verify_candidate` checks the path against it (§9 step 3,
160    /// C6). None for a generation not built by this transaction.
161    #[serde(default)]
162    pub candidate_nar: Option<Hash>,
163    pub base_override: Option<Hash>,
164    pub candidate_override: Option<Hash>,
165    /// `/nix/var/nix/gcroots/planarian/builds/<staged_source>`, adopted at Prepared (I3).
166    pub gc_root: Option<String>,
167    pub recovery: RecoveryStrategy,
168    pub transition: Transition,
169    pub facts: DerivedFacts,
170    pub base: GenerationId,
171    pub candidate: Option<(GenerationId, StorePath)>,
172    pub policy: PolicyVersion,
173    pub approval: Option<ApprovalToken>,
174    pub snapshot: Option<SnapshotId>,
175    pub expected: Expectation,
176    pub started: Timestamp,
177    /// The watchdog acts after this.
178    pub deadline: Timestamp,
179    /// Fixed at Prepared; authorized with the transaction.
180    pub revert_to: GenerationId,
181    /// For `BindDriver`: the driver bound at Prepared, rebound on revert (§12
182    /// execution table). Not in §8 (G12).
183    pub prior_driver: Option<DriverRef>,
184    /// What the probe check needs, journaled so the watchdog can run it alone.
185    pub check: CheckContext,
186    /// §12f: the withdrawn transaction this one prepares again (from its
187    /// proposal). Absent in records from before it.
188    #[serde(default)]
189    pub prepared_again_from: Option<TxnId>,
190}
191
192#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
193#[verifier::external_derive]
194pub enum Outcome {
195    Succeeded,
196    Failed(String),
197    Partial(String),
198    Unknown(String),
199}
200
201} // verus!
202
203impl OwnerId {
204    pub fn pid(&self) -> u32 {
205        match self {
206            OwnerId::Daemon { pid, .. } | OwnerId::Watchdog { pid, .. } => *pid,
207        }
208    }
209
210    pub fn is_watchdog(&self) -> bool {
211        matches!(self, OwnerId::Watchdog { .. })
212    }
213
214    pub fn boot_id(&self) -> Hash {
215        match self {
216            OwnerId::Daemon { boot_id, .. } | OwnerId::Watchdog { boot_id, .. } => *boot_id,
217        }
218    }
219}
220
221/// The manifest part of an evaluated generation.
222#[derive(Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
223pub struct Manifest {
224    pub units: crate::unit::UnitDefs,
225    /// Per-user templates (`Scope::User { uid: 0 }`), instantiated per session.
226    pub user_units: Vec<crate::unit::UnitDef>,
227}
228
229/// Recorded at Prepared (§12 step 4) for the Checking and revert probe runs:
230/// the candidate's and the base's manifests, and every unit's status before.
231#[derive(Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
232pub struct CheckContext {
233    pub candidate: Option<Manifest>,
234    pub base: Manifest,
235    pub pre: std::collections::BTreeMap<UnitId, UnitStatus>,
236    /// Per unit, the Readiness probes passing before (§9, R07): each must
237    /// still pass after, whatever the unit's aggregate status was.
238    #[serde(default)]
239    pub pre_passing: std::collections::BTreeMap<UnitId, Vec<crate::ids::ProbeId>>,
240}
241
242impl Outcome {
243    /// `Partial` and `Unknown` are never success (§12 step 8).
244    pub fn is_success(&self) -> bool {
245        matches!(self, Outcome::Succeeded)
246    }
247
248    pub fn fenced() -> Outcome {
249        Outcome::Failed("fenced".into())
250    }
251
252    pub fn is_fenced(&self) -> bool {
253        matches!(self, Outcome::Failed(m) if m == "fenced")
254    }
255}
256
257#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
258pub struct ApprovalToken {
259    /// hash(transition, staged_source, candidate store path, base generation,
260    /// policy version, cumulative-diff hash, derived facts, expected, revert_to,
261    /// recovery strategy).
262    pub bound_to: Hash,
263    /// Differs from the proposer and holds `class` (I19).
264    pub approver: PrincipalId,
265    pub class: ApproverClass,
266    pub issued: Timestamp,
267    pub expires: Timestamp,
268    pub nonce: [u8; 16],
269    pub used: bool,
270}
271
272pub const TOKEN_LIFETIME: Millis = Millis(24 * 3600 * 1000);
273
274/// How long a transaction may wait in `Built` for an activation window
275/// (§12f, I12); `AwaitingBoot` has no limit.
276pub const PARKING_LIMIT: Millis = Millis(24 * 3600 * 1000);
277
278#[derive(Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
279pub struct Session {
280    pub applied: Vec<TxnId>,
281    pub cumulative: ConfigDiff,
282    pub policy: Option<PolicyVersion>,
283}
284
285// ---------- Incidents ----------
286
287#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
288pub enum IncidentState {
289    Open,
290    Cooldown {
291        until: Timestamp,
292    },
293    /// Reported to the user; no autonomous action until `until` or a human acts.
294    /// `until` is not in §8; without it the hold could not survive a restart.
295    Escalated {
296        until: Timestamp,
297        reason: EscalationReason,
298    },
299    Closed,
300    Regressed {
301        count: u8,
302    },
303}
304
305#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
306pub enum EscalationReason {
307    Regressed,
308    BudgetExhausted,
309    DiagnoserExhausted,
310    /// No eligible known-good generation above the security floor (§12e).
311    RevertBlockedByFloor,
312    RecoveryFailed,
313}
314
315#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
316pub enum IncidentKind {
317    /// A divergence to repair.
318    Repair,
319    /// Three consecutive Unknowns (§10): re-observe through another Readiness
320    /// probe; never a restart.
321    Diagnostic,
322}
323
324#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
325pub struct Incident {
326    pub id: IncidentId,
327    pub kind: IncidentKind,
328    pub target: UnitId,
329    pub divergence: (DesiredStatus, UnitStatus),
330    pub opened: Timestamp,
331    pub attempts: Vec<(TxnId, Outcome)>,
332    /// Persisted; survives daemon restart.
333    pub budget_left: u8,
334    pub state: IncidentState,
335    pub backoff: Millis,
336    /// Earliest time of the next attempt (backoff and defer-to-systemd).
337    /// Not in §8; persisted so a restart does not reset the backoff.
338    pub next_attempt: Timestamp,
339    /// How often this target regressed within the window (§13).
340    pub regressions: u8,
341}
planarian_schema/txn.rs

planarian_schema/
txn.rs
