From 292828a01bf421a72fa8a1c8939f87e676a3a61f Mon Sep 17 00:00:00 2001 From: Giuliano Date: Tue, 4 May 2021 05:28:07 -0700 Subject: [PATCH] A few improvements to the Ivy proof (#288) * Avoid quantifier alternation cycle The problematic quantifier alternation cycle arose because the definition of accountability_violation was unfolded. This commit also restructures the induction proof for clarity. * add count_lines.sh * fix typo and add forgotten complete=fo in comment Co-authored-by: Giuliano --- ivy-proofs/abstract_tendermint.ivy | 3 + ivy-proofs/accountable_safety_1.ivy | 86 ++++++++++++++--------------- ivy-proofs/accountable_safety_2.ivy | 4 +- ivy-proofs/check_proofs.sh | 2 +- ivy-proofs/count_lines.sh | 13 +++++ ivy-proofs/network_shim.ivy | 2 +- 6 files changed, 62 insertions(+), 48 deletions(-) create mode 100755 ivy-proofs/count_lines.sh diff --git a/ivy-proofs/abstract_tendermint.ivy b/ivy-proofs/abstract_tendermint.ivy index d0c0e8d5f..36fe7a546 100644 --- a/ivy-proofs/abstract_tendermint.ivy +++ b/ivy-proofs/abstract_tendermint.ivy @@ -43,6 +43,7 @@ module abstract_tendermint = { relation observed_equivocation(N:node) relation observed_unlawful_prevote(N:node) relation agreement + relation accountability_violation object defs = { # we hide those definitions and use them only when needed private { @@ -54,6 +55,8 @@ module abstract_tendermint = { & forall Q,R . R1 <= R & R < R2 & nset.is_quorum(Q) -> exists N2 . nset.member(N2,Q) & ~observed_prevoted(N2,R,V2) definition [agreement_def] agreement = forall N1,N2,R1,R2,V1,V2 . well_behaved(N1) & well_behaved(N2) & decided(N1,R1,V1) & decided(N2,R2,V2) -> V1 = V2 + + definition [accountability_violation_def] accountability_violation = exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & (forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N)) } } diff --git a/ivy-proofs/accountable_safety_1.ivy b/ivy-proofs/accountable_safety_1.ivy index dc083bb4d..cfa4c32e0 100644 --- a/ivy-proofs/accountable_safety_1.ivy +++ b/ivy-proofs/accountable_safety_1.ivy @@ -35,9 +35,9 @@ isolate abstract_accountable_safety = { # If there is disagreement, then there is evidence that a third of the nodes # have violated the protocol: - invariant [accountability] agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & (forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N)) + invariant [accountability] agreement | accountability_violation proof { - apply lemma_2.thm # this reduces to goal to three subgoals: p1, p2, and p3 (see their definition below) + apply lemma_1.thm # this reduces to goal to three subgoals: p1, p2, and p3 (see their definition below) proof [p1] { assume invs.inv1 } @@ -76,52 +76,50 @@ isolate abstract_accountable_safety = { # For technical reasons, we separate the proof in two steps isolate lemma_1 = { -# complete induction is not built-in, so we introduce it with an axiom. Note that this only holds for a type where 0 is the smallest element - axiom [complete_induction] { - relation p(X:round) - { # base case - property p(0) + specification { + theorem [thm] { + property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) + property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) & V ~= value.nil -> exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) + property [p3] forall R,V. (exists N . well_behaved(N) & decided(N,R,V)) -> 0 <= R & V ~= value.nil & exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_precommitted(N2,R,V) + #------------------------------------------------------------------------------------------------------------------------------------------- + property agreement | accountability_violation } - { # inductive step: show that if the property is true for all X lower or equal to x and y=x+1, then the property is true of y - individual a:round - individual b:round - property (forall X. 0 <= X & X <= a -> p(X)) & round.succ(a,b) -> p(b) + proof { + assume inductive_property # the theorem follows from what we prove by induction below } - #-------------------------- - property forall X . 0 <= X -> p(X) } -# the main lemma: if inv1 and inv2 below hold and a quorum is observed to -# precommit V1 at R1 and another quorum is observed to precommit V2~=V1 at -# R2>=R1, then the intersection of two quorums (i.e. f+1 nodes) is observed to -# violate the protocol - theorem [thm] { - property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) - property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) -> V = value.nil | exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) - #----------------------------------------------------------------------------------------------------------------------- - property forall R2. 0 <= R2 -> ((exists V2,Q1,R1,V1,Q1 . V1 ~= value.nil & V2 ~= value.nil & V1 ~= V2 & 0 <= R1 & R1 <= R2 & nset.is_quorum(Q1) & (forall N . nset.member(N,Q1) -> observed_precommitted(N,R1,V1)) & (exists Q2 . nset.is_quorum(Q2) & forall N . nset.member(N,Q2) -> observed_prevoted(N,R2,V2))) -> exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N)) - } - proof { - apply complete_induction # the two subgoals (base case and inductive case) are then discharged automatically - } - } with this, round, nset, accountable_bft.max_2f_byzantine, defs.observed_equivocation_def, defs.observed_unlawful_prevote_def - -# Now we put lemma_1 in a form that matches exactly the accountability property -# we want to prove. This is a bit cumbersome and could probably be improved. - isolate lemma_2 = { - - theorem [thm] { - property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) - property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) & V ~= value.nil -> exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) - property [p3] forall R,V. (exists N . well_behaved(N) & decided(N,R,V)) -> 0 <= R & V ~= value.nil & exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_precommitted(N2,R,V) - #------------------------------------------------------------------------------------------------------------------------------------------- - property agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N) - } - proof { - assume lemma_1.thm - } + implementation { + # complete induction is not built-in, so we introduce it with an axiom. Note that this only holds for a type where 0 is the smallest element + axiom [complete_induction] { + relation p(X:round) + { # base case + property p(0) + } + { # inductive step: show that if the property is true for all X lower or equal to x and y=x+1, then the property is true of y + individual a:round + individual b:round + property (forall X. 0 <= X & X <= a -> p(X)) & round.succ(a,b) -> p(b) + } + #-------------------------- + property forall X . 0 <= X -> p(X) + } - } with this, round, defs.agreement_def, lemma_1, nset, accountable_bft.max_2f_byzantine + # The main lemma: if inv1 and inv2 below hold and a quorum is observed to + # precommit V1 at R1 and another quorum is observed to precommit V2~=V1 at + # R2>=R1, then the intersection of two quorums (i.e. f+1 nodes) is observed to + # violate the protocol. We prove this by complete induction on R2. + theorem [inductive_property] { + property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V)) + property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) -> V = value.nil | exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V) + #----------------------------------------------------------------------------------------------------------------------- + property forall R2. 0 <= R2 -> ((exists V2,Q1,R1,V1,Q1 . V1 ~= value.nil & V2 ~= value.nil & V1 ~= V2 & 0 <= R1 & R1 <= R2 & nset.is_quorum(Q1) & (forall N . nset.member(N,Q1) -> observed_precommitted(N,R1,V1)) & (exists Q2 . nset.is_quorum(Q2) & forall N . nset.member(N,Q2) -> observed_prevoted(N,R2,V2))) -> accountability_violation) + } + proof { + apply complete_induction # the two subgoals (base case and inductive case) are then discharged automatically + } + } + } with this, round, nset, accountable_bft.max_2f_byzantine, defs.observed_equivocation_def, defs.observed_unlawful_prevote_def, defs.accountability_violation_def, defs.agreement_def } with round @@ -139,6 +137,6 @@ isolate accountable_safety_1 = { invariant abstract_accountable_safety.agreement -> agreement - invariant [accountability] agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> abstract_accountable_safety.observed_equivocation(N) | abstract_accountable_safety.observed_unlawful_prevote(N) + invariant [accountability] agreement | abstract_accountable_safety.accountability_violation } with value, round, proposers, shim, abstract_accountable_safety, abstract_accountable_safety.defs.agreement_def, accountable_safety_1.agreement_def diff --git a/ivy-proofs/accountable_safety_2.ivy b/ivy-proofs/accountable_safety_2.ivy index 5dd0a5bec..7fb928909 100644 --- a/ivy-proofs/accountable_safety_2.ivy +++ b/ivy-proofs/accountable_safety_2.ivy @@ -4,7 +4,7 @@ include tendermint include abstract_tendermint # Here we prove the second accountability property: no well-behaved node is -# every observed to violate the accountability properties. +# ever observed to violate the accountability properties. # The proof is done in two steps: first we prove the the abstract specification # satisfies the property, and then we show by refinement that this property @@ -12,7 +12,7 @@ include abstract_tendermint # To see what is checked in the refinement proof, use `ivy_show isolate=accountable_safety_2 accountable_safety_2.ivy` # To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_accountable_safety_2 accountable_safety_2.ivy` -# To check the whole proof, use `ivy_check accountable_safety_2.ivy`. +# To check the whole proof, use `ivy_check complete=fo accountable_safety_2.ivy`. # Proof that the property holds in the abstract specification # ============================================================ diff --git a/ivy-proofs/check_proofs.sh b/ivy-proofs/check_proofs.sh index 2663eb894..3668db4f3 100755 --- a/ivy-proofs/check_proofs.sh +++ b/ivy-proofs/check_proofs.sh @@ -16,7 +16,7 @@ else fi echo "Checking accountable safety 1:" -res=$(ivy_check complete=fo accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1) +res=$(ivy_check accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1) if [ "$res" = "OK" ]; then echo "OK" else diff --git a/ivy-proofs/count_lines.sh b/ivy-proofs/count_lines.sh new file mode 100755 index 000000000..b2c457e21 --- /dev/null +++ b/ivy-proofs/count_lines.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +r='^\s*$\|^\s*\#\|^\s*\}\s*$\|^\s*{\s*$' # removes comments and blank lines and lines that contain only { or } +N1=`cat tendermint.ivy domain_model.ivy network_shim.ivy | grep -v $r'\|.*invariant.*' | wc -l` +N2=`cat abstract_tendermint.ivy | grep "observed_" | wc -l` # the observed_* variables specify the observations of the nodes +SPEC_LINES=`expr $N1 + $N2` +echo "spec lines: $SPEC_LINES" +N3=`cat abstract_tendermint.ivy | grep -v $r'\|.*observed_.*' | wc -l` +N4=`cat accountable_safety_1.ivy | grep -v $r | wc -l` +PROOF_LINES=`expr $N3 + $N4` +echo "proof lines: $PROOF_LINES" +RATIO=`bc <<< "scale=2;$PROOF_LINES / $SPEC_LINES"` +echo "proof-to-code ratio for the accountable-safety property: $RATIO" diff --git a/ivy-proofs/network_shim.ivy b/ivy-proofs/network_shim.ivy index 6a0e43411..cffc6fc57 100644 --- a/ivy-proofs/network_shim.ivy +++ b/ivy-proofs/network_shim.ivy @@ -112,7 +112,7 @@ isolate shim = { else if m.m_kind = msg_kind.prevote { call prevote_handler.handle(dst,m) } - else if m.m_kind = msg_kind.proposal { + else if m.m_kind = msg_kind.precommit { call precommit_handler.handle(dst,m) } }