Module secret 

Secret shape judgment, the secret: reference grammar and Sealed<T> . Detection is shape-table-first, entropy-second; both are hand-written, regex-free, backtracking-free and float-free — entropy runs in fixed point so the judgment is deterministic and kani-provable. False positives are the accepted normal: the entrance replaces losslessly, only the exits refuse. The part crates/kernel/spec/Secret.lean specifies this module.

Structs

Sealed

A value that cannot reach any sink: no Debug, no Display, no serde, no Clone; drop zeroizes (secrecy::SecretBox). Expose call sites are whitelisted by xtask secret (EXPOSE_WHITELIST).

SecretRef

secret:<realm>/<name>. Deliberately a separate parser from Locator: sharing the grammar would mean a read path could resolve a secret (7.1’s type-level answer). Malformed shapes are E_CONFIG_INVALID.

SecretSpan

One detected span. provider names the shape-table entry; None is an entropy hit. The span carries offsets only — never the bytes (a finding that quoted its match would itself be a leak surface).

Functions

names_a_credential

Whether a name reads as the name of a credential.

scan

Custody’s detection half. Shape table first; entropy second over token runs of at least [ENTROPY_SPAN_MIN_BYTES] that no shape already claimed. Pure, total, deterministic.