Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
# Only a synchronous proof authorizes a PTY write

Status: proposed — the transport-authorization half stands; the scheduling half is withdrawn to an open
question. Do not treat as accepted.

## Context

Two positions were chosen independently. Delivery was to converge onto observed harness state, so that the
per-agent state becomes the source of truth for "is it safe to DING this agent right now", replacing the
one-shot composer gate. Separately, routing was to be **fail-open** for unobservable agents, so a broken
hook never stalls an inbox. But `INVARIANTS.md` pins **Fail-closed observed native DING** — "unread,
blocked, timed-out, errored, unknown, and unrecognized states retain ownership and later FIFO work remains
blocked", with eighteen named tests in `src/ding/mod.rs` — so a design that lets "unknown = interruptible"
reach the DING path deletes that clause.

This record does not reconcile the two positions. It **declines convergence on transport authorization** —
the first position is overruled — and defers the second.

## Decision

Observed harness state is **inadmissible as transport authorization**. The PTY transport layer asks the
synchronous, adjacent composer proof, unchanged; only `ScreenObservation::ProvenIdle` authorizes;
`ActivityState` is not a parameter of that decision and must not become one.

The screen scraper is folded in as an observer that *feeds* shared state — the DING loop publishes what its
already-budgeted peek proved — never as a consumer that reads it. This keeps **Bounded DING PTY probe
churn** intact: a reader must never drive a `pty peek`.

