Skip to content
Open
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
4 changes: 2 additions & 2 deletions INVARIANTS.md

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -81,3 +81,24 @@ boundary; this decision does not claim those later steps are implemented.
implementation changes under R43.
- `INVARIANTS.md` names Codex and OpenCode ownership until the later driver
adoption proofs pass.

## Amendment 1 — 2026-09-08 (Q35)

Johannes approved one bounded exception to the no-compatibility consequence
above. R43 requires a fresh durable attempt token, but the canonical
`st2.delivery-ledger.v1` entry predates that field. Codex and OpenCode already
hold live durable evidence in this format. Rejecting those bytes would preserve
implementation purity by discarding the safety property this work exists to
provide.

A tokenless canonical Codex or OpenCode entry is therefore read only inside the
same locked transaction that owns every mutation. st2 derives a deterministic
128-bit token from the exact immutable entry bytes and persists the token before
any other mutation or transport. All later operations require the exact token.
The reader never dual-writes, never accepts an attempt-only legacy record, and
never makes a pre-token writer a supported rollback target.

This is temporary implementation state under T04. Its remaining inputs stay
countable, and a named deletion signal owns removal of the reader. T03 remains
unchanged for Claude, pi, and OMP: no tokenless attempt-only record has shipped,
so their adoption stays a clean forward-only boundary.
54 changes: 54 additions & 0 deletions docs/vrs/.delta/DELTA-007-tokenless-delivery-ledger-v1-reader.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
# DELTA-007: tokenless canonical delivery entries remain readable during P2 rollout

Status: open

## Divergence

R43 makes an exact attempt token part of every delivery mutation. Canonical
`st2.delivery-ledger.v1` entries written before P2 have no such field. Codex and
OpenCode can still hold live durable evidence in those entries, so rejecting the
record would discard the ownership R43 exists to preserve.

T04 therefore permits one temporary reader case: a tokenless canonical Codex or
OpenCode entry. This is not the pre-ledger `delivery-state.json` translation
owned by DELTA-006 and never applies to Claude, pi, or OMP.

## VRS

[T04](../requirements.md) requires the reader to run inside the same R43
transaction lock, durably add the token before any other mutation or transport,
remain countable, and be deleted after fleet evidence proves that no tokenless
entry can return. Amendment 1 of
[decision 0018](../.decisions/0018-harness-identity-and-delivery-evidence-policy-are-distinct.md)
records Johannes's Q35 choice and makes a pre-token writer an unsupported
rollback target after a token-bearing claim.

## Implementation

The canonical entry parser accepts an absent `attemptToken` only long enough for
the locked transaction loader to derive a deterministic 128-bit token from the
exact immutable entry bytes and persist the token-bearing entry. New claims use
operating-system randomness. Every public mutation receives a canonical entry
with a token and compares that exact token.

The reader never emits tokenless bytes, never dual-writes, and never rewrites a
foreign, malformed, or unsupported ledger. Read-only roster and Doctor
observation count tokenless entries without invoking the backfill.

## Direction

update implementation

## Resolution Signal

`st2 doctor` prints, per seat, a `tokenless delivery ledger (DELTA-007)` advisory
with `tokenlessEntries=<n>` whenever a Codex or OpenCode ledger contains one or
more tokenless canonical entries. Silence means the reader contributed no input
on that seat; observation is read-only and does not make the signal clear.

The delta resolves after the advisory is absent on every admitted host for seven
consecutive days. Decision 0018 Amendment 1 already records that a pre-token
writer is not a supported rollback target, so no second rollback decision is
required. Deletion removes the absent-token parser arm, deterministic backfill,
tokenless counter, Doctor advisory, and this delta in one change. Token-bearing
`st2.delivery-ledger.v1` remains the canonical format.
12 changes: 9 additions & 3 deletions docs/vrs/requirements.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,15 @@ accepted.
- **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
retains no legacy delivery path, downgrade reader, dual write, translation
bridge, or compatibility fence. Preserving the existing Codex and OpenCode
ledger format avoids a migration; it is not a compatibility layer.
retains no legacy attempt-only delivery path, downgrade reader, dual write,
translation bridge, or compatibility fence.
- **T04 Bounded canonical token backfill:** A tokenless canonical
`st2.delivery-ledger.v1` Codex or OpenCode entry is read only to derive and
durably add its exact attempt token under the R43 transaction lock before any
other mutation or transport. st2 never dual-writes the entry. The temporary
reader remains explicit and countable until fleet evidence proves that no
tokenless canonical entry can return; then st2 deletes it. After a
token-bearing claim, rollback to a writer that drops the token is unsupported.

## Requirements

Expand Down
110 changes: 104 additions & 6 deletions docs/vrs/spec.md
Original file line number Diff line number Diff line change
Expand Up @@ -1139,14 +1139,112 @@ does not branch on provider identity when it grades evidence. A synthetic
identity-policy pairing proves that separation without adding a provider
registry or another core branch.

