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

fix wrong axioms (#9511)

Browse Source 
Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>
This commit is contained in:
Giuliano
2022-10-05 02:38:21 -07:00
committed by GitHub
parent abbeb919df
commit b1dc5a6def
1 changed files with 3 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
spec/ivy-proofs/domain_model.ivy
View File

@@ -131,13 +131,14 @@ object nset = { # the type of node sets
object classic_bft = {
relation quorum_intersection
private {
definition [quorum_intersection_def] quorum_intersection = forall Q1,Q2. exists N. well_behaved(N) & nset.member(N, Q1) & nset.member(N, Q2) # every two quorums have a well-behaved node in common
definition [quorum_intersection_def] quorum_intersection = forall Q1,Q2. nset.is_quorum(Q1) & nset.is_quorum(Q2)
-> exists N. well_behaved(N) & nset.member(N, Q1) & nset.member(N, Q2) # every two quorums have a well-behaved node in common
}
}
trusted isolate accountable_bft = {
# this is our baseline assumption about quorums:
private {
property [max_2f_byzantine] exists N . well_behaved(N) & nset.member(N,Q) # every quorum has a well-behaved member
property [max_2f_byzantine] nset.is_quorum(Q) -> exists N . well_behaved(N) & nset.member(N,Q) # every quorum has a well-behaved member
}
}