Skip to content

Commit ddef39b

Browse files
muenchnerkindlmuenchnerkindl
authored
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 <stephan.merz@loria.fr>
1 parent e2fdd9c commit ddef39b

3 files changed

Lines changed: 31 additions & 76 deletions

File tree

‎.github/workflows/CI.yml‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -146,10 +146,6 @@ jobs:
146146
## ATD/EWD require TLAPS' update_enabled_cdot branch
147147
specifications/ewd998/AsyncTerminationDetection_proof.tla
148148
specifications/ewd998/EWD998_proof.tla
149-
## Regressions?
150-
specifications/byzpaxos/Consensus.tla
151-
specifications/LearnProofs/FindHighest.tla
152-
specifications/LoopInvariance/BinarySearch.tla
153149
# Failing; see https://github.com/tlaplus/Examples/issues/67
154150
specifications/Bakery-Boulangerie/Bakery.tla
155151
specifications/Bakery-Boulangerie/Boulanger.tla

‎specifications/LoopInvariance/BinarySearch.tla‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ Inv == /\ TypeOK
130130
(***************************************************************************)
131131
THEOREM Spec => []resultCorrect
132132
<1>1. Init => Inv
133-
BY DEF Init, Inv, TypeOK
133+
BY DEF Init, Inv, TypeOK, SortedSeqs
134134
<1>2. Inv /\ [Next]_vars => Inv'
135135
<2> SUFFICES ASSUME Inv,
136136
[Next]_vars

‎specifications/byzpaxos/Consensus.tla‎

