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-effectscbpvtypesthe compilation ladderthe evaluator machinegrantcapability enforcementexarch-architecturea 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 (Bytes implies Unit) 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/Scheme rules with the derived value form, and the manifest authored as two — a name is a native value or a base frame.
  • codecsfrom-X/to-X as the typed byte↔value crossing: a decoder F[Value] A, an encoder A → 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 } prints a and yields "b", with no 2>/dev/null needed 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 the Capture wrap 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, try as recovery and the only ||, a Bool is 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 ral tool, each exchange a grant-framed ral top-level run; orchestration verbs are ral builtins, not sibling provider tools.
  • hash-addressed-editing — the scheme --edit hash teaches, 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, and edit-hash are 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 a card `` 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 keeps Pin/Unpin as forensic breadcrumbs; the register mirrors tasks/goal for 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). Holds config.ral (custom providers) and global AGENTS.md; trusted because the grant cannot reach it, yet config.ral is still evaluated no-authority because a redirected endpoint is an exfiltration channel.
  • agents-md-injection — exarch injects AGENTS.md files as a Workspace system-prompt section, discovered outermost-first (operator’s <config>/AGENTS.md, then every repo AGENTS.md from the git root down to cwd; the walk stops at the first .git entry). They steer behaviour but add only prompt text, never capabilities — so a cwd AGENTS.md is untrusted yet harmless: it cannot widen the grant, unlike trusted config.ral, which can cause effects.
  • agents — the sub-agent model: a run is a tree of uniform Agent nodes under one shared attend loop, distinguished only by position — the parent-less trunk (conversing when a human is attached, withholding reply) versus every returning agent, keyed on a construction-fixed returns bit, never an is_root flag. Spawning is universal but bounded by fuel, a per-agent budget each fork hands one less unit of to its child; the record-spec agents `start tag forks the serialisable fragment of the parent shell’s value-snapshot onto a detached thread (handle-carrying bindings scrubbed by fork_scrubbed before either seat chooses how the fork waits, so an identity fork and a wire hatch’s EngineSeed mean the same thing — the one snapshot law) and gives the child a name that is its fleet-unique identity; the spec’s type field picks the child’s memory — amnemon blank, mnemon inheriting the parent context with a fresh prompt; an agent may send a marked message to a named descendant; returning is the deliberate reply, which cancels unfinished descendants before the node settles; focus is the dynamic human attachment, immune to the subtree cascade that only agents `cancel, the idle-lease reaper, and /clear perform — Esc interrupts just the focused exchange; self-scheduling authority is inherited; a spawn’s mandatory grant base bounds the child to parent ⊓ base — a lattice meet that narrows but never escalates. A wire-seat trunk still spawns in that one agents `start exchange: its engine listens once, the host dials through Dial, 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 every CONNECT host-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-order FOValue behind a closed, versioned envelope that grows only by class, never by channel; a run’s whole host-facing surface is one Host object 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 first Ping arms 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 compile verbs, 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 at Bind, 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 step with one arm per rule, two terminal shapes, one thunk value, rec n-ary, a frame-counted cap checked before the effect, phrases and Define at the top level, pipes as nodes launched and joined in one rule, the panic walk.
  • builtins-registrybuiltin_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 StageLaunch freeze, the single PipeYield deciding 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, the n ≥ 2 pgid 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::run dispatching on Program::Source/Program::HookRunReport).
  • 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; spawn moves it to a root-parented worker with a 16 MiB-bounded buffer under an idle-observation lease (1 h unobserved, 24 h backstop; service births 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 CancelScope tree (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 → foreground Interrupt, SIGTERM/SIGHUP → root Terminate at exit 143) — backed by an escalation ladder whose third delivery _exits; process::check polls 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 Fault walk (Status / Transport / Terminal) that reads retryability from typed variants, never the Display string; the 429 / 5xx / 4xx split into ProviderError; the one retry_with_backoff driver with a patient rate-limit tier and explicit Retry-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, and user.log is 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 Scheme leaves 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; /resources is 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, so 1.0e300 rather than 1e300 — hence printing then reading is the identity on numbers, while 1e6 remains a word; the emitter that renders a String back 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.

  • supersededtyped-state-flow-wrappers — typed wrappers for shell-state flow; the boundaries closed by env-is-dynamic-only and a current_dir audit, so the wrappers were not built.

  • activehot-path-cancellation — cooperative cancellation in hot loops.

  • activecompletion-escape-refactorEvalSignal retired for Settled + Escape/BodyResult.

  • fixedescape-propagation-bugs — try-swallows-exit and grant tail-call bypass.

  • activerepl-builtins-stay-in-repl — REPL builtins live in the REPL layer, above core.

  • proposedrepl-architecture — REPL direction: stream console now, hybrid workbench later.

  • activebackground-tool-calls — scoped in-turn agent batching is active: dispatch stages a whole tool-call batch under one thread::scope and joins before the parent turn continues; true turn-outliving backgroundable tools remain future work.

  • fixedredirect-drop-on-handler-dispatch — redirects install on the handler arm.

  • activeast-stays-flat — the surface AST enum stays flat.

  • activehandlers-deep-self-masking — handlers are deep and self-masking.

  • activeinfer-case-stays-wholeinfer_case is left as one function.

  • supersededenv-overrides-scope-overlapenv_overrides / scope overlap.

  • openlinux-exec-confinement — path-scoped exec is unenforced on Linux (no landlock).

  • activeenv-is-dynamic-only — the environment is dynamic state, read through $env.

  • supersededmodes-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.

  • supersededreduced-authority-witness — a reduced-authority witness made the capability chokepoint a type.

  • activexdg-resolver-consolidation — one XDG base-directory resolver; exhaustive transport walks.

  • activeexec-authority-partitioned — exec gets a partitioned ExecMap; the two capability folds stay separate.

  • activecapability-stage-collapse — collapse the syntactic/resolved stage split into one always-frozen Capabilities; freeze at decode, the xdg guard a per-profile invariant.

  • activewitness-collapse — the reduced-authority witness collapses to free capability::check_*(&Context, …) functions; a module boundary, not a typestate.

  • proposedstateful-handlers — a handler frame threads a state value across interceptions; a fold, no continuations.

  • rejectedrelated-borrowables-rejected — duplicate-label lint, --effects listing, record restriction, effect rows, capability boxing.

  • activesession-scheme-continuity — turn schemes persist into the next turn’s check, living on the runtime binding (1/4 of the one-mode-engine series).

  • supersededhandler-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-Unit value.

  • supersededir-pipespec-annotation — the checker writes ground mode wires into the IR; the evaluator reads, never infers (3/4, landed). The per-stage Wire is replaced by a single PipeYield per pipeline in pipes-are-positional-byte-wires: with no interior adjacency rule there is no interior adjacency to annotate.

  • supersededunconditional-mode-pass — the inference pass always runs; the runtime mode engine (ty.rs/classify.rs) deleted; --no-typecheck and 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.

  • activeunify-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/output pair 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.

  • supersededalias-head-defines-its-modes — a fresh alias/handler head defines its own modes (unknown head_pipe_spec yields a fresh F[μ, ν]); 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.

  • activecacheless-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; use becomes a scope-projecting wrapper over the shared evaluate_source.

  • activeesc-non-escalating-interrupt — exarch’s Esc drives ral’s non-escalating process::interrupt (the termination counter to exactly 1, never a fetch_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.

  • activeone-debug-path — one debug-tracing primitive, dbg_trace!, gated on debug_assertions alone with no environment flag; the try-caught-error echo shares the gate, and consumers of a debug child’s stderr must drain it concurrently since tracing is unconditional.

  • activewitness-hash-h-prefix — the exarch edit witness is h plus six hex so a bare witness lexes as String, not Val::Int; an all-digit digest would otherwise fail its own equal and trap the agent in an infinite edit loop (string-coercing edit-hash can’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, breaking let-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.

  • proposedraw-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.

  • supersededpure-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 | f is an ordinary pipeline whose producer writes nothing, and value composition lives in application and bind.

  • activechild-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.

  • activeevaluator-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.

  • activehost-embedding-apiBakedPrelude + boot_shell deduplicate hosting a Shell; the postcard bake moves into core, the schema-evolution hazard collapses from three files to one.

  • supersededvalue-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.

  • activeauthenticated-confinement-marker — the OS-confinement marker RAL_SANDBOX_ACTIVE is 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 suppresses net/fs confinement, and bundled coreutils reach the fs floor by running in the confined child (deep-review S1/S2/S8, A8).

  • activeper-root-turn-cancel — one root-turn Token is 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.

  • activeexarch-panic-recovery — a caught panic skips ral’s save/restore epilogues, so exarch’s one persistent Shell is poisoned and reconciled, never unwound frame by frame: the per-call IO frame (tees, surface sink, script location, watchdog scope) self-heals through run_shell’s RAII IoGuard, 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.

  • supersededterminal-foreground-ownership — the tcsetpgrp handoff is gated on owning the terminal’s foreground (startup_foreground, a tcgetpgrp == getpgrp probe), not on being an interactive REPL, so terminal-launched scripts foreground interactive children (claude, fzf); ForegroundGuard masks SIGTTOU during the parent-local restore, and parking on stop stays REPL-only. Superseded by terminal-lease, which reifies startup_foreground as a held lease.

  • proposedprovider-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 XDG config.ral is only for unusual providers (endpoint + protocol completions/responses/anthropicAdapterKind, 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 shared bootstrap::project_dir; outside cwd so the agent can’t reach it — no deny-list), loaded on startup. /model is 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 from ProviderKind::info, models from genai, protocols from AdapterKind. Slices: auto-discovery+picker → tuning → unusual-provider config → OAuth. Since 2026-08-17: that table is identity::built_in_services returning Service structs, a declared endpoint is the same struct rather than a separate arm, and every credential keys on an AccountId — one service may own many accounts.

  • proposedstructural-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, a debug_assert-only guard, a never-populated source identity). Each gets a missing type that makes the bad state unconstructable (ResolvedPath, a parent-linked CancelScope, an RAII IpcEndpoint + Tokened response, a non-invertible Span, a typed record-decode, an Incompleteness signal, 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 discipline clippy.toml already applies to paths. Staged behind the immediate point-fixes.

  • activeno-core-repr-leak-into-exarch — the host reads core’s capability state through accessors (ExecPolicy::admit_label/is_denied), never by destructuring its representation; Subcommands became a BTreeSet (idempotence by construction) and exarch’s prompt stopped matching ExecPolicy. The data-shape corollary of the host-embedding seam.

  • activehandle-settle — a finished handle has one settle {stdout, stderr, outcome: <ok: α | err>}; poll → <pending | settled> reports it as data (total, never raises), while await/race unwrap it to {value, stdout, stderr} and re-raise err (the dead always-0 status field dropped). Buffers drain once into a cached CompletedHandle; a panicked worker’s Disconnected settles as err (fixing poll-forever / race-spin); is-done total. Outcome-as-variant, the orthogonal done/ok split, over sibling ready/failed arms.

  • activetool-boundary-steering — queued prompts drain after the current assistant tool-call batch, before the next provider request. Every requested tool id receives a ToolResult before the user message is appended; same-batch agent calls can overlap, and queued input steers the next assistant step rather than skipping already-issued sibling calls.

  • proposedforce-eliminates-blocks — the surface ! should eliminate a value-producing thunk (a block, U(F α)), not a function-thunk; !$body then types body as a nullary block, so a function-bodied argument fails at the call site instead of returning unrun. The naive runtime arm is unsound — step_force is shared with the elaborator’s App(Force(Variable), args) call head — so the two force sites must first be told apart.

  • activeunify-turn-evaluation — lift one top-level turn into ral_core as eval_turn(shell, src, frame): the frame carries an IoFrame regime sum (Inherit | Capture), the foreground CancelScope, Capabilities, and lifecycle callbacks; TurnOutcome has static and runtime arms (the runtime arm carries result, eval_status, and single_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 by ral_core signal-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 the ral batch path through eval_turn.

  • activeconcurrency-detached-vs-structured — with the root/foreground split, spawn and & are root-detached handle workers, watch is root-detached but REPL-only because it needs a durable output sink, pipelines are foreground-bounded, and par remains the accepted prelude compromise: success joins every root spawn handle, while foreground early exit or first failed await can orphan the unjoined tail until cancel/one-hour ceiling/root abort/session exit. await adopts race’s cancel-aware wait loop, cancel/race loser cancellation use explicit worker teardown, forget is deleted, and exarch arms a frame-owned one hour lifetime ceiling on a shared process::reaper deadline 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.

  • completeturn-local-state — split Shell by lifetime: mobile remains the persistable computation state; turn is the installed top-level frame (Io, surface, typed foreground scope, full non-db location cursor); session holds the durable root, SourceDb, exit hints, and the host-installed builtin table; local shrinks to audit and REPL scratch. eval_turn becomes one TurnState swap 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 own session.builtins; visibility narrows around invariant-bearing state with opaque root/foreground handles and host accessors.

  • supersededbundled-tools-as-exec-images — bundled coreutils/diffutils/ripgrep heads become an ExecImage spawned as ral itself through a hidden bundled-tool sentinel; value-edge bundled heads still route HelperEval, 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.

  • activewatch-repl-builtin — a builtin a host cannot run should be absent from it, not present-but-vetoed: watch left CORE_BUILTINS for core::builtins::WATCH_BUILTIN, a one-entry slice the ral host installs through the same register_builtins mechanism exarch uses for its agent tools — registered process-wide in register_host_surface and 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 and scheme::watch stay private, only the BuiltinEntry moves (the one asymmetry). With watch admission gone from the frame, DetachedPolicy collapsed to the bare per-host lifetime ceiling detached_ceiling: Option<Duration>, and WatchAdmission/the runtime gate are removed. exarch genuinely lacks watch — 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 the watch-admission mechanism of concurrency-detached-vs-structured; the detached-root model, death-clock, reaper, and forget’s deletion stand.

  • supersededlong-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 (verb service), Regime 2 stays deferred.

  • proposedscheduled-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 a fork does not inherit them (host state, like expect_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”); plus after <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 bundled dateuu_datejiff-icu) evaluates the expression; the five-field grammar is parsed in-tree rather than pulling a chrono-based cron crate (a second datetime tree); the reaper fires it, its one action generalised from cancel-a-scope to Cancel | Run so the wakeup rides the existing daemon (recurrence stays host-side, entries one-shot); the nudge synthetic-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 (the ScheduleId pin against agent-binding-reaping was since dissolved by leases-and-budgets — the registry is the authority, schedules re-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 — so PromptQueue (a VecDeque<String>) generalises into a typed per-session inbox (source + drain-boundary tags, the inbound twin of the outbound Signal stream) 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 at check) is not an InboxMsg (data plane), per structural-bug-prevention; a shared channel is not a uniform drain policy. Self-scheduling gated behind a schedule grant authority. Persistence and a durable cron are out of scope (future, paired with long-running-work’s registry).

  • activeasync-agent-toolagent is 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 typed AgentResult through the session inbox. Shipped shape diverges from the original bimodal proposal — there is no mode: "sync" dependency edge or mode field 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 /clear generation rejection, exactly as proposed.

  • activesandbox-external-childrengrant confines 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-shaped net leaves, and offline mode must fail closed where unsupported.

  • activetui-transcript-as-graphic — the scrollback is re-projected as an information graphic whose Bertin variables (shape, value, size, hue, grain) are encoded per-Block rather 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_line earns data-ink via a ctx% value-ramp and a phase Gantt ribbon, collapse becomes graded reduction. Phases 0–2 landed: the per-Block substrate, the data-encoding rail (Move 1), and rule_line’s ramp+ribbon (Move 3); Phases 3–8 (size, grain, reduction, matrix, fidelity, projections) remain proposed.

  • supersededhost-seam-turn-observer — drive both hosts’ turns through one core entry and make the structured surface !Send so the daemon-task hang becomes a compile error; superseded by run-turn-host-loop because !Send forces Shell: !Send, colliding with exarch’s pump/Session move.

  • activerun-turn-host-loop — a turn is one synchronous, runtime-agnostic core entry run_turn(src, TurnRequest) -> TurnReport; TurnRequest carries policy (TurnIo, capabilities, limits, lifecycle, and a turn-local SurfaceSink). exarch owns the event loop and exits on an explicit completion fact, not event-channel disconnect (the invariant; as built this is a worker-set AtomicBool polled by a retained pump/drive with no tokio in the turn loop — the ADR’s select!/oneshot sketch 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; Shell stays Send, 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.

  • activerun-turn-is-host-api — the public evaluation seam is one layer: hosts call Shell::run_turn(src, TurnRequest) -> TurnReport and may name TurnRequest, TurnIo, SurfaceSink/EventSink, lifecycle hooks, Captured, StaticDiagnostics, and TurnReport; TurnFrame, IoFrame, core TurnOutcome, and public eval_turn collapse. TurnIo is host intent, Io/TurnState are materialised resources, and capture/timeout classification live in run_turn beside the state that proves them.

  • openafter-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, narrow Shell host accessors, and consider renaming exarch’s provider-level TurnOutcome. Guardrails: keep Signal/Fact/Transient (the Event/Kind names are since dissolved), keep bytes and surface separate, keep set_stdout until live-printer setup has an explicit replacement, and keep tokio out of ral_core.

  • acceptedsurface-carries-documentssurface carries 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 closed Kind enum 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.jsonl survive). 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, subsumes task + provider_error), diff (the dense composite, subsumes patch with aggregation + disclosure), raw (un-encoded bytes, the scoped “just print it” escape) — plus a card container; composition is one rule at three scales (plane stacks marks, fields nests marks, text nests roles). Core untouched (already carries raw Value; detached replay free); TaskStatus and the four bespoke line builders retire; provider_error folds into the shared fields renderer.

  • proposedsurface-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 recommended edit-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.

  • activehandlers-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). Nullary is 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.

  • fixedterminal-lease — terminal-foreground authority is one session-owned TerminalLease parked in core, with post-startup ForegroundGuard::try_acquire demanding &TerminalLease; TurnRequest separates requested foreground policy (RequestedTerminalAccess) from byte input (TurnStdin), while internal TerminalAccess::ExplicitLoan is only a within-turn loan, so exarch tools are Denied + Empty, piped ral -c can be Denied + Inherit, and _ed-tui is an explicit terminal loan. JobControl was narrowed to a process-group LaunchRole once terminal authority moved to the lease. Landed in 295fe5b.

  • proposedsame-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 fresh Shell whose SessionState is default-constructed and then re-attached field by field. Today blocks evaluate in place (with_block swaps only the mobile on the live shell) while lambdas build a child via with_childchild_ofShell::new(Default::default()) + inherit_from — a hand-maintained allow-list with no totality check, where Shell::new actively re-mints the terminal lease from a blank predicate to None, 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_status always, cwd for a lambda); the owned-Shell construction (from_captured) stays only for genuinely separate runtimes — spawned workers, the cross-process helper, the REPL aside — which correctly default to Denied/no lease. Makes the forgotten-field severance unconstructable rather than guarded, per structural-bug-prevention; refines force-eliminates-blocks (the value-level Block/Lambda elimination split is left intact).

  • proposedrepl-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, the let dependency 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, retained free_refs edges, job-table access in read).

  • activesession-lifetime-event-bus — an async agent is muted only because the event bus is per-turn (pump mints the channel() in its thread::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 stream Born/Token/Died to 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 inbox Turn::Agent). Safe because run-turn-host-loop already made completion a control-flow fact (done), not a bus state: the foreground turn must end on done even 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; /clear ages 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 via AgentOutcome::breadcrumb, so this is only about live streaming.

  • proposedagent-reply-tool — the value a sub-agent hands its parent is the argument of an explicit, hard-terminating reply call, 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. reply is a model-level tool and peer of agent, 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 ends ReadyForUser (exchange-ends-ready). Its root withholding and its nudge-once-then-Empty finish are both revised by reply-terminates-returning-agents.

  • activedeny-binding-path-commands — a name reachable on the effective PATH resolves to that command in head position, so a top-level let (or recursive definition) that would capture it is refused before its RHS runs; reachability is the pure filesystem question Shell::locate_command answers, independent of whether the active grant would admit running it. The guard is session-scope-only and deliberately narrow — nested lets, 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 partfunctions-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 by within or persistently by handle. help splits into the nullary help and the unary explain, 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, echo among 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 for handle/unhandle, superseding the vocabulary but not the content of handlers-and-aliases-are-lambdas. The rename is the unfinished half: alias/unalias are still the surface and install_alias still the API.

  • proposedsurface-carries-control — the surface sink is the language→host typed-Value channel, not only presentation: beside the render classes (a kit `card, a core io event — both terminate in a Card) it now carries a control class, `spawn-started (carrying a live Value::Handle), that exarch consumes to register the handle and arm an inbox-posting waiter — it renders nothing and cannot serialise to events.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 lets spawn notify 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 as SpawnResultTurn::Spawn, generation-gated like AgentResult. Rejects both a second EventSink and giving the worker the foreground Emitter (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).

  • acceptedsurface-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 `card to a session-lived register the focused session draws as a reserved right-hand column (the model-authored dual of the matrix); `unpin drops it. One emit arm, one viewport field, no new concurrency invariant — it reuses value_to_card and is emitted in-turn. Turns tasks.ral from the encode-don’t-stream doctrine’s counterexample into its first client. The concept page is pins.

  • proposedsync-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. surface is the sync channel (in-turn, alive, holds the terminal-lease, renders now); notify is its async sibling (post-turn, deferred, rendered at the next boundary as a fresh turn). Both carry a typed Value and 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-done through its session-lived notify at its existing settle point (tx.send), exarch’s InboxNotify pushes it onto the inbox the async agent already 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-time joined-flag check; the worker emits, it is never observed). Safe by construction: the worker holds notify (session-owned, the same class the async agent worker already holds), never the foreground Emitter, and notify cannot 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, so events.jsonl needs 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 (notify is completion-only).

  • acceptedrecording-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.jsonl sits beside events.jsonl and is fed at the one Emitter::emit seam, so recording rides the emitter rather than the bus channel’s lifetime and a muted forked child still records its whole trace. Kind::Dim becomes Kind::SystemNote because a vocabulary names a thing’s role and only the renderer names its appearance; ordinary operational notes leave events.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 deletes transcript.jsonl outright rather than folding it.

  • amendedreply-terminates-returning-agents — the gate on reply is “does this agent return”, not “sub-agent versus root”: the headless root does return, so it advertises reply on the same interactive flag 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 headless result still carried the positional scrape agent-reply-tool removed everywhere it reached. reply becomes mandatory: a no-reply finish is re-nudged within the existing budget and then fails honestly (never forced tool_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 headless result is typed string | object rather than double-encoding structure into a string.

  • supersedednon-final-bytes-are-effects — at a value boundary — a let, a forced block, a try outcome — the bound value is the value of the boundary’s final computation: eval_seq flushes each non-final element’s bytes to the visible outer stream as effects, so only a final computation that is byte-output with a Unit value has its bytes for a value, decoded as a String with one trailing newline stripped. Capture-everything is rejected for conflating effect with value (it discards length’s answer to keep echo’s line) and for needing a flag that reads whether its binder was user-named. The checker computes the same rule through a final_outputs map distinct from bind_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 in output modes that no longer exist; the boundary rule itself — final computation wins, non-final writes are effects — is exactly the ρ = Bytes ⇒ Unit value-boundary reading of pipes-are-positional-byte-wires.

  • activeshared-transport — the tokio runtime and genai clients belong to the fleet, not to each Provider: an Engine (runtime, cache_key, a transports: Mutex<HashMap<TransportKey, Arc<Transport>>> keyed by credential+adapter) is built once (Engine::new) and hung off the Fleet as Arc<Engine>, while Provider shrinks to a cheap per-agent selection (engine handle + id + model + tuning) that resolves its transport from the shared map instead of calling make_runtime() on every /model switch. Concurrency is already proven — sibling peers already ran detached against their own Arc<Provider>, and runtime.block_on can be invoked from many threads at once. The banner/ctx% chrome now reads the focused agent’s live provider().current() instead of a frozen SessionInfo, so a /model switch and a subsequent /clear cannot disagree; SessionInfo keeps only its static fields. Landed as proposed, including the Backend::Scripted no-runtime test seam (realised in place of the sketched Engine::Scripted). Since 2026-08-17: the id a TransportKey carries is an AccountId, and the flat_rate flag is Service::billing, the one authority on metering.

  • proposedagent-binding-reaping — exarch leases scratch bindings per Agent shell, 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 on Shell::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 refresh Agent::durable immediately 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.

  • supersededlong-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.

  • proposedprovider-heartbeats-and-retry-boundaries — exarch judges provider liveness by raw wire progress, not by semantic model output: Anthropic ping events become heartbeats, long-thinking models such as claude-fable-5 and claude-sonnet-5 may 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.

  • activepartial-poll-pending-outputpoll $h on a still-running handle now returns `pending {stdout, stderr} — the bytes written so far — instead of a Unit payload, cloned non-destructively from the live buffers via a new peek_buffer (the peer of take_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 the CompletedHandle cache, so the completion take_buffer stays 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.

  • fixedwindows-spawn-boundary — Windows pipeline launch gets a custom CreateProcessW layer: 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.

  • activesubagent-memory-modes — sub-agent spawning splits into two model-memory contracts: amnemon is tabula rasa, while mnemon imports the parent’s model-visible context, reuses the parent’s provider selection for cache locality, and appends the tool call’s prompt as the fresh final user prompt. Both keep the same shell snapshot, permission meet, detached drive, and inbox return path; AgentLog drops any unanswered parent tool-call frame before importing context so the child never inherits a dangling protocol.

  • activespawn-fuel-ceiling — every Agent carries fuel: u32; the trunk starts at SPAWN_FUEL = 3 and each fork spends one unit on the child. A new Gate::Spawns axis withholds amnemon/mnemon/commit/verify_commitment once fuel reaches zero, so a delegation chain terminates by tool absence rather than recursing forever — the same silent-gating shape reply/Schedules already 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.

  • supersededprotected-commitment-pinscommitment:* is a protected pin prefix: ordinary surface writes/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 separate reply obligation, but quiet while a verifier child is still running. commit accepts a key and a free-text description and launches an amnemon writer, opening the pin only on a matching structured card with at least one criterion; verify_commitment accepts only the key and launches an amnemon verifier, clearing the pin only on a matching pass verdict — both launch-only and always-asynchronous like amnemon/mnemon, settling on the host’s own thread; /clear still clears them as part of the session reset. Superseded by names-and-schedule-labels, which deletes the feature whole.

  • activeexec-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 git under a layer granting /usr/bin/ — so Seatbelt denied a spawn ral had already run. admitted_literal_paths now draws candidates from the raw union of literal keys and keeps only what evaluate_exec admits; a bare git: Deny projects 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.

  • activeper-agent-eval-cancel — cancellation reaches the eval layer: only the signal-facing session publishes the process-global signal slots (SessionState::publishes_signal_slots; fork_session clears 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 own DurableRoot (Shell::cancel_handle, carried as eval_root on the entry) alongside its Token, so a cancelled agent’s in-flight ral eval unwinds at the evaluator’s poll points (~100 ms) instead of grinding to its timeout_secs wall. The trunk’s entry carries an interrupt-only reach (eval_root: None, via EvalReach::interrupt_only), so a registry terminate on 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).

  • activecancel-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, and agent-cancel, which keep cascading. The drive-loop Token carries a CancelCause and is read two-valuedly at the park — is_cancelled(), true for any cause, still drops the in-flight turn, while the new terminated(), true for any cause but Interrupt, is what ends a non-Held agent — 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 one Held node to every tab through a single-entry AgentRegistry::interrupt with no descendant walk — the trunk included, alongside its ambient-path raise_interrupt.

  • activebranch-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 withholds reply, and conversing is derived from the tool view — returns() reads whether the agent holds reply, never its position — so parking, the reply-nudge, and the advertised tools cannot disagree (agents). One concession buys the whole minimal cut: a trunk /clear clears branches too, so a reaped entry reads !is_live and quiesces instead of parking Held on 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 an AgentResult into the trunk’s context; surviving the trunk’s /clear is given up deliberately, and /close is the one command admitted off the trunk.

  • activesession-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, /clear generation, /resources probe. 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/disownbg is promotion, disown is 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: REPL jobs folds over stopped groups and detached handles (healing the & wart), fg/bg stay pgid-typed, await is the handle’s fg; deep fusion (a Stopped HandleState, terminal semantics in await) is refused as two implementations behind one name. Accumulators (viewports, bus, inboxes) stay probe-only: no capability, no listing. Graduates to a design/residency page once accepted.

  • activesignals-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 CancelCause on the published cancel slots — SIGINT → foreground Interrupt, SIGTERM/SIGHUP → root Terminate (new cause, message “terminated”, exit 143, SIGTERM-first teardown) — process::check polls only the scope tree, and SIGNAL_COUNT is demoted to the escalation ladder (ESCALATION: third delivery _exits; interrupt()/is_interrupted() deleted). RunningChild::wait loses its park_on_stop blocking 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.

  • supersededsession-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.

  • supersededprojection-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.

  • supersededace-free-fs-confinement — the ported DACL tier stamps an inheritable ACE per fs prefix and SetNamedSecurityInfoW propagates it to every existing descendant, so confining one command under a grant over cwd: is O(files under cwd) — 120 s+ on a repo with a target/ (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.

  • proposedvm-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.

  • activeagent-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 open type/grant variant 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-free AgentRegistry::register NameTaken) and a schedule’s its label (schedule answers [label, next-s], unschedule <label>; the sched-<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-cancel resolve by name, closing the silent cross-family id no-op an unschedule <agent-id> once was), while internal AgentId plumbing stays. amnemon/mnemon survive only as the type field’s two memory modes. The protected-commitment feature is retired whole — the commit/verify-commitment builtins, the commit-open/commit-verify desk arms, CommitmentIntent/CommitmentSettle, the commitment:* projection, and PinKind — leaving the pin register as the plain digest mirror plus the host-owned, write-protected services ledger 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’s next-s catches 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: the services ledger 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.

  • activeharness-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 reply cannot wear the block a ral call mints: an act block answers false to observation() 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 stamped 1); 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 — every agent spawn guard — draws nothing at all, because a spawn that never happened is not an event. Since amended: the desk’s recording unified onto one subject field feeding both the rail row and the audit sentence, which schedule’s minted sched-<n> default could disagree with; the label is now mandatory, so the two readers never diverge.

  • activetotal-wait-status — Unix wait results use rustix’s transparent, total WaitStatus through distinct pid/pgid and blocking/polling funnels; the doors own EINTR retry and NOHANG optionality, ECHILD remains an error, Pgid admits only positive identifiers, and neither negative-pid encoding nor fallible enum decode reaches lifecycle code.

  • activesynod-is-a-second-product — synod is its own crate and binary depending on exarch as a library, not a fork and not a --profile inside 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 shared agent-core is 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 three pub promotions in exarch (prompt::render, prompt::host_section, Agent::root), now a reuse boundary under maintenance obligation, with host_section — a developer’s git-and-cwd snapshot — the one expected to be withdrawn first.

  • activesurvives-exit-is-its-own-verbservice is durable within a session and cannot be made durable beyond one: the worker’s external child is setsid’d but its pgid is recorded by the parent (core/src/process/signal/unix.rs:365-371, stored at child.rs:180) and signalled directly at teardown, so leaving the session severs only the tty and buys no lifetime. Empirically forced by terminal-bench 2026-07-25__02-04-52, where exarch’s only two zeros are the two tasks needing a live listener at grade time — kv-store-grpc refused connections (errno 111) ~2 s after exarch exited, having served RPCs seconds before; the same model under a bash harness kept its server alive with nohup and, 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 — as detach, a distinct verb, never a mode of service and never a knob (two handle types, two observability surfaces, no shared code), born by double-fork so the survivor’s pgid is never observed by RunningChild, with all three standard descriptors on /dev/null and 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 the DurableRoot cancel 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. No Handle, 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/service into spawn options) 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, and service all produce the same kind of Handle” is the diagnosis, but the defect it names is that the verbs don’t say which axis they vary (output for watch, time for service, ownership for detach), not that there are too many. detach over daemon because 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, so docs/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 at ral/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-parent is a flag this repo passes rather than a property of confinement, so the engages_sandbox gate is gone, a survivor is confined for life by the frame that bore it, and the authority is the detach: dimension this page guessed at.

  • activewindows-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-served Devices.Plan9 share of the granted folder, one AF_HYPERV socket, 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/c and binfmt_misc Windows interop, which is the negation of “one folder and nothing else”; §2’s WMI fallback went unbuilt. Amends dev/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 are LoadLibraryW’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 (WireStream is UnixStream/TcpStream as std’s owner of a connected socket, no claim about the address family) so synod’s control_seat loses 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 — HcsGrantVmAccess is deliberately not called on the user’s folder.

  • activewindows-machine-broker — synod must install from an ordinary .msi and then run with no permission its user did not already have, so the privilege Hyper-V demands moves out of the application and into a LocalSystem service 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 in service.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 a LocalSystem service checking as itself could read everything and would mount one user’s documents into another’s guest; and the control socket crosses by WSADuplicateSocketW aimed at GetNamedPipeClientProcessId’s answer, never the client’s word for its own pid. The BootBootedAdopted handshake 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. detect prefers 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.

  • activeguest-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 with Path::components rebuilt /work as \work on 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, \tmp against fs read denied by grant: /work, which the agent diagnosed off its own prompt). fold_dots is deliberately not changed: its separator reconstruction is correct for a host path and is_foreign_rooted depends on it; the fault was applying a host kernel to a guest path, one field over from where MachineSpec::resolve had already moved absoluteness into the guest’s namespace (starts_with('/'), never Path::is_absolute). Constraint recorded on the new door: such a prefix must not be reduced on the host, since FsPolicy::meet re-mints through PrefixSet::surface and would fold it straight back — unreachable in synod, whose trunk runs fuel: 0, and correct inside the machine where a nested grant is reduced by the right kernel. The instructive half is why the tests were blind: the_policy_admits_the_guest_namespace_and_denies_the_host_one runs the real grant through ral’s real gate but runs it on the host, so both sides folded wrongly in the same direction and path_within is 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/home cross unfolded through Frame::Attach, guest_path is never joined on the host, deny_paths and exec.dirs are empty. Found by running the installed product, not by CI.

  • supersededcancel-slot-leak — the signal-reachable cancel slots publish a borrowed pointer into a run’s cancel flag, and request loads 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”) and RunGuard’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). publish now leaks one strong share of the scope’s Arc — 32 bytes per publishing run — making every published flag immortal, the same move exarch’s Token slot already makes; the stale-cause symptom (a freed byte re-read as a spurious cancelled/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 spurious cancelled in the parked enquiry two runs in three, and unserialised publishers make an engine cancel miss its run and wait out a 20 s ceiling.

  • activecancel-is-a-join — cancellation is a join-semilattice (CancelCause totally ordered, cancel a fetch_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-lifetime AtomicU8 cells (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 — CancelSlot and its Drop, publish*, the dereferencing request, both AtomicPtr statics, every unsafe in cancel.rs, foreground_cancel_cause, SessionState::publishes_signal_slots, the RunGuard slot fields and drop-order argument, and cancel-slot-leak’s leak — and retires the delivery failures it measured (a spurious cancelled/130 in the parked enquiry; an engine cancel waiting out its 20 s ceiling). Routing is by minting, not by a session flag (spawn_thread builds workers from a fresh SessionState, so a boolean was never the discriminator): DurableRoot::signal_facing folds the root cell, ::foreground folds whichever of the interrupt cell its root does not already fold, ::worker folds neither directly — so a detached worker hears SIGTERM through its parent and cannot absorb a Ctrl-C, by the shape of its fold. Shell::new mints deaf; each primary host boot calls one Shell::face_signals; fork_session is deaf by construction. One private fold, with ScopeNode, its flag, the hears bits and both cells private to cancel.rs, is the structural enforcement bought. REQUESTED_ROOT is never spent — closing signals-are-causes’s idle-SIGTERM residual — and REQUESTED_FOREGROUND is 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::enquire takes the run’s &CancelScope, so a parked enquiry also sees reaper deadlines and cancelled handles. exarch’s per-exchange Token slot is the same alias pattern, left for the same cure.

  • activecancel-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: AtomicU64 ticks 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) — and ScopeNode::hears becomes 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, the RunGuard gate, and overhearing/overhear_signals are 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 extent RunGuard’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’s DurableRoot (Shell::join_session, closing a cancel_handle reachability hole), and hear-without-spend stops being a category, since an interrupt older than every frame the aside mints is simply unreadable from it.

  • supersededthe-guest-gets-a-network-not-a-verb — the single fetch-url verb that was the guest’s whole egress surface is retired outright for a real network: a tun whose only peer is guest-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 the HdvCreateGuestMemoryAperture seam, not availability), CONNECT without 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 clone is off the shipped read-only default; the plain-English jargon guard moved from the retired verb’s refusal text to guest_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 --user as the one install path a fresh-UID jail admits), the 240/minute rate cap being sized off one pip install and not a measurement, how much of a logged request path a review surface should ever truncate, and that reqwest’s blocking client has no read_timeout to bound a stalled-but-open transfer.

  • activeone-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 an http::uri::Authority rejecting IP literals and every port but 443, checks the lowercased name against NetPolicy’s exact hosts list, resolves it once, discards every non-public address, dials and pins the vetted SocketAddrs, then copies bytes unparsed. Rejects keeping the intercepting proxy — its session CA, rcgen, rustls, rustls-platform-verifier and reqwest bought 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, and rate-per-minute are hard errors; the once-per-name blocked card retires with the interception it depended on, leaving the audit ledger’s single Tunnel record 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.

  • activedetach-under-a-grant — closes the sandbox question survives-exit-is-its-own-verb left open, and closes it the other way: detach under confinement was never impossible, it was blocked by a flag this repo passes. bwrap’s --die-with-parent (core/src/sandbox/linux.rs) is PR_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’s prctl and 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 at execve and belong to the process, which only_the_parent_death_tie_distinguishes_a_surrendered_launch asserts by diffing the two argvs; and macOS never had the problem at all, since sandbox_init is applied in-process and the target execved in place, one pid with no supervisor. So Ownership::{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 becomes detach: Option<bool> on the capability lattice, folded at the call by GrantStack::permits_detach and not in SandboxProjection — 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_sandbox existed 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 about pid, wanting one run on Linux.

  • activeexec-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 — so freeze_exec_map stats 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', since Subcommands(∅) 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 explicit dir: sigil was rejected as the larger change to a convention that reads correctly once it stops being silent.

  • activepath-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 name ral.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 — SetNamedSecurityInfoW walks 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 SIDs session::confine mints into its token, so attenuation still shrinks-only and a deny_path is 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 through cap(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/gc tooling, 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_PROTECTED holes, ≤3 ACEs per prefix, token capability-array limits) is open before it is called settled.

  • activeboot-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 wrote ral.net to a guest whose Boot::read predated 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.rs prints the constant and nothing else; vm-image/build-boot.sh compiles it, in the same cargo invocation and from the same checkout that produces the initramfs’s ral-daemon, into boot-manifest.txt’s boot_contract= line — a grepped source line or a hand-kept number would record exactly the drift the number exists to catch; synod/build.rs puts that manifest to boot::check_media and exits 1 with one sentence naming both numbers, the file, and just guest-boot, ral-daemon being a build dependency because the comparison is the build’s business and synod’s own code never asks. Three refusals, not one (numbers differ · no boot_contract= line at all, so media of unknowable vintage · a line that is not a number); absent media is deliberately no failure, since cargo check must 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.

  • activeguest-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 LocalSystem service (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: stdout for --console, a per-machine synod-console-<id>.log in the one cache the backend may write and a service can reach, and a Tail ring the failure quotes; a dead stdout drops 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 one dialled bool, since a failure named its log in its own sentence and so has a reader still to come. console_says answers 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 and broker::VERSION stays 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.

  • activesession-disk-outlives-its-machineStopped is the compute service’s word about the machine, not the worker process’s word about its files: vmwp holds 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 real C:\ProgramData\Synod\Machine. remove now retries every REMOVE_PULSE until REMOVE_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; release writes one stderr line naming the file, its mebibytes and its fate rather than raising an Error, because the same stop runs from Drop where a Result is 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::new sweeps: 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 than ORPHAN_AGE is never asked for). The sweep is structurally incapable of naming rootfs.vhd, its marker, or a wrap in progress — session_disk_epoch parses synod-session-<pid>-<epoch>.vhd and 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_AGE is an order of magnitude rather than a measurement, and whether the macOS backend owes the same sweep is unexamined.

  • activeone-walk-one-anchor — a PATH search is one traversal, from one anchor, yielding one answer. The anchor becomes a SearchCwd whose only constructors are named for provenance — Context::search_cwd (the within [dir: …]-else-cd precedence), Resolver::search_cwd, SearchCwd::of for a front end holding Shell::cwd, SearchCwd::nowhere — so ctx.dir no longer typechecks where a walk wants “here”, which is what let dispatch anchor to an unbound override while vet’s own probe anchored to the cd-mutated cwd. The 126/127 verdict stops being a second walk: path::search returns PathSearch::{Executable, FoundNotExecutable, Missing} from the traversal that produced resolved, CommandIdentity carries it, check_existence pattern-matches it and takes no context at all, and file_exists_on_path is deleted — there is nothing left for walk and verdict to disagree about. An empty PATH element never means the cwd, uniformly and not cfg(windows)-gated: POSIX’s implicit-.-on-PATH is a forty-year-old foot-gun and a trailing ; on Windows is noise no user authored, so honouring it would make every file of every cd’d directory a command; . still says what . means. And %PATHEXT% appends rather than replaces, so build.ps1 no longer resolves to whatever build.exe sits first on PATH. Together these turned build.ps1: permission denied (126, about a file no walk had resolved, with CreateProcess never called) into an honest command not found. A textbook instance of structural-bug-prevention shape 1, the path authorised ≠ the path used.

  • activelaunch-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 from std::env::current_dir() and threads by value into policy::for_invocation’s ceiling, bootstrap::project_dir/log_run_dir, prompt::assemble’s AGENTS.md/skills discovery, and /export’s path resolution, while the live shell seeded at that same spot drifts with every cd the model issues and none of those consumers re-reads it. A desk child reads the same rule from its own side: agent-start narrows policy::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” — then Seat::identity fixes that reading into the child’s own seat, which /clear rebuilds from verbatim rather than probing again. One rule, read from both ends: grants freeze where the agent was started, so re-freezing on cd would silently re-anchor authority nobody re-granted. Companion, at the exarch layer, to capability-freeze’s cwd: sigil rule.

  • activebundled-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 empty env_overrides — which no booted shell has, since seed_default_env_vars installs HOME/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.

  • activea-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::Native in 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, so map $round is 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 (echo and detach) — 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 carried cd and the REPL’s fg/bg/disown across 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 therefore env → handlers → external with 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; _type and the override slot after it are both gone, and a builtin’s type rule is a scheme factory with no second arm to choose. echo leaves the elaborator, which keeps exactly one name-keyed rewrite — exit/quit’s zero-arg argv default, deciding nothing about resolution.

  • activeone-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 leak force_open left and the stage-inheritance it caused); facts authored where they commit; a total projection (every seam ships a tagged `opaque placeholder, never silence — the rail’s dbg_trace drop dies); facts, never prose — with audit { }, try, ral --audit, and the exarch tool call as four delimiters over one collector (Run.trail: Some held at Shell::enter outside the catch_unwind; a recovered panic reports Static, no trail, no ending arm), the desk and the cross-process helpers as authors only — the desk host-side at the commitment arm via one Observed::Act fanned to rail row and per-call fragment, since a wire-seat cancel parked in enquire can unwind a builtin whose act already stands. Worker births become presence-in-trace (Observed::Worker filed at spawn_child after 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 — Stopped draws nothing, job control keeps bindings. The ending becomes a literal sum, shipped as two Ending types along the RunReport/Report seam (live Error/Value engine-side, rendered string on the wire) with render_ending the one lossy projection; transport::Break dissolves; one PROTOCOL_VERSION bump (5 → 6) covers the batch. Rider: schedule’s label is mandatory — one subject field feeding two readers could not hold both the caller’s absent label and the registry’s minted sched-<n> — carried as amendments on agent-names-and-schedule-labels and harness-calls-are-acts.

  • accepteddepth-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_scope only reserves an id and queues the scope, InternCtx::finish — the table’s sole accessor — drains the queue (the queued Arcs pinning interned pointers against reuse; the decoder needed nothing, having never trusted id order). Teardown trampolines: Closure::drop (via Env::dismantle; on Binding until 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 iterative Drop for Env was implemented first and rejected by measurement (O(chain) per env drop turned scope_escapes from 14 s into 11+ minutes), and ownership-traversal in Binding::drop rejected 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.

  • activea-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), with longest_dir_match taking the same split down to directories — allow_dirs against the narrow set, deny_dirs against the broad one — so a symlink can no longer wear an admitted name to reach a denied binary, while an allow on a target still does not reach a link the grant never named. One strict realpath(3) per external dispatch, anchored at cwd_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 (reasonable flags cwd:, /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.

  • activeexchange-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 0 to SPAWN_FUEL (3, shared with exarch’s own trunks), and exarch::headless::converse_settled drives the exchange: the ordinary attend loop under a park policy answering HeldByChildren while children live, Held/Engaged/UntilCancelled never reachable from a synod trunk by construction. Supersedes the “never a fleet” half of the old fuel: 0 comment at synod/src/session.rs; synod is the caller the engine protocol’s wire-side spawn shape was left waiting for.

  • activestore-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_ns beside the hash, reused unopened on a stat match older than the reference checkpoint’s own taken_at_ms — git’s racy guard, stamped at walk start), a walk tolerates a living folder (WalkError::Vanished, hash_fileOk(None), never an abort), and the large-folder warning — with a free_bytes free-space sentence — fires off a stat-only manifest::measure before a byte is read, Conversation::begin no longer joining the before-checkpoint but spawning it as a Baseline that exchange settles 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), end wipes it, and sweep_stale at 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 by cargo clean). Rejected: an APFS clonefile/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).

  • acceptedsynod-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 .zshrc to export from. Two sources in one order — the computer’s credential manager first (provider::keychain, one keyring entry 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, and vault() answers where secrets actually land in a sentence the window prints verbatim, the fallback being an owner-only file through provider::secret_file::write_private — the ChatGPT token store’s existing care, extracted so one Windows DACL implementation serves both callers. Endpoints live in synod’s own providers.ral through a generalised config::load_declared/save_declared, carrying addresses and never keys, a quote in a name being asked about rather than escaped. CredentialStore gains 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.

  • activemodes-solved-by-deferred-joins — one deferred constraint store, drained by the boundary that owns a variable rather than by whatever let a program happens to place; conclusions applied early because a route only moves Var → ground, ground-directed collapse before equation, principality up to variables shared across one binding. Narrowed in place: of the three constraint kinds it named, Join and Alt are gone with the channel ends they merged, leaving the arm-result join alone — the architecture unchanged, its subject matter two-thirds smaller.

  • supersededbyte-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.

  • activepipes-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 be F[ρ] 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 _type probe are deleted; the IR carries one PipeYield per pipeline — Last or Unit, the last stage’s route committed to syntax, so no route reaches the evaluator.

  • activecase-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 the case — 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 no Capture, and retires the runtime unhandled-tag miss. try keeps its first-class handler, because its branch set is never opaque while a case’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 an if-like branch — the recorded status inherited, every context mutation persisting, an unselected arm’s hoisted effects no longer run.

  • activea-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-captured retyped every captured let (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 — so M | from-string still means whatever their session says it means. Name reservation was refused as the non-compositional alternative.

  • activedepth-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.

  • activeno-value-has-an-optional-argumentArgSig::Optional is deleted, leaving Exact and Any: an entry declares its arguments or it takes an open argv, with nothing in between. cd becomes Exact of one String and the REPL’s fg/bg/disown Exact of one Int, so all four cross the arity partition into natives — $cd and $fg exist, a bare head is no longer intercepted (^cd still reaches a handler, as ^jobs does), and echo and detach are the only base frames left. Bare cd is a T0050 arity error rather than $HOME, and a bare fg/bg/disown an error rather than the most recent job — a deliberate break with bash. at_most leaves the BuiltinArity diagnostic along with the Optional arm and the error gains the builtin’s name, so `cd` expected 1 argument, got 0 replaces a nameless count — an improvement for all ~80 builtins rather than a special case for two.

  • activeargv-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 ArgSig is deleted and echo and detach leave the builtin table for the base-frame manifest, typed List String -> Return(Bytes, Unit) and List String -> F Any. Both argv boundaries already had a type and neither was written down — List String inside, bytes at the OS call — so the manifest is authored as two rather than one table read twice, and fixed_arity, native_value, seed_natives_and_base, and derive_sig_scheme all 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 settles elem at String instead 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 deleting BuiltinSig and 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).

  • activeexec-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 is docs/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), with of_value for the spawn, of_ty for the checker, and one remedy per shape so both refusals speak one language — and both maps are wildcard-free, so a new Value or Ty constructor 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.

  • acceptedcontext-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 keeping transcript.jsonl beside the log; one-seam-one-log generalises its fold law from the model view to the whole log, and a-trace-is-a-fold retires transcript.jsonl rather than keeping it beside record.jsonl.

  • acceptedone-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 sealed Protocol class, the resumed scrollback over Display/Forensic commits authored worker-side (the chopper and SurfaceBuffer moved upstream of the seam), user.log a regenerable render. events.jsonl retires; a pre-plan session refuses to resume with a named error; --resume finally 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 legacy Kind stream through a transitional Signal::into_event bridge — with four named blockers (unrecorded live chrome vs. wholesale sync, no UI-thread recorder for SystemNote/ModelChanged, errors that cannot record themselves, ContextEdited’s missing notice commit), and transcript.jsonl still 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 own Entry.at_unix_ms rather 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 one Delta::{Say,Think}, since two independent callbacks cannot express that a run ended where the prose began, and Display::Thinking gives up answer_chars because a commit preceding the prose cannot carry that prose’s mass. Corrected 260816: a block is the run of consecutive Display records 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 whole Unaccounted arithmetic 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.

  • accepteda-trace-is-a-fold — a session keeps one durable record: transcript.jsonl is deleted outright rather than retired to a filtered projection, because an operational view is a fold of record.jsonl like every other durable artifact. Its three unique facts move to truer homes — a per-line clock to the log line’s own private Entry.at_unix_ms, a child’s born/died to its own SessionStarted/SessionEnded bookends, stop_reason to Protocol::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.

  • activea-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 (GetProcessTimes there, None here, where the signal already names the case), compared by the pipeline collector, the only party holding both handles, which now walks its stages peekable so that the next stage is this one’s reader and being final is having the caller for a reader. CommandFailure::from_outcome takes that ReaderCaller or Stage { outlived } — in place of an is_pipeline_non_final flag, 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 (0 for bundled uu_yes, 1 for a GNU-style write-error report, 3328 for the MSYS2 yes.exe on a Windows runner’s PATH, 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.

  • acceptedthe-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.log becomes 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 /export reads 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), so Viewport::sync rebuilds 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 last ral script 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), and context_floor still grades against cumulative session input rather than the last turn’s prompt.

  • activea-failing-cleanup-pre-emptsguard 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’s Err logged as guard: 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 by try and absent from every audit tree, reported only in prose on an unstructured stream. Log-and-continue keeps its spelling and loses its privilege, as guard M { try N { |err| … } } or guard 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 plus render : Err → 𝔹* the clause had mortgaged are owed to nothing else.

  • activediagnostics-are-a-builtin1>&2 leaves the surface, because a message to the human is not standard output pointed somewhere else: warn : String → F[Value] Unit writes the string and a newline to the stderr sink and returns unit, a table entry beside surface whose route stays Value, 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>&2 does 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’s scan_redirect_gt, which sees both descriptors and knows a bare > means fd 1, and names warn and 2>&1 both, since a program holding the exchange backwards means that one. 2> f and 2>&1 stay: an external command’s stderr genuinely needs binding and filing. install_sink_redirects narrows 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 the cross! frame and the crosses constructor of AnswerErr, whose only client this was, and its two routing walks stay one-directional — the surviving rejoins continues on the tail through route, which never calls back — where crosses would have forced mutual recursion and mutual induction on every proof over them.

  • activea-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 TerminateProcess on 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 -1 and a SIGPIPE-ignoring Python producer are both forgiven every run, sh -c 'exit 1' | head -1 keeps its 1 every run. !{ yes ; exit 5 } | head -1 flips 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 or spawn. Supersedes a-producer-that-outlived-its-reader’s causal SIGPIPE/exit-order-clock split: one rule, both platforms.

  • activea-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 (Int its digits, Float the shortest round-trip decimal, always keeping its point), so canonical numerals cross byte-identically and the rest normalise on output (0077, 1.501.5, +55, .50.5, -00); 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, 1e300 printing as 1.0e300 — so printing then reading is the identity on numbers; the grammar was deliberately not widened, 1e6 staying 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_word consults the grammar, so a numeral-shaped String re-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.10 is the numeral 3.1, so version-like tokens are quoted. Corollary landing beside it — unit stops being a word literal, () becomes punctuation that prints as itself, since a literal whose printed form is nothing cannot have one spelling.

  • acceptedthe-evaluator-steps-closuresthe 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 Shell minus its lexical scope; one step, one arm per rule of the plan’s tables. Gone: the recursive tree-walker, the ambient shell.mobile.scope pushed and popped around every scope, the trampoline with its Tail/Raw/Control currency and every absorb_tail seam, Value::Lambda/Value::Block, LetRec, Seq, Mobile. M to x. N puts ⟨N, E⟩ in the To frame before M runs, so a binder’s extent is structural; a; b is a to _. b and a block is a right-nested binder chain. One thunk value and force(thunk M) = M — no bracket, so a forced block’s cd persists like a lambda’s. Two terminal shapes (Value, Lambda) are a type. Recursion is an n-ary rec with a projection, not a record fixpoint. The environment is a three-tier finite map (natives, frozen prelude, persistent bindings) and is not the store; Context stays store, changed only by frames holding undo. The top level is phrases and a Define extends the session environment for every later phrase, installed as it lands; source is a form worth (); use runs under the session environment; $CWD and friends are Observe computations, their names reserved. The cap counts frames (100 000) and reserve runs before any effect. The prelude is invariant by construction — every phrase a Define of a value, the nine ansi-* constants replaced by styled <style> — so the wire ships only the bindings tier. Pipes are Pipe nodes 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: a bind into a large persistent map copies a node path (B5/B7 slower), the representation trade-off recorded in the plan’s §9.

  • acceptedreply-parksa returned value is a fact the registry holds, not a message the parent reads. A child’s reply deposits its faithful FOValue on 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] with agents `read <name> — the one agents tag that answers a value rather than the roster, bindable and idempotent. The standalone reply builtin dies; the child hands up with agents `reply <value>, and the family’s scheme becomes ∀α. … → F α (the pin-read precedent), the price of read living in the one fleet verb. Roster rows gain state (`busy | `waiting-on-agents | `replied | `waiting) and idle-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.

  • acceptedagent-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 — Agent the Arc-shared public half, Avatar the private half every method runs against — with liveness the avatar holding the Arc, status single-writer, the exchange clock on the inbox, and up strong/down weak on the tree. AgentRegistry (34 methods, ~2000 lines) becomes Fleet { names, roots, lease }. Superseded in mechanism, not decision: reply-parks’s “the registry holds the reply” is now “Agent::status holds the reply”.

  • acceptedthe-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 owned genai wire values are manufactured at one door, provider/wire.rs, at most once per HTTP attempt. Diagnosed from a live 36-session fleet run (~12 MB record.jsonl → 2303 MB peak, pure MALLOC_SMALL churn): up to three whole-history deep copies per deliberation step, the retry-closure clone buying nothing since genai consumes a ChatRequest by 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 retroactive omit/repair_end flags live only on the uncached tail renderer. Sealed(ChatRequest) is deliberately not Clone; ChatRequest is named only in wire.rs. The genai floor stands: one whole-history copy per HTTP attempt, ChatRequest being consumed by value.

  • activestatus-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, its WireShell mirror, and its slot in the panic checkpoint are deleted. A Bool is data at the process boundary too: a run that returns exits 0 whatever it returned. Rejected: a clause mapping a returned false to exit 1.

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 F with 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[ρ] A supplies none: Value is 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 decide Capture and 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 the Program sum) that is the only evaluation seam, the host/boot/run split, 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 / Comp call-by-push-value IR, and Toplevel { phrases: Vec<Phrase> } above it; Bind/Phrase::Define carry the checker’s scheme, Rec is an n-ary generalisation of Levy’s rec x. M, and Pipeline carries one non-optional PipeYield plus 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 each Phrase::Define, one PipeYield per pipeline, per-stage value types, Capture nodes) from one SessionSchemes seed; a stage is forced to Return shape, 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 in typecheck/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-tool exec 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 for file-* 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 and CORE_BUILTINS, plus bundled coreutils/diffutils/ripgrep heads dispatched in-process via uutils_invoke; registry/seeding here, runtime exec-image dispatch on runtime.
    • shell-state — runtime Value, the surface sink, handler stack, and the Shell state split by lifetime into env/context/Io / SessionState / LocalState, with a run’s invariant half riding beside it as the Mooring; a scope entry is Binding { 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 carries WireChannel frames; EngineSeed reifies the scrubbed fork for a wire-seat hatch, with fork_scrubbed removing 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), the Host trait every dispatch rides, dispatch_to_report, IdentityTransport/WireTransport and Severed, the --engine process in engine.rs, and the wire-seat hatch in hatch.rs.
    • diagnosticsSpan/FileId byte-range positions rendered directly via ariadne; the layer also exposes byte_to_char and the type-error label so an external surface can draw the same underline; ANSI gating; exit-code hints.
    • prelude — the embedded prelude.ral standard library.
  • repl — the ral binary: 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.
    • startupmain.rs process dispatch, cli.rs argv → Mode (--surface frontend, clap-derived argv terminator), batch.rs execution through core’s framed run door, the annotated-prelude bake, platform glue.
    • loop — the Session state machine over an owned IdentityTransport; one run is a Program::Source dispatch through protocol::dispatch_to_report, seeded from the live session; the selectable frontend, prompt/theme/rc.
    • frontend — the Frontend trait 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::Hook runs, 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; fg resume gated on a held terminal lease.
  • 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 ral tool, 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-writer Status) plus an Avatar (the private half every method runs against), live exactly while its avatar holds the Arc; the thin Fleet is { names, roots, lease }, two Weak doors 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, the MAX_STEPS ceiling, sub-agent forks in two memory modes), the construction-fixed returns bit, HeldByChildren, the fuel spawn budget, the owned hot-swappable provider, dynamic focus, and the subtree cancel cascade over Agent::parent/Agent::children (up strong, down weak). A wire-seat trunk’s agents `start remains one exchange: the engine binds a one-spawn listener, the desk reaches it through its Dial capability, 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 Source run dispatched via dispatch_to_report against the agent’s seat transport (the in-process IdentityTransport, or a wire engine’s WireTransport), under a pushed grant frame, seeded from the live session, with Denied terminal 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 ⊓ base for a spawned child), the six bake-in profiles, and restrict-file self-denial; the boundary is ral’s grant.
    • toolsral alone is the tool; spawning, messaging, cancelling, scheduling, and reply are builtins reached by writing ral inside it, answered by the per-call ExarchDesk, with tools.rs keeping only the ral entry 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, the agent.ral kit over them, and the harness verbs the desk answers (the context family and transcript, the one record-spec agent spawn 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 surface render 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.
  • 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.rs that is the only thing that drives them (one session::Conversation per 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 a LocalSystem broker service (windows-machine-broker) — ral-daemon runs 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 — a tun whose only peer is guest-net, a user-mode TCP/IP stack in a host process, gated by the destination policy defended in egress — replacing the single fetch-url verb 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 to SPAWN_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, over Machine::connect_guest — synod’s MachineDial is the Dial the desk’s wire spawn calls through (agent), and the control and net ports stay the only two the host listens on; exarch::headless::converse_settled holds 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 ral interactively, forwards everything else to /bin/sh.