fix(ding): require positive harness receipts

INVARIANTS.md

@@ -10,7 +10,7 @@ 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/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` |
+| **Fail-closed observed native DING** | Each unread message becomes one normalized `[DING]` frame. Fresh delivery records ownership, then preserves the one combined bracketed-paste, 0.5 second delay, and Return transaction. PTY and Return success are transport only: `Delivered` additionally requires adapter classification of the expected notice text in a submitted-prompt or queued-message pattern while the lowest live composer is empty or an accepted idle placeholder. Every other receipt retains staged ownership. Retry never re-pastes and may send one bare Return only after two adjacent `RetainedSafe` observations; human, modal, active, changed, timed-out, and unknown retry states receive no input. Ownership prevents duplicate paste across command failures, receipt ambiguity, 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_delivery_uses_face607_delay_order_and_seconds`; `src/ding/mod.rs::maintained_composer_classifiers_require_exact_idle_state`; `src/ding/mod.rs::successful_transport_with_retained_or_unproven_pixels_is_not_delivered`; `src/ding/mod.rs::ambiguous_transport_receipt_and_retry_errors_retain_staged_ownership`; `src/ding/mod.rs::adapter_recognized_notice_with_an_empty_live_composer_is_a_positive_receipt`; `src/ding/mod.rs::staged_retry_submits_only_retained_safe_and_requires_a_receipt`; `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` |

docs/vrs/01-ding/01-claude/spec.md

@@ -59,6 +59,15 @@ 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.
 
+## Post-submit receipt
+
+The exact notice as the complete lowest live composer is `RetainedSafe` only
+with the ordinary idle proof and no blocking state; otherwise it is
+`RetainedBlocked`. `Accepted` requires both an empty or recognized placeholder
+in the lowest live composer and the expected notice text in the adapter's
+submitted-prompt or queued-message pattern. A placeholder alone, disappearance,
+a different live draft, and unrecognized pixels are `Unproven`.
+
 ## Blocked states
 
 Return is withheld while the screen shows an active turn or a modal. Two

docs/vrs/01-ding/02-codex/spec.md

@@ -45,6 +45,15 @@ markers rather than by inspecting recovered text.
 Comparison against the expected notice uses the shared soft-wrap candidate
 enumeration in [`../spec.md`](../spec.md).
 
+## Post-submit receipt
+
+The exact notice as the complete lowest live composer is `RetainedSafe` only
+with the ordinary idle proof and no blocking state; otherwise it is
+`RetainedBlocked`. `Accepted` requires both an empty lowest live composer and
+the expected notice text in the adapter's submitted-prompt or queued-message
+pattern. An empty composer alone, disappearance, a different live draft, and
+unrecognized pixels are `Unproven`.
+
 ## Blocked states
 
 Active-turn and modal detection is owned here rather than shared

docs/vrs/01-ding/requirements.md

@@ -41,21 +41,22 @@ is in [`spec.md`](./spec.md).
 
 ## Requirements
 
-### Must never disturb a human
-
-- **DING-R01 Positive idle precondition:** Text is pasted only after a
-  maintained harness's composer has been positively identified as present,
-  empty, and idle. Absence of evidence that a human is typing is not evidence
-  of an idle composer.
-- **DING-R02 Two adjacent exact observations:** Return is pressed only after the
-  exact staged notice has been observed as the complete composer contents twice
-  in immediately adjacent inspections, with the final observation adjacent to
-  the Return itself. Any change, block, or uncertainty between them prevents
-  submission.
-- **DING-R03 Fail-closed default:** A changed composer, a human draft, an
-  active turn, a modal, an unreadable screen, an unrecognized harness, and a
-  bounded observation timeout all withhold Return. The default for anything not
-  positively understood is deferral.
+### 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
+  understood retains staged ownership.
 
 ### Must classify the surface it will actually type into
 
@@ -86,6 +87,13 @@ is in [`spec.md`](./spec.md).
   terminal probe.
 - **DING-R09 Presence gate:** Declared `busy` is observable but never suppresses
   delivery; only fresh `dnd` defers it. Delivery may wake a working agent.
