core: verify and pin the receiver's pre-yield offset() value (review 004 item 12, core-pin-offset-initial-value) — the three engines verified equal live, so the doc-pin branch applies: offset() reads 0 before any yield on every receiver — fresh consumer, stored positive checkpoint, stored negative seed (ADR-023 §2's totality arm, the one a checkpoint-seeded realization would surface on) — 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, composing with the pinned pre-yield save_offset() no-op; the attach read's prefetches sit unobserved and the first recv/try_recv observation is the first move (then the post-yield value, receiver_close_and_save_arms' pin). Verified by code read first (all three offset() bodies are self.position, all three constructors seed position: 0 unconditionally — mem stream.rs:353, sqlite :399, pg :620) then live: new suite row receiver_offset_pre_yield_is_zero (alkstore-contract-suite, stamped ADR-008 §8 + the core-contract.md pin, four arms incl. the first-observation composition leg) green on all three columns, pg against the harness server (parked pglo-poc :15432); pinned in three places: core-contract.md streams/subscribe row (dated 2026-10-11 annotation) + a verification-backlog bullet recording the verified pin, the core trait doc on offset() (core's doc comments are contract text), and the suite row itself — ADR-008 §8's shape comment deliberately left untouched (doc-only verification takes no ADR amendment, noted in the task); no engine code changed, no divergence to raise; gates green: workspace build/tests server-less, full pg column vs harness (135+26+9), clippy -D warnings, fmt --check, doc gate zero warnings, fuzz corpus replay 6/6, wasm32 mem check, taskgraph validate (96); task -> completed

This commit is contained in:
glm-5.3-flash committed 2026-10-11 14:34:15 +00:00
1 parent 321f579ac2
commit 9301bb926b
8 files changed
+196 -21

No files matched your search

+4 -3
View File
@@ -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,
};
+82
View File
@@ -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
+9 -3
View File
@@ -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;
+9 -3
View File
@@ -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,
+9 -3
View File
@@ -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;
+5 -1
View File
@@ -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;
}
+21 -2
View File
@@ -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
+57 -6
View File
@@ -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
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.