Make native delivery claims transactional across all harnesses

[schickling-assistant]

Status

Execution scope and VRS requirements are approved. P1 is ready as #514. P2 is in progress; P3–P4 remain gated behind P2.

This issue owns one four-PR st2 cycle through ready. It does not authorize merge, deployment, dotfiles changes, issue #507, normalized conversations, harness-state/disposition work, or unrelated cleanup.

st2 does not define check:quick or check:all devenv tasks. Each PR uses the repository-owned Nix check derivation as the full local gate.

Motivation

INVARIANTS.md says every native harness keeps durable delivery ownership. Current main does this only for Codex and OpenCode. Claude, pi, and OMP suppress filenames in process-local sets, so a channel restart can transport the same unread message again.

The existing ledger also caches a record and exposes read-modify-write operations separately. Two overlapping writers can both authorize transport. A stale record, negative, rebind, or prune writer can later overwrite a newer claim or evidence. Native channel overlap is reachable during replacement and direct driver invocation, so one transactional boundary must own every mutation.

Settled contract

For every native harness:

1. Persist Attempted before returning one transport permit.
2. Serialize recovery and every ledger mutation under one stable sidecar lock. Re-read and validate current bytes after acquiring the lock.
3. Compare the exact attempt token for later evidence, negative evidence, rebind, and pruning.
4. If a crash makes the outcome ambiguous, hold the message. Time, process liveness, successful local writes, and adapter result names are not evidence.
5. Re-authorize transport only after exact negative evidence for that attempt.
6. Treat recipient/archive evidence as settlement.
7. Own one FIFO head per binding. A later inbox message must not overtake an outstanding head.

This intentionally prefers duplicate prevention over automatic retry when a provider supplies no authoritative receipt.

Identity and evidence policy

Keep provider identity separate from evidence policy. Five stable harness discriminators continue to own persisted wire identity, foreign-ledger rejection, and migration selection. Three closed policies grade evidence:

Evidence policy	Harnesses	Evidence above Attempted
attempt-only	Claude, pi, OMP	None. Local write/flush and extension return are ambiguous.
Codex receipts	Codex	Correlated transport acceptance, consumption, exact request rejection, and exact resumed-history absence.
OpenCode receipts	OpenCode	Correlated transport acceptance, durable read-back, and exact 404 absence.

Pi 0.84.2 and the inspected OMP 18.0.9/18.1.2 releases expose ExtensionAPI.sendUserMessage(...): void. Their current assets emit delivered before the provider's hidden Promise settles. The broad catch can emit failed after a side effect already occurred. Neither frame is a receipt or exact negative.

Claude channel notifications are unacknowledged MCP notifications. A successful flush proves only a local transport write.

Exact operator negative evidence

Attempt-only providers cannot emit a machine negative receipt. To avoid permanent FIFO starvation after a pre-transport crash, an operator may record exact absence after inspecting provider history.

Each attempt-only injected message carries a minimal provider-visible correlation marker containing only the canonical message filename and exact attempt token. The marker is correlation, not a delivery or consumption claim. It contains no host path or identity.

The evidence operation:

• uses the existing same-UID filesystem authority; it is operator evidence, not authenticated-human evidence;
• records OS uid, optional non-authoritative process/ST_AGENT provenance, required reason, binding, filename, correlation, attempt token, ledger precondition, and timestamp;
• refuses stale binding, filename, correlation, attempt, changed ledger bytes, settled state, and malformed/quarantined state;
• persists the negative observation before returning; and
• never performs transport. A later pump must acquire a new transactional claim.

Reproduction evidence

A bounded two-message/two-writer model, exhaustively explored through depth 8, found current restart re-send, split retry/begin double permit, and retry after ambiguous failure. It found zero violations with an atomic claim in the modeled surface.

A source-grounded reviewer then found the broader stale-writer case: transactionality must cover recovery and every mutator, not only retry plus begin. It also found that current pi/OMP/Claude frame metadata does not reach provider history, which requires the correlation marker before operator absence can be exact.

A separate experiment imported the actual pi and OMP TypeScript assets and drove them through a barrier-controlled fake child/provider. Both emitted delivered before hidden completion and both emitted failed after a recorded side effect.

These are deterministic in-repository seams. An external reproduction repository would not isolate another project's defect.

Four-PR execution staircase

The semantic graph is P1 → P2 → {P3, P4}. The review graph stays linear so the final PR can ratify the all-five invariant without an integration branch. Finish each PR's gates before starting the next.

P1 — evidence-policy seam

