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 <giuliano@eic-61-11.galois.com>

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))
         }
     }
 

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

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
 # ============================================================

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

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"

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)
             }
         }