Module taint 

The taint ring. One axiom: external content is always data. Tainted::new is the city-wide sole entrance for foreign bytes; reads hand out borrows, derivation unions provenance, and no method ever returns the bare value — “washing it clean” is a compile error, not a review finding. The part crates/kernel/spec/Taint.lean specifies this module.

Deliberately absent: serde on Tainted (deserialization would be a second entrance and a forged-empty-taint hole) and any into_inner.

Structs

TaintSet

Union semilattice of provenance. Empty means internally produced. Serializable (event payloads and approval items carry source lists); order is BTreeSet’s, hence deterministic.

TaintSource

Non-empty provenance label, e.g. web:example.com, file:upload.

Tainted

External content with its provenance welded on. The value is private; peek lends, map/join derive with automatic union, and nothing returns T by value.