Binding leases

An exarch agent’s top-level scratch names expire when the model stops using them; nothing else about binding does. The model treats top-level let as scratch paper and never erases, so a long session accumulates dead strings, forgotten closures, and settled handles still holding captured output. The binding-lease ledger (core/src/types/shell/bindings.rs, armed only by exarch) removes a name once it has gone 256 ral calls without use — and does nothing else: ral’s semantics are untouched, the REPL never expires anything, and a pruned name afterwards reads exactly like a name that was never bound. agent-binding-reaping is the decision record; this page is how it runs.

What is leased, and what never is

Only names the model itself binds at the session’s top level — residency is by ρ, and a name only Σ answers (a native, a prelude function) is never a ρ entry at all, so it is not a candidate to prune rather than merely exempt from it. Everything else visible when exarch arms the ledger — agent library, rc and host seeds — is sealed as baseline, permanently exempt (Shell::arm_binding_lease, armed once by shell_eval::arm_session_ledgers in the engine’s own boot recipe, so /clear’s rebooted engine re-seals for free). A fork seals its entire inherited scope on the parent’s terms, in core rather than by the host: Shell::construct arms the child’s ledger from the bequest’s terms, sealing every inherited name as baseline, the same code on either seat. So a fork’s lease governs only the names the child itself writes. Its baseline read, Env::all_bindings, still folds in Σ’s prelude beside ρ, so a prelude name that has not been shadowed is sealed as a harmless redundancy over a name the ledger could never reach. Bindings made inside blocks, lambdas, use bodies, or letrec fixpoint frames are invisible to the ledger, since its one chokepoint, note_define, is reached from run_phrases’s Define arm alone, under Mode::Session: they die with their frame anyway.

The clock, and what counts as use

The ledger ticks once per committed source-door run — in exarch, exactly once per ral tool call. No wall clock anywhere: a quiet weekend ages nothing.

Use is read off the program text, never off the running lookup path. When a run compiles, Toplevel::referenced_names collects every variable occurrence and command-head name and renews those entries; the same harvest runs when use (or a host loader) compiles code mid-run. It is the same Mentions walk a node’s own occ is built from (ir): a nested Thunk, list, record, map, or Rec group contributes its own already-computed occ rather than being walked again, so the harvest, like occ itself, is linear in the program’s size and a stored body’s names are counted once, at the run that compiled it, not on every later call. Closure::new keeps exactly what that occ names (a-closure-keeps-only-what-it-mentions). Nothing renews at dispatch: a bare head can only resolve to a binding the elaborator already saw — prelude, session, and lexical names are all in its bound set, and nothing installs into a running environment behind its back — so the harvest is complete by construction. Writing a name is also using it — a rebind restamps at the chokepoint. A run that fails to parse or typecheck ticks the clock but renews nothing: failed runs age your scratch. Listing (/resources, any enumeration) renews nothing either — enumeration is not observation.

What pruning does — and deliberately does not do

At each ready boundary — the tail of every run door — Shell::emit_ready_boundary_notices calls BindingLedger::prune beside the worker-reap drain (take_worker_reap_notices), both only when a surface sink is installed — absent one the ledgers are left untouched, so the notices wait for a run that has one. Every entry idle past the bound is examined: a name whose value still structurally reaches a running worker handle is pinned and re-checked next boundary (pins_running_work — it recurses lists, maps, and variant payloads, and deliberately never looks inside a closure’s captured environment); everything else is unset — value and type-scheme seed in one act — and one Notice::Prune surfaces to the host, which records it as a Forensic::Prune naming what fell (shell_eval::surface::record), shown to no one. A pruned name cannot come back through a panic rollback: Shell::run checkpoints env / context at run entry, after any earlier prune, so the rollback target already excludes what fell. Pruning is the ready boundary’s own door — reached only between runs, on the session scope by construction — so a mid-frame caller such as a builtin body is refused rather than allowed to unset from a transient frame.

What it does not do: it never touches a closure, so it frees a value’s bytes only when no live closure mentions its name, and it never tells the model anything at prune time — the only model-visible consequence is an ordinary undefined variable diagnostic, refused before it runs, if the model names the binding again, with the paper trail waiting in record.jsonl’s Forensic::Prune breadcrumb.

The capture scenario, worked

The case that looks alarming and isn’t:

let big = <5 MB of text>
let f = { … $big … }        # then f is called every run

f renews every call — its name is in each run’s text. big does not: its reference lives inside f’s stored body, compiled once on the run that defined f; later calls recompile nothing, so nothing harvests big again. After 256 idle calls the live name big is pruned — and f keeps working, forever. A closure keeps, at creation, the session bindings its body mentions — big among f’s — and resolves its body against that scope; the session scope is copy-on-write, so unsetting big there cannot reach what f already holds.

This is correct, not a near-miss: once captured, the top-level name big routes nothing. The value’s real owner is f’s capture, and f — the thing actually being used — is the thing whose lease renews. The cost is memory, not correctness: a closure keeps only what it mentions, so pruning big frees its bytes unless a live closure mentions big; f’s capture keeps them resident until f’s own name falls or is rebound and the capture drops. That residency is exactly what the large-binding warning exists to head off — bind a file path, not five megabytes of captured text.

There is no command-position exception: big args inside hot f compiles to an application of the bound variable, exactly like $big, resolves through the captured chain, and touches nothing. What a stored body mentions is harvested once, on the run that compiled it. A false renewal only ever lengthens a lease; the harvest over-approximates in the safe direction throughout.

Where it sits in the decay ladder

Abandonment decays in layers, each with its own bound and its own log line: a worker’s settled registry entry expires after 256 calls unclaimed; and a name holding a settled handle — settled handles are ordinary scratch, and the worker registry retains the handle itself, so no name is ever load-bearing for rediscovery — prunes after 256 idle calls. The model’s later “where did my job go?”, at every layer, has an answer in the log.

See also shell-state (the ledger’s home on LocalState), agent (arming sites and the boundary drain), probe-convention (the /resources rows the ledger answers), and output-capture-and-detachment (the worker half of the same story).