Crate kernel 

Pure decision functions: values in, verdicts out. Zero internal deps. Holds no I/O handles, no clock, no global state (ARCHITECTURE.md paragraph 1). The entry crates/kernel/Spec.lean specifies this crate, and each module names the part under crates/kernel/spec/ that specifies it.

This file is an index, and the modules are the library. Every module is public and a caller reaches a decision through the module that owns it — gate::domain, discard::decide, approval::may_answer — so the module name says which authority answered. What the root re-exports is the vocabulary those signatures are written in: the value types a caller names in its own fields and arguments. A function is never re-exported here, and nothing is renamed on the way out, because a second spelling of one name is the defect xtask lexicon exists to catch.

Re-exports

pub use address::Address;

pub use address::GIT_METADATA;

pub use address::PROTECTED_METADATA;

pub use address::RESERVED_PREFIX;

pub use address::ReadVerdict;

pub use address::SessionName;

pub use approval::AnswerVerdict;

pub use approval::Answerer;

pub use approval::ApprovalClass;

pub use approval::ApprovalId;

pub use approval::ApprovalItem;

pub use approval::Autonomy;

pub use approval::ClusterKey;

pub use approval::Ruling;

pub use backpressure::Admission;

pub use backpressure::ItemMeta;

pub use backpressure::QueueStats;

pub use backpressure::ShedReason;

pub use blockage::Blockage;

pub use blockage::Notice;

pub use blockage::RedNode;

pub use budget::BudgetUse;

pub use budget::ByteLen;

pub use budget::Tokens;

pub use budget::UsdMicros;

pub use change::FileChange;

pub use change::How;

pub use change::Lines;

pub use completion::Completion;

pub use completion::Evidence;

pub use completion::PlannedProgress;

pub use completion::Progress;

pub use completion::UnplannedProgress;

pub use config::ClockStampGranularity;

pub use config::ClockZone;

pub use config::FrozenConfig;

pub use config::ContainerImage;

pub use config::ContainerLimits;

pub use config::EnvVarName;

pub use config::Interpreter;

pub use config::LayeredValue;

pub use config::LiveConfig;

pub use config::SandboxArm;

pub use config::SandboxLimits;

pub use config::McpServer;

pub use config::McpTransport;

pub use config::SecondThreshold;

pub use delegation::Delegate;

pub use delegation::DelegateKind;

pub use delegation::DelegationVerdict;

pub use delegation::Delegator;

pub use delegation::Depth;

pub use discard::Restoration;

pub use discard::DenyReason;

pub use discard::Discard;

pub use discard::DiscardForecast;

pub use discard::DiscardRequest;

pub use discard::DiscardVerdict;

pub use error::AccountDisposition;

pub use error::AxCode;

pub use error::AxError;

pub use error::Carrier;

pub use error::ErrorDraft;

pub use error::GateRefusal;

pub use error::ProviderFailureKind;

pub use error::Retry;

pub use event::record::InputKinds;

pub use event::EventDraft;

pub use event::EventKind;

pub use event::EventRecord;

pub use event::EventRef;

pub use event::Payload;

pub use event::RunId;

pub use event::Seq;

pub use event::TimeMs;

pub use event::WindowClass;

pub use gate::GateOutcome;

pub use gate::ConnectorCall;

pub use gate::DOORS;

pub use gate::DoorId;

pub use gate::EgressAllowlist;

pub use gate::EgressOutcome;

pub use gate::EgressTarget;

pub use goal::GoalEntry;

pub use goal::GoalId;

pub use goal::GoalResource;

pub use goal::GoalVerdict;

pub use idem::Duplicate;

pub use idem::IDEM_DERIVE_V;

pub use idem::IdemGuard;

pub use idem::IdemKey;

pub use keep_warm::KeepWarm;

pub use ledger::GENESIS_PREV;

pub use ledger::Ledger;

pub use locator::B3Hash;

pub use locator::GitOid;

pub use locator::Locator;

pub use locator::Range;

pub use model::AdmissionRequirement;

pub use model::LandingPolicy;

pub use model::Mode;

pub use model::RunPolicy;

pub use model::Window;

pub use model::BuildingPolicy;

pub use model::Ceiling;

pub use model::ChatMessage;

pub use model::ChatRequest;

pub use model::ChatResponse;

pub use model::ContentBlock;

pub use model::CacheCount;

pub use model::ModelRequest;

pub use model::ModelReturn;

pub use model::ModelTag;

pub use model::ModelUsage;

pub use model::Role;

pub use model::StopReason;

pub use model::DialectKind;

pub use model::EarlyCalls;

pub use model::Effort;

pub use model::ImageRef;

pub use model::ImageType;

pub use model::Increment;

pub use model::Increments;

pub use model::MessageBreakpoint;

pub use model::Model;

pub use model::SharedPrefix;

pub use model::SystemBlock;

pub use model::ToolDef;

pub use node_id::NODE_DEPTH_MAX;

pub use node_id::NodeId;

pub use plan::Held;

pub use plan::PlanExit;

pub use plan::PlanNode;

pub use plan::PlanTree;

pub use plan::StopCause;

