Add TryConflict force decision model

Author: lemon-mint

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -458,6 +458,7 @@ Evidence: `examples/kv/cmd/kvnode/main.go`, `examples/kv/cmd/kvnode/main_test.go
 | `tla/EPaxosOptimizedRecovery.tla` | Focused 3/5/7 Accept-Deps stale-dependency optimized-recovery evidence slices. | The concrete `MsgEvidence` exchange, every technical-report branch, and unbounded proof. |
 | `tla/EPaxosTryPreAcceptBranches.tla` | Focused 3/5/7 finite abstract TryPreAccept scenario/stage response-branch slice: stale restart, committed evidence ignore/fail-closed, direct/forced accept, one uncommitted deferral with duplicate suppression, and OK slow-quorum accept with `okVotes >= SlowQuorum` as the only quorum detail in this model. | TryPreAccept message paths, complete optimized-recovery branch parity, unbounded recovery trees, arbitrary message loss, and recovery under reconfiguration. |
 | `tla/EPaxosTryPreAcceptMessagePath.tla` | Focused 3/5/7 finite TryPreAccept request/response message paths: follower commit-only, stale/conflict reject, duplicate matching re-ack without durable rewrite, fresh durable ack; coordinator stale restart, committed evidence/direct accept, uncommitted forced/deferred handling, older-ballot ignore, duplicate OK ignore, first OK below quorum, pre-seeded quorum immediate accept, and OK slow-quorum accept. | Full network histories, evidence-query internals, complete optimized-recovery branch parity, unbounded recovery trees, arbitrary message loss, and recovery under reconfiguration. |
+| `tla/EPaxosTryConflictForce.tla` | Focused 3/5/7 finite quorum-arithmetic check for `tryConflictForcesSlowAccept`: required conflict leader forces slow Accept only without an existing dependency, required deferred-cycle leader forces slow Accept, optional leaders defer, and non-force cases start blocker recovery. | Full recovery histories, TryPreAccept message paths, evidence-query internals, complete optimized-recovery branch parity, and unbounded proof. |
 | `tla/EPaxosEvidenceQuery.tla` | Focused 3/5/7 committed-conflict evidence-query slice: guard-gated `MsgEvidence`, read-only responses, duplicate/mismatched drops, sender-preserving evidence validation, stale rejection restart, and fail-closed fallback. | Every technical-report branch, arbitrary membership/reconfiguration recovery, and unbounded proof. |
 | `tla/EPaxosRecovery.tla` | Stopped-owner dependency recovery and no-op unblocking for finite configs. | Arbitrary recovery under reconfiguration. |
 | `tla/EPaxosRollbackAllocation.tla` | Rollback allocation: a restored local checkpoint learns a later own committed instance from quorum, advances `nextInstance`, skips a known future local ref under a defensive stale-next state, allocates a fresh local ref, and preserves learned-before-fresh apply order. | Full EPaxos recovery, unbounded rollback histories, storage checksums, message loss, or arbitrary multi-replica rollback. |

MODEL_EQ_REPORT.MD

@@ -24,7 +24,7 @@
 - [EPAXOS_IMPLEMENTATION_PROOF.md](EPAXOS_IMPLEMENTATION_PROOF.md) explains the implemented algorithm, property claims, failure-count boundaries, proof rationale, and evidence/non-claims in detail.
 - [MODEL_EQ_REPORT.MD](MODEL_EQ_REPORT.MD) describes the current TLA+ model correspondence and implementation verification scope.
 - [RELEASE_SCOPE.md](RELEASE_SCOPE.md) is the self-contained release-scope lock for closed items, open items, and non-claims.
-- [tla/EPaxos.tla](tla/EPaxos.tla), [tla/EPaxosResponses.tla](tla/EPaxosResponses.tla), [tla/EPaxosRecovery.tla](tla/EPaxosRecovery.tla), [tla/EPaxosOptimizedRecovery.tla](tla/EPaxosOptimizedRecovery.tla), [tla/EPaxosTryPreAcceptBranches.tla](tla/EPaxosTryPreAcceptBranches.tla), [tla/EPaxosTryPreAcceptMessagePath.tla](tla/EPaxosTryPreAcceptMessagePath.tla), [tla/EPaxosEvidenceQuery.tla](tla/EPaxosEvidenceQuery.tla), [tla/EPaxosConfigBarrier.tla](tla/EPaxosConfigBarrier.tla), [tla/EPaxosConfigTransition.tla](tla/EPaxosConfigTransition.tla), [tla/EPaxosConfigRemoveTransition.tla](tla/EPaxosConfigRemoveTransition.tla), [tla/EPaxosConfigChainTransition.tla](tla/EPaxosConfigChainTransition.tla), [tla/EPaxosRevisited.tla](tla/EPaxosRevisited.tla), [tla/TOQClockDiscipline.tla](tla/TOQClockDiscipline.tla), [tla/ReadyAdvance.tla](tla/ReadyAdvance.tla), [tla/Quorum.tla](tla/Quorum.tla), [tla/KVTimestampStaleness.tla](tla/KVTimestampStaleness.tla), and [tla/KVOmissionRecovery.tla](tla/KVOmissionRecovery.tla) contain the finite executable formal models checked by CI.
+- [tla/EPaxos.tla](tla/EPaxos.tla), [tla/EPaxosResponses.tla](tla/EPaxosResponses.tla), [tla/EPaxosRecovery.tla](tla/EPaxosRecovery.tla), [tla/EPaxosOptimizedRecovery.tla](tla/EPaxosOptimizedRecovery.tla), [tla/EPaxosTryPreAcceptBranches.tla](tla/EPaxosTryPreAcceptBranches.tla), [tla/EPaxosTryPreAcceptMessagePath.tla](tla/EPaxosTryPreAcceptMessagePath.tla), [tla/EPaxosTryConflictForce.tla](tla/EPaxosTryConflictForce.tla), [tla/EPaxosEvidenceQuery.tla](tla/EPaxosEvidenceQuery.tla), [tla/EPaxosConfigBarrier.tla](tla/EPaxosConfigBarrier.tla), [tla/EPaxosConfigTransition.tla](tla/EPaxosConfigTransition.tla), [tla/EPaxosConfigRemoveTransition.tla](tla/EPaxosConfigRemoveTransition.tla), [tla/EPaxosConfigChainTransition.tla](tla/EPaxosConfigChainTransition.tla), [tla/EPaxosRevisited.tla](tla/EPaxosRevisited.tla), [tla/TOQClockDiscipline.tla](tla/TOQClockDiscipline.tla), [tla/ReadyAdvance.tla](tla/ReadyAdvance.tla), [tla/Quorum.tla](tla/Quorum.tla), [tla/KVTimestampStaleness.tla](tla/KVTimestampStaleness.tla), and [tla/KVOmissionRecovery.tla](tla/KVOmissionRecovery.tla) contain the finite executable formal models checked by CI.
 - [examples/kv](examples/kv) contains the Pebble/MyRocks-style key-value example.
 - [jepsen](jepsen) contains the Jepsen workload harness for external validation.
 - [tests](tests) contains the repository verification scripts used by CI.

README.md

@@ -85,6 +85,8 @@ This matrix is the current simulation/local-loopback fault-tolerance envelope. A
 | Evidence bundle and go/no-go workflow | `release/EPAXOS_READINESS_EVIDENCE.md`; `tests/go_no_go_workflow.sh`; `tests/ci.sh`; `bash tests/go_no_go_workflow.sh` returns the current `No-go.` decision and lists open release items; `bash tests/release_scope_audit.sh` checks the evidence/workflow paths. |
 
 TryPreAccept message-path coverage note: `tests/tla_model_check.sh` now runs `tla/EPaxosTryPreAcceptMessagePath.cfg`, `tla/EPaxosTryPreAcceptMessagePathFive.cfg`, and `tla/EPaxosTryPreAcceptMessagePathSeven.cfg`; each finite 3/5/7 config covers follower `MsgTryPreAccept` commit-only, stale/conflict reject, duplicate matching re-ack without durable rewrite, fresh durable ack, and coordinator `MsgTryPreAcceptResp` stale restart, older/duplicate OK ignore, first OK below quorum, pre-seeded quorum immediate accept, and OK slow-quorum accept.
+TryConflict force/defer quorum note: `tests/tla_model_check.sh` now runs `tla/EPaxosTryConflictForce.cfg`, `tla/EPaxosTryConflictForceFive.cfg`, and `tla/EPaxosTryConflictForceSeven.cfg`; the finite 3/5/7 model checks `leaderMustBeInCandidateFastQuorum` arithmetic for conflict-leader force, deferred-cycle force, optional-leader deferral, existing-dependency guard, and blocker-recovery deferral.
+
 
 ## Open release items
 
@@ -99,6 +101,8 @@ TryPreAccept message-path coverage note: `tests/tla_model_check.sh` now runs `tl
 TryPreAccept response branch-slice note: `tla/EPaxosTryPreAcceptBranches.tla` is only a finite abstract scenario/stage model for stale restart, committed evidence ignore/fail-closed, direct/forced accept, one uncommitted deferral with duplicate suppression, and OK slow-quorum accept. Its only quorum detail is `okVotes >= SlowQuorum`, it runs for 3/5/7, and complete optimized-recovery branch parity beyond this finite slice remains open.
 
 TryPreAccept message-path limit: `tla/EPaxosTryPreAcceptMessagePath.tla` is finite 3/5/7 request/response path coverage, not a full network, evidence-query-internal, complete optimized-recovery branch-parity, or unbounded recovery proof.
