kernel/
gate.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//! The doors. This module is the library-wide sole producer of gate
7//! refusal codes: every Deny goes through `AxError::refusal` with the
8//! three mandatory parts. Boundary feedback beats opening sermons — the
9//! refusal is the teaching.
10//! The part `crates/kernel/spec/Gate.lean` specifies this module.
11//!
12//! **A door answers Allow or Deny, and never asks a person** — with one
13//! named exception. An action a person would have to approve is either
14//! one the rules already allow or one they already refuse, and both
15//! answers are written down where a person can change them: `CONFIG.toml`
16//! for budgets and trusted connectors, the building's `RULES.toml` for
17//! write domains and egress. A door that escalated would be a door whose
18//! default answer gets clicked through, which is the same as no door.
19//!
20//! [`attach`] is the exception, and it is the only one: what it would
21//! grant is the reading right over every login a person's own browser
22//! holds, so no rule of the city's can answer it. The person's action is
23//! the answer, and the recovery sentence is the question. Whether a door
24//! asks is a property of the door rather than a switch: the roster test
25//! asserts that exactly one door returns [`GateOutcome::Ask`].
26//!
27//! Separate functions, not one fat envelope: each door reads its own
28//! inputs, the effect layer routes by the `Effect` field (5.2), and
29//! kani can walk each door's space without multiplying the others'.
30
31use crate::error::AxError;
32
33mod attach;
34mod command;
35mod discard;
36mod domain;
37mod egress;
38mod spawn;
39mod undoable;
40
41pub use attach::attach;
42pub use command::command;
43pub use discard::discard;
44pub use domain::{domain, reach, replacing};
45pub use egress::{
46    EgressAllowlist, EgressOutcome, EgressTarget, egress, egress_target, host_of, target_of,
47};
48pub use spawn::spawn;
49pub use undoable::{ConnectorCall, reaches_the_undoable, undoable};
50
51/// Deliberately exhaustive, and the third arm is deliberately rare.
52///
53/// Every caller decides all three ways, so a door that starts asking a
54/// person is a compile error at every caller rather than a behaviour
55/// that changes underneath them. Exactly one door answers `Ask`
56/// ([`attach`]); the refusal matrix asserts that count.
57#[derive(Debug)]
58pub enum GateOutcome {
59    Allow,
60    Deny {
61        refusal: Box<AxError>,
62    },
63    /// The door cannot answer, and the person can. The error carries
64    /// the question: `E_APPROVAL_PENDING`, the three gate parts, and a
65    /// recovery sentence naming the action only the person can take.
66    Ask {
67        question: Box<AxError>,
68    },
69}
70
71/// The roster of doors, as data.
72///
73/// The refusal conformance matrix walks [`DOORS`] rather than naming
74/// doors one by one, so a door added to this enum is a door the matrix
75/// judges: [`conformance::sample`] matches exhaustively, and a new
76/// arm without a sample does not compile.
77#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
78pub enum DoorId {
79    /// [`domain`] — may this file be written.
80    Domain,
81    /// [`reach`] — may this area be worked in at all.
82    Reach,
83    /// [`egress`] — may these bytes leave.
84    Egress,
85    /// [`egress_target`] — may this host be reached.
86    EgressHost,
87    /// [`discard`] — may these files go.
88    Discard,
89    /// [`spawn`] — may this position hand work down.
90    Spawn,
91    /// [`undoable`] — may this connector reach what nothing here can
92    /// take back.
93    Undoable,
94    /// [`attach`] — may a run drive the browser a person is already
95    /// using, with that person's logins.
96    Attach,
97    /// [`command`] — may this run start a process.
98    Command,
99    /// [`replacing`] — may this write change a file that is already
100    /// there.
101    Replacing,
102}
103
104/// Every door, in the order this module declares them.
105pub const DOORS: [DoorId; 10] = [
106    DoorId::Domain,
107    DoorId::Reach,
108    DoorId::Egress,
109    DoorId::EgressHost,
110    DoorId::Discard,
111    DoorId::Spawn,
112    DoorId::Undoable,
113    DoorId::Attach,
114    DoorId::Command,
115    DoorId::Replacing,
116];
117
118impl DoorId {
119    /// The door's name in a refusal report, which is the name of the
120    /// function that produced it.
121    #[must_use]
122    pub fn as_str(self) -> &'static str {
123        match self {
124            DoorId::Domain => "domain",
125            DoorId::Reach => "reach",
126            DoorId::Egress => "egress",
127            DoorId::EgressHost => "egress_target",
128            DoorId::Discard => "discard",
129            DoorId::Spawn => "spawn",
130            DoorId::Undoable => "undoable",
131            DoorId::Attach => "attach",
132            DoorId::Command => "command",
133            DoorId::Replacing => "replacing",
134        }
135    }
136}
137
138#[cfg(feature = "conformance")]
139pub mod conformance;
140
141#[cfg(all(test, feature = "conformance"))]
142#[allow(
143    clippy::unwrap_used,
144    clippy::expect_used,
145    clippy::panic,
146    reason = "test code"
147)]
148mod tests;
kernel/gate.rs

kernel/
gate.rs