**Withdrawn: whether observed state may schedule.** The routing layer that would call `is_interruptible`
does not exist, in code or in `spec.md`, so fail-open routing is an open question rather than a decision. It
carries a live cost: if the DING loop ever withholds a poke because observed state is `active`, that is a
**second pre-attempt deferral gate**, and invariant row 17 ("`busy` delivers immediately; only fresh `dnd`
defers", pinned by `pending_delivery_ignores_busy_but_respects_fresh_dnd_archive_and_retry`) needs amending.
This record does not amend it and must not be read as having cleared it.

## Options

| Option | Tradeoffs |
| --- | --- |
| Observed state gates DING directly, fail-open on `unknown` | Delivers the stated goal literally. Deletes the invariant's central clause: an unobservable agent is pasted into blind. Loses adjacency, so it is unsafe even when the observed state is correct. |
| Fail-closed everywhere; unobservable agents are never routed | Preserves the invariant trivially. Makes a broken hook silently remove an agent from the fleet. |
| Only the synchronous proof authorizes; scheduling left undecided | Requires holding two verdicts, and gives PTY agents no "never stalls an inbox" property. Keeps the invariant intact by construction and makes the residual stall visible for the first time. |

## Evidence and Argument

- **Implementation fact — the code already splits the two layers.** Before any bytes are sent,
`observed_poke_with_window` maps an unprovable screen to `PokeOutcome::Deferred`
(`src/ding/mod.rs:607-609`) and `flush_pending` breaks without staging (`:1106`); once a paste may have
landed, every ambiguity yields `Staged` (`:614-617`, `:626-628`, `:680-687`). The invariant's "retain
ownership" clause governs the post-transport phase: it is an *exactly-once* guarantee, not a
never-attempt-when-unsure guarantee.
- **Implementation fact — the native exemption is enforced, not merely true.**
`crates/agent-spec/src/spec.rs:887-888` refuses a declaration carrying both `ding` and `deliver`, so a
natively-delivered agent cannot enter the PTY path at all.
- **Implementation fact — durable state cannot supply what the gate requires.** The gate's safety comes from
*adjacency*: `submit_after_final_observation` is intentionally adjacent to the bare-Return operation, and
`retry_staged_with_window` sends one bare Return only after **two adjacent** `RetainedSafe` observations.
A record written by another process at another time supplies neither. PR #123 draws the same line from the
other side — its lease is capped at two seconds and re-verified against a live PTY STATUS packet before a
generation-guarded write, and a durable record is strictly weaker evidence than that lease.
- **Independent critique — delivered, and it weakened the record.** The reviewer looked for a path by which
an activity signal authorizes a write or releases staged ownership and found none, which is the direct
question. But three supports fell. "rustc enforces the separation" does not survive:
`pty_transport_authorized` and `is_interruptible` have **no production caller** — every call site is
`#[cfg(test)]` — so the property is trivially true of uncalled code and needs a real mechanism the moment
a consumer exists. The two claimed invariant oracles pin structure rather than behaviour; one asserts that
a function whose body is `matches!(screen, ProvenIdle)` equals `screen == ProvenIdle`. And the reviewer
found a concrete defect in the prototype this record cites: its PTY observer proves `idle` for a Claude
pane exactly once, before anyone types into it.

## Consequences

- **Fail-closed observed native DING** needs no amendment. Nothing here reaches the phase it governs.
- Fail-open would not deliver "a broken hook never stalls an inbox" for PTY agents and cannot: if a pane is
permanently unprovable the message stays undelivered whatever a router decides. The honest gain is that
the stall becomes *visible* as `unknown`/`unproven` beside a declared `busy`. Any escape hatch that pastes
into an unprovable pane must be explicitly authored.
- The `reason` field is diagnostic, not a safety hinge; nothing gates on it.
- The **Bounded DING PTY probe churn** claim above is about `pty peek` only. A separate prerequisite is
unresolved: `CodexInboxDelivery` watches the whole agent directory unfiltered
(`src/codex_app_server.rs:326`), so a frequently-written `lifecycle/` beside the inbox turns every
observed transition into an inbox scan. **Mutation-only filesystem wakeups** does not cover it —
`is_mutation` (`src/watch.rs:67-73`) filters `Access`, stopping *read* self-wakes only — so that watcher
must be scoped before the record ships.
- Convergence remains possible on what is actually shared — pre-attempt selection, FIFO ordering, backoff
scheduling. The adjacent proof stays regardless.

## Evidence required for acceptance

- a named test pinning that no PTY write path takes an `ActivityState`. This is a **precondition**, not a
consequence: without a production consumer the guarantee is vacuous;
- a production consumer of the observed state, so the separation is a property of the system;
- a ruling on the withdrawn scheduling half, with invariant row 17 either amended or confirmed unaffected by
a named test;
- the PTY observer's Claude defect closed, or the observer cut from this increment.
27 changes: 27 additions & 0 deletions docs/vrs/.experiments/2026-08-17-captures/capture-a-trivial.jsonl
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
{"t_ms": 0.0, "dir": "out", "frame": {"jsonrpc": "2.0", "id": 0, "method": "initialize", "params": {"clientInfo": {"name": "st2-spike", "title": "st2 spike", "version": "0.0.1"}}}}
{"t_ms": 301.8, "dir": "in", "frame": {"id": 0, "result": {"userAgent": "st2-spike/0.147.0 (NixOS 26.5.0; x86_64) ghostty/1.3.2-HEAD-_6143bac (st2-spike; 0.0.1)", "codexHome": "/home/schickling/.codex", "platformFamily": "unix", "platformOs": "linux"}}}
{"t_ms": 301.9, "dir": "in", "frame": {"method": "remoteControl/status/changed", "params": {"status": "disabled", "serverName": "dev3", "installationId": "b7a622cd-23ef-4915-91a4-ab55a5531179", "environmentId": null}, "emittedAtMs": 1786982514055}}
{"t_ms": 1500.2, "dir": "out", "frame": {"jsonrpc": "2.0", "method": "initialized", "params": {}}}
{"t_ms": 2000.4, "dir": "out", "frame": {"jsonrpc": "2.0", "id": 1, "method": "thread/start", "params": {"cwd": "/tmp/claude-1000/-home-schickling--megarepo-github-com-compoundingtech-st2-refs-heads-schickling-2026-08-17-pi/b7178fd6-43b2-4fc3-9632-e88398ea323c/scratchpad", "approvalPolicy": "never", "sandboxPolicy": {"mode": "read-only"}}}}
{"t_ms": 2265.1, "dir": "in", "frame": {"id": 1, "result": {"thread": {"id": "01a01075-4436-7b41-af77-baab14d82125", "extra": null, "sessionId": "01a01075-4436-7b41-af77-baab14d82125", "forkedFromId": null, "parentThreadId": null, "preview": "", "ephemeral": false, "section": null, "sectionEnteredAt": null, "historyMode": "legacy", "modelProvider": "openai", "createdAt": 1786982516, "updatedAt": 1786982516, "recencyAt": 1786982516, "status": {"type": "idle"}, "path": "/home/schickling/.codex/sessions/2026/08/17/rollout-2026-08-17T18-01-55-01a01075-4436-7b41-af77-baab14d82125.jsonl", "cwd": "/tmp/claude-1000/-home-schickling--megarepo-github-com-compoundingtech-st2-refs-heads-schickling-2026-08-17-pi/b7178fd6-43b2-4fc3-9632-e88398ea323c/scratchpad", "cliVersion": "0.147.0", "source": "vscode", "canAcceptDirectInput": true, "threadSource": null, "agentNickname": null, "agentRole": null, "gitInfo": null, "name": null, "turns": []}, "model": "gpt-5.6-sol", "modelProvider": "openai", "serviceTier": null, "cwd": "/tmp/claude-1000/-home-schickling--megarepo-github-com-compoundingtech-st2-refs-heads-schickling-2026-08-17-pi/b7178fd6-43b2-4fc3-9632-e88398ea323c/scratchpad", "runtimeWorkspaceRoots": ["/tmp/claude-1000/-home-schickling--megarepo-github-com-compoundingtech-st2-refs-heads-schickling-2026-08-17-pi/b7178fd6-43b2-4fc3-9632-e88398ea323c/scratchpad"], "instructionSources": ["/home/schickling/.codex/AGENTS.md"], "approvalPolicy": "never", "approvalsReviewer": "user", "sandbox": {"type": "readOnly", "networkAccess": false}, "activePermissionProfile": {"id": ":read-only", "extends": null}, "reasoningEffort": "low", "multiAgentMode": "explicitRequestOnly"}}}
{"t_ms": 2265.2, "dir": "in", "frame": {"method": "thread/started", "params": {"thread": {"id": "01a01075-4436-7b41-af77-baab14d82125", "extra": null, "sessionId": "01a01075-4436-7b41-af77-baab14d82125", "forkedFromId": null, "parentThreadId": null, "preview": "", "ephemeral": false, "section": null, "sectionEnteredAt": null, "historyMode": "legacy", "modelProvider": "openai", "createdAt": 1786982516, "updatedAt": 1786982516, "recencyAt": 1786982516, "status": {"type": "idle"}, "path": "/home/schickling/.codex/sessions/2026/08/17/rollout-2026-08-17T18-01-55-01a01075-4436-7b41-af77-baab14d82125.jsonl", "cwd": "/tmp/claude-1000/-home-schickling--megarepo-github-com-compoundingtech-st2-refs-heads-schickling-2026-08-17-pi/b7178fd6-43b2-4fc3-9632-e88398ea323c/scratchpad", "cliVersion": "0.147.0", "source": "vscode", "canAcceptDirectInput": true, "threadSource": null, "agentNickname": null, "agentRole": null, "gitInfo": null, "name": null, "turns": []}}, "emittedAtMs": 1786982516019}}
{"t_ms": 2265.2, "dir": "in", "frame": {"method": "warning", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "message": "Under-development features enabled: external_agent_memory_import, realtime_conversation, runtime_metrics, terminal_visualization_instructions. Under-development features are incomplete and may behave unpredictably. To suppress this warning, set `suppress_unstable_features_warning = true` in /home/schickling/.codex/config.toml."}, "emittedAtMs": 1786982516019}}
{"t_ms": 2265.2, "dir": "in", "frame": {"method": "mcpServer/startupStatus/updated", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "name": "playwright", "status": "starting", "error": null, "failureReason": null}, "emittedAtMs": 1786982516019}}
{"t_ms": 2265.3, "dir": "in", "frame": {"method": "mcpServer/startupStatus/updated", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "name": "agentation", "status": "starting", "error": null, "failureReason": null}, "emittedAtMs": 1786982516019}}
{"t_ms": 2300.8, "dir": "out", "frame": {"jsonrpc": "2.0", "id": 2, "method": "turn/start", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "input": [{"type": "text", "text": "Say hi in exactly three words. Do not use any tools."}]}}}
{"t_ms": 2303.1, "dir": "in", "frame": {"id": 2, "result": {"turn": {"id": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "items": [], "itemsView": "notLoaded", "status": "inProgress", "error": null, "startedAt": null, "completedAt": null, "durationMs": null}}}}
{"t_ms": 2334.3, "dir": "in", "frame": {"method": "thread/status/changed", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "status": {"type": "active", "activeFlags": []}}, "emittedAtMs": 1786982516088}}
{"t_ms": 2334.4, "dir": "in", "frame": {"method": "turn/started", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "turn": {"id": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "items": [], "itemsView": "notLoaded", "status": "inProgress", "error": null, "startedAt": 1786982516, "completedAt": null, "durationMs": null}}, "emittedAtMs": 1786982516088}}
{"t_ms": 2398.9, "dir": "in", "frame": {"method": "mcpServer/startupStatus/updated", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "name": "agentation", "status": "ready", "error": null, "failureReason": null}, "emittedAtMs": 1786982516152}}
{"t_ms": 2491.9, "dir": "in", "frame": {"method": "mcpServer/startupStatus/updated", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "name": "playwright", "status": "ready", "error": null, "failureReason": null}, "emittedAtMs": 1786982516245}}
{"t_ms": 5129.9, "dir": "in", "frame": {"method": "warning", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "message": "Skill descriptions were shortened to fit the skills context budget. Codex can still see every skill, but some descriptions are shorter. Disable unused skills or plugins to leave more room for the rest."}, "emittedAtMs": 1786982518883}}
{"t_ms": 5190.3, "dir": "in", "frame": {"method": "hook/started", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "run": {"id": "session-start:5:/etc/codex/requirements.toml", "eventName": "sessionStart", "handlerType": "command", "executionMode": "sync", "scope": "thread", "sourcePath": "/etc/codex/requirements.toml", "source": "system", "displayOrder": 5, "status": "running", "statusMessage": null, "startedAt": 1786982518, "completedAt": null, "durationMs": null, "entries": []}}, "emittedAtMs": 1786982518944}}
{"t_ms": 5238.2, "dir": "in", "frame": {"method": "hook/completed", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "run": {"id": "session-start:5:/etc/codex/requirements.toml", "eventName": "sessionStart", "handlerType": "command", "executionMode": "sync", "scope": "thread", "sourcePath": "/etc/codex/requirements.toml", "source": "system", "displayOrder": 5, "status": "completed", "statusMessage": null, "startedAt": 1786982518, "completedAt": 1786982518, "durationMs": 48, "entries": []}}, "emittedAtMs": 1786982518992}}
{"t_ms": 5238.5, "dir": "in", "frame": {"method": "hook/started", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "run": {"id": "user-prompt-submit:6:/etc/codex/requirements.toml", "eventName": "userPromptSubmit", "handlerType": "command", "executionMode": "sync", "scope": "turn", "sourcePath": "/etc/codex/requirements.toml", "source": "system", "displayOrder": 6, "status": "running", "statusMessage": null, "startedAt": 1786982518, "completedAt": null, "durationMs": null, "entries": []}}, "emittedAtMs": 1786982518992}}
{"t_ms": 5281.2, "dir": "in", "frame": {"method": "hook/completed", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "run": {"id": "user-prompt-submit:6:/etc/codex/requirements.toml", "eventName": "userPromptSubmit", "handlerType": "command", "executionMode": "sync", "scope": "turn", "sourcePath": "/etc/codex/requirements.toml", "source": "system", "displayOrder": 6, "status": "completed", "statusMessage": null, "startedAt": 1786982518, "completedAt": 1786982519, "durationMs": 42, "entries": []}}, "emittedAtMs": 1786982519035}}
{"t_ms": 5281.6, "dir": "in", "frame": {"method": "item/started", "params": {"item": {"type": "userMessage", "id": "01a01075-50fb-72c3-8c16-381d43eec073", "clientId": null, "content": [{"type": "text", "text": "Say hi in exactly three words. Do not use any tools.", "text_elements": []}]}, "threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "startedAtMs": 1786982519035}, "emittedAtMs": 1786982519035}}
{"t_ms": 5281.7, "dir": "in", "frame": {"method": "item/completed", "params": {"item": {"type": "userMessage", "id": "01a01075-50fb-72c3-8c16-381d43eec073", "clientId": null, "content": [{"type": "text", "text": "Say hi in exactly three words. Do not use any tools.", "text_elements": []}]}, "threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "completedAtMs": 1786982519035}, "emittedAtMs": 1786982519035}}
{"t_ms": 5654.7, "dir": "in", "frame": {"method": "account/rateLimits/updated", "params": {"rateLimits": {"limitId": "premium", "limitName": null, "primary": null, "secondary": null, "credits": {"hasCredits": false, "unlimited": false, "balance": "0"}, "individualLimit": null, "spendControlReached": null, "planType": null, "rateLimitReachedType": null}}, "emittedAtMs": 1786982519408}}
{"t_ms": 5655.3, "dir": "in", "frame": {"method": "thread/status/changed", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "status": {"type": "systemError"}}, "emittedAtMs": 1786982519409}}
{"t_ms": 5655.4, "dir": "in", "frame": {"method": "error", "params": {"error": {"message": "You've hit your usage limit. Visit https://chatgpt.com/codex/settings/usage to purchase more credits or try again at Aug 20th, 2026 5:31 AM.", "codexErrorInfo": "usageLimitExceeded", "additionalDetails": null}, "willRetry": false, "threadId": "01a01075-4436-7b41-af77-baab14d82125", "turnId": "01a01075-4558-7fb0-a540-cc2b1c861aa0"}, "emittedAtMs": 1786982519409}}
{"t_ms": 5655.7, "dir": "in", "frame": {"method": "turn/completed", "params": {"threadId": "01a01075-4436-7b41-af77-baab14d82125", "turn": {"id": "01a01075-4558-7fb0-a540-cc2b1c861aa0", "items": [], "itemsView": "notLoaded", "status": "failed", "error": {"message": "You've hit your usage limit. Visit https://chatgpt.com/codex/settings/usage to purchase more credits or try again at Aug 20th, 2026 5:31 AM.", "codexErrorInfo": "usageLimitExceeded", "additionalDetails": null}, "startedAt": 1786982516, "completedAt": 1786982519, "durationMs": 3341}}, "emittedAtMs": 1786982519409}}
Loading
Loading