mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-01-08 22:23:11 +00:00
Code Issues Packages Projects Releases Wiki Activity

strengthen RelockValueIfEnoughPrevotes

Browse Source
This commit is contained in:
Igor Konnov
2022-08-29 11:42:10 +02:00
parent 3ec96cf44c
commit 7f14e3200a
1 changed files with 12 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
spec/light-client/accountability/TendermintAccInv_004_draft.tla
View File

@@ -320,15 +320,21 @@ RelockValueIfEnoughPrevotes ==
/\ m2 \in msgsPrevote[r2]
IN
LET EnoughPrevotesInMiddle ==
\E mr \in Rounds:
/\ r1 <= mr /\ mr <= r2
\E vr \in Rounds:
/\ r1 <= vr /\ vr <= r2
\* count prevotes in the middle round, excluding p
/\ LET Prevotes == {
m \in msgsPrevote[mr] \intersect evidencePrevote:
m.id = v2 /\ (m.src /= p \/ mr < r2)
m \in msgsPrevote[vr] \intersect evidencePrevote:
m.id = v2 /\ (m.src /= p \/ vr < r2)
}
IN
Cardinality(Prevotes) >= THRESHOLD2
/\ Cardinality(Prevotes) >= THRESHOLD2
\* this majority must be backed by a proposal!
/\ LET proposal == [
type |-> "PROPOSE", src |-> Proposer[r2], round |-> r2,
proposal |-> v2, validRound |-> vr
] IN
proposal \in msgsPropose[r2]
IN
RelockedValue => EnoughPrevotesInMiddle
@@ -376,7 +382,7 @@ Inv ==
/\ AllIfValidRoundThenTwoThirds
/\ AllValidAndLocked
/\ AllIfValidRoundThenProposal
\*/\ PrecommitsLockValue
/\ PrecommitsLockValue
\* this is the inductive invariant we like to check
TypedInv == TypeOK /\ Inv