Add TryPreAccept branch slice model

Author: lemon-mint

EPAXOS_IMPLEMENTATION_PROOF.md

@@ -456,6 +456,7 @@ Evidence: `examples/kv/cmd/kvnode/main.go`, `examples/kv/cmd/kvnode/main_test.go
 | `tla/EPaxos.tla` | Normal PreAccept/Accept/Commit, dependency evidence, and deterministic execution. | Full recovery tree and unbounded state space. |
 | `tla/EPaxosResponses.tla` | Response quorum evidence, prepare branch priority, `fast + slow - N` TryPreAccept witness threshold, and ballot-bound current-round AcceptOK evidence. | Unbounded state space. |
 | `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/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/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/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

@@ -49,7 +49,7 @@ This matrix is the current simulation/local-loopback fault-tolerance envelope. A
 | Static/text audit | `tests/audit_repo.sh`; `bash tests/audit_repo.sh`; `tests/ci.sh` |
 | Algorithm correspondence | `EPAXOS.MD`; `MODEL_EQ_REPORT.MD`; `tests/tla_model_check.sh`; `tests/ci.sh` |
 | Implementation proof document | `EPAXOS_IMPLEMENTATION_PROOF.md`; paper-grounded EPaxos/Revisited obligation map; exact failure-count matrix; property-by-property rationale; verification/non-claim matrix; `bash tests/release_scope_audit.sh` |
-| Formal models (finite configured suite) | `tests/tla_model_check.sh`; unique TLC `-metadir` per config; `tla/EPaxos.cfg`; `tla/EPaxosKVConflict.cfg`; `tla/EPaxosThreeReplica.cfg`; `tla/EPaxosResponses.cfg`; `tla/EPaxosResponsesFive.cfg`; `tla/EPaxosRecovery.cfg`; `tla/EPaxosRecoveryFive.cfg`; `tla/EPaxosOptimizedRecovery.cfg`; `tla/EPaxosOptimizedRecoveryFive.cfg`; `tla/EPaxosOptimizedRecoverySeven.cfg`; `tla/EPaxosEvidenceQuery.cfg`; `tla/EPaxosEvidenceQueryFive.cfg`; `tla/EPaxosEvidenceQuerySeven.cfg`; `tla/EPaxosConfigBarrier.cfg`; `tla/EPaxosConfigTransition.cfg`; `tla/EPaxosConfigRemoveTransition.cfg`; `tla/EPaxosConfigChainTransition.cfg`; `tla/EPaxosRollbackAllocation.cfg`; `tla/EPaxosRevisited.cfg`; `tla/TOQClockDiscipline.cfg`; `tla/ReadyAdvance.cfg`; `tla/ReadyAdvanceCapped.cfg`; `tla/KVTimestampStaleness.cfg`; `tla/KVOmissionRecovery.cfg`; `tla/Quorum.cfg`; `MODEL_EQ_REPORT.MD`; `bash tests/tla_model_check.sh` passed with `EPaxosConfigChainTransition.cfg` `299/299`, `EPaxosConfigRemoveTransition.cfg` `70/70`, and `EPaxosRollbackAllocation.cfg` `7/7` generated/distinct states. |
+| Formal models (finite configured suite) | `tests/tla_model_check.sh`; unique TLC `-metadir` per config; `tla/EPaxos.cfg`; `tla/EPaxosKVConflict.cfg`; `tla/EPaxosThreeReplica.cfg`; `tla/EPaxosResponses.cfg`; `tla/EPaxosResponsesFive.cfg`; `tla/EPaxosRecovery.cfg`; `tla/EPaxosRecoveryFive.cfg`; `tla/EPaxosOptimizedRecovery.cfg`; `tla/EPaxosOptimizedRecoveryFive.cfg`; `tla/EPaxosOptimizedRecoverySeven.cfg`; `tla/EPaxosTryPreAcceptBranches.cfg`; `tla/EPaxosTryPreAcceptBranchesFive.cfg`; `tla/EPaxosTryPreAcceptBranchesSeven.cfg`; `tla/EPaxosEvidenceQuery.cfg`; `tla/EPaxosEvidenceQueryFive.cfg`; `tla/EPaxosEvidenceQuerySeven.cfg`; `tla/EPaxosConfigBarrier.cfg`; `tla/EPaxosConfigTransition.cfg`; `tla/EPaxosConfigRemoveTransition.cfg`; `tla/EPaxosConfigChainTransition.cfg`; `tla/EPaxosRollbackAllocation.cfg`; `tla/EPaxosRevisited.cfg`; `tla/TOQClockDiscipline.cfg`; `tla/ReadyAdvance.cfg`; `tla/ReadyAdvanceCapped.cfg`; `tla/KVTimestampStaleness.cfg`; `tla/KVOmissionRecovery.cfg`; `tla/Quorum.cfg`; `MODEL_EQ_REPORT.MD`; `bash tests/tla_model_check.sh` passed with `EPaxosTryPreAcceptBranches.cfg`, `EPaxosTryPreAcceptBranchesFive.cfg`, and `EPaxosTryPreAcceptBranchesSeven.cfg` each at `17/17`, `EPaxosConfigChainTransition.cfg` `299/299`, `EPaxosConfigRemoveTransition.cfg` `70/70`, and `EPaxosRollbackAllocation.cfg` `7/7` generated/distinct states. |
 | Local Jepsen restart/transport/storage gates | `tests/jepsen_local.sh`; `jepsen/src/moreconsensus/epaxos_test.clj`; `tests/ci.sh` |
 | Local destructive-storage recovery | `tests/jepsen_local.sh`; `jepsen/src/moreconsensus/epaxos_test.clj`; manual evidence: `env JEPSEN_LOCAL_FAULTS=destructive-storage bash tests/jepsen_local.sh` |
 | Remote destructive-safety preflight | `tests/jepsen_remote.sh`; `tests/jepsen_remote_preflight_audit.sh`; `jepsen/src/moreconsensus/epaxos_test.clj`; `jepsen/test/moreconsensus/epaxos_test_test.clj`; `bash tests/jepsen_remote_preflight_audit.sh`; remote destructive-storage and wall-clock-skew runs require explicit confirmations, reject broad/unsafe remote directories by default, and support preflight-only validation without touching remote hosts. This is safety preflight evidence, not an external multi-host Jepsen history. |
