Wiki index

Catalog of every page. Read this first, then drill into the pages. How pages are written and kept honest is the maintainer contract.

How this is laid out

Five layers, each with a different relationship to staleness:

• design/ — why the design is what it is: durable theory and cross-cutting concepts.
• internals/ — how it runs: narratives threading several subsystems into one flow.
• invariants/ — the hard rules, one per page.
• decisions/ — why it changed: one dated ADR per decision, status in its frontmatter.
• map/ — where things live: thin pointers into the code, stamped with the commit they track.

Start here

A guided path through the system, why before how: syscalls-are-effects → cbpv → types → the compilation ladder → the evaluator machine → grant → authority tables → capability enforcement → exarch-architecture → a run, end to end.

design/ — the why

• syscalls-are-effects — the foundational principle: a system call is an algebraic-effect operation, separated from its OS interpretation; handlers and reified continuations are orthogonal layers on top.
• cbpv — call-by-push-value: values vs commands, the two sigils, thunks, immutable bindings.
• types — Hindley–Milner with let-polymorphism over computation types F^ε A, where the grade ε says how a computation produces its result: F^p A is Returns A, and a command (an external, a builtin row that writes, a handler arm standing in for one) is F^w Unit, printed Command, so { echo hi } is {Command} and { 'hi' } is {Returns String}. A command’s value is its output: capture is one coercion, decode (capture M), placed by the type where a value is demanded of a command — a let’s right-hand side, an argument to a value-demanding function, a join (capture); a pipeline stage feeds by writing and a decoder ends the byte pipeline; an arm stands in for the head it replaces; every form that suspends a command takes a thunk and its arms join by grade.
• words — a word is one atom (bare, '…', "…", or a splice), whitespace separates words, and two atoms that touch are a parse error naming both readings, checked once at the end of every unit (end_unit) with the grammar’s attachments the only touching allowed; text is built in one visible place, inside "…", and there is no gluing. Why removing word splitting does not make gluing safe, the two gluing designs declined and the slogans that leak, every footgun met on the way (greedy identifiers, -$n, the non-neutral empty splice, spelling vs value, # and ! at a moved boundary, "!{f}[k]", string heads), and why sh-quoted input at the -c door is a different question.
• effects-handlers — algebraic effects; deep, self-masking, tail-resumptive handlers; no first-class resume. A handler reinterprets a bare external name and stands in for what it replaces, so a user arm is List String → Command (its value is its output; a ()-returning stub is admitted); ^name opts out of the stack entirely.
• grant — capabilities; authority attenuated by intersection; exarch’s sandbox; a grant is typed data (tagged places, exec targets, verb lists); directory selectors (system, the package managers) are rows of one table, with a home guard and a read floor.
• authority-tables — fs and exec authority are one structure, a table of scoped rules denoting a function from resolved requests to Belnap evidence (positive and negative support): an exclusion beats every allowance, with no specificity ranking; ↓ closes evidence to a decision once, where it is enforced. The meet is defined by ⟦a ∧ b⟧ = ⟦a⟧ ∧ ⟦b⟧ and represented as denies join, allows meet at their own subjects; an omitted axis is t in a policy and ⊥ in an extension fragment, two types; a layer reads what it writes and, looking down the stack, what it runs; allowances are frozen and exclusions re-resolve; support (carriers, linker) yields to every exclusion. The ten laws and the proof sketch, why the order of the stack matters, the per-axis representation, the read region, the two instances side by side, exec’s two languages and what the kernel is handed, worked cases, and every platform corner case (APFS, Seatbelt, NTFS, Linux casefold, 8.3 names, firmlinks, the Windows root, symlinks, guest prefixes, what the kernel cannot see) with the measurement or incident behind it.
• capability-freeze — one always-frozen Capabilities, whose places and selectors are 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 run in-process and in the OS sandbox: the in-process guard is complete for what ral dispatches, the kernel layer for what a child does on its own; “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 over plain Rémy rows, a slot being a label and a type, whose literals with a spread are updates of one base that add no field.
• records-and-maps — one runtime carrier, two static types that never unify: heterogeneous static-label records vs homogeneous runtime-key maps; the key space, which literal a bracket makes, and the indexing split on the key’s form.
• 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 a ral-written stage is a thread returning its value directly — only an external is a process (stages-are-threads). Lifetime is tail-ward too: an interior edge is dead once its reader stage has ended, and a stage feels that death at exactly one place — its next write to the edge — which is a pipeline’s one forgiven death (the-cut-is-at-the-write).
• name-resolution — where a capability lives: the layering of head names; effects→coreutils, queries→builtins, conveniences→prelude. ^name and a path head are not a fourth layer — both skip env and handlers and land on the external tier directly.
• 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.
• codecs — from-X/to-X as the typed byte↔value crossing: a decoder Returns A reads to EOF and returns a value, an encoder A → Command writes; strict structured decode vs lossy lines, split by one line rule that every reader shares.
• capture — a command’s value is its output: where a value is demanded of a command (a let’s whole right-hand side, an argument to map/filter/sort-list-by, an arm joined with a value arm) it is captured and decoded as a String, so let x = f with f = { hostname } binds the host name and !{ echo a ; echo b } yields "a\nb" with nothing on the terminal. A stdout redirect discharges (let x = to-json 1 > f binds ()), each/fold/spawn/audit absorb a command body, and a tail Run is never captured. capture M : F Bytes is total and exact and decode owns the lossy step; a failing capture flushes what it holds to the sink it replaced, and exactness is kept by refusal at the 16 MiB buffer cap.
• control-operators — the seven 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. audit { } returns a two-field report — outcome, `ok of the value or `err of the very record try hands its handler, beside trail — and nothing else: no status duplicating the host’s, no hint appended to a message. An observation is an envelope around one what whose tag is the kind, so there is no second place for the kind to disagree. Position in the trail is settlement (post-order: a command lands after everything it ran) and nesting is recovered by start–end containment, which needs no parent pointers and so survives transport. Scope-shaped delimiters whose opener owns closing, lexical ownership, processes only transport fragments, the dispatch itself as a delimiter (Run.trail), denials always recorded and allowed checks never — grant has no say — and try reading nothing, the failing name stamped by the dispatch that failed. A builtin application is not an observation: the pure fragment performs no effect, and a builtin that reaches the world does so through a door the trail already watches, which records the effect there as the `write, `read or `worker it is.
• 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. exarch-surface `` pin [key, body] writes a card `` to the focused session's reserved right-hand column; `` unpin drops it, both reached model-side through `exarch-pins` set ``/`` clear “. 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 exarch-tasks/exarch-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 forest of uniform Agent nodes under one shared attend loop, told apart only by position and a construction-fixed Role (Converses, Headless, Child { parent }), never an is_root flag. A root is a session — a fleet holds any number, each a fresh engine with its own record, opened by /new (blank) or /branch (the focused context, fresh shell), ended for good by /close, all reopened by --resume. Spawning is universal but bounded by fuel; exarch-agents `start forks a value snapshot of the parent’s scope — its serialisable fragment, each handle scrubbed to a placeholder by bequeath, the one fork both seats take (the one snapshot law) — and names the child; type picks its memory, amnemon blank or mnemon inheriting the parent’s turn table behind an Inherited link; model is `inherit or `role <name>, a provider the human bound at launch with --role — the agent discovers no model; reply is the one return path; focus is presentation, the idle lease lifecycle; the mandatory grant pushes one layer onto the parent’s stack, so a spawn narrows but never escalates (a-spawn-is-one-layer); a wire-seat trunk spawns in the same one exchange: the engine seals the bequest and names it in its enquiry, the host dials the guest daemon’s factory, and the daemon spawns the child.
• 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 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 channels by direction, by answered/one-way (Dispatch → Report, Control; Enquiry → Answer, Surface), and — for Surface — by the scope of its handler (dispatch or session), a reading Ahman–Pretnar’s asynchronous effects make exact, every payload a first-order FOValue typed once for both ends (Datum, record!) behind a closed, versioned envelope that grows only by class, never by channel; identity is the trivial instantiation of what wire encodes because there is one Engine, born once from an EngineInstaller and an Attach (construction is attach, one verdict under either carrier), driven by two carriers that differ only in the rails they lay — no front-end holds a Shell, the carrier decides fork adoption (Fork::Park + adopt_parked, Fork::Seal) with SpawnGrant::narrow_onto the one layering step, Control’s four verbs (Interrupt, Cancel(id), Terminate, Abort) mean one thing and are how every engine, folding no signals, hears its process’s, reentrancy is refused on both, and every probe is typed once as core’s Probe enum, answered by its own Event::Reading; the guest daemon is the engine factory, listening on one port and admitting only the host’s CID, 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 — lexing whose only context is the innermost delimiter (operators in $[…] a token of their own, a mismatched closer a definite error), recursive-descent + Pratt parsing, the words rule checked at the end of a unit, redirects held by the stage (Ast::Redirected), the flat AST, three-stage head classification.
• type-inference — the HM algorithm: the Inferencer, the Unifier (types and rows by Rémy rewrite), rhs_bound_ty placing the bind rule, the grade store beside the type stores, the pipeline-stage rule, stands_in for handler arms, two-pass arm joins by grade, 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-registry — builtin_registry! and its facets, derived arity, the manifest as a boot manifest seeding natives and base frames, bundled coreutils, host-layer builtins.
• handler-dispatch — the handler stack: two-pass lookup, self-masking strip-and-restore, deep frames on the dynamic context.
• capability-enforcement — the hub: a grant is data with two readers, an in-process guard for what ral does (guard::check_*(&Context, …)) and an OS sandbox for what a spawned program does (SandboxProjection::of); verdicts fold over the GrantStack’s layers, never a flattened frame; for the filesystem the two read one fold and cannot disagree; net is OS-only; the grant body evaluates locally and each external command is its own launch.
• path-judgment — ral judges the object, not the name: four stages for a read by name, and for an open the Shell::locate walk over search handles that never lets the kernel follow a link; a deny holds under every spelling, absent names included (collision_key); the discard device, DOS device names and the pinned-binary write decided before any region.
• exec-judgment — a head is judged by the program it will run, and that program is what runs; the kernel holds the same ExecRules table (Seatbelt, Landlock; none on Windows); a name veto is not a containment boundary, and nothing freezes a directory a write covers (a declared limit); how the deputy meet is built and why its findings live only in the audit trail.
• holding-a-deny — a deny must survive the filesystem moving round it: macOS pins ancestors, a Linux mount is anchored to the inode, and the path’s shape picks the mask. A deny of an absent name in a writable prefix is the one gap: on Linux a spawned program can create it for one launch (Windows carves the allowance around it, so a name made there inherits nothing granted), every later launch masks it, a planted link only widens it, and why no Linux mechanism closes it.
• linux-envelope — the bwrap envelope as the child’s whole world: its namespaces, binds of handles ral opened rather than names, the mounts rebuilt by hand where a host refuses them, pseudo-filesystems that describe the envelope, and a bwrap pinned at boot and locked read-only inside every envelope.
• confined-launch — one confinement point per platform; a warrant handed down on a descriptor no other process can write; Warrant::confine as the only road to the program, so nothing runs unconfined; Windows’ path-keyed capability SIDs; and a missing envelope blamed on the envelope, never the target; frozen allowances stamped through held handles.
• seatbelt-profile — the macOS backend as an object policy rendered in Seatbelt’s name language: two spellings per path, metadata-only ancestor chains that a search handle satisfies (the walk’s O_SEARCH), pins against a renamed parent, every deny after every allow; then build_profile and macos-base.sbpl rule by rule — exec as one SBPL form per kernel rule in Rank order, exec denies denying no reads, and the frozen admitted set, the network closed by absence (net: `offline), the named Mach doors and the three withheld with their reasons as data.
• pipeline-execution — byte edges allocated from stage position in one process group; the resolve-time StageLaunch freeze between a thread and a process, the pipeline’s value always its final stage’s, the held-open read end and the sentinel that hears a dead write and triggers the kill, the anchor process holding the pgid open on every platform and reporting what the kernel already delivered to it, heard as a key only by the pipeline’s terminal loan and all heard out before the fold, teardown as one grace signal per process through the collector, and Windows Job Objects with their spawn-boundary limits.
• a run, end to end — one top-level run for a ral REPL line, a batch script, and an exarch tool call: each a Run dispatched through a transport, entering the one framed door (Shell::run_under dispatching on Program::Source/Program::Hook → RunReport) under a hook’s registered policy where it is one.
• 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 session-owned worker with a 16 MiB-bounded buffer that lives as long as its owner, never reaped for neglect; a listing is data (workers), and worker <id> is the door back to its handle. 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; the closure’s lease renews, never the name it captured).
• cancellation — stopping in-flight work: one cooperative cause-bearing scope tree (Scope read, ScopeNode written) (ReaderGone < Interrupted < Cancelled < TimedOut < Terminated < Aborted), observed by Shell::poll at step boundaries and by sliced waits, raising a stop (Break::stopped, an escape naming its owner’s node) that no try catches, which a guard cleanup’s shield masks for the grace. A gather’s births (a gather { … }’s, or a worker’s body’s) hang under the scope it was entered in (its cradle), so cancellation is hereditary. The platform handlers translate signals into it via two ambient causes that no scope folds — each engine’s host forwards them as Control — — an absolute shutdown cell and a temporal interrupt count a listener reads from its registration and a front-end from each dispatch’s birth, so an interrupt never lands on a dispatch sent after it (SIGINT → foreground Interrupted, SIGTERM/SIGHUP → root Terminated at exit 143) — backed by an escalation ladder whose third delivery _exits; Shell::poll reads only the scope tree; per-host gestures — REPL Ctrl-C foreground-cancels and nothing else, a pipeline’s processes hearing it through the collector’s own teardown, REPL Ctrl-\ root-aborts, a key pressed on a terminal lent to a command or pipeline heard back by its TerminalLoan and struck on the run’s node (the one way a child’s death becomes a stop off any cause in force), 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; reset.rs’s reading of every convention a 429 names its reset by, and the Refused 429 whose deferred reset the terminal trunk’s wakeup resumes at; 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, each fact once: protocol, display and forensic classes feed the model and view folds, transients remain live edges, /clear and /rewind withdraw turns within the one file, and /export or exarch export renders the transcript from it on demand. The model fold is one structure (Context) holding every turn the lineage recorded and where each one is — its records in memory, or a Pointer to the file and byte ranges holding them — and every view, the provider-facing message list included, is a projection of it built on call, memoised nowhere.

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.
• term-depth — a term’s depth is not bounded by its syntax and the language limits it nowhere; every walk that recurses over a term, parse to typecheck and the printers, runs on the compile stack (compile::on_compile_stack), and a new recursive pass runs under that door too. The parser’s nesting cap bounds only the parser; unification alone carries a depth budget (MAX_UNIFY_DEPTH), the structural walks none.
• 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. A row slot is a label and a type, so a field that may be missing is not a record at all; the rule stands on there being no slot that may be absent and no term that asks whether a field is there.
• 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 stays in the context as it lies rather than being closed by a fabricated turn or replaced by a note.
• 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.
• a-failed-run-keeps-its-bindings — a top-level run installs each binding as it lands and a failure undoes nothing: a let that completed before the failing statement stays bound, as do the effects before it (docs/SPEC.md §5.6). The wall and the raise are no exception; the only rollback in the tree is Shell::enter’s host-panic checkpoint. Transactionality is rejected — a script’s effects are irreversible, so reverting the names while the effects stand would leave the model unable to name what it caused.
• 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.
• fields-are-reached-by-name — a record field is reached only by naming it in a row: selection, a map pattern, and a builtin’s own row all name what they read, and no operation reads a field the type does not mention. keys, has, and fields being typed over Map<α> rather than a record row is load-bearing, not incidental — a to-json :: [ρ] → F Str or a record-typed keys would read fields no row names and reopen an-open-spread-must-come-last. structural equality detects what it cannot name (comparing key–value pairs whole at one data type), which is why the weaker typing of a merge is unsound rather than merely useless, and why optionality cannot hide in a record’s width.
• redirects-are-the-three-standard-streams — a redirect is the sum Stdin | Stdout | Stderr | StderrToStdout over its operand, one type at every tier (parsed word, IR value, evaluated string). The fd number is spelling, eliminated at the lexer, which refuses every fd-prefixed form but 2>, 2>>, 2>~ and 2>&1; the token stream carries Redirect { stderr, op } and StderrToStdout, never a number. No tier re-widens the type, so every consumer is an exhaustive case, and a peer cannot send a redirect naming fd 7 over the wire. A list of them is Redirects<T>, a set of bindings with at most one per stream; the parser refuses a second, and 2>&1 is position-free.
• grants-judge-objects — a grant prefix carries two forms, surface as written and real with symlinks followed, and every authority is judged on real: fs on the objects the kernel touches, exec on the real path of the file a head will execute (exec-rules), composition’s evicts on the same forms the in-process guard matches. The surface is for display, never a door; a deny is judged by collision class and an allow by stored name. Held by keeping the form-blind containment kernel pub(super) inside core/src/path/, since a guard must ask on the form its check matches — the xdg: freeze guard once did not, and read a symlink out of HOME as contained.
• paths-are-shown-with-slash — every path string ral produces is /-separated on every host; core::path::show is the one place, a verbatim or device head ral cannot fold is shown as given, and paths handed to the OS stay native.
• a-grant-never-reaches-its-own-key — nothing the agent runs can read the provider keys exarch calls its model with: the key files are denied after composition, beneath every profile and every spawn; the launch-environment copy is blanked in place, not just unset, and the process is non-dumpable, so neither /proc/<pid>/environ nor /proc/<pid>/mem gives a key back. Holes, named: dangerous carries no file deny, an unconfined session can ask the vault, root in a user namespace defeats the seal.
• 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.
• await-is-the-block-run-here — await $h is observationally h’s block run at the await: the same value or raise, and its stdout then its stderr bytes written to the awaiter’s current sinks; the await claims the result, which is claimed once, so a second await fails. The residue is stated: shell state, the interleaving of the two streams, a block that spawns, a cancelled block, and exit. poll and first-settled are the two data projections, and claim nothing.
• a-worker-ends-with-its-children — a gather (a gather { … }, or a worker’s body) ends with its children: on return each child still unclaimed is claimed and awaited exactly in birth order, the first failure being the gather’s and the rest cancelled and drained within the grace; a halting body cancels and drains them; and every exit waits, within the grace, for each child it started that was cancelled and has not ended (I4′). Cancellation is hereditary: a gather’s birth hangs under the scope its gather was entered in, a run’s under the session root, so cancel $h reaches everything $h started.
• exarch-is-a-dag — exarch’s top-level modules form a directed acyclic graph, leaves first (clock/latch/cancel/card/app/skill/library, provider, record, bus, schedule, enquiry, shell_eval, agent, boot, tui/headless, cli/lib); a crate:: reference to a module that already reaches the referrer is a build break, pinned by exarch/tests/layering.rs.

decisions/ — why it changed

Newest last; the page carries the full reasoning.

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

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

• active — completion-escape-refactor — EvalSignal retired for Settled + Escape/BodyResult.

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

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

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

• active — background-tool-calls — scoped in-turn agent batching is active: 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.

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

• active — ast-stays-flat — the surface AST enum stays flat.

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

• active — infer-case-stays-whole — infer_case is left as one function.

• superseded — env-overrides-scope-overlap — env_overrides / scope overlap.

• superseded — linux-exec-confinement — path-scoped exec was unenforced on Linux; closed by landlock-exec-layer.

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

• superseded — modes-equality-constrained-shared — pipeline modes are equality-constrained, in one shared definition; the two-mode lattice it built is deleted by pipes-are-positional-byte-wires, and the one route it left by capture-is-decided-by-syntax: a command is F Unit.

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

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

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

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

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

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

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

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

• superseded — handler-alias-mode-preservation — handlers and aliases preserve a head’s pipe signature (2/4); narrowed in place to the payload route, and then gone with it: an arm stands in for what it replaces (capture-is-decided-by-syntax).

• superseded — ir-pipespec-annotation — the checker writes ground mode wires into the IR; the evaluator reads, never infers (3/4, landed). The per-stage Wire is deleted by pipes-are-positional-byte-wires, and the pipeline’s value is its final stage’s: with no interior adjacency rule there is no interior adjacency to annotate.

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

• active — unify-one-sided-obligations — the co-inductive unifier memoizes one-sided var-vs-structural-key obligations, so a recursive type anchored at a ty-var unifies with the same type anchored at a comp-var instead of overflowing the stack. Its route fingerprint is superseded by capture-is-decided-by-syntax: Return carries no route, so the key keys on the value type alone; the guard stands.

• superseded — alias-head-defines-its-modes — a fresh alias/handler head defines its own modes; preservation binds only a known head; the byte discipline enforces at the connection, not the definition (supersedes handler-alias-mode-preservation). Restated as a single route pin by pipes-are-positional-byte-wires, and replaced by standsFor in capture-is-decided-by-syntax.

• active — cacheless-module-loader — module loads carry no cross-session cache (freshness over a memoisation a shell never needs); the cycle/depth guards are retained and load-bearing; use becomes a scope-projecting wrapper over the shared evaluate_source.

• active — esc-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.

• active — one-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.

• active — witness-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 equality check 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.

• proposed — raw-delimiter-near-miss — a #\' near-miss errors in value position ([L0004]) and back-points the [L0001] it strands in line-leading position; the grammar is unchanged (#\' is still not a raw-string opener). Rests on confirming “do not change the grammar” permits a hard error.

• superseded — pure-pipe-equation — the historical value-edge equation x | f = f !{x}; superseded by pipes-are-positional-byte-wires, where there is no value edge to state an equation about: x | f is an ordinary pipeline whose producer writes nothing, and value composition lives in application and bind.

• superseded — child-eval-unification — one re-exec’d-child eval protocol (run_child_eval + ChildKind) replaces the sandbox/pipeline pair; one wire shape in and out, the two-snapshots-must-agree hazard gone. Superseded by stages-are-threads.

• active — evaluator-runtime-split — the command/pipeline/transport machinery moves to core/src/runtime/; evaluator/ is the ~2.6k CBPV machine and the seam a module boundary, not just a claim.

• active — host-embedding-api — BakedPrelude + boot_shell deduplicate hosting a Shell; the postcard bake moves into core, the schema-evolution hazard collapses from three files to one.

• superseded — value-edge-locality — the historical locality rule for typed value edges; superseded by pipes-are-positional-byte-wires, since the one surviving edge fact is positional and needs no judgment sited anywhere.

• superseded — authenticated-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). Superseded by sandbox-external-children: grant bodies no longer re-exec, so there is nothing to mark.

• active — per-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.

• active — exarch-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.

• superseded — terminal-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.

• active — provider-config-ral-script — exarch declares almost nothing: a famous provider whose conventional key is in the env auto-populates and its models are fetched live (genai all_model_names, lazy + cached + manual fallback); a hand-written XDG config.ral is only for unusual providers (endpoint + protocol completions/responses/anthropic → AdapterKind, no-authority eval); the active provider + model (not 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 whose overlay also carries the tuning rows (the separate /tune was never built); --model/--provider/--max-tokens/--effort returned for headless starts. 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. Since 2026-10-06: there is no manual fallback — an account’s listing is the authority, Bureau::build refuses a model it does not name, and a launch with nothing to restore picks one before its session exists.

• proposed — structural-bug-prevention — a wide review’s serious bugs collapse into nine recurring shapes (check/use path mismatch, cancellation that never cancels, a privileged fd/handle leaking into a confined child, an invertible range, a record read as an ordered key-stream, continuation by token-suffix heuristic, error classification by Display-scraping, a debug_assert-only guard, a never-populated source identity). Each gets a missing type that makes the bad state unconstructable (LexicalPath, 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.

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

• active — handle-settle — a finished handle has one settle {stdout, stderr, outcome: <ok: α | err>}; poll → <pending | settled> reports it as data (total, never raises), 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. Amended 2026-10-19: await and race no longer unwrap the settle; they behave as the block run here, replaying its stdout then its stderr and ending as it ended, and poll, the one data observation, gains elapsed (await-is-the-block-run-here). Amended 2026-10-20: the settle is claimed once, moved out of the cache by await, race, cancel or the handle’s owner; poll claims nothing and, with is-done, fails on a claimed handle (await-is-the-block-run-here).

• active — tool-boundary-steering — queued prompts drain after the current assistant tool-call batch, before the next provider request. Every requested tool id receives a 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.

• proposed — force-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.

• active — unify-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 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. Amended 2026-10-19: par is a call-owned Rust builtin that cancels and drains its fan-out on every exit, so a cancelled par orphans nothing, and a birth inside a worker hangs under that worker (await-is-the-block-run-here).

• active — concurrency-detached-vs-structured — with the root/foreground split, spawn and & are handle workers hung off the root, watch is a root worker 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. Amended 2026-10-19: worker leases are retired, service is deleted, worker <id> re-acquires any worker’s handle, a birth inside a worker hangs under it and is settled by it, and par, all and race are structured, closing the orphan window (await-is-the-block-run-here).

• complete — turn-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.

• superseded — bundled-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.

• active — watch-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 durable-root model, death-clock, reaper, and forget’s deletion stand.

• superseded — long-running-work — long work is born durable via a distinct exarch-registered verb into a listable durable-job registry, never a promoted spawn; the open Regime 1/Regime 2 question and the cancel-by-id/pinning machinery are resolved by leases-and-budgets: Regime 1 ships as the durable lease class of a universal worker registry (verb service), Regime 2 stays deferred. Amended 2026-10-19: the durable class and service are deleted with every worker lease, and worker <id> replaces service-handle (await-is-the-block-run-here).

• proposed — scheduled-wakeups — a cron-like wakeup is a timer that injects a synthetic user turn into the prompt queue, re-engaging the agent loop without a human; it schedules the agent, not a worker (the line that separates it from long-running-work, where a born-durable worker yields a value — here the payload is a prompt the model acts on, no ral code runs). Ephemeral and per-session: schedules live on the Session, die on session end and /clear, and 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 date → uu_date → jiff-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).

• active — async-agent-tool — agent 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.

• active — sandbox-external-children — grant 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.

• active — tui-transcript-as-graphic — the scrollback is re-projected as an information graphic whose Bertin variables (shape, value, size, hue, grain) are encoded per-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.

• superseded — host-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.

• active — run-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 worker can influence; Shell stays Send, tokio stays out of core, same-thread children inherit the surface, workers get bounded once-only surface replay, and the bus remains presentation rather than liveness. Completes unify-turn-evaluation by making REPL, exarch, and batch request suppliers.

• active — run-turn-is-host-api — the public evaluation seam is one layer: hosts call Shell::run_turn(src, TurnRequest) -> 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.

• open — after-turn-api-simplifications — draft follow-on cleanup after the run-turn cutover: the common architectural error is turn-local facts leaking into long-lived or host-owned machinery (completion through presentation transport, surface as persistent cloned state, materialised frames as host API). The draft orders the next simplifications around enforcing that boundary: close old core exports first, move tests to run_turn, shrink or fold exarch’s ral adapter, share the TUI/headless explicit-done driver, 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.

• accepted — surface-carries-documents — surface 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; worker replay free); TaskStatus and the four bespoke line builders retire; provider_error folds into the shared fields renderer.

• proposed — surface-reads-writes-execs — redirect reads/writes and external or bundled exec images surface at the runtime’s syscall sites 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.

• active — handlers-and-aliases-are-lambdas — every per-name handler and alias must be a unary lambda { |args| … } and every catch-all a binary lambda { |name args| … }; the calling convention is fixed by the surface position, not inferred from the value’s runtime shape, and arity is validated at install time (a bare block, a non-lambda, or a wrong-arity lambda is rejected). 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.

• fixed — terminal-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.

• superseded — same-thread-body-shares-the-session — a same-thread thunk body — forcing a block or applying a lambda — must run in the caller’s Shell, sharing the session store by identity, not in a 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_child → child_of → Shell::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). Superseded by the-evaluator-steps-closures: both bodies run in place with no fold-back set, so a forced block’s cd persists too. Amended 2026-10-19: par is a Rust builtin and no longer reaches spawn_thread through spawn (await-is-the-block-run-here).

• superseded — repl-as-structural-surface — superseded: structural surface retired in 261006; 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).

• active — session-lifetime-event-bus — an async agent is muted only because the event bus is per-turn (pump mints the channel() in its thread::scope); an async 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.

• proposed — agent-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.

• superseded — deny-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 by a-binding-shadows-a-command: a binding shadows a command at every scope.

• superseded in part — functions-and-handlers — there are functions and handlers and no third: a function has fixed arity and is applied positionally, a handler takes one argument — the argv packed as List α, a catch-all also the dispatched name — and is installed scoped 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.

• superseded — surface-carries-control — superseded by surface-delivers-itself; 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 worker’s closure is unchanged — so “a worker holds only root/handle-owned resources” (concurrency-detached-vs-structured, watch-repl-builtin) holds by construction; the completion rides the existing inbox as SpawnResult → Turn::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).

• active — surface-delivers-itself — a worker’s surface is a second channel, scoped to the session: a foreground run surfaces on the live, dispatch-scoped channel (Event::Surface, ordered before its Report); a detached spawn worker outlives that dispatch, so its DeferredSurface buffers and, under a FlushGuard on every exit, delivers the batch plus a closing `done to the host’s DeferredSink (SessionEvent::DeferredSurface) before its result is sent — await/race/poll render nothing, and with no sink a worker has no surface. One vocabulary, one decoder, two channels because two scopes: a surface is handled by the innermost handler whose lifetime contains its producer. watch streams its lines on the same channel. exarch posts each batch to the root inbox under a Stamp a /clear invalidates at the pop, decodes it into the root scrollback, and wakes the model with the settled outcome.

• accepted — surface-pins-state — a rendered value is an event or state: surface’s render class gains a disposition, append (event → scrollback, logged) or pin (state → a keyed register slot, overwritten in place, unlogged). `pin [key, body] writes a `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 scrollback 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.

• accepted — recording-follows-the-event — what lands in a durable log is decided by what an event is, not by which thread emitted it: a per-session operational transcript.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 scrollback, 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. Its one carve-out is since withdrawn: --no-logs, “the explicit transient exception”, is deleted, because a session directory inside a TempDir already gives every property the flag claimed while the flag cost a second code path through the whole record layer — every session now has a record.jsonl, and “for every durable session” reads as every session.

• amended — reply-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.

• superseded — non-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.

• active — shared-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 concurrently 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.

• proposed — agent-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. Amended 2026-10-19: the worker idle-observation lease is retired, so a worker lives as long as its owner; the binding lease stands (await-is-the-block-run-here).

• superseded — long-session-resource-budgets — a days-long exarch run is bounded by heap, queues, shell values, and logs, not by model compaction; proposed per-accumulator budgets (bounded bus, windowed scrollbacks, inbox quotas without silent loss, physical post-compaction reclamation, /resources). Carried forward whole into leases-and-budgets, which adds the probe convention, the worker registry as accounting spine, and a per-agent admission cap.

• proposed — provider-heartbeats-and-retry-boundaries — exarch judges provider liveness by raw wire progress, not by semantic model output: Anthropic 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. Amended 2026-09-29: a 429 naming a reset past the patient tier is surfaced at once, and the terminal trunk resumes it by a harness-armed provider-reset wakeup — a new exchange, not a continuation of the refused request.

• active — partial-poll-pending-output — poll $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.

• fixed — windows-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.

• active — subagent-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, background drive, and inbox return path; AgentLog drops any unanswered parent tool-call frame before importing context so the child never inherits a dangling protocol.

• active — spawn-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.

• superseded — protected-commitment-pins — commitment:* 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.

• active — exec-projection-defers-to-gate — the OS exec projection’s admit decision is the in-process gate’s own verdict, queried once per nameable command, not a second derivation of it: the two folds of exec-authority-partitioned stay two, but the projection had been intersecting literals with literals and dirs with dirs, losing every admission that crosses shapes — a literal 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. Amended 2026-10-04: the law stands and the mechanism is gone — guard and kernel read one compiled ExecRules table, the kernel through an ordered rule list rendered from the very table that admitted the launch (exec-rules).

• active — per-agent-eval-cancel — cancellation reaches the eval layer: only the signal-facing session publishes the process-global signal slots (SessionState::publishes_signal_slots; a bequeath/child_of fork 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. Amended 2026-09-23: the reach is now the seat’s InterruptTarget, a republished ControlSender whose terminate cancels the engine’s root under either carrier, and the trunk’s interrupt-only reach is gone — no root carries a lease, and /clear reboots the engine rather than a captured root. The trunk’s turn cancel also rides the ambient foreground cause (cancel-is-a-join, which dissolves the one-publishing-session rule into how a scope is minted).

• active — cancel-per-tab — Esc and Ctrl-C unwind only the focused tab’s current turn: they never cascade to a subtree and never end an agent, so lifecycle death stays with /quit, /close, /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.

• active — session-ledger — the unifying frame over leases-and-budgets: everything alive between turns is a resident with four facets — identity in the ownership tree, a typed capability (Handle, pgid job spec, AgentId, schedule id, top-level name), a lease, a probe — and the session keeps one ledger in five chapters (workers, agents, stopped jobs, schedules, bindings) whose management surfaces are folds written once: list, exit warn-then-sweep, cancellation cascade, /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/disown — bg 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 worker 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 (scrollbacks, bus, inboxes) stay probe-only: no capability, no listing. Graduates to a design/residency page once accepted. Amended 2026-10-19: the durable grade is gone from the order — service is deleted and worker leases are retired, so a worker’s lifetime is its owner’s (await-is-the-block-run-here).

• active — signals-are-causes — closes core-audit #3 (signals can’t preempt a blocked standalone external; SIGTERM never cancels) by deleting the parallel delivery mechanism instead of patching it: the platform handlers translate each delivered signal into a 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.

• superseded — session-scoped-appcontainer — the Windows OS sandbox as one AppContainer profile per shell session, imitating MXC Tier 3 (0e7c3dd) with permanent provenance breadcrumbs; its union-of-projections consequence was judged unsafe for within-session attenuation.

• superseded — projection-keyed-appcontainer — the Windows OS sandbox mints one AppContainer SID per distinct fs projection (bind_spec identity; profile names pid+counter, never content hash), so a child’s kernel-checked authority is exactly its own declared projection — narrowed grants and subagent permissions hold at the OS layer; same-projection commands share one SID and its stamps, profile registrations are ledgered before the OS create, and ACEs revert at session teardown, not frame exit.

• superseded — ace-free-fs-confinement — the ported DACL tier stamps an inheritable ACE per fs prefix and 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.

• proposed — vm-workspaces-cross-by-copy — an exarch VM receives a private ext4 workspace through a bounded, content-addressed bulk plane beside the ral control seam; no host directory or NIC enters the guest, turn-boundary deltas land first in immutable private history, and only explicit witnessed publication changes the granted tree, while ral’s in-process gate and per-spawn OS projection preserve narrower grants inside the VM.

• active — agent-names-and-schedule-labels — the exarch agent surface collapses to one record-spec verb, agent [prompt, name, type: `amnemon|`mnemon, grant] → [name: Str, log-dir: Str]: the closed record row makes a missing/misspelled field a static error naming it, while the 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, with no replacement pin. Amended 2026-10-19: service is deleted and every worker is a titled spawn, so no durable-service legibility remains to fall back on (await-is-the-block-run-here).

• active — harness-calls-are-acts — an act changes the world outside the turn and an observation does not, so a spawn, a message, a schedule, or a 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. Since amended again: only the verb column survives — a verb is a closed vocabulary and aligns, a free agent name is not and was charging every row the width of the longest name nobody used — so a name reads bracketed, [hunter], wherever the TUI draws one, and a reply’s payload, being ral source rather than a sentence, is lexed and coloured like any other ral the TUI shows. Since amended a third time, on both sides of the vocabulary: the read-only `exarch-transcript family drew an act row under a verb minted outside DeskAct, though a read changes nothing outside the turn and the ral call that carried it is already on screen — it is a listing, so it now draws nothing; and context-evict, the family and tag of `exarch-context `evict glued with a hyphen, becomes the one word evict it always was, dropping the verb column from 14 to 11.

• superseded in part — total-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. Its pid side is superseded by one-reaper-one-fold: the reaper’s own waitid/WNOWAIT scan and blocking_reap are the one funnel now, and the pgid funnel was already unreferenced. The pgid side — Pgid’s positive-only identifiers, Pgid::signal_group’s typed send — stands.

• active — synod-is-a-second-product — synod is its own crate and binary depending on exarch as a library, not a fork and not a --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.

• active — survives-exit-is-its-own-verb — service 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. Amended 2026-10-19: service is deleted — with worker leases retired, the time axis it varied no longer exists — and detach stands (await-is-the-block-run-here).

• active — windows-hyper-v-backend — synod’s Windows machine is Hyper-V created directly through the Host Compute System API (computecore.dll, the WSL 2 / Linux-container surface), described by one JSON document whose every part is chosen so the guest cannot tell which hypervisor booted it: Chipset.LinuxKernelDirect, SCSI-attached disks, a host-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.

• active — windows-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 Boot → Booted → Adopted 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.

• active — guest-namespace-prefixes — a grant prefix is folded by the rule of the namespace that will match it, so synod’s guest paths are minted through a POSIX kernel (lex::fold_dots_posix, FrozenPath::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). A guest prefix is re-frozen only by the guard that matches it, inside the machine; the Namespace tag later added beside the fold is gone (one-table-two-instances). 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.

• superseded — cancel-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.

• active — cancel-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 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; a child_of fork 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. Amended 2026-09-23: the join stands, but no scope folds a process cell any more — every signal reaches an engine as Control, forwarded by its carrier (cancellation).

• superseded — cancel-is-a-watermark — “a cause raised for a settled run must not unwind the next one” is a claim about time, which the spend made destructively — and zeroing shared state needs a unique zeroer, whence the whole authority apparatus. Re-index by time instead: CLOCK: 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. Superseded 2026-09-23: no frame reads a watermark; a signal reaches an engine only as Control, forwarded by its carrier (cancellation).

• superseded — the-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 one 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.

• active — one-connect-door-not-four-gates — egress narrows to a destination policy: the guest may open TCP connections to port 443 of the public addresses these exact hostnames resolve to, once, on the host, and to no other destination. The four gates above collapse to one explicit CONNECT-only proxy that reads at most 8 KiB of head, refuses @ in the raw target before parsing it, parses 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.

• active — detach-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.

• superseded — exec-surface-fails-loudly — superseded by grant-surface-is-typed. Was: a path-shaped literal key naming a directory fails at load with a trailing-slash hint, and an empty subcommand list stops being a spelling of 'allow'.

• active — path-derived-capability-sids — a Windows fs grant is keyed by the path it covers, not by the container that consumes it: each (canonical path, kind ∈ {rw, ro, ls}) 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 completion store (stamps.json, atomic tmp+rename, per-path named-mutex merge) and a probe of the root’s own DACL — invalidated before reapply and recorded after completion, 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; 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. Amended 2026-10-20: a capability cannot be denied — the AppContainer pass matches a deny ACE only against the token’s ordinary groups (Forshaw, Windows Security Internals, ch. 7), so the per-path deny capabilities were inert and are removed; an exclusion inside an allowance is carved out of it at each launch — the allowance granted as its existing entries less the excluded ones, each directory on the way only its own listing by an ACE nothing inherits, so a name made there later reaches nothing granted — one on or around an allowance is refused, and every exclusion is proven unreachable at each launch by AuthzAccessCheck on the child’s own package and capability SIDs, and a restricted-token route to denies inside grants is recorded as future work. 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, carving and the access-check gate from inside the child, wide-vs-narrow attenuation, nested-capability subset behaviour, reparse points, ≤3 ACEs per prefix, token capability-array limits) is open before it is called settled.

• active — boot-contract-is-versioned — the ral. kernel-command-line keys and the grammar of their values are one indivisible agreement with a version, ral_daemon::boot::CONTRACT, kept beside the command line’s only writer and only reader so a new key and its bump cannot land in two commits. An installed synod built five days after its guest media 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.

• active — guest-console-outlives-stdout — a diagnostic written to a handle that goes nowhere is not a diagnostic: on an installed synod the machine’s owner is a 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 by this (amended 2026-10-20: broker::VERSION is 3 now, since Reply carries a data-only Error rather than a sentence): the boot error already crosses the pipe to the window, so quoted lines and a log path need no new frame, and a version bump is a compatibility event between an installed service and an installed window. Open: how many lines a failure should quote is a judgement, and nothing surfaces the console into the review screen.

• active — session-disk-outlives-its-machine — Stopped 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.

• active — one-walk-one-anchor — a PATH search is one traversal, from one anchor, yielding one answer. The anchor is an Option<&CwdPath> — Context::search_cwd supplies the within [dir: …]-else-cd precedence, None means no cwd — so ctx.dir does not typecheck 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.

• active — launch-cwd-is-the-freeze-anchor — exarch freezes an agent’s authority against the cwd it was started at, never against the cwd it stands in: a trunk anchors to the launch cwd run() reads once 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: fork_child resolves the child’s one grant layer (policy::base_layer(spec.grant, &cwd), pushed onto a clone of the parent’s GrantStack) against the parent’s live cwd at the instant of the spawn — “so a desk-spawned child starts where the model is” — then the child’s seat keeps that reading for life. Amended 2026-09-23: the layer is resolved engine-side — IdentityTransport::adopt_parked or EngineSeed::decode then Shell::child_of, through SpawnGrant::narrow_onto — against the child’s own cwd, which is the parent’s live one at the fork. Amended 2026-09-22: a `restrict R spawn freezes under the same rule at the same instant, which for a wire spawn puts the decode guest-side — the record crosses the seed unfrozen (a-spawn-is-one-layer). 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.

• active — bundled-tools-always-reexec — every bundled coreutils/diffutils/ripgrep invocation is a ral --ral-bundled-tool <tool> child through the same spawn/wait machinery as a host executable; the inline in-process placement is deleted, its admission gate having required 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.

• active — a-name-is-a-value-or-it-is-handled — the builtin is not a kind of name: a manifest entry’s mechanism is one of ral’s two existing ones and is read off its arity, and effectfulness partitions nothing, since a function is a computation and a computation may act. A fixed-arity entry has a function type (arity 0: a thunk type), so it is a first-class Value::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.

• active — one-delimited-trail — an unwind discards a call’s bindings and keeps its effects, so a dispatch owes its caller a pair — dispatch : Program → Ending × Trace — and the harness stops rebuilding the trace per stratum (the act ledger, birth_epoch’s clock arithmetic with its documented misattribution leak, ToolResult.timed_out, stderr assembled by append order across two layers): one delimited trail under five laws — flat merge; the opener owns closing on every exit, panics included (TrailScope/Audit::close, killing the session-long 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 { }, ral --audit, and the exarch tool call as three 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; amended 2026-09-05: try no longer delimits, the failing dispatch stamps Error.command, and audit { } answers [outcome, trail]), 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.

• accepted — depth-proof-env-seam — a lazy stream is a chain of closures, so any walk that crosses the captured-env link recursively spends stack once per line, and exactly two walks cross it: the seed 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_runtime builds rows by Kahn’s algorithm, linear in the chain.

• superseded — a-head-has-three-identities — superseded by exec-rules. Was: 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.

• active — exchange-ends-at-fleet-quiescence — synod’s after-checkpoint and report refresh wait for the trunk parked and no live children and their results drained, not merely the trunk’s own silence — a deliberate departure from exarch’s chat-while-they-work model, since synod’s checkpoint-before/report-after/undo promise cannot survive a report written while a helper is still writing to the folder it describes. Synod’s trunk fuel lifts from 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.

• superseded — store-lives-as-long-as-the-conversation — the store it re-priced and re-scoped is gone: undo was removed from synod outright on 2026-09-18, and the safety copy with it. What survives is a stat-only report — one walk at the opening, one after each exchange, no byte of the folder ever read — with a fourth change kind, touched, for a file whose size held still while its clock moved, and renames paired on (size, mtime_ns) rather than content. Removed because every defect a review found lived in that machinery, because no platform synod ships on offers a snapshot it can use (macOS clonefile yes, Windows nothing — VSS needs administrator rights and cannot shadow a UNC path), and because the report is consulted after every exchange while the undo almost never was. Undo is now the folder’s own version history. The original record follows. — 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_file → Ok(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).

• accepted — synod-keeps-its-own-accounts — synod stops borrowing exarch’s environment-shaped credential story and gets a desktop-shaped one, exarch’s own behaviour unchanged: a key reaches exarch through the environment because exarch is started from a shell, while synod is double-clicked, inherits the desktop’s environment, and faces someone with no .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. Its order is since reversed, in both products: the launch environment’s key outranks the vault’s, the store keeping the two as layers (was_admitted and admit_key are gone); see provider.

• superseded — modes-solved-by-deferred-joins — one deferred constraint store for the mode joins, drained by the boundary that owns a variable; superseded by capture-is-decided-by-syntax, which removes the routes it solved: arms join by unifying the values they return.

• superseded — byte-only-pipelines — the interim rule pinning both a byte edge’s producer payload and its consumer input to Bytes, while permitting a value-returning final stage; superseded the same day by pipes-are-positional-byte-wires, which keeps its byte-only transport and its refusal of implicit value serialisation but drops the endpoint contract.

• active — pipes-are-positional-byte-wires — | merely connects stdout to stdin, and every interior edge is an operating-system pipe allocated from position. Its route-survival and WF-2 paragraphs are superseded by capture-is-decided-by-syntax: pipes stay positional, a stage writes (F Unit, no value row that returns), and the pipeline’s value is its final stage’s. PipeSpec, PipeMode, ByteMode, ModeVar, Wire, the _type probe, PipeYield and final_route are deleted.

• active — case-is-syntax-try-is-not — a case’s arms become a syntactic list (Vec<CaseArm> in AST and IR), so every alternative is a computation the checker can see and exhaustiveness is decided statically, always. The line falls at the set of alternatives, not the alternatives: the arms are written out at 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.

• active — a-coercion-is-syntax — the byte-to-value coercion the checker inserts is two kernel nodes, Decode(Capture(M)), and no part of it is a name. The old spelling, capture M to __captured . __decode-captured $__captured, wrote a checker-synthesized term in surface machinery and inherited every mechanism the type system cannot vouch for: an alias or handler frame named __decode-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. The coercion is unchanged by capture-is-decided-by-syntax; what changes is who places it, ⟦·⟧ on a let in place of a demand walk.

• active — no-value-has-an-optional-argument — ArgSig::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. Its “route pin” is gone with the route (capture-is-decided-by-syntax).

• active — argv-is-a-list-of-strings — argv is a list of strings, and everything else is lambda calculus: the two argument-passing mechanisms share nothing, so 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, Runtime::install_set/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 rides the entry as a diagnostic facet (T0055 is since deleted: presence lets the row state fail’s message), and T0050 is re-founded on readiness rather than arity — under-application curries, and what is refused is a discarded value still waiting for an argument (fixed-arity).

• active — exec-boundary-gated-statically — shape is exactly what a type states, so the refusal guarding execve(2) fires before the run wherever an argument’s type says the shape (T0057) and at the spawn wherever polymorphism hides it, which 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.

• accepted — context-is-a-projection — the durable law is that no recorded event is removed, while model context is the left-fold projection of an append-only event log; incremental recording is checked against both a from-scratch fold and an independent batch reference, residency follows the addressed view at O(view), and the file’s disk/O(file)-resume price, closed-exchange edits, fresh-shell resume, 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. Two of its accepted losses are withdrawn by context-rollover: spans that leave the view are a queryable store, and the prefix/set asymmetry dissolves with the digest.

• accepted; superseded in part, see session-record — one-seam-one-log — every fact a session records crosses one seam (record::Emitter::emit, append-then-publish under the log’s own mutex) into one durable log, record.jsonl, and every durable artifact is a fold of it: the model context over the 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 (Scrollback::live_tail), one rendering path for live and committed text.

• accepted — a-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.

• active — a-producer-that-outlived-its-reader — the pipeline’s one failure exemption is a fact about two stages, not about the producer’s status word: a non-final stage still running when the stage reading it ended keeps no failure, whatever it exited with, because the rest of its output was owed to nobody. Unix says that with SIGPIPE, Windows with the order the two ended in — ChildHandle::exited_at (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 Reader — Caller 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.

• accepted; amended by the-fold-reports-the-printer-mirrors; superseded in part, see session-record — the-window-is-not-the-transcript — a bounded window may neither be the source of an unbounded transcript nor be re-rendered whole per record. user.log becomes a stream the scrollback 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 (Scrollback::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 Scrollback::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. The growing durable prefix stands; the incremental-sync half, and the “left standing” paragraph with it, is superseded by the-fold-reports-the-printer-mirrors, where the printer mirrors the fold rather than re-deriving it.

• active — a-failing-cleanup-pre-empts — guard M { N } reads one rule for both of the cleanup’s signals: any halt of the cleanup pre-empts the body’s outcome, an ordinary error exactly as the control escape that already did. Body returns and cleanup halts, the halt is the outcome; both halt, the cleanup’s signal wins whichever kinds the two are; body halts and cleanup returns, the body’s signal survives. The retired half was trap-EXIT folklore — the cleanup’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.

• active — diagnostics-are-a-builtin — 1>&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.

• superseded in part — a-stage-ral-stopped-has-no-failure — ral holds a duplicate of each interior edge’s read end until that edge’s writer stage is reaped, so no interior edge can ever deliver a broken-pipe signal or a write error to the stage that writes it; the collector kills a non-final stage once its reader stage is gone — SIGKILL on Unix, a distinctive-code 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. Its parked-pipeline clauses are superseded by ral-does-not-suspend; the forgiven-death rule itself stands.

• active — a-numeral-denotes-its-number — a bare word the numeral grammar accepts is that number in every position — argument, value, redirect target, list element — with no positional asymmetry; a word meaning bytes is quoted ('007'). The complement is one printed spelling per number (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 (007 → 7, 1.50 → 1.5, +5 → 5, .5 → 0.5, -0 → 0); the round trip is a test, never the definition, since classification is a lexical grammar that consults no type, scope, or printer. The printer’s image lies wholly inside the grammar — it restores the point ryu’s shortest form omits, 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.

• accepted — the-evaluator-steps-closures — the evaluator is a CEK machine. A computation closure ⟨M, E⟩ is in focus, the continuation is a stack of frames each carrying the environment it resumes under, and the store is the 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; ~-paths are Tilde computations and the ambient reads are natives (amended by ambient-reads-are-builtins). 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.

• accepted — reply-parks — a 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 running worker, and has no busy children. Amends the terminating half of reply-terminates-returning-agents and clause 2 of exchange-ends-at-fleet-quiescence.

• accepted — agent-and-avatar — an agent existed three times (Agent, registry::Entry, HostServices), and the last two bugs fixed were the copies disagreeing; the fix is two types split along the public/private line — 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”.

• accepted; amended in carrier by the-turn-is-the-atom — the provider-facing history is a persistent value, Rendered (Arc<[ChatMessage]> segments, one per turn, 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 turn’s rendering, keyed by turn id and end slot so staleness is inexpressible; render_turn takes no flags at all, so nothing can vary one. 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.

• active — status-is-the-outcome — a run’s exit status is a pure function of its outcome, computed once and nowhere stored; Shell::last_status ($?), every write to it, 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.

• active — static-diagnostics-render-at-the-seam — RunReport::into_report renders every diagnostic, static and runtime alike: Report::Static carries { rendered, status } — the whole caret report, prefix through hint — and the host prints it and exits on the status. The Diagnostics { Parse, Types, Host } wire enum is deleted, no host having ever classified on it. StaticDiagnostics::Parse/Types carry the Source their carets point into; Host, spanless, does not, so the invariant is type-level. A failed compile registers nothing: compile_run peeks a FileId and returns before install_root_context mints it, and since no program survives a static failure no live span can reference its text — putting it in a registry that is append-only because live spans index it would leave an unreachable, unreclaimable slot per typo, forever. Rejected: registering the source before compiling (spends that slot, and breaks the invariant compile_run reasons from), and shipping ParseError/TypeError over the wire (a live error does not cross the protocol, and the one host wanting structure re-typechecks locally anyway). Fixes the ad916c82 regression, where routing the REPL through the transport dropped the ariadne calls rather than moving them into core, leaving every wire host — the REPL, exarch, and so the model reading exarch’s tool output — with ParseError.message and TypeError’s raw-byte-offset Display. Beside it, a hook run stops registering too: its program is an already-compiled value, so the entry it appended named the empty string — one permanent slot per prompt draw, and one per keystroke under a buffer-change hook.

• active — stages-are-threads — a ral-written pipeline stage is an OS thread running its own CEK machine over a cloned Shell, wired to its neighbours by ordinary kernel pipes; only an external command is a process, and every external still lives in one process group the parent is not a member of. Deletes the re-exec’d pipeline-stage helper and its wire; one anchor process now holds the group joinable on every platform for the pipeline’s whole life, the foreground is claimed before any stage runs, and Ctrl-Z parks a stage thread at its next machine step via a shared gate rather than the kernel stopping it directly. Accepted: a ral-written stage 0 reading an interactive terminal sees EOF, and five dependencies (crossterm the live one) fork outside the Apple spawn lock. Supersedes child-eval-unification; leaves concurrency-primitives-detached-vs-structured’s “pipelines are foreground-bounded” unchanged.

• superseded in part — event-driven-pipeline-collector — every event in a pipeline’s lifecycle is an edge, so the collector that used to poll for them is now a pure fold, step, over one channel: drive is while live() { recv; step; run }, no interval, no backoff. One dedicated thread per blocking wait — a stage’s own settlement, a direct external’s stop (RunningChild::run_pipeline_stage, the sole owner of that child’s wait), the anchor’s witness (two threads, a report reader and an anchor waiter, not the one the plan first described, since nothing multiplexes a pipe read and a waitpid on one thread without machinery this phase does not add), a thread stage’s own interior stop (a condvar on StageStop, not a poll) — replaces RunningChild::try_settle, StageHandle::probe, and the backoff arithmetic. The one timer left re-checks a cancel scope every 200 ms until scopes grow their own notification. Supersedes the polling half of stages-are-threads; leaves standalone RunningChild::wait’s own poll loop, the Windows stage interrupt loop, and forgiveness-origin precision on StageObservation to a later phase. Superseded on the producer side by one-reaper-one-fold: the fold and Effect stand unamended; the waiter-per-external, the two-thread anchor witness, and the cancel timer are replaced by the process-wide reaper and watch_cancel.

• active — ral-does-not-suspend — a stopped child is resumed, at once, by whoever waits on it: Stopped → SIGCONT, one rule, every role, every platform that has stops. None of ral’s three programs need stop/continue job control — exarch never suspends anything, synod runs the shell in a VM, a REPL user has spawn, a second window, and Ctrl-C — and the record elsewhere (fish PR #8021, nushell PR 15202, elvish #988) shows no middle point that stays small: the design space is binary, tracked-with-a-table or not tracked at all. SIGTTIN cycling stays impossible because a spawn worker never receives the tty (route_parent_stdin); the anchor also ignores SIGTSTP/SIGTTIN/SIGTTOU outright. Deletes the job table and jobs/fg/bg/disown, Escape::Stopped, parked.rs and the park effects and levels, StopPolicy/StagePark/StageGate/StageStop, and the three WaitOutcome stop variants in favour of the poll-time WaitPoll::Stopped; GroupRole collapses to owned: bool. Deferral goes with the park it existed for: WriteFate::Defer and StagedWrite are gone, PendingWrite carries its own abandoning Drop. Supersedes, in part, a-stage-ral-stopped-has-no-failure’s parked-pipeline clauses. Its own “what remains of stop” is corrected by one-reaper-one-fold: the reaper answers every stop itself, in one place, and no subscriber ever sees one.

• active — one-reaper-one-fold — the platform offers one select over children (SIGCHLD, RegisterWaitForSingleObject) and every real shell owns it; ral simulated one with a thread per blocking wait instead. A process-wide reaper now owns every wait: ChildHandle::into_watch is the one door from a spawned child to a Watch, a stop is answered with SIGCONT inside the reaper’s own scan and never reaches a subscriber, and an exit is observed with WNOWAIT and left a zombie until Watch::reap — what closes pid reuse structurally. Cancellation becomes an event the same table carries: watch_cancel arms a one-shot closure a signal handler’s reaper::kick or a synchronous CancelScope::cancel both can fire. The pipeline fold gains attribution directly, over the strongest CancelCause the collector sent each stage (sent, since carried by the stage handle itself); the standalone command’s own wait collapses to one recv. Per owned pipeline, thread count drops from k waiters + t stage threads + a report reader + an anchor waiter + a cancel timer to t stage threads + a report reader. Supersedes event-driven-pipeline-collector on the producer side only, and total-wait-status on the pid side only; corrects ral-does-not-suspend’s “what remains of stop”.

• active — the-cut-is-at-the-write — an interior edge is dead once its reader stage has ended, and a stage feels that death at exactly one place — its next write to the dead edge — and nowhere else: a ral-written stage’s own write raises the break at that write, an external’s write is heard by a sentinel reading the held edge in its place, discarding whatever was already pending and taking the first byte after it as the kill’s cue. That break is the pipeline’s one forgiven death; everything a stage does before it, on its own account, runs to completion, and nothing after it is promised. The static redirect exemption is now a corollary rather than a clause: cmd > file | next runs cmd to completion because it never performs the write the cut watches for. Measured on the demand rule it replaces: sh -c 'echo world >&2; echo hello' | true lost world 20/20 runs, and sh -c 'exit 3' | true had its genuine failure laundered into success 20/20 runs, both now fixed. Supersedes, in part, a-stage-ral-stopped-has-no-failure: the forgiven death and the verdict rules stand, only the moment of the cut moves.

• active — an-envelope-does-not-touch-the-host — building a sandbox must not mutate the host tree, so an absent deny inside a write prefix gets no mount on Linux and no ACE on Windows and rests on the in-process gate (macOS holds it in the kernel).

• active — one-delivery-path — a cancellation reaches a pipeline’s processes once, through the collector: the signal relay is deleted, an owner signals its whole pgid and a joiner each pid, a kernel-delivered key the anchor reports is never re-sent, and grace_signal is the one cause→signal table — None for reader-gone and root-abort, so those kill outright at every nesting level. One Ctrl-C is now one SIGINT per external where it was two, !{ yes | cat } | head -1 exits 0, a torn-down pipeline external reports its deadline, and a spawned worker’s pipeline survives a Ctrl-C at the prompt.

• active — the-envelope-is-a-process-namespace — a grant’s envelope confines process identity and lifetime, not only the filesystem and network: every bwrap launch owns its ipc and uts namespaces and, where the host builds them, a pid namespace with a fresh /proc and a cgroup namespace with /sys/fs/cgroup re-rooted on ral’s own cgroup, on both projections — a pseudo-fs inside the envelope describes the envelope, so /sys, being its mounter’s, is narrowed as /etc is — so a confined child sees and signals nothing of the host and a detached survivor is invisible from any later grant. bwrap never execs the payload in place, so a Kept launch reads the payload’s pid over --info-fd and every ladder addresses that session — the mortal monitor is addressed by nobody, and bwrap’s 128 + n is the payload’s death by n. Ownership decides only the two ties (death, address). A host that cannot build the namespace — a container runtime masking /proc — is never refused, only stated: the namespace is an envelope invariant, not a promise a grant names. Rejected: fail-closed, --tmpfs /proc, a process-reach axis, dropping --new-session, a per-session namespace. Amended 2026-10-19: service is deleted, so spawn and detach are the verbs for outliving a command (await-is-the-block-run-here).

• active — landlock-exec-layer — kernel exec confinement on Linux is a Landlock domain the confined payload enters inside the bwrap envelope (a domain handling any fs right forbids mount(2)), handling Execute | Refer and freeing Refer on / so cross-directory renames do not fail EXDEV, admitting the projection’s paths plus the dynamic linkers and ral’s own binary — never a command directory, since execve needs Execute on the binary and its PT_INTERP only. Landlock is allow-list only, so the parent renders a deny inside an allowed directory by subtraction over the tree at launch, a veto only where no trusted write reaches; the ABI 6 signal scope goes on every launch, closing the same-uid kill hole without a pid namespace. Closes linux-exec-confinement.

• active — object-not-name — the in-process fs gate authorises the object a symlink-free, directory-handle walk lands on (Shell::locate, path/walk.rs) and performs the open, staging and rename relative to that handle, so a dangling link is judged at its target and a swapped component is never followed; the before-image is a read the grant must admit. Composition is stacking: there is no Capabilities::meet, because (dirs, literals) is not closed under intersection — the GrantStack folds verdicts per access instead. Numbered redirects are gone (fds 0–2 only), pins derive from rendered deny names, and the projection carries no allow beneath a deny.

• active — seccomp-is-a-typed-deny-set — the Linux seccomp filter becomes seccomp::Filter, a typed deny-set (sandbox/linux/seccomp.rs) compiled by seccompiler instead of eight hand-packed libc::SYS_* numbers: kernel attack surface (ptrace, bpf, module loading, keyrings, userfaultfd, open_by_handle_at, the mount family) is killed with SIGSYS; user-namespace creation, setns, clone3 and ioctl(TIOCSTI) are refused with an errno. One BPF program per distinct verdict, stacked in bwrap’s argv, plus an x86-64-only x32 guard seccompiler’s own arch prologue does not provide. diag now names a denied syscall from the same rule table that enforces it, replacing a wrong guess (“widen the grant’s fs read set”) with the deny-set’s own reason.

• superseded in part, see session-record and an-eviction-is-a-span — context-rollover — exarch stops summarising: when the context fills, everything through the planned cut leaves it (ContextOp::Evict, replacing Fold) and is replaced by one harness-written head marker at message 0 — a pure function of the fold, so the prefix stays byte-stable and cached between cuts — listing what left by number, opening line, id range and KB, with the model’s own optional note beside it. Nothing is lost: the fold keeps a Locus — byte range and digest — for every record a departed turn held, so transcript becomes the door onto the record — `index everything it holds, `read a whole closed exchange back byte-identically, `grep a Rust regex over it all (100 hits, total honest) — while context keeps acting on what is sent (`survey gaining evicted, `drop, `evict). Provider::summarize and its whole apparatus are deleted; the cut keeps the newest half rather than codex’s cut-all, because the live task lives there and a cached half beats re-reading it through the door — and keeps it structurally, plan_forced_eviction drawing only from a slice the newest is not in, so a newest piece outweighing the whole keep budget can no longer take the work in hand with it. A byte range is meaningless without the file it was measured in, so every read checks the record against the Locus’s digest before the parse, naming a rotated segment or an edited log as the mismatch it is; and the door decodes one record at a time rather than a file, since holding the departed history decoded is exactly what freeing residency paid to stop doing. Ids become lineage-monotone: a mnemon child imports its parent’s context under the parent’s own ids behind one Protocol::Inherited link, and resolves any older id through the address that link carries for each row (a memoised, recursive ancestry walk as first landed; a Pointer per row in carrier) — so a child reads everything its lineage ever recorded, the only break being an ancestor’s file taken away by hand, refused naming the path. Accepted: no narrative summary, Drop unindexed in the marker (but listed by `index), a departed row weighed at the weight it left with. Read against codex’s server-side store and against the RLM framing (Zhang & Khattab): the prompt as a variable the model peeks, greps, slices, and delegates. Superseded in part the next day by the-turn-is-the-atom, which keeps every argument and changes the unit.

• active; superseded in part, see session-record and an-eviction-is-a-span — the-turn-is-the-atom — the context is a table of turns; a cut is addressed by a turn id and weighed at every turn boundary. One growing structure, one fold, everything else a projection: Folded { turns: Vec<Turn>, cuts: Vec<Cut> } is the log’s fold, and the context sent to the provider, the survey, the transcript index, the head marker, the pressure reminder and the eviction plan are all pure functions of it. An agentic run takes one prompt and then two hundred tool turns, so exchange-atomic eviction weighed at deliberate entry had exactly one exchange — the one nobody may name — weighed at a boundary that never came; Avatar::evict now runs at the top of every loop iteration, and ContextOp::Evict { through, note } takes every resident turn at or below through bar a user turn whose exchange still has a survivor, so a cut into an exchange keeps its prompt and the invariant “the first resident turn is a user turn” holds. The newest turn is unnameable by construction (plan_forced_eviction’s candidates are every resident turn but the last, and validate_edit refuses it by name), so is_live_exchange stops being an eviction concept and becomes the door’s alone. Turn { id, exchange, kind, label, bytes, held } is the one row — ContextRow, ContextSurveyItem, StoreIndexItem, EvictedRow and span_row all dissolve into it — placement lives in the ledger (Ledger::events is two partition_points), and Rendered caches per turn (TurnRender) with no flags to vary. The pressure reminder rides the steering channel at a tool boundary, latched once per excursion; a mnemon child inherits the parent’s whole table and its cuts, so nothing marker-shaped crosses by value; and the door speaks turns — `read [exchanges, turns] and `grep [pattern, exchanges, turns], the two narrowings a union, a whole exchange still byte-identical and a partial reach answering its turns’ own material. Accepted: a range inside an abandoned exchange returns the real material the context replaced with a note, and old record.jsonl files do not resume. Amended in carrier, the same decision carried through to residency: the structure stops saying that a turn left and says where it is — Folded/Ledger/Cut/Held-as-state collapse into one Context whose Turn carries a Body of either Here { records, origin } or There { at: Pointer, cut }, Held { cut } a projection off it, so the head marker’s misattribution (a survivor user turn drawn under the cut that spared it, and that cut’s row gaining bytes after the fact) is fixed by construction rather than by an id window. Memo, TurnRender, Admission, refold, the model fold’s own fold == memo check and the memoised ancestry walk all go: Context::step judges what it folds, Rendered is owned and rebuilt per request, and a fork’s link carries a Pointer per row so a lineage is flattened at each fork and a seed’s short copy still reads back whole. Also accepted there: the door answers turn material always (no whole-exchange rendering), an unreadable ancestor file is a read error named by path, and the four session bookends move from Protocol to Forensic — Protocol becoming exactly what the fold acts on.

• accepted — the-fold-reports-the-printer-mirrors — the view fold says what each record did to it (Blocks::step -> Delta { Opened, Grew, Patched, Quiet }) and Printer::fact(rec) replaces Printer::sync(&Blocks): every printer is itself a fold over the one log, owning its memo, stepping it per record, drawing the increment — never handed another fold’s memo. The TUI’s scrollback stops being a projection recomputed from that memo and becomes a 1:1 mirror of it, one block per incident, with grouping done online: Thinking, an intent-bearing ToolCall, an observation-origin card and a turn rule join the group at the tail, every other kind is a barrier that ends it, and each of the group’s two parts — the ∴ deliberation and the ▸ run — carries its own dial. Six mechanisms that existed only to survive a rebuild go with it: the Block::rev revision and rebuild floor with its hand-widened back-dependencies, the dial side table, the chrome anchor lane and its stable merge (the first of one-seam-one-log’s live-display blockers), the printer’s own second window (VIEWPORT_MAX_BLOCKS/VIEWPORT_MAX_ROWS, evicted_through), per-sync card decoding, and the separate user.log rendering path. Reveal becomes Detail with three named rungs — Tally, Summary, Full — the “summary plus three lines” rung deleted as neither a summary nor the thing, and with it the only reason a dial needed a kind-aware skip. Retirement to user.log now hangs off the one head trim against BLOCKS_WINDOW. Amends one-seam-one-log and supersedes the-window-is-not-the-transcript’s incremental-sync mechanism, its growing durable prefix standing.

• active — pub-crate-by-default — an item in ral-core is pub because a consumer outside the crate names it and pub(crate) otherwise, because every pub item is invisible to dead_code: visibility is not documentation of intent, it is what lets the compiler say an internal has no callers left. 657 of core/src’s 1676 pub declarations narrow; twelve dead items and seven dead re-export names go with them, each named by the compiler the moment its declaration narrowed. What stays public is a constraint rather than a concession — a consumer, a public enum’s variant payload (rustc’s private_interfaces, a deny here, is the binding limit), a #[macro_export] body’s paths, an example or build script, and the scheme! family whose every member a base frame’s row already names. Core’s own integration tests link the crate externally, so their 19-item reach becomes one enumerated, test-util-gated door, core::test_access, going through internals behaviourally rather than handing out core’s representation; eleven of them stop hand-seeding a shell and boot one through boot_shell.

• active — expression-block-is-a-lexical-mode — $[…] is a lexical mode, not a sublanguage: inside it < > <= >= != && || lex as operator tokens (one DelimKind::Expr on the same delimiter stack that already made newlines whitespace inside […]), the Pratt body’s operands are the ordinary atoms of the value grammar, the five operator forms are plain Ast variants with Spanned operands, and the block leaves no node — the Expr enum, Ast::Expr, the &&/|| fusion pass, the redirect-as-comparison reinterpretation and its glued-digit diagnostic all go. $[$s == 'quit'] is admitted and judged by the checker; outside $[…] > always begins a redirect (so >= stops being a word, as §3.5 always said) and &, &&, || are refused by name. Landing beside it: the error-only tokens Dollar and Ampersand are gone (the lexer refuses the character); a splice inside "…" is the token stream the same text has outside the string, so "!$d" is Force(Variable) like !$d instead of a synthesised !{$d} that interpolated a block. Amended since, twice: inside a string [ is otherwise text, so a splice must say whether the [ after it is its own; the rule now is that $(name) takes nothing after it anywhere and every other splice takes [k] anywhere, so "$(red)[$host]" is a colour and a bracketed host while "!{f}[k]" indexes as !{f}[k] does, and $(red)[x] outside a string is two words that touch. Also: $name[k] is no longer fused at the lexer, and the one rule fusion had been carrying — ! reaches over a dereference’s keys (!$p[tail]) but not a block’s (!{cmd}[k]) — is stated in parse_bang; bracketed literals are read as one item list and sorted into list or map afterwards, retiring the hand-rolled spread-skipping lookahead.

• active — an-external-is-a-byte-operation — an external command is an operation the OS types List String → Bytes; a handler interprets it and cannot re-declare its type. Its route half (head_pipe_route, PipeYield, bytes_promise_broken) is superseded by capture-is-decided-by-syntax: an external is F Unit and an arm stands in for it. ^name joins the path-head class, skipping the handler stack entirely — ^echo is /bin/echo, ^detach is not found — superseding a-name-is-a-value-or-it-is-handled §4 and no-value-has-an-optional-argument’s “^cd still reaches an installed arm” on that point alone; an arm under a native’s or binding’s spelling is unreachable and dead by construction, reported by explain’s shadows: line, never refused at install. A variadic value-returning command is inexpressible as an arm — that capability lives in the value world, a binding over a list. source is deleted (un-checkable: its target is a runtime path against the runtime cwd and grant), leaving use the one loader; the binding-lease ledger’s renewal seams narrow from three to two with it (agent-binding-reaping). seed_env binds a scheme-less name at one fresh monomorphic variable rather than dropping it.

• active — absence-is-merged-not-defaulted — a missing field is filled by merging in a record that supplies it, not by attaching a fallback expression to the pattern that reads it. A bracketed literal’s keys settle its kind, and one explicit field settles it for a two-spread merge ([tier: 'a', ...$given, ...$dflt]) — the field says the literal is a record before either spread is read, and first-spread-wins does the rest. With that route open, map-pattern defaults ([port: p = 8080]) are deleted: they were the only Comp an IrPattern carried, and the sole reason elab_pattern had to run before its own names entered scope, ir::walk_pattern_defaults existed, annotate_pattern was more than a clone, and bind_pattern’s Map arm shaped the row around which entries had a fallback. stage_pattern sheds the mooring/shell parameters it held only to run a default’s nested machine. Migration: let [host: h, port: p = 8080] = $cfg becomes let [host: h, port: p] = [tier: 'a', ...$cfg, ...[port: 8080]] — an explicit entry always wins over a spread regardless of position, so the default must be spelled as a second spread to stay subject to first-spread-wins. Removed along with the map-pattern default: a live soundness hole where a defaulted field’s type was unified with neither its default nor a present field’s actual type, so let [flag: flag = 1] = [:] typechecked and failed at runtime.

• superseded — an-open-spread-must-come-last — superseded by a-field-is-a-flag-and-a-type, which makes a literal a put over one base rather than a concatenation of parts, so there is no last part for an open spread to be and T0023 is deleted; its reading of why concatenation has no mgu stands, and the presence flag it records as rejected is bought differently — a flag that may be a variable over a payload the term rules confine, so order-independence is a theorem about those rules rather than about the algebra. a record literal’s row is the concatenation of its parts, folded from the low-precedence end, so an explicit entry beats every spread and an earlier spread a later one. A literal with two or more spreads used to discard every spread’s row for a free row variable, which satisfies any demand: [dummy: 0, ...[flag: 1], ...[other: 2]] checked and then died at run time. Because a row is a chain with one open end, a spread whose own row is still open can have nothing placed behind it — and since it wins on any field it turns out to carry, those entries could never be read, so the literal is refused (T0023) naming them; binding that row to them instead would force every caller to supply them, so the entries are dead under every sound typing and what refusal costs is exactly the programs whose only type is the concatenation type. A label written twice in one literal is refused too (T0022), so position means one thing throughout. Consequence: defaults cannot be merged behind an unknown record in any spelling, a map-pattern default no more than a second spread — so the deletion in absence-is-merged-not-defaulted stands while its replacement claim narrows to known records, and absence over an unknown record travels as a variant. Presence flags and a concatenation constraint were both rejected: the first is not additive over duplicate-retaining ordered rows, the second has no most general unifier — Wand’s result, read with Harper–Pierce, Rémy and Gaster–Jones in record-concatenation.

• accepted — silence-is-counted-in-probes — a peer is declared dead only for probes this process sent and it did not answer; elapsed time is never evidence. last_seen.elapsed() >= deadline reads as the peer’s silence but establishes only that a clock ran, on the unwritten premise that this process was running to observe it — false across a suspend, which is how a woken Mac showed the assistant stopped for an engine nobody had asked anything, and how a resumed guest killed its run as Corrupt. Liveness::probes() turns the configured deadline into deadline / interval unanswered Pings, the engine counts TICK polls that returned nothing, and await_attached spends patience in condvar waits it observed. A thread that is not scheduled sends no probes and so accuses nobody: immunity by construction, with no suspend detection, no slack factor and no choice between CLOCK_MONOTONIC, CLOCK_BOOTTIME and QPC — which disagree about suspension three different ways, so picking one only moves which host is wrong. Severed::Silent(Duration) keeps its payload and stops lying, the span it names now being the span that was watched. The general rule: a timeout may bound how long we wait, never be the evidence that the peer is dead — death comes from EOF or from unanswered probes. The write deadline stays a span, a blocked write being uncountable, and is noted as the one boundary.

• accepted; superseded in part by an-eviction-is-a-span — an-eviction-is-a-set-of-turns — there is one context edit, and it takes a set of resident turns. context `evict [turns: [Int], note: Str] records Protocol::Evicted { cut: Cut { turns, note }, by }; ContextOp, its Drop arm, EvictionPlan and Held::Dropped are deleted, Held is Resident | Evicted { cut }, and a forced eviction is the same record under another EditAuthority (/rewind <turn> was too until 261007: it is now Protocol::Rewound { anchor }, a truncation of the table that leaves no marker). The writer resolves the set (Context::resolve_cut applies the survivor rule) and records the ids that actually left, so replay departs exactly those and re-derives nothing. Two guards — never an unrecorded, departed, or unclosed turn — and one silent rule, a prompt whose answers still hold a resident turn outside the set; “the live exchange is untouchable” was only the coarsest address for no edit touches the unclosed turn, and is_live_exchange leaves the fold. A turn has a role; there is no exchange: TurnRow { id, role, kind, label, bytes, held } with kind ∈ own | import | inherited, UserPrompt { turn, text } and ContextMessage { id, message } naming turns alone, and “the assistant turns answering prompt u” derived from role and order (Context::answers, Context::prompt_of) where the survivor rule and plan_forced_eviction need it, stored nowhere and shown to no one. Every ral tool result ends with TURN: <id>, appended in agent/shell.rs from AgentLog::current_turn(), so the model has the address of the turn it just took without asking for a survey. A bracketed, user-voice marker stands at each hole — a maximal run of departed turns — rendered in place by render_marker, the former head marker being the hole at position 0, so a late cut no longer touches message 0 and the provider re-reads from the hole. The read door speaks the same address: transcript `read [turns: [Int]] answers [[turn, role, messages]] one element per turn and `grep’s turns is the same optional list, its hits [turn, role, line, text] — exchanges: and the [from, to] pseudo-range are gone, ral’s range a b already being a [Int]. What you can read, you can evict, by the same name.

• superseded — a-field-is-a-flag-and-a-type — superseded by a-table-never-enters-the-unifier: no presence flags, and the spread is an update. a record field is a presence flag paired with a type, and the flag may be a variable. Row::Extend carries a Field — Present τ, Absent, or Var(θ, τ), “a τ, if it is there” — over a two-point flag store, and Row::Empty stops being silence: it says every label off the spine is absent, so meeting a field there retires it rather than erroring. That is what makes a form’s options sayable in a type, so within $o has the literal’s verdict at last. The field rule unifies flags and then payloads: no rule branches on a flag, which is also why the erasure is lossless — presence has no elimination form, so no program could read what the traversals stop at, and Field::Absent stays nullary. As decided here Empty said more — absent at the type an ambient assignment Δ gives the label — which made the algebra unitary; that half was withdrawn four commits later (unitarity-lives-in-the-term-rules) and the page is written as it now stands. A record literal becomes a put over one base: [...b, l̄: v̄] demands of b only a slot at each written label, fresh flag over fresh payload with nothing imposed, and yields those labels Present over b’s own tail — so [...[x: "old"], x: 1] is [x: 1] in the type as it always was at run time, T0023 and the open-spread rule are deleted, and a second base is refused at parse. A repeated label in a record pattern joins the repeated case arm as a parse refusal. Owed and carried rather than discharged: soundness of erasure, conditional on the decoder and module boundaries that hand out unchecked values; the recursive case, where the occurs-through-payloads policy is chosen and the termination proof stays owed, MAX_UNIFY_DEPTH being a resource bound; and one condition that is a rule, not a result — within one check, a label may not be optional at two types that will not unify, which binds the declared option rows and nothing a program can write.

• superseded — unitarity-lives-in-the-term-rules — superseded by a-table-never-enters-the-unifier: with no flags the algebra is unitary unaided. the assignment Δ is withdrawn: an absent field carries no type, and retiring a field imposes no equation on the payload that dies with it. Δ made the row algebra unitary, so the unifier was order-independent on its own; but unitarity of the algebra quantifies over every row the datatype can spell, including rows no rule mints, which is more than a checker owes. What a checker owes is that the programs a user can write get one verdict whichever order their statements are in, and that is carried by two facts instead. The first is confinement, an invariant of the term rules: every variable in the payload of a Field::Var(θ, τ) slot at l occurs nowhere but in payloads of slots whose flag is in θ’s class — Field::Var is minted in exactly two places (the put rule, fresh flag over fresh payload; scope::occurrence, fresh flag over a declared table’s type), no builtin scheme carries one, and only unify_field touches such a payload. So Δ’s extra equation could bind only dead variables, and could fail only where two declared tables disagree at one label. The second is that the one-optional-type door already forbids exactly that, so the door becomes load-bearing rather than incidental and must be re-established for every new site introducing a variable flag; it is sharpened at the same time to compare unifiability rather than ground equality, which subsumes the old test and stops exempting Holds::Shaped. Falling out of the withdrawal: erasure really erases, so generalize’s residual cache is sound for all five sorts again; a retirement spends no depth on its payload; and two latent defects in the deleted equation go with it — the flag was bound before the payload equation ran, and the claim that δ_l was always on the left of the union was false from the second retirement at a label onward. No .ral file in the tree changes its --check output.

• active — a-spawn-is-one-layer — at the root --base and --restrict are two different acts; at a spawn they are the same act, because the parent’s GrantStack is already underneath: fork_child pushes a named base as if it were a restrict, so it can only narrow. One question — what single layer does this child get? — earns one field with six spellings, `inherit | `confined | `read-only | `edit-only | `reasonable | `restrict R, rather than two fields needing a rule for what writing both would mean; the CLI is deliberately not renamed to match, its two flags being two acts that genuinely differ where nothing sits beneath them, and the mirror worth having between the surfaces is in the vocabulary of values, not of flag names. `dangerous leaves the spawn surface: there it resolved to ⊤, a layer that says nothing, so it always meant inherit-the-parent — a confined parent spawning `dangerous got a confined child — and `inherit says that honestly, in the spelling provider/model already use for no opinion, while `dangerous stays a --base name where ⊤ really is no ceiling. R is decoded, not typed. The grant row in scheme_agents stays open under the house law that an open row means a runtime door enumerating the legal labels, so R is validated at that door and walked by decode_capability_map off the same Form::Grant declared table grant [...] { body } and every bake-in profile already pass through — one table, one wording, and no second description of the capability keyset in a different language to keep in step by hand. The wire carries the record unfrozen: EngineSeed.grant becomes ral_core::SpawnGrant { Inherit, Base(String), Restrict(FOValue) }, and a restriction record freezes against the child’s cwd — guest-side for a wire spawn, since the guest is the side standing in it — which is what preserves Capabilities’ resolved-by-construction invariant and hence licenses its unguarded Serialize; host-side fork_child and guest-side apply_seed then resolve through one SpawnGrant::layer, deleting a duplicated narrowing decision. No self-denial for a spawn’s `restrict: --restrict mints a deny layer over the restriction files’ own paths so the agent cannot rewrite its own permissions, while R is a value computed in the parent’s shell with no file to protect, so the asymmetry dissolves rather than needing a mirror. Non-escalation stays structural — one more pushed layer, and the per-check fold ANDs.

• active — the-lent-terminal-returns-the-gesture — only a terminal ral lent can report a key pressed on it: reverses 5803377b’s “whoever sent it” law. A death is a cancellation iff by a signal of a cause in force (signals_of: grace, key, kill); ForegroundGuard becomes TerminalLoan, which alone reads a signal as a key, hears it from a lone tenant’s death or the anchor’s raw Heard, and strikes it on the run’s frame when the terminal returns, so try cannot swallow Ctrl-C. Rejects ral keeping its own pgid for lone children and a seat enum.

• active — within-dir-is-local-state — the working directory is one state cell, and within [dir: d] is its local-state handler: it saves the Cwd — one path, since previous and the children’s OLDPWD are gone — sets d, and restores the saved cell on every exit, so a cd in its body moves only the scope’s directory. Context::dir — the override within saved and restored alone while cd wrote the slot beneath it, so that within handled get and forwarded set — is deleted, and with it the two probes that broke state’s equations inside a within: cd /usr/bin; pwd printing the override, and cd $CWD moving the session on exit. Entry is no cd (no shell.chdir, no observation); a within without dir handles no cell; chpwd compares the session’s directory across each line, and the last-chpwd reading is gone; within [env: …] stays a plain overlay because there is no setenv. Refines the-evaluator-steps-closures.

• accepted — a-closure-keeps-only-what-it-mentions — a thunk value is ⟨M, ρ|occ(M)⟩, built only by Closure::new, which narrows its environment to the names the body mentions by the lease harvest’s walk, so a closure keeps alive only what it can read. The machine’s ⟨M, ρ⟩ are computation closures, a type apart, transient and unscrubbed; a literal !{ … } closes nothing (U-β); no native reads a lexical environment, so explain reflects on the session; a worker starts from its creator’s session and forces its thunk. Amended 2026-10-19: service is deleted, so the workers that start from their creator’s session are spawn, watch, par/all children and a pipeline stage (await-is-the-block-run-here).

• accepted — a-binding-shadows-a-command — let dd = … shadows the command dd lexically, at every scope, and ^dd reaches the binary on PATH. The session-scope refusal of a binding named like a PATH command is deleted: it made a script’s legality depend on the host’s filesystem, while the checker, the runtime and the elaborator already resolved bindings before commands. Supersedes deny-binding-path-commands.

• accepted — recursion-is-guarded-by-data — a recursive type must pass through a list, map, record or variant. Binding a variable to a structure that reaches it along U, →, F and Handle alone is refused as CyclicType (T0073), by a search at the two bind sites that never crosses a data edge; w $w, a function returning itself, and $g $g are refused, streams, trees and json-get’s μβ. Map β are not, and a cyclic scheme prints with a μ. Refines unify-one-sided-obligations.

• accepted — a-let-generalises-what-is-not-weak — every let generalises what is neither free in Γ nor weak, and a weak variable has one type per unit. Weakness is a permanent mark on a type, row or computation variable, inherited by whatever it is united with and never lifted, so generalisation depends only on the syntax of the let’s body; generalize records a scheme’s weak residuals instead of quantifying them, it prints _α, and a later unit re-seeds each as a fresh weak variable rather than reading a foreign id. There is no value restriction: ral has no reference cell, and data of an undecided shape enters only through a boundary whose result is weak. A computed index’s three types are weak, and so is a checked boundary’s result. Refines session-scheme-continuity.

• accepted — a-boundary-is-checked-against-its-type — a door through which a value of a shape the program did not decide enters typed code admits it against the type the checker solved at its call, and never converts. The set is closed: the decoders of undecided shape (from-json, from-jsonl, from-json-at), use, worker, the exarch host’s exarch-agents/exarch-pins/exarch-transcript, and _ed-state. The site rides on the Exec; a mismatch names an RFC 6901 pointer and the line of the use that imposed what it met; a comparable variable is fixed to numbers or text across the unit; a session data binding with residuals is admitted again before each unit that uses it runs. Builds on a-let-generalises-what-is-not-weak. Amended 2026-10-19: core’s worker <id> replaces service-handle in the set (await-is-the-block-run-here).

• accepted — operators-are-kinded — a type variable carries a kind: a set of admissible heads and a deep bit. number, comparable, scalar, sized and data (deep: no block or handle at any depth) constrain + - * /, < >, interpolation, length and == and the encoders; two variables unite at the meet of their kinds, an empty meet is refused, and a meet with one nullary head binds the variable. A scheme prints them ∀α:number., a helper like let log = { |n| echo "n: $n" } stays generic, a refusal is KindMismatch (T0074) with a second caret where the kind was imposed, and () is neither a word nor an interpolant. A bare-label read on a variable is settled by the kind as well as the head, and a computed index $c[$k] is the one deferred relation (c = [e] ∧ k = Int ∨ c = Map e ∧ k = String): a head or a kind settles it, its variables are weak, and one nothing decides by the unit’s end is IndexContainerUnknown (T0075). Refines unify-one-sided-obligations.

• accepted — a-table-never-enters-the-unifier — a declared table never enters the unifier, and a row slot is a label and a type. A form’s options are syntax, consulted key by written key at the form; a contract file’s return is ascribed against its table after inference; the runtime doors keep judging what no rule checked. With no table to type, presence flags go: Row ::= Empty | Extend(Label, Ty, Row) | Var, a field met against Empty is a direct error, check_one_optional_type and ContractClash (T0025) are deleted, and a record’s spread is an update of one base — first in the bracket, adding no field, refused with the nearest spelling or the three idioms (a field given from the start, a nested record, a map) when it names one the base lacks.

• accepted — redirects-are-bindings — a redirect list binds each of stdin, stdout and stderr at most once, and one interpreter serves every shape that carries one. > a > b, 2> e 2>&1, 2>&1 2> e and < a << b are parse errors with a caret on the second redirect; 2>&1 means “wherever stdout goes” independent of position, so 2>&1 > f is > f 2>&1; targets open in the fixed order stdin, stdout, stderr; an external gets a > file as its own fd; a streaming write is committed whatever its body does, only an atomic > can be aborted (amended by a-file-change-is-one-fact: it is reported at settle, not at open). Refuses the POSIX left-to-right fold and last-wins.

• superseded — capture-is-decided-by-syntax — let x = hostname binds the text hostname writes because the checker wraps the command in the capture coercion, once, from the syntax of the right-hand side; superseded by graded-f, which places capture by the type.

• accepted — graded-f — a command’s value is its output: F carries a grade, a command is F^w Unit (Command), and a value demanded of a command captures it. F^p A (Returns A) produces a value, F^w Unit produces output and nothing else; a grade variable prints from ν ξ ο π. One coercion F^w Unit ⇝ F^p String fires at a bind, an argument and a join; one zero-cost upcast F^p Unit ⇝ F^w Unit at joins and handler arms; a stdout redirect discharges; a decoder ends the byte pipeline (T0078). capture_sites, stage_returns, tail_writer and Output are deleted. Known limit: joins are decided in program order, so the verdict is principal on the stated rule but not statement-order independent. Amended 2026-10-19: Handle carries its block’s grade, so await of a Handle Command is a Command, and defer is gone from the absorbing rows (await-is-the-block-run-here).

• active — exec-rules — exec authority is one table and one function: decode keeps the authored ExecGrant, ExecRules::compile turns each layer into rules over real paths, bundled tools, dirs and vetoes (a bare key is the file the host PATH finds, its bundled tool, and for a deny a veto on the name), and ExecRules::verdict alone judges, by Rank (Dir(depth) < Carrier < Exact < Name, equal ranks meeting). A rule holds a name as its polarity reads it, and a stack’s table is allows-meet, denies-join (a met-to-Deny key is kept only where a layer wrote that deny), so that verdict(a ∧ b, p) = verdict(a, p) ∧ verdict(b, p) (a proof sketch is in the page); a folded match ranks at its rule’s own depth, and Exact beats Dir. The kernel gets the same rules ordered by Rank. A Head carries Result<Program, Missing>, so a missing command never reaches the guard (127/126); check_exec mints the Admitted token every launch demands, and the projection renders its table. Supersedes a-head-has-three-identities. Declared limits: a copy under a new name escapes a veto; the kernel sees no argv nor which bundled tool runs; Windows has no kernel exec layer. Mechanics superseded by one-table-two-instances; the law stands.

• active — exec-carriers — the kernel exec set is one law on every platform: ExecRules::kernel’s rule list, ordered by Rank so last-match-wins is the in-process guard’s precedence, plus carriers (what execve forwards to before a program’s own code runs — a #! interpreter, macOS’s root-owned /bin/sh and xcrun shims; never env’s target) and the platform base (the loader and ral). A carrier is admitted only on bytes the uid cannot author (trusted_real, a link-following walk from /), the shebang grammar is the kernels’ narrowed, and the parent computes carriers once at spawn. Seatbelt renders one form per rule, exec denies denying no reads; Landlock admits the allows and subtracts the blocks beneath them, reading the list back as a table. Declared limits: an allowed interpreter runs any script it can read, Landlock subtracts only over the tree at launch, the kernel sees no argv.

• accepted — one-tilde-rule — ~ abbreviates home at the start of a bare word or a double-quoted string, alone or before /, and is an ordinary character anywhere else. "~/x" is one string, the home directory followed by /x, and home is a builtin over the effective environment (amended by ambient-reads-are-builtins, which removed the reserved $HOME register); ~user is gone, so ~bob/x and foo~bar are plain words; a bare ~, a literal word and a $[…] block are value heads, and cwd is absolute, abbreviate-home folding it for display. Amends env-is-dynamic-only.

• accepted — ambient-reads-are-builtins — the shell’s ambient state is read by six nullary builtins — cwd, env, args, user, home, nproc — and by nothing else. $CWD, $ENV, $ARGS, $USER, $HOME and $NPROC are gone, so $NAME is always a lexical variable and ALL-CAPS names bind like any other; $SCRIPT stays as the one reserved name, now refused as a binder; ~ abbreviates home and keeps its own IR node (CompKind::Tilde), Register/Observe are deleted. env and nproc deliberately shadow the coreutils programs (^env reaches them); no prefix. Amends env-is-dynamic-only, one-tilde-rule and the-evaluator-steps-closures.

• active — a-file-change-is-one-fact — what a write or an edit did to a file is one fact, a Change — path, outcome, diff — and a run of changes reads as one patch block, each file once, every file at every rung. Core reports every write at settle with its target before and after (64 KiB, whole or none); exarch diffs them, and an edit diffs the texts it already holds, so it always shows its diff; Diff::between cuts at the source — 2000 rows, a 250 ms deadline, exact counts — and the record carries the diff, never the bytes. Within a file, changes stack rather than compose. Amends tui-transcript-as-graphic and redirects-are-bindings.

• superseded — a-veto-freezes-what-a-write-covers — superseded by authority-is-belnap-evidence. Was: an admitted directory frozen against writes under a covering write prefix (FsRules::write_reach). The freeze made an exec allowance withdraw write authority in the kernel alone and is deleted; what it protected is a declared limit.

• active — denies-hold-under-every-spelling — a deny is judged under the coarsest identity any filesystem gives a name, an allow under the name as stored. lex::collision_key is compatibility caseless matching of the uppercase image (ICU4X; ASCII lower-cases, non-UTF-8 is its own key), path_within takes an Identity, and a rule’s Polarity picks the relation by type, so echo key > .ENV no longer slips an absent deny: [cwd:/.env] on APFS, nor NFD an NFC deny, nor éclair an Éclair deny on NTFS, nor fıle or ｆｉｌｅ a file deny on ZFS. A denial caught by another spelling says so. Windows 8.3 aliases are named through an attribute-only handle, and refused when unnamable. Exec reads names the same way (a deny dir, deny file and veto fold; allows meet, denies join). The page carries what APFS, Seatbelt, NTFS and ZFS were measured to merge, why a deny folds and an allow does not (over-deny against over-grant), and what was rejected: a cfg fold, asking the filesystem, folding allows, keying real, NFKC_Casefold. Accepted over-deny: a distinct secrets beside a denied Secrets on a case-sensitive volume. Residuals: Seatbelt allows over-grant across case on case-sensitive APFS; the Windows allow side keeps its ASCII fold. Its prefix-set mechanics are superseded by one-table-two-instances.

• active — one-table-two-instances — the fs and exec dimensions are one structure, Table<K: Scope>, whose meet is defined by the pointwise law ⟦a ∧ b⟧ = ⟦a⟧ ∧ ⟦b⟧; Region = Table<FrozenPath> and ExecRules = Table<ExecScope> are its instances. Replaces the PrefixSet<Allow|Deny> pair and exec’s four-map table with its hand-written meet, so one law is proved and property-tested once; own() replaces scope-against-scope containment; Carrier becomes a scope kernel() adds, so a carrier loses to an authored exact deny or a veto by rank alone; the authored ExecGrant becomes one map over ExecKey, exec’s three languages being ExecKey → ExecScope → ExecRule (the last since folded into the table by capability-is-data). Deletes the Namespace tag, which, minted relative to the host but compared as absolute, made every nested grant inside synod’s guest meet to nothing. Rejected: a three-state dir key, a scope-vs-scope containment trait, one fs table with op-tagged scopes, a Place subject keeping the tag. Its precedence and binary-verdict parts (rank, Verdict, meet_insert, ranked Carrier) are superseded by authority-is-belnap-evidence. Supersedes the mechanics of exec-rules and denies-hold-under-every-spelling; the theory is authority-tables.

• active — capability-is-data — the capability model reads no session and renders nothing: capability is the lattice and the folds over it, and the in-process guard and the OS sandbox are its two consumers, in the order capability < sandbox < guard. GrantStack::admit is the one exec judgment and the only mint of Admitted; booleans are one Flag with one permits and one Shell::check; SandboxProjection::of(&GrantStack, &Resolver, Option<&Admitted>) is the sandbox’s own fold, and ExecProjection::Restricted carries the guard’s ExecRules (for_kernel), which deletes the ExecRule list and its read-back; the guard words refusals into a typed Denial that Shell::refused records on the trail at one door, and a grant string becomes a FrozenPath in guard::freeze against one FreezeCtx. Reinforces capability-stage-collapse.

• active — the-envelope-mounts-by-handle — every object the bwrap envelope shows is opened by ral in the host, never through a symlink, and mounted by that descriptor; bwrap is never handed a source name. Binds::open plans every bind (the read-only defaults, the read and write prefixes, the program’s real image, the exec table’s allowed files and directories, the cgroup tree and the two pins over everything), opens each object once with RESOLVE_NO_SYMLINKS, and lends a copy per bind at Slot::Mount(i) (fd 107 + i); bwrap_argv renders --ro-bind-fd/--bind-fd from the same vector. A path is its object and its spellings (render_objects), a spelling within another bind left to the host’s own link; a read-only bind within another is dropped, a writable one only within a writable one. ENOENT/ENOTDIR drop a bind, and EACCES drops a system default no grant names; a name now reaching another object, or an open meeting a symlink, refuses the launch, each saying which. A covered admit is frozen, and a deny masked, at every name a bind shows it, a prefix written through a symlink being two binds of one handle; a deny hiding /proc is refused. A bwrap that builds no envelope refuses every confined launch in its own words, and one without --ro-bind-fd (before 0.8.0) naming the version, with no by-name fallback; the probe runs ral’s own pin as a pipeline anchor. Closes the swap race between render and mount; an exec-allowed directory is now readable, as on macOS; the image is no longer linked at its spelling. bwrap execs the trampoline from ral’s pin lent at fd 102 (/proc/self/fd/102 --warrant), so it is the boot inode by construction and Linux re-stats no name (Pinned::verify is macOS’s); both pins are bound read-only by their own descriptors at their current names (Pinned::names), locking the files against write, link, rename and unlink, an unlinked pin getting no bind. Residuals: a destination is still a name bwrap resolves inside, a second hard link to a pin is unlocked, a host bind mount of a denied directory under an allowed one is admitted by inode, and an unlinked trampoline needs a filesystem that serves it (not virtiofs).

• active — grant-surface-is-typed — a grant is a record of tagged values, not strings: places (`cwd src, `absolute P, `xdg-data .) are typed paths, name, a place and dir are the three exec targets (selectors path, system and homebrew valid only under dir), net is `offline, editor and shell are verb lists that join under extension, nested tables are records, every list is a set with repeats idempotent, and a foreign-rooted absolute is a dead grant symmetrically on both platforms. Argument filtering is gone; neutral layers launch ambient; the checker ascribes nested tables from a queue drained in typecheck; records the problem, rejected alternatives and review history. Supersedes the surface half of exec-surface-fails-loudly.

• active — authority-is-belnap-evidence — fs and exec authority is a PBel policy: a function from resolved requests to a pair (positive, negative), composed pointwise and closed to a decision only where it is enforced; an exclusion beats every allowance, an extension (--extend, once) only adds to a ceiling and every later layer restricts, and what a grant lets run or be written it lets be read. Roles are types (policy vs Fragment), every a flag with no negative form, carriers and the linker mere support, allowances frozen and exclusions re-resolved, ral’s binary an ordinary file a bundled tool reads, exarch’s own binary excluded wherever exec restricts, Windows refusing “every path, less exclusions”. Records every departure of the old implementation and why it was wrong, the fourteen decisions with their rationale and rejected alternatives, the seven reviews that shaped them, what was built differently from the plan, the behavior changes, and what the lost write freeze costs (a declared limit, remedied only by a future write-only exclusion). Supersedes a-veto-freezes-what-a-write-covers and the precedence part of one-table-two-instances.

• active — the-image-is-not-pinned — the launcher execs the real path the guard judged on every platform and holds no descriptor on the launched image; the judge→execve window is a declared limit, since any writer who could swap the file could have placed it before judgment. Removes the 12 Oct pin: Program::File is { path, real }, unconfined launches are Launch::new(real), the trampoline execs real inside the envelope, Slot::Image, visible_image, admit_image and image_command are deleted, mounts start at fd 107. A #! script sees its real path as $0 again, and no program inherits a descriptor on itself. Landlock admits the launched file through the table alone, built after judgment. Reversed: the judge→open residual of the-envelope-mounts-by-handle is subsumed, not open.

• accepted — the-seed-rides-the-protocol-sealed — a payload the host relays but never reads crosses as bytes; its content is a contract between the engines at its two ends, and the spawner makes those ends one binary. A sub-agent’s bequest is sealed (Origin::Child(Sealed) in Attach, and FOValue::Bytes in the enquiry), the desk dials a Factory, and the guest daemon spawns every engine on FACTORY_PORT, admitting only VMADDR_CID_HOST. Deletes the hatch: the guest port, the token, the ack, the seed fd, the unreaped-children table, the old hatch-era Birth, Dial. No build-id stamp: PROTOCOL_VERSION gates the envelope before any seed is decoded.

• accepted — sign-in-with-chatgpt-token-sharing — exarch’s chatgpt service speaks OpenAI’s published token-sharing route for open-source apps, and nothing borrowed from the Codex CLI. Loopback-redirect OAuth at auth.openai.com (the device-code flow is deleted), inference at api.openai.com/v1/responses with the plan’s bearer alone, and /v1/models for the catalog; one persisted host id and, per account, the issued client id and retained ID token (SignIn::Register or Reauthorize); the ID token’s payload is decoded and checked (nonce, sub, the plan scope), not signature-verified; Meter::Unpublished, with subscription_sharing_usage_limit_exceeded unwaitable; a plan selection carries effort and no sampling controls or output cap; no store migration. Known gap: genai collapses a mid-stream response.failed.

• active — delimiters-are-handlers-for-poll — a stop is an escape with an owner, not a catchable error: cancellation is one operation, poll, and every delimiter is a handler for it. try catches errors only; a worker’s base consumes a stop naming its own node into the awaiter’s WorkerStopped error; a collector consumes the stops naming its stages’ nodes (forgiveness by name) and tears the siblings down on a stage’s escape; every other stop, like exit, is a top-level effect read as Ending::Stopped. Two cells: Mooring::home written, Shell::scope read, by type; one writer per node; the outermost attaining node is the name; blocked waits are sliced at POLL_SLICE; panics are defects; fail is faithful; poll h total. Amended 2026-10-19: a worker consumes every in-session Cancelled/TimedOut stop, not only one naming its own node, and par is a call-owned builtin that cancels and drains its siblings on every exit (await-is-the-block-run-here). Amended 2026-10-20: the par row is the gather row, par being prelude code over it that still cancels and drains its siblings on every exit (gather).

• active — a-cleanup-is-shielded-within-its-grace — a guard cleanup runs under a shielded child scope that masks every stop from above bar Aborted until since + grace, since being the chain’s first strike and grace the host’s cleanup_grace (5 s): every cleanup of one unwinding ends by one instant, and a run ends within wall + grace + TEARDOWN_GRACE. Cooperative: a group signal still reaches a cleanup’s children, whose death is a failure. Successor to a-failing-cleanup-pre-empts.

• accepted — an-eviction-is-a-span — an eviction takes one contiguous run of the context and leaves one residue standing in its place: a span [from, to] of turn ids, both inclusive, and a note, with no id of its own. Residues nest by containment, so a larger run that covers old residues whole replaces their notes, the same span rewrites one, and a run that reaches into a residue must cover it whole — the one rule the model learns. The context is the frontier — every turn no residue covers and every residue no later residue covers — in id order, a residue rendered by render_residue as one bracketed user-voice message of sentence, note and read-back line, never rows; table order stays id order and TURN: N is unchanged. exarch-context `evict [from, to, note] requires the note; every row is a SpanRow (kind own | import | inherited | residue, location resident | under [from, to] | withdrawn), `index lists residues beside turns and `grep searches notes. The harness’s pressure plan is one prefix span, which may take the live prompt and leaves exactly one residue; it never rewrites a lone residue, and the model, warned first, keeps what was asked only under its own note — reversing an earlier revision that kept the live prompt. The survivor rule and the marker machinery go; /rewind anchors at an item start. Given up: a set with a gap is two evictions. Read against UniiChat: span addressing, nesting by containment, one bounded line and children on demand taken; zoom, the compactor, history as text and the age-merged binary tree not.

• active — await-is-the-block-run-here — await $h behaves as h’s block run at the await, and every concurrent block has exactly one owner, fixed at birth: the calling expression (par, all, race), the session (spawn, watch), or nobody (detach). await replays the worker’s stdout then stderr into the awaiter’s sinks and ends as the block ended; a handle carries its block’s grade, await : Handle^ε α → F^ε α; poll is the one data observation and gains elapsed. A worker’s births hang under its node in its brood: on return it awaits them in birth order, on a halt it cancels and drains them, so cancel $h reaches everything $h started, and its base converts any in-session Cancelled/TimedOut into its own error. par, all and race are Rust over one call-owned birth path (Litter) that ends every child before the call returns. spawn [TITLE] BODY and all [k: BODY] are control operators, since optionality lives in syntax or data, never in a value’s arity; a host’s TitlePolicy may require the title. service, the leases and defer are deleted; a handle’s Stamps are the one clock; workers lists as data and worker <id> is the one door back to a handle. Rejected: a total record-returning await, a gather delimiter, a checker-level title policy, lookup by title, cancel-on-return, re-clocking the idle lease. Amended 2026-10-20: a handle’s result is claimed once, by await, race, cancel or its owner, through one atomic claim that moves it out; a second await fails, race skips a claimed handle and fails only when all are, a second cancel is nothing, and poll claims nothing, so a polled handle stays awaitable and a worker’s join never replays a child an outside await claimed. Amended again 2026-10-20 by gather: the third owner is a gather, poll and first-settled are the two data observations, the Litter and all are gone, and the rejection of a gather delimiter is reversed.

• active — gather — a frame owns the workers born under it, by one mechanism, the brood, and gather { … } gives it syntax; a worker’s body is an implicit gather. Every concurrent block is owned by a gather (hung under the scope it was entered in, joined in birth order on return, cancelled and drained on a halt), the session, or nobody; a gather’s exit also waits, within the grace, for every child it started that was cancelled (I4′). first-settled joins poll as a data observation that claims nothing. The Litter, Birth::Call and the all form are deleted; par is prelude code over gather that keeps input order in bytes and values, beside both and first-of; race stays Rust, the one bounded drain of held handles no gather owns. A gather-owned birth, a worker’s child included, is registered but unannounced. Reverses await-is-the-block-run-here’s rejection of a gather delimiter: one ownership mechanism beats two.

• active — access-is-physical — an access is resolved as the kernel resolves it, and a grant prefix is a logical spelling folded before it is resolved. LexicalPath anchors without folding and LexicalPath::folded is the logical consumers’ explicit step; the walk is the one physical resolver, its Missing::Tolerate mode the lenient canonicaliser, so a deny on a dangling link holds at its target; a trailing separator demands a directory and the root is an object.

related/ — comparison to existing work

ral read against the literature; durable on the external work, keyed to ral’s design pages via the against stamp.

• system-c — Brachthäuser et al. 2022: effects and capabilities reconciled; box = thunk, self-masking as capability-set subtraction, the type-based pole of grant.
• scoped-labels — Leijen 2005: the record calculus row-types implements, minus the restriction primitive — override is shadowing, never removal.
• handlers-of-algebraic-effects — Plotkin–Pretnar 2009: the founding handler calculus, on CBPV, with shell redirection as its own example; ral is its tail-resumptive fragment.
• record-concatenation — Wand 1991, Harper–Pierce 1991, Rémy 1992, Gaster–Jones 1996: the record operation ral declined — concatenation has no principal type (ρ ++ [l: Int] against [l: α | ρ'] has two incomparable solutions), and the three published ways to type it charge compatibility constraints, lacks predicates, or Rémy flags, each already refused elsewhere in ral’s design; a literal with a spread is an update of one base instead, which adds no field. No deletion lifts the restriction — reading a label requires naming it, and the weaker typing is unsound because closed rows are exact — so the borrowable is the predicate route with a modern solver (PureScript’s Union with functional dependencies), at the same price.
• 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’s F carries only its value type, 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 carries no grade at all: a sequence takes its tail’s type rather than multiplying, and a bind annotates nothing. 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 as a fragment of Bruns–Huth’s PBel: the FOUR bilattice is the carrier, ⊕ and ∧ the only operators, ↓ applied once at enforcement; restrict/extend as standard policy composition, deny-overrides as the fail-safe default, and the cross-check of what the code does against the published algebra.
• asynchronous-effects — Ahman–Pretnar 2021/2024: one-way signals out, interrupts in, synchronous calls derived from both — the engine protocol’s calculus; ral keeps enquire primitive for ordering, gives interrupts to the runtime alone, and adds the session scope at which a worker’s signals wait.
• gvisor — Google’s runsc: a userspace reimplementation of the Linux syscall ABI (Sentry + Gofer, each under its own seccomp allow-list) — what ral is instead (authority over OS primitives, two enforcers) and what the typed deny-set takes from it (typed rules, weakenings as first-class data, confining the confiner) versus what it does not (the Sentry itself, OCI plumbing).

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 (Ast::Redirected, CONTROL_OPERATORS); 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, If/CaseArm hold their arms as thunks, and Capture/Decode are checker-inserted; a Pipeline’s value is its final stage’s.
  • ty — the type language as data below the IR: Ty, Kind, Scheme, rendering, and the data of a Site; no unifier, no Value.
  • typecheck — HM with row types; returns an annotated Toplevel (schemes on each Phrase::Define, per-stage value types, Capture/Decode nodes) from one SessionSchemes seed; HeadClass lives in infer.rs; the bind rule, argument adaptation and joins (grade.rs) place capture by type; a non-final stage must write, a pipe edge into a stage-root stdin feed is refused (T0070), and no type relates a stage to its neighbour; handler/alias arms are fixed-arity lambdas that stand in for their head.
  • 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, a ral-written stage as a thread returning its value directly, redirect/exec surfaced at runtime doors, plus the pgid anchor (--ral-pipeline-anchor) held open on every platform.
  • capabilities — the capability model (capability: the lattice and its folds), the guard that reads it in process (guard: free check_*(&Context, …), the freeze, the decoder), path/ grant resolution, and the OS process sandbox (macOS Seatbelt, Linux bwrap, Windows AppContainer over path-derived fs capability SIDs); kernel-denial hints answer once per remedy class — an fs set for a file-* path, the exec set for a process-exec one, the net axis for a socket, and for a Mach or IPC door the base profile’s own recorded reason, since no grant opens one.
  • io-process — byte sinks/sources, the lease-gated foreground handoff, the Cancel|Run reaper daemon; 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 handler stack, the capability types the grant layer interprets (Capabilities, GrantStack), 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 — the wire that carries a shell into a sealed child engine: FOValue, the one first-order value vocabulary (Datum/record! its strict codec), and SerialValue = FOValue<SerialClosure> beside it (seed/table.rs); scopes interned by root identity and rebuilt in dependency order (Kahn); EngineSeed (seed.rs), the scrubbed fork, sealed (seal/Sealed) for the host to relay unread — its environment once, its Context<Vec<WireHandlerFrame>> — with its SpawnGrant crossing unfrozen; length-prefixed frames (frame.rs) under one size fuse, depth-uncapped under serde_stacker, which also carry the engine protocol’s WireChannel.
  • engine-protocol — the one Engine (engine.rs: EngineInstaller, Runtime, Engine::boot, Rails, Scopes; its probe answers in engine/probe.rs), the frame algebra (protocol.rs: Frame, Attach, Event, SessionEvent, Control, Report/Ending; the typed Probe and its rows in protocol/probe.rs; the duplex channel and the liveness law in protocol/channel.rs), the run’s projection onto it (run/report.rs), the two carriers that interpret it (carrier.rs: the Host and Transport traits and their typed probe doors, Ends, dispatch_to_report and the reentrancy registry, Severed; IdentityTransport; WireTransport with its engine half in carrier/wire/serve.rs), the seal a child’s Attach carries (Origin::Child), and SpawnGrant.
  • diagnostics — Span/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 an engine it boots in process and speaks to only through the protocol (no Shell held, batch and REPL booting alike through the _ral-boot door), driving one of two selectable frontends (minimal / readline) over the REPL session and plugins.
  • startup — startup.rs process identity and the repl/batch engine installers, main.rs dispatch, cli.rs argv → Mode (--surface frontend, clap-derived argv terminator), batch.rs booting an IdentityTransport and dispatching the boot door then the script, the annotated-prelude bake, platform glue.
  • loop — the Session state machine over an owned IdentityTransport and no Shell: the two-stage boot (the repl recipe, then the _ral-boot door sourcing profiles and rc engine-side and answering RcSettings), the ReplHost answering repl-editor/repl-plugin enquiries and rendering surfaces, every line, prompt and hook a dispatch, engine state read by probes; the selectable frontend, prompt/theme/rc.
  • frontend — the Frontend trait and its minimal / rustyline editors, each reading the engine only through the transport, the shared prefix-then-fuzzy completion engine over probe-answered sources, and the in-editor plugin surface (ghost text, highlights, keybindings) the editor drives.
  • plugins — the plugin runtime split at the protocol: hooks and aliases registered engine-side by the load doors (each hook’s policy — terminal, aside — its own), editor state and the keybinding router host-side, every hook run a Program::Hook dispatch with source-mapped faults labelled by the engine, the _ed-* builtins as thin doors enquiring repl-editor, a buffer-change circuit breaker, driving the in-editor plugin surface both frontends render.
• exarch — the exarch agent’s front door: startup (CLI dispatch, app/boot, account selection, credential resolution + env scrub, sandbox boot) 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, launch }, two Weak doors over the agent tree, not the tree itself, and the Launch carries the recipe (Genesis) every root is hatched from. 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, per-turn-boundary eviction into the transcript, fresh-shell resume, nudge-retry, sub-agent forks in two memory modes), the construction-fixed Role, HeldByChildren, the fuel spawn budget, the owned hot-swappable provider, dynamic focus, and the subtree cancel cascade over Role::Child/Agent::children (up strong, down weak). A wire-seat trunk’s exarch-agents `start remains one exchange: the engine seals the bequest into its enquiry, the desk makes the child through its Factory capability (the guest daemon, one engine per host dial), and answers only after the child is attached.
  • provider — LLM transport and live model catalogs: famous/custom/ChatGPT-account identity, launch-time --role bindings for spawned agents, 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 the runtime’s syscall sites as structural events, rendered as grouped cards; bulk helper I/O sunk below the ral line, enforced by a clippy-checked set of sites.
  • policy — capability composition as layering: a base ◁ extension ceiling (--extend) with the restrict and deny layers pushed onto a frozen GrantStack, whose per-check fold is the one meet that ever runs, and a spawned child’s adopted fork taking its layer on top of the parent’s stack; the six bake-in profiles, and restrict-file self-denial, and the self layer excluding exarch’s own binary; the boundary is ral’s grant.
  • tools — ral 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, find-files, the skill readers) reading below the redirect frame, the agent.ral kit over them, and the harness verbs the desk answers over one typed enquiry vocabulary (enquiry.rs, one strict decode for door and desk) (exarch-context over what the provider is sent and exarch-transcript over everything the lineage recorded, both speaking turns, the exarch-agents spawn family, exarch-schedules, exarch-pins, 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 on the focused tab, any number of root tabs, and an in-flight reply as a provisional edge.
  • cards — the exarch-surface render document: a closed set of five 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 and accounted for afterwards — a stat-only walk at the opening and another after each exchange, and a plain-language report of the difference; nothing is put back and nothing of the folder is ever read — 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 desk asks MachineFactory (the Factory over Machine::connect_guest) for an engine, and the guest daemon spawns one per host dial on FACTORY_PORT (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).
• repl — the ral binary, including bridge.rs: ral invoked as ral-sh is the POSIX-bridge login shell, routing -c strings and scripts to /bin/sh and interactive sessions to itself.