Harden Ready advancement and KV durability

Author: lemon-mint

EPAXOS.MD

@@ -78,9 +78,11 @@ User commands are emitted to the embedding application through `Ready.Committed`
 
 ## Ready contract
 
-`Ready.Records` are durable consensus state. `Ready.Messages` are transport work. `Ready.Committed` contains user commands that have passed dependency execution and must be applied by the embedding application before they are acknowledged. The embedding application must persist records before sending messages from the same `Ready`. `MustSync` is true when durable records are present.
+`Ready.Records` are durable consensus state. `Ready.Messages` are transport work. `Ready.Committed` contains user commands that have passed dependency execution and must be applied by the embedding application before they are acknowledged. The embedding application must persist every record in a returned `Ready` before sending messages or acknowledging committed commands from that same batch. `MustSync` is true when durable records are present.
 
-`Advance` acknowledges the obligations in the previously returned `Ready`. For user commands, `Advance` queues the corresponding `StatusExecuted` records only after the application has observed `Ready.Committed`; those executed markers appear in a later `Ready.Records` batch and make replay after restart idempotent. Configuration changes and no-op commands do not appear in `Ready.Committed`; their executed records are queued internally when they execute.
+`Advance` returns an error and acknowledges only an exact prefix of the outstanding `Ready`. The acknowledged values must match the records, messages, committed commands, and `MustSync` bit returned by `Ready`; otherwise `Advance` returns `ErrInvalidReady` and leaves the outstanding batch unchanged for retry. A record-only prefix is valid, which lets storage persist part of a batch without marking application commands executed. `Messages` or `Committed` acknowledgements are accepted only after all earlier `Records` from that outstanding batch are acknowledged. When `MaxReadyMessages` caps `Ready.Messages`, records and committed commands still appear in full; after their successful acknowledgement the remaining message tail appears in later `Ready` batches with `MustSync` false.
+
+For user commands, `Advance` queues the corresponding `StatusExecuted` records only after the application has observed and acknowledged `Ready.Committed`; those executed markers appear in a later `Ready.Records` batch and make replay after restart idempotent. Configuration changes and no-op commands do not appear in `Ready.Committed`; their executed records are queued internally when they execute.
 
 ## Checksums and serialization
 

MODEL_EQ_REPORT.MD

@@ -6,19 +6,19 @@ This report maps the current finite TLA+ safety model to the current Go implemen
 
 | Model anchor | Implementation anchor | Evidence |
 | --- | --- | --- |
-| `tla/EPaxos.tla:32` TLA Init | `epaxos/node.go:98` Go node construction | Initialization sets empty instance state before transport steps; Go also restores durable state and configuration history before accepting input. |
+| `tla/EPaxos.tla:32` TLA Init | `epaxos/node.go:99` Go node construction | Initialization sets empty instance state before transport steps; Go also restores durable state and configuration history before accepting input. |
 | `tla/EPaxos.tla:9` TLA Conflicts | `epaxos/types.go:150` Go command conflict predicate and `examples/kv/kv.go:368` KV transaction command construction | The model configures command membership in conflict-key sets; Go conflicts commands by shared conflict-key bytes, and KV transactions deduplicate EPAXOS conflict keys while preserving every payload operation in order. |
