From e44b9ae5a616f6d6fbe044d8e395395accbd45f5 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Sat, 1 Aug 2026 21:42:37 +0300 Subject: [PATCH 1/3] EWD998: close the nine lemmas that were stated without proof EWD998_proof.tla asserted nine lemmas with no proof. Steps carrying no proof generate no obligation, so tlapm reported "All 807 obligations proved" and exited 0, and `--strict` (tlaplus/tlapm#278) exits 11. The six FoldFunctionOnSet* lemmas are now imported from FunctionTheorems, where they are proved. SumIsInt, SumIsNat and SumEqual get structured proofs on top of them, using FS_Subset to carry finiteness from Node to the index set. SumIterate and SumUnion do not go through that way: TLAPS cannot instantiate the second-order op(_,_) against the LAMBDA in Sum. They are proved instead from MapThenSumSetAddElement and MapThenSumSetDisjointUnion in FiniteSetsExtTheorems, whose operator is unary, and which coincide with Sum once the definitions are unfolded. Functions.tla gains SumFunctionOnSet and SumFunction, which FunctionTheorems requires and the vendored copy predates. With tlapm 1.6.0-pre: 851 obligations, all proved, `--strict` exit 0. Runtime rose from roughly one minute to a minute and a half locally, so maxRuntimeMinutes goes from 2 to 4. Signed-off-by: Vasilis Nasopoulos --- specifications/ewd998/EWD998_proof.tla | 91 +++++++++++++------------- specifications/ewd998/Functions.tla | 10 +++ specifications/ewd998/manifest.json | 2 +- 3 files changed, 56 insertions(+), 47 deletions(-) diff --git a/specifications/ewd998/EWD998_proof.tla b/specifications/ewd998/EWD998_proof.tla index 420efcfe..008cdeca 100644 --- a/specifications/ewd998/EWD998_proof.tla +++ b/specifications/ewd998/EWD998_proof.tla @@ -2,7 +2,7 @@ (***************************************************************************) (* Proofs checked by TLAPS about the EWD998 specification. *) (***************************************************************************) -EXTENDS EWD998, FiniteSetTheorems, TLAPS +EXTENDS EWD998, FiniteSetTheorems, FunctionTheorems, FiniteSetsExtTheorems, TLAPS USE NAssumption @@ -54,47 +54,6 @@ IsCommutativeOn(op(_,_), S) == IsIdentityOn(op(_,_), e, S) == \A x \in S : op(e,x) = x -LEMMA FoldFunctionIsFoldFunctionOnSet == - ASSUME NEW op(_,_), NEW base, NEW fun - PROVE FoldFunction(op, base, fun) = FoldFunctionOnSet(op, base, fun, DOMAIN fun) - -LEMMA FoldFunctionOnSetEmpty == - ASSUME NEW op(_,_), NEW base, NEW fun - PROVE FoldFunctionOnSet(op, base, fun, {}) = base - -LEMMA FoldFunctionOnSetIterate == - ASSUME NEW op(_,_), - NEW S, IsFiniteSet(S), NEW T, - NEW base \in T, NEW fun \in [S -> T], - NEW inds \in SUBSET S, NEW e \in inds, - IsAssociativeOn(op, T), IsCommutativeOn(op, T), IsIdentityOn(op, base, T) - PROVE FoldFunctionOnSet(op, base, fun, inds) - = op(fun[e], FoldFunctionOnSet(op, base, fun, inds \ {e})) - -LEMMA FoldFunctionOnSetUnion == - ASSUME NEW op(_,_), - NEW S, IsFiniteSet(S), NEW T, - NEW base \in T, NEW fun \in [S -> T], - NEW inds1 \in SUBSET S, NEW inds2 \in SUBSET S, inds1 \cap inds2 = {}, - IsAssociativeOn(op, T), IsCommutativeOn(op, T), IsIdentityOn(op, base, T) - PROVE FoldFunctionOnSet(op, base, fun, inds1 \cup inds2) - = op(FoldFunctionOnSet(op, base, fun, inds1), FoldFunctionOnSet(op, base, fun, inds2)) - -LEMMA FoldFunctionOnSetEqual == - ASSUME NEW op(_,_), - NEW S, IsFiniteSet(S), NEW T, NEW base \in T, - NEW f \in [S -> T], NEW g \in [S -> T], - NEW inds \in SUBSET S, - \A x \in inds : f[x] = g[x] - PROVE FoldFunctionOnSet(op, base, f, inds) = FoldFunctionOnSet(op, base, g, inds) - -LEMMA FoldFunctionOnSetType == - ASSUME NEW op(_,_), - NEW S, NEW T, IsFiniteSet(S), - NEW base \in T, NEW fun \in [S -> T], - NEW inds \in SUBSET S, - \A x,y \in T : op(x,y) \in T - PROVE FoldFunctionOnSet(op, base, fun, inds) \in T (***************************************************************************) (* The provers have trouble applying these generic lemmas to the specific *) @@ -122,7 +81,19 @@ LEMMA SumIterate == ASSUME NEW fun \in [Node -> Int], NEW inds \in SUBSET Node, NEW e \in inds PROVE Sum(fun, inds) = fun[e] + Sum(fun, inds \ {e}) -\* BY FoldFunctionOnSetIterate, NodeIsFinite, PlusACI DEF Sum (* fails *) +<1>1. IsFiniteSet(inds \ {e}) + BY NodeIsFinite, FS_Subset +<1>2. e \notin inds \ {e} + OBVIOUS +<1>3. inds = (inds \ {e}) \union {e} + OBVIOUS +<1>4. \A s \in (inds \ {e}) \union {e} : fun[s] \in Int + OBVIOUS +<1>5. MapThenSumSet(LAMBDA s : fun[s], (inds \ {e}) \union {e}) + = fun[e] + MapThenSumSet(LAMBDA s : fun[s], inds \ {e}) + BY <1>1, <1>2, <1>4, MapThenSumSetAddElement +<1>. QED + BY <1>3, <1>5 DEF Sum, MapThenSumSet, FoldFunctionOnSet LEMMA SumSingleton == ASSUME NEW fun \in [Node -> Int], NEW x \in Node @@ -133,25 +104,53 @@ LEMMA SumUnion == ASSUME NEW fun \in [Node -> Int], NEW inds1 \in SUBSET Node, NEW inds2 \in SUBSET Node, inds1 \cap inds2 = {} PROVE Sum(fun, inds1 \cup inds2) = Sum(fun, inds1) + Sum(fun, inds2) +<1>1. IsFiniteSet(inds1) /\ IsFiniteSet(inds2) + BY NodeIsFinite, FS_Subset +<1>2. \A x \in inds1 \union inds2 : fun[x] \in Int + OBVIOUS +<1>. QED + BY <1>1, <1>2, MapThenSumSetDisjointUnion + DEF Sum, MapThenSumSet, FoldFunctionOnSet LEMMA SumEqual == ASSUME NEW f \in [Node -> Int], NEW g \in [Node -> Int], NEW inds \in SUBSET Node, \A x \in inds : f[x] = g[x] PROVE Sum(f, inds) = Sum(g, inds) -\* BY FoldFunctionOnSetEqual, NodeIsFinite DEF Sum (* fails *) +<1>1. IsFiniteSet(inds) + BY NodeIsFinite, FS_Subset +<1>. QED + BY <1>1, FoldFunctionOnSetEqual DEF Sum LEMMA SumIsInt == ASSUME NEW fun \in [Node -> Int], NEW inds \in SUBSET Node PROVE Sum(fun, inds) \in Int -BY FoldFunctionOnSetType, NodeIsFinite, Isa DEF Sum +<1>1. IsFiniteSet(inds) + BY NodeIsFinite, FS_Subset +<1>2. \A i \in inds : fun[i] \in Int + OBVIOUS +<1>3. \A t,u \in Int : t + u \in Int + OBVIOUS +<1>4. 0 \in Int + OBVIOUS +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, FoldFunctionOnSetType DEF Sum LEMMA SumIsNat == ASSUME NEW fun \in [Node -> Nat], NEW inds \in SUBSET Node PROVE Sum(fun, inds) \in Nat -BY FoldFunctionOnSetType, NodeIsFinite, \A x,y \in Nat: x+y \in Nat, IsaM("blast") DEF Sum +<1>1. IsFiniteSet(inds) + BY NodeIsFinite, FS_Subset +<1>2. \A i \in inds : fun[i] \in Nat + OBVIOUS +<1>3. \A t,u \in Nat : t + u \in Nat + OBVIOUS +<1>4. 0 \in Nat + OBVIOUS +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, FoldFunctionOnSetType, IsaM("blast") DEF Sum LEMMA SumZero == ASSUME NEW fun \in [Node -> Int], NEW inds \in SUBSET Node, diff --git a/specifications/ewd998/Functions.tla b/specifications/ewd998/Functions.tla index 4b0652b0..e1cd0577 100644 --- a/specifications/ewd998/Functions.tla +++ b/specifications/ewd998/Functions.tla @@ -6,6 +6,7 @@ (* \vspace{12pt}}^' *) (***************************************************************************) +EXTENDS Integers LOCAL INSTANCE Folds (***************************************************************************) @@ -167,6 +168,15 @@ FoldFunctionOnSet(op(_,_), base, fun, indices) == (***************************************************************************) MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices) + +(***************************************************************************) +(* Sum of the values of a function, over a set of indices or over its *) +(* entire domain. Required by FunctionTheorems. *) +(***************************************************************************) +SumFunctionOnSet(fun, indices) == FoldFunctionOnSet(+, 0, fun, indices) + +SumFunction(fun) == SumFunctionOnSet(fun, DOMAIN fun) + ============================================================================= \* Modification History \* Last modified Tue Nov 01 08:46:11 CET 2022 by merz diff --git a/specifications/ewd998/manifest.json b/specifications/ewd998/manifest.json index dafe41cc..95e907ca 100644 --- a/specifications/ewd998/manifest.json +++ b/specifications/ewd998/manifest.json @@ -162,7 +162,7 @@ "features": [], "models": [], "proof": { - "maxRuntimeMinutes": 2 + "maxRuntimeMinutes": 4 } }, { From c45749c4d7eef13b487b3d65c5a1dc4a2d5a5349 Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Sun, 2 Aug 2026 20:28:46 +0300 Subject: [PATCH 2/3] Address review: drop the local Functions copy and the now-unused operators Functions.tla here was a subset of the Community Modules version, which is already on the include path, so the local copy is removed. IsAssociativeOn, IsCommutativeOn and IsIdentityOn were only there to state PlusACI, and PlusACI is no longer referenced now that the fold lemmas come from FunctionTheorems. All four are removed; NodeIsFinite stays. 850 obligations, all proved, --strict exit 0. Signed-off-by: Vasilis Nasopoulos --- specifications/ewd998/EWD998_proof.tla | 28 +--- specifications/ewd998/Functions.tla | 186 ------------------------- 2 files changed, 3 insertions(+), 211 deletions(-) delete mode 100644 specifications/ewd998/Functions.tla diff --git a/specifications/ewd998/EWD998_proof.tla b/specifications/ewd998/EWD998_proof.tla index 008cdeca..9515d554 100644 --- a/specifications/ewd998/EWD998_proof.tla +++ b/specifications/ewd998/EWD998_proof.tla @@ -43,35 +43,13 @@ THEOREM TypeCorrect == Init /\ [][Next]_vars => []TypeOK <1>. QED BY <1>1, <1>2, PTL (***************************************************************************) -(* Lemmas about FoldFunction that should go to a library. *) -(***************************************************************************) -IsAssociativeOn(op(_,_), S) == - \A x,y,z \in S : op(x, op(y,z)) = op(op(x,y), z) - -IsCommutativeOn(op(_,_), S) == - \A x,y \in S : op(x,y) = op(y,x) - -IsIdentityOn(op(_,_), e, S) == - \A x \in S : op(e,x) = x - - -(***************************************************************************) -(* The provers have trouble applying these generic lemmas to the specific *) -(* instances required for the spec so we restate them for the operators *) -(* that appear in the definition of the inductive invariant. *) +(* The provers have trouble applying the generic lemmas to the specific *) +(* instances required for the spec, so the ones needed here are restated *) +(* for the operators that appear in the inductive invariant. *) (***************************************************************************) LEMMA NodeIsFinite == IsFiniteSet(Node) BY FS_Interval DEF Node -LEMMA PlusACI == - /\ IsAssociativeOn(+, Nat) - /\ IsCommutativeOn(+, Nat) - /\ IsIdentityOn(+, 0, Nat) - /\ IsAssociativeOn(+, Int) - /\ IsCommutativeOn(+, Int) - /\ IsIdentityOn(+, 0, Int) -BY DEF IsAssociativeOn, IsCommutativeOn, IsIdentityOn - LEMMA SumEmpty == ASSUME NEW fun PROVE Sum(fun, {}) = 0 diff --git a/specifications/ewd998/Functions.tla b/specifications/ewd998/Functions.tla deleted file mode 100644 index e1cd0577..00000000 --- a/specifications/ewd998/Functions.tla +++ /dev/null @@ -1,186 +0,0 @@ ------------------------------- MODULE Functions ----------------------------- -(***************************************************************************) -(* `^{\large\bf \vspace{12pt} *) -(* Notions about functions including injection, surjection, and bijection.*) -(* Originally contributed by Tom Rodeheffer, MSR. *) -(* \vspace{12pt}}^' *) -(***************************************************************************) - -EXTENDS Integers -LOCAL INSTANCE Folds - -(***************************************************************************) -(* Restriction of a function to a set (should be a subset of the domain). *) -(***************************************************************************) -Restrict(f,S) == [ x \in S |-> f[x] ] - -(***************************************************************************) -(* Restriction of a function to the subset of its domain satisfying a *) -(* test predicate. *) -(* *) -(* Example: *) -(* (LET f == (0 :> "a" @@ 1 :> "b" @@ 2 :> "c") *) -(* IN RestrictDomain(f, LAMBDA x : x \in {0,2})) *) -(* = (0 :> "a" @@ 2 :> "c") *) -(***************************************************************************) -RestrictDomain(f, Test(_)) == Restrict(f, {x \in DOMAIN f : Test(x)}) - -(***************************************************************************) -(* Restriction of a function to the subset of its domain for which the *) -(* function values satisfy a test predicate. *) -(* *) -(* Example: *) -(* (LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* IN RestrictValues(f, LAMBDA y : y \in {0,2})) *) -(* = ("a" :> 0 @@ "b" :> 2) *) -(* *) -(* This is similar to the operator SelectSeq from the standard Sequences *) -(* module and related to standard "filter" functions in functional *) -(* programming. However, SelectSeq produces sequences, whereas *) -(* RestrictValues will in general not. For example, *) -(* *) -(* RestrictValues([0,1,2], LAMBDA y : y \in {0,2}) *) -(* = (1 :> 0 @@ 3 :> 2) *) -(***************************************************************************) -RestrictValues(f, Test(_)) == - LET S == {x \in DOMAIN f : Test(f[x])} - IN Restrict(f, S) - -(***************************************************************************) -(* Check if a function narrow is a restriction of a function wide, i.e. *) -(* Is the domain of narrow a subset of that of wide, and does the *) -(* projection of wide on the domain of narrow have the same image as *) -(* narrow does. *) -(* *) -(* Examples: *) -(* IsRestriction([one |-> 1], [one |-> 1, two |-> 2]) *) -(* IsRestriction([one |-> 1], [one |-> 1]) *) -(* ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3]) *) -(* ~IsRestriction([one |-> 1], [2 |-> two]) *) -(* ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2]) *) -(***************************************************************************) -IsRestriction(narrow, wide) == - /\ DOMAIN narrow \subseteq DOMAIN wide - /\ \A x \in DOMAIN narrow \intersect DOMAIN wide: narrow[x] = wide[x] - -(***************************************************************************) -(* Range of a function. *) -(* Note: The image of a set under function f can be defined as *) -(* Range(Restrict(f,S)). *) -(***************************************************************************) -Range(f) == { f[x] : x \in DOMAIN f } - -(***************************************************************************) -(* Assuming DOMAIN f \subseteq DOMAIN g, apply the binary operation T to *) -(* the corresponding elements of the two functions f and g. *) -(* *) -(* Example: *) -(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3) *) -(* IN Pointwise(f,g,+) = ("a" :> 1 @@ "b" :> 2 @@ "c" :> 5 ) *) -(***************************************************************************) -Pointwise(f, g, T(_,_)) == [ e \in DOMAIN f |-> T(f[e], g[e]) ] - -(***************************************************************************) -(* The inverse of a function. *) -(* Example: *) -(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* IN Inverse(f, DOMAIN f, Range(f)) = *) -(* (0 :> "a" @@ 1 :> "b" @@ 2 :> "c") *) -(* Example: *) -(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* IN Inverse(f, DOMAIN f, {1,3}) = *) -(* 1 :> "b" @@ 3 :> "a") *) -(***************************************************************************) -Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t] - -(***************************************************************************) -(* The inverse of a function. *) -(***************************************************************************) -AntiFunction(f) == Inverse(f, DOMAIN f, Range(f)) - -(***************************************************************************) -(* A function is injective iff it maps each element in its domain to a *) -(* distinct element. *) -(* *) -(* This definition is overridden by TLC in the Java class Functions.java *) -(* The operator is overridden by the Java method with the same name. *) -(***************************************************************************) -IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b - -(***************************************************************************) -(* Set of injections between two sets. *) -(***************************************************************************) -Injection(S,T) == { M \in [S -> T] : IsInjective(M) } - - -(***************************************************************************) -(* A map is a surjection iff for each element in the range there is some *) -(* element in the domain that maps to it. *) -(***************************************************************************) -Surjection(S,T) == { M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t } - - -(***************************************************************************) -(* A map is a bijection iff it is both an injection and a surjection. *) -(***************************************************************************) -Bijection(S,T) == Injection(S,T) \cap Surjection(S,T) - - -(***************************************************************************) -(* An injection, surjection, or bijection exists if the corresponding set *) -(* is nonempty. *) -(***************************************************************************) -ExistsInjection(S,T) == Injection(S,T) # {} -ExistsSurjection(S,T) == Surjection(S,T) # {} -ExistsBijection(S,T) == Bijection(S,T) # {} - --------------------------------------------------------------------------------- - -FoldFunction(op(_,_), base, fun) == - (***************************************************************************) - (* Applies the binary function op on all elements of fun in arbitrary *) - (* order starting with op(f[k], base). The resulting function is: *) - (* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) - (* *) - (* op must be associative and commutative, because we can not assume a *) - (* particular ordering of i, j, and k *) - (* *) - (* Example: *) - (* FoldFunction(LAMBDA x,y: {x} \cup y, {}, <<1,2,1>>) = {1,2} *) - (***************************************************************************) - MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, DOMAIN fun) - - -FoldFunctionOnSet(op(_,_), base, fun, indices) == - (***************************************************************************) - (* Applies the binary function op on the given indices of fun in arbitrary *) - (* order starting with op(f[k], base). The resulting function is: *) - (* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) - (* *) - (* op must be associative and commutative, because we can not assume a *) - (* particular ordering of i, j, and k *) - (* *) - (* indices must be a subset of DOMAIN(fun) *) - (* *) - (* Example: *) - (* FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, <<1,2>>, {}) = {} *) - (***************************************************************************) - MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices) - - -(***************************************************************************) -(* Sum of the values of a function, over a set of indices or over its *) -(* entire domain. Required by FunctionTheorems. *) -(***************************************************************************) -SumFunctionOnSet(fun, indices) == FoldFunctionOnSet(+, 0, fun, indices) - -SumFunction(fun) == SumFunctionOnSet(fun, DOMAIN fun) - -============================================================================= -\* Modification History -\* Last modified Tue Nov 01 08:46:11 CET 2022 by merz -\* Last modified Mon Apr 05 03:25:53 CEST 2021 by marty -\* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav -\* Last modified Fri May 03 12:55:35 PDT 2013 by tomr -\* Created Thu Apr 11 10:30:48 PDT 2013 by tomr From cab9d849172c78b47b3b83f55196661fc8d4838f Mon Sep 17 00:00:00 2001 From: Vasilis Nasopoulos Date: Sun, 2 Aug 2026 21:22:22 +0300 Subject: [PATCH 3/3] Drop the Functions.tla entry from the manifest The module was removed in the previous commit but its manifest entry was left behind, so check_manifest_files.py failed on every platform. Signed-off-by: Vasilis Nasopoulos --- specifications/ewd998/manifest.json | 5 ----- 1 file changed, 5 deletions(-) diff --git a/specifications/ewd998/manifest.json b/specifications/ewd998/manifest.json index 95e907ca..9d8c35b8 100644 --- a/specifications/ewd998/manifest.json +++ b/specifications/ewd998/manifest.json @@ -170,11 +170,6 @@ "features": [], "models": [] }, - { - "path": "specifications/ewd998/Functions.tla", - "features": [], - "models": [] - }, { "path": "specifications/ewd998/SmokeEWD998.tla", "features": [],