@@ -88,12 +88,14 @@ This matrix is the current simulation/local-loopback fault-tolerance envelope. A
 
 | Item | Current state |
 | --- | --- |
-| Broader formal model coverage | Finite configured TLC models are closed above, including bounded prepare branch-priority/try-witness coverage, finite 3-, 5-, and 7-replica Accept-Deps optimized-recovery evidence coverage, finite 3-, 5-, and 7-replica committed-conflict evidence-query guard/fail-closed coverage, finite configuration-barrier coverage, one finite add-voter configuration-transition pinning check, one finite remove-voter configuration-transition pinning check, one finite add-then-remove configuration-chain pinning check, a finite rollback-allocation next-instance/skip/apply-order check, and a finite `TOQClockDiscipline` bounded-skew/bounded-delay `ProcessAt` contract; unbounded proof, even-size optimized-quorum proof, operational synchronized-clock/OWD-measurement implementation proof for TOQ deployments, arbitrary membership-change proof, arbitrary multi-step reconfiguration chains, joint consensus, recovery under configuration changes, durable replay, complete optimized-recovery branch parity, full rollback-history proof, and arbitrary application/state-machine semantics remain open. |
+| Broader formal model coverage | Finite configured TLC models are closed above, including bounded prepare branch-priority/try-witness coverage, finite 3-, 5-, and 7-replica Accept-Deps optimized-recovery evidence coverage, finite 3-, 5-, and 7-replica abstract TryPreAccept response branch-slice coverage, finite 3-, 5-, and 7-replica committed-conflict evidence-query guard/fail-closed coverage, finite configuration-barrier coverage, one finite add-voter configuration-transition pinning check, one finite remove-voter configuration-transition pinning check, one finite add-then-remove configuration-chain pinning check, a finite rollback-allocation next-instance/skip/apply-order check, and a finite `TOQClockDiscipline` bounded-skew/bounded-delay `ProcessAt` contract; unbounded proof, complete optimized-recovery branch parity beyond the finite TryPreAccept branch slice, even-size optimized-quorum proof, operational synchronized-clock/OWD-measurement implementation proof for TOQ deployments, arbitrary membership-change proof, arbitrary multi-step reconfiguration chains, joint consensus, recovery under configuration changes, durable replay, full rollback-history proof, and arbitrary application/state-machine semantics remain open. |
 | Deployment manifest | Example systemd artifacts now exist (`deploy/systemd/kvnode@.service`, `deploy/systemd/kvnode.env.example`) plus `tests/kvnode_systemd_manifest_audit.sh`, which renders the example EnvironmentFile into the `ExecStart` contract and keeps `systemd-analyze verify` opt-in via `KVNODE_SYSTEMD_ANALYZE=yes`; these artifacts are checked by `tests/operations_readiness_audit.sh`. A reviewed and exercised target deployment under systemd/container/orchestration remains open before this can be a production manifest claim. |
 | Data lifecycle | Local destructive-storage remove/restore evidence exists, the KV example has exercised Pebble checkpoint/whole-directory restore plus offline and live-source checkpoint-backed repair tests for checksum-detected bit-level corruption, `examples/kv/cmd/kvcheckpoint` provides a maintained offline checkpoint/verify/verified-restore/repair helper, `TestRestoreRejectsCorruptCheckpointWithoutReplacingLiveData` verifies restore fails closed before replacement, and `docs/operations/kvnode-data-lifecycle-incident-runbook.md` documents checkpoint, verification, repair, restore, checksum-mismatch, and evidence-capture procedures. A reviewed operator backup/restore/disaster-recovery drill in the target environment remains open. |
 | Capacity envelope | `tests/kvnode_capacity_envelope.sh` is an opt-in bounded harness for throughput, latency, memory RSS, disk growth, queue depth, value size, scan limit, and peer-count samples; `tests/kvnode_local_capacity_drill.sh` starts a disposable three-node loopback cluster and runs that harness against all three client/admin listeners with PIDs and data dirs; `bash -n tests/kvnode_capacity_envelope.sh`, `bash tests/kvnode_capacity_envelope.sh --help`, `bash tests/kvnode_local_capacity_drill.sh --help`, and `tests/operations_readiness_audit.sh` pass. Local loopback samples have passed, including the earlier single-node workstation sample and a three-node local wrapper sample with 5 ops per value-size phase, 64/1024-byte values, scan limits 1/8, and peer_count=3. This is workstation harness evidence only; measured target-environment capacity results remain open. |
 | Incident readiness | `docs/operations/kvnode-data-lifecycle-incident-runbook.md` now covers storage failure, network partition, peer compromise, replay/checksum suspicion, and recovery stalls, with evidence-capture steps and non-claims; `tests/kvnode_incident_tabletop_drill.sh` locally rehearses the storage-failure and network-partition test-fault branches on a disposable loopback cluster; `tests/operations_readiness_audit.sh` checks those artifacts. Operator-reviewed target-environment tabletop or live drill evidence remains open. |
 
