kernel/discard.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: deletion as an effect class, judged by effect and never by
7//! intent. C14 in the type: a Discard without a
8//! restoration plan cannot be constructed; the unplanned path exists only
9//! as a request shape for exec forecasts — and the door denies it.
10//! This module is the discard door's sole authority; `gate::discard`
11//! delegates wholly and only shapes the refusal.
12//! The part `crates/kernel/spec/Discard.lean` specifies this module.
13
14mod forecast;
15mod request;
16mod verdict;
17
18pub use forecast::{DiscardForecast, forecast};
19pub use request::{DenyReason, Discard, DiscardRequest, Restoration};
20pub use verdict::{DiscardVerdict, decide};