From b1dc5a6def974d8fcd8b7733bb56993f960dabd3 Mon Sep 17 00:00:00 2001 From: Giuliano Date: Wed, 5 Oct 2022 02:38:21 -0700 Subject: [PATCH] fix wrong axioms (#9511) Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- spec/ivy-proofs/domain_model.ivy | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/spec/ivy-proofs/domain_model.ivy b/spec/ivy-proofs/domain_model.ivy index 0f12f7288..1fd3cc99e 100644 --- a/spec/ivy-proofs/domain_model.ivy +++ b/spec/ivy-proofs/domain_model.ivy @@ -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 } }