[calvin-archastro]

Replaces #48 (replayed onto main after #47; conflicts in package.json, README, model.yml resolved by keeping both).

Merge order: independent of #47. The Actions wake-up model that builds on this contract is a separate PR stacked on #47 (it merges after both). Expect a trivial conflict in verify/package.json, verify/README.md and model.yml between this and #47: both add scripts and rows next to each other.

What

pail events v2. Design: a bucket notification is only a hint; truth is re-reading the key. Consumers are idempotent, delivery is at-least-once, a dropped notification costs latency, never correctness.

1. --cursor FILE | bucket:AREA/KEY: on start, diff every watched key against the saved heads (deletions too), emit with "source":"resume", then stream. The cursor moves only after the line is out. File cursor: temp file, fsync, rename. Bucket cursor: CAS, and a second consumer on it fails loudly.
2. --safety-poll SECS (default 60, 0 off): with Pub/Sub, also re-list everything. Polling already re-lists every --interval-ms.
3. --prefix AREA/PREFIX: object events {key, version, old, op: put|delete, source, at} for the sibling area <repo>.AREA/ (--prefix actions/ = <repo>.actions/). Same nudge-then-re-list rule, same cursor. Pub/Sub messages for the area are hints too. The cursor object in the area is never an event.
4. Formal model verify/events/ (in a subdirectory: the digest of the other generated artifacts is untouched) and a refinement of the real events::Watcher against it.
5. pail-ci keeps a cursor (default per store under $XDG_STATE_HOME), so a restart builds what landed while it was down. Docs, --help, README updated.

Model and refinement

• Properties: noLoss (up, quiescent, one scan later: emitted state == store), cursorBehindOut (never skip), intentRecorded, noRedundant; in the sim noPhantom, perKeyOrder, cursorMonotone.
• Environment: writers put/remove; notifications dropped, repeated, reordered; consumer crashes between any two steps and restarts from its cursor.
• Refinement (tests/events_refinement.rs, 8 scenarios x 2 modes): the harness holds the notifications and drops the watcher to crash it, and drives the real Watcher::{open, observe, scan, mark, emit, save} over file://. Compared after every step: the store, the cursor read back from its file or bucket object, the watcher's beliefs, the lines written. Refs with a cursor file, and sibling-area objects with a bucket cursor.
• Not vacuous: 8 mutants of events.rs (no mark, dirty not unsure, cursor before line, no dedupe, Unsure == anything, no deletions in scan, mark not cleared, memory not updated) each fail a scenario.

What the model found

• The first pail events was two of the model's mutants: a restart seeded its memory from the store (events during downtime lost) and with Pub/Sub nothing re-listed (a lost notification lost the event).
• A hole in the first cursor design: line out, crash before the cursor moves, then the key is deleted (or a ref reset to the commit the cursor holds). The restart sees store == cursor, emits nothing, and the readers never learn of the deletion. Fixed with a write-ahead mark: the cursor records the intent to emit a key before the line, so a restarted consumer is unsure of it and emits what is there.

Verification

• cargo fmt --check, cargo test --release (all): pass. (cargo clippy is not in CI; the repo has pre-existing warnings, none in the new code.)
• verify: npm run check, npm test, witness:events, simulate:events (100k runs), mutate:events: pass. All six switches are caught (table in verify/README.md).
• Long runs are in .github/workflows/model.yml (manual), not ci.yml.
• Not tested against a real Pub/Sub or the GCS emulator: the Pub/Sub response parsing is a unit test, hints are injected (Source::Hints) in the loop tests, and stores are file://. No cloud resources were created.

Flags

--prefix, --cursor, --safety-poll. --cursor conflicts with --initial. Without --cursor behaviour is as before (a restart takes the present state as seen).

🤖 Generated with Claude Code