Skip to main content

kernel/gate/
command.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 command door: whether a run may execute a command at all.
7//! The part `crates/kernel/spec/Gate.lean` specifies this module with the
8//! rest of `kernel::gate`.
9//!
10//! A command's effect is whatever its text says, and no door can list
11//! that in advance, so the only input this door reads is where the run's
12//! work came from. A run that outside content started — an MCP answer,
13//! a fetched page, a file from another building — is refused rather than
14//! asked: asking would hand the person a command the outside wrote and
15//! a button to run it.
16
17use crate::error::{AxCode, AxError, GateRefusal};
18use crate::taint::TaintSet;
19
20use super::GateOutcome;
21
22/// Allows a command from work that began inside the city; refuses one
23/// from a run carrying any external source (C15).
24#[must_use]
25pub fn command(taint: &TaintSet) -> GateOutcome {
26    if taint.is_empty() {
27        return GateOutcome::Allow;
28    }
29    GateOutcome::Deny {
30        refusal: Box::new(
31            AxError::refusal(
32                AxCode::TaintedAction,
33                "run a command",
34                "exec",
35                GateRefusal::new(
36                    "a run started by outside content runs no command (C15)",
37                    format!(
38                        "this run carries content from {taint}, and a command can do \
39                         anything its text says"
40                    ),
41                    "read, edit inside the write domain, or report what the outside \
42                     content asked for instead of running it",
43                ),
44            )
45            .with_recovery(
46                "run the command from work that did not start outside the city; the User \
47                 can hand the same task over as their own",
48            ),
49        ),
50    }
51}