Add config chain recovery evidence model

Author: lemon-mint

EPAXOS.MD

@@ -111,9 +111,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, newly added voters cannot count for pre-addition instances, and current-configuration proposals from a removed local replica remain 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, and retry-timer rebroadcast after removal/addition, plus staged old-instance recovery-after-removal, lost+duplicate recovery response de-duplication, recovery-after-addition, and old-config prepare/accept recovery retry-timer slices. Arbitrary durable histories, arbitrary recovery under reconfiguration, arbitrary retry histories, arbitrary message loss, 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, and old-config prepare/accept recovery retry-timer slices. Arbitrary durable histories, arbitrary recovery under reconfiguration, arbitrary retry histories, arbitrary message loss, joint consensus, and unbounded membership changes remain outside the current claim.
 
 ## Ready contract
 

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -337,20 +337,22 @@ Finite replay coverage:
 - 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.
+- `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/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 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, and one finite old-config recovery retry-timer 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, 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, and one finite old-config recovery retry-timer 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, 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`.
 
 Additional source anchors for finite add/de-dup recovery coverage: `tla/EPaxosConfigAddRecovery.tla`, `tla/EPaxosConfigAddRecovery.cfg`, `tla/EPaxosConfigRecoveryDedup.cfg`.
 Additional source anchors for finite config-recovery retry coverage: `tla/EPaxosConfigRecoveryRetry.tla`, `tla/EPaxosConfigRecoveryRetry.cfg`, and `epaxos/recovery_test.go` (`TestOldConfigRecoveryRetryUsesPinnedVotersAfterRemoval`, `TestOldConfigRecoveryRetryUsesPinnedVotersAfterAddition`).
 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`).
 
 ## 15. Property-by-property rationale
 
@@ -487,6 +489,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/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/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. |