Cover Revisited fast-wait commit path

Author: lemon-mint

MODEL_EQ_REPORT.MD

@@ -15,7 +15,8 @@ This report maps the current finite TLA+ safety model to the current Go implemen
 | `tla/EPaxos.tla:63` TLA Commit | `epaxos/node.go:621` Go commit handler | Commit stores final value/attributes and invokes dependency-closed execution. |
 | `tla/EPaxos.tla:69` TLA Prepare | `epaxos/node.go:634` 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:660` 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:935` Go executor and `epaxos/node.go:368` Ready acknowledgement | Execution collapses committed dependency SCCs; user commands are emitted through `Ready.Committed`, and durable `StatusExecuted` records are emitted only after `Advance` validates the acknowledged Ready prefix and acknowledges application. |
+| `tla/EPaxos.tla:76` TLA Execute | `epaxos/node.go:935` 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:368` Advance and `epaxos/node.go:494` enqueueExecutedRecords | Ready acknowledgement, exact-prefix validation, and delayed durable `StatusExecuted` emission are implementation validation rather than modeled state. |
 | `tla/EPaxos.tla:96` TLA DependencyClosure | `epaxos/node.go:1035` 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:1084` 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. |
 | `tla/EPaxos.tla:83` TLA Tick | `epaxos/node.go:238` Go logical tick | Tick advances logical time and dispatches logical timers; no wall-clock API is used in the core. |
@@ -26,25 +27,25 @@ 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:196` transport nemesis, and `jepsen/src/moreconsensus/epaxos_test.clj:224` storage nemesis | Local transport partition and storage-unavailable 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:227` transport nemesis, and `jepsen/src/moreconsensus/epaxos_test.clj:255` storage nemesis | Local transport partition and storage-unavailable 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, and checksum pooling 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, and 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, 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 `tests/ci.sh` passing after the strict Ready acknowledgement, durable in-process cluster, restart health-probe, reusable decode scratch, checksum pooling, and late fast-quorum Revisited coverage 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, and 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, 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 `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 28 tests with 73 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, client/nemesis routing, restart nemesis behavior, transport nemesis control requests, and storage nemesis control requests.
 - Observed focused `bash tests/jepsen_local.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 4, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 2, :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 2, :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 16, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 8, :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 6, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 5, :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 5, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 1, :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 17, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 5, :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 15, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 10, :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.
-- Checksum, wire-decoder tolerance, storage virtualization, recovery response collection, transport fault control, storage fault control, and example KV apply/scan storage semantics are verified by implementation and Jepsen tests but outside the current TLA safety state.
+- Ready acknowledgement, delayed durable execution markers, checksum, wire-decoder tolerance, storage virtualization, recovery response collection, transport fault control, storage fault control, 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, and storage-unavailable profiles, but it still lacks SSH-managed multi-host deployment, destructive disk nemeses, and long-duration operational coverage.

epaxos/remaining_test.go

@@ -312,6 +312,115 @@ func TestTimeOptimizationDelaysSlowAcceptUntilFastWaitTick(t *testing.T) {
 	}
 }
 