This section specifies the complete R43 target. At this stage, only Codex and
OpenCode own delivery through the ledger. Claude, pi, and OMP have the
attempt-only policy, but their drivers adopt durable ownership in separate
changes. Transactional mutation, exact attempt tokens, FIFO enforcement,
provider-visible correlation, and operator-negative evidence are also separate
implementation steps. `INVARIANTS.md` names only the subset proved by the
The current production adopters are Codex and OpenCode. Claude, pi, and OMP
map to attempt-only policy, but their drivers do not own delivery through this
ledger until their process-local suppression is replaced.

### Transaction boundary

Each per-agent, per-harness ledger has one permanent sibling lock file. st2
opens the lock without following symlinks, holds an exclusive local kernel lock,
and never removes or renames the lock file. Initial recovery and every mutation
run as one transaction:

```text
lock → re-read exact bytes → validate → compare attempt/precondition
→ decide one transition → fsync staged bytes → rename → fsync directory
→ return result → unlock
```

The in-process object is configuration, not authority. A cached observation
never authorizes transport. A transaction that cannot prove whether its commit
landed returns no transport permit; a later transaction re-reads the durable
result.

`claim` is the only transport authorization. It combines the former retry
decision and attempt write. Under the lock it admits only the canonical FIFO
head, requires no outstanding attempt or exact negative evidence for that
head's current token, generates a fresh opaque 128-bit attempt token, persists
`Attempted`, and only then returns one token-bearing permit. A later filename
cannot overtake an outstanding head. A binding change cannot discard an
ambiguous attempt.

Positive evidence, provider negative evidence, archive pruning, binding
changes, and operator evidence compare the complete attempt identity:
`(binding, filename, provider correlation, attempt token)`. Stale evidence is a
typed refusal and writes nothing. Positive phases remain monotone. Exact
negative evidence is retained as evidence for its token; one later `claim`
consumes it by persisting a new token before another transport can start.
Archive settlement removes only the exact token captured by the reconciling
snapshot, so a stale unread snapshot cannot delete a replacement attempt.

### Canonical token backfill

The pre-token and token-bearing records share the canonical
`st2.delivery-ledger.v1` schema. Under T04, a tokenless Codex or OpenCode entry
is a temporary read case, not a second writer format. The transaction derives a
deterministic 128-bit token from the exact immutable entry bytes and durably
adds it before any other mutation or transport. New claims always use
fail-closed operating-system randomness. The implementation counts remaining
tokenless inputs and deletes this reader only after its recorded fleet signal
stays clear. A pre-token writer is not a supported rollback target after a
token-bearing claim.

### Attempt-only correlation and operator evidence

An attempt-only transport places this exact first line in provider-visible
content:

```text
[st2-delivery filename=<canonical-message-filename> attempt=<attempt-token>]
```

The marker contains no path, agent identity, binding, provider correlation,
reason, or delivery claim. It identifies only the exact durable attempt that an
operator can seek in provider history. The marker renderer validates the
canonical filename and token and has no provider branch.

The same-UID operator command records absence; it does not transport:

```text
st2 message delivery-negative <agent> <filename> \
--attempt-token <token> \
--ledger-sha256 <exact-observed-ledger-digest> \
--reason <non-empty-reason>
```

The transaction verifies unchanged ledger bytes, harness and agent ownership,
the exact attempt tuple, an unsettled state, and the absence of an archive
receipt. It persists source `operator`, OS uid, optional non-authoritative
process and `ST_AGENT` provenance, reason, binding, filename, provider
correlation, attempt token, ledger precondition, and observation time before
returning a receipt. A changed digest, stale token, settled entry, malformed
ledger, or foreign ledger refuses without rewriting bytes. A later pump must
perform a separate `claim`.

### Operator visibility

Read-only delivery observation never invokes recovery or token backfill.
`st2 agents` joins a ledger adopter to one typed `delivery` value:

- `absent` when the provider has no ledger file;
- `idle` when a readable ledger has no unsettled entry;
- `held` with the closed hold reason, filename, exact ledger digest, and the
attempt token and recovery command when actionable. The token and recovery
command are null for a DELTA-007 tokenless row; the recovery command is also
null after exact negative evidence; or
- `indeterminate` when existing bytes cannot be validated.

The normal roster omits private state paths, bindings, and provider-native
correlation. Human output renders the same fact as
`delivery:held(<reason>)`. This field is independent of presence, observed
harness state, native-driver diagnostics, context, and inbox count.
`INVARIANTS.md` names only the harness adopters and proof set present in the
current implementation.

`st2 doctor` reports the count of observed DELTA-007 tokenless rows without
backfilling them. The diagnostic is advisory and byte-preserving.

## Message lifecycle

```text
Expand Down
Loading
Loading