From f6209b2f59d30b3d6ed12bd4b66beffb6b13ffed Mon Sep 17 00:00:00 2001 From: Jason Stiebs Date: Fri, 11 Sep 2026 12:30:08 -0500 Subject: [PATCH 1/2] Retain snapshot commit evidence after installation --- test/formal/README.md | 11 +++++- test/formal/SnapshotAssembly.tla | 31 +++++++++------ test/formal/check_matrix.sh | 2 +- test/formal/check_snapshot_commit.exs | 54 +++++++++++++++++++++++++++ 4 files changed, 84 insertions(+), 14 deletions(-) create mode 100644 test/formal/check_snapshot_commit.exs diff --git a/test/formal/README.md b/test/formal/README.md index 7eae990..dc4e4e0 100644 --- a/test/formal/README.md +++ b/test/formal/README.md @@ -19,6 +19,12 @@ at a previously committed exact state until every chunk and a valid terminal commit for one snapshot are present; stale or mixed partial state can never become visible. +The commit invariant retains the last installation's commit evidence separately +from disposable staging. The formal matrix also removes the terminal-commit guard +in an isolated copy and requires TLC to reject it specifically with +`NoCommitMeansNoInstall`. A surviving mutant, parser error, or runtime failure +fails this qualification. + `PeerEviction.tla` isolates the lifecycle boundary for a peer which never returns and for a later process using the same node name with a fresh generation. During its finite faulty prefix it retains and reorders stale @@ -66,9 +72,12 @@ TLA_JAR=/path/to/tla2tools.jar \ TLA_CONFIG="$PWD/test/formal/SnapshotAssembly.cfg" \ test/formal/check.sh -# Run all default models +# Run all default models and snapshot commit qualification (also requires Elixir) TLA_JAR=/path/to/tla2tools.jar test/formal/check_matrix.sh +# Run only snapshot assembly and its negative commit qualification +TLA_JAR=/path/to/tla2tools.jar elixir test/formal/check_snapshot_commit.exs + # Also run the larger two-key, three-sequence anti-entropy state space TLA_JAR=/path/to/tla2tools.jar TLA_EXTENDED=1 test/formal/check_matrix.sh ``` diff --git a/test/formal/SnapshotAssembly.tla b/test/formal/SnapshotAssembly.tla index ce75e21..6fb5fd2 100644 --- a/test/formal/SnapshotAssembly.tla +++ b/test/formal/SnapshotAssembly.tla @@ -44,6 +44,7 @@ Message == VARIABLES authorityEpoch, cursor, visible, + installedCommitted, stagedSnapshot, stagedChunks, stagedRows, @@ -52,13 +53,14 @@ VARIABLES authorityEpoch, messages vars == - <> Init == /\ authorityEpoch = 1 /\ cursor = 0 /\ visible = {} + /\ installedCommitted = TRUE /\ stagedSnapshot = 0 /\ stagedChunks = {} /\ stagedRows = {} @@ -69,20 +71,20 @@ Init == SendChunk(snapshot, chunk) == /\ messages' = messages \union {[kind |-> "chunk", snapshot |-> snapshot, chunk |-> chunk]} - /\ UNCHANGED <> SendCommit(snapshot) == /\ snapshot \in commitAllowed /\ messages' = messages \union {[kind |-> "commit", snapshot |-> snapshot, chunk |-> 0]} - /\ UNCHANGED <> InvalidateBeforeCommit(snapshot) == /\ snapshot \in commitAllowed /\ commitAllowed' = commitAllowed \ {snapshot} - /\ UNCHANGED <> Valid(snapshot) == @@ -102,7 +104,7 @@ StartChunk(message) == /\ stagedChunks' = {message.chunk} /\ stagedRows' = ChunkRows(message.snapshot, message.chunk) /\ stagedCommitted' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> StartCommit(message) == /\ message.kind = "commit" @@ -111,7 +113,7 @@ StartCommit(message) == /\ stagedChunks' = {} /\ stagedRows' = {} /\ stagedCommitted' = TRUE - /\ UNCHANGED <> + /\ UNCHANGED <> ContinueChunk(message) == /\ message.kind = "chunk" @@ -122,11 +124,13 @@ ContinueChunk(message) == IN IF stagedCommitted /\ nextChunks = Chunks THEN /\ cursor' = SnapshotSeq(message.snapshot) /\ visible' = SnapshotRows(message.snapshot) + (* Retain the actual pre-install evidence after staging is cleared. *) + /\ installedCommitted' = stagedCommitted /\ stagedSnapshot' = 0 /\ stagedChunks' = {} /\ stagedRows' = {} /\ stagedCommitted' = FALSE - ELSE /\ UNCHANGED <> + ELSE /\ UNCHANGED <> /\ stagedChunks' = nextChunks /\ stagedRows' = nextRows /\ UNCHANGED <> @@ -138,12 +142,14 @@ ContinueCommit(message) == /\ IF stagedChunks = Chunks THEN /\ cursor' = SnapshotSeq(message.snapshot) /\ visible' = SnapshotRows(message.snapshot) + (* This transition delivers the terminal commit itself. *) + /\ installedCommitted' = TRUE /\ stagedSnapshot' = 0 /\ stagedChunks' = {} /\ stagedRows' = {} /\ stagedCommitted' = FALSE ELSE /\ stagedCommitted' = TRUE - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> Ignore(message) == @@ -163,7 +169,7 @@ Deliver(message) == Drop(message) == /\ message \in messages /\ messages' = messages \ {message} - /\ UNCHANGED <> InstallNewAuthority == @@ -171,6 +177,7 @@ InstallNewAuthority == /\ authorityEpoch' = 2 /\ cursor' = 0 /\ visible' = {} + /\ installedCommitted' = TRUE (* Invisible old staging may remain until expiry, but can never commit. *) /\ UNCHANGED <> @@ -181,7 +188,7 @@ DiscardStaging == /\ stagedChunks' = {} /\ stagedRows' = {} /\ stagedCommitted' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> Next == \/ \E snapshot \in Snapshots, chunk \in Chunks : SendChunk(snapshot, chunk) @@ -196,6 +203,7 @@ TypeOK == /\ authorityEpoch \in {1, 2} /\ cursor \in 0..2 /\ visible \subseteq Rows + /\ installedCommitted \in BOOLEAN /\ stagedSnapshot \in {0} \union Snapshots /\ stagedChunks \subseteq Chunks /\ stagedRows \subseteq Rows @@ -217,8 +225,7 @@ StagingBelongsToOneSnapshot == stagedRows = UNION {ChunkRows(stagedSnapshot, chunk) : chunk \in stagedChunks} NoCommitMeansNoInstall == - stagedSnapshot # 0 /\ ~stagedCommitted => - SnapshotSeq(stagedSnapshot) > cursor + installedCommitted Spec == Init /\ [][Next]_vars diff --git a/test/formal/check_matrix.sh b/test/formal/check_matrix.sh index 19521e9..68419de 100755 --- a/test/formal/check_matrix.sh +++ b/test/formal/check_matrix.sh @@ -14,7 +14,7 @@ run_check() { } run_check GroupAntiEntropy GroupAntiEntropy -run_check SnapshotAssembly SnapshotAssembly +elixir "${script_dir}/check_snapshot_commit.exs" run_check PeerEviction PeerEviction run_check AuthorityProjection AuthorityProjection run_check AuthorityHint AuthorityHint diff --git a/test/formal/check_snapshot_commit.exs b/test/formal/check_snapshot_commit.exs new file mode 100644 index 0000000..8c57c33 --- /dev/null +++ b/test/formal/check_snapshot_commit.exs @@ -0,0 +1,54 @@ +defmodule Group.Formal.SnapshotCommitQualification do + @moduledoc false + + def run do + directory = __DIR__ + spec = Path.join(directory, "SnapshotAssembly.tla") + config = Path.join(directory, "SnapshotAssembly.cfg") + check = Path.join(directory, "check.sh") + + run_check!(check, spec, config, 0) + + source = File.read!(spec) + guard = "IN IF stagedCommitted /\\ nextChunks = Chunks" + + unless length(:binary.matches(source, guard)) == 1 do + raise "snapshot commit mutation must match exactly one installation guard" + end + + artifacts = + Path.expand( + "../../tmp/formal/snapshot-commit-#{System.pid()}-#{System.unique_integer([:positive])}", + directory + ) + + File.mkdir_p!(artifacts) + mutant = Path.join(artifacts, "SnapshotAssembly.tla") + mutant_config = Path.join(artifacts, "SnapshotAssembly.cfg") + File.write!(mutant, String.replace(source, guard, "IN IF nextChunks = Chunks")) + + # Isolate this obligation: another invariant must not receive credit for + # detecting the missing commit, nor may a parse/runtime failure count as a kill. + File.write!(mutant_config, "SPECIFICATION Spec\nINVARIANT NoCommitMeansNoInstall\n") + + # TLC's stable VIOLATION_SAFETY exit status, not an error-message match. + run_check!(check, mutant, mutant_config, 12) + IO.puts("snapshot commit invariant rejects installation without a terminal commit") + IO.puts("qualification artifacts: #{artifacts}") + end + + defp run_check!(check, spec, config, expected_status) do + {_output, status} = + System.cmd("bash", [check], + env: [{"TLA_SPEC", spec}, {"TLA_CONFIG", config}], + into: IO.stream(), + stderr_to_stdout: true + ) + + unless status == expected_status do + raise "TLC exited #{status}, expected #{expected_status} for #{spec}" + end + end +end + +Group.Formal.SnapshotCommitQualification.run() From ec70081134f165558967d80ea001d145664a7a49 Mon Sep 17 00:00:00 2001 From: Jason Stiebs Date: Fri, 11 Sep 2026 16:12:47 -0500 Subject: [PATCH 2/2] Exclude formal qualification scripts from ExUnit discovery --- mix.exs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mix.exs b/mix.exs index f9b9580..09ab78e 100644 --- a/mix.exs +++ b/mix.exs @@ -10,7 +10,7 @@ defmodule Group.MixProject do version: @version, elixir: "~> 1.19", elixirc_paths: elixirc_paths(Mix.env()), - test_ignore_filters: [~r"^test/jepsen/", ~r"^test/mutation/"], + test_ignore_filters: [~r"^test/jepsen/", ~r"^test/mutation/", ~r"^test/formal/"], start_permanent: Mix.env() == :prod, deps: deps(), aliases: aliases(),