Wiki index
Catalog of every page. Read this first, then drill into the pages. How pages are written and kept honest is the maintainer contract.
How this is laid out
Five layers, each with a different relationship to staleness:
design/— why the design is what it is: durable theory and cross-cutting concepts.internals/— how it runs: narratives threading several subsystems into one flow.invariants/— the hard rules, one per page.decisions/— why it changed: one dated ADR per decision, status in its frontmatter.map/— where things live: thin pointers into the code, stamped with the commit they track.
Start here
A guided path through the system, why before how: syscalls-are-effects → cbpv → types → the compilation ladder → the evaluator machine → grant → capability enforcement → exarch-architecture → a run, end to end.
design/ — the why
- syscalls-are-effects — the foundational principle: a system call is an algebraic-effect operation, separated from its OS interpretation; handlers and reified continuations are orthogonal layers on top.
- cbpv — call-by-push-value: values vs commands, the two sigils, thunks, immutable bindings.
- types — Hindley–Milner with let-polymorphism over computation types
F[ρ] A; the payload routeρnames which of a computation’s two products a value boundary reads — its returned value or its stdout, never both — and says nothing about whether it writes. WF-2 (BytesimpliesUnit) is an obligation reproved at each of the two operations that ground a route; the route is inference machinery only — grounding it is the checker’s last act, spent immediately on syntax the evaluator reads. - effects-handlers — algebraic effects; deep, self-masking, tail-resumptive handlers; no first-class
resume. - grant — capabilities; authority attenuated by intersection; exarch’s sandbox.
- capability-freeze — one always-frozen
Capabilities, resolved at decode time; the freeze pass is the one-way door and the xdg-escape guard a per-profile invariant. - two-enforcers — why capability checks gate in-process and in the OS sandbox: each enforces where the other is blind, “all sandbox” is strictly weaker.
- capability-carriers — why authority needs three forms, not one: the rule you write, the live act of judging, and the flat checklist for the blunt OS guard.
- row-types — open-row-polymorphic records with scoped labels and spread shadowing.
- records-and-maps — one runtime carrier, two static types: heterogeneous static-label records vs homogeneous runtime-key maps; the key space, the indexing split, the forgetful Record→Map coercion.
- pipelines —
|as a positional byte wire: stdout to stdin, neither endpoint promising traffic, non-final returned values discarded rather than serialised. Two static rules, each about one stage: it must be a computation ready to run, not a function awaiting an argument, and past the first position it may not bind stdin at its own root — a feed that shadows the whole stage leaves the producer across the|writing for nobody. Ordinary application/bind compose values, decoder tails remain the idiom, and the final value report is helper-staged for now. Lifetime is tail-ward too: ral kills a non-final stage once its reader stage is gone, and that kill is a pipeline’s one forgiven death (a-stage-ral-stopped-has-no-failure). - name-resolution — where a capability lives: the layering of head names; effects→coreutils, queries→builtins, conveniences→prelude.
- builtins — the structured primitive set: the three kinds of irreducibility (reaches a syscall/shell state · base computation · undelivable type), the families, the
Sig/Schemerules with the derived value form, and the manifest authored as two — a name is a native value or a base frame. - codecs —
from-X/to-Xas the typed byte↔value crossing: a decoderF[Value] A, an encoderA → F[Bytes] Unit; strict structured decode vs lossy line streams. - capture — a command’s value is its stdout, a block’s value is its last statement’s, and a discarded statement’s bytes go out: so
!{ echo a ; echo b }printsaand yields"b", with no2>/dev/nullneeded to keep setup noise out of a result. Discarded bytes leave the whole capture chain — the nearest enclosing visible stream, never an enclosing buffer — which is the clause an implementation can get subtly wrong at two levels of nesting. Realised twice: statically by pushing theCapturewrap to the payload leaf (so non-final statements are never inside the bracket), dynamically by a per-boundary flush where a thunk boundary hides the sequence from that walk. It is also why a statement boundary is its own former and not sugar for a bind on a dropped variable — a bind at a byte payload installs the buffer and destroys the bytes, at the very same type. Exactness is kept by refusal at the 16 MiB buffer cap: a capture that reaches it fails rather than bind a truncated prefix, flushing what it holds where a failing capture’s bytes always go. - control-operators — the five reserved operators vs control flow as library; audit ownership.
- failure — failure is status, not truth;
?fallback chains,tryas recovery and the only||, aBoolis data. - scoping — lexical scoping for data, dynamic scoping for ambient authority.
- audit — execution as a flat, lexically-scoped trail of
Observations; scope-shaped delimiters whose opener owns closing, lexical ownership, processes only transport fragments, and the dispatch itself as a delimiter (Run.trail). - exarch-architecture — the agent as a provider loop over one
raltool, each exchange a grant-framed ral top-level run; orchestration verbs are ral builtins, not sibling provider tools. - hash-addressed-editing — the scheme
--edit hashteaches, string replacement being the taught default; exarch addresses a line by an adaptive-context witness: a digest of the line plus the smallest window of neighbours (≥ ±5, grown only where a line repeats) that names it uniquely, no line number.view-hash,view-hash-around, andedit-hashare all path-based, sharing one witness function and one read door, so the hash a read shows is always a valid handle;edit-hash path [[hash: …, line: …], …]resolves every hash against one read before writing one atomic batch. Closes with a comparison against the two anchor-based edit harnesses it descends from — Bölük’s hashline (disambiguates by line number) and Dirac’s stateful single-token anchors (by construction) — reaching their ambiguity-free editing statelessly, by growing the window. - pins — a pin is state a kit publishes to a keyed register slot, overwritten in place — the model-authored dual of the agent matrix.
surface ``pin [key, body]writes acard `` to the focused session's reserved right-hand column; ``unpin “ drops it. Never landed in scrollback and not restored on resume (what is, not what happened), though the record log keepsPin/Unpinas forensic breadcrumbs; the register mirrorstasks/goalfor the nudge that tells the model, once, whenever what it has pinned changes and it is actionable; every key is model-chosen and the write side has no reserved key or guard at all. - exarch-config-dir — exarch’s trusted configuration lives in the XDG config home (
$XDG_CONFIG_HOME/exarch/), structurally outside the working tree the sandboxed agent can write, and distinct from the per-project state home (model selection + run logs) and the cache home (model catalog). Holdsconfig.ral(custom providers) and globalAGENTS.md; trusted because the grant cannot reach it, yetconfig.ralis still evaluated no-authority because a redirected endpoint is an exfiltration channel. - agents-md-injection — exarch injects
AGENTS.mdfiles as aWorkspacesystem-prompt section, discovered outermost-first (operator’s<config>/AGENTS.md, then every repoAGENTS.mdfrom the git root down to cwd; the walk stops at the first.gitentry). They steer behaviour but add only prompt text, never capabilities — so a cwdAGENTS.mdis untrusted yet harmless: it cannot widen the grant, unlike trustedconfig.ral, which can cause effects. - agents — the sub-agent model: a run is a tree of uniform
Agentnodes under one sharedattendloop, distinguished only by position — the parent-less trunk (conversing when a human is attached, withholdingreply) versus every returning agent, keyed on a construction-fixedreturnsbit, never anis_rootflag. Spawning is universal but bounded byfuel, a per-agent budget each fork hands one less unit of to its child; the record-specagents `starttag forks the serialisable fragment of the parent shell’s value-snapshot onto a detached thread (handle-carrying bindings scrubbed byfork_scrubbedbefore either seat chooses how the fork waits, so an identity fork and a wire hatch’sEngineSeedmean the same thing — the one snapshot law) and gives the child a name that is its fleet-unique identity; the spec’stypefield picks the child’s memory —amnemonblank,mnemoninheriting the parent context with a fresh prompt; an agent may send a marked message to a named descendant; returning is the deliberatereply, which cancels unfinished descendants before the node settles; focus is the dynamic human attachment, immune to the subtree cascade that onlyagents `cancel, the idle-lease reaper, and/clearperform —Escinterrupts just the focused exchange; self-scheduling authority is inherited; a spawn’s mandatorygrantbase bounds the child toparent ⊓ base— a lattice meet that narrows but never escalates. A wire-seat trunk still spawns in that oneagents `startexchange: its engine listens once, the host dials throughDial, and one ack after child creation makes the returned roster honest. - egress — egress is a destination policy: the guest may
open TCP connections to port 443 of the public addresses these exact
hostnames resolve to, once, on the host, and to no other destination.
synod’s guest network terminates everyCONNECThost-side, vets and pins the resolved address, then copies bytes both ways unparsed; the honest residual is that an allowed host still receives whatever the guest sends it, and a shared CDN edge can carry more than one name — which is why the audit ledger is load-bearing rather than decorative. - residency — everything that stays alive between runs — a detached worker, a stopped pgid group, a sub-agent, a schedule, a top-level binding — is a resident with four facets (identity, capability, lease, probe); the ledger is an interface each chapter answers through its own representation, never a fused struct, and lifetime moves along one graded residency order, from foreground through stopped/background/durable to survives-exit, discovered mid-flight by interactive work and declared at birth by agent work.
- engine-protocol — the front-end↔engine protocol is one duplex stream sorted into four channels by direction and by answered/one-way (
Dispatch → Report,Control;Enquiry → Answer,Surface), every payload a first-orderFOValuebehind a closed, versioned envelope that grows only by class, never by channel; a run’s whole host-facing surface is oneHostobject riding the dispatch, realised by exactly two bindings — a direct call sharing an address space, or a codec across a socket, a process, or a vsock into a guest, where the guest binds an ephemeral listener per spawn and the host dials in; any frame is proof of life, the firstPingarms the read deadline, and every terminal cause collapses into one type,Severed, that ends the front-end’s session.
internals/ — how it runs
- compilation-ladder — source → tokens → flat AST → CBPV IR → annotated typed IR; the two
compileverbs, per-run seeding, the annotated prelude bake. - surface-syntax — context-free lexing, recursive-descent + Pratt parsing, the flat AST, three-stage head classification.
- type-inference — the HM algorithm: the Inferencer, the Unifier (types, rows by Rémy rewrite, payload routes by equality), the one shape rule that forces every pipeline stage to
Return, WF-2 reproved at each route grounder, the one deferred arm-result join, generalisation atBind, the verdict written onto the IR to survive into the next run. - evaluator-machine — the CEK machine: computation closures in focus, frames carrying environments, one
stepwith one arm per rule, two terminal shapes, one thunk value,recn-ary, a frame-counted cap checked before the effect, phrases andDefineat the top level, pipes as nodes launched and joined in one rule, the panic walk. - builtins-registry —
builtin_registry!and its facets, derived arity, the manifest as a boot manifest seeding natives and base frames, bundled coreutils, host-layer builtins. - handler-dispatch — the handler stack: two-pass lookup, self-masking strip-and-restore, deep frames on the dynamic context.
- capability-enforcement — the meet-fold chokepoint as a module boundary (
capability::check_*(&Context, …)); in-process gate for what ral dispatches, an OS sandbox for what a spawned child does (net is OS-only; per-command on macOS/Linux, projection-keyed on Windows); the grant body evaluates locally. - pipeline-execution — byte edges allocated from stage position in one process group; the route-blind resolve-time
StageLaunchfreeze, the singlePipeYielddeciding the helper-staged value report, the held-open read end and the collector’s tail-first kill of a stage whose reader is gone, shared child-eval frame pair, then ≥ 2pgid anchor, Windows Job Objects and their spawn-boundary limits. - a run, end to end — one top-level run for a ral REPL line and an exarch tool call, through the shared framed door (
Shell::rundispatching onProgram::Source/Program::Hook→RunReport). - output-capture-and-detachment — capture drains each child’s pipe to EOF, so a process that never closes it stalls the foreground to the wall and is killed with its tree;
spawnmoves it to a root-parented worker with a 16 MiB-bounded buffer under an idle-observation lease (1 h unobserved, 24 h backstop;servicebirths the durable class). A long-running server is the canonical case. - binding-leases — exarch expires idle top-level scratch names: the unlocked single-writer ledger on
LocalState, the committed-run clock, static use-harvest over the typed IR, the prune verb whose signature pairs notices with the post-prune checkpoint, the pin walk that refuses closure captures — and the worked capture scenario (a hot closure keeps a pruned name’s value alive and working; command-position use renews, value-position does not). - cancellation — stopping in-flight work: one cooperative cause-bearing
CancelScopetree (Interrupt < Explicit < Deadline < Terminate < RootAbort) that the platform handlers translate signals into via two ambient causes — an absolute shutdown cell and a temporal interrupt watermark read against a frame’s birth (SIGINT → foregroundInterrupt, SIGTERM/SIGHUP → rootTerminateat exit 143) — backed by an escalation ladder whose third delivery_exits;process::checkpolls only the scope tree; per-host gestures — REPL Ctrl-C relays + foreground-cancels, REPL Ctrl-\root-aborts, exarch TUI active-exchange Ctrl-C/Esc drives a per-exchange token. - provider-fault-recovery — genai errors at the LLM boundary: the structural
Faultwalk (Status/Transport/Terminal) that reads retryability from typed variants, never theDisplaystring; the 429 / 5xx / 4xx split intoProviderError; the oneretry_with_backoffdriver with a patient rate-limit tier and explicitRetry-After; the streaming commit-don’t-double-render rule; the idle timeout that turns a silent socket into a retryable fault with a bounded budget. - session-record — one append-then-publish seam writes
record.jsonl; sealed protocol/display/forensic classes feed the model and view folds, transients remain live edges, anduser.logis a bounded viewport’s rendered stream rather than a second authority.
invariants/ — hard rules
- fixed-arity — application is fixed-arity; the manifest is authored as two and arity follows — derived from a table entry’s type rule, while the argv half has no arity at all — so a base-frame row has no first-class form, and a handler consumes its argv packed as one list of strings.
- single-binary — ral ships as one executable; no sibling helpers.
- ir-pure-cbpv — the IR carries no surface sugar; conveniences unfold at elaboration.
- optionality-via-variants — no Option/null; optionality is open variants.
- exchange-ends-ready — an exchange leaves a fresh prompt admissible however it ends; only outstanding tool calls hold the log, and an exchange abandoned short of a reply is left as it lies rather than closed by a fabricated one.
- schemes-leave-closed — a
Schemeleaves its minting unifier only if closed; quantification is nominal-by-listing, so a residual id aliases a foreign unifier’s variables. - exec-argv-is-words — an argv the shell renders is total, an argv crossing into
execve(2)is words; the shapes that are not words are declared once (RefusedArg) and read at both moments a call can be refused — the checker before the run, the spawn at it. - probe-convention — every session-lived resident or accumulator exposes a non-renewing resource probe whose policy names its bound;
/resourcesis the fold over those probes. - transcript-admission — every provider-facing message is repaired or refused at the commit boundary so the durable model projection contains only serialisable, sendable turns.
- numerals-denote-numbers — a bare word the numeral grammar accepts denotes that number in every position, with no positional asymmetry; classification is lexical, never type-directed; every number has one printed spelling, so canonical spellings are fixed points of classify-then-print and bytes require quotes (
'007'). The printer’s whole image lies inside the grammar — it restores the point ryu omits, so1.0e300rather than1e300— hence printing then reading is the identity on numbers, while1e6remains a word; the emitter that renders aStringback as source consults the grammar for the same reason, so a numeral-shaped string comes back quoted.
decisions/ — why it changed
Newest last; the page carries the full reasoning.
-
superseded — typed-state-flow-wrappers — typed wrappers for shell-state flow; the boundaries closed by env-is-dynamic-only and a
current_diraudit, so the wrappers were not built. -
active — hot-path-cancellation — cooperative cancellation in hot loops.
-
active — completion-escape-refactor —
EvalSignalretired forSettled+ Escape/BodyResult. -
fixed — escape-propagation-bugs — try-swallows-exit and grant tail-call bypass.
-
active — repl-builtins-stay-in-repl — REPL builtins live in the REPL layer, above core.
-
proposed — repl-architecture — REPL direction: stream console now, hybrid workbench later.
-
active — background-tool-calls — scoped in-turn agent batching is active:
dispatchstages a whole tool-call batch under onethread::scopeand joins before the parent turn continues; true turn-outliving backgroundable tools remain future work. -
fixed — redirect-drop-on-handler-dispatch — redirects install on the handler arm.
-
active — ast-stays-flat — the surface AST enum stays flat.
-
active — handlers-deep-self-masking — handlers are deep and self-masking.
-
active — infer-case-stays-whole —
infer_caseis left as one function. -
superseded — env-overrides-scope-overlap —
env_overrides/ scope overlap. -
open — linux-exec-confinement — path-scoped exec is unenforced on Linux (no landlock).
-
active — env-is-dynamic-only — the environment is dynamic state, read through
$env. -
superseded — modes-equality-constrained-shared — pipeline modes are equality-constrained, in one shared definition; the two-mode lattice it built is deleted by pipes-are-positional-byte-wires, leaving one payload route under the same equality rule.
-
superseded — reduced-authority-witness — a reduced-authority witness made the capability chokepoint a type.
-
active — xdg-resolver-consolidation — one XDG base-directory resolver; exhaustive transport walks.
-
active — exec-authority-partitioned — exec gets a partitioned
ExecMap; the two capability folds stay separate. -
active — capability-stage-collapse — collapse the syntactic/resolved stage split into one always-frozen
Capabilities; freeze at decode, the xdg guard a per-profile invariant. -
active — witness-collapse — the reduced-authority witness collapses to free
capability::check_*(&Context, …)functions; a module boundary, not a typestate. -
proposed — stateful-handlers — a handler frame threads a state value across interceptions; a fold, no continuations.
-
rejected — related-borrowables-rejected — duplicate-label lint,
--effectslisting, record restriction, effect rows, capability boxing. -
active — session-scheme-continuity — turn schemes persist into the next turn’s check, living on the runtime binding (1/4 of the one-mode-engine series).
-
superseded — handler-alias-mode-preservation — handlers and aliases preserve a head’s pipe signature (2/4); narrowed in place to the one thing left to preserve, the payload route, with the pin now also enforcing WF-2 — a defect it carried, which let a byte-routed head admit an arm returning a non-
Unitvalue. -
superseded — ir-pipespec-annotation — the checker writes ground mode wires into the IR; the evaluator reads, never infers (3/4, landed). The per-stage
Wireis replaced by a singlePipeYieldper pipeline in pipes-are-positional-byte-wires: with no interior adjacency rule there is no interior adjacency to annotate. -
superseded — unconditional-mode-pass — the inference pass always runs; the runtime mode engine (
ty.rs/classify.rs) deleted;--no-typecheckand its fragment/verdict apparatus retired — value-type errors fatal on every path (4/4, window closed). Superseded in vocabulary only by pipes-are-positional-byte-wires: there is no mode pass left to make unconditional, but the pass itself still runs on every evaluated path. -
active — unify-one-sided-obligations — the co-inductive unifier memoizes one-sided var-vs-structural-key obligations, so a recursive type anchored at a ty-var unifies with the same type anchored at a comp-var instead of overflowing the stack. Narrowed in place: the key that once fingerprinted an
input/outputpair now carries one field, the payload route — added back deliberately, since deleting the pair alone would have left a key that forgets the route and silently conflates two obligations the guard exists to keep apart. -
superseded — alias-head-defines-its-modes — a fresh alias/handler head defines its own modes (unknown
head_pipe_specyields a freshF[μ, ν]); preservation binds only a known head;?chains union their arms’ modes; the byte discipline enforces at the connection, not the definition (supersedes handler-alias-mode-preservation). Restated as a single route pin, with the WF-2 obligation it was missing, by pipes-are-positional-byte-wires. -
active — cacheless-module-loader — module loads carry no cross-session cache (freshness over a memoisation a shell never needs); the cycle/depth guards are retained and load-bearing;
usebecomes a scope-projecting wrapper over the sharedevaluate_source. -
active — esc-non-escalating-interrupt — exarch’s Esc drives ral’s non-escalating
process::interrupt(the termination counter to exactly 1, never afetch_add), so the first press returns to the prompt and repeated presses can’t reach the third-signal_exit; only a genuine external signal still escalates. -
active — one-debug-path — one debug-tracing primitive,
dbg_trace!, gated ondebug_assertionsalone with no environment flag; thetry-caught-error echo shares the gate, and consumers of a debug child’s stderr must drain it concurrently since tracing is unconditional. -
active — witness-hash-h-prefix — the exarch edit witness is
hplus six hex so a bare witness lexes asString, notVal::Int; an all-digit digest would otherwise fail its ownequaland trap the agent in an infinite edit loop (string-coercingedit-hashcan’t recover a leading-zero digest). Its open language question — type-directed literals — is answered, DECLINED in favour of literal syntax by a-numeral-denotes-its-number: both candidates this ADR named (bidirectional elaboration threading expected types to leaves, and a polymorphic literal with defaulting) were examined and rejected — the second for losing principality across the default, breakinglet-naming’s meaning preservation, forking on the monomorphism restriction, and needing a joint fixpoint with the route solver; qualified literals with evidence are left open for the future. -
proposed — raw-delimiter-near-miss — a
#\'near-miss errors in value position ([L0004]) and back-points the [L0001] it strands in line-leading position; the grammar is unchanged (#\'is still not a raw-string opener). Rests on confirming “do not change the grammar” permits a hard error. -
superseded — pure-pipe-equation — the historical value-edge equation
x | f = f !{x}; superseded by pipes-are-positional-byte-wires, where there is no value edge to state an equation about:x | fis an ordinary pipeline whose producer writes nothing, and value composition lives in application and bind. -
active — child-eval-unification — one re-exec’d-child eval protocol (
run_child_eval+ChildKind) replaces the sandbox/pipeline pair; one wire shape in and out, the two-snapshots-must-agree hazard gone. -
active — evaluator-runtime-split — the command/pipeline/transport machinery moves to
core/src/runtime/;evaluator/is the ~2.6k CBPV machine and the seam a module boundary, not just a claim. -
active — host-embedding-api —
BakedPrelude+boot_shelldeduplicate hosting a Shell; the postcard bake moves into core, the schema-evolution hazard collapses from three files to one. -
superseded — value-edge-locality — the historical locality rule for typed value edges; superseded by pipes-are-positional-byte-wires, since the one surviving edge fact is positional and needs no judgment sited anywhere.
-
active — authenticated-confinement-marker — the OS-confinement marker
RAL_SANDBOX_ACTIVEis trusted only when it carries a per-re-exec capability token the parent shipped in the IPC request (not the bare inheritable env var); a forged marker no longer suppressesnet/fs confinement, and bundled coreutils reach the fs floor by running in the confined child (deep-review S1/S2/S8, A8). -
active — per-root-turn-cancel — one root-turn
Tokenis shared down parent and sub-agent turns; minting is the reset, and exarch session-shell boot owns stale-interrupt discard plus cancel-handler re-chaining. -
active — exarch-panic-recovery — a caught panic skips ral’s save/restore epilogues, so exarch’s one persistent
Shellis poisoned and reconciled, never unwound frame by frame: the per-call IO frame (tees,surfacesink, script location, watchdog scope) self-heals throughrun_shell’s RAIIIoGuard, and the rest of the dynamic context rolls back to the(env, context, last_status)checkpoint the engine’s run door takes at each call’s entry — completed calls’ bindings and cwd survive, the panicking call’s grant frame, env/cwd, and handler mutations roll back. Host state installed for the duration of one tool call restores on unwind or is reconciled at the panic boundary; never a hand-written epilogue a panic can skip. -
superseded — terminal-foreground-ownership — the
tcsetpgrphandoff is gated on owning the terminal’s foreground (startup_foreground, atcgetpgrp == getpgrpprobe), not on being an interactive REPL, so terminal-launched scripts foreground interactive children (claude,fzf);ForegroundGuardmasks SIGTTOU during the parent-local restore, and parking on stop stays REPL-only. Superseded by terminal-lease, which reifiesstartup_foregroundas a held lease. -
proposed — provider-config-ral-script — exarch declares almost nothing: a famous provider whose conventional key is in the env auto-populates and its models are fetched live (genai
all_model_names, lazy + cached + manual fallback); a hand-written XDGconfig.ralis only for unusual providers (endpoint + protocolcompletions/responses/anthropic→AdapterKind, no-authority eval); the active model + tuning are picker-written runtime state at$XDG_STATE_HOME/exarch/<project-slug>/state.json(per-project, beside that project’s session logs via the sharedbootstrap::project_dir; outside cwd so the agent can’t reach it — no deny-list), loaded on startup./modelis a searchable strip picker, a secondary picker sets tuning. Reasoning is never stripped (genai handles it per adapter; DeepSeek/Kimi require the echo). DRY: provider knowledge fromProviderKind::info, models from genai, protocols fromAdapterKind. Slices: auto-discovery+picker → tuning → unusual-provider config → OAuth. Since 2026-08-17: that table isidentity::built_in_servicesreturningServicestructs, a declared endpoint is the same struct rather than a separate arm, and every credential keys on anAccountId— one service may own many accounts. -
proposed — structural-bug-prevention — a wide review’s serious bugs collapse into nine recurring shapes (check/use path mismatch, cancellation that never cancels, a privileged fd/handle leaking into a confined child, an invertible range, a record read as an ordered key-stream, continuation by token-suffix heuristic, error classification by
Display-scraping, adebug_assert-only guard, a never-populated source identity). Each gets a missing type that makes the bad state unconstructable (ResolvedPath, a parent-linkedCancelScope, an RAIIIpcEndpoint+Tokenedresponse, a non-invertibleSpan, a typed record-decode, anIncompletenesssignal, typed provider-error variants, PWD/OLDPWD excluded from settable env, a non-optional source id) with a clippy backstop only at the one sanctioned call site — type-first, lint-as-backstop, the disciplineclippy.tomlalready applies to paths. Staged behind the immediate point-fixes. -
active — no-core-repr-leak-into-exarch — the host reads core’s capability state through accessors (
ExecPolicy::admit_label/is_denied), never by destructuring its representation;Subcommandsbecame aBTreeSet(idempotence by construction) and exarch’s prompt stopped matchingExecPolicy. The data-shape corollary of the host-embedding seam. -
active — handle-settle — a finished handle has one settle
{stdout, stderr, outcome: <ok: α | err>};poll → <pending | settled>reports it as data (total, never raises), whileawait/raceunwrap it to{value, stdout, stderr}and re-raiseerr(the dead always-0statusfield dropped). Buffers drain once into a cachedCompletedHandle; a panicked worker’sDisconnectedsettles aserr(fixingpoll-forever /race-spin);is-donetotal. Outcome-as-variant, the orthogonal done/ok split, over siblingready/failedarms. -
active — tool-boundary-steering — queued prompts drain after the current assistant tool-call batch, before the next provider request. Every requested tool id receives a
ToolResultbefore the user message is appended; same-batchagentcalls can overlap, and queued input steers the next assistant step rather than skipping already-issued sibling calls. -
proposed — force-eliminates-blocks — the surface
!should eliminate a value-producing thunk (a block,U(F α)), not a function-thunk;!$bodythen typesbodyas a nullary block, so a function-bodied argument fails at the call site instead of returning unrun. The naive runtime arm is unsound —step_forceis shared with the elaborator’sApp(Force(Variable), args)call head — so the two force sites must first be told apart. -
active — unify-turn-evaluation — lift one top-level turn into
ral_coreaseval_turn(shell, src, frame): the frame carries anIoFrameregime sum (Inherit|Capture), the foregroundCancelScope,Capabilities, and lifecycle callbacks;TurnOutcomehas static and runtime arms (the runtime arm carriesresult,eval_status, andsingle_command). The root/foreground split fixes exarch’s collateral kill by rooting detached workers at the durable shell root while compiled turns run under a child foreground scope. Scope cancellation is cause-bearing (Interrupt,Explicit,Deadline,RootAbort), translated into the scope tree byral_coresignal-safe cancel slots published per turn: Ctrl-C/Esc interrupt the foreground, handle cancellation and deadlines reap workers decisively, and Ctrl-\aborts the root. The single timer/reaper service and the death-clock were since built in concurrency-detached-vs-structured (process::reaper; exarch’s per-call watchdog thread retired onto it). Still deferred: the worker registry/survivor warning, and unifying theralbatch path througheval_turn. -
active — concurrency-detached-vs-structured — with the root/foreground split,
spawnand&are root-detached handle workers,watchis root-detached but REPL-only because it needs a durable output sink, pipelines are foreground-bounded, andparremains the accepted prelude compromise: success joins every rootspawnhandle, while foreground early exit or first failedawaitcan orphan the unjoined tail until cancel/one-hour ceiling/root abort/session exit.awaitadoptsrace’s cancel-aware wait loop,cancel/raceloser cancellation use explicit worker teardown,forgetis deleted, and exarch arms a frame-owned one hour lifetime ceiling on a sharedprocess::reaperdeadline service (the timer/reaper the turn-evaluation ADR left unbuilt). Truly long-lived agent jobs remain future separate host-managed work rather than a per-spawn timeout knob. The death-clock’s creation-age policy and the no-introspection doctrine were since amended by leases-and-budgets (idle-observation lease over a universal worker registry); the handle model and everything else stand. -
complete — turn-local-state — split
Shellby lifetime:mobileremains the persistable computation state;turnis the installed top-level frame (Io,surface, typed foreground scope, full non-dblocation cursor);sessionholds the durable root,SourceDb, exit hints, and the host-installed builtin table;localshrinks to audit and REPL scratch.eval_turnbecomes oneTurnStateswap plus same-extent signal-slot publication; same-thread IO still keeps its inherit/return manifest; IPC mobiles do not carry builtin bodies, so receivers preserve their ownsession.builtins; visibility narrows around invariant-bearing state with opaque root/foreground handles and host accessors. -
superseded — bundled-tools-as-exec-images — bundled coreutils/diffutils/ripgrep heads become an
ExecImagespawned as ral itself through a hidden bundled-tool sentinel; value-edge bundled heads still routeHelperEval, and the pipeline helper stops being a coreutils launcher. Its inline clean-terminal placement is withdrawn by bundled-tools-always-reexec; the image representation, entrypoint, pipeline rules, and audit story carry forward. -
active — watch-repl-builtin — a builtin a host cannot run should be absent from it, not present-but-vetoed:
watchleftCORE_BUILTINSforcore::builtins::WATCH_BUILTIN, a one-entry slice the ral host installs through the sameregister_builtinsmechanism exarch uses for its agent tools — registered process-wide inregister_host_surfaceand installed in both the REPL and batch paths (the ral binary has a durable stdout sink in every mode); exarch installs only its agent tools. Core keeps the host-agnostic primitives (spawn/await/race/cancel/poll); the line-framed spawn machinery andscheme::watchstay private, only theBuiltinEntrymoves (the one asymmetry). Withwatchadmission gone from the frame,DetachedPolicycollapsed to the bare per-host lifetime ceilingdetached_ceiling: Option<Duration>, andWatchAdmission/the runtime gate are removed. exarch genuinely lackswatch— absent from its builtin table,help, and system prompt — so naming it is an ordinary unknown command (a shell defers to external-command exec → command not found at runtime), not the compile-time diagnostic the proposal first claimed. Revises only thewatch-admission mechanism of concurrency-detached-vs-structured; the detached-root model, death-clock, reaper, andforget’s deletion stand. -
superseded — long-running-work — long work is born durable via a distinct exarch-registered verb into a listable durable-job registry, never a promoted
spawn; the open Regime 1/Regime 2 question and the cancel-by-id/pinning machinery are resolved by leases-and-budgets: Regime 1 ships as the durable lease class of a universal worker registry (verbservice), Regime 2 stays deferred. -
proposed — scheduled-wakeups — a cron-like wakeup is a timer that injects a synthetic user turn into the prompt queue, re-engaging the agent loop without a human; it schedules the agent, not a worker (the line that separates it from long-running-work, where a born-durable worker yields a value — here the payload is a prompt the model acts on, no ral code runs). Ephemeral and per-session: schedules live on the
Session, die on session end and/clear, and aforkdoes not inherit them (host state, likeexpect_action). The when is a cron expression — model-fluent, and the right surface for the calendar schedules a headless resident agent needs (“weekdays at 09:00”); plusafter <dur>for the one-shot relative delay cron cannot express. It reuses what is already compiled:jiff(timezone/DST next-occurrence, a hard transitive dep via the bundleddate→uu_date→jiff-icu) evaluates the expression; the five-field grammar is parsed in-tree rather than pulling achrono-based cron crate (a second datetime tree); the reaper fires it, its one action generalised from cancel-a-scope toCancel | Runso the wakeup rides the existing daemon (recurrence stays host-side, entries one-shot); thenudgesynthetic-prompt path delivers it. Delivery at the turn boundary (not mid-turn steering, which is user redirection); one pending wakeup per schedule (cron overlap-skip, also the suspend catch-up bound); a listable registry with cancel-by-id (theScheduleIdpin against agent-binding-reaping was since dissolved by leases-and-budgets — the registry is the authority,schedulesre-lists after compaction). The one genuinely new mechanism is a delivery seam: decomposing “something happens to the loop later” into(trigger, effect, target), cron and a future async worker share an effect+target — post a message, wake the loop — soPromptQueue(aVecDeque<String>) generalises into a typed per-session inbox (source + drain-boundary tags, the inbound twin of the outboundSignalstream) and the idle wait becomes a select over{input, inbox}; built once, for cron now and async delivery later. Two seams kept orthogonal by type: an event-trigger (a worker settling) is not a zero-delay timer entry, and a cancellation (control plane, read atcheck) is not anInboxMsg(data plane), per structural-bug-prevention; a shared channel is not a uniform drain policy. Self-scheduling gated behind aschedulegrant authority. Persistence and a durable cron are out of scope (future, paired with long-running-work’s registry). -
active — async-agent-tool —
agentis a launch-only, always-asynchronous orchestration edge: it forks a child, returns an opaque start receipt{id, title, status, log_dir}at once, and later delivers a typedAgentResultthrough the session inbox. Shipped shape diverges from the original bimodal proposal — there is nomode: "sync"dependency edge ormodefield at all (exarch/src/tools/agent.rs); every call is the orchestration edge, and a caller wanting an in-turn answer waits on the inbox delivery instead. The async path is an ephemeral, listable per-session registry (agents/agent_cancel) with request-local provider cancellation, explicit reaper ceiling, and/cleargeneration rejection, exactly as proposed. -
active — sandbox-external-children —
grantconfines external children under the effective sandbox instead of re-execing the grant body; bundled heads become exec images when process semantics are required, pipeline helpers stay, endpoint-shapednetleaves, and offline mode must fail closed where unsupported. -
active — tui-transcript-as-graphic — the scrollback is re-projected as an information graphic whose Bertin variables (shape, value, size, hue, grain) are encoded per-
Blockrather than buried in prose: the decorative❖rail becomes a 2-column marginal index (shape→kind, hue→agent, value→magnitude), the tab bar becomes a reorderable agents×steps matrix,rule_lineearns data-ink via actx%value-ramp and a phase Gantt ribbon, collapse becomes graded reduction. Phases 0–2 landed: the per-Blocksubstrate, the data-encoding rail (Move 1), andrule_line’s ramp+ribbon (Move 3); Phases 3–8 (size, grain, reduction, matrix, fidelity, projections) remain proposed. -
superseded — host-seam-turn-observer — drive both hosts’ turns through one core entry and make the structured surface
!Sendso the daemon-task hang becomes a compile error; superseded by run-turn-host-loop because!SendforcesShell: !Send, colliding with exarch’spump/Sessionmove. -
active — run-turn-host-loop — a turn is one synchronous, runtime-agnostic core entry
run_turn(src, TurnRequest) -> TurnReport;TurnRequestcarries policy (TurnIo, capabilities, limits, lifecycle, and a turn-localSurfaceSink). exarch owns the event loop and exits on an explicit completion fact, not event-channel disconnect (the invariant; as built this is a worker-setAtomicBoolpolled by a retainedpump/drivewith no tokio in the turn loop — the ADR’sselect!/oneshotsketch is the proposal shape, see its As-built note). The daemon hang dies because completion is a control-flow fact no detached worker can influence;ShellstaysSend, tokio stays out of core, same-thread children inherit the surface, detached workers get bounded once-only surface replay, and the bus remains presentation rather than liveness. Completes unify-turn-evaluation by making REPL, exarch, and batch request suppliers. -
active — run-turn-is-host-api — the public evaluation seam is one layer: hosts call
Shell::run_turn(src, TurnRequest) -> TurnReportand may nameTurnRequest,TurnIo,SurfaceSink/EventSink, lifecycle hooks,Captured,StaticDiagnostics, andTurnReport;TurnFrame,IoFrame, coreTurnOutcome, and publiceval_turncollapse.TurnIois host intent,Io/TurnStateare materialised resources, and capture/timeout classification live inrun_turnbeside the state that proves them. -
open — after-turn-api-simplifications — draft follow-on cleanup after the run-turn cutover: the common architectural error is turn-local facts leaking into long-lived or host-owned machinery (completion through presentation transport, surface as persistent cloned state, materialised frames as host API). The draft orders the next simplifications around enforcing that boundary: close old core exports first, move tests to
run_turn, shrink or fold exarch’s ral adapter, share the TUI/headless explicit-done driver, narrowShellhost accessors, and consider renaming exarch’s provider-levelTurnOutcome. Guardrails: keepSignal/Fact/Transient(theEvent/Kindnames are since dissolved), keep bytes and surface separate, keepset_stdoutuntil live-printer setup has an explicit replacement, and keep tokio out ofral_core. -
accepted — surface-carries-documents —
surfacecarries a render document — an ordered stack of Bertin marks the kit composes in ral — that one generic interpreter binds to visual variables, replacing the closed tag set (`patch/`wrote/`task/`meter) exarch decodes into a closedKindenum with a bespoke renderer each (five Rust sites per surfaceable thing). The set of cards becomes open (compose marks, zero Rust per card), the set of marks stays closed and small (so the renderer is total and reflow/disclosure/aggregation/events.jsonlsurvive). The discipline extends tui-transcript-as-graphic from chrome to content: the kit declares data and its level of measurement (quantitative → size/value/grain; nominal → hue/shape), exarch owns the binding, so magnitude can never land on hue. Five marks —text(qualitative, nominal-roled spans),measure(magnitude bar),fields(aligned matrix, subsumestask+provider_error),diff(the dense composite, subsumespatchwith aggregation + disclosure),raw(un-encoded bytes, the scoped “just print it” escape) — plus acardcontainer; composition is one rule at three scales (plane stacks marks,fieldsnests marks,textnests roles). Core untouched (already carries rawValue; detached replay free);TaskStatusand the four bespokelinebuilders retire;provider_errorfolds into the sharedfieldsrenderer. -
proposed — surface-reads-writes-execs — redirect reads/writes and external or bundled exec images surface at runtime doors as structural I/O events that exarch renders with the existing card marks. Bulk helper I/O (
grep-files,window-hash, and recommendededit-hash) moves below the ral line so plumbing does not leak onto the rail; events carry path/mode/argv/status/outcome, not file-size counts, and enforcement is a clippy-checked door set plus outcome-fused emit. -
active — handlers-and-aliases-are-lambdas — every per-name handler and alias must be a unary lambda
{ |args| … }and every catch-all a binary lambda{ |name args| … }; the calling convention is fixed by the surface position, not inferred from the value’s runtime shape, and arity is validated at install time (a bare block, a non-lambda, or a wrong-arity lambda is rejected).Nullaryis removed: a bare-block handler is no longer treated as a zero-argument handler. The rationale is structural — currying makes a binary lambda used as a unary handler return a partial-application closure rather than fault, a silent wrong result, so the bad state is made unconstructable at install rather than guarded at dispatch. -
fixed — terminal-lease — terminal-foreground authority is one session-owned
TerminalLeaseparked in core, with post-startupForegroundGuard::try_acquiredemanding&TerminalLease;TurnRequestseparates requested foreground policy (RequestedTerminalAccess) from byte input (TurnStdin), while internalTerminalAccess::ExplicitLoanis only a within-turn loan, so exarch tools areDenied + Empty, pipedral -ccan beDenied + Inherit, and_ed-tuiis an explicit terminal loan.JobControlwas narrowed to a process-groupLaunchRoleonce terminal authority moved to the lease. Landed in295fe5b. -
proposed — same-thread-body-shares-the-session — a same-thread thunk body — forcing a block or applying a lambda — must run in the caller’s
Shell, sharing the session store by identity, not in a freshShellwhoseSessionStateis default-constructed and then re-attached field by field. Today blocks evaluate in place (with_blockswaps only the mobile on the live shell) while lambdas build a child viawith_child→child_of→Shell::new(Default::default())+inherit_from— a hand-maintained allow-list with no totality check, whereShell::newactively re-mints the terminal lease from a blank predicate toNone, severing it from every function/alias/handler body (terminal-lease, fixed as a way-station). The semantics has no second store: CBPV elimination threads one ⟨M, ρ, σ⟩. The decision routes lambda elimination through the in-place mechanism blocks already use, parameterised by a small explicit fold-back set (last_statusalways,cwdfor a lambda); the owned-Shellconstruction (from_captured) stays only for genuinely separate runtimes — spawned workers, the cross-process helper, the REPL aside — which correctly default toDenied/no lease. Makes the forgotten-field severance unconstructable rather than guarded, per structural-bug-prevention; refines force-eliminates-blocks (the value-levelBlock/Lambdaelimination split is left intact). -
proposed — repl-as-structural-surface — the interactive shell is a projection of live program state, not a line editor over a transcript: a third
Frontend— a ratatui inline viewport whose scrollback stays the terminal’s — renders the three dimensions the runtime computes each turn and discards unless they fail, per-stage pipeline types as the line is composed, theletdependency graph as a re-flowable worksheet, and running handles and pgid jobs as a matrix, in the same graphic vocabulary as tui-transcript-as-graphic. The owned-block shell is rejected for reconstructing at the terminal layer what ral already knows at the language layer; the substrate extensions are small (per-stage types written by the annotation pass, retainedfree_refsedges, job-table access inread). -
active — session-lifetime-event-bus — an async
agentis muted only because the event bus is per-turn (pumpmints thechannel()in itsthread::scope); a detached child that outlives the turn cannot hold the turn’s sender, the same denial watch-repl-builtin makes. Minting the(tx, rx)once per session lets a background child streamBorn/Token/Diedto a live tab through the existing id-routed draw path — pure presentation, nothing the model sees changes (its reply still returns only as the deferred inboxTurn::Agent). Safe because run-turn-host-loop already made completion a control-flow fact (done), not a bus state: the foreground turn must end ondoneeven while the channel is non-empty with concurrent producers, and the{input, inbox}idle select (scheduled-wakeups) gains the bus as a third source so background tabs advance at rest. Worker lifetime/registry/generation/reaper-ceiling untouched;/clearages out live tabs by generation; TUI-only (headless keeps muting). Answers async-agent-tool’s deferred “lift the bus” open question; the settle breadcrumb is already one path viaAgentOutcome::breadcrumb, so this is only about live streaming. -
proposed — agent-reply-tool — the value a sub-agent hands its parent is the argument of an explicit, hard-terminating
replycall, not the prose of whatever step happened to end the run: the positional scrape — which handed a parent a 396-character sign-off and dropped the 3354-character brief that preceded a tool call — is severed with no fallback.replyis a model-level tool and peer ofagent, not a ral builtin, because finishing-and-returning is an agent-protocol act; it terminates only once every call in the batch has its result, so the exchange still endsReadyForUser(exchange-ends-ready). Its root withholding and its nudge-once-then-Emptyfinish are both revised by reply-terminates-returning-agents. -
active — deny-binding-path-commands — a name reachable on the effective
PATHresolves to that command in head position, so a top-levellet(or recursive definition) that would capture it is refused before its RHS runs; reachability is the pure filesystem questionShell::locate_commandanswers, independent of whether the active grant would admit running it. The guard is session-scope-only and deliberately narrow — nestedlets, lambda parameters, the prelude, builtins and coreutils all stay shadowable, only the outermost, least-owned namespace layer is protected — and dynamic by necessity, since PATH probing is I/O and the elaborator is pure. -
superseded in part — functions-and-handlers — there are functions and handlers and no third: a function has fixed arity and is applied positionally, a handler takes one argument — the argv packed as
List α, a catch-all also the dispatched name — and is installed scoped bywithinor persistently byhandle.helpsplits into the nullaryhelpand the unaryexplain, leaving fixed-arity exception-free. Its “every builtin is a function” resolves the other way in a-name-is-a-value-or-it-is-handled — a variadic entry is a host-installed handler at the base of the stack,echoamong them, rather than elaborator sugar — which is what makes the dichotomy exhaustive. “Alias” then names nothing distinct — it was only a handler’s persistent install form — and retires forhandle/unhandle, superseding the vocabulary but not the content of handlers-and-aliases-are-lambdas. The rename is the unfinished half:alias/unaliasare still the surface andinstall_aliasstill the API. -
proposed — surface-carries-control — the
surfacesink is the language→host typed-Valuechannel, not only presentation: beside the render classes (a kit`card, a coreioevent — both terminate in aCard) it now carries a control class,`spawn-started(carrying a liveValue::Handle), that exarch consumes to register the handle and arm an inbox-posting waiter — it renders nothing and cannot serialise toevents.jsonl, so the host dispatches surfaced values by class. The fulcrum: once one surfaced event draws nothing, “surface is presentation” is the meaning of one decoder arm, not the channel. This letsspawnnotify instead of being polled: the control event is surfaced in-turn (no foreground resource outlives the turn) and the detached worker’s closure is unchanged — so “detachment holds only root/handle-owned resources” (concurrency-detached-vs-structured, watch-repl-builtin) holds by construction; the completion rides the existing inbox asSpawnResult→Turn::Spawn, generation-gated likeAgentResult. Rejects both a secondEventSinkand giving the worker the foregroundEmitter(the unsafe variant, where “only call.inbox()” is mere discipline). Extends surface-carries-documents and surface-reads-writes-execs (render vs control, one level up from operation vs appearance); refines the poll idiom and the poll-instructing timeout text of concurrency-detached-vs-structured; needs one shell-free handle settle whose two-observer cache handoff is the sole concurrency risk. Answers part of session-lifetime-event-bus’s background-surfacing open question (control class only; the render class stays foreclosed). -
accepted — surface-pins-state — a rendered value is an event or state:
surface’s render class gains a disposition, append (event → scrollback, logged) or pin (state → a keyed register slot, overwritten in place, unlogged).`pin [key, body]writes a`cardto a session-lived register the focused session draws as a reserved right-hand column (the model-authored dual of the matrix);`unpindrops it. Oneemitarm, one viewport field, no new concurrency invariant — it reusesvalue_to_cardand is emitted in-turn. Turnstasks.ralfrom the encode-don’t-stream doctrine’s counterexample into its first client. The concept page is pins. -
proposed — sync-surface-async-notify — counter-proposal to surface-carries-control: there are exactly two language→host channels, split by the one property a value’s tag can never carry — lifetime.
surfaceis the sync channel (in-turn, alive, holds the terminal-lease, renders now);notifyis its async sibling (post-turn, deferred, rendered at the next boundary as a fresh turn). Both carry a typedValueand both dispatch by class, so a new event is a new decoder arm on whichever channel’s lifetime fits — never a new channel.spawn’s completion is the first async event: the detached worker emits a structural`spawn-donethrough its session-livednotifyat its existing settle point (tx.send), exarch’sInboxNotifypushes it onto the inbox the asyncagentalready uses, and it lands next turn as[spawn 'build' finished]. This deletes the sibling’s machinery — no non-rendering control class, no exarch waiter thread, no shell-free core settle, no two-observer cache handoff (deliver-once becomes a boundary-timejoined-flag check; the worker emits, it is never observed). Safe by construction: the worker holdsnotify(session-owned, the same class the asyncagentworker already holds), never the foregroundEmitter, andnotifycannot splice into sealed scrollback because it only ever lands at a boundary — the late-card hazard is a property of the delivery regime, not of holding a channel. Honours the one-channel instinct at the right grain (don’t proliferate pipes; dispatch by class), correcting only its collapse of the lifetime axis. The async value is data, not a live handle, soevents.jsonlneeds no special-casing. Refines concurrency-detached-vs-structured’s poll idiom (shared with the sibling); extends operation vs appearance (surface-reads-writes-execs) to sync vs async; the live-render question of session-lifetime-event-bus stays foreclosed (notifyis completion-only). -
accepted — recording-follows-the-event — what lands in a durable log is decided by what an event is, not by which thread emitted it: a per-session operational
transcript.jsonlsits besideevents.jsonland is fed at the oneEmitter::emitseam, so recording rides the emitter rather than the bus channel’s lifetime and a muted forked child still records its whole trace.Kind::DimbecomesKind::SystemNotebecause a vocabulary names a thing’s role and only the renderer names its appearance; ordinary operational notes leaveevents.jsonl, whose fold determines the model view while projection-neutral breadcrumbs remain; and the screen stops inventing events — a model switch emits through a recording emitter, view chrome (legend, clipboard, export, UI errors) draws straight to the viewport, and the “nothing to compact” no-op is dropped. Extends tui-transcript-as-graphic’s role-not-appearance discipline from the rail to the event vocabulary; context-is-a-projection names the superseding log/fold rule and the two-record unification debt, half paid by one-seam-one-log (the durable log unified; live display and the transcript still open) and paid in full by a-trace-is-a-fold, which deletestranscript.jsonloutright rather than folding it. -
amended — reply-terminates-returning-agents — the gate on
replyis “does this agent return”, not “sub-agent versus root”: the headless root does return, so it advertisesreplyon the sameinteractiveflag that already decides parking, while the conversing interactive root keeps it withheld — the old proxy read correctly only while sub-agents were the sole returning agents, and the headlessresultstill carried the positional scrape agent-reply-tool removed everywhere it reached.replybecomes mandatory: a no-reply finish is re-nudged within the existing budget and then fails honestly (never forcedtool_choice, never a scraped fragment that reads as an answer), and the payload is rendered to its consumer — prose for a model parent, a faithful value for the harness, so headlessresultis typedstring | objectrather than double-encoding structure into a string. -
superseded — non-final-bytes-are-effects — at a value boundary — a
let, a forced block, atryoutcome — the bound value is the value of the boundary’s final computation:eval_seqflushes each non-final element’s bytes to the visible outer stream as effects, so only a final computation that is byte-output with aUnitvalue has its bytes for a value, decoded as aStringwith one trailing newline stripped. Capture-everything is rejected for conflating effect with value (it discardslength’s answer to keepecho’s line) and for needing a flag that reads whether its binder was user-named. The checker computes the same rule through afinal_outputsmap distinct frombind_outputs— a node’s effect output is not its value byte-source — so a binding’s static type is the value the evaluator produces. Superseded because its statement was cast inoutputmodes that no longer exist; the boundary rule itself — final computation wins, non-final writes are effects — is exactly theρ = Bytes ⇒ Unitvalue-boundary reading of pipes-are-positional-byte-wires. -
active — shared-transport — the tokio runtime and genai clients belong to the fleet, not to each
Provider: anEngine(runtime,cache_key, atransports: Mutex<HashMap<TransportKey, Arc<Transport>>>keyed by credential+adapter) is built once (Engine::new) and hung off theFleetasArc<Engine>, whileProvidershrinks to a cheap per-agent selection (engine handle + id + model + tuning) that resolves its transport from the shared map instead of callingmake_runtime()on every/modelswitch. Concurrency is already proven — sibling peers already ran detached against their ownArc<Provider>, andruntime.block_oncan be invoked from many threads at once. The banner/ctx%chrome now reads the focused agent’s liveprovider().current()instead of a frozenSessionInfo, so a/modelswitch and a subsequent/clearcannot disagree;SessionInfokeeps only its static fields. Landed as proposed, including theBackend::Scriptedno-runtime test seam (realised in place of the sketchedEngine::Scripted). Since 2026-08-17: the id aTransportKeycarries is anAccountId, and theflat_rateflag isService::billing, the one authority on metering. -
proposed — agent-binding-reaping — exarch leases scratch bindings per
Agentshell, not per fleet: ral/REPL bindings remain ordinary lexical state, while an optional ral-tool-call epoch lets core renew and prune top-level scratch at ready boundaries. Lease records live onShell::local, generation guards require one lease-aware top-level write door, accepted source turns harvest static read/write sets, running handles recursively pin any top-level value that reaches them, settled handles are scratch, and exarch must refreshAgent::durableimmediately after a committed prune so panic recovery cannot resurrect deleted names. leases-and-budgets answers its host-pins question: durable jobs need none — the worker registry retains the handle itself. -
superseded — long-session-resource-budgets — a days-long exarch run is bounded by heap, queues, shell values, and logs, not by model compaction; proposed per-accumulator budgets (bounded bus, windowed viewports, inbox quotas without silent loss, physical post-compaction reclamation,
/resources). Carried forward whole into leases-and-budgets, which adds the probe convention, the worker registry as accounting spine, and a per-agent admission cap. -
proposed — provider-heartbeats-and-retry-boundaries — exarch judges provider liveness by raw wire progress, not by semantic model output: Anthropic
pingevents become heartbeats, long-thinking models such asclaude-fable-5andclaude-sonnet-5may remain semantically quiet without tripping a decoded-event timeout, raw silence remains retryable, explicit wall-clock budgets stay separate, and exhausted provider failures surface as provider errors rather than synthetic model-visible nudges. Partial streamed work still commits and continues through truncation recovery. -
active — partial-poll-pending-output —
poll $hon a still-running handle now returns`pending{stdout, stderr}— the bytes written so far — instead of aUnitpayload, cloned non-destructively from the live buffers via a newpeek_buffer(the peer oftake_buffer). Chosen cumulative (a growing prefix), not a drain-on-poll delta: draining would reintroduce the peek-vs-drain split the settle decision closed and break theCompletedHandlecache, so the completiontake_bufferstays the sole place bytes leave a buffer. The cost is a deliberate reversal — pending polls are non-idempotent (monotone growth), so 260615’s “repeated observations are consistent” is re-scoped to settled observations only. Watched handles buffer nothing and report empty; the 16 MiB cap still bounds a chatty server. Gives exarch a headless, pull-based read of a running worker — the counterpart to REPL-only watch. -
fixed — windows-spawn-boundary — Windows pipeline launch gets a custom
CreateProcessWlayer: helper protocol handles cross by explicit handle list, not parent-global inheritable bits, and pipeline children enter their Job Object before user code can run, via a job-list attribute or suspended-create/assign/resume. This closes the report/value/gate handle leak race and the direct-external early-fork escape without making helper routing a safety crutch. -
active — subagent-memory-modes — sub-agent spawning splits into two model-memory contracts:
amnemonis tabula rasa, whilemnemonimports the parent’s model-visible context, reuses the parent’s provider selection for cache locality, and appends the tool call’spromptas the fresh final user prompt. Both keep the same shell snapshot, permission meet, detacheddrive, and inbox return path;AgentLogdrops any unanswered parent tool-call frame before importing context so the child never inherits a dangling protocol. -
active — spawn-fuel-ceiling — every
Agentcarriesfuel: u32; the trunk starts atSPAWN_FUEL = 3and eachforkspends one unit on the child. A newGate::Spawnsaxis withholdsamnemon/mnemon/commit/verify_commitmentoncefuelreaches zero, so a delegation chain terminates by tool absence rather than recursing forever — the same silent-gating shapereply/Schedulesalready use, not a dispatch-time refusal. Refines uniform-agent-nodes’s unbounded-depth claim: fuel is a pure function of tree position, so no agent is privileged by special-case code. -
superseded — protected-commitment-pins —
commitment:*is a protected pin prefix: ordinarysurfacewrites/unpins to it are rejected, and a live commitment pin rides the same one uniform pinned-state nudge every other pin kind does — budget-free, for every actionable agent regardless of role, additive with a returning agent’s separatereplyobligation, but quiet while a verifier child is still running.commitaccepts a key and a free-text description and launches anamnemonwriter, opening the pin only on a matching structured card with at least one criterion;verify_commitmentaccepts only the key and launches anamnemonverifier, clearing the pin only on a matching pass verdict — both launch-only and always-asynchronous likeamnemon/mnemon, settling on the host’s own thread;/clearstill clears them as part of the session reset. Superseded by names-and-schedule-labels, which deletes the feature whole. -
active — exec-projection-defers-to-gate — the OS exec projection’s admit decision is the in-process gate’s own verdict, queried once per nameable command, not a second derivation of it: the two folds of exec-authority-partitioned stay two, but the projection had been intersecting literals with literals and dirs with dirs, losing every admission that crosses shapes — a literal
gitunder a layer granting/usr/bin/— so Seatbelt denied a spawn ral had already run.admitted_literal_pathsnow draws candidates from the raw union of literal keys and keeps only whatevaluate_execadmits; a baregit: Denyprojects as a final-path-component regex rather than one PATH-resolved literal, so the OS layer enforces the basename veto too.Capabilities::meet’s subject-free pre-mash stays the one approximate surface, fail-closed, with a differential conservatism test asserting the projection never admits a path the gate denies. -
active — per-agent-eval-cancel — cancellation reaches the eval layer: only the signal-facing session publishes the process-global signal slots (
SessionState::publishes_signal_slots;fork_sessionclears it), restoring the slots’ single-thread LIFO discipline and closing a cross-session mistarget (the accompanying use-after-free claim is corrected by cancel-slot-leak: one publisher already suffices to hit it); and the registry cascade cancels each parented agent’s ownDurableRoot(Shell::cancel_handle, carried aseval_rooton the entry) alongside itsToken, so a cancelled agent’s in-flightraleval unwinds at the evaluator’s poll points (~100 ms) instead of grinding to itstimeout_secswall. The trunk’s entry carries an interrupt-only reach (eval_root: None, viaEvalReach::interrupt_only), so a registryterminateon it cannot poison the session; its turn cancel also rides the ambient foreground cause (cancel-is-a-join, which dissolves the one-publishing-session rule into how a scope is minted). -
active — cancel-per-tab — Esc and Ctrl-C unwind only the focused tab’s current turn: they never cascade to a subtree and never end an agent, so lifecycle death stays with
/quit,/clear, the reaper ceiling, andagent-cancel, which keep cascading. The drive-loopTokencarries aCancelCauseand is read two-valuedly at the park —is_cancelled(), true for any cause, still drops the in-flight turn, while the newterminated(), true for any cause butInterrupt, is what ends a non-Heldagent — so an interrupted parked sub-agent re-parks instead of dying, and an interrupt cannot orphan because it never removes or settles an entry. Generalises esc-non-escalating-interrupt from the oneHeldnode to every tab through a single-entryAgentRegistry::interruptwith no descendant walk — the trunk included, alongside its ambient-pathraise_interrupt. -
active — branch-minimal — a branch is an ordinary parented registry child that converses:
/branch [prompt]forks the trunk’s conversation with mnemon inheritance and the trunk’s capabilities verbatim, but withholdsreply, and conversing is derived from the tool view —returns()reads whether the agent holdsreply, never its position — so parking, the reply-nudge, and the advertised tools cannot disagree (agents). One concession buys the whole minimal cut: a trunk/clearclears branches too, so a reaped entry reads!is_liveand quiesces instead of parkingHeldon a dead entry, and the hour ceiling is registered off because a human-typed turn is not the model recursion it bounds. The settle epilogue is empty for a non-returning child, so no branch death ever posts anAgentResultinto the trunk’s context; surviving the trunk’s/clearis given up deliberately, and/closeis the one command admitted off the trunk. -
active — session-ledger — the unifying frame over leases-and-budgets: everything alive between turns is a resident with four facets — identity in the ownership tree, a typed capability (
Handle, pgid job spec,AgentId, schedule id, top-level name), a lease, a probe — and the session keeps one ledger in five chapters (workers, agents, stopped jobs, schedules, bindings) whose management surfaces are folds written once: list, exit warn-then-sweep, cancellation cascade,/cleargeneration,/resourcesprobe. Lifetime moves on a graded partial order of residency (foreground → stopped → background → durable → survives-exit); leases push down, verbs move up; the REPL’s job control is the discovery traversal (Ctrl-Z/bg/fg/disown—bgis promotion,disownis Regime 2’s shipping interactive ancestor) while agent work declares its grade at birth — dissolving birth-vs-promote into two disciplines of one order. Splices job control at the listing layer only: REPLjobsfolds over stopped groups and detached handles (healing the&wart),fg/bgstay pgid-typed,awaitis the handle’sfg; deep fusion (aStoppedHandleState, terminal semantics inawait) is refused as two implementations behind one name. Accumulators (viewports, bus, inboxes) stay probe-only: no capability, no listing. Graduates to adesign/residencypage once accepted. -
active — signals-are-causes — closes core-audit #3 (signals can’t preempt a blocked standalone external; SIGTERM never cancels) by deleting the parallel delivery mechanism instead of patching it: the platform handlers translate each delivered signal into a
CancelCauseon the published cancel slots — SIGINT → foregroundInterrupt, SIGTERM/SIGHUP → rootTerminate(new cause, message “terminated”, exit 143, SIGTERM-first teardown) —process::checkpolls only the scope tree, andSIGNAL_COUNTis demoted to the escalation ladder (ESCALATION: third delivery_exits;interrupt()/is_interrupted()deleted).RunningChild::waitloses itspark_on_stopblocking bypass — parking is a stop classification, every external wait is one cancel-aware poll loop — so SIGTERM now preempts even an interactive foreground external; the REPL loop observes a sticky root cancel at the prompt boundary and exits with its code (also un-bricks Ctrl-\). Rejects the audit’s self-pipe sketch (the poll loop was never blocked) and boot-time root-slot publication (the slots’ LIFO discipline) — the latter dissolved, and the idle-SIGTERM residual closed, by cancel-is-a-join, which replaces the slot substrate. -
superseded — session-scoped-appcontainer — the Windows OS sandbox as one AppContainer profile per shell session, imitating MXC Tier 3 (0e7c3dd) with permanent provenance breadcrumbs; its union-of-projections consequence was judged unsafe for within-session attenuation.
-
superseded — projection-keyed-appcontainer — the Windows OS sandbox mints one AppContainer SID per distinct fs projection (bind_spec identity; profile names pid+counter, never content hash), so a child’s kernel-checked authority is exactly its own declared projection — narrowed grants and subagent permissions hold at the OS layer; same-projection commands share one SID and its stamps, profile registrations are ledgered before the OS create, and ACEs revert at session teardown, not frame exit.
-
superseded — ace-free-fs-confinement — the ported DACL tier stamps an inheritable ACE per fs prefix and
SetNamedSecurityInfoWpropagates it to every existing descendant, so confining one command under a grant overcwd:is O(files under cwd) — 120 s+ on a repo with atarget/(48k files), symmetric on teardown. The cost is inherent to ACL-confining an existing tree; excluding subtrees is whack-a-mole. Records the exact findings and the three MXC tiers with on-host availability (T1 BaseContainer feature OFF; T2 BFS present but the tier MXC ships disabled; T3 DACL the pathology). Decision deferred; leading candidate is a tiered detector, BFS-preferred, spike-gated, with a reduced-authority fallback. -
proposed — vm-workspaces-cross-by-copy — an exarch VM receives a private ext4 workspace through a bounded, content-addressed bulk plane beside the ral control seam; no host directory or NIC enters the guest, turn-boundary deltas land first in immutable private history, and only explicit witnessed publication changes the granted tree, while ral’s in-process gate and per-spawn OS projection preserve narrower grants inside the VM.
-
active — agent-names-and-schedule-labels — the exarch agent surface collapses to one record-spec verb,
agent [prompt, name, type: `amnemon|`mnemon, grant]→[name: Str, log-dir: Str]: the closed record row makes a missing/misspelled field a static error naming it, while the opentype/grantvariant rows defer to runtime doors that enumerate the legal tags. An agent’s model-facing identity becomes its name (fleet-unique among live agents — the desk’s cheap didactic pre-check plus the race-freeAgentRegistry::registerNameTaken) and a schedule’s its label (scheduleanswers[label, next-s],unschedule <label>; thesched-<n>default this decision minted was retired by harness-calls-are-acts’s amendment, which made the label mandatory); numeric ids leave the model surface entirely (message/agent-cancelresolve by name, closing the silent cross-family id no-op anunschedule <agent-id>once was), while internalAgentIdplumbing stays.amnemon/mnemonsurvive only as thetypefield’s two memory modes. The protected-commitment feature is retired whole — thecommit/verify-commitmentbuiltins, thecommit-open/commit-verifydesk arms,CommitmentIntent/CommitmentSettle, thecommitment:*projection, andPinKind— leaving the pin register as the plain digest mirror plus the host-owned, write-protectedservicesledger pin. Records: record specs give static field diagnostics and an extensible surface (future per-child budgets ride as new fields); names survive context compaction and read in prose; the schedule receipt’snext-scatches a mis-meant cron at arm time; commitments did not earn their machinery. Supersedes protected-commitment-pins; amends subagent-memory-modes (verb → field) and agent-tool-to-exarch-builtin (the class inventory); async-agent-tool, spawn-fuel-ceiling, and the engine protocol’s enquiry channel stand unchanged. Amended 2026-08-27: theservicesledger pin’s write protection recorded here is removed — killed outright, on the operator’s own judgment alone — leaving the pin register entirely model-authored; durable-service legibility falls back to the ordinary worker-birth trail card and/resources’ aggregate count, with no replacement pin. -
active — harness-calls-are-acts — an act changes the world outside the turn and an observation does not, so a spawn, a message, a schedule, or a
replycannot wear the block aralcall mints: an act block answersfalsetoobservation()and so renders standalone under the barrier rule of tui-transcript-as-graphic instead of folding into a run of reads, takes two rail shapes —↗for fleet acts, the outbound twin of the existing↘, and◷for time acts — and a three-column verb · subject · payload row with the verb pinned to a constant width, replacing six host-authored sentences whose whole content was those three facts. The magnitude bar goes, having ranked nothing (a desk result is one line, so every act stamped1); the subject reaches the bus as its own field rather than baked into prose; failure is a tier on the act row, since a refused act is still an act attempted; and a refusal raised before the act — everyagentspawn guard — draws nothing at all, because a spawn that never happened is not an event. Since amended: the desk’s recording unified onto onesubjectfield feeding both the rail row and the audit sentence, whichschedule’s mintedsched-<n>default could disagree with; the label is now mandatory, so the two readers never diverge. -
active — total-wait-status — Unix wait results use rustix’s transparent, total
WaitStatusthrough distinct pid/pgid and blocking/polling funnels; the doors ownEINTRretry andNOHANGoptionality,ECHILDremains an error,Pgidadmits only positive identifiers, and neither negative-pid encoding nor fallible enum decode reaches lifecycle code. -
active — synod-is-a-second-product — synod is its own crate and binary depending on exarch as a library, not a fork and not a
--profileinside it: it owns a folder grant, an office persona, and its session assembly, and borrows the provider layer, the turn driver, the card bus,Scratch, and the prompt renderer. A sharedagent-coreis refused as speculative surgery on a guessed boundary (extract it when a third product supplies evidence); a flag is refused because a product is not a flag — two audiences’ conditionals in one turn loop, and neither release can decline the other’s half-built features. The price is threepubpromotions in exarch (prompt::render,prompt::host_section,Agent::root), now a reuse boundary under maintenance obligation, withhost_section— a developer’s git-and-cwd snapshot — the one expected to be withdrawn first. -
active — survives-exit-is-its-own-verb —
serviceis durable within a session and cannot be made durable beyond one: the worker’s external child issetsid’d but its pgid is recorded by the parent (core/src/process/signal/unix.rs:365-371, stored atchild.rs:180) and signalled directly at teardown, so leaving the session severs only the tty and buys no lifetime. Empirically forced by terminal-bench2026-07-25__02-04-52, where exarch’s only two zeros are the two tasks needing a live listener at grade time —kv-store-grpcrefused connections (errno 111) ~2 s after exarch exited, having served RPCs seconds before; the same model under a bash harness kept its server alive withnohupand, on that task, produced a worse artifact, so exarch lost the process it had correctly built rather than the reasoning. Revives Regime 2 from long-running-work — now that its “only if a concrete need appears” condition is met — asdetach, a distinct verb, never a mode ofserviceand never a knob (two handle types, two observability surfaces, no shared code), born by double-fork so the survivor’s pgid is never observed byRunningChild, with all three standard descriptors on/dev/nulland no file written anywhere — the receipt is{pid, desc}and the survivor is mute, so the only way to learn whether it lives is to probe what it serves: the competing escape (registering outside theDurableRootcancel scope) defeats the signal but leaves a pipe whose read end closes at exit, killing anything that logs while passing tests on servers that stay quiet. NoHandle, since a surviving process is not a ral thread and shared eliminators meaning different things would be a worse lie than the doc bug — which is also what earns the name, under the test this page adopts: a verb is earned when the type changes, not when the policy changes. By that test the converse collapse (watch/serviceintospawnoptions) is rejected, because watch-repl-builtin wants a host to lack an affordance rather than veto it, and options cannot be absent — only vetoed;docs/SPEC.md:1741’s “par,spawn,watch, andserviceall produce the same kind ofHandle” is the diagnosis, but the defect it names is that the verbs don’t say which axis they vary (output forwatch, time forservice, ownership fordetach), not that there are too many.detachoverdaemonbecause it names the act rather than a kind of program. Records two further findings: the kill that ends a service today is a footrace between the worker’s ≤100 ms poll (child.rs:395-396,:430) and an exiting main thread that never blocks for it, sodocs/SPEC.md:1907’s third clause is true by accident and not stable across machines; and exarch’s self-verification is structurally blind here — every probe it can make is on the wrong side of the boundary that kills the server, so no diligence closes the gap.exarch/data/ral.md:193(“work that is meant to run indefinitely”) is wrong and corrected in terms of consequence independently of anything else; a synchronous pgid-ledger shutdown sweep (the shape atral/src/jobs.rs:308-346) is deferred as the race’s complement, not its substitute. Sandbox interaction was left open here and is settled the other way by detach-under-a-grant:--die-with-parentis a flag this repo passes rather than a property of confinement, so theengages_sandboxgate is gone, a survivor is confined for life by the frame that bore it, and the authority is thedetach:dimension this page guessed at. -
active — windows-hyper-v-backend — synod’s Windows machine is Hyper-V created directly through the Host Compute System API (
computecore.dll, the WSL 2 / Linux-container surface), described by one JSON document whose every part is chosen so the guest cannot tell which hypervisor booted it:Chipset.LinuxKernelDirect, SCSI-attached disks, a host-servedDevices.Plan9share of the granted folder, oneAF_HYPERVsocket, a COM-port console, and no network adapter at all. Brokering through the WSL service is rejected outright — it needs no privilege but puts the agent in a shared utility VM with/mnt/candbinfmt_miscWindows interop, which is the negation of “one folder and nothing else”; §2’s WMI fallback went unbuilt. Amendsdev/docs/VM/SYNOD.md§2 in two rows, both corrections toward less ceremony: direct kernel boot instead of Gen-2 UEFI with a unified kernel image (no bootloader, no ESP, no boot disk to keep in step), and a fixed VHD wrapped on first launch instead of VHDX at install time (sectors verbatim + one 512-byte footer, so wrapping is an append, not a converter’s worth of code for snapshots and resize synod never uses). Narrows §2’s portability argument: both backends share the folder live — virtiofs on macOS, 9p2000.L on Windows, the mechanism WSL itself uses for/mnt/c— because the guarantee §4 was buying is host-side and transport-independent (checkpoint, content-addressed history, change report, conflict-checked put-back), so the workspace machinery is unchanged. HCS entry points areLoadLibraryW’d rather than statically imported, so a Windows without the Virtual Machine Platform feature gets a sentence instead of a process that will not start; the socket’s descriptor names SYSTEM, built-in Administrators, and this user’s SID, never a wildcard. Deployment consequence, since amended: HCS serves only administrators and members of the local Hyper-V Administrators group, empty by default, so whatever process creates the machine must be one of the two — checked before a folder is granted, never mid-session; windows-machine-broker moves that requirement off the user and onto a service. Makes the engine protocol platform-neutral (WireStreamisUnixStream/TcpStreamas std’s owner of a connected socket, no claim about the address family) so synod’scontrol_seatloses its last#[cfg]. Open: the guest’s own boot is not yet verified (a machine now creates and starts), and whether the host’s 9p server can read the granted folder without an explicit access grant is untested —HcsGrantVmAccessis deliberately not called on the user’s folder. -
active — windows-machine-broker — synod must install from an ordinary
.msiand then run with no permission its user did not already have, so the privilege Hyper-V demands moves out of the application and into aLocalSystemservice the installer registers (SynodMachineBroker,vm-manager/src/broker/,synod/wix/broker-service.wxs): the window asks over\\.\pipe\synod-machine-broker, the service creates the machine. Joining users to Hyper-V Administrators is rejected for a specific reason — that group may attach a physical disk, and a guest reading a raw disk reads past every NTFS permission, so the remedy would install a local privilege escalation in order to run an application whose whole claim is that it sees one folder; brokering through WSL’s own service stays rejected on the guest’s topology (windows-hyper-v-backend), which no saved privilege buys back. The shape is WSL’s, Docker’s, and VirtualBox’s. What makes it safe is the narrowness of what it accepts: one instruction (boot a machine over this folder), with media, devices, cache, and resources all constructed by the service from its own installed state — so if a request field ever reaches HCS without passing a check inservice.rs, the argument stops being true. Two decisions carry the weight: the folder is checked by impersonating the pipe’s client (ImpersonateNamedPipeClient) and opening it as them, since aLocalSystemservice checking as itself could read everything and would mount one user’s documents into another’s guest; and the control socket crosses byWSADuplicateSocketWaimed atGetNamedPipeClientProcessId’s answer, never the client’s word for its own pid. TheBoot→Booted→Adoptedhandshake exists because closing the broker’s own socket handle early races the duplication while never closing it means the guest never sees the EOF a closing client should cause, so the inside-out power-off never starts. The connection is the lease: a machine lives exactly as long as the pipe connection that asked for it, held in the serving thread, so a dead client takes its machine with it and there is no table to keep honest.detectprefers the broker and needs no boot media from the application at all, falling back to in-process creation only in a checkout. Consequence: a privileged service is part of what synod ships, and it is the thing to review hardest. -
active — guest-namespace-prefixes — a grant prefix is folded by the rule of the namespace that will match it, so synod’s guest paths are minted through a POSIX kernel (
lex::fold_dots_posix,NormalizedPrefix::from_guest) rather than the host’s: capability-freeze’s one-kernel promise is really one kernel per namespace, on both sides of a match, and a host that folds withPath::componentsrebuilt/workas\workon Windows — a relative path in the namespace it claimed to name — so the gate inside the guest denied the agent the only folder it had (fs read: \work, \tmpagainstfs read denied by grant: /work, which the agent diagnosed off its own prompt).fold_dotsis deliberately not changed: its separator reconstruction is correct for a host path andis_foreign_rooteddepends on it; the fault was applying a host kernel to a guest path, one field over from whereMachineSpec::resolvehad already moved absoluteness into the guest’s namespace (starts_with('/'), neverPath::is_absolute). Constraint recorded on the new door: such a prefix must not be reduced on the host, sinceFsPolicy::meetre-mints throughPrefixSet::surfaceand would fold it straight back — unreachable in synod, whose trunk runsfuel: 0, and correct inside the machine where a nestedgrantis reduced by the right kernel. The instructive half is why the tests were blind:the_policy_admits_the_guest_namespace_and_denies_the_host_oneruns the real grant through ral’s real gate but runs it on the host, so both sides folded wrongly in the same direction andpath_withinis separator-insensitive under Windows path identity regardless — a host-side simulation of a guest-side gate cannot see a namespace split, so the new tests assert on bytes, with a#[cfg(unix)]test pinning the two kernels to one law where one machine can see both. Audited at the same time and correct:cwd/homecross unfolded throughFrame::Attach,guest_pathis never joined on the host,deny_pathsandexec.dirsare empty. Found by running the installed product, not by CI. -
superseded — cancel-slot-leak — the signal-reachable cancel slots publish a borrowed pointer into a run’s cancel flag, and
requestloads the slot then dereferences it; a process-directed signal lands on an arbitrary unblocked thread, so those two instants can straddle the scope’s death — a use-after-free reachable from a handler, needing only one publisher, since the second party to the race is the signal. The old SAFETY note (“the guard restores the prior pointer before the scope can drop”) andRunGuard’s field-order argument are both same-thread claims about publication, silent about the handler that already holds the pointer in a register; the one-publishing-session rule is likewise a delivery invariant, not a safety one, and production runs two publishing sessions anyway (the REPL’s hook shell beside the main session).publishnow leaks one strong share of the scope’sArc— 32 bytes per publishing run — making every published flag immortal, the same move exarch’sTokenslot already makes; the stale-cause symptom (a freed byte re-read as a spuriouscancelled/130) goes with it. This closes the memory-safety hole, not the design: two process-lifetime flags drained by the run door remain live, justified not by the dropped-signal window but by deleting the pointer and its bookkeeping outright, with an epoch-tagged slab and an inverted publication also open. Measured evidence that concurrent publishers do real damage: unconditional test publication raises spuriouscancelledin the parked enquiry two runs in three, and unserialised publishers make an engine cancel miss its run and wait out a 20 s ceiling. -
active — cancel-is-a-join — cancellation is a join-semilattice (
CancelCausetotally ordered,cancelafetch_max, a scope’s cancellation the join over its chain), so a signal handler holding no scope should contribute an element, not alias one: two process-lifetimeAtomicU8cells (REQUESTED_FOREGROUND,REQUESTED_ROOT) carry the handler’s cause and a scope folds a cell iff it was minted facing it (ScopeNode::hears, immutable). This deletes the whole apparatus the aliased pointer required —CancelSlotand itsDrop,publish*, the dereferencingrequest, bothAtomicPtrstatics, everyunsafeincancel.rs,foreground_cancel_cause,SessionState::publishes_signal_slots, theRunGuardslot fields and drop-order argument, and cancel-slot-leak’s leak — and retires the delivery failures it measured (a spuriouscancelled/130 in the parked enquiry; an engine cancel waiting out its 20 s ceiling). Routing is by minting, not by a session flag (spawn_threadbuilds workers from a freshSessionState, so a boolean was never the discriminator):DurableRoot::signal_facingfolds the root cell,::foregroundfolds whichever of the interrupt cell its root does not already fold,::workerfolds neither directly — so a detached worker hears SIGTERM through its parent and cannot absorb a Ctrl-C, by the shape of its fold.Shell::newmints deaf; each primary host boot calls oneShell::face_signals;fork_sessionis deaf by construction. One privatefold, withScopeNode, its flag, thehearsbits and both cells private tocancel.rs, is the structural enforcement bought.REQUESTED_ROOTis never spent — closing signals-are-causes’s idle-SIGTERM residual — andREQUESTED_FOREGROUNDis spent at a top-level run entry, an affine half cancel-is-a-watermark then dissolves. Accepts one semantic change: a shared element is sharing, not shadowing, so a Ctrl-C during a nested run unwinds the whole nest, as a POSIX shell’s does.EnquiryDesk::enquiretakes the run’s&CancelScope, so a parked enquiry also sees reaper deadlines and cancelled handles. exarch’s per-exchangeTokenslot is the same alias pattern, left for the same cure. -
active — cancel-is-a-watermark — “a cause raised for a settled run must not unwind the next one” is a claim about time, which the spend made destructively — and zeroing shared state needs a unique zeroer, whence the whole authority apparatus. Re-index by time instead:
CLOCK: AtomicU64ticks once per raised interrupt,STAMPED[cause]records the instant it was last raised at, a foreground frame records its birth instant at mint, and it observes⨆{ c : STAMPED[c] > birth }. The two ambient causes become typed rather than procedurally distinguished — shutdown is absolute (a plain lattice element, true for every observer forever), an interrupt is temporal (true relative to a birth date, a Kripke/presheaf reading) — andScopeNode::hearsbecomes a three-way sum,Nothing | Shutdown | InterruptsSince(u64). With no reset there is no spender:REQUESTED_FOREGROUND,spend_foreground_request,faces_foreground,SessionState::fronts_foreground, theRunGuardgate, andoverhearing/overhear_signalsare all deleted rather than relocated, and the handler stays async-signal-safe at two lock-free RMWs. One stamp per cause, not one packed word: a frame reads a suffix of the escalation order, so instant-major loses an old strong cause to a young weak one and cause-major hides a young weak one from a frame born between them. Forces one repair that closes a latent hole: the run door mints each entry as a child of the frame it displaces rather than a sibling under the root, so the cancel tree finally is the dynamic extentRunGuard’s LIFO already described — a nested run observes its outer run’s interrupt by ancestry, and an outer run’s wall now reaches into the nest, which it never did. The aside needs no constructor of its own: the REPL’s hook shell shares the session’sDurableRoot(Shell::join_session, closing acancel_handlereachability hole), and hear-without-spend stops being a category, since an interrupt older than every frame the aside mints is simply unreadable from it. -
superseded — the-guest-gets-a-network-not-a-verb — the single
fetch-urlverb that was the guest’s whole egress surface is retired outright for a real network: atunwhose only peer isguest-net, a user-mode TCP/IP stack in a host process, policed by four gates (DNS, TCP accept-by-minted-address, an intercepting proxy on 80/443, refusal by absence) rather than a per-protocol enquiry. Rejects the macOS-only hypervisor frame tap (no Windows equivalent this cheap), the HDV device model on Windows (declined on theHdvCreateGuestMemoryApertureseam, not availability),CONNECTwithout interception (loses precisely because synod ships to arbitrary machines with no IT department curating a tight allowlist), and per-domain consent cards (trains “always allow”). Host-mode exarch loses its web door; the response-size and rate caps were resized, not just renamed, for a guest that runs real installs rather than one enquiry at a time; the audit ledger grew a discriminant per gate;git cloneis off the shipped read-only default; the plain-English jargon guard moved from the retired verb’s refusal text toguest_net::refusal::Refusal’s. The engine protocol’s enquiry channel still carries the agent, schedule, and reply families, untouched by this decision. Open: the jail-vs-install collision (pip3 --useras the one install path a fresh-UID jail admits), the 240/minute rate cap being sized off onepip installand not a measurement, how much of a logged request path a review surface should ever truncate, and thatreqwest’s blocking client has noread_timeoutto bound a stalled-but-open transfer. -
active — one-connect-door-not-four-gates — egress narrows to a destination policy: the guest may open TCP connections to port 443 of the public addresses these exact hostnames resolve to, once, on the host, and to no other destination. The four gates above collapse to one explicit
CONNECT-only proxy that reads at most 8 KiB of head, refuses@in the raw target before parsing it, parses anhttp::uri::Authorityrejecting IP literals and every port but 443, checks the lowercased name againstNetPolicy’s exacthostslist, resolves it once, discards every non-public address, dials and pins the vettedSocketAddrs, then copies bytes unparsed. Rejects keeping the intercepting proxy — its session CA,rcgen,rustls,rustls-platform-verifierandreqwestbought a method-level narrowing already undermined by shared CDN edges — normalising wildcard/IDNA hostnames now, and a private-network escape hatch in the address classifier.read/write,max-bytes, andrate-per-minuteare hard errors; the once-per-name blocked card retires with the interception it depended on, leaving the audit ledger’s singleTunnelrecord and an optional pre-tunnel HTTP error as the remaining channels — named as a decision, not an omission. No session CA is minted; the fixed live-tunnel cap is an implementation limit, not policy. Does not reverse the-guest-gets-a-network-not-a-verb’s core claim that the guest reaches the network itself rather than a bespoke verb, only its four-gate account of what makes that safe. Open: wildcard/IDNA hostnames, and that a shared CDN edge can still carry more than one name behind an allowed tunnel. -
active — detach-under-a-grant — closes the sandbox question survives-exit-is-its-own-verb left open, and closes it the other way:
detachunder confinement was never impossible, it was blocked by a flag this repo passes. bwrap’s--die-with-parent(core/src/sandbox/linux.rs) isPR_SET_PDEATHSIG(SIGKILL)over the envelope, and against a double fork it is indeterminate rather than fatal — whether it fires at all is a race between bwrap’sprctland the intermediate’s_exit(0), so the survivor is either killed moments after birth or never tied to us at all. Nothing else about the envelope is a relationship with a parent: mount ns, net ns and seccomp are entered atexecveand belong to the process, whichonly_the_parent_death_tie_distinguishes_a_surrendered_launchasserts by diffing the two argvs; and macOS never had the problem at all, sincesandbox_initis applied in-process and the targetexecved in place, one pid with no supervisor. SoOwnership::{Kept, Surrendered}is threaded to the bwrap argv and decides that flag alone. The consequence is stronger than the ban it replaces: the old rule permitted survivors only where no sandbox engaged, so every detached process in existence was born unconfined under--base dangerous; the new one births them under the frame’s projection and freezes it for life, since no later frame can name the process to widen it. The authority becomesdetach: Option<bool>on the capability lattice, folded at the call byGrantStack::permits_detachand not inSandboxProjection— it gates a verb, it does not describe a confinement. Silence permits, as on every other axis: the opt-in alternative was rejected as the only dimension where absence of an opinion would deny rather than inherit. Absence and refusal stay different axes (watch-repl-builtin) but absence now answers only the host’s question, no longer smuggling in a capability judgement made once at boot —engages_sandboxexisted solely for that and is deleted. Refusal precedes budget admission, so nothing born means nothing spent; the budget stays one monotone session-wide counter, a per-frame allowance rejected for having no honest release point. Left open: whether bwrap keeps a supervisor process, which decides whether the receipt’s pid names the program or the envelope — a documentation question aboutpid, wanting one run on Linux. -
active — exec-surface-fails-loudly — two exec-grant spellings that the decoder accepted and then read as something other than what they look like now fail at load: a path-shaped literal key naming a directory (
'/usr/bin'where'/usr/bin/'was meant) granted a binary that cannot exist, matched nothing, and let deny-by-default refuse every command the author meant to admit — failing closed but unreadably — sofreeze_exec_mapstats it and errors with the hint, the freeze pass already being where the environment is consulted; and an empty subcommand list stops being a third spelling of'allow', sinceSubcommands(∅)is legitimately the meet’s deny every invocation, so one object meant ⊥ inside the lattice and ⊤ at the surface and deleting the last entry jumped from near-zero authority to full. Follow-on to exec-authority-partitioned on the surface encoding alone; the value vocabulary and the lattice are untouched, and an explicitdir:sigil was rejected as the larger change to a convention that reads correctly once it stops being silent. -
active — path-derived-capability-sids — a Windows fs grant is keyed by the path it covers, not by the container that consumes it: each
(canonical path, kind ∈ {rw, ro, deny})derives a deterministic capability nameral.fs.<kind>.<128-bit-truncated SHA-256 of the canonical path>— hashed as-is, never case-folded, since a case-sensitive directory’s two distinct names must not merge into one authority — and thence a capability SID, whose inheritable ACE is stamped once, ever, and never reverted. This deletes the propagation wall ace-free-fs-confinement measured —SetNamedSecurityInfoWwalks every existing descendant synchronously because NTFS checks each file’s own descriptor, so a 100k-file tree cost tens of seconds to minutes per projection, per session, and again at teardown. Persistence is safe because a capability SID is read only in the AppContainer pass of the access check, whose result intersects the normal user pass, so an ACE no live token names is inert (Chromium’s LPAC install-dir pattern). Two witnesses gate a skip — a grow-only stamp store (stamps.json, atomic tmp+rename, per-path named-mutex merge) and a probe of the root’s own DACL — recorded after the apply, so a crash re-stamps idempotently and a child in the interim fails closed. A spawn’s reach becomes the capability SIDssession::confinemints into its token, so attenuation still shrinks-only and adeny_pathis its own opted-into capability, letting projection-specific denies coexist on a shared path; the per-projection AppContainer profile survives for the deny-by-default token and named-object separation, carrying no fs authority (projection-keyed-appcontainer superseded), and teardown restores nothing, so exit no longer hangs. The load-bearing accepted trade is that stamped authority is object-sticky where a grant rule is path-based: an ACE lives on the NTFS object and Windows never re-inherits on a same-volume rename, so a file moved into a granted tree stays dark (fail-closed) while a file moved out of an rw tree keeps its capability ACE and stays writable throughcap(A)even inside a ro-granted tree B (fail-open) — hard links across differently-granted prefixes being the same fact respelled. Both drifts predate this page; restore-at-teardown merely bounded the fail-open one to a session, and persistence extends it indefinitely. Mitigations weighed:ral sandbox restamp/gctooling, an opt-in background re-verify (O(N) reads, so never per-session — it would reinstate the cost removed), USN-journal tracking rejected on wrap/crash complexity. The millisecond steady state is the no-drift fast path only. Shipped as the interim that keeps default-deny reads; tiers A/B of ace-free-fs-confinement remain the destination, and a validation matrix (three-arm LowBox spawn, deny-over-allow from inside the child, wide-vs-narrow attenuation, nested-capability subset behaviour, reparse points,SE_DACL_PROTECTEDholes, ≤3 ACEs per prefix, token capability-array limits) is open before it is called settled. -
active — boot-contract-is-versioned — the
ral.kernel-command-line keys and the grammar of their values are one indivisible agreement with a version,ral_daemon::boot::CONTRACT, kept beside the command line’s only writer and only reader so a new key and its bump cannot land in two commits. An installed synod built five days after its guest media wroteral.netto a guest whoseBoot::readpredated it; the guest refused the whole line — correctly, since a setting it cannot interpret is authority nobody granted — powered off, and the only thing the host could say was the guest did not dial the control plane within 60s of starting. Softening the refusal is rejected, and so is a run-time check: by the time a command line exists there is no channel to negotiate over, so every honest moment for the comparison is before host and media are packaged together.ral-daemon/examples/boot-contract.rsprints the constant and nothing else;vm-image/build-boot.shcompiles it, in the same cargo invocation and from the same checkout that produces the initramfs’sral-daemon, intoboot-manifest.txt’sboot_contract=line — a grepped source line or a hand-kept number would record exactly the drift the number exists to catch;synod/build.rsputs that manifest toboot::check_mediaand exits 1 with one sentence naming both numbers, the file, andjust guest-boot,ral-daemonbeing a build dependency because the comparison is the build’s business and synod’s own code never asks. Three refusals, not one (numbers differ · noboot_contract=line at all, so media of unknowable vintage · a line that is not a number); absent media is deliberately no failure, sincecargo checkmust still work and Tauri already names a missing bundle resource. Amends the first open question of windows-hyper-v-backend. Open: nothing enforces the bump itself, and an installed mismatch is still only legible after the fact — through the guest’s own words rather than a check. -
active — guest-console-outlives-stdout — a diagnostic written to a handle that goes nowhere is not a diagnostic: on an installed synod the machine’s owner is a
LocalSystemservice (windows-machine-broker) whose standard output writes nowhere at all, and the console pump both wrote only there and stopped on its first failed write — which under a service is the first chunk — so the one line explaining a refused boot was discarded every time while the failure said the reason was “above”. The pump now tees:stdoutfor--console, a per-machinesynod-console-<id>.login the one cache the backend may write and a service can reach, and aTailring the failure quotes; a deadstdoutdrops that sink and keeps the other two. Bounded by construction (RETAINED_LINES,LINE_LIMIT,LOG_LIMIT,LOG_LIFETIME), keeping the log’s head because a boot explains itself at its beginning; kept when the boot failed and discarded when it dialled, told apart by onedialledbool, since a failure named its log in its own sentence and so has a reader still to come.console_saysanswers in three ways that leave the reader in three different places — the guest’s last words quoted, the guest said nothing (itself the finding), or no console could be opened (a fault in synod, said as one). The broker protocol is deliberately not changed andbroker::VERSIONstays 2: the boot error string already crosses the pipe to the window, so quoted lines and a log path need no new frame, and a version bump is a compatibility event between an installed service and an installed window. Open: how many lines a failure should quote is a judgement, and nothing surfaces the console into the review screen. -
active — session-disk-outlives-its-machine —
Stoppedis the compute service’s word about the machine, not the worker process’s word about its files:vmwpholds the session VHD open for a moment after the machine reports stopped, so the single-shot delete at teardown lost a race it could not see, and since nothing ever reads the machine cache, lost meant forever — six orphans, ~300 MB, in one realC:\ProgramData\Synod\Machine.removenow retries everyREMOVE_PULSEuntilREMOVE_GRACE, reading the deadline after an attempt so the disk is always asked for at least once, and treating an already-absent file as released;releasewrites one stderr line naming the file, its mebibytes and its fate rather than raising anError, because the samestopruns fromDropwhere aResultis discarded, and because a caller could not tell it apart from “the guest had to be stopped for” — a claim about the user’s own work.Hyperv::newsweeps: a just-constructed backend owns no session disk, so everything of that shape belongs to a finished run, with another live synod covered twice over (its worker holds the file open, and a disk younger thanORPHAN_AGEis never asked for). The sweep is structurally incapable of namingrootfs.vhd, its marker, or a wrap in progress —session_disk_epochparsessynod-session-<pid>-<epoch>.vhdand answers nothing otherwise — and takes age from the name the making process wrote, not from a filesystem timestamp. Generalises to a rule for anything the backend leaves behind, named by shape and bounded by age, which the console log of guest-console-outlives-stdout is written under. Open:ORPHAN_AGEis an order of magnitude rather than a measurement, and whether the macOS backend owes the same sweep is unexamined. -
active — one-walk-one-anchor — a
PATHsearch is one traversal, from one anchor, yielding one answer. The anchor becomes aSearchCwdwhose only constructors are named for provenance —Context::search_cwd(thewithin [dir: …]-else-cdprecedence),Resolver::search_cwd,SearchCwd::offor a front end holdingShell::cwd,SearchCwd::nowhere— soctx.dirno longer typechecks where a walk wants “here”, which is what let dispatch anchor to an unbound override while vet’s own probe anchored to thecd-mutated cwd. The 126/127 verdict stops being a second walk:path::searchreturnsPathSearch::{Executable, FoundNotExecutable, Missing}from the traversal that producedresolved,CommandIdentitycarries it,check_existencepattern-matches it and takes no context at all, andfile_exists_on_pathis deleted — there is nothing left for walk and verdict to disagree about. An emptyPATHelement never means the cwd, uniformly and notcfg(windows)-gated: POSIX’s implicit-.-on-PATHis a forty-year-old foot-gun and a trailing;on Windows is noise no user authored, so honouring it would make every file of everycd’d directory a command;.still says what.means. And%PATHEXT%appends rather than replaces, sobuild.ps1no longer resolves to whateverbuild.exesits first onPATH. Together these turnedbuild.ps1: permission denied(126, about a file no walk had resolved, withCreateProcessnever called) into an honestcommand not found. A textbook instance of structural-bug-prevention shape 1, the path authorised ≠ the path used. -
active — launch-cwd-is-the-freeze-anchor — exarch freezes an agent’s authority against the cwd it was started at, never against the cwd it stands in: a trunk anchors to the launch cwd
run()reads once fromstd::env::current_dir()and threads by value intopolicy::for_invocation’s ceiling,bootstrap::project_dir/log_run_dir,prompt::assemble’sAGENTS.md/skills discovery, and/export’s path resolution, while the live shell seeded at that same spot drifts with everycdthe model issues and none of those consumers re-reads it. A desk child reads the same rule from its own side:agent-startnarrowspolicy::narrow(&s.caps, spec.grant, &s.cwd)against the parent’s live cwd at the instant of the spawn — “so a desk-spawned child starts where the model is” — thenSeat::identityfixes that reading into the child’s own seat, which/clearrebuilds from verbatim rather than probing again. One rule, read from both ends: grants freeze where the agent was started, so re-freezing oncdwould silently re-anchor authority nobody re-granted. Companion, at the exarch layer, to capability-freeze’scwd:sigil rule. -
active — bundled-tools-always-reexec — every bundled coreutils/diffutils/ripgrep invocation is a
ral --ral-bundled-tool <tool>child through the same spawn/wait machinery as a host executable; the inline in-process placement is deleted, its admission gate having required emptyenv_overrides— which no booted shell has, sinceseed_default_env_varsinstallsHOME/USER/PATH/SHLVL/OS_*at every boot — so the gate, runner, mutex, cwd-agreement predicate, and two silent I/O doors guarded a path only tests could reach. One placement, one exec door. -
active — a-name-is-a-value-or-it-is-handled — the builtin is not a kind of name: a manifest entry’s mechanism is one of ral’s two existing ones and is read off its arity, and effectfulness partitions nothing, since a function is a computation and a computation may act. A fixed-arity entry has a function type (arity 0: a thunk type), so it is a first-class
Value::Nativein a base env scope — it curries by collecting arguments, prints as<native NAME>, is equal by name plus collected arguments, crosses the wire by name re-linked against the receiving manifest, and types as the η-equivalent lambda does, uncurried all the way, somap $roundis ill-typed by design and the Bind rethunk is the idiom. An open-argv entry has no function type to curry, so it is only interpretable as command syntax and lives where that is interpreted: a base frame beneath the handler stack’s run frames (echoanddetach) — stackable, forwardable, and unremovable because no mutator’s index space contains it. The third arity class this page classified, an optional argument, is gone with no-value-has-an-optional-argument, which carriedcdand the REPL’sfg/bg/disownacross the partition into natives; arity then stops being the partition at all with argv-is-a-list-of-strings, which authors the manifest as two — a native table and a base-frame manifest — leaving arity a consequence of which half a name is in, and the argv half with no arity at all. Resolution is thereforeenv → handlers → externalwith no builtin arm, and it is the only arbiter of interception: T0043/T0044 and every name-admission check die with no successor, shadowing is the discipline, and^name— which skips the env by definition — reaches an installed handler. Facts the registry used to assert are derived instead: arity is the curry depth of the entry’s scheme, and the scheme is the entry’s value form. The page recorded one hand-written override,_type, whoseα → F αcorrelated argument and result;_typeand the override slot after it are both gone, and a builtin’s type rule is a scheme factory with no second arm to choose.echoleaves the elaborator, which keeps exactly one name-keyed rewrite —exit/quit’s zero-arg argv default, deciding nothing about resolution. -
active — one-delimited-trail — an unwind discards a call’s bindings and keeps its effects, so a dispatch owes its caller a pair —
dispatch : Program → Ending × Trace— and the harness stops rebuilding the trace per stratum (the act ledger,birth_epoch’s clock arithmetic with its documented misattribution leak,ToolResult.timed_out, stderr assembled by append order across two layers): one delimited trail under five laws — flat merge; the opener owns closing on every exit, panics included (TrailScope/Audit::close, killing the session-long leakforce_openleft and the stage-inheritance it caused); facts authored where they commit; a total projection (every seam ships a tagged`opaqueplaceholder, never silence — the rail’sdbg_tracedrop dies); facts, never prose — withaudit { },try,ral --audit, and the exarch tool call as four delimiters over one collector (Run.trail: Someheld atShell::enteroutside thecatch_unwind; a recovered panic reportsStatic, no trail, no ending arm), the desk and the cross-process helpers as authors only — the desk host-side at the commitment arm via oneObserved::Actfanned to rail row and per-call fragment, since a wire-seat cancel parked inenquirecan unwind a builtin whose act already stands. Worker births become presence-in-trace (Observed::Workerfiled atspawn_childafter the reservation), the trail rides the Report whole and unbounded (a tail cap would evict exactly the early births the orphan join needs), and one renderer (shell_eval::report::render) composes rendering, remedy, audit sentence, and an orphan sentence deliberately widened to every binding-discarding ending —Stoppeddraws nothing, job control keeps bindings. The ending becomes a literal sum, shipped as twoEndingtypes along theRunReport/Reportseam (liveError/Valueengine-side, rendered string on the wire) withrender_endingthe one lossy projection;transport::Breakdissolves; onePROTOCOL_VERSIONbump (5 → 6) covers the batch. Rider:schedule’s label is mandatory — onesubjectfield feeding two readers could not hold both the caller’s absent label and the registry’s mintedsched-<n>— carried as amendments on agent-names-and-schedule-labels and harness-calls-are-acts. -
accepted — depth-proof-env-seam — a lazy stream is a chain of closures, so any walk that crosses the captured-env link recursively spends stack once per line, and exactly two walks cross it: the serial encoder (a helper stage aborted on a few-hundred-line
from-lines) and drop glue (a 60k-line stream aborted teardown). Encoding defers:intern_scopeonly reserves an id and queues the scope,InternCtx::finish— the table’s sole accessor — drains the queue (the queuedArcs pinning interned pointers against reuse; the decoder needed nothing, having never trusted id order). Teardown trampolines:Closure::drop(viaEnv::dismantle; onBindinguntil 260826, when the persistent map made binding drops loop-resident) keeps a thread-local queue — a closure dying inside another closure’s drop hands its bindings over and returns, so glue still does all traversal (shared spines stay one decrement, nothing is cloned to be destroyed) while the stack between links stays constant. An iterativeDrop for Envwas implemented first and rejected by measurement (O(chain) per env drop turnedscope_escapesfrom 14 s into 11+ minutes), and ownership-traversal inBinding::droprejected on paper (consuming shared persistent containers deep-copies elements to destroy the copies — O(n²) accumulator rebinds). Pure-data depth stays recursive everywhere by design;for_shell’s O(n²) pass build is noted, not fixed. -
active — a-head-has-three-identities — a command head is two spellings and a file, and the gate’s asymmetry runs over all three: admission reads the spellings (
policy_names), every veto reads the canonical form and its basename too (deny_names_from), withlongest_dir_matchtaking the same split down to directories —allow_dirsagainst the narrow set,deny_dirsagainst the broad one — so a symlink can no longer wear an admitted name to reach a denied binary, while anallowon a target still does not reach a link the grant never named. One strictrealpath(3)per external dispatch, anchored atcwd_chain. The limit is stated rather than left to be found: a copy under a new name is a different file that no resolution recovers, defeating the gate and Seatbelt’s/bash$regex alike, so a name veto narrows an allow set and is not containment — the boundary is the projection the copy inherits, which reaches nothing its author could not. Amended 2026-08-14: the ADR’s “the boundary is the confused-deputy property, an exec-admitted directory must not be writable” is wrong in both directions. In-projection overlap escalates nothing and every bake-in requires it (reasonableflagscwd:,/tmp,tempdir:); the predicate that bites is authority outliving or exceeding the projection, and the class neither dimension reaches is a write some unconfined host process later interprets as code — grant §Concessions. -
active — exchange-ends-at-fleet-quiescence — synod’s after-checkpoint and report refresh wait for the trunk parked and no live children and their results drained, not merely the trunk’s own silence — a deliberate departure from exarch’s chat-while-they-work model, since synod’s checkpoint-before/report-after/undo promise cannot survive a report written while a helper is still writing to the folder it describes. Synod’s trunk fuel lifts from
0toSPAWN_FUEL(3, shared with exarch’s own trunks), andexarch::headless::converse_settleddrives the exchange: the ordinaryattendloop under a park policy answeringHeldByChildrenwhile children live,Held/Engaged/UntilCancellednever reachable from a synod trunk by construction. Supersedes the “never a fleet” half of the oldfuel: 0comment atsynod/src/session.rs; synod is the caller the engine protocol’s wire-side spawn shape was left waiting for. -
active — store-lives-as-long-as-the-conversation — the history store is re-priced and re-scoped together, one decision: a capture is a stat walk (
mtime_nsbeside the hash, reused unopened on a stat match older than the reference checkpoint’s owntaken_at_ms— git’s racy guard, stamped at walk start), a walk tolerates a living folder (WalkError::Vanished,hash_file→Ok(None), never an abort), and the large-folder warning — with afree_bytesfree-space sentence — fires off a stat-onlymanifest::measurebefore a byte is read,Conversation::beginno longer joining the before-checkpoint but spawning it as aBaselinethatexchangesettles before driving the model. What made the pricing’s persistence assumptions moot: the store now lives exactly as long as its conversation — every open store holds a shared advisory lock (flock/LockFileEx),endwipes it, andsweep_staleat startup collects whatever a crashed run left unlocked. Triggered by a 63 GB, 184k-file grant (minutes of silence per message, a warning after its wait, a 45 GB store, a capture crashed bycargo clean). Rejected: an APFSclonefile/VSS copy-on-write baseline (parked — optimises a once-per-conversation cost already priced and named) and a size-budgeted archive with whole-job eviction (unworkable — a live undo’s baseline weighs what the folder weighs, so no budget could shrink it). -
accepted — synod-keeps-its-own-accounts — synod stops borrowing exarch’s environment-shaped credential story and gets a desktop-shaped one, exarch’s own behaviour unchanged: a key reaches exarch through the environment because exarch is started from a shell, while synod is double-clicked, inherits the desktop’s environment, and faces someone with no
.zshrcto export from. Two sources in one order — the computer’s credential manager first (provider::keychain, onekeyringentry per(app, provider-label), so two products’ keys are two entries), the environment underneath, still swept and scrubbed first because that is the step which must run single-threaded. A computer with no credential manager is told about, not lied to:Entry::store_status()is asked, andvault()answers where secrets actually land in a sentence the window prints verbatim, the fallback being an owner-only file throughprovider::secret_file::write_private— theChatGPTtoken store’s existing care, extracted so one Windows DACL implementation serves both callers. Endpoints live in synod’s ownproviders.ralthrough a generalisedconfig::load_declared/save_declared, carrying addresses and never keys, a quote in a name being asked about rather than escaped.CredentialStoregains four window-facing mutators (known/admit_key/forget/retire) and records provenance at the binding (was_admitted) rather than letting an application re-derive it by interrogating its vault entry by entry — a round trip per provider, and an unlock prompt apiece, every time an accounts list is drawn. The real Keychain/Credential Manager/Secret Service round trips are untested: no GUI runs in the development sandbox. -
active — modes-solved-by-deferred-joins — one deferred constraint store, drained by the boundary that owns a variable rather than by whatever
leta program happens to place; conclusions applied early because a route only movesVar → ground, ground-directed collapse before equation, principality up to variables shared across one binding. Narrowed in place: of the three constraint kinds it named,JoinandAltare gone with the channel ends they merged, leaving the arm-result join alone — the architecture unchanged, its subject matter two-thirds smaller. -
superseded — byte-only-pipelines — the interim rule pinning both a byte edge’s producer payload and its consumer input to
Bytes, while permitting a value-returning final stage; superseded the same day by pipes-are-positional-byte-wires, which keeps its byte-only transport and its refusal of implicit value serialisation but drops the endpoint contract. -
active — pipes-are-positional-byte-wires —
|merely connects stdout to stdin: neither endpoint promises traffic, a non-final stage’s returned value is discarded rather than serialised, and every interior edge is an operating-system pipe allocated from position. The one surviving stage rule is a shape premise — a stage must beF[ρ] A, not a function still awaiting an argument — so a whole-stage block literal is accepted, a footgun preferred to a syntax-directed rule that two spellings of one computation would answer differently. The payload route survives only for value boundaries, branch joins, higher-order forwarding, and the final report; WF-2 is carried by the one byte-routed computation,CompTy::bytes()=F[Bytes] Unit— landing on the byte side unifies with it whole, repairing a live defect at the alias/handler pin.PipeSpec,PipeMode,ByteMode,ModeVar,Wire, and the_typeprobe are deleted; the IR carries onePipeYieldper pipeline —LastorUnit, the last stage’s route committed to syntax, so no route reaches the evaluator. -
active — case-is-syntax-try-is-not — a
case’s arms become a syntactic list (Vec<CaseArm>in AST and IR), so every alternative is a computation the checker can see and exhaustiveness is decided statically, always. The line falls at the set of alternatives, not the alternatives: the arms are written out at thecase— a computed table, a...spread arm, a repeated tag, and an empty list are parse errors — while an arm’s body stays an ordinary computation, an atom naming a handler elaborating to that handler applied to the payload. It repairs four defects that were one fact, an arm the checker cannot see getting noCapture, and retires the runtime unhandled-tag miss.trykeeps its first-class handler, because its branch set is never opaque while acase’s would be, and composable elimination algebras are excluded permanently: an assembled table is a totality claim with no proof behind it. Operationally an arm becomes anif-like branch — the recorded status inherited, every context mutation persisting, an unselected arm’s hoisted effects no longer run. -
active — a-coercion-is-syntax — the byte-to-value coercion the checker inserts is two kernel nodes,
Decode(Capture(M)), and no part of it is a name. The old spelling,capture M to __captured . __decode-captured $__captured, wrote a checker-synthesized term in surface machinery and inherited every mechanism the type system cannot vouch for: an alias or handler frame named__decode-capturedretyped every capturedlet(unsound), the fixed binder overwrote and leaked$__captured, the builtin panicked on a spread call past its static arity, and the buffer was copied twice on the shell’s hottest path. Whatever the checker writes is syntax; whatever the user writes is theirs to redefine — soM | from-stringstill means whatever their session says it means. Name reservation was refused as the non-compositional alternative. -
active — depth-is-guarded-where-it-multiplies — a depth budget belongs to unification, the one traversal whose depth is not bounded by the source; the structural walks beside it stay unbudgeted by design, since a syntactic ceiling of 64 already bounds what a program can write and a type built one constructor per statement is only as deep as its file is long. Records the reproduction that closed a proposed stack-overflow finding — 150,000 levels of nesting checked without overflow or
TypeTooDeep— and the fact that attempt did produce: checking is superlinear in nesting depth, 3× the depth for 12× the time. -
active — no-value-has-an-optional-argument —
ArgSig::Optionalis deleted, leavingExactandAny: an entry declares its arguments or it takes an open argv, with nothing in between.cdbecomesExactof oneStringand the REPL’sfg/bg/disownExactof oneInt, so all four cross the arity partition into natives —$cdand$fgexist, a bare head is no longer intercepted (^cdstill reaches a handler, as^jobsdoes), andechoanddetachare the only base frames left. Barecdis a T0050 arity error rather than$HOME, and a barefg/bg/disownan error rather than the most recent job — a deliberate break with bash.at_mostleaves theBuiltinAritydiagnostic along with theOptionalarm and the error gains the builtin’s name, so`cd` expected 1 argument, got 0replaces a nameless count — an improvement for all ~80 builtins rather than a special case for two. -
active — argv-is-a-list-of-strings — argv is a list of strings, and everything else is lambda calculus: the two argument-passing mechanisms share nothing, so
ArgSigis deleted andechoanddetachleave the builtin table for the base-frame manifest, typedList String -> Return(Bytes, Unit)andList String -> F Any. Both argv boundaries already had a type and neither was written down —List Stringinside, bytes at the OS call — so the manifest is authored as two rather than one table read twice, andfixed_arity,native_value,seed_natives_and_base, andderive_sig_schemeall become total. §6.6’s “remain ral values” wart dies by the coercion, not by weakening the check: a call’s argv elements are rendered before they are unified, so a heterogeneous handler call settleselematStringinstead of raising T0010, and the unification an arm’s soundness rests on is kept and made true. The price is the rule — an arm consumes what an exec call would, because otherwise it is not substitutable for the command it stands in for, so an arm that wants a number parses it. It stops short of deletingBuiltinSigand the argument templates, whose five diagnostics are the templates’ own agenda, and leaves R0001-as-a-static-diagnostic reachable and deliberately untaken, for exec-boundary-gated-statically to take. That agenda is now closed out and the templates are gone: a builtin’s type rule is a scheme factory and nothing else, T0054 and T0055 ride the entry as a diagnostic facet and a post-check, and T0050 is re-founded on readiness rather than arity — under-application curries, and what is refused is a discarded value still waiting for an argument (fixed-arity). -
active — exec-boundary-gated-statically — shape is exactly what a type states, so the refusal guarding
execve(2)fires before the run wherever an argument’s type says the shape (T0057) and at the spawn wherever polymorphism hides it, which isdocs/SPEC.md§6.5’s promise finally delivered for an external’s arguments. The refused set is declared once —RefusedArg(core/src/types/exec_arg.rs), withof_valuefor the spawn,of_tyfor the checker, and one remedy per shape so both refusals speak one language — and both maps are wildcard-free, so a newValueorTyconstructor cannot compile without a verdict on each side. Two facts fall out of writing them side by side: a record is a map at run time and refused as one, a tagged value is a word and refused by neither. Concrete types only, and never a spread: a variable’s shape and a spread’s element count are the run’s business, an empty spread refuses nothing, so no program that ran before stops running and the gate is pure gain. No renderability class and no deferred obligation — first-orderness is the wrong predicate, and the exact obligation on a type variable stays a separate question whose open half is the policy for a variable that never grounds. -
accepted — context-is-a-projection — the durable law is that no recorded event is removed, while model context is the left-fold projection of an append-only event log; incremental recording is checked against both a from-scratch fold and an independent batch reference, residency follows the addressed view at O(view), and the file’s disk/O(file)-resume price, closed-exchange edits, fresh-shell resume, transient
--no-logs, and deferred segment rotation are explicit. It amends recording-follows-the-event with the debt of keepingtranscript.jsonlbeside the log; one-seam-one-log generalises its fold law from the model view to the whole log, and a-trace-is-a-fold retirestranscript.jsonlrather than keeping it besiderecord.jsonl. -
accepted — one-seam-one-log — every fact a session records crosses one seam (
record::Emitter::emit, append-then-publish under the log’s own mutex) into one durable log,record.jsonl, and every durable artifact is a fold of it: the model context over the sealedProtocolclass, the resumed scrollback overDisplay/Forensiccommits authored worker-side (the chopper andSurfaceBuffermoved upstream of the seam),user.loga regenerable render.events.jsonlretires; a pre-plan session refuses to resume with a named error;--resumefinally restores the user’s scrollback and cumulative usage, not just the model’s memory. Explicitly incomplete for live display — the running frame still draws the legacyKindstream through a transitionalSignal::into_eventbridge — with four named blockers (unrecorded live chrome vs. wholesalesync, no UI-thread recorder forSystemNote/ModelChanged, errors that cannot record themselves,ContextEdited’s missing notice commit), andtranscript.jsonlstill an independent trace — since deleted whole by a-trace-is-a-fold, which folds its one genuinely unique fact (t_ms) into the log’s ownEntry.at_unix_msrather than keeping a second trace. Pays half of recording-follows-the-event’s two-record debt. Corrected 260815: a reasoning run commits at the seam where the prose after it resumes, not at the step’s end — which the paragraph chopper had turned into the middle of the answer, landing∴between the paragraphs already committed and the tail not yet; the provider’s two stream callbacks collapse into oneDelta::{Say,Think}, since two independent callbacks cannot express that a run ended where the prose began, andDisplay::Thinkinggives upanswer_charsbecause a commit preceding the prose cannot carry that prose’s mass. Corrected 260816: a block is the run of consecutiveDisplayrecords of one lane, joined by the view fold (Blocks::push), so the producer’s cut falls at the last newline and carries no meaning — the fence-safe paragraph scanner, the whitespace-partition rule, and the printer’s wholeUnaccountedarithmetic delete, and the live answer reads as prose (reasoning as reasoning) rather than as a magnitude bar: the printer keeps only the open line past that same newline and renders it inside the block that will absorb it (Viewport::live_tail), one rendering path for live and committed text. -
accepted — a-trace-is-a-fold — a session keeps one durable record:
transcript.jsonlis deleted outright rather than retired to a filtered projection, because an operational view is a fold ofrecord.jsonllike every other durable artifact. Its three unique facts move to truer homes — a per-line clock to the log line’s own privateEntry.at_unix_ms, a child’sborn/diedto its ownSessionStarted/SessionEndedbookends,stop_reasontoProtocol::AssistantMessage, which already carried it — and the fourth,/resources’ pressure figures, is named a loss rather than deferred to a fold that cannot exist, since no session records pressure as a fact. Pays in full the two-record debt recording-follows-the-event booked and one-seam-one-log paid by half. -
active — a-producer-that-outlived-its-reader — the pipeline’s one failure exemption is a fact about two stages, not about the producer’s status word: a non-final stage still running when the stage reading it ended keeps no failure, whatever it exited with, because the rest of its output was owed to nobody. Unix says that with SIGPIPE, Windows with the order the two ended in —
ChildHandle::exited_at(GetProcessTimesthere,Nonehere, where the signal already names the case), compared by the pipeline collector, the only party holding both handles, which now walks its stagespeekableso that the next stage is this one’s reader and being final is having the caller for a reader.CommandFailure::from_outcometakes thatReader—CallerorStage { outlived }— in place of anis_pipeline_non_finalflag, so the forgiveness reads once. Rejected:STATUS_PIPE_CLOSING, the NTSTATUS the tree carried as “Windows’ SIGPIPE analogue” and which no process exits with — a cut-short Windows producer exits however its author chose (0for bundleduu_yes,1for a GNU-style write-error report,3328for the MSYS2yes.exeon a Windows runner’sPATH, SIGPIPE’s 13 in the Cygwin wait-status encoding), so no constant can carry the fact and it had to come from elsewhere. Unix is unchanged by construction; Windows forgiveness is broader only inside the pipe’s EOF-propagation window. -
accepted — the-window-is-not-the-transcript — a bounded window may neither be the source of an unbounded transcript nor be re-rendered whole per record.
user.logbecomes a stream the viewport is a window over: a block is written once, when eviction drops it, into a retired prefix that only grows, while the resident blocks are written past it provisionally at flush points and rewound by the next retirement — so/exportreads whole mid-session, a resumed run appends rather than repeating its replayed window (Viewport::seed), and a tombstoned sub-agent no longer regenerates an empty file over its own transcript. It supersedes one-seam-one-log’s whole-file render, which lost past eviction exactly what the incremental tee it replaced lost past resume. The second half is the printer’s own cost: the view fold stamps each row with the revision it last moved at (Block::rev), soViewport::syncrebuilds only from the first row past the revision it last synced and carries every block below over whole, with two back-dependencies named where the floor is computed (a reasoning row’s grain over the answer run beneath it, an answer’s echo signal over the lastralscript below the floor) and rows this window already evicted never built again. A block’s fidelity is thereby stamped by the turn that built it rather than restamped by every later sync, which is what tui-transcript-as-graphic says turn-level context pressure is. Left standing and named: the flatten is still rebuilt whole when stale (per frame, not per record), andcontext_floorstill grades against cumulative session input rather than the last turn’s prompt. -
active — a-failing-cleanup-pre-empts —
guard M { N }reads one rule for both of the cleanup’s signals: any halt of the cleanup pre-empts the body’s outcome, an ordinary error exactly as the control escape that already did. Body returns and cleanup halts, the halt is the outcome; both halt, the cleanup’s signal wins whichever kinds the two are; body halts and cleanup returns, the body’s signal survives. The retired half was trap-EXIT folklore — the cleanup’sErrlogged asguard: cleanup failed: …and the body’s result left standing — whose cost is that a cleanup cannot fail the computation: a lease unreleased or a staging file uncommitted reached the caller as success, uncatchable bytryand absent from everyaudittree, reported only in prose on an unstructured stream. Log-and-continue keeps its spelling and loses its privilege, asguard M { try N { |err| … } }orguard M { attempt N }— primitives strict, sugar soft. Typing is untouched, a halt carrying no value. This isβguard-halt, the kernel’s detour through؛, and it was the Agda kernel’s one standing owned divergence: the shell’s side moved, and the machine-own stderr writer plusrender : Err → 𝔹*the clause had mortgaged are owed to nothing else. -
active — diagnostics-are-a-builtin —
1>&2leaves the surface, because a message to the human is not standard output pointed somewhere else:warn : String → F[Value] Unitwrites the string and a newline to the stderr sink and returnsunit, a table entry besidesurfacewhose route staysValue, so a caller binding the computation’s payload never picks the message up — the property the redirect could not have, since it worked by making the two streams one. That is also the redirect’s honest indictment:1>&2does not mark a line diagnostic, it moves the payload stream, taking every byte the command owed its caller with it, and is therefore safe only where nothing is listening — a fact about the call site, not about the redirect. The refusal sits in the lexer’sscan_redirect_gt, which sees both descriptors and knows a bare>means fd 1, and nameswarnand2>&1both, since a program holding the exchange backwards means that one.2> fand2>&1stay: an external command’s stderr genuinely needs binding and filing.install_sink_redirectsnarrows with the surface to the 2→1 direction, closing a case the surface no longer opens. The model is paid immediately: the Agda kernel’s stderr parcel loses thecross!frame and thecrossesconstructor ofAnswerErr, whose only client this was, and its two routing walks stay one-directional — the survivingrejoinscontinues on the tail throughroute, which never calls back — wherecrosseswould have forced mutual recursion and mutual induction on every proof over them. -
active — a-stage-ral-stopped-has-no-failure — ral holds a duplicate of each interior edge’s read end until that edge’s writer stage is reaped, so no interior edge can ever deliver a broken-pipe signal or a write error to the stage that writes it; the collector kills a non-final stage once its reader stage is gone — SIGKILL on Unix, a distinctive-code
TerminateProcesson Windows — and that kill is the pipeline’s one forgiven death, every other exit status kept — the kill precedes the wait, so it can land only on a live process or a zombie, and a zombie’s recorded status is untouchable. Measured on Linux, 960 trials (120 per case, idle and under load), zero variance:yes | head -1and a SIGPIPE-ignoring Python producer are both forgiven every run,sh -c 'exit 1' | head -1keeps its 1 every run.!{ yes ; exit 5 } | head -1flips from 5 to 0 — the escape never occurs — and a producer that must run to completion regardless of its reader loses the SIGPIPE-ignore opt-out, the rewrite being its own statement orspawn. Supersedes a-producer-that-outlived-its-reader’s causal SIGPIPE/exit-order-clock split: one rule, both platforms. -
active — a-numeral-denotes-its-number — a bare word the numeral grammar accepts is that number in every position — argument, value, redirect target, list element — with no positional asymmetry; a word meaning bytes is quoted (
'007'). The complement is one printed spelling per number (Intits digits,Floatthe shortest round-trip decimal, always keeping its point), so canonical numerals cross byte-identically and the rest normalise on output (007→7,1.50→1.5,+5→5,.5→0.5,-0→0); the round trip is a test, never the definition, since classification is a lexical grammar that consults no type, scope, or printer. The printer’s image lies wholly inside the grammar — it restores the point ryu’s shortest form omits,1e300printing as1.0e300— so printing then reading is the identity on numbers; the grammar was deliberately not widened,1e6staying a word, since an exponent-only token is a digest or an identifier as often as a number. The dual holds on the emitting side:is_bare_wordconsults the grammar, so a numeral-shapedStringre-rendered as source comes back quoted. Answers witness-hash-h-prefix’s open language question by declining type-directed literals: checker-decided words are rejected for importing Haskell’s defaulting corner (principality lost across the default,let-naming no longer meaning-preserving, a monomorphism-restriction-shaped fork, a joint fixpoint with the route solver, and errors that cannot name the offending word), canonical-spelling classification for coupling the grammar to the printer, and head-directed elaboration for letting two mechanisms decide one question; qualified literals with evidence are explicitly not foreclosed. Named sharp edge:3.10is the numeral 3.1, so version-like tokens are quoted. Corollary landing beside it —unitstops being a word literal,()becomes punctuation that prints as itself, since a literal whose printed form is nothing cannot have one spelling. -
accepted — the-evaluator-steps-closures — the evaluator is a CEK machine. A computation closure ⟨M, E⟩ is in focus, the continuation is a stack of frames each carrying the environment it resumes under, and the store is the
Shellminus its lexical scope; onestep, one arm per rule of the plan’s tables. Gone: the recursive tree-walker, the ambientshell.mobile.scopepushed and popped around every scope, the trampoline with itsTail/Raw/Controlcurrency and everyabsorb_tailseam,Value::Lambda/Value::Block,LetRec,Seq,Mobile.M to x. Nputs ⟨N, E⟩ in theToframe before M runs, so a binder’s extent is structural;a; bisa to _. band a block is a right-nested binder chain. One thunk value andforce(thunk M) = M— no bracket, so a forced block’scdpersists like a lambda’s. Two terminal shapes (Value,Lambda) are a type. Recursion is an n-aryrecwith a projection, not a record fixpoint. The environment is a three-tier finite map (natives, frozen prelude, persistent bindings) and is not the store;Contextstays store, changed only by frames holding undo. The top level is phrases and aDefineextends the session environment for every later phrase, installed as it lands;sourceis a form worth();useruns under the session environment;$CWDand friends areObservecomputations, their names reserved. The cap counts frames (100 000) andreserveruns before any effect. The prelude is invariant by construction — every phrase aDefineof a value, the nineansi-*constants replaced bystyled <style>— so the wire ships only the bindings tier. Pipes arePipenodes between machines; no frame crosses the wire. Parked: handlers and grants on the stack (S9). Measured: pipeline launch −91 %, tail loop −55 %, non-tail call −22 %; open: abindinto a large persistent map copies a node path (B5/B7 slower), the representation trade-off recorded in the plan’s §9. -
accepted — reply-parks — a returned value is a fact the registry holds, not a message the parent reads. A child’s
replydeposits its faithfulFOValueon its own registry entry, cancels its descendants, and parks the child under the existing one-hour idle lease; the parent is woken with one line and fetches[name, reply]withagents `read <name>— the oneagentstag that answers a value rather than the roster, bindable and idempotent. The standalonereplybuiltin dies; the child hands up withagents `reply <value>, and the family’s scheme becomes∀α. … → F α(thepin-readprecedent), the price ofreadliving in the one fleet verb. Roster rows gainstate(`busy | `waiting-on-agents | `replied | `waiting) andidle-s, derived at listing time; a parent holds for busy children, not live ones; any message — the parent’s or a human’s — renews the lease; and the nudge layer has one gate: an agent is nudged only if it has not replied, waits on no detached work, and has no busy children. Amends the terminating half of reply-terminates-returning-agents and clause 2 of exchange-ends-at-fleet-quiescence. -
accepted — agent-and-avatar — an agent existed three times (
Agent,registry::Entry,HostServices), and the last two bugs fixed were the copies disagreeing; the fix is two types split along the public/private line —AgenttheArc-shared public half,Avatarthe private half every method runs against — with liveness the avatar holding theArc, status single-writer, the exchange clock on the inbox, and up strong/down weak on the tree.AgentRegistry(34 methods, ~2000 lines) becomesFleet { names, roots, lease }. Superseded in mechanism, not decision: reply-parks’s “the registry holds the reply” is now “Agent::statusholds the reply”. -
accepted — the-transcript-is-a-value — the provider-facing history is a persistent value,
Transcript(Arc<[ChatMessage]>segments, one per closed span, cloned by refcount bump), and ownedgenaiwire values are manufactured at one door,provider/wire.rs, at most once per HTTP attempt. Diagnosed from a live 36-session fleet run (~12 MBrecord.jsonl→ 2303 MB peak, pureMALLOC_SMALLchurn): up to three whole-history deep copies per deliberation step, the retry-closure clone buying nothing since genai consumes aChatRequestby value per call regardless. The model fold’s memo caches each closed span’s rendering once, keyed by span id and end index so staleness is inexpressible; the retroactiveomit/repair_endflags live only on the uncached tail renderer.Sealed(ChatRequest)is deliberately notClone;ChatRequestis named only inwire.rs. The genai floor stands: one whole-history copy per HTTP attempt,ChatRequestbeing consumed by value. -
active — status-is-the-outcome — a run’s exit status is a pure function of its outcome, computed once and nowhere stored;
Shell::last_status($?), every write to it, itsWireShellmirror, and its slot in the panic checkpoint are deleted. ABoolis data at the process boundary too: a run that returns exits 0 whatever it returned. Rejected: a clause mapping a returnedfalseto exit 1.
related/ — comparison to existing work
ral read against the literature; durable on the external work, keyed to ral’s
design pages via the against stamp.
- system-c — Brachthäuser et al. 2022: effects and capabilities reconciled; box = thunk, self-masking as capability-set subtraction, the type-based pole of grant.
- scoped-labels — Leijen 2005: the record calculus row-types implements, minus the restriction primitive — override is shadowing, never removal.
- handlers-of-algebraic-effects — Plotkin–Pretnar 2009: the founding handler calculus, on CBPV, with shell redirection as its own example; ral is its tail-resumptive fragment.
- rows-and-handlers — Hillerström–Lindley 2016: the effect typing ral declined — the same row machinery extended to every arrow; nearly ral’s runtime, the inverse of ral’s wild/handleable split.
- call-by-push-value — Levy 1999/2003: the substrate taken as surface design; ral tags
Fwith a payload route rather than grading it, adds the pipe as a combinator that lives outside the calculus, drops computation products. - cbpve — McDermott 2025: the reference ral’s returner is read against, and the reading is negative — ral is not a graded CBPV. Of the ordered monoid
(E, ≤, 1, ·)a grade needs,F[ρ] Asupplies none:Valueis not “no effects”, a sequence takes its tail’s route rather than multiplying, and the one subsumption instance is a branch-join rule, not a permissiveness order. The paper’s own bind rule is the proof — a grade acts on the continuation’s type, while ral’s bind readsρto decideCaptureand then drops it, and an annotation a bind may drop is metadata about a crossed boundary. The Gifford-style{reads-stdin, writes-stdout}pair that was an instance is deleted: a may-write grade over opaque external children is uninferable where it matters. Theorem 12 is kept on file for the day effects return — any algebra whose multiplication is its join satisfies the coherence condition by idempotence, so a pure may-use analysis is coherent for free and a quantitative one is not. - access-control-algebra — XACML, Saltzer–Schroeder, Bruns–Huth, Bonatti, Tschantz–Krishnamurthi, Al-Shaer–Hamed: grant’s restrict/extend-base as standard policy composition — deny-overrides (a deny is a floor, both ways) as fail-safe default; the four-valued bilattice is the deeper structure.
map/ — where things live
- core — ral-core overview hub: the compile-to-typed-IR pipeline, the single framed run door (
Shell::run, dispatching on theProgramsum) that is the only evaluation seam, thehost/boot/runsplit, and the subsystems below.- syntax — lexer, parser, flat AST; a command’s payload route is the projection of its declared type; one shared depth cap bounds lexer and parser recursion.
- elaboration — surface AST → CBPV IR; the one sugar-aware phase.
- ir — the
Val/Compcall-by-push-value IR, andToplevel { phrases: Vec<Phrase> }above it;Bind/Phrase::Definecarry the checker’s scheme,Recis an n-ary generalisation of Levy’srec x. M, andPipelinecarries one non-optionalPipeYieldplus per-stage value types as typing metadata rather than transport; no route type is reachable from here. - typecheck — HM with row types; returns an annotated
Toplevel(schemes on eachPhrase::Define, onePipeYieldper pipeline, per-stage value types,Capturenodes) from oneSessionSchemesseed; a stage is forced toReturnshape, a pipe edge into a stage-root stdin feed is refused (T0070), and no type relates a stage to its neighbour; WF-2 is an obligation at the two route grounders; handler/alias arms are fixed-arity lambdas pinned to their head’s route; the route types live intypecheck/route.rs, private to the checker, under an equality-strict unify rule. - evaluator — the CEK machine over computation closures: crate-private verbs entered only through the framed run door; frames carry their own resuming environment, tail calls push none, scope frames, matching, audit; a same-thread β-step runs in the caller’s session, block and lambda uniform.
- runtime — the command/pipeline machinery the machine dispatches into: byte pipes allocated between stages from position alone, bundled heads as
--ral-bundled-toolexec images, external children spawned under the effective sandbox, grant bodies run locally, helper-staged final-value reporting, redirect/exec surfaced at runtime doors, plus the shared re-exec’d-child eval runner (child_eval.rs). - capabilities — the grant decision layer (free
capability::check_*(&Context, …)folds),path/grant resolution, and the OS process sandbox (macOS Seatbelt, Linux bwrap, Windows AppContainer over path-derived fs capability SIDs); kernel-denial hints offer a path to grant only forfile-*denials. - io-process — byte sinks/sources, the lease-gated foreground handoff, the Cancel|Run reaper daemon, Stream labels; the guest spawn jail’s per-engine uid/cgroup sequencing off a guest-global counter file, and the recorded gap — no seccomp yet filters
socket(AF_VSOCK)from inside it. - builtins — the
builtin_registry!macro andCORE_BUILTINS, plus bundled coreutils/diffutils/ripgrep heads dispatched in-process viauutils_invoke; registry/seeding here, runtime exec-image dispatch on runtime. - shell-state — runtime
Value, thesurfacesink, handler stack, and theShellstate split by lifetime intoenv/context/Io/SessionState/LocalState, with a run’s invariant half riding beside it as theMooring; a scope entry isBinding { value, scheme }. - transport — serde mirror (
SerialValue = FOValue<Closure>,SerialBinding) and wire envelope (WireShell) carrying a shell — values and schemes — across a re-exec; the codec also carriesWireChannelframes;EngineSeedreifies the scrubbed fork for a wire-seat hatch, withfork_scrubbedremoving handle-carrying bindings before the identity arm parks or the wire arm listens, so both seats snapshot the same fragment. - engine-protocol — the front-end⇄engine frame algebra (
Frame,Event,SessionEvent,Report/Ending), theHosttrait every dispatch rides,dispatch_to_report,IdentityTransport/WireTransportandSevered, the--engineprocess inengine.rs, and the wire-seat hatch inhatch.rs. - diagnostics —
Span/FileIdbyte-range positions rendered directly via ariadne; the layer also exposesbyte_to_charand the type-error label so an external surface can draw the same underline; ANSI gating; exit-code hints. - prelude — the embedded
prelude.ralstandard library.
- repl — the
ralbinary: argv dispatch into a run through core’s framed door, driving one of three selectable frontends (minimal / readline / structural live-state projection) over the REPL session, plugins, and jobs.- startup —
main.rsprocess dispatch,cli.rsargv →Mode(--surfacefrontend, clap-derived argv terminator),batch.rsexecution through core’s framed run door, the annotated-prelude bake, platform glue. - loop — the
Sessionstate machine over an ownedIdentityTransport; one run is aProgram::Sourcedispatch throughprotocol::dispatch_to_report, seeded from the live session; the selectable frontend, prompt/theme/rc. - frontend — the
Frontendtrait and its minimal / rustyline / structural editors, the shared fuzzy completion engine, and the in-editor plugin surface (ghost text, highlights, keybindings) both TUIs drive. - plugins — the plugin runtime: the hook model with source-mapped faults and a buffer-change circuit breaker, hooks registered in the shell’s hook table and framed as
Program::Hookruns, the_ed-*editor builtins, keybindings, and captured session commands, driving the in-editor plugin surface both frontends render. - jobs — process-group job control, fg/bg/disown,
Escape::Stopped;fgresume gated on a held terminal lease.
- startup —
- exarch — the exarch agent’s front door: startup (CLI dispatch, bootstrap, account selection, credential resolution + env scrub, sandbox early_init) and system-prompt assembly; the agent is a provider loop over one
raltool, each exchange a grant-framed ral run.- agent — an agent is an
Arc<Agent>(the public half: identity, the two cancel doors, mailbox, provider, immutable config, single-writerStatus) plus anAvatar(the private half every method runs against), live exactly while its avatar holds theArc; the thinFleetis{ names, roots, lease }, twoWeakdoors over the agent tree, not the tree itself. Each agent is seated on an identity or wire transport (an in-process shell, or a remote engine one process per session), the attend loop (round-trips, tool dispatch with tool-boundary steering, the record-backed model projection and context edits, auto-compaction, fresh-shell resume, nudge-retry, theMAX_STEPSceiling, sub-agent forks in two memory modes), the construction-fixedreturnsbit,HeldByChildren, thefuelspawn budget, the owned hot-swappable provider, dynamic focus, and the subtree cancel cascade overAgent::parent/Agent::children(up strong, down weak). A wire-seat trunk’sagents `startremains one exchange: the engine binds a one-spawn listener, the desk reaches it through itsDialcapability, and the guest acks only after the child exists. - provider — LLM transport and live model catalogs: famous/custom/ChatGPT-account identity, shared OAuth renewal, streaming liveness, retry, prompt caching, usage/pricing, structural error classification.
- shell-eval — one tool call as a transport-level
Sourcerun dispatched viadispatch_to_reportagainst the agent’s seat transport (the in-processIdentityTransport, or a wire engine’sWireTransport), under a pushed grant frame, seeded from the live session, withDeniedterminal access; buffered output digested for the transcript, the surface host sink decoding card marks onto the bus. - io-surface — redirect reads/writes and exec images surface at runtime I/O doors as structural events, rendered as grouped cards; bulk helper I/O sunk below the ral line, enforced by a clippy-checked door set.
- policy — capability composition (base ∨ extend ⊓ restrict for the root,
parent ⊓ basefor a spawned child), the six bake-in profiles, and restrict-file self-denial; the boundary is ral’s grant. - tools —
ralalone is the tool; spawning, messaging, cancelling, scheduling, andreplyare builtins reached by writing ral inside it, answered by the per-callExarchDesk, withtools.rskeeping only theralentry and the shared fork-detach-register spawn spine. - builtins — the resident host atoms (
view-text/view-hash,grep-files,edit-hash/edit-replace,explore-dir,fff, the skill readers,service-handle) reading below the redirect frame, theagent.ralkit over them, and the harness verbs the desk answers (thecontextfamily andtranscript, the one record-specagentspawn verb, the label-keyed schedule family,reply), for search, adaptive-context line witnesses, witnessed editing, and sub-agent orchestration. There is no model-facing network builtin; a guest reaches the network itself, policed host-side (egress). - frontend — the
Signal::{Fact,Transient}bus, one durable session record with model/view folds, the headless frontend, and the inline TUI: a two-voice transcript laid out as a graphic — human band vs agent field, the marginal rail, slash-command routing, and an in-flight reply as a provisional edge. - cards — the
surfacerender document: a closed set of six Bertin marks a kit composes in ral, decoded once and drawn through one generic interpreter; the kit names data and level of measurement, the host owns the visual binding.
- agent — an agent is an
- synod — the office-work sibling, one crate in two halves: the library modules any host could drive, and the desktop shell rooted at
synod/src/main.rsthat is the only thing that drives them (onesession::Conversationper folder). One granted folder worked in place under a checkpoint→report→undo safety net (content-addressed per-folder history, conflict-checked put-back), an office persona, exarch embedded as a library; every conversation boots a real hardware machine from shipped boot media (no software-only fallback) — one guest, two lifecycle backends, Virtualization.framework on macOS and Hyper-V through HCS on Windows (windows-hyper-v-backend), the Windows machine created by an unprivileged request to aLocalSystembroker service (windows-machine-broker) —ral-daemonruns as PID 1 in the guest, and one engine process per session speaks the wire (engine-protocol); the macOS path runs end to end, while on Windows a machine creates, starts, and boots a kernel and an initramfs as far as the daemon, and a guest that completes its boot and dials is not witnessed yet. The kernel command line is a versioned agreement compared against the media at package time (boot-contract-is-versioned), the guest’s console is teed to a bounded log and quoted in the boot failure (guest-console-outlives-stdout), and teardown waits out the worker process that holds the session disk, with a sweep for what earlier runs left (session-disk-outlives-its-machine). The guest also gets a network of its own — atunwhose only peer isguest-net, a user-mode TCP/IP stack in a host process, gated by the destination policy defended in egress — replacing the singlefetch-urlverb an earlier design made the whole egress surface (the-guest-gets-a-network-not-a-verb, one-connect-door-not-four-gates). The trunk’s fuel lifts toSPAWN_FUEL, so the office assistant may delegate to helpers running concurrently in the same guest: the host dials into the guest, one connection per spawn, overMachine::connect_guest— synod’sMachineDialis theDialthe desk’s wire spawn calls through (agent), and the control and net ports stay the only two the host listens on;exarch::headless::converse_settledholds the exchange open until the whole fleet quiesces, not just the trunk (exchange-ends-at-fleet-quiescence). - ral-sh — the POSIX-bridge login-shell dispatcher; execs
ralinteractively, forwards everything else to/bin/sh.