mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-05-23 07:31:29 +00:00
Code Issues Packages Projects Releases Wiki Activity

PBTS/tla: decision on valid values invariant

Browse Source
This commit is contained in:
Daniel Cason
2022-05-02 15:57:07 +02:00
committed by Daniel
parent fa5138b759
commit 30c0cfbbfd
2 changed files with 18 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
View File

@@ -522,6 +522,15 @@ AgreementOnValue ==
/\ decision[p] = Decision(v, t, r1)
/\ decision[q] = Decision(v, t, r2)
\* [PBTS-INV-VALID.0]
ConsensusValidValue ==
\A p \in Corr:
\* decision[p] = Decision(v, t, r)
LET dec == decision[p] IN dec /= NilDecision => IsValid(dec[1])
\* [PBTS-INV-MONOTONICITY.0]
\* TODO: we would need to compare timestamps of blocks from different height
\* [PBTS-CONSENSUS-TIME-VALID.0]
ConsensusTimeValid ==
\A p \in Corr, t \in Timestamps :

9
spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
View File

@@ -789,6 +789,15 @@ DisagreementOnValue ==
/\ decision[p] = Decision(p1, r1)
/\ decision[q] = Decision(p2, r2)
\* [PBTS-INV-VALID.0]
ConsensusValidValue ==
\A p \in Corr:
\* decision[p] = Decision(Proposal(v,t,pr), r)
LET prop == decision[p][1] IN prop /= NilProposal => IsValid(prop[1])
\* [PBTS-INV-MONOTONICITY.0]
\* TODO: we would need to compare timestamps of blocks from different height
\* [PBTS-CONSENSUS-TIME-VALID.0]
ConsensusTimeValid ==
\A p \in Corr: