planarian_schema/
unit.rs

1//! Units, desired state, the graph, risk metadata and probes (§8).
2
3use crate::ids::{Millis, ProbeId, Timestamp};
4use serde::{Deserialize, Deserializer, Serialize, Serializer};
5use std::collections::{BTreeMap, BTreeSet};
6use std::fmt;
7use std::str::FromStr;
8use vstd::prelude::*;
9
10// The unit and risk types `policy` reads, visible to its proofs.
11verus! {
12
13/// Written `<kind>:<name>` for system scope and `<kind>@<uid>[/<session>]:<name>`
14/// for user scope, e.g. `service:sshd`, `service@1000:pipewire`,
15/// `service:external:gym-upstream`. Serialized in that form so it can key JSON maps.
16#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
17pub struct UnitId {
18    pub kind: UnitKind,
19    pub name: String,
20    pub scope: Scope,
21}
22
23/// `Target` is not in §8; added for units such as `graphical-session` (G4).
24#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
25#[derive(Serialize, Deserialize)]
26#[verifier::external_derive]
27pub enum UnitKind {
28    Service,
29    Device,
30    Target,
31}
32
33#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
34#[derive(Serialize, Deserialize)]
35#[verifier::external_derive]
36pub enum Scope {
37    System,
38    User { uid: u32, session: Option<String> },
39}
40
41#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
42#[derive(Serialize, Deserialize)]
43#[verifier::external_derive]
44pub enum Actor {
45    Daemon,
46    Watchdog,
47    /// Filled from `SO_PEERCRED` → pid → logind (§10). `session` is None only
48    /// for callers outside any logind session (a root timer), which never
49    /// satisfy an "own session" floor; `seat` is None for SSH and other remote
50    /// sessions, which are never local.
51    User { uid: u32, session: Option<String>, seat: Option<String>, active: bool },
52    Model(crate::ids::ModelId),
53    /// Reserved: remote principals via a relay; in Phase A, only a local agent
54    /// the journal has no start for (it holds nothing; §11).
55    Agent(crate::ids::PrincipalId),
56    /// The actor of an `Inferred` override (§11): never a caller, never authorized.
57    Unattributed,
58}
59
60#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
61#[derive(Serialize, Deserialize)]
62#[verifier::external_derive]
63pub struct Override {
64    pub unit: UnitId,
65    pub desired: OverrideDesired,
66    pub until: Until,
67    pub reason: String,
68    /// Always overwritten by the daemon from the caller's credentials (§11).
69    /// `Actor::Unattributed` exactly when `attribution == Inferred`.
70    pub by: Actor,
71    pub attribution: Attribution,
72    /// An `Inferred` override a user has acknowledged: the console stops
73    /// listing it; it still holds until it ends (§11, B-11).
74    #[serde(default)]
75    pub acknowledged: bool,
76}
77
78/// What the override holds the unit to (§8). A `Stopped` override also undoes
79/// a generation activation that starts the unit again (principle 9).
80#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
81#[derive(Serialize, Deserialize)]
82#[verifier::external_derive]
83pub enum OverrideDesired {
84    /// Do not repair; take no action.
85    LeaveAlone,
86    /// Stop or kill a service.
87    Stopped,
88    /// Disable or mask.
89    Absent,
90    /// Unmount, eject or unbind a device.
91    Detected,
92}
93
94#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
95#[derive(Serialize, Deserialize)]
96#[verifier::external_derive]
97pub enum Attribution {
98    /// Reached Planarian with the actor's identity before it took effect.
99    Attested,
100    /// The unattributed residue (§11): recorded as an inference, never as fact.
101    Inferred,
102}
103
104#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
105#[derive(Serialize, Deserialize)]
106#[verifier::external_derive]
107pub enum Until {
108    At(Timestamp),
109    NextBoot,
110    Explicit,
111}
112
113#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
114#[derive(Serialize, Deserialize)]
115#[verifier::external_derive]
116pub enum Sensitivity {
117    Routine,
118    Security,
119    UserData,
120    External,
121    Core,
122}
123
124/// Ordered by how much it costs the user; §11 compares with `>=`.
125#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
126#[derive(Serialize, Deserialize)]
127#[verifier::external_derive]
128pub enum Disruption {
129    None,
130    Brief,
131    SessionLoss,
132    DataInterruption,
133    ConnectivityLoss,
134}
135
136/// Ordered from most to least reversible (§13 step 3).
137#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
138#[derive(Serialize, Deserialize)]
139#[verifier::external_derive]
140pub enum Recovery {
141    Idempotent,
142    Revertible,
143    NonReversible,
144}
145
146/// A set of `Sensitivity` values, as flags so the proofs can read it.
147/// Serialized as the list of members in declaration order, as the
148/// `BTreeSet` it replaces was.
149#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
150pub struct Sensitivities {
151    pub routine: bool,
152    pub security: bool,
153    pub user_data: bool,
154    pub external: bool,
155    pub core: bool,
156}
157
158impl Sensitivities {
159    pub open spec fn has(self, s: Sensitivity) -> bool {
160        match s {
161            Sensitivity::Routine => self.routine,
162            Sensitivity::Security => self.security,
163            Sensitivity::UserData => self.user_data,
164            Sensitivity::External => self.external,
165            Sensitivity::Core => self.core,
166        }
167    }
168
169    /// Nothing but `Routine` is present (an empty set counts as Routine).
170    pub open spec fn routine_only(self) -> bool {
171        !self.security && !self.user_data && !self.external && !self.core
172    }
173
174    pub fn contains(&self, s: Sensitivity) -> (r: bool)
175        ensures r == self.has(s),
176    {
177        match s {
178            Sensitivity::Routine => self.routine,
179            Sensitivity::Security => self.security,
180            Sensitivity::UserData => self.user_data,
181            Sensitivity::External => self.external,
182            Sensitivity::Core => self.core,
183        }
184    }
185
186    pub fn only_routine(&self) -> (r: bool)
187        ensures r == self.routine_only(),
188    {
189        !self.security && !self.user_data && !self.external && !self.core
190    }
191
192    pub fn union(&self, other: &Sensitivities) -> (r: Sensitivities)
193        ensures forall|s: Sensitivity| #[trigger] r.has(s) == (self.has(s) || other.has(s)),
194    {
195        Sensitivities {
196            routine: self.routine || other.routine,
197            security: self.security || other.security,
198            user_data: self.user_data || other.user_data,
199            external: self.external || other.external,
200            core: self.core || other.core,
201        }
202    }
203
204    pub fn insert(&mut self, s: Sensitivity)
205        ensures forall|t: Sensitivity| #[trigger] final(self).has(t) == (old(self).has(t) || t == s),
206    {
207        match s {
208            Sensitivity::Routine => self.routine = true,
209            Sensitivity::Security => self.security = true,
210            Sensitivity::UserData => self.user_data = true,
211            Sensitivity::External => self.external = true,
212            Sensitivity::Core => self.core = true,
213        }
214    }
215}
216
217} // verus!
218
219impl Actor {
220    /// A user outside any logind session (a root timer, a test). Never local,
221    /// never "own session".
222    pub fn user(uid: u32) -> Actor {
223        Actor::User { uid, session: None, seat: None, active: false }
224    }
225
226    /// A user in the active local session `session` on `seat0`.
227    pub fn local(uid: u32, session: &str) -> Actor {
228        Actor::User { uid, session: Some(session.into()), seat: Some("seat0".into()), active: true }
229    }
230
231    /// The principal behind this actor (§11). A human is their uid; the
232    /// non-human actors of Phase A have fixed ids above every uid.
233    pub fn principal(&self) -> crate::ids::PrincipalId {
234        use crate::ids::PrincipalId;
235        const BASE: u64 = 1 << 32;
236        match self {
237            Actor::User { uid, .. } => PrincipalId(*uid as u64),
238            Actor::Daemon => PrincipalId(BASE),
239            Actor::Watchdog => PrincipalId(BASE + 1),
240            Actor::Model(_) => PrincipalId(BASE + 2),
241            Actor::Unattributed => PrincipalId(BASE + 3),
242            Actor::Agent(p) => *p,
243        }
244    }
245
246    pub fn uid(&self) -> Option<u32> {
247        match self {
248            Actor::User { uid, .. } => Some(*uid),
249            _ => None,
250        }
251    }
252}
253
254impl Override {
255    /// An attested override: the action reached Planarian with `by`'s identity first.
256    pub fn attested(unit: UnitId, desired: OverrideDesired, until: Until, reason: String, by: Actor) -> Override {
257        Override { unit, desired, until, reason, by, attribution: Attribution::Attested, acknowledged: false }
258    }
259}
260
261impl Sensitivities {
262    pub const ALL: [Sensitivity; 5] =
263        [Sensitivity::Routine, Sensitivity::Security, Sensitivity::UserData, Sensitivity::External, Sensitivity::Core];
264
265    pub fn of(items: &[Sensitivity]) -> Sensitivities {
266        let mut out = Sensitivities::default();
267        for s in items {
268            out.insert(*s);
269        }
270        out
271    }
272
273    /// Members in declaration order.
274    pub fn members(&self) -> Vec<Sensitivity> {
275        Self::ALL.into_iter().filter(|s| self.contains(*s)).collect()
276    }
277}
278
279impl Serialize for Sensitivities {
280    fn serialize<S: Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
281        self.members().serialize(s)
282    }
283}
284
285impl<'de> Deserialize<'de> for Sensitivities {
286    fn deserialize<D: Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
287        Ok(Sensitivities::of(&Vec::<Sensitivity>::deserialize(d)?))
288    }
289}
290
291impl UnitId {
292    pub fn system(kind: UnitKind, name: &str) -> UnitId {
293        UnitId { kind, name: name.to_owned(), scope: Scope::System }
294    }
295
296    pub fn service(name: &str) -> UnitId {
297        UnitId::system(UnitKind::Service, name)
298    }
299
300    pub fn device(name: &str) -> UnitId {
301        UnitId::system(UnitKind::Device, name)
302    }
303
304    pub fn target(name: &str) -> UnitId {
305        UnitId::system(UnitKind::Target, name)
306    }
307}
308
309impl fmt::Display for UnitId {
310    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
311        let kind = match self.kind {
312            UnitKind::Service => "service",
313            UnitKind::Device => "device",
314            UnitKind::Target => "target",
315        };
316        match &self.scope {
317            Scope::System => write!(f, "{kind}:{}", self.name),
318            Scope::User { uid, session: None } => write!(f, "{kind}@{uid}:{}", self.name),
319            Scope::User { uid, session: Some(s) } => write!(f, "{kind}@{uid}/{s}:{}", self.name),
320        }
321    }
322}
323
324#[derive(Debug, PartialEq, Eq)]
325pub struct ParseUnitIdError(pub String);
326
327impl FromStr for UnitId {
328    type Err = ParseUnitIdError;
329
330    fn from_str(s: &str) -> Result<Self, Self::Err> {
331        let err = || ParseUnitIdError(s.to_owned());
332        let (head, name) = s.split_once(':').ok_or_else(err)?;
333        if name.is_empty() {
334            return Err(err());
335        }
336        let (kind, scope) = match head.split_once('@') {
337            None => (head, Scope::System),
338            Some((kind, user)) => {
339                let (uid, session) = match user.split_once('/') {
340                    None => (user, None),
341                    Some((uid, session)) => (uid, Some(session.to_owned())),
342                };
343                (kind, Scope::User { uid: uid.parse().map_err(|_| err())?, session })
344            }
345        };
346        let kind = match kind {
347            "service" => UnitKind::Service,
348            "device" => UnitKind::Device,
349            "target" => UnitKind::Target,
350            _ => return Err(err()),
351        };
352        Ok(UnitId { kind, name: name.to_owned(), scope })
353    }
354}
355
356impl Serialize for UnitId {
357    fn serialize<S: Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
358        s.collect_str(self)
359    }
360}
361
362impl<'de> Deserialize<'de> for UnitId {
363    fn deserialize<D: Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
364        let s = String::deserialize(d)?;
365        s.parse().map_err(|e: ParseUnitIdError| serde::de::Error::custom(format!("bad unit id {:?}", e.0)))
366    }
367}
368
369// ---------- Actors ----------
370
371// ---------- Desired ----------
372
373#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
374pub enum Condition {
375    Always,
376    /// logind reports a session of class `user` with a seat, or a remote user
377    /// session; greeter, `manager` and background sessions never count (§10).
378    /// `seated` asks for a session at a seat: the graphical expectation
379    /// (S05), which an SSH-only login never carries. As an atom (what holds
380    /// now), it says whether that session has a seat.
381    SessionEstablished {
382        uid: Option<u32>,
383        #[serde(default)]
384        seated: bool,
385    },
386    DeviceConnected(UnitId),
387    OnAcPower,
388    OnBattery,
389    /// Quiet mode (§12f; signals in §10): a GameMode client, a gamescope
390    /// session, a fullscreen surface holding an idle-inhibitor, or Do Not Disturb.
391    Foreground {
392        session: String,
393    },
394    All(Vec<Condition>),
395    Any(Vec<Condition>),
396}
397
398impl Condition {
399    /// `atoms` is the set of atomic conditions that hold right now.
400    pub fn holds(&self, atoms: &BTreeSet<Condition>) -> bool {
401        match self {
402            Condition::Always => true,
403            Condition::All(cs) => cs.iter().all(|c| c.holds(atoms)),
404            Condition::Any(cs) => cs.iter().any(|c| c.holds(atoms)),
405            Condition::SessionEstablished { uid, seated } => atoms.iter().any(|a| {
406                matches!(a, Condition::SessionEstablished { uid: u, seated: s }
407                    if (uid.is_none() || u == uid) && (*s || !*seated))
408            }),
409            atom => atoms.contains(atom),
410        }
411    }
412
413    /// The condition asks for a seated session somewhere (S05).
414    pub fn needs_seat(&self) -> bool {
415        match self {
416            Condition::SessionEstablished { seated, .. } => *seated,
417            Condition::All(cs) | Condition::Any(cs) => cs.iter().any(Condition::needs_seat),
418            _ => false,
419        }
420    }
421}
422
423#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
424pub enum DesiredStatus {
425    Running,
426    Stopped,
427    Bound,
428    Absent,
429}
430
431#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
432pub struct Desired {
433    pub status: DesiredStatus,
434    pub when: Condition,
435}
436
437impl Override {
438    /// `NextBoot` overrides are dropped by state assembly on boot, so here they hold.
439    pub fn holds_at(&self, now: Timestamp) -> bool {
440        match self.until {
441            Until::At(t) => now < t,
442            Until::NextBoot | Until::Explicit => true,
443        }
444    }
445}
446
447// ---------- Graph ----------
448
449/// Confidence in per-mille (0..=1000). Used instead of `f32` to stay in the
450/// Verus subset and keep comparisons exact.
451#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
452#[serde(transparent)]
453pub struct Confidence(pub u16);
454
455#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
456pub enum EdgeKind {
457    /// After=/Before=: never followed in diagnosis.
458    Ordering,
459    /// Wants=: weak; never a root cause for the wanting unit.
460    Wants,
461    /// Requires=/BindsTo=/Requisite= or manifest: functional prerequisite.
462    Requires,
463    /// Manifest or learned; may form cycles (§13).
464    Diagnostic { confidence: Confidence },
465}
466
467#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
468pub struct Edge {
469    pub from: UnitId,
470    pub to: UnitId,
471    pub kind: EdgeKind,
472    pub origin: EdgeOrigin,
473}
474
475#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
476pub enum EdgeOrigin {
477    SystemdRequires,
478    SystemdWants,
479    SystemdAfter,
480    Manifest,
481    Learned,
482}
483
484// ---------- Risk metadata ----------
485
486#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
487pub struct SystemdRestartPolicy {
488    pub restart: bool,
489    pub restart_sec: Millis,
490    pub start_limit_burst: u32,
491}
492
493#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
494pub struct UnitDef {
495    pub id: UnitId,
496    pub desired: Desired,
497    pub edges: Vec<Edge>,
498    pub sensitivity: Sensitivities,
499    pub restart_disruption: Disruption,
500    pub probes: Vec<ProbeDef>,
501    pub synonyms: Vec<String>,
502    pub systemd_restart: Option<SystemdRestartPolicy>,
503    /// How long after the unit comes up a failing health probe is not yet a
504    /// fault (it may still be starting). `None`: the daemon's default.
505    #[serde(default)]
506    pub startup_grace: Option<Millis>,
507    /// A runtime-settable option (§12a) whose other values can restore this
508    /// unit: `wifi.network` for a Wi-Fi interface. When it diverges, the
509    /// diagnoser may propose another value the backend says is available.
510    #[serde(default)]
511    pub runtime_repair: Option<String>,
512    /// The manifest's `inferStops = false` (§11, B-11): a stop outside
513    /// Planarian is a fault (restarted and alarmed), never inferred as a
514    /// person's intent. Backup, sync and the desktop's own units.
515    #[serde(default)]
516    pub stops_are_faults: bool,
517    /// §12d *Network security fails closed*: its failure holds the machine's
518    /// traffic. Computed by the module (nix/module.nix `isNetworkSecurity`),
519    /// exported, never a manifest option. Interim (B-21): the netwatch
520    /// footprint replaces it.
521    #[serde(default)]
522    pub holds: bool,
523    /// What the hold still lets it reach (the manifest's `holdAllow`).
524    #[serde(default)]
525    pub hold_allow: Vec<HoldEndpoint>,
526    /// Its own interfaces, which the hold passes (`holdInterfaces`).
527    #[serde(default)]
528    pub hold_interfaces: Vec<String>,
529}
530
531/// An endpoint a held unit still needs to reconnect (§12d `holdAllow`).
532#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
533pub struct HoldEndpoint {
534    pub address: String,
535    pub port: u16,
536    pub protocol: String,
537}
538
539pub type UnitDefs = BTreeMap<UnitId, UnitDef>;
540
541// ---------- Health ----------
542
543#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
544pub struct ProbeDef {
545    pub id: ProbeId,
546    pub kind: ProbeKind,
547    pub timeout: Millis,
548    pub origin: ProbeOrigin,
549    /// Readiness feeds Running/Unknown; Diagnostic never does.
550    pub role: ProbeRole,
551    pub cadence: Cadence,
552    pub cost: ProbeCost,
553    pub side_effects: SideEffects,
554    /// What a pass actually shows, in plain words.
555    pub establishes: String,
556}
557
558#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
559pub enum ProbeOrigin {
560    Canonical,
561    User,
562}
563
564#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
565pub enum ProbeKind {
566    SystemdActive,
567    Tcp {
568        addr: String,
569    },
570    Http {
571        url: String,
572        status: u16,
573    },
574    DBus {
575        service: String,
576        path: String,
577        method: String,
578    },
579    FilePresent {
580        path: String,
581    },
582    /// Administrator-authored manifest entries only; flagged in the console and journal (§9).
583    Exec {
584        argv: Vec<String>,
585        sandbox: ProbeSandbox,
586    },
587    /// Free space on the filesystem holding `path`: at least `min_bytes` and at
588    /// least `min_permille` of its size (§10 storage units). Not in §8.
589    FreeSpace {
590        path: String,
591        min_bytes: u64,
592        min_permille: u16,
593    },
594    /// A systemd target in the user's session reached within `within` of that
595    /// session's creation (§9 graphical-session). Evaluated by `state` from logind
596    /// and systemd together; bound to one session id (§10). Not in §8.
597    SessionTarget {
598        target: String,
599        within: Millis,
600    },
601}
602
603#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
604pub struct ProbeSandbox {
605    pub uid: u32,
606    pub caps: Vec<String>,
607    pub max_output: u32,
608    pub cpu_ms: u32,
609    pub network: bool,
610}
611
612#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
613pub enum ProbeRole {
614    Readiness,
615    Diagnostic,
616}
617
618#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
619pub enum Cadence {
620    EveryTick,
621    Every(Millis),
622    OnEvent,
623    OnDemand,
624}
625
626#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
627pub enum ProbeCost {
628    Trivial,
629    Cheap,
630    WakesHardware,
631}
632
633#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
634pub enum SideEffects {
635    None,
636    /// Bounded read-only I/O, permitted for Readiness probes at the declared rate.
637    Measurement {
638        bytes_max: u32,
639        per: Millis,
640    },
641    Audible,
642    Visible,
643    RemoteStateChange,
644    Disk,
645}
646
647#[derive(Debug, PartialEq, Eq)]
648pub enum ProbeContractError {
649    /// A Readiness probe with side effects other than None or Measurement.
650    ReadinessWithSideEffects(ProbeId),
651    /// A side-effecting probe that is not OnDemand (§18.4).
652    SideEffectsOnCadence(ProbeId),
653}
654
655impl ProbeDef {
656    /// The parts of the probe contract (§10) that are decidable from the definition.
657    pub fn check_contract(&self) -> Result<(), ProbeContractError> {
658        let benign = matches!(self.side_effects, SideEffects::None | SideEffects::Measurement { .. });
659        if !benign && self.role == ProbeRole::Readiness {
660            return Err(ProbeContractError::ReadinessWithSideEffects(self.id.clone()));
661        }
662        if !benign && self.cadence != Cadence::OnDemand {
663            return Err(ProbeContractError::SideEffectsOnCadence(self.id.clone()));
664        }
665        Ok(())
666    }
667}
668
669#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
670pub enum ProbeResult {
671    Pass,
672    Fail(String),
673    Timeout,
674    Error(String),
675    /// Still running, or not yet started, when the batch deadline passed
676    /// (§10): recorded Unknown and abandoned. Not `Timeout`, which is a probe
677    /// past its own deadline, so a probe that only waited behind a wedged one
678    /// is not blamed for it.
679    Abandoned,
680}
681
682/// `probe` is not in §8; status derivation cannot match evidence to probes without it (G11).
683#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
684pub struct Evidence {
685    pub probe: ProbeId,
686    pub result: ProbeResult,
687    pub at: Timestamp,
688    pub stale_after: Millis,
689}
690
691impl Evidence {
692    pub fn fresh_at(&self, now: Timestamp) -> bool {
693        now <= self.at.plus(self.stale_after)
694    }
695}
696
697#[cfg(test)]
698mod tests {
699    use super::*;
700
701    #[test]
702    fn unit_id_roundtrip() {
703        for s in [
704            "service:sshd",
705            "device:fs-root",
706            "target:graphical-session",
707            "service@1000:pipewire",
708            "service@1000/c2:pipewire",
709            "service:external:gym-upstream",
710        ] {
711            let id: UnitId = s.parse().unwrap();
712            assert_eq!(id.to_string(), s);
713        }
714        let ext: UnitId = "service:external:gym-upstream".parse().unwrap();
715        assert_eq!(ext.name, "external:gym-upstream");
716        assert!("bogus:x".parse::<UnitId>().is_err());
717        assert!("service:".parse::<UnitId>().is_err());
718        assert!("service@x:y".parse::<UnitId>().is_err());
719    }
720
721    #[test]
722    fn unit_id_keys_json_maps() {
723        let mut m = BTreeMap::new();
724        m.insert(UnitId::service("sshd"), 1);
725        let json = serde_json::to_string(&m).unwrap();
726        assert_eq!(json, r#"{"service:sshd":1}"#);
727        assert_eq!(serde_json::from_str::<BTreeMap<UnitId, i32>>(&json).unwrap(), m);
728    }
729
730    #[test]
731    fn conditions() {
732        let mut atoms = BTreeSet::new();
733        assert!(Condition::Always.holds(&atoms));
734        assert!(!Condition::SessionEstablished { uid: None, seated: false }.holds(&atoms));
735        atoms.insert(Condition::SessionEstablished { uid: Some(1000), seated: false });
736        assert!(Condition::SessionEstablished { uid: None, seated: false }.holds(&atoms));
737        assert!(Condition::SessionEstablished { uid: Some(1000), seated: false }.holds(&atoms));
738        assert!(!Condition::SessionEstablished { uid: Some(1001), seated: false }.holds(&atoms));
739        let any = Condition::Any(vec![
740            Condition::OnBattery,
741            Condition::SessionEstablished { uid: Some(1000), seated: false },
742        ]);
743        assert!(any.holds(&atoms));
744        assert!(!Condition::All(vec![Condition::OnBattery, Condition::Always]).holds(&atoms));
745    }
746
747    /// S05: an SSH-only session satisfies `SessionEstablished` but not the
748    /// graphical expectation; a seated one satisfies both.
749    #[test]
750    fn only_a_seated_session_expects_a_desktop() {
751        let seat = Condition::SessionEstablished { uid: None, seated: true };
752        let mut atoms: BTreeSet<Condition> = [Condition::SessionEstablished { uid: Some(1000), seated: false }].into();
753        assert!(!seat.holds(&atoms));
754        assert!(Condition::SessionEstablished { uid: None, seated: false }.holds(&atoms));
755        atoms.insert(Condition::SessionEstablished { uid: Some(1002), seated: true });
756        assert!(seat.holds(&atoms));
757        assert!(!Condition::SessionEstablished { uid: Some(1000), seated: true }.holds(&atoms));
758        assert!(Condition::SessionEstablished { uid: Some(1002), seated: true }.holds(&atoms));
759        assert!(Condition::All(vec![Condition::Always, seat]).needs_seat());
760    }
761
762    fn probe(role: ProbeRole, side_effects: SideEffects, cadence: Cadence) -> ProbeDef {
763        ProbeDef {
764            id: ProbeId("p".into()),
765            kind: ProbeKind::SystemdActive,
766            timeout: Millis::secs(10),
767            origin: ProbeOrigin::Canonical,
768            role,
769            cadence,
770            cost: ProbeCost::Trivial,
771            side_effects,
772            establishes: String::new(),
773        }
774    }
775
776    #[test]
777    fn probe_contract() {
778        let m = SideEffects::Measurement { bytes_max: 4096, per: Millis::secs(5) };
779        assert!(probe(ProbeRole::Readiness, m, Cadence::EveryTick).check_contract().is_ok());
780        assert!(probe(ProbeRole::Readiness, SideEffects::Audible, Cadence::OnDemand).check_contract().is_err());
781        assert!(probe(ProbeRole::Diagnostic, SideEffects::Audible, Cadence::EveryTick).check_contract().is_err());
782        assert!(probe(ProbeRole::Diagnostic, SideEffects::Audible, Cadence::OnDemand).check_contract().is_ok());
783    }
784}
planarian_schema/unit.rs

planarian_schema/
unit.rs
