Add config transition retry evidence model

Author: lemon-mint

EPAXOS.MD

@@ -113,7 +113,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, lost+duplicate recovery response de-duplication, recovery-after-addition, and old-config prepare/accept 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 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.
 
 ## Ready contract
 

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -338,15 +338,17 @@ Finite replay coverage:
 - `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/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.
 
 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, 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 durable restart-replay 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`).
 
 ## 15. Property-by-property rationale
 
@@ -483,6 +485,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/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/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/EPaxosConfigRecoveryRetry.tla` | One finite old-config recovery retry-timer slice where prepare/accept retries after removal include removed voter 4 for old pinned instances, prepare/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 recovery histories, retry histories beyond this timer slice, joint consensus, arbitrary message loss, arbitrary membership histories, application output, and unbounded proof. |