Add mid-chain recovery retry coverage

Author: lemon-mint

EPAXOS.MD

@@ -117,7 +117,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, a mid-chain instance from `{1,2,3,4}` still needs the old 3/4 quorum after the current config becomes `{1,3,4}`, and current-configuration proposals from a removed local replica remain rejected.
 
-The finite configuration evidence currently covers an executed add/remove durable replay slice, local-owner old-config PreAccept/Accept response de-duplication with the owner vote counted separately from remote responses, retry-timer rebroadcast after removal/addition, mid-chain recovery after an add-then-remove history, staged old-instance recovery-after-removal, lost+duplicate recovery response de-duplication, recovery-after-addition, old-config prepare/accept recovery retry-timer slices, and an explicit finite old-config lost-response-before-retry recovery slice. Arbitrary durable histories, arbitrary recovery under reconfiguration, arbitrary retry histories, arbitrary message loss beyond that named finite pre-retry loss shape, joint consensus, and unbounded membership changes remain outside the current claim.
+The finite configuration evidence currently covers an executed add/remove durable replay slice, local-owner old-config PreAccept/Accept response de-duplication with the owner vote counted separately from remote responses, retry-timer rebroadcast after removal/addition, mid-chain recovery after an add-then-remove history, staged old-instance recovery-after-removal, lost+duplicate recovery response de-duplication, recovery-after-addition, old-config prepare/accept recovery retry-timer slices, an explicit finite old-config lost-response-before-retry recovery slice, and an explicit finite mid-chain lost-response-before-retry recovery slice. Arbitrary durable histories, arbitrary recovery under reconfiguration, arbitrary retry histories, arbitrary message loss beyond that named finite pre-retry loss shape, joint consensus, and unbounded membership changes remain outside the current claim.
 
 ## Ready contract
 

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -345,12 +345,13 @@ Finite replay coverage:
 - `tla/EPaxosConfigChainRecovery.tla` checks a finite mid-chain recovery case after `{1,2,3}` adds voter 4 and then removes voter 2: an instance pinned to Conf2 `{1,2,3,4}` remains in prepare/accept when only current Conf3 quorum responses are present, advances when removed voter 2 supplies the modeled third old-quorum vote, and rejects removed-voter new-config proposals. The matching Go regression is `TestOldConfigRecoveryUsesPinnedMidChainVotersAfterAddThenRemove`.
 - `tla/EPaxosConfigRecoveryRetry.tla` checks finite logical prepare/accept retry rebroadcasts for both removal and addition recovery slices: old peers and old dependency widths are retained, the removed old voter remains a retry target for old removal instances, the added current voter is excluded for old pre-addition instances, and pure retries have no durable/application effects.
 - `tla/EPaxosConfigRecoveryLostResponseRetry.tla` checks one finite explicit old-config lost-response-before-retry recovery slice: removed-voter prepare and accept responses are not counted before deterministic retry rebroadcast, retries stay pinned to old peers and old dependency width, and replacement responses after retry complete recovery through the old 3/4 quorum. This is separate from `EPaxosConfigRecoveryRetry` and does not claim arbitrary message-loss retry behavior.
