Skip to content
Merged
8 changes: 4 additions & 4 deletions INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ materialization, messaging, DING, or presence must preserve them.
| **Clean exec teardown** | Killing an exec task reaps its whole process group. | `tests/exec_backend.rs::exec_kill_reaps_the_whole_process_group_not_just_the_leader` |
| **Bounded restart diagnostics** | Relaunching an exec task preserves the just-finished log as one prior generation while bounding retained diagnostics to current plus prior. Final retirement removes the PID and both logs. | `tests/exec_backend.rs::exec_restart_reap_keeps_bounded_diagnostics_and_final_remove_cleans_them`; `tests/run.rs::up_once_finally_removes_dead_retired_tasks_without_restarting_them` |
| **Exactly-once-safe native bus** | Messages use stable `<unix-ms>-<rand6>.md` files. An archive filename is a durable receipt that shadows and cleans restored inbox replicas and makes repeated archive cleanup idempotent. | `src/message.rs::filename_grammar`; `src/message.rs::archive_receipt_suppresses_and_idempotently_cleans_a_restored_inbox_copy`; `tests/message.rs` |
| **Fail-closed observed native DING** | Each unread message becomes one normalized `[DING]` frame. A maintained Codex or Claude composer must be positively empty before a bracketed paste, then show the exact notice in two immediately adjacent inspections before a separate bare Return. Human, modal, active, changed, timed-out, and unknown states never receive Return. Once paste starts, inspect-only staged ownership prevents duplicate paste across command failures, archive races, and restart adoption. Startup backlog otherwise becomes one generic recovery DING; new arrivals remain FIFO; `busy` delivers immediately; only fresh `dnd` defers. | `src/ding.rs::poke_text_normalizes_and_bounds_untrusted_fields`; `src/ding.rs::malicious_controls_cannot_escape_the_single_paste_frame`; `src/ding.rs::pty_stage_and_submit_are_separate_exact_sequences`; `src/ding.rs::maintained_composer_classifiers_require_exact_idle_state`; `src/ding.rs::paste_then_two_exact_observations_precede_return`; `src/ding.rs::changed_modal_ambiguous_and_bounded_timeout_never_return`; `src/ding.rs::final_observation_change_and_staged_retry_are_fail_closed`; `src/ding.rs::staged_ownership_survives_archive_and_never_repastes`; `src/ding.rs::pty_commands_have_a_real_outer_timeout`; `src/ding.rs::session_watch_has_startup_grace_debounce_and_live_reset`; `src/ding.rs::new_arrivals_is_fifo_and_archive_receipts_prevent_reding`; `src/ding.rs::pending_delivery_ignores_busy_but_respects_fresh_dnd_archive_and_retry`; `src/ding.rs::startup_recovery_notice_retries_in_memory`; `src/ding.rs::startup_backlog_gets_one_generic_recovery_then_new_arrivals_poke` |
| **Mutation-only filesystem wakeups** | Supervisor and DING filesystem watchers ignore read/open access events and wake early only for create, modify, rename, or remove events. Their own catalog and inbox reads therefore cannot bypass the bounded timer cadence or form a Linux inotify CPU loop. | `src/watch.rs::only_mutations_wake_watch_loops`; `src/watch.rs::linux_reads_are_silent_but_real_mutations_wake`; `src/ding.rs::idle_ding_does_not_spin_on_its_own_inbox_reads`; `src/run.rs::idle_supervisor_does_not_spin_on_its_own_catalog_reads` |
| **Bounded DING PTY probe churn** | An unsafe or active composer retains its FIFO notice but deferred delivery retries use a bounded backoff, so each inbox poll cannot spawn another short-lived PTY probe. | `src/ding.rs::deferred_delivery_backoff_bounds_short_lived_pty_attempts` |
| **Agent-declared presence discipline** | The shipped bus contract requires agents to declare `busy` before executing work, use `available` only while yielding or ready, and reserve `dnd` for an explicit hold. Both native harnesses materialize that contract. Busy remains observable but does not suppress DING; fresh `dnd` is the only delivery gate. | `tests/compile_agent.rs::compile_agent_generates_claude_then_materializes_verbatim_persona`; `tests/compile_agent.rs::compile_agent_generates_codex_then_materializes_composed_agents_md`; `src/ding.rs::pending_delivery_ignores_busy_but_respects_fresh_dnd_archive_and_retry` |
| **Fail-closed observed native DING** | Each unread message becomes one normalized `[DING]` frame. A maintained Codex or Claude composer must be positively empty before a bracketed paste, then show the exact notice in two immediately adjacent inspections before a separate bare Return. Human, modal, active, changed, timed-out, and unknown states never receive Return. Once paste starts, inspect-only staged ownership prevents duplicate paste across command failures, archive races, and restart adoption. Startup backlog otherwise becomes one generic recovery DING; new arrivals remain FIFO; `busy` delivers immediately; only fresh `dnd` defers. | `src/ding/mod.rs::poke_text_normalizes_and_bounds_untrusted_fields`; `src/ding/mod.rs::malicious_controls_cannot_escape_the_single_paste_frame`; `src/ding/mod.rs::pty_stage_and_submit_are_separate_exact_sequences`; `src/ding/mod.rs::maintained_composer_classifiers_require_exact_idle_state`; `src/ding/mod.rs::paste_then_two_exact_observations_precede_return`; `src/ding/mod.rs::changed_modal_ambiguous_and_bounded_timeout_never_return`; `src/ding/mod.rs::final_observation_change_and_staged_retry_are_fail_closed`; `src/ding/mod.rs::staged_ownership_survives_archive_and_never_repastes`; `src/ding/mod.rs::pty_commands_have_a_real_outer_timeout`; `src/ding/mod.rs::session_watch_has_startup_grace_debounce_and_live_reset`; `src/ding/mod.rs::new_arrivals_is_fifo_and_archive_receipts_prevent_reding`; `src/ding/mod.rs::pending_delivery_ignores_busy_but_respects_fresh_dnd_archive_and_retry`; `src/ding/mod.rs::startup_recovery_notice_retries_in_memory`; `src/ding/mod.rs::startup_backlog_gets_one_generic_recovery_then_new_arrivals_poke` |
| **Mutation-only filesystem wakeups** | Supervisor and DING filesystem watchers ignore read/open access events and wake early only for create, modify, rename, or remove events. Their own catalog and inbox reads therefore cannot bypass the bounded timer cadence or form a Linux inotify CPU loop. | `src/watch.rs::only_mutations_wake_watch_loops`; `src/watch.rs::linux_reads_are_silent_but_real_mutations_wake`; `src/ding/mod.rs::idle_ding_does_not_spin_on_its_own_inbox_reads`; `src/run.rs::idle_supervisor_does_not_spin_on_its_own_catalog_reads` |
| **Bounded DING PTY probe churn** | An unsafe or active composer retains its FIFO notice but deferred delivery retries use a bounded backoff, so each inbox poll cannot spawn another short-lived PTY probe. | `src/ding/mod.rs::deferred_delivery_backoff_bounds_short_lived_pty_attempts` |
| **Agent-declared presence discipline** | The shipped bus contract requires agents to declare `busy` before executing work, use `available` only while yielding or ready, and reserve `dnd` for an explicit hold. Both native harnesses materialize that contract. Busy remains observable but does not suppress DING; fresh `dnd` is the only delivery gate. | `tests/compile_agent.rs::compile_agent_generates_claude_then_materializes_verbatim_persona`; `tests/compile_agent.rs::compile_agent_generates_codex_then_materializes_composed_agents_md`; `src/ding/mod.rs::pending_delivery_ignores_busy_but_respects_fresh_dnd_archive_and_retry` |
| **Stable roster JSON** | `st2 agents --json [--enrich]` preserves field names, order, null handling, presence, explicit retirement state, activity, and inbox counts. Human output marks retired declarations without changing active rows. | `src/agents.rs::agents_json_has_stable_wire_shape`; `tests/status_agents.rs::roster_json_and_human_output_distinguish_retirement_from_presence` |
| **Agent-declared presence** | Refresh preserves non-DND declared status and only advances liveness; a missing status starts as `available`, while `dnd` is never refreshed and an unrefreshed declaration ages to `unknown`. | `src/status.rs::refresh_preserves_value_and_bumps_mtime`; `src/status.rs::refresh_leaves_dnd_to_age_out`; `src/status.rs::refresh_missing_writes_available_default`; `src/status.rs::stale_mtime_reads_as_unknown_regardless_of_contents` |
| **Retirement health** | A retired declaration is healthy only after every declared task ID is absent. Any live or dead declared task record reports incomplete retirement; retired declarations do not require presence. Live declarations retain their existing task and presence checks. | `tests/doctor.rs::retired_declaration_is_healthy_when_tasks_and_presence_are_absent`; `tests/doctor.rs::retired_declaration_is_unhealthy_while_a_declared_task_is_alive`; `tests/doctor.rs::retired_declaration_is_unhealthy_while_a_dead_task_record_remains` |
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
# DING harness dispatch is positional, and each harness owns its own vocabulary

