From 9301bb926b3b4423f626248c6eeae87f2b0ab8f9 Mon Sep 17 00:00:00 2001 From: "glm-5.3-flash" Date: Sun, 11 Oct 2026 14:34:15 +0000 Subject: [PATCH] =?UTF-8?q?core:=20verify=20and=20pin=20the=20receiver's?= =?UTF-8?q?=20pre-yield=20offset()=20value=20(review=20004=20item=2012,=20?= =?UTF-8?q?core-pin-offset-initial-value)=20=E2=80=94=20the=20three=20engi?= =?UTF-8?q?nes=20verified=20equal=20live,=20so=20the=20doc-pin=20branch=20?= =?UTF-8?q?applies:=20offset()=20reads=200=20before=20any=20yield=20on=20e?= =?UTF-8?q?very=20receiver=20=E2=80=94=20fresh=20consumer,=20stored=20posi?= =?UTF-8?q?tive=20checkpoint,=20stored=20negative=20seed=20(ADR-023=20?= =?UTF-8?q?=C2=A72's=20totality=20arm,=20the=20one=20a=20checkpoint-seeded?= =?UTF-8?q?=20realization=20would=20surface=20on)=20=E2=80=94=20the=20no-y?= =?UTF-8?q?ield=20sentinel,=20never=20the=20stored=20checkpoint:=20the=20c?= =?UTF-8?q?heckpoint=20gates=20the=20feed's=20attach-read=20start=20while?= =?UTF-8?q?=20the=20receiver's=20offset=20tracks=20the=20last-yielded=20ev?= =?UTF-8?q?ent=20only,=20composing=20with=20the=20pinned=20pre-yield=20sav?= =?UTF-8?q?e=5Foffset()=20no-op;=20the=20attach=20read's=20prefetches=20si?= =?UTF-8?q?t=20unobserved=20and=20the=20first=20recv/try=5Frecv=20observat?= =?UTF-8?q?ion=20is=20the=20first=20move=20(then=20the=20post-yield=20valu?= =?UTF-8?q?e,=20receiver=5Fclose=5Fand=5Fsave=5Farms'=20pin).=20Verified?= =?UTF-8?q?=20by=20code=20read=20first=20(all=20three=20offset()=20bodies?= =?UTF-8?q?=20are=20self.position,=20all=20three=20constructors=20seed=20p?= =?UTF-8?q?osition:=200=20unconditionally=20=E2=80=94=20mem=20stream.rs:35?= =?UTF-8?q?3,=20sqlite=20:399,=20pg=20:620)=20then=20live:=20new=20suite?= =?UTF-8?q?=20row=20receiver=5Foffset=5Fpre=5Fyield=5Fis=5Fzero=20(alkstor?= =?UTF-8?q?e-contract-suite,=20stamped=20ADR-008=20=C2=A78=20+=20the=20cor?= =?UTF-8?q?e-contract.md=20pin,=20four=20arms=20incl.=20the=20first-observ?= =?UTF-8?q?ation=20composition=20leg)=20green=20on=20all=20three=20columns?= =?UTF-8?q?,=20pg=20against=20the=20harness=20server=20(parked=20pglo-poc?= =?UTF-8?q?=20:15432);=20pinned=20in=20three=20places:=20core-contract.md?= =?UTF-8?q?=20streams/subscribe=20row=20(dated=202026-10-11=20annotation)?= =?UTF-8?q?=20+=20a=20verification-backlog=20bullet=20recording=20the=20ve?= =?UTF-8?q?rified=20pin,=20the=20core=20trait=20doc=20on=20offset()=20(cor?= =?UTF-8?q?e's=20doc=20comments=20are=20contract=20text),=20and=20the=20su?= =?UTF-8?q?ite=20row=20itself=20=E2=80=94=20ADR-008=20=C2=A78's=20shape=20?= =?UTF-8?q?comment=20deliberately=20left=20untouched=20(doc-only=20verific?= =?UTF-8?q?ation=20takes=20no=20ADR=20amendment,=20noted=20in=20the=20task?= =?UTF-8?q?);=20no=20engine=20code=20changed,=20no=20divergence=20to=20rai?= =?UTF-8?q?se;=20gates=20green:=20workspace=20build/tests=20server-less,?= =?UTF-8?q?=20full=20pg=20column=20vs=20harness=20(135+26+9),=20clippy=20-?= =?UTF-8?q?D=20warnings,=20fmt=20--check,=20doc=20gate=20zero=20warnings,?= =?UTF-8?q?=20fuzz=20corpus=20replay=206/6,=20wasm32=20mem=20check,=20task?= =?UTF-8?q?graph=20validate=20(96);=20task=20->=20completed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- alkstore-contract-suite/src/lib.rs | 7 +- alkstore-contract-suite/src/properties.rs | 82 +++++++++++++++++++++++ alkstore-mem/tests/contract_suite.rs | 12 +++- alkstore-postgres/tests/contract_suite.rs | 12 +++- alkstore-sqlite/tests/contract_suite.rs | 12 +++- alkstore/src/event_receiver.rs | 6 +- docs/architecture/core-contract.md | 23 ++++++- tasks/core-pin-offset-initial-value.md | 63 +++++++++++++++-- 8 files changed, 196 insertions(+), 21 deletions(-) diff --git a/alkstore-contract-suite/src/lib.rs b/alkstore-contract-suite/src/lib.rs index b15e449..a70ac87 100644 --- a/alkstore-contract-suite/src/lib.rs +++ b/alkstore-contract-suite/src/lib.rs @@ -45,7 +45,8 @@ pub use properties::{ payload_round_trip_stores_exact_encoding, payload_too_large_never_produced_on_mem, payload_too_large_never_produced_on_sqlite, payload_too_large_produced_on_pg, publish_with_key_tx_commit_atomicity, queue_depth_reclaim_and_dead_letter, - receiver_close_and_save_arms, scheduler_boundary_fires, scheduler_bounded_catchup, - scheduler_leadership_discipline, stream_ordering_equivalence, sweep_no_stranded_rows, - trim_to_semantics, wake_receiver_shapes, with_tx_panicking_closure_rolls_back, + receiver_close_and_save_arms, receiver_offset_pre_yield_is_zero, scheduler_boundary_fires, + scheduler_bounded_catchup, scheduler_leadership_discipline, stream_ordering_equivalence, + sweep_no_stranded_rows, trim_to_semantics, wake_receiver_shapes, + with_tx_panicking_closure_rolls_back, }; diff --git a/alkstore-contract-suite/src/properties.rs b/alkstore-contract-suite/src/properties.rs index 93496b3..a53be7b 100644 --- a/alkstore-contract-suite/src/properties.rs +++ b/alkstore-contract-suite/src/properties.rs @@ -1508,6 +1508,88 @@ pub async fn receiver_close_and_save_arms(factory: &dyn StoreFactory) { ); } +/// **Receiver pre-yield `offset()` initial value** — `offset()` reads +/// 0 before any event has been yielded, on every receiver: a fresh +/// consumer's (no checkpoint), a consumer with a stored checkpoint +/// (the attach read prefetches past it unobserved), and a consumer +/// with a negative checkpoint (the ADR-023 §2 totality seed — a +/// checkpoint-seeded realization would surface it here). The +/// pre-yield value is the no-yield sentinel, never the stored +/// checkpoint: the checkpoint gates the feed's attach-read start, +/// while the receiver's offset tracks the last-yielded event only — +/// the pre-yield `save_offset()` no-op (stored checkpoint untouched) +/// and the 0 sentinel compose. The first `recv`/`try_recv` +/// observation is the first move; the post-yield value is the +/// last-yielded event's offset (`receiver_close_and_save_arms`' pin). +/// +/// Contract stamp: ADR-008 §8 (`EventReceiver`'s `offset() -> i64` +/// shape, "the receiver's current offset") — the pre-yield return +/// pinned in the core-contract.md streams row (annotated 2026-10-11, +/// review-004 item 12's named-gap verification). +pub async fn receiver_offset_pre_yield_is_zero(factory: &dyn StoreFactory) { + let store = factory.open().await.expect("factory opens a store"); + + let stream = store.stream("events").await.unwrap(); + let published = stream.publish(json!({"n": 1})).await.unwrap(); + + // Arm 1: fresh consumer — no checkpoint exists at all. + let mut fresh = stream.subscribe("fresh-preyield").await.unwrap(); + assert_eq!( + fresh.offset(), + 0, + "a fresh consumer's pre-yield offset() reads the 0 sentinel" + ); + + // Arm 2: consumer with a stored positive checkpoint — the attach + // read starts past it, yet the receiver's offset stays at the + // sentinel until an event is observed. + stream + .save_offset("seeded-preyield", published) + .await + .unwrap(); + let seeded = stream.subscribe("seeded-preyield").await.unwrap(); + assert_eq!( + seeded.offset(), + 0, + "a checkpointed consumer's pre-yield offset() reads the 0 sentinel, not the stored checkpoint" + ); + + // Arm 3: consumer with a stored negative checkpoint (ADR-023 §2's + // totality row: the seed stores raw) — the arm where a + // checkpoint-seeded realization would diverge. + stream + .save_offset("seeded-negative-preyield", -5) + .await + .unwrap(); + let negative = stream.subscribe("seeded-negative-preyield").await.unwrap(); + assert_eq!( + negative.offset(), + 0, + "a negative-checkpoint consumer's pre-yield offset() reads the 0 sentinel, not the seed" + ); + + // The first observation is the first move: the fresh receiver's + // attach-read-prefetched event yields and the post-yield value + // lands the last-yielded offset exactly (the sentinel composes + // with the yield discipline). + let first = fresh + .recv() + .await + .expect("the fresh receiver is open and holds the prefetched event") + .unwrap(); + assert_eq!( + first.offset, published, + "the fresh receiver's first yield carries the prefetched event" + ); + assert_eq!( + fresh.offset(), + published, + "the first yield moves offset() off the sentinel to the last-yielded offset" + ); + + factory.teardown().await.expect("factory teardown"); +} + /// **Wake semantics under the pinned `WakeReceiver` shapes** — the /// wake contract's pinnable core, tolerance-bounded (wakes are /// best-effort hints — the row asserts state outcomes, never delivery diff --git a/alkstore-mem/tests/contract_suite.rs b/alkstore-mem/tests/contract_suite.rs index a5f6626..444a686 100644 --- a/alkstore-mem/tests/contract_suite.rs +++ b/alkstore-mem/tests/contract_suite.rs @@ -47,9 +47,10 @@ mod rows { name_validation_rejects_empty_and_reserved, outbox_enqueue_tx_commit_atomicity, payload_round_trip_stores_exact_encoding, payload_too_large_never_produced_on_mem, publish_with_key_tx_commit_atomicity, queue_depth_reclaim_and_dead_letter, - receiver_close_and_save_arms, scheduler_boundary_fires, scheduler_bounded_catchup, - scheduler_leadership_discipline, stream_ordering_equivalence, sweep_no_stranded_rows, - trim_to_semantics, wake_receiver_shapes, with_tx_panicking_closure_rolls_back, + receiver_close_and_save_arms, receiver_offset_pre_yield_is_zero, scheduler_boundary_fires, + scheduler_bounded_catchup, scheduler_leadership_discipline, stream_ordering_equivalence, + sweep_no_stranded_rows, trim_to_semantics, wake_receiver_shapes, + with_tx_panicking_closure_rolls_back, }; use super::MemFactory; @@ -118,6 +119,11 @@ mod rows { receiver_close_and_save_arms(&factory()).await; } + #[tokio::test(flavor = "current_thread")] + async fn row_receiver_offset_pre_yield_is_zero() { + receiver_offset_pre_yield_is_zero(&factory()).await; + } + #[tokio::test(flavor = "current_thread")] async fn row_job_handle_validity_predicate() { job_handle_validity_predicate(&factory()).await; diff --git a/alkstore-postgres/tests/contract_suite.rs b/alkstore-postgres/tests/contract_suite.rs index f6fd9a9..90f754f 100644 --- a/alkstore-postgres/tests/contract_suite.rs +++ b/alkstore-postgres/tests/contract_suite.rs @@ -170,9 +170,10 @@ mod rows { name_validation_rejects_empty_and_reserved, outbox_enqueue_tx_commit_atomicity, payload_round_trip_stores_exact_encoding, payload_too_large_produced_on_pg, publish_with_key_tx_commit_atomicity, queue_depth_reclaim_and_dead_letter, - receiver_close_and_save_arms, scheduler_boundary_fires, scheduler_bounded_catchup, - scheduler_leadership_discipline, stream_ordering_equivalence, sweep_no_stranded_rows, - trim_to_semantics, wake_receiver_shapes, with_tx_panicking_closure_rolls_back, + receiver_close_and_save_arms, receiver_offset_pre_yield_is_zero, scheduler_boundary_fires, + scheduler_bounded_catchup, scheduler_leadership_discipline, stream_ordering_equivalence, + sweep_no_stranded_rows, trim_to_semantics, wake_receiver_shapes, + with_tx_panicking_closure_rolls_back, }; use super::PgFactory; @@ -253,6 +254,11 @@ mod rows { receiver_close_and_save_arms, "row-receiver-arms" ); + harness_row!( + row_receiver_offset_pre_yield_is_zero, + receiver_offset_pre_yield_is_zero, + "row-receiver-offset-preyield" + ); harness_row!( row_job_handle_validity_predicate, job_handle_validity_predicate, diff --git a/alkstore-sqlite/tests/contract_suite.rs b/alkstore-sqlite/tests/contract_suite.rs index bd3ed6c..0f3a5d3 100644 --- a/alkstore-sqlite/tests/contract_suite.rs +++ b/alkstore-sqlite/tests/contract_suite.rs @@ -74,9 +74,10 @@ mod rows { name_validation_rejects_empty_and_reserved, outbox_enqueue_tx_commit_atomicity, payload_round_trip_stores_exact_encoding, payload_too_large_never_produced_on_sqlite, publish_with_key_tx_commit_atomicity, queue_depth_reclaim_and_dead_letter, - receiver_close_and_save_arms, scheduler_boundary_fires, scheduler_bounded_catchup, - scheduler_leadership_discipline, stream_ordering_equivalence, sweep_no_stranded_rows, - trim_to_semantics, wake_receiver_shapes, with_tx_panicking_closure_rolls_back, + receiver_close_and_save_arms, receiver_offset_pre_yield_is_zero, scheduler_boundary_fires, + scheduler_bounded_catchup, scheduler_leadership_discipline, stream_ordering_equivalence, + sweep_no_stranded_rows, trim_to_semantics, wake_receiver_shapes, + with_tx_panicking_closure_rolls_back, }; use super::SqliteFactory; @@ -145,6 +146,11 @@ mod rows { receiver_close_and_save_arms(&factory("row-receiver-arms")).await; } + #[tokio::test(flavor = "multi_thread")] + async fn row_receiver_offset_pre_yield_is_zero() { + receiver_offset_pre_yield_is_zero(&factory("row-receiver-offset-preyield")).await; + } + #[tokio::test(flavor = "multi_thread")] async fn row_job_handle_validity_predicate() { job_handle_validity_predicate(&factory("row-handle-predicate")).await; diff --git a/alkstore/src/event_receiver.rs b/alkstore/src/event_receiver.rs index 309d62c..98f9c3a 100644 --- a/alkstore/src/event_receiver.rs +++ b/alkstore/src/event_receiver.rs @@ -53,6 +53,10 @@ pub trait EventReceiver: Send { /// The receiver's current offset (the last-yielded event's /// offset), used when a consumer wants to interleave the direct - /// save form with the receiver's position. + /// save form with the receiver's position. Before any event has + /// yielded it reads 0 — the no-yield sentinel, not the consumer's + /// stored checkpoint (the checkpoint gates the feed's start; the + /// first `recv`/`try_recv` observation is the first move; + /// annotated 2026-10-11, review-004 item 12). fn offset(&self) -> i64; } diff --git a/docs/architecture/core-contract.md b/docs/architecture/core-contract.md index 07c8434..fddd635 100644 --- a/docs/architecture/core-contract.md +++ b/docs/architecture/core-contract.md @@ -5,7 +5,8 @@ publish→wake ordering tolerance recorded; ADR-023 §2's `heartbeat(extend)`/`save_offset` classifications; `EventReceiver::try_recv`'s closed shape; `get_job`'s id-global prose — then wave-8 gate: flipped stable with the close-out pass's suite legs -landed; the contract text freezes at the gate, ADR-017 §2)" +landed; the receiver `offset()` pre-yield pin, review-004 item 12; +the contract text freezes at the gate, ADR-017 §2)" --- # Core contract @@ -364,7 +365,15 @@ business-tx shape). Depth pinned by receiver's engine-side trigger is engine-internal, but events never require polling to become visible (the queues row's pg re-poll safety net is an admission of LISTEN loss, not the - posture). + posture). The receiver's `offset()` reads 0 before any event + yields *(annotated 2026-10-11, review-004 item 12's named gap)*: + the pre-yield value is the no-yield sentinel, not the consumer's + stored checkpoint — the saved checkpoint gates the feed's + attach-read start, while the receiver's offset tracks the + last-yielded event only, so the pre-yield `save_offset()` no-op + (stored checkpoint untouched) and the 0 sentinel compose. Events + the attach read prefetches sit in the receiver's feed unobserved; + the first `recv`/`try_recv` observation is the first move. ### queues @@ -838,6 +847,16 @@ before the engine specs are called `stable`: cadence (config-surface accounting — wall-clock cadence measurements stay out of the contract suite's deterministic posture). +- **Receiver `offset()` pre-yield initial value on all three + engines** (the 2026-10-11 general review's item 12, the named + gap) — `offset()` reads 0 before any yield for a fresh consumer, a + consumer with a stored checkpoint, and a consumer with a + negative-seed checkpoint (the ADR-023 §2 totality arm) — the + no-yield sentinel, never the stored checkpoint; the first + `recv`/`try_recv` observation is the first move. Pinned in the + streams row above and verified in + `receiver_offset_pre_yield_is_zero`, green on all three columns + (2026-10-11). ## Design Decisions diff --git a/tasks/core-pin-offset-initial-value.md b/tasks/core-pin-offset-initial-value.md index fc430f6..eda588f 100644 --- a/tasks/core-pin-offset-initial-value.md +++ b/tasks/core-pin-offset-initial-value.md @@ -1,7 +1,7 @@ --- id: core-pin-offset-initial-value name: Verify and pin EventReceiver::offset()'s pre-yield value (review 004 item 12) -status: pending +status: completed depends_on: [] scope: narrow risk: low @@ -38,14 +38,14 @@ conversation, not a doc edit. ## Acceptance Criteria -- [ ] The three engines' pre-yield `offset()` values verified equal by +- [x] The three engines' pre-yield `offset()` values verified equal by live runs (the probe/leg recorded; green on all three columns — pg against the harness server) -- [ ] core-contract.md's `EventReceiver::offset()` text pins the +- [x] core-contract.md's `EventReceiver::offset()` text pins the pre-yield return with a dated annotation - [ ] If divergent instead: the divergence recorded and raised with the user (this AC replaces the doc pin, not supplements it) -- [ ] Doc gate green; any new suite leg green on all three columns +- [x] Doc gate green; any new suite leg green on all three columns ## References @@ -58,8 +58,59 @@ conversation, not a doc edit. ## Notes -> To be filled by implementation agent +- **The engines were equal — the doc-pin branch applies, not the + divergence branch.** Read first (all three `offset()` bodies are + `self.position`, and all three constructors initialize + `position: 0` unconditionally — mem + `alkstore-mem/src/stream.rs:353`, sqlite + `alkstore-sqlite/src/stream.rs:399`, pg + `alkstore-postgres/src/stream.rs:620`), then verified live by the + new suite leg on all three columns: 0 on every pre-yield arm + (fresh, positive-checkpoint, negative-seed), no divergence to + raise. +- **Probe home: the contract suite** (the task's first choice) — a + new row `receiver_offset_pre_yield_is_zero` in + `alkstore-contract-suite/src/properties.rs`, wired into all three + engines' `tests/contract_suite.rs` executors. Four arms: fresh + consumer, consumer with a stored positive checkpoint, consumer + with a stored negative checkpoint (the ADR-023 §2 totality seed — + the arm a checkpoint-seeded realization would surface on), and a + first-observation composition leg (the attach read prefetches + unobserved; the first `recv` moves `offset()` to the last-yielded + offset). Stamp per the `version_stamp` convention: ADR-008 §8's + `EventReceiver` shape + the core-contract.md pin (no ADR owns this + property's pre-yield arm — the review item is the pin's origin, so + the backlog row is the cited pin). +- **Doc pin location**: the task said "core-contract.md's + `EventReceiver::offset()` paragraph" — no such standalone paragraph + exists; the receiver's contract text lives in the streams/ + `subscribe(consumer)` bullet (ADR-008 §8 pins only the shape + comment "the receiver's current offset"). The pin landed there + (dated annotation), *and* on `offset()`'s own trait doc in + `alkstore/src/event_receiver.rs` (core's doc comments are contract + text per AGENTS.md; dated the same). ADR-008 §8's shape comment was + deliberately left untouched — a doc-only verification task takes no + ADR amendment. +- **Verification-backlog bullet added** (core-contract.md), matching + the section's evolved role: the new bullet records the verified pin + with the row's name and the all-three-columns result, same posture + as the review-004 suite legs before it. +- Frontmatter `last_updated` extended with the pin (dated), keeping + the freeze note intact. ## Summary -> To be filled on completion \ No newline at end of file +The pre-yield `offset()` question closed: all three engines return 0 +before any yield regardless of stored checkpoint (positive, negative, +or absent) — the no-yield sentinel, composing with the pinned +pre-yield `save_offset()` no-op; the first `recv`/`try_recv` +observation is the first move. Pinned in three places: the contract +text (core-contract.md streams row + verification-backlog bullet, +dated 2026-10-11), the core trait doc (`event_receiver.rs::offset()`), +and the suite (new stamped row `receiver_offset_pre_yield_is_zero` on +`alkstore-contract-suite`). Verified: the new row green on all three +columns (pg against the harness server `pglo-poc` :15432), full pg +column green (135+26+9), workspace tests green server-less, clippy `-D +warnings`, `cargo fmt --check`, doc gate zero warnings, fuzz corpus +replay 6/6, wasm32 mem check green. Contract-observation only — no +engine code changed, no ADR amendment. \ No newline at end of file