From a9ced3573a75e8bc0789b1f664db7d56dadd5ad4 Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Fri, 1 Nov 2024 13:38:39 +0300
Subject: [PATCH] Add CommittedNotTruncated

---
 safekeeper/spec/ProposerAcceptorStatic.tla    | 27 +++++++++----------
 .../MCProposerAcceptorStatic_p2_a3_t2_l2.cfg  |  2 +-
 safekeeper/spec/readme.md                     |  7 +++++
 3 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla
index 4930240f24..010f63f630 100644
--- a/safekeeper/spec/ProposerAcceptorStatic.tla
+++ b/safekeeper/spec/ProposerAcceptorStatic.tla
@@ -234,8 +234,8 @@ UpdateTerm(p, a) ==
   /\ acc_state' = [acc_state EXCEPT ![a].term = prop_state[p].term]
   /\ UNCHANGED <<prop_state, committed>>
 
-\* Find highest common point in the logs of proposer p and acceptor a.
-\* Returns <term, lsn> of the highest common point.
+\* Find highest common point (LSN of the first divergent record) in the logs of
+\* proposer p and acceptor a. Returns <term, lsn> of the highest common point.
 FindHighestCommonPoint(prop_th, acc_th, acc_flush_lsn) ==
     LET
       \* First find index of the highest common term. 
@@ -362,18 +362,17 @@ LogIsMonotonic ==
 LogSafety ==
     \A c1, c2 \in committed: (c1.lsn = c2.lsn) => (c1 = c2)
 
-\* \* Next record we are going to push to acceptor must never overwrite committed
-\* \* different record.
-\* CommittedNotOverwritten ==
-\*   \A p \in proposers: \A a \in acceptors:
-\*     (/\ prop_state[p].state = "leader"
-\*      /\ prop_state[p].term = acc_state[a].term
-\*      /\ a \in DOMAIN prop_state[p].next_send_lsn) =>
-\*        LET
-\*          next_e == NextEntry(p, a)
-\*        IN
-\*          (next_e /= NULL) =>
-\*           ((commit_lsns[a] >= next_e.lsn) => (acc_state[a].wal[next_e.lsn] = next_e))
+\* 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.
diff --git a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
index 6282bb6798..a232328d13 100644
--- a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
+++ b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
@@ -12,7 +12,7 @@ TypeOk
 ElectionSafety
 LogIsMonotonic
 LogSafety
-\* CommittedNotOverwritten
+CommittedNotTruncated
 SYMMETRY ProposerAcceptorSymmetry
 CHECK_DEADLOCK FALSE
 ALIAS Alias
diff --git a/safekeeper/spec/readme.md b/safekeeper/spec/readme.md
index e69de29bb2..3d0a04fefa 100644
--- a/safekeeper/spec/readme.md
+++ b/safekeeper/spec/readme.md
@@ -0,0 +1,7 @@
+Directory structure:
+- Use modelcheck.sh to run TLC.
+- MC*.tla contains bits of TLA+ needed for TLC like constraining the state space, and models/ actual models.
+- Other .tla files are the actual specs.
+
+Structure is partially borrowed from
+[logless-reconfig](https://github.com/will62794/logless-reconfig), thanks to it.