+TryConflict force/defer limit: `tla/EPaxosTryConflictForce.tla` is finite quorum-arithmetic coverage for one uncommitted-conflict force/defer decision, not arbitrary recovery history, full message delivery, complete optimized-recovery branch parity, or unbounded proof.
+
 
 ## Review baseline
 

RELEASE_SCOPE.md

@@ -81,6 +81,7 @@ Status: no-go evidence bundle for the active EPaxos production-readiness goal. T
 - `JAVA_BIN=/opt/homebrew/opt/openjdk/bin/java bash tests/tla_model_check.sh` passed after wiring `tla/EPaxosConfigChainTransition.cfg`; `EPaxosConfigChainTransition.cfg` generated 299 states and 299 distinct states with no TLC error.
 - `JAVA_BIN=/opt/homebrew/opt/openjdk/bin/java bash tests/tla_model_check.sh` passed after wiring `tla/EPaxosTryPreAcceptBranches.cfg`, `tla/EPaxosTryPreAcceptBranchesFive.cfg`, and `tla/EPaxosTryPreAcceptBranchesSeven.cfg`; each abstract branch-slice config generated 17 states and 17 distinct states with no TLC error.
 - `JAVA_BIN=/opt/homebrew/opt/openjdk/bin/java bash tests/tla_model_check.sh` passed after wiring `tla/EPaxosTryPreAcceptMessagePath.cfg`, `tla/EPaxosTryPreAcceptMessagePathFive.cfg`, and `tla/EPaxosTryPreAcceptMessagePathSeven.cfg`; each finite message-path config generated 32 states and 32 distinct states with no TLC error.
