Model storage fencing and crash durability with StreamData

[jeregrine]

Problem

Example-based tests cover selected durability and ownership scenarios, but do not explore varied sequences of updates, crashes, restarts, and historical-token mutations. A useful generated test needs an independent correctness model: an unsynced update is not a durable acknowledgement, and an old ETag must not become valid again after deletion and recreation.

Fix

Add StreamData as a test-only dependency and two sequential command models against real single-node EKV:

• Object generations: generate claims, reads, conditional writes, and conditional deletes across three keys. The model uses its own logical generations to decide whether opaque historical ETags should succeed, checking all modeled keys after every command. Every sequence includes stale write/delete attempts against a recreated object.
• Acknowledged durability: generate unsynced updates, all three strict-sync callback forms, process kills, explicit restarts, and graceful termination through the DurableServer API. Track memory and durable values separately, disable automatic/periodic persistence, and require each sequence to include a strict acknowledgement followed by a crash. Unacknowledged calls fail the scenario rather than being treated as proof that nothing committed.

Every generated input and shrink attempt gets fresh storage and a supervision tree. Teardown keeps EKV alive until DurableServer stops, then removes the sample's directory. A dedicated cleanup regression deliberately fails one sample and checks that the next starts empty. Fixed registered names are reused only in synchronous properties, avoiding per-input atom allocation.

The properties join the default suite with a budget of 100 sequences each. DURABLE_PROPERTY_RUNS controls longer campaigns; the README explains seed replay, shrinking, resource ownership, and scope.

Supporting information

These models verify sequential, per-key behavior. They do not establish distributed linearizability, external-side-effect fencing, deterministic scheduling, lease-boundary behavior, or recovery from commit-success/response-loss faults. Cordon/delete lifecycle workflows, eventual discovery, resource bounds, and mirror phases need additional models and fault controls.

The models themselves require neither LocalStack nor cloud credentials. Main's global test helper still contacts LocalStack even when selecting only properties; #33 or the alternative isolation implementation in #34 removes that unrelated dependency. This branch does not include either competing fixture-isolation change.

No production behavior changes. StreamData is the only dependency added; existing dependency versions remain unchanged.