From 50a23d5a14919e0572277a5f233b864f8b513dff Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Mon, 4 Nov 2024 14:53:50 +0300
Subject: [PATCH] Move CommittedNotTruncated

---
 safekeeper/spec/ProposerAcceptorStatic.tla    | 29 ++++++++++++-------
 .../MCProposerAcceptorStatic_p2_a5_t2_l2.cfg  |  1 -
 .../MCProposerAcceptorStatic_p2_a5_t3_l3.cfg  |  1 -
 3 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla
index 40b6f4cd31..7de8a0cbd3 100644
--- a/safekeeper/spec/ProposerAcceptorStatic.tla
+++ b/safekeeper/spec/ProposerAcceptorStatic.tla
@@ -382,17 +382,6 @@ LogIsMonotonic ==
 LogSafety ==
     \A c1, c2 \in committed: (c1.lsn = c2.lsn) => (c1 = c2)
 
-\* Sanity check: TruncateWal must never delete committed record.
-CommittedNotTruncated ==
-    \A p \in proposers: \A a \in acceptors:
-      (/\ prop_state[p].state = "leader"
-       /\ prop_state[p].term = acc_state[a].term) =>
-         LET
-            hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a))
-            truncated_lsns == {lsn \in DOMAIN acc_state[a].wal: lsn >= hcp.lsn}
-            truncated_records == {[term |-> acc_state[a].wal[lsn], lsn |-> lsn]: lsn \in truncated_lsns}
-         IN
-            \A r \in truncated_records: r \notin committed
 
 \********************************************************************************
 \* Invariants which don't need to hold, but useful for playing/debugging.
@@ -419,4 +408,22 @@ MaxTruncatedTerms ==
             truncated_records_terms == {acc_state[a].wal[lsn]: lsn \in truncated_lsns}
          IN
             Cardinality(truncated_records_terms) < 2
+
+\* Check that TruncateWal never deletes committed record.
+\* It might seem that this should an invariant, but it is not.
+\* With 5 nodes, it is legit to truncate record which had been
+\* globally committed: e.g. nodes abc can commit record of term 1 in 
+\* term 3, and after that leader of term 2 can delete such record 
+\* on d. On 10 cores TLC can find such a trace in ~7 hours.
+CommittedNotTruncated ==
+    \A p \in proposers: \A a \in acceptors:
+      (/\ prop_state[p].state = "leader"
+       /\ prop_state[p].term = acc_state[a].term) =>
+         LET
+            hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a))
+            truncated_lsns == {lsn \in DOMAIN acc_state[a].wal: lsn >= hcp.lsn}
+            truncated_records == {[term |-> acc_state[a].wal[lsn], lsn |-> lsn]: lsn \in truncated_lsns}
+         IN
+            \A r \in truncated_records: r \notin committed
+
 ====
diff --git a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t2_l2.cfg b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t2_l2.cfg
index d418ddf45f..ebf4724633 100644
--- a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t2_l2.cfg
+++ b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t2_l2.cfg
@@ -11,7 +11,6 @@ TypeOk
 ElectionSafety
 LogIsMonotonic
 LogSafety
-CommittedNotTruncated
 SYMMETRY ProposerAcceptorSymmetry
 CHECK_DEADLOCK FALSE
 ALIAS Alias
diff --git a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t3_l3.cfg b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t3_l3.cfg
index a81dc9cde1..bb77350c58 100644
--- a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t3_l3.cfg
+++ b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a5_t3_l3.cfg
@@ -11,7 +11,6 @@ TypeOk
 ElectionSafety
 LogIsMonotonic
 LogSafety
-\* CommittedNotTruncated
 SYMMETRY ProposerAcceptorSymmetry
 CHECK_DEADLOCK FALSE
 ALIAS Alias