Skip to main content

kernel/
secret.rs

1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at https://mozilla.org/MPL/2.0/.
4// Copyright (c) 2026 2youg1 and the sprawling contributors
5
6//! Secret shape judgment, the `secret:` reference grammar and `Sealed<T>`
7//!. Detection is shape-table-first, entropy-second;
8//! both are hand-written, regex-free, backtracking-free and float-free —
9//! entropy runs in fixed point so the judgment is deterministic and
10//! kani-provable. False positives are the accepted normal: the entrance
11//! replaces losslessly, only the exits refuse.
12//! The part `crates/kernel/spec/Secret.lean` specifies this module.
13
14mod hex_run;
15mod scan;
16mod sealed;
17mod span;
18
19pub use scan::{names_a_credential, scan};
20pub use sealed::Sealed;
21pub use span::{SecretRef, SecretSpan};