fix(ding): release vanished archived FIFO ownership

INVARIANTS.md

@@ -11,7 +11,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. 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` |
+| **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. Retry never re-pastes and may send one bare Return only after two adjacent `RetainedSafe` observations. A maintained adapter's positive `NotRetained` observation releases only an already archived staged head; unread, blocked, timed-out, errored, unknown, and unrecognized states retain ownership and later FIFO work remains blocked. Ownership prevents duplicate paste across command failures, receipt ambiguity, archive races, and restart adoption without letting a vanished archived head block FIFO indefinitely. 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_retry_keeps_unproven_and_retained_blocked_owned`; `src/ding/mod.rs::staged_ownership_survives_archive_and_never_repastes`; `src/ding/mod.rs::archived_not_retained_releases_fifo_without_repasting_owned_notice`; `src/ding/mod.rs::unread_not_retained_keeps_fifo_ownership_without_repasting`; `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/native_only.rs::clean_path_executes_the_maintained_native_authoring_guide`; `src/ding/mod.rs::pending_delivery_ignores_busy_but_respects_fresh_dnd_archive_and_retry` |

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

@@ -65,8 +65,9 @@ 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`.
+submitted-prompt or queued-message pattern. A parsed placeholder, empty
+composer, or different live draft that is not accepted is `NotRetained`.
+Disappearance and unrecognized pixels are `Unproven`.
 
 ## Blocked states
 

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

@@ -51,8 +51,8 @@ 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`.
+pattern. A parsed empty composer or different live draft that is not accepted
+is `NotRetained`. Disappearance and unrecognized pixels are `Unproven`.
 
 ## Blocked states
 

docs/vrs/01-ding/requirements.md

@@ -56,7 +56,11 @@ is in [`spec.md`](./spec.md).
   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.
+  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
+  receipt already removed the notice from the inbox. An unread notice remains
+  staged even after positive absence, so it is never pasted again.
 
 ### Must classify the surface it will actually type into
 
@@ -91,9 +95,11 @@ is in [`spec.md`](./spec.md).
   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.
+  change, disappearance alone, and ambiguous pixels are not receipts. A
+  maintained adapter that successfully parses the live composer may separately
+  prove `NotRetained`; this is never delivery and releases only an already
+  archived staged head. Unread, unreadable, unrecognized, and ambiguous attempts
+  retain staged ownership and retry by inspection without re-pasting.
 
 ## Evidence
 

docs/vrs/01-ding/spec.md

@@ -34,12 +34,14 @@ record ownership ─► combined transport (paste ─► 0.5s ─► Return) ─
                          └──────────────────────────────────────────────► Staged
 
 receipt ─┬─ Accepted ──────────────────────────────────────────────► Delivered
-         └─ RetainedSafe / RetainedBlocked / Unproven ────────────► Staged
+         └─ RetainedSafe / RetainedBlocked / NotRetained / Unproven ► Staged
 
 staged retry ─► receipt ─┬─ Accepted ──────────────────────────────► Delivered
                          ├─ RetainedSafe ─► final receipt ─┬─ Accepted ─► Delivered
                          │                                 ├─ RetainedSafe ─► Return ─► receipt
                          │                                 └─ other ────────► Staged
+                         ├─ NotRetained + archived ────────────────► release head
+                         ├─ NotRetained + unread ──────────────────► Staged
                          └─ RetainedBlocked / Unproven ─────────────► Staged
 ```
 
@@ -56,22 +58,27 @@ 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
+bounded observation loop asks the selected harness adapter for one of five
 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 |
+| `NotRetained` | A maintained adapter parsed the live composer and positively proved that the exact notice is neither its complete contents nor an accepted submission |
 | `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.
+observation timeout never become delivery. `NotRetained` requires successful
+parsing by a maintained adapter; missing or unrecognized composer evidence stays
+`Unproven`. 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. `NotRetained` releases ownership
+only when the notice is already archived; an unread notice remains staged.
+`RetainedBlocked`, `NotRetained`, and `Unproven` send no input. No retry
+re-pastes.
 
 ## Harness dispatch
 
@@ -126,13 +133,16 @@ the original text either lost one inter-word space or split a token, so each
 boundary yields exactly two candidates. Comparison against the expected notice
 succeeds if any candidate matches exactly. The bounded notice length keeps the
 candidate set small; an unfamiliar multiline shape yields no match and fails
-closed.
+closed: it is `Ambiguous` before submission and `Unproven` after transport,
+never positive `NotRetained` evidence.
 
 ## Retry and suppression
 
 Deferred notices retain FIFO order and retry on a bounded backoff, so an
 indefinitely occupied composer cannot spawn a terminal probe per inbox poll