+- `JAVA_BIN=/opt/homebrew/opt/openjdk/bin/java bash tests/tla_model_check.sh` passed after wiring `tla/EPaxosTryConflictForce.cfg`, `tla/EPaxosTryConflictForceFive.cfg`, and `tla/EPaxosTryConflictForceSeven.cfg`; the finite force/defer configs generated 104/104, 168/168, and 232/232 states respectively with no TLC error.
 
 ### Fault-tolerance envelope proof summary
 
@@ -164,6 +165,8 @@ Non-claims remain explicit: No target-environment remote claim, no in-place Pebb
   - Add finite 3-, 5-, and 7-replica abstract scenario/stage TryPreAccept response-branch coverage: stale restart, committed evidence ignore/fail-closed, direct/forced accept, one uncommitted deferral with duplicate suppression, and OK slow-quorum accept. The only quorum detail modeled inside this slice is `okVotes >= SlowQuorum`; this is not a TryPreAccept message-path model, complete optimized-recovery branch parity, or unbounded recovery proof.
 - `tla/EPaxosTryPreAcceptMessagePath.tla`, `tla/EPaxosTryPreAcceptMessagePath.cfg`, `tla/EPaxosTryPreAcceptMessagePathFive.cfg`, and `tla/EPaxosTryPreAcceptMessagePathSeven.cfg`
   - Add finite 3-, 5-, and 7-replica TryPreAccept request/response message-path coverage for follower `MsgTryPreAccept` commit-only, stale/conflict reject, duplicate matching re-ack without durable rewrite, fresh durable ack, and coordinator `MsgTryPreAcceptResp` stale restart, committed evidence/direct accept, uncommitted forced/deferred handling, older-ballot ignore, duplicate OK ignore, first OK below quorum, pre-seeded quorum immediate accept, and OK slow-quorum accept. This is not a full-network, evidence-query-internal, complete optimized-recovery branch-parity, or unbounded recovery proof.
