Skip to content
Merged
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
2 changes: 1 addition & 1 deletion INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ materialization, messaging, DING, or presence must preserve them.
| **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` |
| **Derived companion lifecycle** | A generated DING or launched stream starts only with an eligible canonical agent, is suppressed or stopped while that target is held, suspended, unavailable, retired, or terminally parked, and remains coupled without changing explicit sibling task behavior. A stream lowers its authored adapter launch directly, parks and surfaces independently, and neither makes an otherwise empty agent runnable nor claims a delivery transport. Stream authoring is serialized, authority-scoped, source-preserving, and fail-closed for Nix ownership and invalid declarations. Healthy compact startup launches companions in one pass, and targeted reconciliation holds a missing generated companion rather than broadening to its agent. | `crates/agent-spec/tests/discovery.rs::streams_are_typed_and_only_launched_streams_lower_to_derived_exec_tasks`; `crates/agent-spec/tests/discovery.rs::stream_names_launches_and_task_collisions_fail_closed`; `src/agent_author.rs::stream_add_supports_external_command_and_argv_and_external_remove_is_idempotent`; `src/agent_author.rs::stream_authoring_enforces_authority_nix_ownership_and_canonical_validation`; `tests/run.rs::fresh_compact_agent_launches_with_its_derived_ding`; `tests/run.rs::held_adopt_only_compact_agent_stops_its_live_derived_ding`; `tests/run.rs::parked_compact_agent_stops_its_live_derived_ding`; `tests/run.rs::retired_compact_agent_stops_agent_and_derived_ding`; `tests/run.rs::selected_missing_derived_ding_is_held_without_broadening_to_its_agent`; `tests/run.rs::fresh_compact_agent_launches_with_its_derived_stream`; `tests/run.rs::retired_compact_agent_stops_agent_and_derived_stream`; `tests/run.rs::suspended_compact_agent_stops_its_derived_stream_without_touching_a_sibling`; `tests/run.rs::held_adopt_only_compact_agent_stops_its_live_derived_stream`; `tests/run.rs::a_crash_looping_stream_parks_and_surfaces_without_disturbing_its_agent`; `tests/run.rs::parked_compact_agent_stops_its_live_derived_stream`; `tests/run.rs::selected_missing_derived_stream_is_held_without_broadening_to_its_agent`; `tests/run.rs::a_launched_stream_alone_is_rejected_before_reconciliation`; `tests/run.rs::a_stream_does_not_claim_a_delivery_transport` |
| **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` |
| **Durable native delivery ownership** | Each native harness keeps one monotone evidence chain per inbox filename in `delivery-ledger.json`. Ownership is persisted before the transport call, so a crash between attempt and evidence reopens as an ambiguous attempt that holds instead of re-sending. Evidence only advances, and only to a phase the harness can actually observe: Codex proves transport acceptance and consumption, OpenCode transport acceptance and durable read-back, and a record claiming any other phase is refused. Only an authoritative negative receipt re-authorizes a retry. Settlement stays with the recipient: an entry is released only on a phase its profile releases, and is otherwise reconciled away when the message leaves the unread set. A foreign, malformed, or self-inconsistent record quarantines delivery without rewriting it, and the persisted ledger is owner-only with no temp residue. | `src/delivery_ledger.rs::tests::begin_persists_attempted_before_transport`; `src/delivery_ledger.rs::tests::positive_evidence_never_downgrades`; `src/delivery_ledger.rs::tests::profiles_accept_only_evidence_their_harness_can_produce`; `src/delivery_ledger.rs::tests::negative_receipt_is_the_only_retry_authority`; `src/delivery_ledger.rs::tests::opencode_persistence_holds_until_archive`; `src/delivery_ledger.rs::tests::foreign_or_malformed_state_quarantines_without_rewriting`; `src/delivery_ledger.rs::tests::every_entry_must_validate_its_own_correlation`; `src/delivery_ledger.rs::tests::the_persisted_ledger_is_owner_only_and_leaves_no_temp_residue` |
| **Durable native delivery ownership** | Each native harness keeps one monotone evidence chain per inbox filename in `delivery-ledger.json`. Ownership is persisted before the transport call, so a crash between attempt and evidence reopens as an ambiguous attempt that holds instead of re-sending. Evidence only advances, and only to a phase the harness can actually observe: Codex proves transport acceptance and consumption, OpenCode transport acceptance and durable read-back, and a record claiming any other phase is refused. Only an authoritative negative receipt re-authorizes a retry. Settlement stays with the recipient: an entry is released only on a phase its profile releases, and is otherwise reconciled away when the message leaves the unread set. A foreign, malformed, or self-inconsistent record quarantines delivery without rewriting it, and the persisted ledger is owner-only with no temp residue. A delivery attempt an earlier release left behind is carried forward rather than re-sent: the pre-ledger `delivery-state.json` record is translated exactly once, when no ledger file exists, into an asserted phase that holds the delivery and authorizes no transport until this build observes evidence of its own. | `src/delivery_ledger.rs::tests::begin_persists_attempted_before_transport`; `src/delivery_ledger.rs::tests::positive_evidence_never_downgrades`; `src/delivery_ledger.rs::tests::profiles_accept_only_evidence_their_harness_can_produce`; `src/delivery_ledger.rs::tests::negative_receipt_is_the_only_retry_authority`; `src/delivery_ledger.rs::tests::opencode_persistence_holds_until_archive`; `src/delivery_ledger.rs::tests::foreign_or_malformed_state_quarantines_without_rewriting`; `src/delivery_ledger.rs::tests::every_entry_must_validate_its_own_correlation`; `src/delivery_ledger.rs::tests::the_persisted_ledger_is_owner_only_and_leaves_no_temp_residue`; `src/delivery_ledger.rs::tests::an_asserted_phase_suppresses_a_duplicate_and_authorizes_no_transport`; `src/migrations/delivery_state/mod.rs::tests::a_carried_forward_attempt_is_an_assertion_that_authorizes_no_transport`; `src/migrations/delivery_state/mod.rs::tests::translation_happens_once_and_leaves_the_old_record_in_place`; `src/migrations/delivery_state/mod.rs::tests::deletion_trigger_absent_old_record_makes_this_module_a_no_op` |
| **Idempotent service requests** | A declared non-agent service principal publishes one exact JSON request per caller-supplied idempotency key to a canonical Agent Spec inbox. Concurrent or crash-replayed publication reuses the reserved filename; conflicting key reuse fails. The typed reply routes to the principal's canonical inbox without an Agent Spec identity or orphan mailbox. | `tests/request_cli.rs::stable_request_key_atomically_deduplicates_one_canonical_agent_message`; `tests/request_cli.rs::concurrent_replays_publish_exactly_one_request`; `tests/request_cli.rs::typed_reply_routes_to_the_principal_and_status_is_a_tagged_json_union`; `tests/request_cli.rs::request_api_rejects_agent_impersonation_and_unknown_flat_principals` |
| **Bounded idempotent stream ingress** | A running agent accepts events only for a declared stream. Within the retained 128-receipt ring, concurrent or crash-replayed `(stream, event-id)` publication reuses one canonical filename, conflicting content fails, and supersession archives only the matching keyed predecessor or the stream-wide head through ordinary archive semantics. State remains bounded and honestly treats an identity evicted from the ring as new without searching inbox or archive history. Events do not write the Sent ledger and DING marks them as stream work. | `tests/event_e2e.rs::stable_event_identity_publishes_exactly_one_canonical_message`; `tests/event_e2e.rs::concurrent_replays_publish_exactly_one_event`; `tests/event_e2e.rs::conflicting_reuse_and_undeclared_or_suspended_ingress_fail_closed`; `tests/event_e2e.rs::supersede_collapses_only_the_matching_key_and_preserves_archive_receipts`; `tests/event_e2e.rs::keyless_supersede_replaces_the_stream_wide_head`; `tests/event_e2e.rs::crash_replay_honors_an_archive_receipt_and_never_restores_the_inbox_copy`; `tests/event_e2e.rs::subject_frontmatter_injection_is_refused_before_any_write`; `tests/event_e2e.rs::stream_state_is_bounded_and_forgets_only_beyond_its_honest_horizon`; `tests/event_e2e.rs::event_emit_cli_returns_a_stable_json_receipt_and_ding_marks_the_record`; `tests/stream_authoring_cli.rs::a_direct_adapter_launch_executes_the_exact_event_cli_contract`; `tests/run.rs::suspend_and_resume_relaunch_the_agent_and_stream_together` |
| **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` |
Expand Down
85 changes: 85 additions & 0 deletions docs/vrs/.delta/DELTA-006-delivery-state-v1-arm.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
# DELTA-006: the pre-ledger `delivery-state.json` boundary arm outlives its own necessity

Status: open

## Divergence

The canonical delivery ledger owns exactly one schema, `st2.delivery-ledger.v1`,
and `src/delivery_ledger.rs` is written as though only that format had ever
shipped. It nevertheless carries one statement that knows otherwise: the
`ErrorKind::NotFound` arm of `Ledger::open` calls
`crate::migrations::delivery_state::recover`, which reads the single-binding
`delivery-state.json` record every pre-ledger release wrote and carries an
in-flight attempt forward as an assertion instead of letting it be re-sent.

That arm is correct today and is dead weight the moment no such record exists
anywhere. Nothing in the code can observe that condition, so the divergence is
between an implementation that must still translate a retired format and a
design that owns one format — and it closes by deletion, on a fleet
observation, not by an amendment.

## VRS

No ratified requirement mentions either record. The rule the arm exists to
preserve is [`DING-R07`](../01-ding/requirements.md) staged ownership: once an
attempt has started, ambiguity about whether it landed is resolved by
inspection, never by pasting the same notice again. A release boundary is
exactly such an ambiguity — the old binary's record is the only evidence that
an attempt was made — so dropping that record on upgrade would resolve the
ambiguity by re-sending, which DING-R07 forbids and DING-T01 answers the other
way: every ambiguous case resolves toward deferral.

Requirements therefore need no change. What needs recording is that a piece of
the implementation is deliberately temporary, with the observation that ends
it.

## Implementation

`src/migrations/delivery_state/` owns the whole boundary: `mod.rs` (the entry
point, the ownership filter, the legacy filename), `codex_v1.rs`, and
`opencode_v1.rs` (one retired wire struct each, plus the meaning of its
labels — Codex's `accepted` was a typed in-turn receipt and grades to
`consumed`, OpenCode's was a storage read-back and grades to `persisted`).

Canonical code gains one version-free concept, `Attestation{Observed,
Asserted}` on `Entry`: a phase this build graded versus a phase another
authority asserted. An assertion bounds what already happened, so it suppresses
a duplicate; it is not an observation, so it authorizes no transport until this
build sees something itself. That distinction is permanent and would be needed
by any future asserting authority, so it stays when the arm goes.

Deletion is `git rm -r src/migrations` plus replacing the seam arm with
`Ok(())`, which is byte-for-byte a first run on a fresh seat. Measured cost of
that deletion: one compile error, at the seam.

## Direction

update implementation

## Resolution Signal

Both commands below print nothing, on every admitted host, for seven
consecutive days:

```sh
state="${XDG_STATE_HOME:-$HOME/.local/state}/st2"

# 1. No pre-ledger record is left beside any per-harness state dir, so no
# unread attempt can still need carrying forward.
find "$state/codex" "$state/opencode" -maxdepth 2 -name delivery-state.json -print

# 2. No ledger entry still holds a phase this fleet never observed. While one
# exists, the translation that produced it is load-bearing.
find "$state/codex" "$state/opencode" -maxdepth 2 -name delivery-ledger.json -print0 \
| xargs -0 -r jq -r 'select([.entries[].attestation] | any(. == "asserted")) | input_filename'
```

Clause 1 also requires that rollback to a pre-ledger release has stopped being
supported: while it is supported, a rolled-back binary can write a new
`delivery-state.json`, and the roll-forward window it opens is pinned by
`migrations::delivery_state::tests::a_rollback_then_roll_forward_does_not_see_the_record_written_in_between`.

The local half of the trigger — that with no old record present the module
contributes nothing and writes nothing, so removing it cannot change observed
behaviour — is asserted by
`migrations::delivery_state::tests::deletion_trigger_absent_old_record_makes_this_module_a_no_op`.
Loading
Loading