Function write_budget_refusal 

pub fn write_budget_refusal(
    tool_name: &str,
    arguments: &Value,
    workdir: &Path,
    budget: &WriteBudget,
) -> Option<String>

Refuse a call that would take the run past a write ceiling, or fill the disk.

Returns the refusal, or None to proceed.

Two shapes of call reach here and they are not symmetric. A write_file declares its size, so it is judged before it runs and nothing is written. A shell redirect does not, so it is judged on what the run has already spent - which stops the call after the one that overran, not the one that did. That asymmetry is inherent: Leviath never sees those bytes, and the alternative is refusing every redirect on a run near its budget.

The disk check applies to both, and to a shell call with any write target at all: a machine with no room left should not be handed a command that writes, whatever its size turns out to be.