Skip to main content

Module mode

Module mode 

Source
Expand description

Run modes and admission. A run sits in exactly one mode; the catalog lists only that one (progressive disclosure — the other mode’s text stays out of the window).

One exception, and it is one line long: dev_entry tells a run that this city’s own code is changeable, and names the evidence a change can be asked to carry. Without it an agent working in this city never learns that the city’s own code and SPECs are changeable at all, or under what discipline — and a capability nobody is told about is one nobody uses.

The half that decides is admits: it says whether what a run produced may land, given the run policy it was dispatched under (crates/runtime/spec/Mode.lean §8-54). The evidence arrives as plain answers rather than as an instrument’s type, because the instruments live in citysim, outside this crate, and the question here is not how evidence was gathered but whether enough of it exists.

Structs§

PolicyCell
The run policy in force for one run (crates/runtime/spec/PolicyTake.lean §8-62, runtime D28).
PolicyReader
What a write gate reads: the policy in force, never a change that has arrived and not yet been taken.
Produced
What a run has to show for itself.

Enums§

Admission
Whether this may land, and if not, what to do about it.

Constants§

DEV_ENTRY
The name of the catalog row that opens the developer discipline.

Functions§

admits
Whether what a run produced may be merged, under the policy it was dispatched with (crates/runtime/spec/Mode.lean §8-54).
catalog_entry
The catalog row for this mode: disclosure one-liner plus the expansion text. The chat row is the whole of what chat mode does: one line telling the resident that the person is talking with it.
core_tools
The resident tools a run in mode may run (crates/runtime/Spec.lean §8-60). The request carries the union of every mode’s core (in_some_core), and mode_admits refuses at the call a tool the mode in force does not run; every other admitted tool waits in the dormant index. A name here travels only where the building admitted it: the hall registers no exec, so exec is in no tier there.
dev_entry
The row that tells a run this city is changeable, and nothing more.
in_some_core
Whether name travels as a tool in every request of a session: it is in the core of some mode. The tool array is this union in every mode (runtime D25), so a change of mode mid-session leaves its bytes alone; mode_admits is where the mode in force still decides.
mode_admits
The gate a resident tool asks at its call: a tool that some mode carries and the mode in force does not is refused, before it does anything (runtime D25). A tool outside every core is the catalog’s to reach through call, and this gate does not judge it.