• Retain five stable harness/wire discriminators.
• Introduce three closed evidence policies and driver-owned translation.
• Preserve complete Codex/OpenCode compact JSON bytes, retry decisions, retention decisions, correlation, rebind, migration, and archive behavior.
• Prove the seam with a synthetic policy without adding another ledger provider branch.
• Narrow the currently false all-native-harness invariant to exactly the proved providers.

P2 — transactional ledger and recovery

• Put initial recovery and every mutator behind one stable sidecar-lock transaction.
• Replace split authorization/begin with one exact attempt-token claim.
• Apply Q35's bounded tokenless-v1 Codex/OpenCode backfill under the same transaction lock.
• Add operator-negative evidence and the provider-visible correlation-marker contract.
• Prove two-writer and stale-writer exclusion across claim, evidence, negative, rebind, and prune.
• Prove crash points, FIFO, archive settlement, exact-negative retry, and malformed/quarantined fail-closed behavior.

P3 — pi and OMP adoption

• Use stable non-session bindings and the production assets.
• Inject the exact correlation marker and claim durably before transport.
• Treat extension return and current outcome frames as ambiguous.
• Delete the shared process-local suppression state and misleading delivered/failed frames.
• Add named pi/OMP invariant evidence.

P4 — Claude adoption

• Use the packaged plugin and the same correlation contract.
• Claim durably before the unacknowledged MCP notification.
• Delete the final process-local suppression state.
• Restore the all-five invariant only after named Claude evidence passes.

Readiness gates

Every PR remains draft until all applicable gates pass:

• focused unit, property/model, crash, concurrency, and integration tests;
• the production asset/plugin against a controlled peer;
• relevant disposable real-provider positive-delivery probes;
• devenv tasks run check:quick;
• independent code review and addressed findings.

P1/P2 require fresh Codex and OpenCode compatibility probes. P3 requires real pi and OMP positive-delivery probes. P4 requires a real Claude positive-delivery probe. Real probes prove only that the exact production integration delivered a unique nonce. Deterministic tests prove locking, crash safety, FIFO, restart hold, and duplicate exclusion; silence over a timeout is never negative evidence.

A missing provider executable or unreliable shared build environment leaves the current PR draft. It does not authorize a workaround or side work on #507.

Forward-only adoption

Do not add an attempt-only legacy delivery path, downgrade reader, dual write, translation bridge, or compatibility fence.

P3 and P4 are reversible before their first deployed attempt-only record. After that record exists, pre-adoption binaries are unsupported and recovery rolls forward. This four-PR cycle does not deploy, so it does not cross that boundary. A future activation must make the forward-only point explicit before adoption.

Q35 exposed one contradiction in the approved P2 shape: an exact durable attempt token cannot both preserve tokenless canonical Codex/OpenCode entries and require no reader for them. Johannes selected one bounded exception. Under the new transaction lock, P2 derives and durably backfills a token for a tokenless canonical st2.delivery-ledger.v1 entry before any other mutation or transport. It never dual-writes. The temporary reader remains countable until a deletion signal proves it can be removed. After a token-bearing claim, rollback to a writer that drops the token is unsupported. This exception does not apply to Claude, pi, or OMP.

Acceptance

• Five harness identities remain distinct from the three evidence policies.
• Complete Codex/OpenCode byte and decision equivalence passes.
• A synthetic policy works without a new core provider branch.
• Recovery and every mutator re-read and update under one stable lock.
• Two barrier-synchronized writers cannot both claim one filename or overwrite newer state through another mutator.
• Two filenames cannot bypass one outstanding FIFO head.
• Crash injection covers before claim, after durable Attempted, before transport, after transport, after positive evidence, after exact negative evidence, and after archive settlement.
• No second transport occurs without exact negative evidence for the same attempt.
• Operator absence is provider-visible, exact, audited, compare-and-set, and separate from transport.
• A held ambiguous delivery is visible in the normal operator surface, not only in the ledger.
• Claude/pi/OMP ambiguous outcomes remain held across restart.
• Codex and OpenCode retain their stronger receipt and reconciliation behavior.
• Real-provider positive-delivery probes pass for all five harnesses before the relevant PR is ready.
• Process-local suppression and misleading pi/OMP outcome frames are deleted at adoption.
• INVARIANTS.md states only behavior proved by named tests after every PR.
• No attempt-only backward-compatibility or downgrade path is added; Q35's bounded canonical token backfill is the only compatibility reader.

Relationships