Status: accepted

## Context

DING classified a screen by asking, in a fixed order, whether it looked like one
maintained harness and then the other, and it applied one shared active-turn and
modal predicate to every harness. Both choices were sound while the classifier
was small. Both produced defects once a real fleet ran against it.

Ordered dispatch has no way to express *which composer will receive the
keystrokes*. It answers "does this screen contain harness X" when the safety
question is "what will this pane do with input". A shared blocked-predicate has
the same shape of error one level down: it lets one harness's rendering decide
another harness's safety gate.

Splitting the implementation into one module per harness forced the question,
because a module boundary has to be drawn somewhere, and the wrong boundary
would have preserved both defects behind a tidier layout.

## Evidence and Argument

Three independent forms, none of which is reasoning alone:

- **Implementation fact.** The shared active-turn predicate contains literals
drawn from one harness's rendering — plan prompts, capacity notices, retry
hints — and applies them to every pane. It also *omitted* that harness's
animated progress line, which does not always carry an interrupt hint. The
omission is only invisible while a separate parse defect keeps such screens
unclassifiable; removing that defect makes a mid-turn pane satisfy both the
idle and empty proofs.
- **Independent critique.** An automated review of the change that reordered the
two harness checks identified the transcript case: a pane whose scrollback
contains a captured screen from another harness would be classified on that
scrollback rather than on its own live composer, admitting a paste — or a
Return — into a human's draft. This was found by an adversarial reader, not by
the change's author.
- **Implementation fact.** The two harnesses do not match against the same
representation. One locates its composer in the raw screen including escape
sequences, yielding a byte offset; the other locates against ANSI-stripped
lines, yielding a line index. Any positional rule must therefore normalize to
a common unit, which an ordered chain never had to confront and which a naive
positional comparison would get silently wrong.