+- `tla/EPaxosTryConflictForce.tla`, `tla/EPaxosTryConflictForce.cfg`, `tla/EPaxosTryConflictForceFive.cfg`, and `tla/EPaxosTryConflictForceSeven.cfg`
+  - Add finite 3-, 5-, and 7-replica quorum-arithmetic coverage for `tryConflictForcesSlowAccept`: a conflict leader forces slow Accept only when the candidate lacks that dependency and every possible candidate fast quorum must include the leader, a deferred-cycle leader can independently force slow Accept when required, and optional/non-required leaders defer with blocker recovery. This is not a full recovery, network, or unbounded proof.
 - `tla/EPaxosEvidenceQuery.tla`, `tla/EPaxosEvidenceQuery.cfg`, `tla/EPaxosEvidenceQueryFive.cfg`, and `tla/EPaxosEvidenceQuerySeven.cfg`
   - Add finite 3-, 5-, and 7-replica committed-conflict evidence-query coverage: candidate-dependency/same-config guards before `MsgEvidence`, read-only response handling, duplicate/mismatched response drops, sender-preserving `AcceptEvidence` validation, stale TryPreAccept rejection restart, and fail-closed slow accept on missing, legacy-only, malformed, contradictory, or insufficient evidence.
 - `tla/EPaxosConfigBarrier.tla` and `tla/EPaxosConfigBarrier.cfg`
@@ -212,6 +215,7 @@ The following blockers are still listed in `RELEASE_SCOPE.md` and prevent a go d
 - Broader formal model coverage remains open beyond the finite configured TLC suite; `tla/EPaxosResponses.tla` adds bounded prepare branch-priority/try-witness checks, `tla/EPaxosOptimizedRecovery.tla` adds finite 3-, 5-, and 7-replica Accept-Deps optimized-recovery evidence checks, `tla/EPaxosEvidenceQuery.tla` adds finite 3-, 5-, and 7-replica committed-conflict evidence-query guard/fail-closed checks, `tla/EPaxosConfigBarrier.tla` adds finite local config-barrier checks, `tla/EPaxosConfigTransition.tla` adds one finite add-voter config-transition pinning check, `tla/EPaxosConfigRemoveTransition.tla` adds one finite remove-voter config-transition pinning check, `tla/EPaxosConfigChainTransition.tla` adds one finite add-then-remove configuration-chain pinning check, `tla/EPaxosRollbackAllocation.tla` adds one finite rollback-allocation next-instance/skip/apply-order check, and `tla/TOQClockDiscipline.tla` adds a finite bounded-skew/bounded-delay `ProcessAt` contract check, but operational synchronized-clock/OWD-measurement implementation proof for TOQ deployments, unbounded proof, arbitrary membership-change proof, arbitrary multi-step reconfiguration proof, recovery under configuration changes, complete optimized-recovery branch parity, full rollback-history proof, and arbitrary application/state-machine semantics remain open.
 - `tla/EPaxosTryPreAcceptBranches.tla` is a finite abstract scenario/stage branch slice only; it covers stale restart, committed evidence ignore/fail-closed, direct/forced accept, one uncommitted deferral with duplicate suppression, and OK slow-quorum accept for 3/5/7 with `okVotes >= SlowQuorum` as the only quorum detail. Complete optimized-recovery branch parity beyond that slice remains open.
 - `tla/EPaxosTryPreAcceptMessagePath.tla` adds finite 3/5/7 concrete TryPreAccept request/response message-path coverage, including pre-seeded quorum immediate accept, but complete optimized-recovery branch parity beyond the finite branch/message-path/evidence-query slices remains open.