• Define Axe harness drivers and extract all harness-specific behavior from st2 core #162 owns the broader harness-driver boundary. This issue is its first static vertical slice.
• feat(delivery): durable delivery ledger, newest-format only #484 introduced the shared durable ledger.
• feat(delivery): carry pre-ledger delivery attempts forward through a boundary arm #485 and DELTA-006 own the separate temporary Codex/OpenCode pre-ledger migration boundary.
• DELTA-007 owns Q35's bounded tokenless canonical-ledger reader and deletion signal.

Posted on behalf of @schickling

field	value
agent_identity	dev3.direct.omp.9exwnk6h
session	dev3.9exwnk6h
agent_persona	generalist
agent_supervisor	unavailable
agent_tool	OMP
agent_tool_version	18.1.7
agent_runtime	OMP 18.1.7
tooling_profile	dotfiles@931583a

[schickling-assistant]

@myobie — docs/vrs/spec.md requires your explicit approval before changing docs/vrs/requirements.md. Johannes has confirmed the #506 direction after an independent critique. May the implementation add the following minimal requirement delta?

Proposed acceptable tradeoff

• T03 Forward-only attempt-only adoption: After Claude, pi, or OMP writes its first durable attempt-only delivery record, st2 does not support rollback to a release that cannot interpret that record. Recovery rolls forward. st2 does not retain a legacy delivery path, downgrade reader, dual write, translation bridge, or compatibility fence. Preserving the existing Codex/OpenCode ledger format is avoidance of migration, not a compatibility layer.

Proposed requirement

• R41 Transactional native delivery ownership: Every managed native harness owns delivery through one durable per-agent, per-harness ledger and one FIFO head. Five stable harness identities remain distinct from three closed evidence policies. Initial recovery and every ledger mutation serialize under one stable local kernel lock, re-read and validate current bytes after lock acquisition, compare an exact attempt token, and persist Attempted before returning at most one transport permit. A later transport is authorized only by exact negative evidence for that attempt; time, process liveness, local write success, and adapter result names are not evidence. Recipient/archive evidence settles the message. Attempt-only transports expose the exact message and attempt correlation in provider history. A same-UID filesystem operator may record audited correlated absence with a required reason and exact ledger precondition; evidence recording never performs transport.

If approved, P1 will add this requirement text plus one proposed decision that records the rejected compatibility/registry alternatives and the supporting experiments. The implementation then proceeds as four gated PRs described in the issue body. No source implementation starts before your approval. Merge and deployment remain separate gates.

Posted on behalf of @schickling

field	value
agent_identity	dev3.direct.omp.9exwnk6h
session	dev3.9exwnk6h
agent_persona	generalist
agent_supervisor	unavailable
agent_tool	OMP
agent_tool_version	18.1.7
agent_runtime	OMP 18.1.7
tooling_profile	dotfiles@931583a

[myobie]

Approved — add T03 and R41 as proposed and go ahead with the four gated PRs.

One non-blocking ask: make a held message visible where an operator already looks, not only in the ledger. My fleet runs unattended overnight, and a held message is only safer than a duplicate if somebody finds out about it.

[schickling-assistant]

Nathan approved T03 and the proposed transactional-delivery requirement. The proposal used R41, but R41 already names Typed agent desired state in the requirements ledger. P1 records the approved text unchanged as R43, the next unused requirement identifier. This is an identifier correction only.

Nathan’s held-message visibility ask is now explicit in the issue acceptance criteria.

Posted on behalf of @schickling

field	value
agent_identity	dev3.direct.omp.9exwnk6h
session	dev3.9exwnk6h
agent_persona	generalist
agent_supervisor	unavailable
agent_tool	OMP
agent_tool_version	18.1.7
agent_runtime	OMP 18.1.7
tooling_profile	dotfiles@931583a

[schickling-assistant]

P2 implementation surfaced one format contradiction: the canonical st2.delivery-ledger.v1 row in production has no attempt token, while the new fence requires one. Johannes selected a bounded canonical-v1 backfill rather than quarantining every existing ledger.

P2 now backfills tokenless rows under the transaction lock with a deterministic 128-bit token derived from the immutable row bytes, persists before any transport, counts the remaining tokenless rows read-only, and tracks deletion in DELTA-007. There is no dual write or general legacy reader. Rollback to a token-dropping writer is unsupported after token-bearing state is claimed.

Posted on behalf of @schickling

field	value
agent_identity	dev3.direct.omp.9exwnk6h
session	dev3.9exwnk6h
agent_persona	generalist
agent_supervisor	unavailable
agent_tool	OMP
agent_tool_version	18.1.7
agent_runtime	OMP 18.1.7
tooling_profile	dotfiles@931583a