crates/nornir-purgatory/src/subtract.rs
//! **The subtractor and its three invariants** — each a test, not a convention.
//!
//! Stage 1 (the build-thing variant's committed fragments) is POLICY: a floor
//! that cannot regress. Stage 2 (this) is EVIDENCE: a subtraction on that floor.
//! `workspace_nordisk/mimir-v2.md`:
//!
//! 1. **Subtract only.** Stage 2 may never add or re-enable. Evidence must not be
//! able to weaken policy.
//! 2. **Hardening is immune.** Every symbol named by a stage-1 fragment is
//! off-limits. *"Nothing calls `seccomp(2)`"* is true of a clean boot;
//! dropping `CONFIG_SECCOMP` for it would be catastrophic.
//! 3. **Fail closed on doubt.** No evidence, stale evidence, or an unsound call
//! graph ⇒ subtract NOTHING.
//!
//! Invariant 3 is not hypothetical and it is why this crate exists before the
//! gate does. On 2026-09-06 a red test showed `ra_ingest` fabricating a
//! cross-repo call edge — def-site keys are `file#Lline:Ccol`, workspace-relative
//! and merged across members, so two members' `src/lib.rs` line 7 are the SAME
//! STRING. A gate on that graph *refuses clean builds and passes dirty ones*.
//! That input must yield zero subtractions, and [`Freshness::Unsound`] is how it
//! says so.
//!
//! # And the decisions that are NOT taken here
//!
//! mimir-v2 §8 leaves two open, both the owner's, and neither is anticipated in
//! code: the `RECIPE_SCHEMA` 4→5 bump, and **whether stage 2 may subtract at all
//! on the assured appliance or must report only**. [`Policy::report_only`] exists
//! so the second can be answered either way without touching this logic — it is
//! a switch with no default opinion baked in, and the caller must state it.
use std::collections::BTreeSet;
/// How much the evidence can be trusted. Drives invariant 3.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Freshness {
/// Measured from a graph believed sound, at this revision.
Fresh { revision: String },
/// Evidence exists but is older than the code it describes.
Stale { why: String },
/// The graph is known to be wrong (the moniker collision, a failed ingest).
Unsound { why: String },
/// There is no evidence at all.
Absent,
}
impl Freshness {
/// May ANY subtraction be proposed from evidence of this quality?
///
/// Only `Fresh`. Three of the four arms are refusals, which is the ratio
/// invariant 3 asks for — doubt is the common case, not the exception.
#[must_use]
pub fn is_usable(&self) -> bool {
matches!(self, Freshness::Fresh { .. })
}
/// Why nothing was subtracted, for the decision record.
#[must_use]
pub fn refusal(&self) -> Option<String> {
match self {
Freshness::Fresh { .. } => None,
Freshness::Stale { why } => Some(format!("evidence is STALE ({why})")),
Freshness::Unsound { why } => Some(format!("call graph is UNSOUND ({why})")),
Freshness::Absent => Some("there is NO evidence".to_string()),
}
}
}
/// **What an evidence source is competent to judge.**
///
/// A syscall probe knows nothing about a NIC driver: it can say `SECCOMP` was
/// reached and `BPF_SYSCALL` was not, and about `E1000` it has no opinion. The
/// first real [`crate::EvidenceSource`] made this unavoidable — without it,
/// fresh probe evidence subtracted every enabled symbol it had not seen, which
/// was every driver in the kernel. A symbol outside the scope is SPARED, and the
/// record says so.
///
/// The default is the empty `Only` — an evidence source that has not stated its
/// competence judges nothing. `Whole` must be said out loud.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Scope {
/// The evidence covers every symbol (a complete call graph).
Whole,
/// The evidence can only speak about these.
Only(BTreeSet<String>),
}
impl Default for Scope {
fn default() -> Scope {
Scope::Only(BTreeSet::new())
}
}
impl Scope {
#[must_use]
pub fn covers(&self, symbol: &str) -> bool {
match self {
Scope::Whole => true,
Scope::Only(s) => s.contains(symbol),
}
}
}
/// What the appliance's own code demonstrably reaches.
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct Demand {
/// Kconfig symbols the measured code needs.
pub symbols: BTreeSet<String>,
/// Which symbols the evidence may pronounce on at all. See [`Scope`].
pub scope: Scope,
pub freshness_note: String,
}
/// The caller's stance, stated rather than defaulted.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Policy {
/// Symbols stage 1 named. **Immune** — invariant 2.
pub immune: BTreeSet<String>,
/// Propose and record, but never actually subtract. mimir-v2 §8 leaves this
/// open for the assured appliance and it is the owner's call, so there is no
/// default: the caller says which it means.
pub report_only: bool,
}
/// One proposed removal, with the reason that ships with the artifact.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Subtraction {
pub symbol: String,
pub why: String,
}
/// What the gate decided, and why — this is the record that ships.
///
/// *"Otherwise nobody can answer later why a shipped appliance lacks something,
/// and the next person re-adds it blind."*
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Decision {
pub subtractions: Vec<Subtraction>,
/// Considered and spared, with the reason — immunity or demand.
pub spared: Vec<Subtraction>,
/// Set when nothing was subtracted because of invariant 3.
pub refused: Option<String>,
pub report_only: bool,
pub evidence: Freshness,
}
impl Decision {
/// Rows in the workspace form (`nornir-workspace.toml:36`).
#[must_use]
pub fn rows(&self) -> Vec<String> {
let mut out = Vec::new();
if let Some(r) = &self.refused {
out.push(format!(
"{:<28} as bra FAIL CLOSED: {r}, so ZERO symbols were subtracted. Invariant 3 — no evidence, stale evidence or an unsound call graph subtracts NOTHING. A gate that guessed here would refuse clean builds and pass dirty ones.",
"purgatory-refused"
));
return out;
}
for s in &self.subtractions {
out.push(format!(
"{:<28} {} {} CONFIG_{}: {}",
format!("purge-{}", s.symbol.to_ascii_lowercase()),
if self.report_only {
"new "
} else {
"done "
},
if self.report_only {
"WOULD SUBTRACT (report-only)"
} else {
"SUBTRACTED"
},
s.symbol,
s.why
));
}
out
}
}
/// **Propose subtractions from `effective`, honouring all three invariants.**
///
/// `effective` is what actually shipped; `demand` is what the code reaches.
pub fn propose(
effective: &crate::kconfig::Effective,
demand: &Demand,
policy: &Policy,
evidence: &Freshness,
) -> Decision {
// ── INVARIANT 3, first and before anything is examined ───────────────────
if !evidence.is_usable() {
return Decision {
subtractions: Vec::new(),
spared: Vec::new(),
refused: evidence.refusal(),
report_only: policy.report_only,
evidence: evidence.clone(),
};
}
let mut subtractions = Vec::new();
let mut spared = Vec::new();
for symbol in effective.enabled() {
// ── INVARIANT 2 — a stage-1 symbol is untouchable, whatever evidence says.
if policy.immune.contains(symbol) {
spared.push(Subtraction {
symbol: symbol.to_string(),
why: "IMMUNE: named by a stage-1 fragment (policy). Evidence may not weaken \
policy — 'nothing calls seccomp(2)' is true of a clean boot."
.to_string(),
});
continue;
}
if demand.symbols.contains(symbol) {
spared.push(Subtraction {
symbol: symbol.to_string(),
why: "REACHED: the measured call graph demands it".to_string(),
});
continue;
}
// ── SCOPE — the evidence has no opinion here, so neither do we.
if !demand.scope.covers(symbol) {
spared.push(Subtraction {
symbol: symbol.to_string(),
why: "OUT OF SCOPE: the evidence cannot see this symbol (a syscall probe knows \
nothing about a driver), so absence of demand is not absence of use"
.to_string(),
});
continue;
}
subtractions.push(Subtraction {
symbol: symbol.to_string(),
why: format!(
"enabled in the shipped kernel, named by no stage-1 fragment, and not reached \
by the measured code ({})",
demand.freshness_note
),
});
}
// ── INVARIANT 1 is structural: nothing above can emit an ADD. `Subtraction`
// is the only output type and it carries no value to set. There is no arm
// that turns evidence into an enable, which is the strongest form the
// guarantee takes — the same shape as tunnr's `exposure::Verdict`, which
// has no wildcard arm for the same reason.
Decision {
subtractions,
spared,
refused: None,
report_only: policy.report_only,
evidence: evidence.clone(),
}
}
/// **The gate's contract**, so it can be tested without a warehouse or a
/// kernel tree (`mimir-v2.md` §4).
pub trait Subtractor {
fn propose(
&self,
effective: &crate::kconfig::Effective,
demand: &Demand,
evidence: &Freshness,
) -> Decision;
/// Stage 1's symbols as THIS subtractor protects them.
fn immune(&self) -> &BTreeSet<String>;
}
/// The bare policy: [`propose`] with the fragment symbols and nothing more.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PolicySubtractor {
pub policy: Policy,
}
impl Subtractor for PolicySubtractor {
fn propose(
&self,
effective: &crate::kconfig::Effective,
demand: &Demand,
evidence: &Freshness,
) -> Decision {
propose(effective, demand, &self.policy, evidence)
}
fn immune(&self) -> &BTreeSet<String> {
&self.policy.immune
}
}
/// **The first real [`Subtractor`]: policy read through the Kconfig graph.**
///
/// Three things the bare [`propose`] cannot know without a tree:
///
/// 1. **Invariant 2 is transitive.** A fragment that names
/// `STACKPROTECTOR_STRONG` has also claimed `STACKPROTECTOR`, because it
/// `depends on` it; subtract the dependency and `olddefconfig` silently drops
/// the hardening symbol. So [`Subtractor::immune`] here is
/// [`KconfigTree::policy_closure`] of the fragment symbols — what policy
/// implies is policy.
/// 2. **Futility is reported.** A subtraction of `X` while an enabled SURVIVOR
/// `select`s `X` is a directive `olddefconfig` will put straight back — the
/// 2026-09-07 `BLK_DEV_IO_TRACE select DEBUG_FS` defect. It is spared and the
/// record names the selector and the Kconfig file, so the next step is obvious.
/// 3. **Invariant 3 has a Kconfig arm.** A graph read from one kernel release
/// says nothing about a `.config` produced by another, and a `.config` with no
/// release banner cannot be matched at all. Both are `Stale` and subtract nothing.
///
/// [`KconfigTree::policy_closure`]: crate::kconfig::tree::KconfigTree::policy_closure
#[derive(Debug, Clone)]
pub struct KconfigAwareSubtractor<'t> {
tree: &'t crate::kconfig::tree::KconfigTree,
seeds: BTreeSet<String>,
policy: Policy,
}
impl<'t> KconfigAwareSubtractor<'t> {
/// `seeds` are the fragment symbols ([`crate::immune_from_fragments`]);
/// `report_only` is `mimir-v2.md` §8's open question and has no default.
#[must_use]
pub fn new(
tree: &'t crate::kconfig::tree::KconfigTree,
seeds: BTreeSet<String>,
report_only: bool,
) -> KconfigAwareSubtractor<'t> {
let immune = tree.policy_closure(&seeds);
KconfigAwareSubtractor {
tree,
seeds,
policy: Policy {
immune,
report_only,
},
}
}
/// The fragment symbols before the closure widened them.
#[must_use]
pub fn seeds(&self) -> &BTreeSet<String> {
&self.seeds
}
}
impl Subtractor for KconfigAwareSubtractor<'_> {
fn propose(
&self,
effective: &crate::kconfig::Effective,
demand: &Demand,
evidence: &Freshness,
) -> Decision {
// ── INVARIANT 3, the Kconfig arm: the graph must be THIS kernel's.
let evidence = if !evidence.is_usable() {
evidence.clone()
} else {
match (effective.release(), self.tree.release()) {
(Some(c), Some(t)) if c != t => Freshness::Stale {
why: format!("the produced .config is kernel {c} but the Kconfig graph was read from a {t} tree"),
},
(None, _) => Freshness::Stale {
why: "the produced .config carries no `# Linux/<arch> <release> Kernel Configuration` banner, so it cannot be matched to the Kconfig graph".to_string(),
},
(_, None) => Freshness::Stale {
why: "the Kconfig tree has no VERSION/PATCHLEVEL/SUBLEVEL in its Makefile, so it cannot be matched to the .config".to_string(),
},
_ => evidence.clone(),
}
};
let mut d = propose(effective, demand, &self.policy, &evidence);
// ── FUTILITY: a surviving selector would undo the subtraction.
let cut: BTreeSet<String> = d.subtractions.iter().map(|s| s.symbol.clone()).collect();
let enabled = effective.enabled();
let mut keep = Vec::new();
for s in std::mem::take(&mut d.subtractions) {
let survivors: Vec<_> = self
.tree
.selected_by(&s.symbol)
.iter()
.filter(|sel| enabled.contains(sel.by.as_str()) && !cut.contains(&sel.by))
.collect();
if survivors.is_empty() {
keep.push(s);
} else {
let who: Vec<String> = survivors
.iter()
.map(|sel| format!("{} ({}:{})", sel.by, sel.file, sel.line))
.collect();
d.spared.push(Subtraction {
symbol: s.symbol.clone(),
why: format!(
"SELECTED BY {}: subtracting CONFIG_{} alone is futile — olddefconfig would put it straight back through `select`. Subtract the selector first, or accept it.",
who.join(", "),
s.symbol
),
});
}
}
d.subtractions = keep;
d
}
fn immune(&self) -> &BTreeSet<String> {
&self.policy.immune
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::kconfig::Effective;
fn shipped() -> Effective {
Effective::from_produced_config(
"CONFIG_SECCOMP=y\nCONFIG_BLK_DEV_IO_TRACE=y\nCONFIG_DEBUG_FS=y\n\
CONFIG_E1000=m\n# CONFIG_ATA is not set\n",
)
}
fn immune(syms: &[&str]) -> BTreeSet<String> {
syms.iter().map(|s| (*s).to_string()).collect()
}
fn fresh() -> Freshness {
Freshness::Fresh {
revision: "deadbeef".into(),
}
}
fn demand(syms: &[&str]) -> Demand {
Demand {
symbols: syms.iter().map(|s| (*s).to_string()).collect(),
// A complete call graph — said out loud, because the default is not.
scope: Scope::Whole,
freshness_note: "call_edges @ deadbeef".into(),
}
}
/// **INVARIANT 3 — the one that matters most, driven all four ways.** The
/// 2026-09-06 fabricated cross-repo edge is `Unsound`, and it must subtract
/// nothing at all.
#[test]
fn doubt_of_every_kind_subtracts_absolutely_nothing() {
for ev in [
Freshness::Absent,
Freshness::Stale {
why: "older than HEAD".into(),
},
Freshness::Unsound {
why: "ra_ingest moniker collision fabricates cross-repo edges".into(),
},
] {
let d = propose(
&shipped(),
&demand(&[]),
&Policy {
immune: immune(&[]),
report_only: false,
},
&ev,
);
assert!(d.subtractions.is_empty(), "{ev:?} must subtract nothing");
assert!(d.refused.is_some(), "{ev:?} must say WHY nothing happened");
assert!(d.rows()[0].contains("FAIL CLOSED"));
}
// The non-vacuous half: with FRESH evidence the same input DOES subtract,
// so the three refusals above are not merely a function that never works.
let d = propose(
&shipped(),
&demand(&[]),
&Policy {
immune: immune(&[]),
report_only: false,
},
&fresh(),
);
assert!(
!d.subtractions.is_empty(),
"fresh evidence must actually subtract"
);
assert!(d.refused.is_none());
}
/// **INVARIANT 2 — `CONFIG_SECCOMP` is the worked example, and it is
/// catastrophic to get wrong.** Nothing calls `seccomp(2)` on a clean boot.
#[test]
fn a_hardening_symbol_is_immune_even_when_nothing_reaches_it() {
let d = propose(
&shipped(),
&demand(&[]), // nothing is reached — maximum pressure to subtract
&Policy {
immune: immune(&["SECCOMP"]),
report_only: false,
},
&fresh(),
);
let cut: Vec<&str> = d.subtractions.iter().map(|s| s.symbol.as_str()).collect();
assert!(!cut.contains(&"SECCOMP"), "SECCOMP must survive: {cut:?}");
assert!(d
.spared
.iter()
.any(|s| s.symbol == "SECCOMP" && s.why.contains("IMMUNE")));
// …and the guard is not simply sparing everything.
assert!(cut.contains(&"BLK_DEV_IO_TRACE"), "{cut:?}");
}
/// **INVARIANT 1 — structural.** There is no output that can enable a symbol:
/// a disabled one is never even a candidate, and `Subtraction` carries no
/// value to set.
#[test]
fn nothing_disabled_can_ever_be_turned_back_on() {
let d = propose(
&shipped(),
&demand(&["ATA"]), // evidence CLAIMS the code needs a vetoed symbol
&Policy {
immune: immune(&[]),
report_only: false,
},
&fresh(),
);
assert!(
!d.subtractions.iter().any(|s| s.symbol == "ATA")
&& !d.spared.iter().any(|s| s.symbol == "ATA"),
"a symbol that is OFF is not a candidate in either direction"
);
// Demand cannot re-enable: ATA is still absent from every output.
assert!(d.rows().iter().all(|r| !r.contains("ATA")));
}
/// A module is surface and is a candidate; a reached symbol is spared.
#[test]
fn modules_are_candidates_and_reached_symbols_are_spared() {
let d = propose(
&shipped(),
&demand(&["E1000"]),
&Policy {
immune: immune(&[]),
report_only: false,
},
&fresh(),
);
assert!(d
.spared
.iter()
.any(|s| s.symbol == "E1000" && s.why.contains("REACHED")));
let d2 = propose(
&shipped(),
&demand(&[]),
&Policy {
immune: immune(&[]),
report_only: false,
},
&fresh(),
);
assert!(
d2.subtractions.iter().any(|s| s.symbol == "E1000"),
"an unreached module is compiled, shipped and loadable — it is surface"
);
}
/// `report_only` changes the WORDS and not the analysis — so the assured
/// appliance can be answered either way (mimir-v2 §8, the owner's) without a
/// second code path to keep in step.
#[test]
fn report_only_proposes_the_same_set_and_says_it_did_not_act() {
let act = propose(
&shipped(),
&demand(&[]),
&Policy {
immune: immune(&[]),
report_only: false,
},
&fresh(),
);
let rep = propose(
&shipped(),
&demand(&[]),
&Policy {
immune: immune(&[]),
report_only: true,
},
&fresh(),
);
assert_eq!(
act.subtractions, rep.subtractions,
"the analysis must not differ"
);
assert!(rep
.rows()
.iter()
.all(|r| r.contains("WOULD SUBTRACT (report-only)")));
assert!(act
.rows()
.iter()
.all(|r| r.contains("SUBTRACTED") && !r.contains("WOULD")));
}
}