Model Ready Advance and guard destructive storage

Author: lemon-mint

MODEL_EQ_REPORT.MD

@@ -16,7 +16,7 @@ This report maps the current finite TLA+ safety model to the current Go implemen
 | `tla/EPaxos.tla:69` TLA Prepare | `epaxos/node.go:669` Go prepare handler | Prepare persists higher promises and returns local accepted/committed state for recovery; TLA abstracts this as the ballot-raising recovery step. |
 | Not represented in current TLA safety model | `epaxos/node.go:695` Go prepare response handler | Recovery response quorum handling is verified by Go tests, but the current TLA model abstracts away recovery quorum collection. |
 | `tla/EPaxos.tla:76` TLA Execute | `epaxos/node.go:970` Go executor | Both make a committed command executable only after dependencies outside its component are executed; Go then exposes user commands through `Ready.Committed` instead of modeling application acknowledgement as TLA state. |
-| Not represented in current TLA safety model | `epaxos/node.go:403` Advance and `epaxos/node.go:529` enqueueExecutedRecords | Ready acknowledgement, exact-prefix validation, and delayed durable `StatusExecuted` emission are implementation validation rather than modeled state. |
+| `tla/ReadyAdvance.tla:66` TLA Ready, `tla/ReadyAdvance.tla:73` TLA Advance, and `tla/ReadyAdvance.tla:89` TLA Ready safety invariants | `epaxos/node.go:377` Ready, `epaxos/node.go:403` Advance, `epaxos/node.go:435` validateReadyAck, and `epaxos/node.go:529` enqueueExecutedRecords | Ready/Advance are modeled as a stable outstanding batch, non-empty exact-prefix acknowledgement, durable-record barrier before message or command acknowledgement, capped message visibility, and post-command executed durable-record emission. |
 | `tla/EPaxos.tla:96` TLA DependencyClosure | `epaxos/node.go:1070` Go component readiness | Component readiness requires outside committed dependencies to be executed before application emission. |
 | `tla/EPaxos.tla:98` TLA ConflictOrder | `epaxos/types.go:150` Go command conflict predicate and `epaxos/node.go:1119` Go dependency references | Both require conflicting executed commands to be ordered by dependencies; Go interprets dependency vectors as known per-replica prefixes through configuration history. |
 | Not represented in current TLA safety model | `epaxos/node.go:272` ProposeConfChange and `epaxos/node.go:290` confChangeQuorum | Membership-change proposal validation and rejected no-op configuration commands are implementation validation rather than modeled state. |
@@ -28,26 +28,26 @@ This report maps the current finite TLA+ safety model to the current Go implemen
 | `tla/Quorum.tla:9` and `tla/Quorum.tla:55` TLA quorum formulas/intersections | `epaxos/quorum.go:15` Go quorum calculation | Both define supported cluster sizes one through seven, majority slow quorum `n/2 + 1`, conservative fast quorum `n - ((n - 1) / 4)`, explicit expected tables, and quorum-intersection invariants checked by TLC and Go tests. |
 | `tla/EPaxosKVConflict.cfg:11` selective command set | `examples/kv/kv.go:368` Go transaction conflict-key construction | The KV conflict TLC config models independent single-key commands and a transaction-like command that conflicts with both keys; atomic multi-key apply and duplicate-key payload ordering remain implementation-tested at the example storage layer. |
 | Not represented in current TLA safety model | `examples/kv/kv.go:305` Go scan implementation | Advanced scan ordering, reverse ordering, timestamp collision behavior, and Pebble durability are example storage semantics verified by Go tests rather than by the current TLA state. |
