Add config recovery duplicate dedup coverage

Author: lemon-mint

EPAXOS.MD

@@ -111,7 +111,7 @@ On restart, `NewRawNode` loads durable records, remembers any stored historical
 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, newly added voters cannot count for pre-addition instances, and current-configuration proposals from a removed local replica remain rejected.
 
-The finite configuration evidence currently covers an executed add/remove durable replay slice plus staged old-instance recovery-after-removal and recovery-after-addition slices. Arbitrary durable histories, arbitrary 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 staged old-instance recovery-after-removal, lost+duplicate recovery response de-duplication, and recovery-after-addition slices. Arbitrary durable histories, arbitrary recovery under reconfiguration, retries/timer rebroadcast, arbitrary message loss, joint consensus, and unbounded membership changes remain outside the current claim.
 
 ## Ready contract
 

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -330,15 +330,16 @@ 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.
+- `tla/EPaxosConfigRecoveryDedup.tla` checks a finite staged de-duplication case for that removal recovery path: one lost prepare/accept response and one duplicate prepare/accept response leave the old quorum below 3/4, and a distinct removed-voter response is still required. The matching Go regression keeps the recovered no-op out of application output.
 - `tla/EPaxosConfigAddRecovery.tla` checks the complementary finite staged add case where the current config is `{1,2,3,4}`, the old instance remains pinned to `{1,2,3}`, added voter 4 attempts prepare/accept responses without entering the old quorum sets, the old 2/3 quorum is sufficient even though the current quorum would be 3/4, and the recovered no-op executes.
 
 Open limitation:
 
-- 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, one staged old-instance recovery-after-removal slice, and one staged old-instance recovery-after-addition 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.
+- 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, one staged old-instance recovery-after-removal slice, one staged lost+duplicate recovery response de-duplication slice, and one staged old-instance recovery-after-addition slice. They do not cover arbitrary/multi-step reconfiguration chains, joint consensus, arbitrary recovery under configuration changes, arbitrary durable histories, retries/timer rebroadcast, arbitrary message loss, or unbounded configuration histories.
 
-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`.
+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`, `tla/EPaxosConfigRecoveryDedup.tla`.
 
-Additional source anchors for finite add-recovery coverage: `tla/EPaxosConfigAddRecovery.tla`, `tla/EPaxosConfigAddRecovery.cfg`.
+Additional source anchors for finite add/de-dup recovery coverage: `tla/EPaxosConfigAddRecovery.tla`, `tla/EPaxosConfigAddRecovery.cfg`, `tla/EPaxosConfigRecoveryDedup.cfg`.
 
 ## 15. Property-by-property rationale
 
@@ -475,6 +476,7 @@ Evidence: `examples/kv/cmd/kvnode/main.go`, `examples/kv/cmd/kvnode/main_test.go
 | `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/EPaxosConfigRecoveryDedup.tla` | One finite staged lost+duplicate response de-duplication slice where an old four-voter instance recovery remains below old quorum after one lost response and a duplicate voter-3 response, then advances only after distinct removed voter 4 answers. | Retries, timer rebroadcast, arbitrary recovery under configuration changes, joint consensus, arbitrary message loss, arbitrary membership histories, application output, and unbounded proof. |
 | `tla/EPaxosConfigAddRecovery.tla` | One finite staged recovery-after-addition slice where an old three-voter instance is recovered after the current config adds voter 4; added-voter prepare/accept attempts do not enter old quorum sets, old 2/3 quorum is sufficient, and the no-op executes. | 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. |