Fixed (and simplified) proof in byzpaxos/Consensus.tla (#163)

* Fixed (and simplified) proof in byzpaxos/Consensus.tla
* Also fixed minor failure in LoopInvariance/BinarySearch.tla
* Check fixed proofs in CI

Signed-off-by: Stephan Merz <[email protected]>

Author: muenchnerkindl

.github/workflows/CI.yml

@@ -146,10 +146,6 @@ jobs:
             ## ATD/EWD require TLAPS' update_enabled_cdot branch
             specifications/ewd998/AsyncTerminationDetection_proof.tla
             specifications/ewd998/EWD998_proof.tla
-            ## Regressions?
-            specifications/byzpaxos/Consensus.tla
-            specifications/LearnProofs/FindHighest.tla
-            specifications/LoopInvariance/BinarySearch.tla
             # Failing; see https://github.com/tlaplus/Examples/issues/67
             specifications/Bakery-Boulangerie/Bakery.tla
             specifications/Bakery-Boulangerie/Boulanger.tla

specifications/LoopInvariance/BinarySearch.tla

@@ -130,7 +130,7 @@ Inv == /\ TypeOK
 (***************************************************************************)
 THEOREM Spec => []resultCorrect
 <1>1. Init => Inv
-  BY DEF Init, Inv, TypeOK
+  BY DEF Init, Inv, TypeOK, SortedSeqs
 <1>2. Inv /\ [Next]_vars => Inv'
   <2> SUFFICES ASSUME Inv,
                       [Next]_vars

specifications/byzpaxos/Consensus.tla

@@ -147,7 +147,7 @@ LEMMA InductiveInvariance ==
   OBVIOUS
 <1>1. CASE Next 
   \* In the following BY proof, <1>1 denotes the case assumption Next 
-  BY <1>1, FS_EmptySet, FS_AddElement DEF Inv, TypeOK, Next
+  BY <1>1, FS_EmptySet, FS_Singleton DEF Inv, TypeOK, Next
 <1>2. CASE vars' = vars
   BY <1>2 DEF Inv, TypeOK, vars  
 <1>3. QED
@@ -164,9 +164,10 @@ THEOREM Invariance == Spec => []Inv
 (* We now define LiveSpec to be the algorithm's specification with the     *)
 (* added fairness condition of weak fairness of the next-state relation,   *)
 (* which asserts that execution does not stop if some action is enabled.   *)
-(* The temporal formula Success asserts that some value is eventually      *)
-(* chosen.  Below, we prove that LiveSpec implies Success This means that, *)
-(* in every behavior satisfying LiveSpec, some value is chosen.            *)
+(* The temporal formula Success asserts that some value is chosen.         *)
+(* Below, we prove that LiveSpec implies that Success holds eventually.    *)
+(* This means that, in every behavior satisfying LiveSpec, some value will *)
+(* be chosen.                                                              *)
 (***************************************************************************)
 LiveSpec == Spec /\ WF_vars(Next)
 Success == <>(chosen # {})
@@ -177,48 +178,17 @@ Success == <>(chosen # {})
 ASSUME ValueNonempty == Value # {}
 
 (***************************************************************************)
-(* TLAPS does not yet reason about ENABLED.  Therefore, we must omit all   *)
-(* proofs that involve ENABLED formulas.  To perform as much of the proof  *)
-(* as possible, as much as possible we restrict the use of an ENABLED      *)
-(* expression to a step asserting that it equals its definition.  ENABLED  *)
-(* A is true of a state s iff there is a state t such that the step s -> t *)
-(* satisfies A.  It follows from this semantic definition that ENABLED A   *)
-(* equals the formula obtained by                                          *)
-(*                                                                         *)
-(*  1. Expanding all definitions of defined symbols in A until all primes  *)
-(*     are priming variables.                                              *)
-(*                                                                         *)
-(*  2. For each primed variable, replacing every instance of that primed   *)
-(*     variable by a new symbol (the same symbol for each primed           *)
-(*     variable).                                                          *)
-(*                                                                         *)
-(*  3. Existentially quantifying over those new symbols.                   *)
+(* Since fairness is defined in terms of the ENABLED operator, we must     *)
+(* characterize states at which an action is enabled. It is usually a good *)
+(* idea to prove a separate lemma for this.                                *)
 (***************************************************************************)
-LEMMA EnabledDef ==
-        TypeOK => 
-          ((ENABLED <<Next>>_vars) <=> (chosen = {}))
-<1> DEFINE E == 
-       \E chosenp :
-               /\ /\ chosen = {}
-                  /\ \E v \in Value: chosenp = {v}
-               /\ ~ (<<chosenp>> = <<chosen>>)
-<1>1. E = ENABLED <<Next>>_vars
-  \* BY DEF Next, vars (* and def of ENABLED *)
-  PROOF OMITTED
-<1>2. SUFFICES ASSUME TypeOK
-               PROVE  E = (chosen = {})
-  BY <1>1, Zenon
-<1>3. E = \E chosenp : E!(chosenp)!1
-  BY <1>2, Isa  DEF TypeOK
-<1>4. @ = (chosen = {})
- BY <1>2, ValueNonempty, Zenon DEF TypeOK
-<1>5. QED
- BY <1>3, <1>4, Zenon
+LEMMA EnabledNext ==
+    (ENABLED <<Next>>_vars) <=> (chosen = {})
+BY ValueNonempty, ExpandENABLED DEF Next, vars
 
 (***************************************************************************)
-(* Here is our proof that Livespec implies Success.  It uses the standard  *)
-(* TLA proof rules.  For example RuleWF1 is defined in the TLAPS module to *)
-(* be the rule WF1 discussed in                                            *)
+(* Here is our proof that Livespec implies Success. The overall approach   *)
+(* to the proof follows the rule WF1 discussed in                          *)
 (*                                                                         *)
 (* `. AUTHOR  = "Leslie Lamport",                                          *)
 (*    TITLE   = "The Temporal Logic of Actions",                           *)
@@ -229,29 +199,21 @@ LEMMA EnabledDef ==
 (*    month   = may,                                                       *)
 (*    PAGES   = "872--923"         .'                                      *)
 (*                                                                         *)
-(* PTL stands for propositional temporal logic reasoning.  We expect that, *)
-(* when TLAPS handles temporal reasoning, it will use a decision procedure *)
-(* for PTL.                                                                *)
+(* In the actual proof, use of this rule is subsumed by appealing to the   *)
+(* PTL decision procedure for propositional temporal logic. When reasoning *)
+(* about the liveness of more complex specifications, an additional        *)
+(* invariant would typically be required.                                  *)
 (***************************************************************************)
 THEOREM LiveSpec => Success
-<1>1. []Inv /\ [][Next]_vars /\ WF_vars(Next) => (chosen = {} ~> chosen # {})
-  <2>. DEFINE P == chosen = {}
-              Q == chosen # {}
-  <2>1. SUFFICES [][Next]_vars /\ WF_vars(Next) => ((Inv /\ P) ~> Q)
-    BY PTL
-  <2>2. (Inv /\ P) /\ [Next]_vars => ((Inv' /\ P') \/ Q')
-    BY InductiveInvariance
-  <2>3. (Inv /\ P) /\ <<Next>>_vars => Q'
-    BY DEF Inv, Next, vars
-  <2>4. (Inv /\ P) => ENABLED <<Next>>_vars
-    BY EnabledDef DEF Inv
-  <2>. HIDE DEF P,Q
-  <2>. QED
-    BY <2>2, <2>3, <2>4, PTL
-<1>2. (chosen = {} ~> chosen # {}) => ((chosen = {}) => <>(chosen # {}))
-  BY PTL
-<1>3. QED
-  BY Invariance, <1>1, <1>2, PTL DEF LiveSpec, Spec, Init, Success
+<1>1. [][Next]_vars /\ WF_vars(Next) => [](Init => Success)
+  <2>1. Init' \/ (chosen # {})'
+    BY DEF Init
+  <2>2. Init /\ <<Next>>_vars => (chosen # {})'
+    BY DEF Init, Next, vars
+  <2>3. Init => ENABLED <<Next>>_vars
+    BY EnabledNext DEF Init
+  <2>. QED  BY <2>1, <2>2, <2>3, PTL DEF Success
+<1>2. QED  BY <1>1, PTL DEF LiveSpec, Spec, Success
 
 -----------------------------------------------------------------------------
 (***************************************************************************)
@@ -260,15 +222,12 @@ THEOREM LiveSpec => Success
 (***************************************************************************)
 THEOREM LiveSpecEquals ==
           LiveSpec <=> Spec /\ ([]<><<Next>>_vars \/ []<>(chosen # {}))
-<1>1. /\ Spec <=> Spec /\ []TypeOK
-      /\ LiveSpec <=> LiveSpec /\ []TypeOK
-  BY Invariance, PTL DEF LiveSpec, Inv
-<1>2. (chosen # {}) <=> ~(chosen = {})
+<1>1. (chosen # {}) <=> ~(chosen = {})
   OBVIOUS
-<1>3. []TypeOK => (([]<>~ENABLED <<Next>>_vars) <=> []<>(chosen # {}))
-  BY <1>2, EnabledDef, PTL
+<1>2. ([]<>~ENABLED <<Next>>_vars) <=> []<>(chosen # {})
+  BY <1>1, EnabledNext, PTL
 <1>4. QED
-  BY <1>1, <1>3, PTL DEF LiveSpec
+  BY <1>2, PTL DEF LiveSpec
 =============================================================================
 \* Modification History
 \* Last modified Mon May 11 18:36:27 CEST 2020 by merz