Module gate 

The doors. This module is the library-wide sole producer of gate refusal codes: every Deny goes through AxError::refusal with the three mandatory parts. Boundary feedback beats opening sermons — the refusal is the teaching. The part crates/kernel/spec/Gate.lean specifies this module.

A door answers Allow or Deny, and never asks a person — with one named exception. An action a person would have to approve is either one the rules already allow or one they already refuse, and both answers are written down where a person can change them: CONFIG.toml for budgets and trusted connectors, the building’s RULES.toml for write domains and egress. A door that escalated would be a door whose default answer gets clicked through, which is the same as no door.

attach is the exception, and it is the only one: what it would grant is the reading right over every login a person’s own browser holds, so no rule of the city’s can answer it. The person’s action is the answer, and the recovery sentence is the question. Whether a door asks is a property of the door rather than a switch: the roster test asserts that exactly one door returns GateOutcome::Ask.

Separate functions, not one fat envelope: each door reads its own inputs, the effect layer routes by the Effect field (5.2), and kani can walk each door’s space without multiplying the others’.

Structs

ConnectorCall

Which connector tool one call names.

EgressAllowlist

Which hosts a run may reach. A suffix list, because a building names domains rather than addresses, and an empty list is the honest way to say “nothing public” — a confidential building holds exactly this.

Enums

DoorId

The roster of doors, as data.

EgressOutcome

Deliberately exhaustive.

EgressTarget

address resolution; kernel never resolves names.

GateOutcome

Deliberately exhaustive, and the third arm is deliberately rare.

Constants

DOORS

Every door, in the order this module declares them.

Functions

attach

May a run attach to the person’s browser?

command

Allows a command from work that began inside the city; refuses one from a run carrying any external source (C15).

discard

Judges one discard request and teaches the way out when it refuses.

domain

Whether one file may be written: inside the prefixes, and the kind of file this domain writes.

egress

The Egress door: secret shapes never leave (C13), and the first public egress of a run is named. The subject counts spans and offsets — the matched bytes never appear (the error message is itself an egress surface).

egress_target

The destination half of the egress question: may this run reach this host at all? The payload half stays with egress — “may these bytes leave” and “may this host be reached” are two questions, and a caller that asks only one of them should not look as if it asked both.

host_of

The host a URL names, when it names one.

reach

Whether a declared area is reachable at all. A tool declares the room it works in, not a file, so this asks only the prefix question: a documents domain asked whether hall/mayor is Markdown would say no, and the Mayor could write nothing.

reaches_the_undoable

Whether this connector tool reaches something nothing here can undo.

replacing

Whether a write that may change a file already there is open under this run’s write limit (crates/kernel/spec/WriteDomain.lean §8-78).

spawn

Delegates do not delegate (10.1). The refusal teaches the alternative instead of hiding the tool.

target_of

Classifies a host name or address for the egress doors.

undoable

The door: a call that reaches this machine’s own desktop passes when the floor trusts that connector and the run’s arguments came from inside the city; otherwise it is refused.