Skip to main content

brainos_identity/
types.rs

1//! Core identity types.
2
3use std::fmt;
4
5use async_trait::async_trait;
6use serde::{Deserialize, Serialize};
7use thiserror::Error;
8
9/// Stable identifier for the human owner of the Brain instance. Single-user
10/// by design (per `docs/ROADMAP.md` § "What Is NOT on the Roadmap").
11#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)]
12pub struct UserId(pub String);
13
14impl fmt::Display for UserId {
15    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16        f.write_str(&self.0)
17    }
18}
19
20impl From<&str> for UserId {
21    fn from(s: &str) -> Self {
22        Self(s.to_string())
23    }
24}
25
26impl From<String> for UserId {
27    fn from(s: String) -> Self {
28        Self(s)
29    }
30}
31
32/// Opaque agent identifier. Examples: `"claude-code"`, `"cursor"`,
33/// `"terminal:zsh"`, `"reflex:fs"`, `"mcp:stdio"`.
34#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)]
35pub struct AgentId(pub String);
36
37impl fmt::Display for AgentId {
38    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
39        f.write_str(&self.0)
40    }
41}
42
43impl From<&str> for AgentId {
44    fn from(s: &str) -> Self {
45        Self(s.to_string())
46    }
47}
48
49impl From<String> for AgentId {
50    fn from(s: String) -> Self {
51        Self(s)
52    }
53}
54
55/// Authorization tier — used both as the principal's authorization level and
56/// as the tier required by an action. Ordered so `>=` answers "does this
57/// principal's tier satisfy the action's required tier?".
58///
59/// Per-tier policy (`requires_confirmation`, `default_timeout`) mirrors
60/// VISION §6 (human in the loop): each tier maps to a distinct approval
61/// ceremony. `Read`/`Write`/`Execute` are auto-approved (with audit
62/// recording); `Destructive` and `External` block on explicit human
63/// approval.
64///
65/// # Examples
66///
67/// ```
68/// use brainos_identity::Tier;
69///
70/// // Tiers are ordered by escalating risk.
71/// assert!(Tier::Read < Tier::Write);
72/// assert!(Tier::Execute < Tier::External);
73///
74/// // Only the top two tiers block on explicit human approval.
75/// assert!(!Tier::Execute.requires_confirmation());
76/// assert!(Tier::Destructive.requires_confirmation());
77/// ```
78#[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, Hash)]
79#[serde(rename_all = "snake_case")]
80pub enum Tier {
81    /// Read-only — never requires confirmation.
82    Read,
83    /// Write — implicit confirmation, user can undo.
84    Write,
85    /// Execute — sandboxed, reversible.
86    Execute,
87    /// Destructive — explicit approval required.
88    Destructive,
89    /// External — explicit approval + credential audit.
90    External,
91}
92
93impl Tier {
94    /// Whether this tier requires explicit confirmation before execution.
95    pub fn requires_confirmation(self) -> bool {
96        matches!(self, Tier::Destructive | Tier::External)
97    }
98
99    /// Default approval timeout for this tier.
100    ///
101    /// These are kept humane (tens of seconds, not minutes): an interactive
102    /// user answers in seconds, and the non-interactive CLI now fast-fails an
103    /// unanswerable gate (W1) instead of blocking to the deadline, so a long
104    /// server timeout only ever punished people. Destructive gets the most
105    /// breathing room because an irreversible action deserves a beat of
106    /// consideration; Read the least because it barely warrants a pause.
107    pub fn default_timeout(self) -> std::time::Duration {
108        match self {
109            Tier::Read => std::time::Duration::from_secs(30),
110            Tier::Write => std::time::Duration::from_secs(45),
111            Tier::Execute => std::time::Duration::from_secs(60),
112            Tier::Destructive => std::time::Duration::from_secs(90),
113            Tier::External => std::time::Duration::from_secs(60),
114        }
115    }
116}
117
118impl fmt::Display for Tier {
119    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
120        f.write_str(match self {
121            Tier::Read => "read",
122            Tier::Write => "write",
123            Tier::Execute => "execute",
124            Tier::Destructive => "destructive",
125            Tier::External => "external",
126        })
127    }
128}
129
130/// Who is asking. Threaded through `Signal` so every downstream component
131/// (audit, confirmation, capability index) can read it.
132#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
133pub struct Principal {
134    pub user_id: UserId,
135    pub agent_id: AgentId,
136    /// Dotted-string capability scopes the principal holds. Wildcards like
137    /// `fs.*` match every action under `fs`. Empty list = no permissions.
138    pub scopes: Vec<String>,
139    pub tier: Tier,
140}
141
142impl Principal {
143    /// Returns `true` iff `verb_ns.verb_action` is covered by any scope
144    /// in this principal's scope list. Scope strings support exact match
145    /// (`"shell.exec"`) and namespace wildcards (`"fs.*"`).
146    pub fn has_scope(&self, verb_ns: &str, verb_action: &str) -> bool {
147        let target = format!("{verb_ns}.{verb_action}");
148        for scope in &self.scopes {
149            if scope == &target {
150                return true;
151            }
152            // Namespace wildcard: "fs.*" matches "fs.read", "fs.write", etc.
153            if let Some(prefix) = scope.strip_suffix(".*") {
154                if verb_ns == prefix {
155                    return true;
156                }
157            }
158            // Global wildcard: "*" matches everything.
159            if scope == "*" {
160                return true;
161            }
162        }
163        false
164    }
165}
166
167/// How a [`ModifierConstraint`] compares an allow-list entry against the
168/// actual modifier value pulled from an [`AuthorizationRequest`].
169#[derive(Clone, Copy, Debug, Default, Serialize, Deserialize, PartialEq, Eq)]
170#[serde(rename_all = "snake_case")]
171pub enum MatchKind {
172    /// Value must equal an allow entry exactly. The default — the strictest
173    /// and the only safe choice for opaque identifiers (server names, ids).
174    #[default]
175    Exact,
176    /// Value must start with an allow entry. For path-like or prefix-shaped
177    /// modifiers. (The built-in `path_allowlist` uses a stricter
178    /// segment-boundary prefix; this is the plain `starts_with` form.)
179    Prefix,
180    /// Host-suffix match (case-insensitive): an entry `example.com` permits
181    /// `example.com` and any `*.example.com` subdomain. A leading `*.` on the
182    /// entry is accepted and ignored, so `*.example.com` behaves identically.
183    HostSuffix,
184}
185
186/// A per-principal constraint on one modifier of one verb (or verb namespace).
187///
188/// This is the general form of the older `path_allowlist`: that list is the
189/// built-in path constraint; `constraints` lets a principal scope *any*
190/// modifier — `net.http` `host`, `shell.exec` `command`, `mcp.mount` `name`,
191/// and so on. It is the enforcement substrate for capability-scoped Skill
192/// Packs: a pack granted `net.http` to `api.github.com` cannot reach
193/// `evil.com`, enforced at signal-entry rather than at execution.
194///
195/// Semantics (fail-closed): when a principal carries a constraint whose
196/// [`Self::applies_to`] matches the request's verb, the named `modifier` MUST
197/// be present in the request and its value MUST be [`Self::permits`]ted —
198/// otherwise the check denies. An empty `allow` list denies everything for
199/// that `(verb, modifier)` pair.
200#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
201pub struct ModifierConstraint {
202    /// Verb this governs: an exact `"net.http"`, a namespace wildcard
203    /// `"net.*"`, or the global `"*"`.
204    pub verb: String,
205    /// Modifier key read from the request (e.g. `"host"`, `"command"`).
206    pub modifier: String,
207    #[serde(default)]
208    pub match_kind: MatchKind,
209    /// Permitted values. Empty = deny everything for this `(verb, modifier)`.
210    #[serde(default)]
211    pub allow: Vec<String>,
212}
213
214impl ModifierConstraint {
215    /// Does this constraint govern `verb_ns.verb_action`? Supports exact
216    /// match, a `"ns.*"` namespace wildcard, and the global `"*"`.
217    pub fn applies_to(&self, verb_ns: &str, verb_action: &str) -> bool {
218        if self.verb == "*" {
219            return true;
220        }
221        if let Some(prefix) = self.verb.strip_suffix(".*") {
222            return verb_ns == prefix;
223        }
224        let mut target = String::with_capacity(verb_ns.len() + 1 + verb_action.len());
225        target.push_str(verb_ns);
226        target.push('.');
227        target.push_str(verb_action);
228        self.verb == target
229    }
230
231    /// Is `value` permitted by this constraint's allow-list under its
232    /// [`MatchKind`]? An empty allow-list permits nothing.
233    pub fn permits(&self, value: &str) -> bool {
234        self.allow.iter().any(|entry| match self.match_kind {
235            MatchKind::Exact => entry == value,
236            MatchKind::Prefix => value.starts_with(entry.as_str()),
237            MatchKind::HostSuffix => host_suffix_match(entry, value),
238        })
239    }
240}
241
242/// `entry` permits `value` when `value` is the host itself or a subdomain of
243/// it. A leading `*.` on the entry is stripped first so `example.com` and
244/// `*.example.com` behave identically. Case-insensitive.
245fn host_suffix_match(entry: &str, value: &str) -> bool {
246    let base = entry.trim_start_matches("*.").to_ascii_lowercase();
247    if base.is_empty() {
248        return false;
249    }
250    let value = value.to_ascii_lowercase();
251    value == base || value.ends_with(&format!(".{base}"))
252}
253
254/// Identifier the adapter passes when resolving a principal from auth context.
255#[derive(Clone, Debug, PartialEq, Eq)]
256pub enum AgentHint {
257    /// API-key-style identification (HTTP / WS / gRPC).
258    AgentId(AgentId),
259    /// Unknown caller — the store decides whether to materialise a default
260    /// or refuse.
261    Anonymous,
262}
263
264/// Authorization context for `IdentityStore::check`. Carries the verb plus
265/// a free-form `modifiers` JSON object so scope checks can read fields like
266/// `path` / `cwd`. The intent-routing `IntentToken` carries the same fields
267/// and reduces to this struct at the call site.
268#[derive(Clone, Debug)]
269pub struct AuthorizationRequest {
270    pub verb_ns: String,
271    pub verb_action: String,
272    pub modifiers: serde_json::Value,
273}
274
275impl AuthorizationRequest {
276    pub fn new(verb_ns: impl Into<String>, verb_action: impl Into<String>) -> Self {
277        Self {
278            verb_ns: verb_ns.into(),
279            verb_action: verb_action.into(),
280            modifiers: serde_json::Value::Null,
281        }
282    }
283
284    pub fn with_modifiers(mut self, modifiers: serde_json::Value) -> Self {
285        self.modifiers = modifiers;
286        self
287    }
288
289    /// Read a string from `modifiers[key]`; returns `None` if absent or
290    /// not a string. Used by path-scope check paths.
291    pub fn modifier_str(&self, key: &str) -> Option<&str> {
292        self.modifiers.get(key)?.as_str()
293    }
294}
295
296/// Result of an authorization check.
297///
298/// `EscalateToUser` is the default stance: missing scope is never a silent
299/// fail. The `ConfirmationEngine` shows the user a prompt with the carried
300/// reason; the user can approve once, grant a standing approval, or reject.
301#[derive(Clone, Debug, PartialEq, Eq)]
302pub enum CheckOutcome {
303    Allow,
304    EscalateToUser { reason: String },
305    Deny { reason: String },
306}
307
308#[derive(Debug, Error)]
309pub enum IdentityError {
310    #[error("unknown agent: {0}")]
311    UnknownAgent(String),
312    #[error("config error: {0}")]
313    Config(String),
314    #[error("io: {0}")]
315    Io(#[from] std::io::Error),
316    #[error("yaml: {0}")]
317    Yaml(#[from] serde_yaml::Error),
318}
319
320/// Async trait every adapter holds an `Arc<dyn IdentityStore>` to. The
321/// default implementation is [`crate::ConfigIdentityStore`]; production
322/// deployments can wrap it with caching, rate limiting, or signed-token
323/// validators without changing the trait.
324#[async_trait]
325pub trait IdentityStore: Send + Sync {
326    /// Resolve a `Principal` from an adapter-supplied hint. Returns
327    /// `Err(UnknownAgent)` if the hint cannot be mapped — the caller
328    /// decides whether to escalate or refuse.
329    async fn principal_for(&self, agent_hint: &AgentHint) -> Result<Principal, IdentityError>;
330
331    /// Authorize an action. The `required` tier names the minimum tier the
332    /// principal must hold *and* the verb in `req` must be covered by one
333    /// of `p.scopes`. Path-scope checks read `req.modifier_str("path")` /
334    /// `req.modifier_str("cwd")`.
335    async fn check(
336        &self,
337        p: &Principal,
338        req: &AuthorizationRequest,
339        required: Tier,
340    ) -> CheckOutcome;
341}
342
343#[cfg(test)]
344mod tests {
345    use super::*;
346
347    #[test]
348    fn tier_is_strictly_ordered() {
349        assert!(Tier::Read < Tier::Write);
350        assert!(Tier::Write < Tier::Execute);
351        assert!(Tier::Execute < Tier::Destructive);
352        assert!(Tier::Destructive < Tier::External);
353    }
354
355    #[test]
356    fn tier_satisfies_via_ge() {
357        // An Execute-tier principal satisfies a Write requirement.
358        assert!(Tier::Execute >= Tier::Write);
359        // A Read-tier principal does NOT satisfy Execute.
360        assert!(Tier::Read < Tier::Execute);
361    }
362
363    #[test]
364    fn requires_confirmation_only_destructive_external() {
365        assert!(!Tier::Read.requires_confirmation());
366        assert!(!Tier::Write.requires_confirmation());
367        assert!(!Tier::Execute.requires_confirmation());
368        assert!(Tier::Destructive.requires_confirmation());
369        assert!(Tier::External.requires_confirmation());
370    }
371
372    #[test]
373    fn default_timeout_increases_with_tier() {
374        assert!(Tier::Read.default_timeout() < Tier::Execute.default_timeout());
375        assert!(Tier::Execute.default_timeout() < Tier::Destructive.default_timeout());
376    }
377
378    #[test]
379    fn external_timeout_is_shorter_than_destructive() {
380        // External lives in chat; a 5-min deadlock there feels broken.
381        assert!(Tier::External.default_timeout() < Tier::Destructive.default_timeout());
382    }
383
384    #[test]
385    fn display_matches_serde_repr() {
386        assert_eq!(Tier::Destructive.to_string(), "destructive");
387        let json = serde_json::to_string(&Tier::Destructive).unwrap();
388        assert_eq!(json, "\"destructive\"");
389    }
390
391    #[test]
392    fn has_scope_exact_match() {
393        let p = Principal {
394            user_id: "k".into(),
395            agent_id: "claude-code".into(),
396            scopes: vec!["shell.exec".into()],
397            tier: Tier::Execute,
398        };
399        assert!(p.has_scope("shell", "exec"));
400        assert!(!p.has_scope("shell", "kill"));
401        assert!(!p.has_scope("fs", "read"));
402    }
403
404    #[test]
405    fn has_scope_namespace_wildcard() {
406        let p = Principal {
407            user_id: "k".into(),
408            agent_id: "claude-code".into(),
409            scopes: vec!["fs.*".into()],
410            tier: Tier::Write,
411        };
412        assert!(p.has_scope("fs", "read"));
413        assert!(p.has_scope("fs", "write"));
414        assert!(!p.has_scope("shell", "exec"));
415    }
416
417    #[test]
418    fn has_scope_global_wildcard() {
419        let p = Principal {
420            user_id: "k".into(),
421            agent_id: "root".into(),
422            scopes: vec!["*".into()],
423            tier: Tier::External,
424        };
425        assert!(p.has_scope("shell", "exec"));
426        assert!(p.has_scope("fs", "read"));
427        assert!(p.has_scope("net", "http"));
428    }
429
430    #[test]
431    fn auth_request_modifier_str_reads_paths() {
432        let req = AuthorizationRequest::new("fs", "read")
433            .with_modifiers(serde_json::json!({ "path": "/tmp/x", "limit": 10 }));
434        assert_eq!(req.modifier_str("path"), Some("/tmp/x"));
435        assert_eq!(req.modifier_str("limit"), None); // number, not string
436        assert_eq!(req.modifier_str("missing"), None);
437    }
438
439    fn constraint(
440        verb: &str,
441        modifier: &str,
442        match_kind: MatchKind,
443        allow: &[&str],
444    ) -> ModifierConstraint {
445        ModifierConstraint {
446            verb: verb.into(),
447            modifier: modifier.into(),
448            match_kind,
449            allow: allow.iter().map(|s| s.to_string()).collect(),
450        }
451    }
452
453    #[test]
454    fn constraint_applies_to_exact_namespace_and_global() {
455        let exact = constraint("net.http", "host", MatchKind::HostSuffix, &[]);
456        assert!(exact.applies_to("net", "http"));
457        assert!(!exact.applies_to("net", "connect"));
458        assert!(!exact.applies_to("fs", "read"));
459
460        let ns = constraint("net.*", "host", MatchKind::HostSuffix, &[]);
461        assert!(ns.applies_to("net", "http"));
462        assert!(ns.applies_to("net", "connect"));
463        assert!(!ns.applies_to("fs", "read"));
464
465        let global = constraint("*", "host", MatchKind::HostSuffix, &[]);
466        assert!(global.applies_to("anything", "at-all"));
467    }
468
469    #[test]
470    fn constraint_exact_match() {
471        let c = constraint(
472            "mcp.mount",
473            "name",
474            MatchKind::Exact,
475            &["github", "filesystem"],
476        );
477        assert!(c.permits("github"));
478        assert!(!c.permits("git")); // not a prefix match
479        assert!(!c.permits("evil"));
480    }
481
482    #[test]
483    fn constraint_prefix_match() {
484        let c = constraint(
485            "shell.exec",
486            "command",
487            MatchKind::Prefix,
488            &["git ", "cargo "],
489        );
490        assert!(c.permits("git status"));
491        assert!(c.permits("cargo build"));
492        assert!(!c.permits("rm -rf /"));
493    }
494
495    #[test]
496    fn constraint_host_suffix_match() {
497        let c = constraint(
498            "net.http",
499            "host",
500            MatchKind::HostSuffix,
501            &["github.com", "*.internal.example"],
502        );
503        assert!(c.permits("github.com")); // bare host
504        assert!(c.permits("api.github.com")); // subdomain
505        assert!(c.permits("svc.internal.example")); // leading *. on entry ignored
506        assert!(c.permits("API.GitHub.com")); // case-insensitive
507        assert!(!c.permits("github.com.evil.com")); // suffix-boundary respected
508        assert!(!c.permits("evil.com"));
509    }
510
511    #[test]
512    fn constraint_empty_allow_denies_everything() {
513        let c = constraint("net.http", "host", MatchKind::HostSuffix, &[]);
514        assert!(!c.permits("github.com"));
515        assert!(!c.permits(""));
516    }
517
518    // ── Property tests ────────────────────────────────────────────────
519    //
520    // Scope and host matching are access-control predicates: a prefix
521    // confusion (e.g. "fs.*" matching "fsx.read", or host entry
522    // "example.com" matching "evilexample.com") is a privilege escalation.
523    // These assert the boundary holds for arbitrary names.
524
525    use proptest::prelude::*;
526
527    fn principal_with(scopes: Vec<String>) -> Principal {
528        Principal {
529            user_id: "u".into(),
530            agent_id: "a".into(),
531            scopes,
532            tier: Tier::Execute,
533        }
534    }
535
536    proptest! {
537        #![proptest_config(ProptestConfig { cases: 512, .. ProptestConfig::default() })]
538
539        /// The global "*" scope covers every verb.
540        #[test]
541        fn global_scope_covers_everything(ns in "[a-z]{1,8}", action in "[a-z]{1,8}") {
542            prop_assert!(principal_with(vec!["*".into()]).has_scope(&ns, &action));
543        }
544
545        /// A namespace wildcard "X.*" covers a verb iff its namespace is
546        /// exactly X — never a namespace that merely shares a prefix
547        /// ("fs.*" must not cover "fsx.read").
548        #[test]
549        fn namespace_wildcard_matches_only_its_namespace(
550            scope_ns in "[a-z]{1,8}",
551            ns in "[a-z]{1,8}",
552            action in "[a-z]{1,8}",
553        ) {
554            let p = principal_with(vec![format!("{scope_ns}.*")]);
555            prop_assert_eq!(p.has_scope(&ns, &action), ns == scope_ns);
556        }
557
558        /// An exact scope "a.b" covers a verb iff both parts match exactly.
559        #[test]
560        fn exact_scope_matches_only_exact_verb(
561            sn in "[a-z]{1,8}", sa in "[a-z]{1,8}",
562            ns in "[a-z]{1,8}", action in "[a-z]{1,8}",
563        ) {
564            let p = principal_with(vec![format!("{sn}.{sa}")]);
565            prop_assert_eq!(p.has_scope(&ns, &action), ns == sn && action == sa);
566        }
567
568        /// `applies_to` shares the wildcard semantics: "X.*" governs a verb
569        /// iff its namespace is exactly X (same prefix-confusion guard).
570        #[test]
571        fn constraint_namespace_wildcard_is_exact(
572            verb_ns in "[a-z]{1,8}",
573            ns in "[a-z]{1,8}",
574            action in "[a-z]{1,8}",
575        ) {
576            let c = constraint(&format!("{verb_ns}.*"), "host", MatchKind::Exact, &[]);
577            prop_assert_eq!(c.applies_to(&ns, &action), ns == verb_ns);
578        }
579
580        /// Host-suffix matching: an entry permits the exact host and any
581        /// subdomain, but never a sibling that only shares a leading
582        /// substring without a label boundary ("example.com" must reject
583        /// "xexample.com"). Case-insensitive. The "*." prefix is a no-op.
584        #[test]
585        fn host_suffix_respects_label_boundary(
586            base in "[a-z]{1,6}\\.[a-z]{2,4}",
587            label in "[a-z]{1,5}",
588        ) {
589            let c = constraint("net.http", "host", MatchKind::HostSuffix, &[&base]);
590            let subdomain = format!("{label}.{base}");
591            let sibling = format!("{label}{base}"); // no label boundary
592            let upper = base.to_uppercase();
593
594            // Exact host and a real subdomain are permitted.
595            prop_assert!(c.permits(&base));
596            prop_assert!(c.permits(&subdomain));
597            // Case-insensitive on the value.
598            prop_assert!(c.permits(&upper));
599            // A sibling with no label boundary is rejected.
600            prop_assert!(!c.permits(&sibling));
601
602            // A "*.base" entry behaves identically to "base".
603            let starred_entry = format!("*.{base}");
604            let starred = constraint("net.http", "host", MatchKind::HostSuffix, &[&starred_entry]);
605            for v in [base.clone(), subdomain.clone(), sibling.clone()] {
606                prop_assert_eq!(c.permits(&v), starred.permits(&v));
607            }
608        }
609    }
610
611    // ── Tier authorization & confirmation-gate properties ─────────────
612    //
613    // `Tier` is the spine of the security model: authorization is the single
614    // comparison `principal.tier >= action.tier`, and the confirm engine
615    // gates on `requires_confirmation()`. Two failure modes matter — a
616    // *reorder* of the enum silently rewires every `>=` check, and a *gap*
617    // (a dangerous tier that skips confirmation while a milder one requires
618    // it) would let an irreversible action through unprompted. These pin the
619    // ladder and prove the gate is the monotone `>= Destructive` cut.
620
621    fn any_tier() -> impl Strategy<Value = Tier> {
622        prop_oneof![
623            Just(Tier::Read),
624            Just(Tier::Write),
625            Just(Tier::Execute),
626            Just(Tier::Destructive),
627            Just(Tier::External),
628        ]
629    }
630
631    /// The derived `Ord` follows declaration order; this is the canonical
632    /// ladder every `principal >= action` check depends on. A reorder of the
633    /// enum variants would silently change authorization semantics — this
634    /// turns that into a test failure.
635    #[test]
636    fn tier_ladder_is_canonical() {
637        let mut all = [
638            Tier::External,
639            Tier::Read,
640            Tier::Destructive,
641            Tier::Write,
642            Tier::Execute,
643        ];
644        all.sort();
645        assert_eq!(
646            all,
647            [
648                Tier::Read,
649                Tier::Write,
650                Tier::Execute,
651                Tier::Destructive,
652                Tier::External,
653            ]
654        );
655    }
656
657    proptest! {
658        #![proptest_config(ProptestConfig { cases: 256, .. ProptestConfig::default() })]
659
660        /// The confirmation gate is exactly the `>= Destructive` cut:
661        /// Read/Write/Execute auto-approve, Destructive/External block. This
662        /// ties the predicate to the ordering so the two can't drift apart.
663        #[test]
664        fn confirmation_gate_is_the_destructive_cut(t in any_tier()) {
665            prop_assert_eq!(t.requires_confirmation(), t >= Tier::Destructive);
666        }
667
668        /// Requiring confirmation is upward-closed: if a tier needs a human,
669        /// every higher (more dangerous) tier does too. No gap where a
670        /// stronger action skips the gate a weaker one is held to.
671        #[test]
672        fn confirmation_requirement_is_upward_closed(a in any_tier(), b in any_tier()) {
673            let (lo, hi) = if a <= b { (a, b) } else { (b, a) };
674            if lo.requires_confirmation() {
675                prop_assert!(hi.requires_confirmation());
676            }
677        }
678
679        /// Authorization (`principal >= required`) is upward-closed in the
680        /// principal: raising a principal's tier never revokes access it
681        /// already had to a given required tier.
682        #[test]
683        fn authorization_is_upward_closed(
684            required in any_tier(),
685            p in any_tier(),
686            q in any_tier(),
687        ) {
688            let (lo, hi) = if p <= q { (p, q) } else { (q, p) };
689            if lo >= required {
690                prop_assert!(hi >= required);
691            }
692        }
693
694        /// A principal satisfies a required tier iff the requirement sits at
695        /// or below it — the whole authorization rule in one line.
696        #[test]
697        fn principal_satisfies_iff_required_at_or_below(
698            principal in any_tier(),
699            required in any_tier(),
700        ) {
701            prop_assert_eq!(principal >= required, required <= principal);
702        }
703
704        /// Every tier carries a positive, humane default timeout (no zero or
705        /// runaway deadline). Deliberately not monotone — External is shorter
706        /// than Destructive by design — so this asserts bounds, not ordering.
707        #[test]
708        fn default_timeout_is_positive_and_bounded(t in any_tier()) {
709            let secs = t.default_timeout().as_secs();
710            prop_assert!((1..=300).contains(&secs));
711        }
712    }
713}