153 lines
7.6 KiB
Markdown
153 lines
7.6 KiB
Markdown
---
|
|
id: suite-stream-rows
|
|
name: Contract-suite rows — cross-engine stream ordering equivalence + trim_to semantics
|
|
status: completed
|
|
depends_on: []
|
|
scope: moderate
|
|
risk: low
|
|
impact: phase
|
|
level: implementation
|
|
tags: [wave-5, contract-suite, streams]
|
|
---
|
|
|
|
## Description
|
|
|
|
Add the streams contract rows to
|
|
`alkstore-contract-suite/src/properties.rs` and wire them into both
|
|
engines' suite targets, discharging two backlog rows
|
|
(core-contract.md §Verification backlog): "Cross-engine stream
|
|
equivalence" (ADR-015 §3/§4) and "`trim_to` semantics on both
|
|
engines" (ADR-015 §5 — the legs the existing `extent_clamp_semantics`
|
|
row does not carry).
|
|
|
|
Rows to add:
|
|
|
|
- **`stream_ordering_equivalence`** — the ordering guarantee row:
|
|
a publish sequence with keyed/unkeyed interleavings yields `offset
|
|
ASC` global FIFO per stream — same publish order → same read order
|
|
on `read_since`, `read_from_consumer`, and a subscriber's attach
|
|
drain alike; offsets are strictly increasing per stream (per-stream
|
|
relative order — absolute offset values are explicitly *not*
|
|
cross-pinned: pg bigserial vs SQLite AUTOINCREMENT); `key`
|
|
round-trips exactly (`None` stays `None`, `Some` stays `Some`, on
|
|
every read form); `stream` carries the stream name and `created_at`
|
|
is unix-seconds-at-publish (informational — tolerance-bounded
|
|
proximity to now, never an ordering assertion). The single-event
|
|
key/payload round-trip already pins in
|
|
`payload_round_trip_stores_exact_encoding` — this row owns the
|
|
*sequence/ordering* property.
|
|
- **`trim_to_semantics`** — the full ADR-015 §5 row: exact-boundary
|
|
trim (`offset <= horizon` — the horizon's own row deletes,
|
|
horizon+1 survives), surviving rows keep their offsets (gaps legal,
|
|
never renumbered — the negative-horizon/immutability legs already
|
|
pin in `extent_clamp_semantics`; this row owns the exact-boundary
|
|
and resume legs), a read from a trimmed-away region resumes at the
|
|
trim horizon's first remaining row, a saved offset below the horizon
|
|
stays a valid position marker (`get_offset` returns it;
|
|
`read_from_consumer` resumes at the horizon), trim emits no
|
|
dedicated wake and no notify (a pre-attached listener idles across
|
|
the trim — tolerance-bounded absence), and a subscriber with a
|
|
saved checkpoint never loses its place across a trim (its next read
|
|
continues from the horizon, not from a renumbered past).
|
|
|
|
## Acceptance Criteria
|
|
|
|
- [x] Two rows exist, version-stamped (ADR-015 §3/§4/§5, ADR-019 §6
|
|
as applicable)
|
|
- [x] Rows wired into both engines' `contract_suite.rs` targets
|
|
- [x] SQLite column green server-less; pg column green against the
|
|
harness server
|
|
- [x] No duplication with the existing rows' legs (cross-reference in
|
|
each row's doc comment which row owns which leg)
|
|
- [x] `cargo test -p alkstore-sqlite -p alkstore-postgres` green
|
|
(pg rows skip cleanly server-less); clippy `-D warnings`; fmt clean
|
|
|
|
## References
|
|
|
|
- docs/architecture/core-contract.md §Verification backlog (cross-engine
|
|
stream equivalence; trim_to semantics)
|
|
- docs/architecture/decisions/015-streams-depth.md §3/§4/§5
|
|
- docs/architecture/decisions/019-mechanism-handle-surfaces.md §6
|
|
- alkstore-contract-suite/src/properties.rs (the existing rows whose
|
|
legs this task complements)
|
|
|
|
## Notes
|
|
|
|
> Decisions of record the implementation made that the description
|
|
> didn't pin:
|
|
|
|
- **Sequence shape** — the ordering row publishes 6 events
|
|
(unkeyed, keyed `Some("a")`, keyed `None` explicitly, unkeyed, keyed
|
|
`Some("a")`, unkeyed) into one stream and pins the same order across
|
|
four read forms: whole `read_since`, cursor-paginated `read_since`
|
|
(limit 2, chained), `read_since` from a mid-stream cursor,
|
|
`read_from_consumer` (fresh consumer = 0 and from a mid saved
|
|
checkpoint), and a subscriber's attach drain. The explicit-`None`
|
|
keyed publish form's equivalence to plain `publish` (ADR-015 §2) is
|
|
pinned as part of the sequence (its event carries `key = None` like
|
|
a plain publish's, indistinguishably) — it was otherwise unpinned in
|
|
the suite. `created_at` is asserted as a ±10 s tolerance band around
|
|
the run's clock read, never an ordering assertion (the band is a test
|
|
constant; the row text documents it as informational).
|
|
- **Subscriber-drain pattern** — both rows lead the attach drain with a
|
|
blocking `recv()` (first event) and then drain `try_recv` until
|
|
`None`, mirroring `receiver_close_and_save_arms`' pattern: the
|
|
engines deliver the attach read asynchronously, so a leading
|
|
`try_recv` could observe an empty feed early. All drains stay single
|
|
page-sized (≤ 6 events), so the drain-to-None termination is
|
|
not page-boundary sensitive.
|
|
- **Idle-absence window** — the pre-attached listener idles across the
|
|
trims in a 400 ms bounded window with 50 ms `try_recv` polls
|
|
(same shape as the pg engine's own trim test
|
|
`trim_to_trims_the_exact_boundary_and_never_renumbers`); on SQLite
|
|
the wake fires (spurious watcher hint, contract-legal per ADR-015 §5)
|
|
but delivers nothing — the assertion is on delivered events, not on
|
|
wake counts.
|
|
- **Re-attach legs** — the subscriber-never-loses-its-place property is
|
|
pinned in two directions: a fresh `subscribe("behind")` with a
|
|
saved checkpoint below the horizon attach-drains exactly the
|
|
surviving sequence (resumes at the horizon, never a renumbered
|
|
past), and a fresh `subscribe("listener")` with the pre-trim
|
|
checkpoint above the horizon yields nothing (its place kept).
|
|
- **pg LISTEN/NOTIFY channel collision** — pg's wake channels are
|
|
mechanism-named and database-wide (not schema-scoped), so a
|
|
concurrently running suite row publishing to its own "events" stream
|
|
delivers cross-schema *wakes* to this row's subscriber. The row is
|
|
safe against this by construction — wakes only trigger re-drains
|
|
from this row's own schema's storage, which yields nothing — so no
|
|
rename away from "events" was needed. (Observed an unreproducible
|
|
single failure across 14 pg suite runs during development, under the
|
|
concurrent SQLite+pg gate condition; see Summary.)
|
|
|
|
## Summary
|
|
|
|
> What landed, verified how:
|
|
|
|
Two rows added to `alkstore-contract-suite/src/properties.rs`,
|
|
re-exported from the crate's lib, wired into both engines'
|
|
`contract_suite.rs` targets (SQLite: direct test fns; pg: the
|
|
`harness_row!` macro with unique factory tags) — 21 rows in each
|
|
engine's column, up from 19:
|
|
|
|
- `stream_ordering_equivalence` — ADR-015 §4/§3/§1 stamped;
|
|
key/payload byte-exactness cross-referenced to
|
|
`payload_round_trip_stores_exact_encoding`, tx-seam legs to
|
|
`publish_with_key_tx_commit_atomicity`.
|
|
- `trim_to_semantics` — ADR-015 §5/ADR-019 §6 stamped; the
|
|
negative-horizon/immutability legs cross-referenced to
|
|
`extent_clamp_semantics` (ADR-023 §2). Owns the exact-boundary,
|
|
resume, checkpoint-validity, re-attach, and idle-absence legs.
|
|
|
|
Verification: `cargo test -p alkstore-sqlite -p alkstore-postgres
|
|
--test contract_suite` green — 21/21 against the SQLite factory, 21/21
|
|
against the harness server (`pglo-poc` :15432, `postgres`/`poc`/`blobs`)
|
|
including both new rows, and server-less the pg rows skip cleanly.
|
|
Full workspace `cargo test` green (12 test binaries, all ok), `cargo
|
|
clippy --workspace --all-targets -- -D warnings` clean, `cargo fmt
|
|
--check` clean. Stability: the pg suite passed 7 consecutive full runs
|
|
plus 5 focused runs of the two new rows (`--test-threads=6`) and 2
|
|
SQLite-focused runs; one unreproducible single failure of
|
|
`row_trim_to_semantics` occurred during development under the
|
|
concurrent SQLite+pg run condition (14+ pg runs since — none failed);
|
|
the row's wake-driven legs are bounded-wait/state-outcome shaped, so
|
|
the suite's determinism posture holds. |