-| `tla/EPaxos.tla:18` TLA SafeDeps | `epaxos/node.go:729` Go attribute computation | Both model and implementation require known conflicting commands to appear in dependency attributes. |
-| `tla/EPaxos.tla:42` TLA PreAccept | `epaxos/node.go:257` Go proposal path | Local proposal computes attributes, persists pre-accepted records, indexes conflicts, and emits pre-accept messages. |
-| `tla/EPaxos.tla:42` TLA PreAccept receive | `epaxos/node.go:422` Go pre-accept handler | Remote pre-accept merges local conflicts with proposer attributes and stores the pre-accepted value. |
-| `tla/EPaxos.tla:54` TLA Accept | `epaxos/node.go:478` Go accept handler | Accept stores slow-path attributes unless the instance is already committed or promised higher. |
-| `tla/EPaxos.tla:63` TLA Commit | `epaxos/node.go:522` Go commit handler | Commit stores final value/attributes and invokes dependency-closed execution. |
-| `tla/EPaxos.tla:69` TLA Prepare | `epaxos/node.go:535` 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:561` 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:836` Go executor and `epaxos/node.go:367` Ready acknowledgement | Execution collapses committed dependency SCCs; user commands are emitted through `Ready.Committed`, and durable `StatusExecuted` records are emitted only after `Advance` acknowledges application. |
-| `tla/EPaxos.tla:96` TLA DependencyClosure | `epaxos/node.go:936` 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:985` 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:237` Go logical tick | Tick advances logical time and dispatches logical timers; no wall-clock API is used in the core. |
+| `tla/EPaxos.tla:18` TLA SafeDeps | `epaxos/node.go:828` Go attribute computation | Both model and implementation require known conflicting commands to appear in dependency attributes. |
+| `tla/EPaxos.tla:42` TLA PreAccept | `epaxos/node.go:258` Go proposal path | Local proposal computes attributes, persists pre-accepted records, indexes conflicts, and emits pre-accept messages. |
+| `tla/EPaxos.tla:42` TLA PreAccept receive | `epaxos/node.go:521` Go pre-accept handler | Remote pre-accept merges local conflicts with proposer attributes and stores the pre-accepted value. |
+| `tla/EPaxos.tla:54` TLA Accept | `epaxos/node.go:577` Go accept handler | Accept stores slow-path attributes unless the instance is already committed or promised higher. |
+| `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: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. |
 | Not represented in current TLA safety model | `epaxos/checksum.go:65` Go record checksum | Durable record checksum coverage is implementation validation rather than modeled state. |
 | Not represented in current TLA safety model | `epaxos/checksum.go:84` Go message checksum | Transport checksum coverage is implementation validation rather than modeled state. |
 | Not represented in current TLA safety model | `epaxos/codec.go:41` Go decoder | Wire-decoder input tolerance and error-path destination cleanup are implementation validation rather than modeled state. |
@@ -30,15 +30,16 @@ This report maps the current finite TLA+ safety model to the current Go implemen
 
 ## Current verification evidence
 
-- Observed `tests/ci.sh` passing after the storage-fault hardening 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, allocation/pool ownership assertions, decoder fuzz seeds, 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, 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 `Advance` at 100.0% after the executed-record acknowledgement cap test.
+- Observed `tests/ci.sh` passing after the strict Ready acknowledgement and durable in-process cluster 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, 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 `Advance`, `validateReadyAck`, `commandEqual`, and `instanceNumsEqual` at 100.0% after strict acknowledgement mismatch tests.
+- 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 26 tests with 67 assertions for register delete normalization, indeterminate mutation response classification, transaction body encoding, grouped reads, scan shape checking, restart fault selection, transport fault selection, storage fault selection, client/nemesis routing, restart nemesis behavior, transport nemesis control requests, and storage nemesis control requests.
-- Observed `tests/ci.sh` local transport profile reporting register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 11, :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 register `:linearizable {:valid? true}`, scan shape `:scan-shape {:valid? true, :checked 6, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 2, :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 5, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 5, :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 13, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 4, :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 9, :bad-count 0}`, transaction `:txn-atomic {:valid? true, :checked 9, :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

README.md

@@ -1,6 +1,6 @@
 # moreconsensus
 
-`moreconsensus` is a Go library for building replicated services with Egalitarian Paxos (EPaxos). The public API follows the shape of etcd raft: applications drive a deterministic `RawNode`, persist `Ready` records, send `Ready` messages, apply committed commands, and then call `Advance`.
+`moreconsensus` is a Go library for building replicated services with Egalitarian Paxos (EPaxos). The public API follows the shape of etcd raft: applications drive a deterministic `RawNode`, persist `Ready` records, send `Ready` messages, apply committed commands, and then call `Advance` with the acknowledged `Ready` prefix.
 
 ## Core features
 

epaxos/branch_test.go

@@ -50,7 +50,9 @@ func TestConstructionAndReadyBranches(t *testing.T) {
 	if !rn.Ready().Empty() {
 		t.Fatal("empty ready should be empty")
 	}
-	rn.Advance(Ready{})
+	if err := rn.Advance(Ready{}); err != nil {
+		t.Fatal(err)
+	}
 	if _, err := rn.Propose(Command{Kind: CommandConfChange}); err == nil {
 		t.Fatal("expected conf command rejection")
 	}
@@ -64,8 +66,15 @@ func TestConstructionAndReadyBranches(t *testing.T) {
 	if !rn.Ready().Empty() {
 		t.Fatal("ready while awaiting advance should be empty")
 	}
-	rn.Advance(Ready{Records: rd.Records[:1]})
-	rn.Advance(rd)
+	if err := rn.Advance(Ready{Records: rd.Records[:1], MustSync: rd.MustSync}); err != nil {
+		t.Fatal(err)
+	}
+	tail := rn.Ready()
+	if !tail.Empty() {
+		if err := rn.Advance(tail); err != nil {
+			t.Fatal(err)
+		}
+	}
 }
 
 func TestDirectProtocolBranches(t *testing.T) {

epaxos/internal_test.go

@@ -181,7 +181,9 @@ func TestRejectPathsAndTimers(t *testing.T) {
 	if err := s.nodes[msg.To].Step(lowAccept); err != nil {
 		t.Fatal(err)
 	}
-	s.nodes[1].Advance(rd)
+	if err := s.nodes[1].Advance(rd); err != nil {
+		t.Fatal(err)
+	}
 	inst := s.nodes[1].instances[ref]
 	s.nodes[1].onTimer(inst, timerPreAccept)
 	s.nodes[1].startAccept(inst, inst.rec.Attributes())

epaxos/node.go

@@ -1,6 +1,7 @@
 package epaxos
 
 import (
+	"bytes"
 	"container/heap"
 	"encoding/binary"
 	"fmt"
@@ -363,15 +364,18 @@ func (n *RawNode) Ready() Ready {
 	return rd
 }
 
-// Advance acknowledges that the caller persisted and applied the Ready batch.
-func (n *RawNode) Advance(rd Ready) {
+// Advance acknowledges a prefix of the outstanding Ready batch or returns ErrInvalidReady without mutating node state.
+func (n *RawNode) Advance(rd Ready) error {
 	if !n.awaitAdvance {
-		return
+		if rd.Empty() {
+			return nil
+		}
+		return ErrInvalidReady
 	}
-	ackedCommitted := len(rd.Committed)
-	if ackedCommitted > len(n.pendingReady.Committed) {
-		ackedCommitted = len(n.pendingReady.Committed)
+	if err := n.validateReadyAck(rd); err != nil {
+		return err
 	}
+	ackedCommitted := len(rd.Committed)
 	if len(rd.Records) >= len(n.pendingReady.Records) {
 		n.pendingReady.Records = nil
 	} else {
@@ -390,6 +394,101 @@ func (n *RawNode) Advance(rd Ready) {
 	n.pendingReady.MustSync = len(n.pendingReady.Records) > 0
 	n.enqueueExecutedRecords(rd.Committed[:ackedCommitted])
 	n.awaitAdvance = false
+	return nil
+}
+
+func (n *RawNode) validateReadyAck(rd Ready) error {
+	if len(rd.Records) == 0 && len(rd.Messages) == 0 && len(rd.Committed) == 0 {
+		return ErrInvalidReady
+	}
+	if rd.MustSync != n.pendingReady.MustSync {
+		return ErrInvalidReady
+	}
+	if len(rd.Records) > len(n.pendingReady.Records) || len(rd.Committed) > len(n.pendingReady.Committed) {
+		return ErrInvalidReady
+	}
+	visibleMessages := len(n.pendingReady.Messages)
+	if n.maxReadyMessages > 0 && visibleMessages > n.maxReadyMessages {
+		visibleMessages = n.maxReadyMessages
+	}
+	if len(rd.Messages) > visibleMessages {
+		return ErrInvalidReady
+	}
+	if (len(rd.Messages) > 0 || len(rd.Committed) > 0) && len(rd.Records) != len(n.pendingReady.Records) {
+		return ErrInvalidReady
+	}
+	for i := range rd.Records {
+		if !instanceRecordEqual(rd.Records[i], n.readyRecord(n.pendingReady.Records[i])) {
+			return ErrInvalidReady
+		}
+	}
+	for i := range rd.Messages {
+		if !messageEqual(rd.Messages[i], n.pendingReady.Messages[i].Clone()) {
+			return ErrInvalidReady
+		}
+	}
+	for i := range rd.Committed {
+		if !committedCommandEqual(rd.Committed[i], n.pendingReady.Committed[i].Clone()) {
+			return ErrInvalidReady
+		}
+	}
+	return nil
+}
+
+func instanceRecordEqual(a, b InstanceRecord) bool {
+	return a.Ref == b.Ref &&
+		a.Ballot == b.Ballot &&
+		a.Status == b.Status &&
+		a.Seq == b.Seq &&
+		a.Checksum == b.Checksum &&
+		instanceNumsEqual(a.Deps, b.Deps) &&
+		commandEqual(a.Command, b.Command)
+}
+
+func messageEqual(a, b Message) bool {
+	return a.Type == b.Type &&
+		a.From == b.From &&
+		a.To == b.To &&
+		a.Ref == b.Ref &&
+		a.Ballot == b.Ballot &&
+		a.Seq == b.Seq &&
+		a.Reject == b.Reject &&
+		a.RejectHint == b.RejectHint &&
+		a.RecordStatus == b.RecordStatus &&
+		a.Checksum == b.Checksum &&
+		instanceNumsEqual(a.Deps, b.Deps) &&
+		commandEqual(a.Command, b.Command)
+}
+
+func committedCommandEqual(a, b CommittedCommand) bool {
+	return a.Ref == b.Ref &&
+		a.Seq == b.Seq &&
+		instanceNumsEqual(a.Deps, b.Deps) &&
+		commandEqual(a.Command, b.Command)
+}
+
+func commandEqual(a, b Command) bool {
+	if a.ID != b.ID || a.Kind != b.Kind || !bytes.Equal(a.Payload, b.Payload) || len(a.ConflictKeys) != len(b.ConflictKeys) {
+		return false
+	}
+	for i := range a.ConflictKeys {
+		if !bytes.Equal(a.ConflictKeys[i], b.ConflictKeys[i]) {
+			return false
+		}
+	}
+	return true
+}
+
+func instanceNumsEqual(a, b []InstanceNum) bool {
+	if len(a) != len(b) {
+		return false
+	}
+	for i := range a {
+		if a[i] != b[i] {
+			return false
+		}
+	}
+	return true
 }
 
 func (n *RawNode) enqueueExecutedRecords(committed []CommittedCommand) {