From 40d883d0d61805bcba89b3b55dcb84d8b150d299 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Mon, 8 Dec 2025 11:44:00 +0100 Subject: [PATCH 1/8] adapting proofs to modified FS_Induction theorem Signed-off-by: Stephan Merz --- specifications/LoopInvariance/Quicksort.tla | 24 +++----- specifications/byzpaxos/BPConProof.tla | 11 ++-- specifications/byzpaxos/VoteProof.tla | 68 +++------------------ specifications/ewd998/EWD998_proof.tla | 5 +- 4 files changed, 26 insertions(+), 82 deletions(-) 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/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 From 57bc62663cf99cdaac21880ea36de19c22d958fd Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Mon, 8 Dec 2025 13:23:07 +0100 Subject: [PATCH 2/8] skip long-running proofs in CI Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 0efddefb..0c268550 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -135,9 +135,16 @@ jobs: - name: Check proofs if: matrix.os != 'windows-latest' && !matrix.unicode run: | + # skip proofs that take too long on certain GitHub runners + SKIP=( + "specifications/ewd998/EWD998_proof.tla" + "specifications/LoopInvariance/Quicksort.tla" + "specifications/lamport_mutex/LamportMutex_proofs.tla" + ) python $SCRIPT_DIR/check_proofs.py \ --tlapm_path $DEPS_DIR/tlapm \ - --examples_root . + --examples_root . \ + --skip "${SKIP[@]}" - name: Smoke-test manifest generation script run: | python $SCRIPT_DIR/generate_manifest.py \ From 018369bed39e87e81812919fab846f130e8b2b55 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 11 Dec 2025 17:15:34 +0100 Subject: [PATCH 3/8] request longer timeout for CI proof checking Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 1 - specifications/LoopInvariance/manifest.json | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 0c268550..788a69c8 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -138,7 +138,6 @@ jobs: # skip proofs that take too long on certain GitHub runners SKIP=( "specifications/ewd998/EWD998_proof.tla" - "specifications/LoopInvariance/Quicksort.tla" "specifications/lamport_mutex/LamportMutex_proofs.tla" ) python $SCRIPT_DIR/check_proofs.py \ 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" } }, { From 26a68877ea52c07148a1749bf32f431fdc19aa97 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sat, 13 Dec 2025 08:18:08 +0100 Subject: [PATCH 4/8] longer timeouts for proofs Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 11 +++++------ specifications/ewd998/manifest.json | 2 +- specifications/lamport_mutex/manifest.json | 2 +- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 788a69c8..22598e71 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -136,14 +136,13 @@ jobs: if: matrix.os != 'windows-latest' && !matrix.unicode run: | # skip proofs that take too long on certain GitHub runners - SKIP=( - "specifications/ewd998/EWD998_proof.tla" - "specifications/lamport_mutex/LamportMutex_proofs.tla" - ) + # SKIP=( + # "specifications/ewd998/EWD998_proof.tla" + # "specifications/lamport_mutex/LamportMutex_proofs.tla" + # ) python $SCRIPT_DIR/check_proofs.py \ --tlapm_path $DEPS_DIR/tlapm \ - --examples_root . \ - --skip "${SKIP[@]}" + --examples_root ." - name: Smoke-test manifest generation script run: | python $SCRIPT_DIR/generate_manifest.py \ 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" } }, { From d6aa38aae3fdead710047848f21d2d7c45f386ca Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sat, 13 Dec 2025 14:56:27 +0100 Subject: [PATCH 5/8] fix typo in CI.yml Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 22598e71..98e91f1b 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -142,7 +142,7 @@ jobs: # ) python $SCRIPT_DIR/check_proofs.py \ --tlapm_path $DEPS_DIR/tlapm \ - --examples_root ." + --examples_root . - name: Smoke-test manifest generation script run: | python $SCRIPT_DIR/generate_manifest.py \ From 53e79d744bd47d6ad4ed44b7433aceff68a866c6 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sun, 14 Dec 2025 09:15:32 +0100 Subject: [PATCH 6/8] set 1000 seconds limit for proof checking per example Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 98e91f1b..fb380d78 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -135,13 +135,9 @@ jobs: - name: Check proofs if: matrix.os != 'windows-latest' && !matrix.unicode run: | - # skip proofs that take too long on certain GitHub runners - # SKIP=( - # "specifications/ewd998/EWD998_proof.tla" - # "specifications/lamport_mutex/LamportMutex_proofs.tla" - # ) python $SCRIPT_DIR/check_proofs.py \ --tlapm_path $DEPS_DIR/tlapm \ + --runtime_seconds_limit 1000 \ --examples_root . - name: Smoke-test manifest generation script run: | From 20193ba618fe4c612b14caa0e935a04d14947cb4 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sun, 14 Dec 2025 09:44:34 +0100 Subject: [PATCH 7/8] fix typo Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index fb380d78..008c9e12 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -137,7 +137,7 @@ jobs: run: | python $SCRIPT_DIR/check_proofs.py \ --tlapm_path $DEPS_DIR/tlapm \ - --runtime_seconds_limit 1000 \ + --runtime_seconds_limit "1000" \ --examples_root . - name: Smoke-test manifest generation script run: | From 6f27db0dc0138d3c3feb5ed2a615db87b9130645 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sun, 14 Dec 2025 10:56:16 +0100 Subject: [PATCH 8/8] reverting time limit Signed-off-by: Stephan Merz --- .github/workflows/CI.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 008c9e12..0efddefb 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -137,7 +137,6 @@ jobs: run: | python $SCRIPT_DIR/check_proofs.py \ --tlapm_path $DEPS_DIR/tlapm \ - --runtime_seconds_limit "1000" \ --examples_root . - name: Smoke-test manifest generation script run: |