-| Not represented in current TLA safety model | `examples/kv/cmd/kvnode/main.go:285` transport fault control, `examples/kv/cmd/kvnode/main.go:311` storage fault control, `jepsen/src/moreconsensus/epaxos_test.clj:234` local destructive-storage nemesis, `jepsen/src/moreconsensus/epaxos_test.clj:311` transport nemesis, `jepsen/src/moreconsensus/epaxos_test.clj:339` storage nemesis, `jepsen/src/moreconsensus/epaxos_test.clj:389` remote config, `jepsen/src/moreconsensus/epaxos_test.clj:477` remote DB, and `jepsen/src/moreconsensus/epaxos_test.clj:522` remote destructive-storage nemesis | Local transport partition, storage-unavailable, destructive-storage, and opt-in SSH-managed remote controls are external validation mechanisms for the KV example and Jepsen workload rather than modeled state. |
+| Not represented in current TLA safety model | `examples/kv/cmd/kvnode/main.go:285` transport fault control, `examples/kv/cmd/kvnode/main.go:311` storage fault control, `jepsen/src/moreconsensus/epaxos_test.clj:233` local destructive-storage nemesis, `jepsen/src/moreconsensus/epaxos_test.clj:310` transport nemesis, `jepsen/src/moreconsensus/epaxos_test.clj:338` storage nemesis, `jepsen/src/moreconsensus/epaxos_test.clj:388` remote config, `jepsen/src/moreconsensus/epaxos_test.clj:475` remote DB, and `jepsen/src/moreconsensus/epaxos_test.clj:520` remote destructive-storage nemesis | Local transport partition, storage-unavailable, node-down-until-restore destructive-storage, and opt-in SSH-managed remote controls are external validation mechanisms for the KV example and Jepsen workload rather than modeled state. |
 
 ## Current verification evidence
 
-- Observed `tests/ci.sh` passing after the strict Ready acknowledgement, durable in-process cluster, restart health-probe, reusable decode scratch, checksum pooling, late fast-quorum Revisited coverage, configuration-change validation, and Jepsen destructive-storage changes. The gate ran root Go tests, root coverage at 100.0%, example Go tests, example coverage at 100.0%, tagged kvnode tests, root/example/kvnode race checks, TLC model checks, local Jepsen restart, transport, storage, destructive-storage profiles, and the repository text audit.
+- Observed `tests/ci.sh` passing after the strict Ready acknowledgement, Ready/Advance TLA model, durable in-process cluster, restart health-probe, reusable decode scratch, checksum pooling, late fast-quorum Revisited coverage, configuration-change validation, and destructive-storage node-down-until-restore fix. The gate ran root Go tests, root coverage at 100.0%, example Go tests, example coverage at 100.0%, tagged kvnode tests, root/example/kvnode race checks, TLC model checks, local Jepsen restart, transport, storage, destructive-storage profiles, and the repository text audit.
 - Observed `go test ./epaxos` passing with deterministic randomized simulation coverage for three- and five-node clusters, duplicate/drop/reorder delivery, logical ticks, restarts, dependency-vector prefix execution ordering, Ready/Advance durability, strict Ready acknowledgement validation, Revisited fast-wait slow-path fallback and late fast-commit behavior, configuration-change rejection and invalid committed config no-op behavior, allocation/pool ownership assertions, decoder fuzz seeds, reusable decode scratch growth/reset coverage, zero-allocation pre-sized scratch decode, input-byte aliasing, and decoder error cleanup.
 - Observed `go test ./examples/kv` and `go test -tags kvnode ./examples/kv/cmd/kvnode` passing with KV duplicate-key transaction payload-order semantics, deduplicated EPAXOS conflict keys, durable in-process cluster restart through Pebble-backed EPaxOS storage, post-Advance executed-record persistence, negative scan-limit rejection, transport fault-route coverage, and storage fault-route coverage that rejects work before RawNode progress.
 - Observed `go test ./epaxos -coverprofile=coverage.out -count=1` reporting 100.0% statement coverage and `go tool cover -func=coverage.out` reporting `ProposeConfChange`, `confChangeQuorum`, `DecodeMessageWithScratch`, `DecodeScratch.deps`, `DecodeScratch.conflictKeys`, `writeByte`, `Advance`, `validateReadyAck`, `commandEqual`, and `instanceNumsEqual` at 100.0%.
 - Observed `go test ./examples/kv -coverprofile=coverage.out -count=1` reporting 100.0% statement coverage and `go tool cover -func=coverage.out` reporting `drainWithLimit` at 100.0% after the durable-applier acknowledgement-error test.
