kernel/discard/
verdict.rs

1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at https://mozilla.org/MPL/2.0/.
4// Copyright (c) 2026 2youg1 and the sprawling contributors
5
6//! Discard verdicts: the decision table.
7//! The part `crates/kernel/spec/Discard.lean` specifies this module with the
8//! rest of `kernel::discard`.
9
10use super::request::{DenyReason, DiscardRequest};
11
12/// Deliberately exhaustive verdict.
13#[derive(Debug, Clone, Copy, PartialEq, Eq)]
14pub enum DiscardVerdict {
15    Allow,
16    Deny { reason: DenyReason },
17}
18
19/// The decision table, in fixed order: no plan denies, taint
20/// denies, the rest passes.
21///
22/// Scale and ownership pass because a planned discard carries a
23/// restoration and is therefore reversible: no file count, byte count
24/// or other resident's registered asset interrupts a person, because an
25/// interruption is not a rule. What still bounds a delete in advance is written where
26/// rules live — the write domain says which files a resident reaches
27/// at all, and the registry keeps the evidence that puts a deleted
28/// asset back.
29pub fn decide(req: &DiscardRequest) -> DiscardVerdict {
30    let taint = match req {
31        DiscardRequest::Unplanned { .. } => {
32            return DiscardVerdict::Deny {
33                reason: DenyReason::NoRestoration,
34            };
35        }
36        DiscardRequest::Planned(discard) => discard.taint(),
37    };
38    if taint.is_empty() {
39        DiscardVerdict::Allow
40    } else {
41        DiscardVerdict::Deny {
42            reason: DenyReason::Tainted,
43        }
44    }
45}
46
47#[cfg(test)]
48#[allow(
49    clippy::unwrap_used,
50    clippy::expect_used,
51    clippy::panic,
52    clippy::indexing_slicing,
53    reason = "test code"
54)]
55mod tests {
56    use super::super::request::{Discard, DiscardRequest, Restoration};
57    use super::*;
58    use crate::address::Address;
59    use crate::budget::ByteLen;
60    use crate::locator::Locator;
61    use crate::taint::{TaintSet, TaintSource};
62    fn addr(raw: &str) -> Address {
63        Address::parse(raw).unwrap()
64    }
65    fn tracked() -> Restoration {
66        Restoration::Tracked(Locator::parse(&format!("file:b/x.md@{}", "ab".repeat(20))).unwrap())
67    }
68    fn clean(paths: Vec<Address>, bytes: u64) -> Discard {
69        Discard::new(paths, tracked(), TaintSet::empty(), ByteLen::new(bytes)).unwrap()
70    }
71
72    #[test]
73    fn the_decision_table_holds_in_order() {
74        // Allow: planned and clean-handed, at any scale.
75        assert_eq!(
76            decide(&DiscardRequest::Planned(clean(vec![addr("b/x.md")], 100))),
77            DiscardVerdict::Allow
78        );
79        let many: Vec<Address> = (0..17).map(|i| addr(&format!("b/f{i}.md"))).collect();
80        assert_eq!(
81            decide(&DiscardRequest::Planned(clean(many, 4_000_000))),
82            DiscardVerdict::Allow,
83            "a big delete that can be put back is a delete"
84        );
85        // Tainted denies, whatever the scale.
86        let tainted = Discard::new(
87            vec![addr("b/x.md")],
88            tracked(),
89            TaintSet::of(TaintSource::new("web:evil").unwrap()),
90            ByteLen::new(1),
91        )
92        .unwrap();
93        assert_eq!(
94            decide(&DiscardRequest::Planned(tainted)),
95            DiscardVerdict::Deny {
96                reason: DenyReason::Tainted
97            }
98        );
99        // Unplanned denies: no restoration, no delete.
100        assert_eq!(
101            decide(&DiscardRequest::Unplanned {
102                paths: vec![addr("b/x.md")],
103                taint: TaintSet::empty(),
104                total_bytes: ByteLen::new(1)
105            }),
106            DiscardVerdict::Deny {
107                reason: DenyReason::NoRestoration
108            }
109        );
110    }
111}
112
113// No kani harness lives here. Deciding a discard takes a `Vec` of
114// addresses and a `BTreeSet` of taint sources, and CBMC cannot bound
115// those loops: one run burned six hours and a second ran forty-five
116// minutes under `--default-unwind 32`, both on `tainted_never_allows`,
117// and neither returned. The fail-closed propositions are held by the
118// tests above (`crates/kernel/Spec.lean` §2).
kernel/discard/verdict.rs

kernel/discard/
verdict.rs
