From db343caf5dbb5eb98fa44b8067198f2fe63d0652 Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Mon, 2 Dec 2024 12:02:26 +0100
Subject: [PATCH] Fix BecomeLeader, adjust init and target confs.

---
 safekeeper/spec/ProposerAcceptorReconfig.tla | 11 ++++++++++-
 safekeeper/spec/ProposerAcceptorStatic.tla   | 17 ++++++++++-------
 2 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla
index d5c6ef2374..aac56d06f7 100644
--- a/safekeeper/spec/ProposerAcceptorReconfig.tla
+++ b/safekeeper/spec/ProposerAcceptorReconfig.tla
@@ -65,6 +65,11 @@ Init ==
            /\ prop_conf = [p \in proposers |-> init_conf]
            /\ acc_conf = [a \in acceptors |-> init_conf]
            /\ conf_store = init_conf
+           \* We could start with anything, but to reduce space state start with
+           \* the most reasonable total acceptors - 1 conf size, which e.g.
+           \* makes basic {a1} -> {a2} change in {a1, a2} acceptors and {a1, a2,
+           \* a3} -> {a2, a3, a4} in {a1, a2, a3, a4} acceptors models even in
+           \* the smallest models with single change.
            /\ Cardinality(init_members) = Cardinality(acceptors) - 1
 
 \********************************************************************************
@@ -106,6 +111,11 @@ BecomeLeader(p) ==
        \* https://groups.google.com/g/tlaplus/c/U6tOJ4dsjVM/m/UdOznPCVBwAJ
        \* so repeat the null check.
        \/ (prop_conf[p].newMembers /= NULL)  /\ (PAS!FormsQuorum(DOMAIN prop_state[p].votes, prop_conf[p].newMembers))
+    \* DoBecomeLeader will copy WAL of the highest voter to proposer's WAL, so
+    \* ensure its conf is still the same. In the impl WAL fetching also has to
+    \* check the configuration.
+    /\ prop_conf[p].generation = acc_conf[PAS!MaxVoteAcc(p)].generation
+    /\ \A a \in DOMAIN prop_state[p].votes: prop_conf[p].generation = acc_conf[a].generation
     /\ PAS!DoBecomeLeader(p)
     /\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
 
@@ -175,7 +185,6 @@ ProposerSwitchConf(p, a) ==
 StartChange(new_members) ==
     \* Possible only if we don't already have the change in progress.
     /\ conf_store.newMembers = NULL
-    /\ Cardinality(new_members) = 1
     \* Not necessary, but reduces space a bit.
     /\ new_members /= conf_store.members
     /\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> new_members]
diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla
index 85f5879947..fab085bc2e 100644
--- a/safekeeper/spec/ProposerAcceptorStatic.tla
+++ b/safekeeper/spec/ProposerAcceptorStatic.tla
@@ -265,18 +265,21 @@ TermLsnGE(tl1, tl2) ==
 MaxTermLsn(term_lsn_set) ==
     CHOOSE max_tl \in term_lsn_set: \A tl \in term_lsn_set: TermLsnGE(max_tl, tl)
 
+\* Find acceptor with the highest <last_log_term, lsn> vote in proposer p's votes.
+MaxVoteAcc(p) ==
+    CHOOSE a \in DOMAIN prop_state[p].votes:
+        LET a_vote == prop_state[p].votes[a]
+            a_vote_term_lsn == [term |-> LastLogTerm(a_vote.termHistory), lsn |-> a_vote.flushLsn]
+            vote_term_lsns == {[term |-> LastLogTerm(v.termHistory), lsn |-> v.flushLsn]: v \in Range(prop_state[p].votes)}
+        IN
+            a_vote_term_lsn = MaxTermLsn(vote_term_lsns)
+
 \* Workhorse for BecomeLeader.
 \* Assumes the check prop_state[p] votes is quorum has been done *outside*.
 DoBecomeLeader(p) ==
     LET
         \* Find acceptor with the highest <last_log_term, lsn> vote.
-        max_vote_acc ==
-            CHOOSE a \in DOMAIN prop_state[p].votes:
-                LET a_vote == prop_state[p].votes[a]
-                    a_vote_term_lsn == [term |-> LastLogTerm(a_vote.termHistory), lsn |-> a_vote.flushLsn]
-                    vote_term_lsns == {[term |-> LastLogTerm(v.termHistory), lsn |-> v.flushLsn]: v \in Range(prop_state[p].votes)}
-                IN
-                    a_vote_term_lsn = MaxTermLsn(vote_term_lsns)
+        max_vote_acc == MaxVoteAcc(p)
         max_vote == prop_state[p].votes[max_vote_acc]
         prop_th == Append(max_vote.termHistory, [term |-> prop_state[p].term, lsn |-> max_vote.flushLsn])
     IN