+- **DING-R10 Positive harness receipt:** `Delivered` requires adapter-provided
+  classification that the expected notice text is visible in that harness's
+  submitted-prompt or queued-message pattern while its lowest live composer is
+  empty or an accepted idle placeholder. PTY command success, generic screen
+  change, disappearance alone, and ambiguous pixels are not receipts. Until
+  that evidence exists, a transport attempt retains staged ownership and
+  retries by inspection without re-pasting.
 
 ## Evidence
 

docs/vrs/01-ding/spec.md

@@ -29,24 +29,49 @@ notice, yields exactly one state:
 ## Delivery
 
 ```text
-peek ─► classify ─┬─ ExactSafe ────► final observation ─► Return ─► Delivered
-                  ├─ ExactBlocked ─────────────────────────────────► Staged
-                  ├─ Changed / Ambiguous ──────────────────────────► Deferred
-                  └─ EmptySafe ─► paste ─► observe until deadline ─┬► Delivered
-                                                                   ├► Staged
-                                                                   └► Deferred
+record ownership ─► combined transport (paste ─► 0.5s ─► Return) ─► receipt
+                         │ command failure or ambiguity                 │
+                         └──────────────────────────────────────────────► Staged
+
+receipt ─┬─ Accepted ──────────────────────────────────────────────► Delivered
+         └─ RetainedSafe / RetainedBlocked / Unproven ────────────► Staged
+
+staged retry ─► receipt ─┬─ Accepted ──────────────────────────────► Delivered
+                         ├─ RetainedSafe ─► final receipt ─┬─ Accepted ─► Delivered
+                         │                                 ├─ RetainedSafe ─► Return ─► receipt
+                         │                                 └─ other ────────► Staged
+                         └─ RetainedBlocked / Unproven ─────────────► Staged
 ```
 
-Delivery is two-phase: a bracketed paste that carries no Return, then a separate
-bare Return gated on a second exact observation (`DING-R02`). The observation
-loop after paste runs to a bounded deadline; expiry yields `Staged`, never a
-Return.
+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.
 
-Every failure of a terminal command after paste has begun resolves to `Staged`
-rather than `Deferred` (`DING-R07`): the paste may already have reached the
-harness, so ownership is retained and retry re-inspects instead of re-pasting. A
-retry of a staged payload is inspect-only — it may submit or defer, but it never
-pastes.
+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
+the harness, so ownership is retained and retry re-inspects instead of
+re-pasting. A staged retry is inspect-only unless two adjacent `RetainedSafe`
+observations authorize one bare Return (`DING-R02`).
+
+Return is transport, not a delivery receipt. After any submission attempt, a
+bounded observation loop asks the selected harness adapter for one of four
+states:
+
+| Receipt state | Meaning |
+| --- | --- |
+| `Accepted` | The expected notice text is visible in an adapter-recognized submitted-prompt or queued-message pattern while the lowest live composer is empty or an accepted idle placeholder |
+| `RetainedSafe` | The exact notice remains the complete live composer and Return is currently safe |
+| `RetainedBlocked` | The exact notice remains the complete live composer but the harness is active or blocked |
+| `Unproven` | No positive acceptance or exact retained-composer state was proven |
+
+Only `Accepted` becomes `Delivered` (`DING-R10`). PTY command success, generic
+screen change, disappearance alone, a changed composer, unreadable output, and
+observation timeout retain `Staged` ownership. A staged retry completes without
+input when it observes `Accepted`; it may send one bare Return only after two
+adjacent `RetainedSafe` observations, then must obtain the same positive
+receipt. `RetainedBlocked` and `Unproven` send no input. No retry re-pastes.
 
 ## Harness dispatch
 
@@ -66,6 +91,11 @@ pasted into a pane — without a per-pair special case. When exactly one harness
 locates a composer, that one is classified; when none do, the screen is
 `Ambiguous`.
 
+Post-submit receipt classification uses that same positional dispatch and a
+shared `ReceiptState` type. Each adapter owns the renderer-specific proof that
+the exact notice is retained or accepted; shared delivery code never matches
+Codex or Claude pixels directly (`DING-R06`, `DING-R10`).
+
 Positions are compared in one unit. Harnesses do not agree on what they match
 against: some locate against the raw screen including escape sequences, others
 against ANSI-stripped lines. A raw byte offset and a stripped line index are not

src/ding/composer.rs

