From 7886f520c5936f32251d36cc7be6a48a34683042 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@informal.systems>
Date: Fri, 19 Aug 2022 09:40:12 +0200
Subject: [PATCH] final fix of the inductive invariant

---
 .../TendermintAccInv_004_draft.tla            | 21 +++++++++----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
index bdac92bba..d9d78be28 100644
--- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
@@ -172,8 +172,7 @@ TwoThirdsPrevotes(vr, v) ==
 \* 1) the process is faulty,
 \* 2) the PREVOTE contains Nil,
 \* 3) a) there is a proposal in an earlier (valid) round,
-\*    b) there are two thirds of PREVOTES in that round,
-\*    c) there is no precommit message on another value in between the rounds.
+\*    b) there are two thirds of PREVOTES in that round.
 IfSentPrevoteThenReceivedProposalOrTwoThirds(r) ==
   \A mpv \in msgsPrevote[r]:
     \* case 1
@@ -190,11 +189,6 @@ IfSentPrevoteThenReceivedProposalOrTwoThirds(r) ==
             /\ ProposalInRound(r, mpv.id, vr)
             \* condition 3b
             /\ TwoThirdsPrevotes(vr, mpv.id)
-            \* condition 3c
-            /\ \A mr \in Rounds:
-                 \/ ~(vr <= mr /\ mr <= r)
-                 \/ \A m \in msgsPrecommit[mr]:
-                      m.src = mpv.src => m.id \in { NilValue, mpv.id }
 
 AllIfSentPrevoteThenReceivedProposalOrTwoThirds ==
   \A r \in Rounds:
@@ -320,11 +314,16 @@ RelockValueIfEnoughPrevotes ==
         /\ m1 \in msgsPrecommit[r1]
         /\ m2 \in msgsPrevote[r2]
       IN
-      LET EnoughPrevotesLater ==
-        LET Prevotes == { m \in msgsPrevote[r2]: m.id = v2 /\ m.src /= p } IN
-        Cardinality(Prevotes) >= THRESHOLD2
+      LET EnoughPrevotesInMiddle ==
+        \E mr \in Rounds:
+          /\ r1 < mr /\ mr <= r2
+          \* count prevotes in the middle round, excluding p if mr = r2
+          /\ LET Prevotes == { m \in msgsPrevote[mr]:
+                                m.id = v2 /\ (m.src /= p \/ mr < r2) }
+             IN
+             Cardinality(Prevotes) >= THRESHOLD2
       IN
-      RelockedValue => EnoughPrevotesLater
+      RelockedValue => EnoughPrevotesInMiddle
 
 \* a combination of all lemmas
 Inv ==