[paymog]

Summary

A job that retry gives up on is no longer silently completed. The runner now keeps it as a dead ticket, with its payload and the reason (WhySpent, WhyLate, WhyUnsafe), so a caller can tell a delivered job from an abandoned one and replay it later with revive.

What changes for callers

• R.dead(A, s) lists the dead tickets of a State, newest first.
• R.revive(~A, ~penc, r, id, deadline) makes a dead ticket pending again with a new retry budget.
• R.cancel now also drops a dead ticket.
• A Settled attempt still completes. Retry.Settled covers both a success and a failure that another try would repeat, so the runner cannot tell them apart. The README says so under Trust boundary.

This is a breaking change to State (a third field) and Op (two new records, tags 8 and 9), so runner rises to 0.6.0.0. No sibling imports runner.

Laws

• New dead_never_selected: after Abandon{i, why} and any ops with no Revive of i, no Select takes i.
• complete_never_selected and recovered_never_selected gain one hypothesis: i is not dead, as a running ticket is not. cancel_never_selected is unchanged; Cancel now clears all three registries.
• requeue_stop ("plan stops ⇒ Complete") is no longer true. settled_complete, unsafe_abandon, and transient_abandon replace it.

The proof generalizes the old gone invariant to inv(i, P, s), where P is a predicate on the dead list. gone uses "i is absent", and the dead law uses "anything". The same per-op helpers serve both.

Verification

• scripts/check.sh runner: PROOF.bend checks every law, and a deliberately wrong dead_never_selected body fails.
• check.bend: a job that fails every attempt ends dead with its payload, keeps it across a reopen, runs 3 more attempts after revive, and cancel drops it. The op and snapshot codecs round-trip Abandon, Revive, and dead tickets.
• bench/run.py 1 12 runs, and all checksums agree.

Closes #444