+- `tla/EPaxosConfigChainRecoveryLostResponseRetry.tla` checks one finite mid-chain lost-response-before-retry recovery slice: after `{1,2,3}` adds voter 4 and then removes voter 2, current Conf3 quorum responses from local 1 plus voter 4 remain below the Conf2 quorum, deterministic retries stay pinned to Conf2 peers `{2,3,4}` and width-4 dependencies, removed-voter prepare and accept responses are explicit pre-retry losses, and replacement responses complete the Conf2 3/4 quorum. The matching Go regression is `TestOldConfigChainRecoveryRetryCompletesAfterLostPreRetryResponses`.
 - `tla/EPaxosConfigTransitionRetry.tla` checks finite logical PreAccept/Accept retry rebroadcasts for normal local-owner old instances after both removal and addition transitions: old peers and old dependency widths are retained, the removed old voter remains a retry target for old removal instances, the added current voter is excluded for old pre-addition instances, and pure retries have no durable/application effects.
 - `tla/EPaxosConfigTransitionDedup.tla` checks finite response de-duplication for normal local-owner old instances after removal and addition transitions: the local owner vote is counted separately from remote responses, duplicate old-voter PreAccept/Accept responses do not advance below old quorum, added current voters are excluded for pre-addition instances, and the modeled second distinct old remote response advances only at old quorum.
 
 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 mid-chain recovery slice after that chain, one durable restart-replay slice, one normal old-config transition response de-duplication slice, one normal old-config transition retry-timer slice, one staged old-instance recovery-after-removal slice, one staged lost+duplicate recovery response de-duplication slice, one staged old-instance recovery-after-addition slice, one finite old-config recovery retry-timer slice, and one explicit finite old-config lost-response-before-retry recovery slice. They do not cover arbitrary/multi-step reconfiguration chains, joint consensus, arbitrary recovery under configuration changes, arbitrary durable histories, arbitrary retry/timer histories, arbitrary message loss beyond the named finite pre-retry loss slice, 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 mid-chain recovery slice after that chain, one durable restart-replay slice, one normal old-config transition response de-duplication slice, one normal old-config transition retry-timer slice, one staged old-instance recovery-after-removal slice, one staged lost+duplicate recovery response de-duplication slice, one staged old-instance recovery-after-addition slice, one finite old-config recovery retry-timer slice, one explicit finite old-config lost-response-before-retry recovery slice, and one finite mid-chain lost-response-before-retry recovery slice. They do not cover arbitrary/multi-step reconfiguration chains, joint consensus, arbitrary recovery under configuration changes, arbitrary durable histories, arbitrary retry/timer histories, arbitrary message loss beyond the named finite pre-retry loss slices, 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`, `tla/EPaxosConfigRecoveryDedup.tla`.
 
@@ -360,6 +361,7 @@ Additional source anchors for finite config-recovery lost-response retry coverag
 Additional source anchors for finite config-transition retry coverage: `tla/EPaxosConfigTransitionRetry.tla`, `tla/EPaxosConfigTransitionRetry.cfg`, and `epaxos/recovery_test.go` (`TestOldConfigTransitionRetryUsesPinnedVotersAfterRemoval`, `TestOldConfigTransitionRetryUsesPinnedVotersAfterAddition`).
 Additional source anchors for finite config-transition response de-duplication coverage: `tla/EPaxosConfigTransitionDedup.tla`, `tla/EPaxosConfigTransitionDedup.cfg`, and `epaxos/recovery_test.go` (`TestOldConfigTransitionDedupUsesPinnedVotersAfterRemoval`, `TestOldConfigTransitionDedupUsesPinnedVotersAfterAddition`).
 Additional source anchors for finite mid-chain config-recovery coverage: `tla/EPaxosConfigChainRecovery.tla`, `tla/EPaxosConfigChainRecovery.cfg`, and `epaxos/recovery_test.go` (`TestOldConfigRecoveryUsesPinnedMidChainVotersAfterAddThenRemove`).
+Additional source anchors for finite mid-chain config-recovery lost-response retry coverage: `tla/EPaxosConfigChainRecoveryLostResponseRetry.tla`, `tla/EPaxosConfigChainRecoveryLostResponseRetry.cfg`, and `epaxos/recovery_test.go` (`TestOldConfigChainRecoveryRetryCompletesAfterLostPreRetryResponses`).
 
 ## 15. Property-by-property rationale
 
@@ -497,6 +499,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/EPaxosConfigChainRecovery.tla` | One finite mid-chain recovery slice where a Conf2 instance remains pinned to `{1,2,3,4}` after the current config becomes `{1,3,4}`; current-conf quorum responses do not advance prepare/accept, removed voter 2 supplies the modeled third old-quorum vote, and the no-op executes without application output. | Arbitrary recovery histories, arbitrary membership histories, retries, joint consensus, message loss, application output, and unbounded proof. |
+| `tla/EPaxosConfigChainRecoveryLostResponseRetry.tla` | One finite mid-chain lost-response retry slice where a Conf2 instance remains pinned to `{1,2,3,4}` after the current config becomes `{1,3,4}`; current-conf quorum responses do not advance prepare/accept before retry, deterministic retries rebroadcast to Conf2 peers `{2,3,4}` with width-4 dependencies, removed-voter prepare and accept responses are explicit pre-retry losses, replacement responses complete the Conf2 quorum, and the no-op executes without application output. | Arbitrary recovery histories, arbitrary retry histories, arbitrary message loss beyond this named finite pre-retry loss shape, joint consensus, arbitrary membership histories, application output, and unbounded proof. |
 | `tla/EPaxosConfigTransitionRetry.tla` | One finite normal old-config transition retry-timer slice where local-owner PreAccept/Accept retries after removal include removed voter 4 for old pinned instances, local-owner PreAccept/Accept retries after addition exclude added voter 4 for old pinned instances, dependency width stays old, and pure retries emit no durable/application effects. | Arbitrary retry histories beyond this timer slice, joint consensus, arbitrary message loss, arbitrary membership histories, application output, and unbounded proof. |
 | `tla/EPaxosConfigTransitionDedup.tla` | One finite normal old-config transition response de-duplication slice where the local owner vote is counted separately from remote PreAccept/Accept responses, duplicate old-voter responses and added current voter responses do not satisfy old pinned quorums, and the modeled second distinct old remote advances at quorum. | Arbitrary message histories, joint consensus, arbitrary membership histories, application output, and unbounded proof. |
 | `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. |