pub use pursuit::Pursuit;

pub use pursuit::PursuitState;

pub use pursuit::PursuitVerdict;

pub use reach::Answered;

pub use reach::Connected;

pub use reach::Named;

pub use reach::Proxying;

pub use reach::Reach;

pub use reach::Through;

pub use registry::Artifact;

pub use registry::Claim;

pub use registry::RegisterVerdict;

pub use registry::Registry;

pub use registry::ResidentId;

pub use release::Maturity;

pub use release::Release;

pub use release::ReleaseVerdict;

pub use repair::RepairVerdict;

pub use retries::Retries;

pub use secret::Sealed;

pub use secret::SecretRef;

pub use secret::SecretSpan;

pub use share::Share;

pub use share::WHOLE_PPB;

pub use spine::EvidenceCell;

pub use spine::NewChild;

pub use spine::ROADMAP_COLUMNS;

pub use spine::ROADMAP_FILE;

pub use spine::ROADMAP_STATUS_SPELLINGS;

pub use spine::RoadmapRow;

pub use spine::RoadmapShape;

pub use spine::RoadmapStatus;

pub use spine::ScopeChange;

pub use spine::WriteMoment;

pub use stall::ActionFingerprint;

pub use stall::StallVerdict;

pub use taint::TaintSet;

pub use taint::TaintSource;

pub use taint::Tainted;

pub use tool::writes::Writes;

pub use tool::CostTier;

pub use tool::Effect;

pub use tool::ExecArm;

pub use tool::GateSubject;

pub use tool::RenderIntent;

pub use tool::ServerLabel;

pub use tool::Temporal;

pub use tool::TimeoutMs;

pub use tool::Tool;

pub use tool::ToolCall;

pub use tool::ToolMeta;

pub use tool::ToolName;

pub use tool::ToolOutcome;

pub use version::Version;

pub use version::VersionVerdict;

pub use write_domain::DocumentReason;

pub use write_domain::DomainPrefixes;

pub use write_domain::DomainVerdict;

pub use write_domain::EditSample;

pub use write_domain::EditWarVerdict;

pub use write_domain::WriteDomain;

pub use write_domain::WriteLimit;

Modules

account_recovery

Which account of a provider a request goes out on, and after a failure whether it goes out again on the same account, moves to another, or stops. The part crates/kernel/spec/AccountRecovery.lean specifies this module (crates/kernel/Spec.lean §8-86, kernel D54 and D55).

address

Address: canonical relative path inside a city, and the WriteDomain primitive is_within. The part crates/kernel/spec/Address.lean specifies this module.

approval

The Approval Inbox holds design questions and nothing else (9.2). The part crates/kernel/spec/Approval.lean specifies this module.

backpressure

Admission control: the city-wide shedding posture. One function serves every queue-shaped resource — signal queues and fd headroom alike; capacity semantics belong to the caller. Queues and counters live in storage::queue, never here. The part crates/kernel/spec/Backpressure.lean specifies this module.

blockage

Red, and how far it reaches. The part crates/kernel/spec/Blockage.lean specifies this module.

budget

Money and quantities as integers (15.3-6), and what a piece of work turned out to cost. The part crates/kernel/spec/Budget.lean specifies this module.

change

What moved between two checkpoints, as a fact rather than as a patch. The part crates/kernel/spec/Change.lean specifies this module.

completion

Completion and progress. Claiming done makes nothing done: Completion::Done cannot be built without evidence the city recorded itself (the runtime checks depth). Progress is honest in the type: only a planned run owns a ratio method — an unplanned run has nothing to ask a percentage from. The part crates/kernel/spec/Completion.lean specifies this module.

config

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

consts_external

External-fact constants: values that follow the outside world. Changing one requires evidence that the world changed, never our own preference. The part crates/kernel/spec/ConstsExternal.lean specifies this module.

consts_policy

Policy constants: our choices. Changing one changes behavior and therefore requires EVAL evidence or an explicit ruling. Data only — zero branches by charter. The part crates/kernel/spec/ConstsPolicy.lean specifies this module.

degradation

Degrade truthfully: which resource is the bottleneck, the readings that show it, and what the person can do about it. Readings are sampled by the caller; this module only decides. The one state that stops the city taking on new work is a disk close to full, and the refusal carries that Degradation::DiskLow so the door can say how much to free. The part crates/kernel/spec/Degradation.lean specifies this module.

delegation

Delegation: two delegate kinds, one level deep. The guard is two-layered on purpose: statically, a Delegate value has no delegate method — minting a grandchild cannot be spelled; dynamically, admit re-checks depth at every spawn so a hand-rolled path cannot sneak past the type. One level is an invariant, not a constant — a constant would imply it is tunable. The part crates/kernel/spec/Delegation.lean specifies this module.

discard

Discard: deletion as an effect class, judged by effect and never by intent. C14 in the type: a Discard without a restoration plan cannot be constructed; the unplanned path exists only as a request shape for exec forecasts — and the door denies it. This module is the discard door’s sole authority; gate::discard delegates wholly and only shapes the refusal. The part crates/kernel/spec/Discard.lean specifies this module.

