Expand description
Three-layer config resolution and the frozen/live split. FrozenConfig and LiveConfig share no field: the freeze
line is a machine-checkable property, not a review note.
The part crates/kernel/spec/Config.lean specifies this module.
Structs§
- Clock
Zone - One concern timezone: an already-resolved offset, never a tz name — re-resolving names against a moving tz database would fork replayed history.
- EnvVar
Name - One environment variable name a scope declares its runs may inherit.
- Frozen
Config - Frozen at Run start, never re-read within the Run. Fields only grow.
- Layered
Value - One value across the City -> Building -> Resident override ladder. Lower layers win; absence falls through upward.
- Live
Config - 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.
- Sandbox
Limits - 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.
- Second
Threshold - Where the context reminder’s second rung sits: a whole percent of the
window,
31through90(the three numbers live inconsts_policy).
Enums§
- Clock
Stamp Granularity - Clock-stamp cadence for result envelopes. The
granularity rides the enum;
Offcosts 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.
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).