Expand description
Turn loop and tool surface: frozen prefix, handoff, replay/fork, result pipeline, sandbox ladder.
Re-exports§
pub use backlog::Backlog;pub use backlog::BacklogId;pub use backlog::BacklogKind;pub use backlog::Finished;pub use backlog::Standing;pub use backlog::Started;pub use backlog::Ceiling;pub use backlog::Unapplied;pub use backlog::Unseen;pub use backlog::Chunk;pub use backlog::Exit;pub use backlog::PollBudget;pub use backlog::RunProcesses;pub use backlog::Sink;pub use backlog::Stream;pub use tools::BoundReader;pub use tools::CallTool;pub use tools::ChildStatus;pub use tools::DescribeTool;pub use tools::EditTool;pub use tools::ProviderMode;pub use tools::ReadBound;pub use tools::ReadTool;pub use tools::SearchTool;pub use tools::StatusSnapshot;pub use tools::StatusTool;pub use tools::parse_arm;pub use tools::version_of;pub use tools::ExecSetup;pub use tools::ExecTool;pub use tools::FailureClass;pub use tools::Shell;pub use tools::ShellCount;pub use tools::ShellTally;pub use tools::SucceedTool;pub use tools::Succession;pub use tools::SuccessionDesk;pub use catalog::Catalog;pub use catalog::CatalogEntry;pub use catalog::Expansion;pub use clock::ClockReading;pub use clock::ClockStamp;pub use clock::StampGate;pub use clock::ZoneEntry;pub use clock::stamp;pub use digest::Breaker;pub use digest::BreakerVerdict;pub use digest::Digest;pub use digest::DigestOutcome;pub use digest::StructureNode;pub use digest::digest_once;pub use digest::structure_of;pub use handoff::Handoff;pub use handoff::ResumeSeed;pub use handoff::resume;pub use mode::Admission;pub use mode::PolicyCell;pub use mode::PolicyReader;pub use mode::Produced;pub use mode::admits;pub use offload::OffloadRecord;pub use offload::OffloadSite;pub use offload::offload;pub use offload::rematerialize;pub use pipeline::connector::CONNECTOR_CAP_BYTES;pub use pipeline::connector::package_connector;pub use pipeline::connector::png_picture;pub use pipeline::exec::EXEC_CAP_BYTES;pub use pipeline::exec::SieveSite;pub use pipeline::exec::package_exec;pub use pipeline::PackContext;pub use pipeline::Packaged;pub use pipeline::SieveRequest;pub use pipeline::exit_code_in;pub use pipeline::package;pub use pipeline::pinned_original;pub use prefix::FrozenPrefix;pub use prefix::FrozenSegment;pub use prefix::SegmentSlot;pub use prefix::PrefixPlan;pub use prefix::SegmentCaps;pub use prefix::SegmentSource;pub use prefix::SourceDoc;pub use prefix::build_prefix;pub use reminder::ContextGauge;pub use reminder::ContextReading;pub use reminder::ContextReminder;pub use replay::VerifiedLedger;pub use replay::VerifiedLine;pub use run::Advance;pub use run::Run;pub use run::RunHooks;pub use run::RunPlan;pub use run::SafePoint;pub use run::drive;pub use sieve::CommandKey;pub use sieve::FilterTable;pub use sieve::SieveHistory;pub use sieve::SieveRecord;pub use sieve::Sieved;pub use sieve::sieve;pub use transcript::Transcript;pub use transcript::TranscriptRecord;pub use turn::Admitted;pub use turn::ConcurrentInvoke;pub use turn::Interrupt;pub use turn::NextCall;pub use turn::PhaseOutcome;pub use turn::Turn;pub use turn::TurnCancelled;pub use turn::TurnReport;
Modules§
- backlog
- The work still running while a run goes on, and the one place it is stopped.
- bench
- The tool bench: which door one call goes through, in which order, and what comes back when a door says no.
- catalog
- Progressive disclosure and the truncation lock
(
crates/runtime/Spec.lean§8-60, §8-61). Only what this session can actually reach is listed — admission is the caller’s evidence: the assembler registers the tools a building’s vocation, rules and book allow, and reads each building’s reading room off itscity::policyrules. Of what is admitted, the mode’s core travels as tools; the rest is one line each in the dormant index, and a run fetches a guide withdescribeand runs a dormant tool throughcall. - clock
- ClockStamp: pure formatting of an injected instant against already-resolved zone offsets, and the one spelling of a moment a person or a model reads: ISO 8601, UTC, to the second. Nothing here samples a clock; the calendar is integer arithmetic so replay and live share one algorithm and no tz database.
- compaction
- When to shorten something, and what to keep.
- conversation
- The run’s conversation history: the volatile half of a request.
- diagnostics
- The diagnostic log: write-only, five levels, three required fields.
The design this implements is
docs/logging.md. - digest
- The digest pipeline: what a long document looks like from outside.
- elision
- What a cut says, and where a cut may land.
- fork
- Fork: a new Run whose in-window history is a byte-identical prefix of
the mother sequence. Forking is not
resurrection: the mother’s frozen state never changes, and the new
RunId arrives from the caller — this module is pure.
crates/runtime/spec/Fork.leanproves what a fork must hold (§8-2): the prefix is the mother’s first lines, and the cut never splits a wave. - handoff
- Freezing and resume. A Handoff is the five-section crossing point between a frozen Run and its successor. It is never a new authority: on conflict, fresh reads and real execution win.
- mode
- 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).
- offload
- The shared shrink primitive: lossy-but-restorable, owned here and nowhere else. Four invariants, each enforced in code: store-before-cut; substitute (hint included) never larger than the original nor the cap; only lossy transforms store; the substitute always carries a materialized read-only rest path. CAS dedup makes repeated offloads of the same bytes idempotent.
- pipeline
- The result pipeline: shrink order and the envelope’s three attachments, assembled in one place. Order is the law: offload always precedes truncation; plain truncation is the no-CAS fallback and never stores. The three attachment sentences are defined here once — changing them changes window bytes and passes through the SPEC.
- prefix
- Frozen prefix assembly: four segments, assembled
once at Run start, never reassembled within the Run. Volatile types
(TimeMs, usage, signals) have no conversion into
FrozenSegment— the absence of those impls is the isolation guarantee (15.3-4). - redact
- What a model said, on its way into history.
- reminder
- How full the window is, from the provider’s own count.
- replay
- Offline replay: re-verifies a Ledger without re-executing anything. The second and last minting point for EventRef.
- run
- The run driver: dispatch, turns, freeze — the single authority for the event sequence a run leaves behind. The real city and citysim call this same code, so the simulator’s byte fixtures are evidence about production rather than about a second implementation of the same idea.
- sieve
- What survives a command’s output, decided by which command produced
it.
compactionreads the shape of a text; this reads the identity of its author, becausecargo buildandgit statusare both logs and their noise has nothing in common. - tools
- The L0 three. Index only: no logic lives here.
- transcript
- What one run actually saw, written beside its room when it freezes.
- turn
- The turn typestate: Assembling -> Calling ->
ToolWave -> Recording, phase changes carrying
&mut dyn Ledger. Interrupts are consumed only at phase boundaries — the boundary snapshot is a parameter of every transition, and no method exists that could observe one mid-phase. That absence is A9’s structural half. A wave is many effects rather than one, so every call in it is a boundary of the same kind: the executor is asked before each, and a halt ends the wave there instead of after its last call. Steer consumes at a boundary too, but advances: it is an addition to the window, not an ending.
Structs§
- Absent
Sandbox - What a binary built without an execution engine offers: a refusal that names the missing piece.
- Echo
Sandbox - A pass-through stand-in: stdout echoes stdin, plus whatever script output the test queued. Used where the test is about the caller’s logic rather than the boundary.
- Fault
Sandbox - A fault stand-in: pops a scripted outcome per call, so a caller’s handling of exhaustion and traps is testable without provoking the real engine into either.
- Fuel
- Instruction budget. Exhaustion ends the guest; it does not fail the host.
- Mount
- One granted capability: a host directory visible to the guest under
guest, writable or not. The mount list is the whole of what the job can reach. - Sandbox
Job - Sandbox
Outcome - Skill
Pin - One skill a run was dispatched with, pinned to the bytes it read.
- Watchdog
- One watchdog per run: it holds the correction history, the ceiling the person set on retries, and the account round of the model call in flight.
Enums§
- Disposal
- Deliberately exhaustive: a new disposal must force every run loop to decide, not fall through a catch-all.
- Freeze
Reason - Opening
- How the first user message opens: kernel’s, because
run_startedrecords it (crates/kernel/Spec.lean§8-82-1). How a run’s first user message opens. - Sandbox
Exit - How the guest ended. Every variant is a fact about the guest — the host never hides a guest failure behind a success.
Traits§
- Sandbox
- The seam. One method: hand it a job, get back what the guest did.
Send, because theexectool that holds one isSend(crates/sprawling/Spec.lean§8-44); every adapter here already was.
Functions§
- backoff_
ms - How long
runwaits before asking again afterfailure, thefailures_in_a_row-th since its provider last answered: the longer of the schedule below and the provider’s ownretry-after.