error

AxError, the one error shape of the whole city, and AxCode, the closed set of 35 error codes. The part crates/kernel/spec/Error.lean specifies this module.

event

EventRecord and the closed EventKind set: the value layer of “the Ledger is the only history”.

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.

goal

Same-resource mutual exclusion. Detection is kernel’s; arbitration is not — reading statements and judging intent belongs to models (collab::arbiter) and humans. The part crates/kernel/spec/Goal.lean specifies this module.

idem

IdemKey: the dedup key for outward actions. The part crates/kernel/spec/Idem.lean specifies this module.

keep_warm

Keep-warm: whether, and when, a prompt cache still in use is renewed before the provider lets it expire. The part crates/kernel/spec/KeepWarm.lean specifies this module.

layout

Where a city keeps each kind of file on disk: one derivation from the city root and an address (crates/kernel/spec/Layout.lean §8-56).

ledger

The Ledger port: the only write entrance to history (seam list, ARCHITECTURE section 3), plus the chain rule both adapters and replay share. The part crates/kernel/spec/Ledger.lean specifies this module.

locator

Locator: the one grammar for referring to content across events and sessions. The part crates/kernel/spec/Locator.lean specifies this module. Two schemes only:

model

The model seam (seam registry ARCHITECTURE 3). Every provider call carries a BuildingPolicy value; the policy is defined here (kernel cannot name outer crates) and evaluated by city::policy — dependency inversion, same as the ledger seam. The part crates/kernel/spec/Model.lean specifies this module.

node_id

A plan node’s address: the dotted path that says where it hangs. The part crates/kernel/spec/NodeId.lean specifies this module.

plan

The plan as a tree: what the nodes are, what each one is worth, what may be started now, and the two ways a held node is put down. The part crates/kernel/spec/Plan.lean specifies this module.

policy_limit

Policy limits as values (crates/kernel/spec/PolicyLimit.lean §8-73): each type carries one ceiling’s legal domain and the one refusal that says no, so a caller hands over what it observed and cannot spell a second refusal.

pursuit

A pursuit: a goal the city keeps working towards, and the one condition under which a city that holds one stops. The part crates/kernel/spec/Pursuit.lean specifies this module.

reach

Where a call to a provider stops, stage by stage. The part crates/kernel/spec/Reach.lean specifies this module.

registry

The three registry books: Artifact, Asset, Resident census. The load-bearing line is the Claim/Artifact split — an unverified result is testimony, and Artifact::verify is the only door between the two (player–referee in the type). The registry is a value, not a store: state lives with the caller and is rebuilt from the Ledger. The part crates/kernel/spec/Registry.lean specifies this module.

release

Which release a binary is, and how two releases order. The part crates/kernel/spec/Release.lean specifies this module.

repair

Repair leases: when the environment itself is broken, repair is serialized — one live lease per scope subtree, so two runs can never “fix” the same breakage into a bigger one. The active table is the caller’s state; kernel only judges. The part crates/kernel/spec/Repair.lean specifies this module.

retries

How many times a failed call is made again. The part crates/kernel/spec/Retries.lean specifies this module.

secret

Secret shape judgment, the secret: reference grammar and Sealed<T> . Detection is shape-table-first, entropy-second; both are hand-written, regex-free, backtracking-free and float-free — entropy runs in fixed point so the judgment is deterministic and kani-provable. False positives are the accepted normal: the entrance replaces losslessly, only the exits refuse. The part crates/kernel/spec/Secret.lean specifies this module.

share

How much of the whole plan one node is, and why nobody can mint more. The part crates/kernel/spec/Share.lean specifies this module.

spine

The spine documents’ grammar: how a row of Roadmap.md is written and read, and the six fields a Memo outline carries. The part crates/kernel/spec/Spine.lean specifies this module.

stall

The sole stall criterion. Watchdog consumes the verdict and decides disposal; it never re-derives the criterion — “what counts as stalled” lives here and nowhere else. The part crates/kernel/spec/Stall.lean specifies this module.

taint

The taint ring. One axiom: external content is always data. Tainted::new is the city-wide sole entrance for foreign bytes; reads hand out borrows, derivation unions provenance, and no method ever returns the bare value — “washing it clean” is a compile error, not a review finding. The part crates/kernel/spec/Taint.lean specifies this module.

tool

The tool seam (seam registry ARCHITECTURE 3). ToolMeta is the eight-field registration: a tool without a complete meta is invisible to the model. effect decides which gate a call passes; temporal decides whether its envelope carries a clock stamp. The part crates/kernel/spec/Tool.lean specifies this module.

version

Optimistic concurrency: writes carry a base_version; a stale base yields a verdict, never a silent merge. The part crates/kernel/spec/Version.lean specifies this module.

write_domain

WriteDomain prefix checking and edit-war detection. C17 is enforced twice on purpose: a reserved prefix cannot be constructed into a domain, and a reserved target is refused at judgment even so — fail-closed has no single point of failure. The part crates/kernel/spec/WriteDomain.lean specifies this module.

Structs

Origin

Where a session branched off: one run of this city, and the line in it that the branch starts after.