## Options

| Option | Tradeoffs |
| --- | --- |
| Keep ordered dispatch, special-case the transcript screen | Smallest change. The rule has to be written for each pair of harnesses, so it grows quadratically, and the next harness reopens the same class of defect. Does not address the shared predicate. |
| Reverse the order instead | Trades one wrong answer for another: it restores the original defect, where a used pane of the first harness is unclassifiable, from the opposite side. |
| Positional dispatch over a harness registry, with per-harness vocabulary | Requires an interface, a position type, and a unit conversion that did not previously exist. Duplicates some near-identical interrupt literals across harnesses. Makes the transcript case structural rather than special-cased, and confines each harness's rendering to its own safety gate. |

## Decision

Positional dispatch over a registry, with each harness owning its composer
markers, footer chrome, idle proof, and active-turn and modal detection.

Every registered harness is asked to locate a composer; the one lowest on the
screen is classified. This is correct by construction rather than by
enumeration: scrollback is above the live composer, so the composer that will
receive the keystrokes is the lowest one, whatever a transcript happens to
contain. Positions are normalized to a screen row before comparison, because the
harnesses report incomparable units.

Shared code keeps only what is genuinely common to every harness. The duplicated
interrupt literals are accepted cost: a shared vocabulary is what let one
harness's strings, and one harness's omissions, silently govern another's panes.

## Consequences

- Adding a harness is a new module and a registry entry; it does not edit shared
classification. This is the property that keeps the transcript defect from
recurring per pair.
- Widening what counts as blocked remains always-safe and may be done per
harness. Widening what counts as idle requires evidence from a real screen —
a rule this decision does not relax.
- The requirements this pins are `DING-R04` and `DING-R06` in
[`../01-ding/requirements.md`](../01-ding/requirements.md).
111 changes: 111 additions & 0 deletions docs/vrs/01-ding/01-claude/spec.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
# Claude harness specification

