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

tune the evidence

Browse Source
This commit is contained in:
Igor Konnov
2022-08-24 00:46:33 +02:00
parent 31b8021672
commit 3ec96cf44c
2 changed files with 14 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/light-client/accountability/TendermintAccInv_004_draft.tla
+5 -2
View File
@@ -295,12 +295,15 @@ PrecommitsLockValue ==
\A r \in Rounds:
\A v \in ValidValues:
\/ LET Precommits == {
m \in msgsPrecommit[r]: m.id = v /\ m.src \in Corr
m \in msgsPrecommit[r] \intersect evidencePrecommit:
m.id = v /\ m.src \in Corr
}
IN
Cardinality(Senders(Precommits)) < THRESHOLD1
\/ \A fr \in Rounds, w \in Values:
LET Prevotes == { m \in msgsPrevote[fr]: m.id = w } IN
LET Prevotes == {
m \in msgsPrevote[fr] \intersect evidencePrevote: m.id = w
} IN
(fr > r /\ w /= v) => (Cardinality(Senders(Prevotes)) < THRESHOLD2)
\* Another lemma by Josef Widder:
spec/light-client/accountability/TendermintAcc_004_draft.tla
+9 -5
View File
@@ -382,7 +382,8 @@ UponQuorumOfPrecommitsAny(p) ==
LET Committers == { m.src: m \in MyEvidence } IN
\* compare the number of the unique committers against the threshold
/\ Cardinality(Committers) >= THRESHOLD2 \* line 47
/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
\*/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
/\ UNCHANGED evidencePrecommit
/\ round[p] + 1 \in Rounds
/\ StartRound(p, round[p] + 1)
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
@@ -434,7 +435,8 @@ OnQuorumOfNilPrevotes(p) ==
/\ step[p] = "PREVOTE"
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilValue) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
/\ evidencePrevote' = PV \union evidencePrevote
\*/\ evidencePrevote' = PV \union evidencePrevote
/\ UNCHANGED evidencePrevote
/\ BroadcastPrecommit(p, round[p], Id(NilValue))
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
@@ -455,9 +457,10 @@ OnRoundCatchup(p) ==
Src(EvPropose) \union Src(EvPrevote) \union Src(EvPrecommit)
IN
/\ Cardinality(Faster) >= THRESHOLD1
/\ evidencePropose' = EvPropose \union evidencePropose
/\ evidencePrevote' = EvPrevote \union evidencePrevote
/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
/\ UNCHANGED <<evidencePropose, evidencePrevote, evidencePrecommit>>
\*/\ evidencePropose' = EvPropose \union evidencePropose
\*/\ evidencePrevote' = EvPrevote \union evidencePrevote
\*/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
/\ StartRound(p, r)
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
@@ -495,6 +498,7 @@ EquivocationBy(p) ==
/\ m2.src = p
/\ m1.round = m2.round
IN
\/ EquivocationIn(evidencePropose)
\/ EquivocationIn(evidencePrevote)
\/ EquivocationIn(evidencePrecommit)