Skip to content
Draft
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
1 change: 1 addition & 0 deletions AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -389,6 +389,7 @@ Before finishing a change, ensure:
- [`docs/protocol/`](docs/protocol/) — the authoritative protocol contracts: [`scheduler-semantics.md`](docs/protocol/scheduler-semantics.md) (the canonical acceptance algorithm, I1) and [`application-contract.md`](docs/protocol/application-contract.md) (the `Application` FFI trait contract).
- [`docs/invariants.md`](docs/invariants.md) — register of cross-module invariants (what's load-bearing across files) + the fail-loud check policy.
- [`docs/review/`](docs/review/) — dated correctness-review ledgers; open findings, settled designs, work packages.
- [`docs/plans/`](docs/plans/) — active coordination tracks; agreed work split, design directions, open decisions.
- [`docs/threat-model/README.md`](docs/threat-model/README.md) — trust boundaries, in-scope and out-of-scope threats.
- [`docs/recovery/README.md`](docs/recovery/README.md) — recovery design, TLA+ formal verification, design history.
- [`docs/snapshots/`](docs/snapshots/) — app snapshots: [`format.md`](docs/snapshots/format.md) (dump trait + wire format) and [`lifecycle.md`](docs/snapshots/lifecycle.md) (take/promote/GC/lease design + crash-safety).
Expand Down
1 change: 1 addition & 0 deletions CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ Rust edition 2024 / Axum API / SQLite (rusqlite, WAL) / EIP-712 signing / SSZ en
- **[`docs/protocol/`](docs/protocol/)** — the authoritative protocol contracts: [`scheduler-semantics.md`](docs/protocol/scheduler-semantics.md) (canonical acceptance algorithm) and [`application-contract.md`](docs/protocol/application-contract.md) (the `Application` FFI trait). Read before touching the scheduler, the gold frontier, the fold, or an `Application` impl.
- **[`docs/invariants.md`](docs/invariants.md)** — cross-module invariants register + the fail-loud check policy. Check it before changing anything it lists as load-bearing.
- **[`docs/review/`](docs/review/)** — dated correctness-review ledgers: known-open findings, settled designs, work packages. Check for open findings in code you're about to touch.
- **[`docs/plans/`](docs/plans/)** — active coordination tracks: agreed work split, design directions, and open decisions across in-flight efforts. Check before starting work that might belong to a track.
- **[`docs/threat-model/README.md`](docs/threat-model/README.md)** — trust boundaries and in-scope threats.
- **[`docs/recovery/README.md`](docs/recovery/README.md)** — preemptive recovery design + TLA+ proofs.
- **[`docs/snapshots/lifecycle.md`](docs/snapshots/lifecycle.md)** — snapshot lifecycle design + invariants (take/promote/GC, crash-safety). Read before touching the inclusion lane's safe-frontier/snapshot path.
Expand Down
296 changes: 296 additions & 0 deletions docs/plans/2026-07-coordination-tracks.md

Large diffs are not rendered by default.

206 changes: 206 additions & 0 deletions docs/plans/2026-07-track3-feed-replay-design.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
# Feed & Replay Protocol — Design Draft (Track 3)

**Status: draft for review** (us, Stephen, Bart). Supersedes the ad-hoc WS
protocol; closes review F7/WP5. On acceptance, the normative parts graduate
into `docs/protocol/` and the README's WS section is rewritten against them.

## 1. Motivation

The current protocol is an unframed infinite stream of a two-variant enum
over a WS socket, with every session-level signal smuggled into transport
close frames. Three defects drive the redesign:

- **F7 (high, open):** no invalidation/rollback signal. Recovery cascades
invalidate already-streamed rows and re-sequence replacements at higher
offsets under a *reused* batch nonce, so a cursor-resumed mirror silently
diverges. The interim rule ("treat any socket drop as a discontinuity and
rebuild the soft suffix") works but is undocumented, wasteful, and easy to
get wrong.
- **No historical bootstrap:** the catch-up window is shallow (static cap);
a consumer cannot build state from genesis over the feed at all.
- **No control plane:** policy violations are prose in close reasons;
the catch-up→live transition is unmarked; there is no handshake.

Consumer model (Bart's libdex is the concrete instance): replay finalized
history via HTTP, then subscribe for the soft tip, maintaining a bit-exact
mirror of the dapp state — with recovery detectable and recoverable.

## 2. Concepts and coordinates

- **Input-box coordinate** `input_index: u64` — position in `safe_inputs`
(per-application InputBox order). Append-only, sourced from L1 safe
blocks: immutable once present.
- **Feed coordinate** `offset: u64` — position in the ordered L2-tx stream
(`valid_sequenced_l2_txs` rowid). Append-only, **but** rows above the gold
boundary can be invalidated (hidden, then re-sequenced at new offsets) by
recovery.
- **Gold boundary `G`** — the greatest offset belonging to a batch that is
scheduler-accepted on L1 (`safe_accepted_batches` frontier). Rows with
`offset <= G` are recovery-stable: they can never be invalidated. `G` only
advances.
- **Generation `g: u64`** — the stream's "reality version". Bumped by every
recovery cascade. Two events with the same offset but different
generations may differ; everything at or below `G` is generation-free.
- **Live head `H`** — the greatest currently-valid offset.

## 3. Generation semantics

- Persisted in a new singleton (`feed_generation`), read at subscribe time
and bumped **in the same transaction** as `cascade_invalidate_from` (both
the startup-recovery path and `setup --recovery`'s rebuild path).
- Monotonic across DB rebuilds: `setup --recovery` reconstructs the DB from
a dump + L1, so the generation must be carried in the dump's sequencer
sidecar (`DumpInfo` gains a `feed_generation` field) and bumped once on
every rebuild. Without this, a rebuilt deployment would reset to 0 and a
mirror would mistake it for a fresh reality. (Open question 3 if we would
rather derive it from something already durable.)
- Exposed three ways: `GET /generation` (trivial JSON, cheap to poll), the
subscribe handshake (§5), and best-effort in-band `Discontinuity` events.

## 4. Historical replay endpoints (HTTP, paginated, finalized-only)

Both endpoints serve **immutable data only** and therefore carry no
generation. Pages are stable forever: aggressively cacheable, safe to
mirror, resumable at any time.

### 4.1 `GET /inputs?from_index=N&limit=K`

Raw input-box order over `safe_inputs`: direct inputs **and** our own
batches, exactly as L1 ordered them, each row with the PR #26 provenance:

```json
{ "items": [ { "input_index": 7, "sender": "0x…", "payload": "0x…",
"block_number": 123, "block_timestamp": 1700000000,
"transaction_hash": "0x…" } ],
"next_index": 8, "end_index": 41 }
```

`end_index` is the current exclusive upper bound of the table. Rows appear
here once the L1 safe head passes them — this endpoint's data is "safe" in
the L1 sense by construction.

### 4.2 `GET /l2-txs?from_offset=N&limit=K`

Feed order, **capped at the gold boundary `G`**. Items use the same shapes
as the WS data events (§5.3) so a replay page and a live event are
interchangeable inputs to a mirror:

```json
{ "items": [ /* same JSON shapes as WS user_op / direct_input events */ ],
"next_offset": 101, "gold_boundary": 250 }
```

The server never serves `offset > G` here. A client sees `next_offset >
gold_boundary` as "history exhausted — switch to the subscription".

Storage note: `G` is computable as the max offset of rows whose batch nonce
is ≤ the `safe_accepted_batches` frontier nonce; add a dedicated indexed
query, computed per page request (it only advances, so a stale read is
merely conservative).

## 5. WS subscription v2

### 5.1 Handshake

`GET /subscribe?from_offset=N[&generation=g]` upgrades, then the server's
**first frame is always** `hello`:

```json
{ "kind": "hello", "generation": 4, "live_head": 312, "gold_boundary": 250,
"max_subscribers": 64 }
```

- If the client supplied `generation` and it is stale, the server sends
`{ "kind": "error", "error": "stale_generation", "current_generation": 4 }`
after `hello`, then closes 1008. The client rebuilds its soft suffix
(everything above its last known `G`) and resubscribes.
- Omitting `generation` means "no continuity claim" — accepted, and the
client must treat its own soft suffix as void (fresh-mirror semantics).

### 5.2 Depth guarantee (replaces the static catch-up cap)

**Invariant: any `from_offset >= G` is always serveable.** The static
50k-event cap is replaced by the rule "the WS covers everything above the
gold boundary; HTTP replay covers everything at or below it." The soft
suffix is exactly the region a mirror cannot get elsewhere, so the server
must never refuse it. A `from_offset < G` request gets:

```json
{ "kind": "error", "error": "below_gold_boundary", "gold_boundary": 250 }
```

then a 1008 close — the client pages `/l2-txs` up to `G` first. This makes
the replay+subscribe pair a closed system with a two-step client loop:

1. Page `/l2-txs` until `next_offset > gold_boundary` (call it `G0`).
2. Subscribe `from_offset = G0, generation = g` (from `/generation` or the
last `hello`). On `stale_generation`: drop the soft suffix, goto 1 (only
the suffix above the *new* `G` needs re-pulling — `G` advanced past
everything that settled meanwhile). On `below_gold_boundary`: goto 1.

No race window: between steps 1 and 2, `G` can only advance, and rows in
`(G0, G]` are still serveable over WS by the invariant (they were above the
boundary when sequenced and remain valid).

### 5.3 Events

Data events keep PR #26's **denormalized per-row context** (`user_op` /
`direct_input` with nonce, safe_block, batch_nonce, input_index,
block_timestamp, transaction_hash). Rationale: Bart has confirmed this field
set suffices for a bit-exact mirror; stateless consumers need no
boundary-tracking; and the replay endpoint reuses the shapes verbatim.
Normalized `frame_sealed`/`batch_sealed` boundary events are **rejected for
now** (open question 1 records the revisit trigger).

Control events (new, same tagged enum):

- `hello` — §5.1.
- `live` — sent once when catch-up reaches the live head; everything after
is a soft confirmation in real time. (Consumers that only care about
settled state can hold their render until this.)
- `discontinuity { new_generation }` — **best-effort only**: sent on
graceful invalidations. A crash or danger-detector exit sends nothing —
the load-bearing detection is `stale_generation` at resubscribe. Mirrors
MUST NOT rely on receiving this event.
- `error { error, … }` — typed, replaces close-reason prose. The socket
still closes 1008 after; the close reason becomes advisory.

### 5.4 Wire format

JSON text frames, serde-tagged (`"kind"`), new fields mandatory (we break
old clients freely). `WsTxMessage = BroadcastTxMessage` stays the single
shared type; control events join the same enum so the SDK matches
exhaustively.

## 6. What this replaces

- `WS_CATCHUP_WINDOW_EXCEEDED_REASON` and the `live_start_offset` close
reason — superseded by `below_gold_boundary` + `/l2-txs`.
- The interim "rebuild on any socket drop" rule (F7) — superseded by the
generation contract; the rule survives only as the omitted-generation
fallback (§5.1).
- README's WS section — rewritten from this doc.

## 7. Implementation stages (separate PRs)

1. **Replay endpoints** — additive: the two HTTP routes + gold-boundary
query + tests (pagination, immutability across a forced cascade,
provenance fields). No WS changes; ships value to Bart immediately.
2. **Generation plumbing** — `feed_generation` singleton + bump-in-cascade
+ `DumpInfo` carry + `GET /generation`. Still no WS change.
3. **WS v2** — handshake, control events, depth-guarantee rework, SDK +
harness update, README rewrite, F7 ledger tick.

## 8. Open questions

1. **Boundary events**: revisit if a consumer ever needs frame/batch
boundaries the denormalized rows can't express (e.g. exact frame fee
schedule per epoch). Trigger: a second consumer with fold-shaped needs.
2. **`/inputs` shape**: confirm with Bart how his consumer reconciles
against raw L1 order (vs. only feed order + L1 settlement via
batch_nonce) so 4.1 serves exactly that need.
3. **Generation continuity across rebuilds**: `DumpInfo` carry (proposed) vs
deriving from an existing durable counter. DumpInfo carry is simple but
means generation is only as durable as the promoted dump.
4. **Auth/limits**: replay endpoints are unauthenticated reads like
`/latest_snapshot`; decide rate limits before public exposure.
Loading