diff --git a/specifications/LoopInvariance/Quicksort.tla b/specifications/LoopInvariance/Quicksort.tla index 380f2e9a..76bb5a49 100644 --- a/specifications/LoopInvariance/Quicksort.tla +++ b/specifications/LoopInvariance/Quicksort.tla @@ -104,14 +104,12 @@ LEMMA NonemptyMin == ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), NEW x \in S PROVE /\ Min(S) \in S /\ Min(S) <= x -<1>. DEFINE P(T) == T \in SUBSET Int => - /\ T # {} => Min(T) \in T - /\ \A y \in T : Min(T) <= y +<1>. DEFINE P(T) == /\ T # {} => Min(T) \in T + /\ \A y \in T : Min(T) <= y <1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW y, y \notin T, P(T) +<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW y \in S \ T PROVE P(T \cup {y}) - <2>. HAVE T \cup {y} \in SUBSET Int <2>1. CASE T = {} <3>1. y = Min(T \cup {y}) BY <2>1 DEF Min @@ -135,7 +133,7 @@ LEMMA NonemptyMin == <4>. QED BY <4>1, <4>2 <3>. QED BY <3>1, <3>2 <2>. QED BY <2>1, <2>2 -<1>3. \A T : IsFiniteSet(T) => P(T) +<1>3. P(S) <2>. HIDE DEF P <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>. QED BY <1>3 @@ -144,14 +142,12 @@ LEMMA NonemptyMax == ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), NEW x \in S PROVE /\ Max(S) \in S /\ x <= Max(S) -<1>. DEFINE P(T) == T \in SUBSET Int => - /\ T # {} => Max(T) \in T - /\ \A y \in T : y <= Max(T) +<1>. DEFINE P(T) == /\ T # {} => Max(T) \in T + /\ \A y \in T : y <= Max(T) <1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW y, y \notin T, P(T) +<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW y \in S \ T PROVE P(T \cup {y}) - <2>. HAVE T \cup {y} \in SUBSET Int <2>1. CASE T = {} <3>1. y = Max(T \cup {y}) BY <2>1 DEF Max @@ -175,7 +171,7 @@ LEMMA NonemptyMax == <4>. QED BY <4>1, <4>2 <3>. QED BY <3>1, <3>2 <2>. QED BY <2>1, <2>2 -<1>3. \A T : IsFiniteSet(T) => P(T) +<1>3. P(S) <2>. HIDE DEF P <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>. QED BY <1>3 @@ -260,9 +256,9 @@ BY PermsOfLemma DEF Partitions (* Below is the TLA+ translation of the PlusCal code. *) (***************************************************************************) \* BEGIN TRANSLATION -VARIABLES seq, seq0, U, pc +VARIABLES pc, seq, seq0, U -vars == << seq, seq0, U, pc >> +vars == << pc, seq, seq0, U >> Init == (* Global variables *) /\ seq \in Seq(Values) \ {<< >>} diff --git a/specifications/LoopInvariance/manifest.json b/specifications/LoopInvariance/manifest.json index 77abcd41..4e72970f 100644 --- a/specifications/LoopInvariance/manifest.json +++ b/specifications/LoopInvariance/manifest.json @@ -56,7 +56,7 @@ ], "models": [], "proof": { - "runtime": "00:00:45" + "runtime": "00:05:00" } }, { diff --git a/specifications/byzpaxos/BPConProof.tla b/specifications/byzpaxos/BPConProof.tla index 1e1c49c5..6c8ec407 100644 --- a/specifications/byzpaxos/BPConProof.tla +++ b/specifications/byzpaxos/BPConProof.tla @@ -673,16 +673,15 @@ MaxBallot(S) == (* maximum of S when S is nonempty, we need the following fact. *) (***************************************************************************) LEMMA FiniteSetHasMax == - \A S \in SUBSET Int : - IsFiniteSet(S) /\ (S # {}) => \E max \in S : \A x \in S : max >= x -<1>. DEFINE P(S) == S \subseteq Int /\ S # {} => - \E max \in S : \A x \in S : max >= x + ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), S # {} + PROVE \E max \in S : \A x \in S : max >= x +<1>. DEFINE P(T) == T # {} => \E max \in T : \A x \in T : max >= x <1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW x, P(T) +<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T PROVE P(T \cup {x}) BY <1>2 -<1>3. \A S : IsFiniteSet(S) => P(S) +<1>3. P(S) <2>. HIDE DEF P <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>. QED BY <1>3, Zenon diff --git a/specifications/byzpaxos/VoteProof.tla b/specifications/byzpaxos/VoteProof.tla index 628c324e..c313093c 100644 --- a/specifications/byzpaxos/VoteProof.tla +++ b/specifications/byzpaxos/VoteProof.tla @@ -1022,13 +1022,13 @@ ASSUME ValueNonempty == Value # {} LEMMA FiniteSetHasMax == ASSUME NEW S \in SUBSET Int, IsFiniteSet(S), S # {} PROVE \E max \in S : \A x \in S : max >= x -<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E max \in T : \A x \in T : max >= x +<1>. DEFINE P(T) == T # {} => \E max \in T : \A x \in T : max >= x <1>1. P({}) OBVIOUS -<1>2. ASSUME NEW T, NEW x, P(T), x \notin T +<1>2. ASSUME NEW T \in SUBSET S, P(T), NEW x \in S \ T PROVE P(T \cup {x}) BY <1>2 -<1>3. \A T : IsFiniteSet(T) => P(T) +<1>3. P(S) <2>. HIDE DEF P <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>. QED BY <1>3, Zenon @@ -1150,50 +1150,6 @@ LiveSpec == Spec /\ LiveAssumption (***************************************************************************) ----------------------------------------------------------------------------- (***************************************************************************) -(* Here are two temporal-logic proof rules. Their validity is obvious *) -(* when you understand what they mean. *) -(***************************************************************************) -THEOREM AlwaysForall == - ASSUME NEW CONSTANT S, NEW TEMPORAL P(_) - PROVE (\A s \in S : []P(s)) <=> [](\A s \in S : P(s)) -OBVIOUS - -LEMMA EventuallyAlwaysForall == - ASSUME NEW CONSTANT S, IsFiniteSet(S), - NEW TEMPORAL P(_) - PROVE (\A s \in S : <>[]P(s)) => <>[](\A s \in S : P(s)) -<1>. DEFINE A(x) == <>[]P(x) - L(T) == \A s \in T : A(s) - R(T) == \A s \in T : P(s) - Q(T) == L(T) => <>[]R(T) -<1>1. Q({}) - <2>1. R({}) OBVIOUS - <2>2. <>[]R({}) BY <2>1, PTL - <2>. QED BY <2>2 -<1>2. ASSUME NEW T, NEW x - PROVE Q(T) => Q(T \cup {x}) - <2>1. L(T \cup {x}) => A(x) - <3>. HIDE DEF A - <3>. QED OBVIOUS - <2>2. L(T \cup {x}) /\ Q(T) => <>[]R(T) - OBVIOUS - <2>3. <>[]R(T) /\ A(x) => <>[](R(T) /\ P(x)) - BY PTL - <2>4. R(T) /\ P(x) => R(T \cup {x}) - OBVIOUS - <2>5. <>[](R(T) /\ P(x)) => <>[]R(T \cup {x}) - BY <2>4, PTL - <2>. QED - BY <2>1, <2>2, <2>3, <2>5 -<1>. HIDE DEF Q -<1>3. \A T : IsFiniteSet(T) => Q(T) - BY <1>1, <1>2, FS_Induction, IsaM("blast") -<1>4. Q(S) - BY <1>3 -<1>. QED - BY <1>4 DEF Q ------------------------------------------------------------------------------ -(***************************************************************************) (* Here is our proof that LiveSpec implements the specification LiveSpec *) (* of module Consensus under our refinement mapping. *) (***************************************************************************) @@ -1257,7 +1213,6 @@ THEOREM Liveness == LiveSpec => C!LiveSpec <>[](\A self \in Q : maxBal[self] = b) <2>. DEFINE MB(s) == maxBal[s] = b <2>0. (\A self \in Q : <>[]MB(self)) => <>[](\A self \in Q : MB(self)) - \* BY <1>a, EventuallyAlwaysForall \* fails, even when hiding the definition of MB <3>. HIDE DEF MB <3>. DEFINE A(x) == <>[]MB(x) L(T) == \A self \in T : A(self) \* NB: changing the names of the bound vars makes the QED step fail! @@ -1281,11 +1236,9 @@ THEOREM Liveness == LiveSpec => C!LiveSpec BY <4>4, PTL <4>. QED BY <4>1, <4>2, <4>3, <4>5 <3>. HIDE DEF I - <3>3. \A T : IsFiniteSet(T) => I(T) - BY <3>1, <3>2, FS_Induction, IsaM("blast") - <3>4. I(Q) - BY <1>a, <3>3 - <3>. QED BY <3>4 DEF I + <3>3. I(Q) + BY <1>a, <3>1, <3>2, FS_Induction, IsaM("blast") + <3>. QED BY <3>3 DEF I <2>1. SUFFICES ASSUME NEW self \in Q PROVE Spec /\ LiveAssumption!(Q, b) => <>[]MB(self) BY <2>0, Isa @@ -1481,7 +1434,6 @@ THEOREM Liveness == LiveSpec => C!LiveSpec <3>4. QED BY <3>2, <3>3, PTL <2>4. (\A self \in Q : <>[]Voted(self)) => <>[](\A self \in Q : Voted(self)) - \* again, we need to redo the proof instead of using lemma EventuallyAlwaysForall <3>. DEFINE A(x) == <>[]Voted(x) L(T) == \A self \in T : A(self) R(T) == \A self \in T : Voted(self) @@ -1504,11 +1456,9 @@ THEOREM Liveness == LiveSpec => C!LiveSpec BY <4>4, PTL <4>. QED BY <4>1, <4>2, <4>3, <4>5 <3>. HIDE DEF I - <3>3. \A T : IsFiniteSet(T) => I(T) - BY <3>1, <3>2, FS_Induction, IsaM("blast") - <3>4. I(Q) - BY <1>a, <3>3 - <3>. QED BY <3>4 DEF I + <3>3. I(Q) + BY <1>a, <3>1, <3>2, FS_Induction, IsaM("blast") + <3>. QED BY <3>3 DEF I <2>. QED BY <2>1, VT2, <2>2, <2>3, <2>4, PTL diff --git a/specifications/ewd998/EWD998_proof.tla b/specifications/ewd998/EWD998_proof.tla index 2bd8a15b..b0a6886e 100644 --- a/specifications/ewd998/EWD998_proof.tla +++ b/specifications/ewd998/EWD998_proof.tla @@ -159,12 +159,11 @@ LEMMA SumZero == PROVE Sum(fun, inds) = 0 <1>1. IsFiniteSet(inds) BY NodeIsFinite, FS_Subset -<1>. DEFINE P(T) == T \subseteq inds => Sum(fun, T) = 0 +<1>. DEFINE P(T) == Sum(fun, T) = 0 <1>2. P({}) BY SumEmpty -<1>3. ASSUME NEW T, NEW x, IsFiniteSet(T), P(T), x \notin T +<1>3. ASSUME NEW T \in SUBSET inds, IsFiniteSet(T), P(T), NEW x \in inds \ T PROVE P(T \cup {x}) - <2>. HAVE T \cup {x} \in SUBSET inds <2>1. Sum(fun, T \cup {x}) = fun[x] + Sum(fun, (T \cup {x}) \ {x}) BY SumIterate <2>2. /\ fun[x] = 0 diff --git a/specifications/ewd998/manifest.json b/specifications/ewd998/manifest.json index 85d3a0c9..0a8c93b2 100644 --- a/specifications/ewd998/manifest.json +++ b/specifications/ewd998/manifest.json @@ -154,7 +154,7 @@ "features": [], "models": [], "proof": { - "runtime": "00:00:30" + "runtime": "00:05:00" } }, { diff --git a/specifications/lamport_mutex/manifest.json b/specifications/lamport_mutex/manifest.json index cb278619..bb2dbaa2 100644 --- a/specifications/lamport_mutex/manifest.json +++ b/specifications/lamport_mutex/manifest.json @@ -15,7 +15,7 @@ "features": [], "models": [], "proof": { - "runtime": "00:00:45" + "runtime": "00:05:00" } }, {