You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: MODEL_EQ_REPORT.MD
+9-8Lines changed: 9 additions & 8 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -26,22 +26,23 @@ This report maps the current finite TLA+ safety model to the current Go implemen
26
26
|`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. |
27
27
|`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. |
28
28
| 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. |
29
-
| Not represented in current TLA safety model |`examples/kv/cmd/kvnode/main.go:259` transport fault control and `jepsen/src/moreconsensus/epaxos_test.clj:183` transport nemesis| Local transport partition control is an external validation mechanism for the KV example and Jepsen workload rather than modeled state. |
29
+
| 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. |
30
30
31
31
## Current verification evidence
32
32
33
-
- Observed `tests/ci.sh` passing after the 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, the local Jepsen restart profile, and the repository text audit.
33
+
- 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.
34
34
- 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.
35
-
- 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, and transport fault-route coverage.
35
+
- 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.
36
36
- 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.
37
37
- 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.
38
-
- Observed targeted `lein test moreconsensus.epaxos-test-test` from `jepsen` passing 22 tests with 57 assertions for register delete normalization, indeterminate mutation response classification, transaction body encoding, grouped reads, scan shape checking, restart fault selection, transport fault selection, client/nemesis routing, restart nemesis behavior, and transport nemesis control requests.
- Observed repository text audit with no disallowed external-project name, scaffolding marker, or wall-clock API matches.
42
43
43
44
## Open correspondence risks
44
45
45
46
- The TLA+ model is finite-bounded for TLC, so it demonstrates correspondence for the configured state space rather than unbounded proof.
46
-
- Checksum, wire-decoder tolerance, storage virtualization, recovery response collection, transport fault control, and example KV apply/scan storage semantics are verified by implementation and Jepsen tests but outside the current TLA safety state.
47
-
- Local Jepsen now covers loopback process restart and transport partitionprofiles, but it still lacks SSH-managed multi-host deployment, disk-fault nemeses, and long-duration operational coverage.
47
+
- 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.
48
+
- Local Jepsen now covers loopback process restart, transport partition, and storage-unavailable profiles, but it still lacks SSH-managed multi-host deployment, destructive disk nemeses, and long-duration operational coverage.
0 commit comments