Module config 

Three-layer config resolution, specified by crates/kernel/spec/Config.lean. FrozenConfig and LiveConfig share no field; tests check this property.

Structs

ClockZone

One concern timezone: an already-resolved offset, never a tz name — re-resolving names against a moving tz database would fork replayed history.

ContainerImage

A locally installed image ID. Registry references and mutable tags cannot reach an execution request through this type.

ContainerLimits

Every limit is explicit and nonzero. CPU is in millicpu, memory is in bytes, and the process count bounds descendants as well as PID 1.

EnvVarName

One environment variable name a scope declares its runs may inherit.

FrozenConfig

Frozen at Run start, never re-read within the Run. Fields only grow.

LayeredValue

One value across the City -> Building -> Resident override ladder. Lower layers win; absence falls through upward.

LiveConfig

Hot-reloadable surface. Empty: the type exists so the no-field-overlap assertion guards every field added to it.

McpServer

One external tool server this run may reach, as its configuration states it: a label, a program on this machine, and that program’s arguments.

SandboxLimits

What a run’s execution boundary allows. Resolved as one value rather than field by field: a layer that speaks about the sandbox speaks about all of it, so an under-specified layer can only ever reduce what a run may do, never silently grant something the layer above it never mentioned.

SearchSupplier

One search service reached over MCP streamable HTTP.

SecondThreshold

Where the context reminder’s second rung sits: a whole percent of the window, 31 through 90 (the three numbers live in consts_policy).

StatedConfig

Every concern’s ladder, handed to freeze together: the values always travel from the configuration reader to the freeze as one, so a concern added later is a field here and freeze keeps its signature.

Enums

ClockStampGranularity

Clock-stamp cadence for result envelopes. The granularity rides the enum; Off costs zero bytes in the window.

Interpreter

Which interpreter a building’s shell lines run under (crates/kernel/spec/Config.lean §8-22, crates/runtime/Spec.lean §8-13-2 D30).

McpTransport

How this city reaches one server. Exhaustive rather than a URL that might also be a command: the three are different machines to start talking to, they fail differently, and a configuration that leaves it to be guessed is one that guesses wrong on the day it matters.

SandboxArm

One sandbox mechanism family, shared by configuration and doctor reports.

SearchConfiguration

What a layer says about web search. Three arms and no enabled switch, so each of the three intents has one spelling: the default supplier, this supplier, none. Default is a stated value, not an absence: a layer that states it covers a farther layer’s Custom.

Functions

freeze

Resolves the ladder into the Run-start snapshot. Absence everywhere falls back to the policy default; the zones ladder overrides as a whole list (a building that writes zones replaces the city list).