+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.
+
 ## Review baseline
 
 The review baseline is the current repository state after the EPaxos recovery, Revisited chain-pruning, explicit TOQ core behavior, deterministic `ProcessAt` timing, persistence, local fault-injection campaign, Jepsen checker, and documentation updates verified by `tests/ci.sh`. Reviewers should begin with:

RELEASE_SCOPE.md

@@ -79,6 +79,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/EPaxosConfigRemoveTransition.cfg`; `EPaxosConfigRemoveTransition.cfg` generated 70 states and 70 distinct states with no TLC error.
 - `go test ./epaxos -run TestRemoveVoterConfChangeKeepsOldInFlightInstancePinned -count=1` passed after making per-instance quorum thresholds/broadcasts use `Ref.Conf` and rejecting local proposals from removed voters (`artifact://964`).
 - `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.
 
 ### Fault-tolerance envelope proof summary
 
@@ -158,6 +159,8 @@ Non-claims remain explicit: No target-environment remote claim, no in-place Pebb
   - Adds a 5-replica finite stopped-owner recovery configuration for the existing `EPaxosRecovery.tla` model.
 - `tla/EPaxosOptimizedRecovery.tla`, `tla/EPaxosOptimizedRecovery.cfg`, `tla/EPaxosOptimizedRecoveryFive.cfg`, and `tla/EPaxosOptimizedRecoverySeven.cfg`
   - Add finite 3-, 5-, and 7-replica optimized-recovery coverage: prepare fast-witness threshold gates TryPreAccept, AcceptReply evidence is recorded without changing chosen attributes, and Accept-Deps covers only the stale-dependency case where chosen `Deps` already order the conflict.
+- `tla/EPaxosTryPreAcceptBranches.tla`, `tla/EPaxosTryPreAcceptBranches.cfg`, `tla/EPaxosTryPreAcceptBranchesFive.cfg`, and `tla/EPaxosTryPreAcceptBranchesSeven.cfg`
+  - 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/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`
@@ -204,6 +207,7 @@ Non-claims remain explicit: No target-environment remote claim, no in-place Pebb
 The following blockers are still listed in `RELEASE_SCOPE.md` and prevent a go decision:
 
 - 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.
 - 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.