-- Observed `tests/tla_model_check.sh` running TLC for `tla/EPaxos.cfg` with 11162 generated states and 2002 distinct states, `tla/EPaxosKVConflict.cfg` with 3042650 generated states and 166034 distinct states, `tla/EPaxosThreeReplica.cfg` with 1104121 generated states and 123821 distinct states, and `tla/Quorum.cfg` with 2 generated states and 1 distinct state; all completed with no invariant violation.
-- Observed targeted `lein test moreconsensus.epaxos-test-test` from `jepsen` passing 38 tests with 100 assertions for register delete normalization, indeterminate mutation response classification, transaction body encoding, grouped reads, scan shape checking, restart fault selection, restart health probing, transport fault selection, storage fault selection, destructive-storage generator and nemesis routing, guarded destructive restore, remote config/DB command construction, remote control routing, client/nemesis routing, restart nemesis behavior, transport nemesis control requests, and storage nemesis control requests.
-- Observed focused `JEPSEN_LOCAL_FAULTS=destructive-storage bash tests/jepsen_local.sh` local destructive-storage profile reporting process storage removal and restoration with `:action :storage-removed`, `:action :storage-restored`, `:status 200`, and `:healthy true`, plus register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 7, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 9, :bad-count 0}`, and overall `:valid? true`.
-- Observed `tests/ci.sh` local restart profile reporting health-checked restart nemesis values with `:action :started`, `:status 200`, and `:healthy true`, plus register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 7, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 4, :bad-count 0}`, and overall `:valid? true`.
-- Observed `tests/ci.sh` local transport profile reporting register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 10, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 6, :bad-count 0}`, and overall `:valid? true`.
-- Observed `tests/ci.sh` local storage profile reporting register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 8, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 2, :bad-count 0}`, and overall `:valid? true`.
-- Observed `tests/ci.sh` local destructive-storage profile reporting process storage removal and restoration with `:action :storage-removed`, `:action :storage-restored`, `:status 200`, and `:healthy true`, plus register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 14, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 6, :bad-count 0}`, and overall `:valid? true`.
+- Observed `tests/tla_model_check.sh` running TLC for `tla/EPaxos.cfg` with 11162 generated states and 2002 distinct states, `tla/EPaxosKVConflict.cfg` with 3042650 generated states and 166034 distinct states, `tla/EPaxosThreeReplica.cfg` with 1104121 generated states and 123821 distinct states, `tla/ReadyAdvance.cfg` with 93 generated states and 39 distinct states, `tla/ReadyAdvanceCapped.cfg` with 77 generated states and 39 distinct states, and `tla/Quorum.cfg` with 2 generated states and 1 distinct state; all completed with no invariant violation.
+- Observed targeted `lein test moreconsensus.epaxos-test-test` from `jepsen` passing 42 tests with 114 assertions for register delete normalization, indeterminate mutation response classification, transaction body encoding, grouped reads, scan shape checking, restart fault selection, restart health probing, transport fault selection, storage fault selection, destructive-storage generator and nemesis routing, node-down destructive storage removal, restore-before-restart behavior, remote config/DB command construction, remote control routing, client/nemesis routing, restart nemesis behavior, transport nemesis control requests, and storage nemesis control requests.
+- Observed focused `JEPSEN_LOCAL_FAULTS=destructive-storage bash tests/jepsen_local.sh` local destructive-storage profile reporting process storage removal as a stopped node, restoration with `:action :storage-restored`, `:status 200`, and `:healthy true`, plus register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 3, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 1, :bad-count 0}`, and overall `:valid? true`.
+- Observed `tests/ci.sh` local restart profile reporting health-checked restart nemesis values with `:action :started`, `:status 200`, and `:healthy true`, plus register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 6, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 7, :bad-count 0}`, and overall `:valid? true`.
+- Observed `tests/ci.sh` local transport profile reporting register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 9, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 3, :bad-count 0}`, and overall `:valid? true`.
+- Observed `tests/ci.sh` local storage profile reporting register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 12, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 7, :bad-count 0}`, and overall `:valid? true`.
+- Observed `tests/ci.sh` local destructive-storage profile reporting process storage removal as a stopped node and restoration with `:action :storage-restored`, `:status 200`, and `:healthy true`, plus register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 4, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 6, :bad-count 0}`, and overall `:valid? true`.
 - Observed repository text audit with no disallowed external-project name, scaffolding marker, or wall-clock API matches.
 
 ## Open correspondence risks
 
 - The TLA+ model is finite-bounded for TLC, so it demonstrates correspondence for the configured state space rather than unbounded proof.