The screen grammar by which DING recognizes a Claude composer. It realizes
[`../requirements.md`](../requirements.md) through the mechanism in
[`../spec.md`](../spec.md).

## Status

Active.

## Locating the composer

The composer is drawn between two horizontal rules. Both are located by
structure rather than by width: a rule is a line whose trimmed content is at
least forty characters and consists entirely of the box-drawing horizontal
character. The composer occupies the rows between the last two rules on the
ANSI-stripped screen; the footer is everything below the lower rule.

The prompt is the `❯` character followed by a no-break space. A narrow space is
load-bearing here: the no-break space is Unicode whitespace, so trimming a
composer row before removing the prompt erases the prompt on an *empty*
composer and makes it unlocatable. The prompt is therefore removed before any
trimming.

Locating the composer is what identifies the harness. Startup output, including
the version banner, is not used: an inspection sees the current viewport, so
anything printed once at session start is absent from every screen after the
first (`DING-R05`). The banner is in fact weaker than that argument assumes — at
common pane widths it is not rendered at all, so it is absent from the very
first screen too.

Failing to locate a composer means this harness proves nothing about the screen;
it does not by itself make the screen `Ambiguous`. Under positional dispatch the
screen is offered to every maintained harness, so a pane holding another
harness's live composer is classified by that harness (`DING-R04`). `Ambiguous`
is the result when *no* harness locates a composer.

## Proving idle

The footer carries the permission-mode indicator that ships with the composer
chrome. Idle requires both the mode marker and the permission state to be
present.

The keybinding hint that may appear beside them is **not** an idle signal. It is
composed at runtime from a keybinding lookup, so its text changes when the
binding is remapped and it is absent from many screens that are equally idle.
It may corroborate an idle footer; it may not decide one.

## Proving empty

Two shapes count as positively empty:

- an empty composer, and
- a composer holding only the rotating example placeholder, matched as the exact
`Try "<single-line example>"` grammar with a bounded, control-free example.

The empty composer is the stronger of the two. The placeholder is not styled
differently from typed input, so recognizing it relies on a text grammar a human
could in principle type; an empty composer cannot be confused with a human
draft, because a draft is not empty.

## Blocked states

Return is withheld while the screen shows an active turn or a modal. Two
distinct shapes prove an active turn:

- an explicit interrupt hint, and
- the animated progress line, which carries a rotating verb followed by an
ellipsis, and which **carries no interrupt hint at all**.

The second shape is required. A pane mid-turn has an empty composer and
unchanged footer chrome, so without it a working agent's screen satisfies both
the idle and empty proofs and would receive a Return mid-turn. On the current
build the first shape is not observed at all: no interrupt hint accompanies the
progress line at any width, so the second shape is the only one that fires. The
first is retained because it is cheap and fails closed.

The predicate is derived from real captured screens, and two properties of those
screens constrain it more tightly than it first appears.

**The leading glyph is not a stable key.** It animates through several
box-drawing and punctuation characters within a single turn. Matching any one of
them fails open for most of the turn.

**The elapsed timer is not always present.** Some active frames render the verb
and ellipsis alone, with no parenthesized timer. Requiring a timer would fail
open on exactly those frames.

**A completed turn renders an almost identical line**, distinguished only by
using a past-tense verb with an elapsed duration in place of the ellipsis. This
is the trap: that completed line sits above *every* idle composer, immediately
after every turn. A predicate keyed on the glyph, or on any shape that both
lines share, would therefore treat every idle pane as blocked and stop delivery
permanently, rather than erring conservatively as a widened blocked-check
normally does. The distinguishing signal is the ellipsis directly following a
single verb; nothing coarser is safe in the delivery-stopping direction.

Modal prompts specific to this harness — plan prompts, retry and capacity
notices, queued-message notices — are also blocking and are owned here, not by
shared code (`DING-R06`).

## Known limits

- The permission-state literal proves one permission mode. A pane in another
mode does not reach a positively idle state and defers indefinitely rather
than delivering. Widening this is a behavior change to what counts as idle,
which per [`../spec.md`](../spec.md) requires evidence from a real screen, not
a looser match.
- Recognition is tied to this harness's current rendering. A renderer change
defers delivery until the grammar is updated; it does not produce a wrong
delivery, because every unrecognized shape is `Ambiguous`.
Loading
Loading