planarian_exec/residue.rs
1//! The residue classifier (§11, owner decision Q5; U3 in docs/assumptions.md):
2//! which unit endings Planarian did not cause are a person's stop, taken as
3//! intended until the next boot, and which are faults or alarms. Pure, so
4//! its rules are checked by Kani (`kani.rs`) in Phase A and by Verus in C.
5
6use planarian_schema::Ending;
7
8/// What the daemon observed about one unit between two ticks.
9#[derive(Clone, Copy, Debug, PartialEq, Eq)]
10pub struct EndingFacts {
11 /// Running or Degraded at the last tick.
12 pub was_up: bool,
13 /// Failed or Stopped now.
14 pub now_down: bool,
15 /// Stopped (inactive), not Failed.
16 pub stopped_cleanly: bool,
17 /// How the main process ended, if the supervisor says.
18 pub ended: Option<Ending>,
19 /// A service (only services have a residue).
20 pub service: bool,
21 /// Planarian acted on it, or changed the generation, since the last tick.
22 pub touched_by_planarian: bool,
23 /// Desired present under the current conditions.
24 pub expected: bool,
25 /// A unit it Requires crashed this tick: it went down with that fault.
26 pub requirement_crashed: bool,
27 /// Security-sensitive.
28 pub security: bool,
29 /// `inferStops = false` (B-11).
30 pub stops_are_faults: bool,
31 /// systemd restarts it (`Restart=`).
32 pub systemd_restarts: bool,
33 /// The posture infers intent (Relaxed or Standard).
34 pub lenient: bool,
35 /// A network tool (`UnitDef.holds`): §12d holds its traffic when it
36 /// fails or is stopped outside Planarian and it is protecting.
37 pub network_tool: bool,
38 /// A hold is in place for it now (`SystemState.holds`, or the host's
39 /// `/run/planarian/hold/<unit>`), read after any attempt to apply one.
40 pub held: bool,
41 /// The daemon has asked the host to hold it for this stop; the host's
42 /// condition (the footprint, a release) decides, as OnFailure= does.
43 pub hold_tried: bool,
44}
45
46#[derive(Clone, Copy, Debug, PartialEq, Eq)]
47pub enum Residue {
48 /// Not a stop outside Planarian (it did not go down, Planarian caused
49 /// it, it is not desired, or it went down with a crash).
50 NotAStop,
51 /// A fault: a crash, a non-zero exit or the OOM killer; or a stop the
52 /// posture or systemd's own restart leaves to the incident manager.
53 Fault,
54 /// A security-sensitive unit stopped outside Planarian: alarmed and
55 /// started again.
56 AlarmSecurity(Ending),
57 /// A unit that must keep running (`inferStops = false`): alarmed and
58 /// started again.
59 AlarmMustRun(Ending),
60 /// Taken as intended: an inferred override until the next boot.
61 Intended(Ending),
62 /// §12d: a network tool stopped outside Planarian, not yet held. Ask
63 /// the host to hold it, then classify again with `hold_tried`.
64 HoldFirst(Ending),
65 /// §12d, §11: its traffic is held, so the stop is "always a fault, §11
66 /// residue": restarted at once without asking (`restarts_held_unit`)
67 /// and alarmed, never taken as intended, whatever its sensitivity.
68 AlarmHeld(Ending),
69}
70
71pub fn classify(f: &EndingFacts) -> Residue {
72 let went_down_unexplained =
73 f.was_up && f.now_down && f.service && !f.touched_by_planarian && f.expected && !f.requirement_crashed;
74 if !went_down_unexplained {
75 return Residue::NotAStop;
76 }
77 // A unit inactive (not failed) after running was stopped on request
78 // (`systemctl stop`), whatever its exit status; a failed one counts only
79 // if a termination signal ended it.
80 let e = match f.ended {
81 Some(e) if e.is_termination() => e,
82 _ if f.stopped_cleanly => Ending::Signal(15),
83 _ => return Residue::Fault,
84 };
85 if f.held {
86 return Residue::AlarmHeld(e);
87 }
88 if f.network_tool && !f.hold_tried {
89 return Residue::HoldFirst(e);
90 }
91 // A network tool the host declined to hold (not protecting) is not a
92 // network-security unit (§12d): the residue rule below applies.
93 if f.security {
94 return Residue::AlarmSecurity(e);
95 }
96 if f.stops_are_faults {
97 return Residue::AlarmMustRun(e);
98 }
99 if f.lenient && !f.systemd_restarts { Residue::Intended(e) } else { Residue::Fault }
100}
101
102#[cfg(test)]
103mod tests {
104 use super::*;
105 use proptest::prelude::*;
106
107 fn ending() -> impl Strategy<Value = Ending> {
108 prop_oneof![any::<i32>().prop_map(Ending::Exited), any::<i32>().prop_map(Ending::Signal), Just(Ending::OomKill)]
109 }
110
111 /// Each flag leans (4 in 5) towards the value that reaches `Intended`
112 /// (an unexplained stop of an untagged service under a lenient
113 /// posture), so the property meets that path often, not one case in
114 /// thousands; every combination is still generated.
115 fn lean(towards: bool) -> impl Strategy<Value = bool> {
116 proptest::bool::weighted(if towards { 0.8 } else { 0.2 })
117 }
118
119 fn facts() -> impl Strategy<Value = EndingFacts> {
120 (
121 (lean(true), lean(true), lean(true), lean(true), lean(false), lean(true), lean(false)),
122 (lean(false), lean(false), lean(false), lean(true), any::<bool>(), any::<bool>(), any::<bool>()),
123 proptest::option::weighted(0.9, prop_oneof![4 => Just(Ending::Signal(15)), 1 => ending()]),
124 )
125 .prop_map(
126 |(
127 (was_up, now_down, stopped_cleanly, service, touched_by_planarian, expected, requirement_crashed),
128 (security, stops_are_faults, systemd_restarts, lenient, network_tool, held, hold_tried),
129 ended,
130 )| EndingFacts {
131 was_up,
132 now_down,
133 stopped_cleanly,
134 ended,
135 service,
136 touched_by_planarian,
137 expected,
138 requirement_crashed,
139 security,
140 stops_are_faults,
141 systemd_restarts,
142 lenient,
143 network_tool,
144 held,
145 hold_tried,
146 },
147 )
148 }
149
150 /// main's classifier before #55, verbatim (the reference for the frame
151 /// condition: where #55 does not apply, nothing changes).
152 fn classify_before(f: &EndingFacts) -> Residue {
153 let went_down_unexplained =
154 f.was_up && f.now_down && f.service && !f.touched_by_planarian && f.expected && !f.requirement_crashed;
155 if !went_down_unexplained {
156 return Residue::NotAStop;
157 }
158 let e = match f.ended {
159 Some(e) if e.is_termination() => e,
160 _ if f.stopped_cleanly => Ending::Signal(15),
161 _ => return Residue::Fault,
162 };
163 if f.security {
164 return Residue::AlarmSecurity(e);
165 }
166 if f.stops_are_faults {
167 return Residue::AlarmMustRun(e);
168 }
169 if f.lenient && !f.systemd_restarts { Residue::Intended(e) } else { Residue::Fault }
170 }
171
172 proptest! {
173 #![proptest_config(ProptestConfig { cases: 1024, ..ProptestConfig::default() })]
174
175 /// The frame condition (prop-auditor, #55): a unit not held, and not
176 /// a network tool awaiting its hold attempt (not one, or asked and
177 /// declined), is classified exactly as before. So #55 holds only what
178 /// §12d holds: not every network tool, not every lenient unit.
179 #[test]
180 fn outside_a_hold_the_classifier_is_unchanged(f in facts()) {
181 if !f.held && (!f.network_tool || f.hold_tried) {
182 prop_assert_eq!(classify(&f), classify_before(&f), "{:?}", f);
183 }
184 }
185
186 /// §12d, §11: a unit whose traffic is held is never taken as
187 /// intended; and a network tool's stop is never taken as intended
188 /// before the host has been asked to hold it (and declined).
189 #[test]
190 fn held_or_unasked_network_tools_are_never_intended(f in facts()) {
191 let r = classify(&f);
192 if f.held {
193 prop_assert!(!matches!(r, Residue::Intended(_)), "{f:?} -> {r:?}");
194 }
195 if f.network_tool && !f.hold_tried {
196 prop_assert!(!matches!(r, Residue::Intended(_)), "{f:?} -> {r:?}");
197 }
198 // A hold is only asked for a network tool, once.
199 if matches!(r, Residue::HoldFirst(_)) {
200 prop_assert!(f.network_tool && !f.hold_tried && !f.held);
201 }
202 }
203 }
204}