Modal replay: at most two simulations across invocations

docs/uk_replay/RECIPE.md

@@ -598,10 +598,51 @@ fields and head effects. `--allow-changed-existing` permits replacement only
 after that report has been reviewed; original bytes remain in the backup.
 `--allow-partial` permits read-only inspection of a focused download, but
 partial or noncanonical outputs cannot be adopted. Keep raw receipts for
-provenance. Each Modal invocation uses one replay worker. Count every
-active invocation and local simulation toward the overall maximum of two;
-separate invocations do not share a global concurrency gate. A full event
-plus one focused repeat uses both slots. Remote wall time is recorded
+provenance. Each Modal invocation uses one replay worker and first takes one of two
+simulation slots in the Modal Dict `scorecard-replay-simulation-slots`
+(`modal_uk_event.SimulationSlots`), waiting while both are held, so Modal
+invocations never run more than two simulations at once. How the slots hold:
+
+* A slot has one chain of claims per calendar day,
+  `claim-{slot}-{day}-{generation}`. A slot changes hands only through
+  `put(..., skip_if_exists=True)`, Modal's atomic create-if-absent: a caller
+  creates a chain's next generation only when its newest one is released or
+  lapsed. Nothing is deleted, there is no pointer that a late write could
+  roll back, and a holder writes only its own claims, to release or shorten
+  them. A lease that crosses midnight holds a claim in both days' chains.
+* A day's chain matters for at most a day plus a lease, far inside the 7 days
+  after which Modal expires an idle entry, so no claim that still matters
+  can have expired, and a write that arrives days late lands in a chain that
+  no longer governs anything. The guarantee needs no assumption about how
+  long a step stalls.
+* Leases run on Modal's clock: each invocation measures its offset from
+  Modal with a small remote function, checks it again after waiting for a
+  slot (a drift over 30 seconds stops the run, exit 75), and takes over a
+  lapsed claim only 2 minutes after its expiry.
+* The lease is 4 hours. The remote function refuses to start unless its
+  whole 3-hour timeout plus a 10-minute margin fits inside it, so a run
+  ends before its slot can pass on, even if the client dies.
+* A finished or never-started run frees its slot at once. When `app.run()`
+  exits after ctrl-C, Modal's client has already asked the server to stop
+  the app's tasks, and the slot frees 10 minutes later. Anything else after
+  the run started (a lost connection, which Modal's runner re-raises
+  without that request; a remote error; a failed stop request; a client
+  killed outright) leaves the claim until the lease lapses. A failed
+  release never costs a returned result: it is downloaded and the claim
+  lapses.
+* The slot is taken with the app already open, after the image build, so a
+  build never eats into a lease; an invocation waits for a slot (polling
+  every 30 seconds, in no set order) with its app open and idle.
+* `tests/test_modal_uk_event.py` checks this call by call: Hypothesis
+  interleaves several holders' Dict calls, each on its own clock within the
+  enforced drift, with clock jumps of any size at any point, midnight
+  crossings, crashes, interrupts, lost connections and Modal's 7-day expiry,
+  and asserts that no two runs overlap on a slot and that both slots can be
+  taken once every lease has lapsed.
+
+Local simulations are not in that lease: count them yourself toward the
+overall maximum of two. A full event plus one focused repeat uses both
+slots. Remote wall time is recorded
 separately in `MODAL_RECEIPT.json`; use the completed event's observed timings
 when planning the next lane.