@@ -1,7 +1,7 @@
 //! What a peeked screen proves about one exact notice, and the routing that decides which
 //! composer on the screen is the live one.
 
-use super::harness::{self, Screen};
+use super::harness::{self, ReceiptState, Screen};
 
 /// What the current bottom composer proves about one exact normalized notice.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
@@ -22,7 +22,10 @@ pub(super) enum ComposerState {
 /// discarded one inter-word space or split a token. Current 80-column Codex/Claude composers wrap
 /// long DING rows at 70+ content cells and indent continuations by exactly two cells. Short or
 /// unfamiliar multiline input remains literal and cannot equal a normalized single-line DING.
-pub(super) fn logical_soft_wrap_candidates(input: &str, minimum_first_content_chars: usize) -> Vec<String> {
+pub(super) fn logical_soft_wrap_candidates(
+    input: &str,
+    minimum_first_content_chars: usize,
+) -> Vec<String> {
     let rows: Vec<&str> = input.lines().collect();
     let Some(first) = rows.first() else {
         return vec![String::new()];
@@ -144,12 +147,39 @@ pub(super) fn strip_ansi(input: &str) -> String {
 /// construction, so picking the lowest needs no per-pair special case.
 pub(super) fn classify_composer(screen: &str, expected: &str) -> ComposerState {
     let plain = strip_ansi(screen);
-    let screen = Screen { raw: screen, plain: &plain };
+    let screen = Screen {
+        raw: screen,
+        plain: &plain,
+    };
     harness::all()
         .into_iter()
-        .filter_map(|harness| harness.locate(&screen).map(|located| (located.row, harness)))
+        .filter_map(|harness| {
+            harness
+                .locate(&screen)
+                .map(|located| (located.row, harness))
+        })
         .max_by_key(|(row, _)| *row)
         .map(|(_, harness)| harness.classify(&screen, expected))
         // No maintained composer is locatable, so nothing is proven either way.
         .unwrap_or(ComposerState::Ambiguous)
 }
+
+/// Route post-submit receipt classification through the lowest maintained live composer, using
+/// the same positional rule as pre-submit classification.
+pub(super) fn classify_receipt(screen: &str, expected: &str) -> ReceiptState {
+    let plain = strip_ansi(screen);
+    let screen = Screen {
+        raw: screen,
+        plain: &plain,
+    };
+    harness::all()
+        .into_iter()
+        .filter_map(|harness| {
+            harness
+                .locate(&screen)
+                .map(|located| (located.row, harness))
+        })
+        .max_by_key(|(row, _)| *row)
+        .map(|(_, harness)| harness.receipt(&screen, expected))
+        .unwrap_or(ReceiptState::Unproven)
+}

src/ding/harness/claude.rs

@@ -1,7 +1,7 @@
 //! The Claude Code composer: a `❯` row between two full-width rules, with the permission-mode
 //! footer below it.
 
-use super::{Harness, Located, Screen};
+use super::{Harness, Located, ReceiptState, Screen, screen_has_accepted_notice};
 use crate::ding::composer::{ComposerState, logical_soft_wrap_candidates, looks_like_choice_menu};
 
 pub(super) struct Claude;
@@ -17,6 +17,26 @@ impl Harness for Claude {
         };
         classify_claude_composer(screen.plain, (logical_inputs, footer), expected)
     }
+
+    fn receipt(&self, screen: &Screen<'_>, expected: &str) -> ReceiptState {
+        let Some((_, logical_inputs, footer)) = located_bottom_claude_composer(screen.plain) else {
+            return ReceiptState::Unproven;
+        };
+        let exact = logical_inputs.iter().any(|input| input == expected);
+        let placeholder = logical_inputs.len() == 1
+            && (logical_inputs[0].is_empty() || is_claude_idle_placeholder(&logical_inputs[0]));
+        let idle_footer = footer.contains("⏵⏵") && footer.contains("permissions on");
+        let blocked = interaction_blocked(screen.plain);
+        if exact && idle_footer && !blocked {
+            ReceiptState::RetainedSafe
+        } else if exact {
+            ReceiptState::RetainedBlocked
+        } else if placeholder && screen_has_accepted_notice(screen, '❯', expected) {
+            ReceiptState::Accepted
+        } else {
+            ReceiptState::Unproven
+        }
+    }
 }
 
 fn classify_claude_composer(