Retain snapshot commit evidence after installation

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(),

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
 ```

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 ==
-  <<authorityEpoch, cursor, visible, stagedSnapshot, stagedChunks,
+  <<authorityEpoch, cursor, visible, installedCommitted, stagedSnapshot, stagedChunks,
     stagedRows, stagedCommitted, commitAllowed, messages>>
 
 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 <<authorityEpoch, cursor, visible, stagedSnapshot,
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, stagedSnapshot,
                  stagedChunks, stagedRows, stagedCommitted, commitAllowed>>
 
 SendCommit(snapshot) ==
   /\ snapshot \in commitAllowed
   /\ messages' = messages \union
        {[kind |-> "commit", snapshot |-> snapshot, chunk |-> 0]}
-  /\ UNCHANGED <<authorityEpoch, cursor, visible, stagedSnapshot,
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, stagedSnapshot,
                  stagedChunks, stagedRows, stagedCommitted, commitAllowed>>
 
 InvalidateBeforeCommit(snapshot) ==
   /\ snapshot \in commitAllowed
   /\ commitAllowed' = commitAllowed \ {snapshot}
-  /\ UNCHANGED <<authorityEpoch, cursor, visible, stagedSnapshot,
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, stagedSnapshot,
                  stagedChunks, stagedRows, stagedCommitted, messages>>
 
 Valid(snapshot) ==
@@ -102,7 +104,7 @@ StartChunk(message) ==
   /\ stagedChunks' = {message.chunk}
   /\ stagedRows' = ChunkRows(message.snapshot, message.chunk)
   /\ stagedCommitted' = FALSE
-  /\ UNCHANGED <<authorityEpoch, cursor, visible, commitAllowed, messages>>
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, commitAllowed, messages>>
 
 StartCommit(message) ==
   /\ message.kind = "commit"
@@ -111,7 +113,7 @@ StartCommit(message) ==
   /\ stagedChunks' = {}
   /\ stagedRows' = {}
   /\ stagedCommitted' = TRUE
-  /\ UNCHANGED <<authorityEpoch, cursor, visible, commitAllowed, messages>>
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, commitAllowed, messages>>
 
 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 <<cursor, visible, stagedSnapshot, stagedCommitted>>
+        ELSE /\ UNCHANGED <<cursor, visible, installedCommitted, stagedSnapshot, stagedCommitted>>
              /\ stagedChunks' = nextChunks
              /\ stagedRows' = nextRows
   /\ UNCHANGED <<authorityEpoch, commitAllowed, messages>>
@@ -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 <<cursor, visible, stagedSnapshot, stagedChunks, stagedRows>>
+          /\ UNCHANGED <<cursor, visible, installedCommitted, stagedSnapshot, stagedChunks, stagedRows>>
   /\ UNCHANGED <<authorityEpoch, commitAllowed, messages>>
 
 Ignore(message) ==
@@ -163,14 +169,15 @@ Deliver(message) ==
 Drop(message) ==
   /\ message \in messages
   /\ messages' = messages \ {message}
-  /\ UNCHANGED <<authorityEpoch, cursor, visible, stagedSnapshot,
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, stagedSnapshot,
                  stagedChunks, stagedRows, stagedCommitted, commitAllowed>>
 
 InstallNewAuthority ==
   /\ authorityEpoch = 1
   /\ authorityEpoch' = 2
   /\ cursor' = 0
   /\ visible' = {}
+  /\ installedCommitted' = TRUE
   (* Invisible old staging may remain until expiry, but can never commit. *)
   /\ UNCHANGED <<stagedSnapshot, stagedChunks, stagedRows, stagedCommitted,
                  commitAllowed, messages>>
@@ -181,7 +188,7 @@ DiscardStaging ==
   /\ stagedChunks' = {}
   /\ stagedRows' = {}
   /\ stagedCommitted' = FALSE
-  /\ UNCHANGED <<authorityEpoch, cursor, visible, commitAllowed, messages>>
+  /\ UNCHANGED <<authorityEpoch, cursor, visible, installedCommitted, commitAllowed, messages>>
 
 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
 

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

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()