+func TestTimeOptimizationLateFastQuorumCommitsWithoutAccept(t *testing.T) {
+	store := NewMemoryStorage()
+	rn, err := NewRawNode(Config{ID: 1, Voters: makeIDs(5), Storage: store, RetryTicks: 10, TimeOptimization: true, TimeOptimizationTicks: 3})
+	if err != nil {
+		t.Fatal(err)
+	}
+	cmd := Command{ID: CommandID{Client: 8, Sequence: 1}, Payload: []byte("late-fast-value"), ConflictKeys: [][]byte{[]byte("late-fast-key")}}
+	ref, err := rn.Propose(cmd)
+	if err != nil {
+		t.Fatal(err)
+	}
+	rd := rn.Ready()
+	if len(rd.Messages) != 4 {
+		t.Fatalf("initial preaccept messages = %#v", rd.Messages)
+	}
+	if err := store.ApplyReady(rd); err != nil {
+		t.Fatal(err)
+	}
+	advanceOK(t, rn, rd)
+
+	inst := rn.instances[ref]
+	if inst == nil {
+		t.Fatalf("missing local instance %s", ref)
+	}
+	stepMatchingPreAcceptResp := func(from ReplicaID) {
+		t.Helper()
+		resp := Message{
+			Type:         MsgPreAcceptResp,
+			From:         from,
+			To:           1,
+			Ref:          ref,
+			Ballot:       inst.rec.Ballot,
+			Seq:          inst.rec.Seq,
+			Deps:         append([]InstanceNum(nil), inst.rec.Deps...),
+			RecordStatus: StatusPreAccepted,
+		}
+		if err := rn.Step(resp); err != nil {
+			t.Fatalf("step matching preaccept response from %d: %v", from, err)
+		}
+	}
+
+	for _, from := range []ReplicaID{2, 3} {
+		stepMatchingPreAcceptResp(from)
+	}
+	if got, slow, fast := len(inst.preOK), rn.q.slowQuorum(), rn.q.fastQuorum(); got != slow || got >= fast {
+		t.Fatalf("preaccept votes = %d, want slow quorum %d below fast quorum %d", got, slow, fast)
+	}
+	if inst.phase != phasePreAccept {
+		t.Fatalf("phase after slow quorum preaccept responses = %d, want preaccept", inst.phase)
+	}
+	if rn.HasReady() {
+		t.Fatalf("slow quorum response produced ready work before fast-wait deadline: %#v", rn.Ready())
+	}
+
+	for tick := uint64(1); tick < 3; tick++ {
+		rn.Tick()
+		if inst.phase != phasePreAccept {
+			t.Fatalf("phase after tick %d = %d, want preaccept before fast-wait deadline", tick, inst.phase)
+		}
+		if rn.HasReady() {
+			t.Fatalf("ready work appeared after tick %d before fast-wait deadline: %#v", tick, rn.Ready())
+		}
+	}
+
+	stepMatchingPreAcceptResp(4)
+	if got, fast := len(inst.preOK), rn.q.fastQuorum(); got != fast {
+		t.Fatalf("preaccept votes after late response = %d, want fast quorum %d", got, fast)
+	}
+	if inst.phase != phaseCommitted {
+		t.Fatalf("phase after late fast-quorum response = %d, want committed", inst.phase)
+	}
+	if inst.rec.Status != StatusExecuted {
+		t.Fatalf("instance status after dependency-ready commit = %s, want executed", inst.rec.Status)
+	}
+
+	rd = rn.Ready()
+	if len(rd.Records) != 1 || rd.Records[0].Ref != ref || rd.Records[0].Status != StatusCommitted {
+		t.Fatalf("late fast-quorum ready records = %#v, want committed record for %s", rd.Records, ref)
+	}
+	if len(rd.Messages) != 4 {
+		t.Fatalf("late fast-quorum commit messages = %#v", rd.Messages)
+	}
+	seen := make(map[ReplicaID]bool, 4)
+	for _, msg := range rd.Messages {
+		if msg.Type == MsgAccept {
+			t.Fatalf("late fast-quorum response emitted accept message: %#v", msg)
+		}
+		if msg.Type != MsgCommit || msg.From != 1 || msg.Ref != ref || msg.RecordStatus != StatusCommitted {
+			t.Fatalf("late fast-quorum message = %#v, want commit for %s from replica 1", msg, ref)
+		}
+		seen[msg.To] = true
+	}
+	for _, to := range []ReplicaID{2, 3, 4, 5} {
+		if !seen[to] {
+			t.Fatalf("missing commit message to replica %d in %#v", to, rd.Messages)
+		}
+	}
+	if len(rd.Committed) != 1 {
+		t.Fatalf("late fast-quorum committed commands = %#v, want one command", rd.Committed)
+	}
+	committed := requireCommittedForRef(t, rd, ref)
+	if committed.Command.Kind != CommandUser || committed.Command.ID != cmd.ID || !bytes.Equal(committed.Command.Payload, cmd.Payload) {
+		t.Fatalf("committed command = %#v, want user command %#v", committed.Command, cmd)
+	}
+	if len(committed.Command.ConflictKeys) != 1 || !bytes.Equal(committed.Command.ConflictKeys[0], cmd.ConflictKeys[0]) {
+		t.Fatalf("committed conflict keys = %#v, want %#v", committed.Command.ConflictKeys, cmd.ConflictKeys)
+	}
+}
+
 func TestRemainingResponseBranches(t *testing.T) {
 	rn, err := NewRawNode(Config{ID: 1, Voters: makeIDs(3)})
 	if err != nil {