From a9662b6f645367a5d5b7bc9430b3a158ab545fde Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Mon, 2 Dec 2024 12:11:10 +0300
Subject: [PATCH] do not append on non members

---
 safekeeper/spec/ProposerAcceptorReconfig.tla | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla
index ed5d298c89..31bb6c244b 100644
--- a/safekeeper/spec/ProposerAcceptorReconfig.tla
+++ b/safekeeper/spec/ProposerAcceptorReconfig.tla
@@ -128,6 +128,10 @@ AppendEntry(p, a) ==
     /\ prop_state[p].state = "leader"
     \* Configuration must be the same.
     /\ prop_conf[p].generation = acc_conf[a].generation
+    \* And a is member of it. Ignoring this likely wouldn't hurt, but not useful
+    \* either.
+    /\ \/ a \in prop_conf[p].members
+       \/ (prop_conf[p].newMembers /= NULL) /\ (a \in prop_conf[p].newMembers)
     /\ PAS!AppendEntry(p, a)
     /\ UNCHANGED <<prop_conf, acc_conf, conf_store>>