Module oracle 

The soak safety/liveness oracle.

Given the recorded outcome of every write op plus a final read of every key, check asserts the invariants a correct conditional-write store must hold under concurrent multi-replica load and replica-kill chaos:

• No lost update — every committed op-id on a contended key survives in that key’s final record, exactly once.
• Conflicts surface — racing writers observed Conflict (never a silent overwrite). Zero observed conflicts means the invariant was never actually exercised, which is itself a failure. The same holds for deletes racing edits: zero delete conflicts is a failure.
• One commit per base — on a lifecycle key, two edits never both commit on the same base revision, and an edit never commits on the same base as a delete that actually wrote a tombstone there. A delete acknowledged without evidence that it wrote (a no-op over a later tombstone, or a raced evidence read) is ambiguous and skipped, never flagged.
• Durability under churn — every acked unique-key write is still readable, and every acked delete still reads as a tombstone (no resurrection).
• Replicas agree on deletion (#203) — once the writers have stopped and every replica is live again, each lifecycle key is live on every replica or a tombstone on every replica (never a mix), every replica reports the same raw revision, each replica’s consumer read agrees with its own raw read on whether the key is live, and a key that had committed writes is never physically absent.
• Liveness — the run made progress and every writer finished.

What “replicas agree” means here. The HA soak’s replicas are gonzalod processes over one shared bucket, so no replica holds its own copy. In that topology the agreement check catches daemon read-path bugs (caching, raw reads routed to consumer reads, tombstone filtering), not storage replication, which the sync and git-pull tests cover. The check itself is topology-agnostic: it compares per-replica views and would apply unchanged to independent stores that had been synced.

Per-replica agreement is checked for the life-* keys; deleted unique keys are checked through one replica, because they use the same read path.

This is a targeted invariant oracle, not a linearizability checker: it asserts on set membership / agreement / completion, never on exact interleavings, so normal scheduling jitter cannot flake it.

Structs

FinalContended

The final observed state of one contended key.

FinalLifecycle

The final per-replica state of one lifecycle key, in replica order.

FinalUnique

The final observed state of one unique (uncontended) key.

LifecycleRecord

One recorded lifecycle op.

OpRecord

One recorded write against a contended key: the unique op-id and its result.

ReplicaView

One replica’s view of a lifecycle key after settling.

SoakStats

Everything the oracle needs: op outcomes, final reads, and writer completion.

Enums

LifecycleOp

A lifecycle op against a life-* key: the delete/recreate stream (#203).

LifecycleResult

The outcome of one lifecycle op. Lifecycle ops are not retried: a lost race is recorded as Conflict and the writer moves on.

OpResult

The result of a single conditional-write op, as observed by the driver.

RawState

What one replica’s raw read (get_raw) returned for a key after settling. Revisions are rendered as "<counter>:<hash>" so the oracle stays pure.

Violation

A violated invariant. An empty check result means the soak passed.

Functions

check

Check every soak invariant. Returns the (possibly empty) set of violations.

delete_conflicts

Delete ops that lost a race (Conflict). Edit and recreate conflicts don’t count.