Module write_domain 

WriteDomain prefix checking and edit-war detection. C17 is enforced twice on purpose: a reserved prefix cannot be constructed into a domain, and a reserved target is refused at judgment even so — fail-closed has no single point of failure. The part crates/kernel/spec/WriteDomain.lean specifies this module.

Structs

DomainPrefixes

A validated set of prefixes.

EditSample

One observed write, in time order (slice order is the clock).

Enums

DocumentReason

Why a documents domain refuses a target that is inside its prefixes.

DomainVerdict

Deliberately exhaustive verdict; prefixes feeds the refusal’s nearby list.

EditWarVerdict

WriteDomain

The set of prefixes one actor may write under, and what it may write inside them.

WriteLimit

What a run may do to a file that already exists inside its write domain (crates/kernel/spec/WriteDomain.lean §8-78).

Functions

observe_edit_war

Edit-war detection: a “reclaim” is run X editing a file back after run Y took it (X, Y, X). Reclaims at or over EDIT_WAR_FREEZE freeze that file. Per-address, deterministic: addresses are examined in BTreeMap order, first hit wins.