Module discard 

Discard: deletion as an effect class, judged by effect and never by intent. C14 in the type: a Discard without a restoration plan cannot be constructed; the unplanned path exists only as a request shape for exec forecasts — and the door denies it. This module is the discard door’s sole authority; gate::discard delegates wholly and only shapes the refusal. The part crates/kernel/spec/Discard.lean specifies this module.

Structs

Discard

A planned discard. Private fields; the sole constructor checks the plan’s scheme — C14’s type half.

Enums

DenyReason

Why a discard is refused. Two reasons, and both are rules a person can read: a delete with no way back, and a delete a run asked for because something outside the city told it to.

DiscardForecast

Deliberately exhaustive forecast.

DiscardRequest

What reaches the door: a planned discard, or an unplanned request from the exec forecast path (text prediction cannot mint plans).

DiscardVerdict

Deliberately exhaustive verdict.

Restoration

Tracked rides git (file:), Interred rides CAS (cas:), Rebuildable names its reason. No fourth storage authority exists.

Functions

decide

The decision table, in fixed order: no plan denies, taint denies, the rest passes.

forecast

The pre-judgment: Program reads (path, args) whole — a whitelisted name with poisoned args is no trust at all; Python and Shell get substring conservatism.