+- `tla/EPaxosTryConflictForce.tla` adds finite 3/5/7 quorum-arithmetic coverage for uncommitted-conflict force/defer decisions, but arbitrary recovery histories and complete optimized-recovery branch parity remain open.
 - Deployment manifest artifacts are example/operator material only; `tests/kvnode_systemd_manifest_audit.sh` renders and audits the example `ExecStart` contract, but reviewed execution under a target system manager, container, or orchestration environment remains open.
 - Data lifecycle now has a maintained local offline `kvcheckpoint` helper plus runbook/audit evidence, but a reviewed operator backup/restore/disaster-recovery drill in the target environment remains open. The mixed-version drill's binary rollback keeps current data and does not exercise checkpoint restore.
 - Target-environment capacity-envelope measurements remain open; local evidence now includes a single-node workstation sample plus a three-node loopback wrapper sample, but neither is a measured target-environment capacity result.

release/EPAXOS_READINESS_EVIDENCE.md

@@ -114,6 +114,9 @@ require_text "TryPreAccept response branch-slice"
 require_text "tla/EPaxosTryPreAcceptMessagePath.cfg"
 require_text "tla/EPaxosTryPreAcceptMessagePathSeven.cfg"
 require_text "TryPreAccept message-path coverage"
+require_text "tla/EPaxosTryConflictForce.cfg"
+require_text "tla/EPaxosTryConflictForceSeven.cfg"
+require_text "force/defer quorum"
 require_text "tla/EPaxosEvidenceQuery.tla"
 require_text "tla/EPaxosEvidenceQuerySeven.cfg"
 require_text 'unique TLC `-metadir`'
@@ -207,6 +210,10 @@ require_path "tla/EPaxosTryPreAcceptMessagePath.tla"
 require_path "tla/EPaxosTryPreAcceptMessagePath.cfg"
 require_path "tla/EPaxosTryPreAcceptMessagePathFive.cfg"
 require_path "tla/EPaxosTryPreAcceptMessagePathSeven.cfg"
+require_path "tla/EPaxosTryConflictForce.tla"
+require_path "tla/EPaxosTryConflictForce.cfg"
+require_path "tla/EPaxosTryConflictForceFive.cfg"
+require_path "tla/EPaxosTryConflictForceSeven.cfg"
 require_path "tla/EPaxosEvidenceQuery.tla"
 require_path "tla/EPaxosEvidenceQuerySeven.cfg"
 require_path "tla/EPaxosConfigTransition.tla"

tests/release_scope_audit.sh

@@ -77,6 +77,10 @@ for cfg in tla/EPaxosTryPreAcceptMessagePath.cfg tla/EPaxosTryPreAcceptMessagePa
   run_tlc tla/EPaxosTryPreAcceptMessagePath.tla "$cfg"
 done
 
+for cfg in tla/EPaxosTryConflictForce.cfg tla/EPaxosTryConflictForceFive.cfg tla/EPaxosTryConflictForceSeven.cfg; do
+  run_tlc tla/EPaxosTryConflictForce.tla "$cfg"
+done
+
 for cfg in tla/EPaxosEvidenceQuery.cfg tla/EPaxosEvidenceQueryFive.cfg tla/EPaxosEvidenceQuerySeven.cfg; do
   run_tlc tla/EPaxosEvidenceQuery.tla "$cfg"
 done

tests/tla_model_check.sh

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+INVARIANT TypeOK
+INVARIANT Safety
+PROPERTY EventuallyCoversForceDecision
+CHECK_DEADLOCK FALSE
+CONSTANTS
+    ReplicaCount = 3