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, and the revision chain grew by one per committed put.
• 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.
• Durability under churn — every acked unique-key write is still readable.
• Liveness — the run made progress and every writer finished.

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

Structs

FinalContended

The final observed state of one contended key.

FinalUnique

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

OpRecord

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

SoakStats

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

Enums

OpResult

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

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.