diff --git a/docs/vrs/01-ding/requirements.md b/docs/vrs/01-ding/requirements.md index 130f72fa..3fe9a55d 100644 --- a/docs/vrs/01-ding/requirements.md +++ b/docs/vrs/01-ding/requirements.md @@ -20,10 +20,10 @@ is in [`spec.md`](./spec.md). ## Assumptions -- **DING-A01 Rendered screens only:** The only available evidence about a - composer's state is a rendered terminal screen. No maintained harness exposes - an evented idle signal, so every precondition below is a measured heuristic - over text. `DQ2` in [`../spec.md`](../spec.md) tracks closing that gap. +`DING-A01 Rendered screens only` is retired. Rendered-screen evidence is a +limit of the legacy `ding` transport. It is not an assumption for a maintained +harness that declares a native `deliver` transport. + - **DING-A02 Cooperative human:** The human sharing a pane is not adversarial. A screen that deliberately imitates another harness's composer is a correctness concern, not a security boundary, consistent with `A02`. @@ -41,21 +41,43 @@ is in [`spec.md`](./spec.md). ## Requirements -### Must preserve initial transport and gate every retry - -- **DING-R01 Combined initial transport:** A fresh notice uses one bounded PTY - transaction containing the bracketed paste, the accepted 0.5 second delay, - and Return. Ownership is recorded before that command starts. Composer - heuristics do not split or suppress this initial transport. -- **DING-R02 Two adjacent retained-safe retry observations:** A later bare - Return is permitted only for a transport-owned payload whose exact notice is - still the complete composer and is classified `RetainedSafe` in two - immediately adjacent inspections. The final observation is adjacent to the - Return itself. Any change, block, or uncertainty prevents retry submission. -- **DING-R03 Fail-closed receipt and retry:** After the initial transport, a - changed composer, a human draft, an active turn, a modal, an unreadable - screen, an unrecognized harness, and a bounded observation timeout never - become `Delivered` and receive no retry input. Anything not positively +### Must select one explicit transport + +- **DING-R11 Declared transport:** An agent selects at most one delivery + transport. `ding` selects the legacy screen transport. `deliver "mcp"` + selects the Claude native transport. `deliver "app-server"` selects the + Codex native transport. A declaration with neither node has no DING delivery. + A declaration with both nodes, multiple `deliver` nodes, or an unsupported + `deliver` value is invalid. +- **DING-R12 No transport inference:** st2 does not infer a native transport + from an agent command or a screen. Native delivery uses the declared adapter. + A binary that supports `deliver` validates its value and its mutual exclusion + with `ding`. +- **DING-R13 Durable native delivery:** The inbox file remains the source of + truth for native delivery. Only the adapter's declared success condition can + complete a delivery attempt. A closed, unavailable, stale, or unknown native + transport leaves the message unread and retryable. Archive precedence and + restart recovery remain unchanged. +- **DING-R14 Missing transport report:** Doctor reports an active agent that + declares neither `ding` nor `deliver`. The omission remains a valid opt-out + and does not block the agent. The report makes a no-delivery state visible. + +### Must preserve legacy transport and gate every legacy retry + +- **DING-R01 Combined initial transport:** A fresh legacy notice uses one + bounded PTY transaction containing the bracketed paste, the accepted 0.5 + second delay, and Return. Ownership is recorded before that command starts. + Composer heuristics do not split or suppress this initial transport. +- **DING-R02 Two adjacent retained-safe retry observations:** A later legacy + bare Return is permitted only for a transport-owned payload whose exact + notice is still the complete composer and is classified `RetainedSafe` in + two immediately adjacent inspections. The final observation is adjacent to + the Return itself. Any change, block, or uncertainty prevents retry + submission. +- **DING-R03 Fail-closed receipt and retry:** After the initial legacy + transport, a changed composer, a human draft, an active turn, a modal, an + unreadable screen, an unrecognized harness, and a bounded observation timeout + never become `Delivered` and receive no retry input. Anything not positively understood retains staged ownership. On an inspect-only staged retry, a maintained adapter may positively prove that the exact owned payload is no longer retained; that proof relinquishes ownership only when an archive diff --git a/docs/vrs/01-ding/spec.md b/docs/vrs/01-ding/spec.md index 3d432022..65b114d1 100644 --- a/docs/vrs/01-ding/spec.md +++ b/docs/vrs/01-ding/spec.md @@ -10,6 +10,42 @@ specified in [`01-claude/spec.md`](./01-claude/spec.md) and Active. A map to the implementation and its evidence, not a replacement for the tests. +## Delivery selection + +Delivery is opt-in. An agent declaration selects one transport: + +| Declaration | Transport | +| --- | --- | +| `ding` | Legacy screen transport | +| `deliver "mcp"` | Claude native MCP transport | +| `deliver "app-server"` | Codex native app-server transport | +| Neither node | No delivery | + +`ding` and `deliver` are mutually exclusive. More than one `deliver` node is +invalid. Any other `deliver` value is invalid. st2 does not infer a transport +from the agent command because command arguments are opaque. + +The native selector is a new `deliver` node. A binary released before this +contract ignores that unknown agent child. It lowers a valid `deliver`-only +agent with no delivery sidecar. The agent receives no DING. It does not silently +use the legacy screen transport. This is a visible delivery outage. + +A binary that supports `deliver` validates its value and its mutual exclusion +with `ding`. Native delivery must not be encoded as an argument to `ding`, +because a pre-change parser would accept that form as legacy `ding` and use the +wrong transport. Doctor reports an active agent that declares no transport. The +report does not make the valid no-delivery opt-out an error. + +The durable inbox is the source of truth for every transport. An archive with +the same message name wins. A native adapter completes delivery only after its +declared provider-specific success condition. If the adapter is closed, +unavailable, stale, or in an unknown state, it sends no unsafe input and leaves +the inbox message unread for retry. Native adapters do not use the +rendered-screen classifier. + +The rest of this document defines the unchanged legacy screen transport. The +native wire contracts are in each maintained harness specification. + ## Composer states One inspection of a rendered screen, evaluated against one exact expected @@ -45,11 +81,11 @@ staged retry ─► receipt ─┬─ Accepted ─────────── └─ RetainedBlocked / Unproven ─────────────► Staged ``` -Fresh delivery preserves the production transport: one bounded PTY transaction -contains a bracketed paste, a 0.5 second delay, and Return (`DING-R01`). -Ownership is recorded immediately before that transaction. The production path -does not inspect the composer first and does not use the separate staging -helper. +Fresh legacy delivery preserves the production transport: one bounded PTY +transaction contains a bracketed paste, a 0.5 second delay, and Return +(`DING-R01`). Ownership is recorded immediately before that transaction. The +production path does not inspect the composer first and does not use the +separate staging helper. Every failure of that terminal command or of the following receipt observation resolves to `Staged` (`DING-R07`): the paste and Return may already have reached @@ -148,10 +184,11 @@ Declared `busy` never suppresses delivery; only fresh `dnd` defers it ## Known limits -- Idle proof depends on footer chrome that a harness may render differently - across permission or approval modes. A harness whose footer is not recognized - in a given mode defers indefinitely rather than delivering. This is an - explicit limit per `T01`, and each harness spec states which modes it proves. -- The classifier is a measured heuristic over rendered text, not an evented - signal, so a renderer change can defer delivery until the grammar is updated. - Tracked as `DQ2` in [`../spec.md`](../spec.md). +- Legacy idle proof depends on footer chrome that a harness may render + differently across permission or approval modes. A harness whose footer is + not recognized in a given mode defers indefinitely rather than delivering. + This is an explicit limit per `T01`, and each harness spec states which modes + it proves. +- The legacy classifier is a measured heuristic over rendered text, not an + evented signal, so a renderer change can defer legacy delivery until the + grammar is updated. Maintained native transports do not use this classifier. diff --git a/docs/vrs/02-agent-spec/spec.md b/docs/vrs/02-agent-spec/spec.md index 5ef2aedb..e7b524d3 100644 --- a/docs/vrs/02-agent-spec/spec.md +++ b/docs/vrs/02-agent-spec/spec.md @@ -358,10 +358,13 @@ Authoring: [pinned complete declaration][evals-fields]. st2 source: