RenewLease now demands current durable authority, AttemptExecuting, and a
non-terminal phase so a live lease cannot be extended after authority loss.
Align the mutable API renew prose with that precondition.
Move API artifacts out of docs/spec, define concrete execution and deletion refinements, and document TLA+ abstraction boundaries so architecture prose cannot become a competing protocol specification.
Encode zero-orphan intent as EventuallyNonWinnerStagingCleaned and
EventuallySystemQuiescent under recovery. Stop authorized attempts on
FinalizeCancel and do not re-publish cancel notices after terminal so fair
behaviors can reach SystemQuiescent (TLC-checked on Remora.cfg).
Clarify the deadlock sink is not a product SLO: residual staging and coord
cleanup are best-effort GC, while safety remains CommittedResult and
StagingOwnership.
Drop LiveProgressAligned in favor of well-formedness and lease-compatible
progress, stop durable CAS from clearing Redis progress, and add ambient
ClearStaleLiveProgress so TLC matches Postgres + Dragonfly separation.
Replace tautological invariants with non-trivial ones, allow multi-shot
coordination loss and re-partition, fix reap/progress lifecycle, enable
deadlock checking via Done, and add stress and multi-shot TLC configs.