-- Ready acknowledgement, delayed durable execution markers, membership-change validation, checksum, wire-decoder tolerance, storage virtualization, recovery response collection, transport fault control, storage fault control, destructive-storage control, SSH-managed Jepsen lifecycle, and example KV apply/scan storage semantics are verified by implementation and Jepsen tests but outside the current TLA safety state.
-- Local Jepsen now covers loopback process restart with health-checked rejoin, transport partition, storage-unavailable, and destructive-storage remove/restore profiles. SSH-managed multi-host deployment is implemented through `tests/jepsen_remote.sh` and remote DB/nemesis unit tests, but this workstation did not exercise real SSH hosts or long-duration operational runs.
+- Membership-change validation, checksum, wire-decoder tolerance, storage virtualization, recovery response collection, transport fault control, storage fault control, destructive-storage control, SSH-managed Jepsen lifecycle, and example KV apply/scan storage semantics are verified by implementation and Jepsen tests but outside the current TLA safety state.
+- Local Jepsen now covers loopback process restart with health-checked rejoin, transport partition, storage-unavailable, and destructive-storage removal that keeps a node down until original storage is restored. SSH-managed multi-host deployment is implemented through `tests/jepsen_remote.sh` and remote DB/nemesis unit tests, but this workstation did not exercise real SSH hosts or long-duration operational runs.

README.md

@@ -26,7 +26,7 @@
 
 ## Operational validation
 
-- `JEPSEN_LOCAL_FAULTS=destructive-storage bash tests/jepsen_local.sh` runs the loopback KV cluster while each process is stopped, its Pebble directory is moved aside, an empty directory is started, and the original directory is restored.
+- `JEPSEN_LOCAL_FAULTS=destructive-storage bash tests/jepsen_local.sh` runs the loopback KV cluster while each selected process is stopped, its Pebble directory is moved aside, and the original directory is restored before the process rejoins.
 - `JEPSEN_NODES=n1,n2,n3 bash tests/jepsen_remote.sh` builds `kvnode`, uploads it to each SSH-managed host, starts one node per host, and runs the destructive-storage profile by default. `JEPSEN_REMOTE_FAULTS=restart|transport|storage|destructive-storage`, `JEPSEN_REMOTE_DURATION`, `JEPSEN_REMOTE_CONCURRENCY`, `MORECONSENSUS_KVNODE_HTTP_PORT`, and `MORECONSENSUS_KVNODE_REMOTE_DIR` tune that run.
 
 ## Module layout

jepsen/src/moreconsensus/epaxos_test.clj

@@ -217,8 +217,7 @@
         data-dir (local-data-dir cfg node)
         backup-dir (local-storage-backup-dir cfg node)]
     (local-move-if-present! data-dir backup-dir)
-    (let [start (start-node! cfg node)]
-      {:node node :action :storage-removed :stop stop :start start})))
+    {:node node :action :storage-removed :stop stop}))
 
 (defn restore-local-storage! [cfg node]
   (let [data-dir (local-data-dir cfg node)
@@ -460,8 +459,7 @@
         data-dir (remote-node-data-dir cfg node)
         backup-dir (remote-node-backup-dir cfg node)]
     (remote-move-if-present! data-dir backup-dir)
-    (let [start (start-remote-node! cfg node)]
-      {:node node :action :storage-removed :stop stop :start start})))
+    {:node node :action :storage-removed :stop stop}))
 
 (defn restore-remote-storage! [cfg node]
   (let [data-dir (remote-node-data-dir cfg node)