Lines changed: 30 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,7 @@ LEMMA InductiveInvariance ==
147147
OBVIOUS
148148
<1>1. CASE Next
149149
\* In the following BY proof, <1>1 denotes the case assumption Next
150-
BY <1>1, FS_EmptySet, FS_AddElement DEF Inv, TypeOK, Next
150+
BY <1>1, FS_EmptySet, FS_Singleton DEF Inv, TypeOK, Next
151151
<1>2. CASE vars' = vars
152152
BY <1>2 DEF Inv, TypeOK, vars
153153
<1>3. QED
@@ -164,9 +164,10 @@ THEOREM Invariance == Spec => []Inv
164164
(* We now define LiveSpec to be the algorithm's specification with the *)
165165
(* added fairness condition of weak fairness of the next-state relation, *)
166166
(* which asserts that execution does not stop if some action is enabled. *)
167-
(* The temporal formula Success asserts that some value is eventually *)
168-
(* chosen. Below, we prove that LiveSpec implies Success This means that, *)
169-
(* in every behavior satisfying LiveSpec, some value is chosen. *)
167+
(* The temporal formula Success asserts that some value is chosen. *)
168+
(* Below, we prove that LiveSpec implies that Success holds eventually. *)
169+
(* This means that, in every behavior satisfying LiveSpec, some value will *)
170+
(* be chosen. *)
170171
(***************************************************************************)
171172
LiveSpec == Spec /\ WF_vars(Next)
172173
Success == <>(chosen # {})
@@ -177,48 +178,17 @@ Success == <>(chosen # {})
177178
ASSUME ValueNonempty == Value # {}
178179

179180
(***************************************************************************)
180-
(* TLAPS does not yet reason about ENABLED. Therefore, we must omit all *)
181-
(* proofs that involve ENABLED formulas. To perform as much of the proof *)
182-
(* as possible, as much as possible we restrict the use of an ENABLED *)
183-
(* expression to a step asserting that it equals its definition. ENABLED *)
184-
(* A is true of a state s iff there is a state t such that the step s -> t *)
185-
(* satisfies A. It follows from this semantic definition that ENABLED A *)
186-
(* equals the formula obtained by *)
187-
(* *)
188-
(* 1. Expanding all definitions of defined symbols in A until all primes *)
189-
(* are priming variables. *)
190-
(* *)
191-
(* 2. For each primed variable, replacing every instance of that primed *)
192-
(* variable by a new symbol (the same symbol for each primed *)
193-
(* variable). *)
194-
(* *)
195-
(* 3. Existentially quantifying over those new symbols. *)
181+
(* Since fairness is defined in terms of the ENABLED operator, we must *)
182+
(* characterize states at which an action is enabled. It is usually a good *)
183+
(* idea to prove a separate lemma for this. *)
196184
(***************************************************************************)
197-
LEMMA EnabledDef ==
198-
TypeOK =>
199-
((ENABLED <<Next>>_vars) <=> (chosen = {}))
200-
<1> DEFINE E ==
201-
\E chosenp :
202-
/\ /\ chosen = {}
203-
/\ \E v \in Value: chosenp = {v}
204-
/\ ~ (<<chosenp>> = <<chosen>>)
205-
<1>1. E = ENABLED <<Next>>_vars
206-
\* BY DEF Next, vars (* and def of ENABLED *)
207-
PROOF OMITTED
208-
<1>2. SUFFICES ASSUME TypeOK
209-
PROVE E = (chosen = {})
210-
BY <1>1, Zenon
211-
<1>3. E = \E chosenp : E!(chosenp)!1
212-
BY <1>2, Isa DEF TypeOK
213-
<1>4. @ = (chosen = {})
214-
BY <1>2, ValueNonempty, Zenon DEF TypeOK
215-
<1>5. QED
216-
BY <1>3, <1>4, Zenon
185+
LEMMA EnabledNext ==
186+
(ENABLED <<Next>>_vars) <=> (chosen = {})
187+
BY ValueNonempty, ExpandENABLED DEF Next, vars
217188

218189
(***************************************************************************)
219-
(* Here is our proof that Livespec implies Success. It uses the standard *)
220-
(* TLA proof rules. For example RuleWF1 is defined in the TLAPS module to *)
221-
(* be the rule WF1 discussed in *)
190+
(* Here is our proof that Livespec implies Success. The overall approach *)
191+
(* to the proof follows the rule WF1 discussed in *)
222192
(* *)
223193
(* `. AUTHOR = "Leslie Lamport", *)
224194
(* TITLE = "The Temporal Logic of Actions", *)
@@ -229,29 +199,21 @@ LEMMA EnabledDef ==
229199
(* month = may, *)
230200
(* PAGES = "872--923" .' *)
231201
(* *)
232-
(* PTL stands for propositional temporal logic reasoning. We expect that, *)
233-
(* when TLAPS handles temporal reasoning, it will use a decision procedure *)
234-
(* for PTL. *)
202+
(* In the actual proof, use of this rule is subsumed by appealing to the *)
203+
(* PTL decision procedure for propositional temporal logic. When reasoning *)
204+
(* about the liveness of more complex specifications, an additional *)
205+
(* invariant would typically be required. *)
235206
(***************************************************************************)
236207
THEOREM LiveSpec => Success
237-
<1>1. []Inv /\ [][Next]_vars /\ WF_vars(Next) => (chosen = {} ~> chosen # {})
238-
<2>. DEFINE P == chosen = {}
239-
Q == chosen # {}
240-
<2>1. SUFFICES [][Next]_vars /\ WF_vars(Next) => ((Inv /\ P) ~> Q)
241-
BY PTL
242-
<2>2. (Inv /\ P) /\ [Next]_vars => ((Inv' /\ P') \/ Q')
243-
BY InductiveInvariance
244-
<2>3. (Inv /\ P) /\ <<Next>>_vars => Q'
245-
BY DEF Inv, Next, vars
246-
<2>4. (Inv /\ P) => ENABLED <<Next>>_vars
247-
BY EnabledDef DEF Inv
248-
<2>. HIDE DEF P,Q
249-
<2>. QED
250-
BY <2>2, <2>3, <2>4, PTL
251-
<1>2. (chosen = {} ~> chosen # {}) => ((chosen = {}) => <>(chosen # {}))
252-
BY PTL
253-
<1>3. QED
254-
BY Invariance, <1>1, <1>2, PTL DEF LiveSpec, Spec, Init, Success
208+
<1>1. [][Next]_vars /\ WF_vars(Next) => [](Init => Success)
209+
<2>1. Init' \/ (chosen # {})'
210+
BY DEF Init
211+
<2>2. Init /\ <<Next>>_vars => (chosen # {})'
212+
BY DEF Init, Next, vars
213+
<2>3. Init => ENABLED <<Next>>_vars
214+
BY EnabledNext DEF Init
215+
<2>. QED BY <2>1, <2>2, <2>3, PTL DEF Success
216+
<1>2. QED BY <1>1, PTL DEF LiveSpec, Spec, Success
255217

256218
-----------------------------------------------------------------------------
257219
(***************************************************************************)
@@ -260,15 +222,12 @@ THEOREM LiveSpec => Success
260222
(***************************************************************************)
261223
THEOREM LiveSpecEquals ==
262224
LiveSpec <=> Spec /\ ([]<><<Next>>_vars \/ []<>(chosen # {}))
263-
<1>1. /\ Spec <=> Spec /\ []TypeOK
264-
/\ LiveSpec <=> LiveSpec /\ []TypeOK
265-
BY Invariance, PTL DEF LiveSpec, Inv
266-
<1>2. (chosen # {}) <=> ~(chosen = {})
225+
<1>1. (chosen # {}) <=> ~(chosen = {})
267226
OBVIOUS
268-
<1>3. []TypeOK => (([]<>~ENABLED <<Next>>_vars) <=> []<>(chosen # {}))
269-
BY <1>2, EnabledDef, PTL
227+
<1>2. ([]<>~ENABLED <<Next>>_vars) <=> []<>(chosen # {})
228+
BY <1>1, EnabledNext, PTL
270229
<1>4. QED
271-
BY <1>1, <1>3, PTL DEF LiveSpec
230+
BY <1>2, PTL DEF LiveSpec
272231
=============================================================================
273232
\* Modification History
274233
\* Last modified Mon May 11 18:36:27 CEST 2020 by merz

0 commit comments

Comments
 (0)