Add finite config recovery coverage

Author: lemon-mint

EPAXOS.MD

@@ -109,8 +109,9 @@ User commands are emitted to the embedding application through `Ready.Committed`
 On restart, `NewRawNode` loads durable records, remembers any stored historical configurations, then replays executed configuration-change records in instance order to rebuild intermediate configuration ids that are needed by old in-flight instances. Replay rejects a stored configuration id whose voters conflict with the voters deterministically produced by executed configuration commands. A replayed unexecuted configuration command remains a pending barrier, so the restarted node still rejects new local proposals until that command executes.
 
 When TOQ is enabled, default `TOQSyncGroup` selection and one-way-delay validation run after executed configuration replay, so an omitted sync group defaults to the replayed current voters and an explicit stale sync group containing a removed voter is rejected.
+Recovery, retry, and broadcast paths select voter sets and slow-quorum thresholds by the instance `Ref.Conf`, so an old instance can still use a removed voter for its old pinned quorum while current-configuration proposals from that removed local replica remain rejected.
 
-The finite replay evidence currently covers an executed add/remove history plus stored-configuration conflict rejection. Arbitrary durable histories, recovery under reconfiguration, joint consensus, and unbounded membership changes remain outside the current claim.
+The finite configuration evidence currently covers an executed add/remove durable replay slice plus one staged old-instance recovery-after-removal slice. Arbitrary durable histories, arbitrary recovery under reconfiguration, joint consensus, and unbounded membership changes remain outside the current claim.
 
 ## Ready contract
 

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -329,12 +329,13 @@ Why this is safe inside the bounded claim:
 Finite replay coverage:
 
 - `NewRawNode` loads durable instance records, remembers stored configuration states, replays executed configuration-change records in instance order, reconstructs intermediate `ConfID` domains needed by old in-flight records, and rejects a stored historical `ConfID` if its voters conflict with the voters deterministically produced by replayed commands. A replayed unexecuted configuration command remains a proposal barrier. TOQ configuration is validated after replay, so the default sync group uses the replayed current voters and explicit stale sync groups fail closed.
+- Recovery for an old pinned instance uses `Ref.Conf` to choose prepare/accept voters and slow-quorum thresholds. `tla/EPaxosConfigRecovery.tla` checks a finite staged removal case where the current config is `{1,2,3}`, the old instance remains pinned to `{1,2,3,4}`, removed voter 4 counts only for the old prepare/accept quorum, the smaller current quorum is insufficient for that old instance, and removed-voter current-config proposals are rejected.
 
 Open limitation:
 
-- The current formal models cover a finite local barrier, one add-voter transition, one remove-voter transition, one add-then-remove chain, and one durable restart-replay slice. They do not cover arbitrary/multi-step reconfiguration chains, joint consensus, recovery under configuration changes, arbitrary durable histories, or unbounded configuration histories.
+- The current formal models cover a finite local barrier, one add-voter transition, one remove-voter transition, one add-then-remove chain, one durable restart-replay slice, and one staged old-instance recovery-after-removal slice. They do not cover arbitrary/multi-step reconfiguration chains, joint consensus, arbitrary recovery under configuration changes, arbitrary durable histories, message loss, or unbounded configuration histories.
 
-Source anchors: `epaxos/node.go` (`NewRawNode`, `Propose`, `ProposeConfChange`, `configureTOQ`, `confChangeQuorumFrom`, `markPendingConf`, `refreshPendingConf`, `computeAttrsAt`, `rememberConf`, `replayExecutedConfig`, `replayConfChange`, `applyConfChange`, per-instance quorum/broadcast helpers), `epaxos/config_change_ordering_test.go`, `epaxos/toq_test.go`, `epaxos/sim_test.go`, `tla/EPaxosConfigBarrier.tla`, `tla/EPaxosConfigTransition.tla`, `tla/EPaxosConfigRemoveTransition.tla`, `tla/EPaxosConfigChainTransition.tla`, `tla/EPaxosConfigReplay.tla`.
+Source anchors: `epaxos/node.go` (`NewRawNode`, `Propose`, `ProposeConfChange`, `configureTOQ`, `confChangeQuorumFrom`, `confFor`, `votersForConf`, `slowQuorumForConf`, `broadcast`, `startPrepare`, `handlePrepareResp`, `startAccept`, `handleAcceptResp`, `markPendingConf`, `refreshPendingConf`, `computeAttrsAt`, `rememberConf`, `replayExecutedConfig`, `replayConfChange`, `applyConfChange`, per-instance quorum/broadcast helpers), `epaxos/config_change_ordering_test.go`, `epaxos/toq_test.go`, `epaxos/sim_test.go`, `epaxos/recovery_test.go`, `tla/EPaxosConfigBarrier.tla`, `tla/EPaxosConfigTransition.tla`, `tla/EPaxosConfigRemoveTransition.tla`, `tla/EPaxosConfigChainTransition.tla`, `tla/EPaxosConfigReplay.tla`, `tla/EPaxosConfigRecovery.tla`.
 
 ## 15. Property-by-property rationale
 
@@ -470,6 +471,7 @@ Evidence: `examples/kv/cmd/kvnode/main.go`, `examples/kv/cmd/kvnode/main_test.go
 | `tla/EPaxosConfigTransition.tla` | One finite add-voter transition and config pinning. | Multi-step, joint consensus, recovery during config change. |
 | `tla/EPaxosConfigRemoveTransition.tla` | One finite remove-voter transition where an old in-flight instance remains pinned to old voters/quorum and a later instance excludes the removed voter. | Multi-step, joint consensus, recovery during config change. |
 | `tla/EPaxosConfigChainTransition.tla` | One finite add-then-remove chain where old and mid-flight instances remain pinned across two config changes. | Arbitrary multi-step, joint consensus, recovery during config change. |
+| `tla/EPaxosConfigRecovery.tla` | One finite staged recovery-under-removal slice where an old four-voter instance is recovered after the current config removes voter 4; prepare/accept quorums use the old slow quorum, count the removed voter only for that old instance, and reject removed-voter new-config proposals. | Arbitrary recovery under configuration changes, joint consensus, message loss, arbitrary membership histories, and unbounded proof. |
 | `tla/EPaxosRevisited.tla` | TOQ envelope, delayed assignment, pending-decision blocking, receiver processing, fast-wait behavior, and chain pruning. | Real clock synchronization and OWD measurement. |
 | `tla/TOQClockDiscipline.tla` | Finite bounded-skew/bounded-delay `ProcessAt` contract; in Go this maps to `TOQOneWayDelay` values that already include skew margin. | Operational clock-sync implementation or delay measurement. |
 | `tla/ReadyAdvance.tla` | Durable Ready/Advance prefix acknowledgement and retry. | Concrete storage engine behavior. |