-(`DING-R08`). Archive receipts remove pending notices without another attempt.
+(`DING-R08`). A staged archived head advances FIFO only after a maintained
+adapter positively observes `NotRetained`; an unread head does not release.
+Archive receipts remove pending notices that do not already own a transport.
 Declared `busy` never suppresses delivery; only fresh `dnd` defers it
 (`DING-R09`).
 

src/ding/composer.rs

@@ -18,20 +18,35 @@ pub(super) enum ComposerState {
     Ambiguous,
 }
 
+/// Logical inputs reconstructed from renderer-proven boundaries, or an unsupported shape.
+pub(super) enum SoftWrapCandidates {
+    Proven(Vec<String>),
+    Unsupported,
+}
+
+impl SoftWrapCandidates {
+    pub(super) fn proven(&self) -> Option<&[String]> {
+        match self {
+            Self::Proven(candidates) => Some(candidates),
+            Self::Unsupported => None,
+        }
+    }
+}
+
 /// Enumerate the two logical strings possible at each renderer-shaped soft-wrap row: the TUI either
 /// 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.
+/// unfamiliar multiline input is unsupported rather than positive mismatch evidence.
 pub(super) fn logical_soft_wrap_candidates(
     input: &str,
     minimum_first_content_chars: usize,
-) -> Vec<String> {
+) -> SoftWrapCandidates {
     let rows: Vec<&str> = input.lines().collect();
     let Some(first) = rows.first() else {
-        return vec![String::new()];
+        return SoftWrapCandidates::Proven(vec![String::new()]);
     };
     if rows.len() == 1 {
-        return vec![(*first).to_string()];
+        return SoftWrapCandidates::Proven(vec![(*first).to_string()]);
     }
     let mut candidates = vec![(*first).to_string()];
     let mut previous = *first;
@@ -41,21 +56,21 @@ pub(super) fn logical_soft_wrap_candidates(
             || !row.starts_with("  ")
             || row.trim().is_empty()
         {
-            return vec![input.to_string()];
+            return SoftWrapCandidates::Unsupported;
         }
         let continuation = row.strip_prefix("  ").expect("prefix checked").trim_end();
         let mut next = Vec::with_capacity(candidates.len().saturating_mul(2).min(32));
         for candidate in candidates {
             if next.len() >= 32 {
-                return vec![input.to_string()];
+                return SoftWrapCandidates::Unsupported;
             }
             next.push(format!("{candidate}{continuation}"));
             next.push(format!("{candidate} {continuation}"));
         }
         candidates = next;
         previous = row;
     }
-    candidates
+    SoftWrapCandidates::Proven(candidates)
 }
 
 pub(super) fn looks_like_choice_menu(plain: &str) -> bool {

src/ding/harness/claude.rs

@@ -2,7 +2,9 @@
 //! footer below it.
 
 use super::{Harness, Located, ReceiptState, Screen, screen_has_accepted_notice};
-use crate::ding::composer::{ComposerState, logical_soft_wrap_candidates, looks_like_choice_menu};
+use crate::ding::composer::{
+    ComposerState, SoftWrapCandidates, logical_soft_wrap_candidates, looks_like_choice_menu,
+};
 
 pub(super) struct Claude;
 
@@ -22,6 +24,9 @@ impl Harness for Claude {
         let Some((_, logical_inputs, footer)) = located_bottom_claude_composer(screen.plain) else {
             return ReceiptState::Unproven;
         };
+        let Some(logical_inputs) = logical_inputs.proven() 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]));
@@ -34,16 +39,19 @@ impl Harness for Claude {
         } else if placeholder && screen_has_accepted_notice(screen, '❯', expected) {
             ReceiptState::Accepted
         } else {
-            ReceiptState::Unproven
+            ReceiptState::NotRetained
         }
     }
 }
 
 fn classify_claude_composer(
     plain: &str,
-    (logical_inputs, footer): (Vec<String>, String),
+    (logical_inputs, footer): (SoftWrapCandidates, String),
     expected: &str,
 ) -> ComposerState {
+    let Some(logical_inputs) = logical_inputs.proven() else {
+        return ComposerState::Ambiguous;
+    };
     let exact = logical_inputs.iter().any(|input| input == expected);
     // An empty composer is a stronger positive-empty proof than the placeholder below, because no
     // human draft can be empty. Claude only shows the rotating placeholder on an unused pane.
@@ -85,7 +93,7 @@ fn is_claude_idle_placeholder(input: &str) -> bool {
 /// row Claude may either wrap at a discarded space or split a token, so each proven boundary has
 /// exactly two candidates: join with one space or with none. The bounded DING length keeps this set
 /// small; any unfamiliar multiline shape fails closed.
-fn located_bottom_claude_composer(plain: &str) -> Option<(usize, Vec<String>, String)> {
+fn located_bottom_claude_composer(plain: &str) -> Option<(usize, SoftWrapCandidates, String)> {
     let lines: Vec<&str> = plain.lines().collect();
     let separators: Vec<usize> = lines
         .iter()