Theorems for sum of constant function#124
Merged
Merged
Conversation
Adds a new `tlaps` job to both the push (main.yml) and pull request (pr.yml) GitHub Actions workflows. The job downloads the TLAPS 1.6.0-pre release from tlaplus/tlapm and runs `tlapm` on every modules/*_proofs.tla file, ensuring the proofs of the theorems in FoldsTheorems, FunctionTheorems, FiniteSetsExtTheorems and SequencesExtTheorems remain valid as the modules evolve. The job runs as a matrix on ubuntu-latest (x86_64-linux-gnu) and macos-latest (arm64-darwin), the two platforms for which the 1.6.0-pre release ships a tlapm binary. All proof files are checked even if one fails so a single regression does not mask others. [CI] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The first case of THEOREM Fun_NatBijSingleton was discharged by a single
one-liner
BY 1..1 = {1} DEF Bijection, Surjection
which asks the default SMT pipeline to simultaneously unfold Bijection =
Injection \cap Surjection, expand the set comprehension defining
Surjection, instantiate the nested \A t \in S : \E s \in 1..1 : f[s] = t
and witness the outer \E s : S = {s}. This worked with the bundled
provers shipped with the macOS arm64 build of TLAPS 1.6.0-pre but failed
with the Linux x86_64 build, which ships different Z3/Zenon/Isabelle
binaries and runs on a slower CI runner. The same input file even
produced a different obligation count on the two platforms (771 vs.
732), so relying on a single SMT step for this obligation is inherently
fragile.
Rewrite the case as five small steps that any backend can close: extract
the typing and surjection facts from the definitions, derive f[1] \in S,
prove \A t \in S : t = f[1] by PICKing the (unique) index in 1..1, then
WITNESS f[1]. No backend has to invent the existential witness or
reason about set intersection at the same time as a quantified
comprehension, so the proof is robust across tlapm builds and timeout
budgets.
All 795 obligations of FunctionTheorems_proofs continue to check locally
with `tlapm --cleanfp`.
[Proofs]
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
THEOREM MaxInterval and THEOREM MinInterval in FiniteSetsExtTheorems_proofs were both discharged by a single BY DEF Max (resp. BY DEF Min) After unfolding, the obligation contains the raw CHOOSE that defines Max/Min, e.g. (CHOOSE x \in a..b : \A y \in a..b : x >= y) = b To close that in one shot, a backend has to reason about CHOOSE uniqueness while simultaneously doing arithmetic on the interval a..b. Zenon has very limited support for CHOOSE and reported "exhausted search space" with the macOS arm64 build of TLAPS 1.6.0-pre, while another bundled prover happened to find the proof on Linux. Either way, relying on a CHOOSE-savvy backend for these two facts is fragile across tlapm builds. Rewrite both proofs to go through the existing MaxInt / MinInt introduction rules of the same module, which already hide the CHOOSE behind ASSUME S \in SUBSET Int, x \in S, \A y \in S : x >= y PROVE Max(S) = x interface. Each new proof supplies the two trivial arithmetic side conditions (b \in a..b and \A y \in a..b : b >= y, and the symmetric pair for Min) so that no backend ever sees the CHOOSE. All 419 obligations of FiniteSetsExtTheorems_proofs continue to check locally with `tlapm --cleanfp`. [Proofs] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Member
Author
|
@muenchnerkindl This PR was primarily generated by Claude Opus 4.7. I’ve reviewed it and believe it’s in good shape for your review. |
Contributor
|
Hi @lemmy, thanks for this contribution! I suggest to generalize the first theorem so that it only requires the function to be constant over the set that is summed over (cf. push). What do you think? |
Add SumFunctionOnSetConst and SumFunctionConst stating that summing a constant function over a finite set equals the constant times the cardinality of the set, together with corresponding proofs and an example in the doc comments. [Feature] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Signed-off-by: Stephan Merz <stephan.merz@loria.fr> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Member
Author
Thanks @muenchnerkindl, I squashed your commit into mine and removed the commented code. |
lemmy
added a commit
to tlaplus/Examples
that referenced
this pull request
May 13, 2026
Each affected directory now has a `<Spec>_proof.tla` module that
mechanically checks the safety obligations of its TLA+ specification
(typically Spec => []TypeInvariant, plus any SafetyInvariant or
strengthened inductive invariant the spec defines). The original
specifications themselves are not modified by this commit; the prior
commit names a few previously-anonymous `ASSUME` blocks that the
proofs cite by reference.
Specifications covered:
- KeyValueStore
- MultiCarElevator/Elevator
- PaxosHowToWinATuringAward/Voting
- SpecifyingSystems chapters: AsynchronousInterface, FIFO,
HourClock, Composing, Liveness, RealTime, CachingMemory, TLC
- TwoPhase
- allocator (Simple, Scheduling, Implementation)
- byihive/VoucherLifeCycle
- ewd687a/EWD687a
- ewd998/EWD998PCal and EWD998 (TerminationDetection lifted to
Spec => []...)
- transaction_commit (TCommit, TwoPhase, PaxosCommit)
- CoffeeCan, DieHard, MissionariesAndCannibals, SpanTree
(TypeInvariant / TypeOK)
- spanning (SntMsg) and glowingRaccoon clean+stages (TypeOK +
primerPositive + preservationInvariant)
- ReadersWriters (TypeOK + Safety: mutex + at-most-one-writer)
- CigaretteSmokers (TypeOK + AtMostOne)
- LamportMutex (BoundedNetwork, via NetworkInv pigeonhole)
- TeachingConcurrency/Simple and SimpleRegular (TypeOK and Inv
exposed as named theorems matching the .cfg invariants)
Proof-only assumptions added in `*_proof.tla` (not in the spec):
- CigaretteSmokers_proof: IngredientsFinite (Cardinality is
already used inside the spec's own ASSUME, so finiteness is
implicit).
- ReadersWriters_proof: NumActorsIsNat (NumActors \in Nat).
- Elevator_proof: ElevatorFloorDisjoint (Floor \cap Elevator = {};
a TLC modelling convention not stated in the spec).
- SchedulingAllocator_proof, AllocatorImplementation_proof:
ClientsFinite (the spec only assumes Resources finite).
- EWD687a_proof: ProcsFinite (finite process set).
- glowingRaccoon clean_proof and stages_proof: ConstantsAreNat
(DNA, PRIMER \in Nat; without this Spec => []TypeOK is false).
Spec ASSUMEs restated under a name in the proof file (no new fact):
- CigaretteSmokers_proof: OffersAssumption.
- spanning_proof: NoPrntFact.
- SpanTree_proof: ConstantsAssumption.
- CoffeeCan_proof: MaxBeanFact.
Non-trivial proof obligations discharged:
- PaxosCommit_proof: MaximumProp -- the recursive `Maximum` operator
is shown to return the largest element of its (non-empty, finite,
integer >= -1) input via well-founded induction on the strict-subset
ordering, going through a hand-proved recursion equation for the
inner CHOOSE'd recursive function.
- SchedulingAllocator_proof: PermSeqsType -- analogous well-founded
structural induction over `PermSeqs(S)`, plus an explicit
finiteness assumption on `Clients` (added in the proof file only).
- AllocatorImplementation_proof: PermSeqsType -- the same proof
threaded through the `Sched!` instance. One sub-step
(`Sched!PermSeqs(S) = PermsFn(S)[S]`) remains OMITTED because
tlapm's INSTANCE expansion currently mangles the inner LET binding
inside the LET-bound recursive function.
- EWD687a_proof: TreeNodesNonNeutral, TreeStructure, TreeIsTree,
Inv2GivesTreeBody, SpecGivesAlwaysTreeBody -- the structural half
of TreeWithRoot (graph + non-neutral conjuncts) discharged from the
existing Inv1 / Inv2 / NoCycle invariants.
- CRDT_proof: the four previously OMITTED Sum lemmas (SumType,
SumIsZero, SumWeaklyMonotonic, SumStronglyMonotonic) are reduced
to SumFunctionNat, SumFunctionZero, SumFunctionMonotonic, and
SumFunctionStrictlyMonotonic in the community-modules
FunctionTheorems (strengthened and CI-verified in
tlaplus/CommunityModules#124) via the
trivial unfolding Sum(f) = SumFunction(f); FiniteSetTheorems is
dropped from EXTENDS accordingly. The downstream Measure*/Gossip*
lemmas and the OGLiveness / Convergence theorems that already cited
these now check end-to-end (280 obligations).
Remaining OMITTED obligations:
- Elevator_proof: Inv2Next (the inductive step for the strengthened
Inv2; each of its ~10 conjuncts is proven preserved per-action
individually, only the full assembly is left), and four narrow
function-evaluation lemmas (GetDirectionEval, GetDistanceEval,
CanServiceCallEval, PeopleWaitingEval) that unfold a multi-arg
`f[a, b]` definition -- a known tlapm/SMT/Zenon/Isabelle gap,
cf. https://discuss.tlapl.us/msg01519.html.
- EWD687a_proof: AreConnectedToLeader (constructing the path to
Leader by iterating upEdge needs SimplePath/Cardinality
reasoning), Thm_TreeWithRoot's QED (bridges TreeWithRoot's
`LET ... IN [](...)` shape and the equivalent
`[](LET ... IN ...)` that PTL would consume), and Thm_DT2
(Spec => DT2; needs an inductive invariant over
msgs/rcvdUnacked/acks/sentUnacked).
- AllocatorImplementation_proof: PermSeqsIsPermsFn, the equality
`Sched!PermSeqs(S) = PermsFn(S)[S]`, blocked by tlapm rendering
the INSTANCE-expanded inner LET binding as a self-recursive
CHOOSE.
- EWD998PCal_proof: Refinement (Spec => EWD998Spec); per-disjunct
step-simulation requires bag-level lemmas plus the EWD998-level
invariant `B = Sum(counter, Node)` for the token-pass disjunct.
Also, the unique-token preservation conjunct of NetworkOK is
deferred in PCalTypeOKInductive.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to tlaplus/Examples
that referenced
this pull request
May 13, 2026
Each affected directory now has a `<Spec>_proof.tla` module that
mechanically checks the safety obligations of its TLA+ specification
(typically Spec => []TypeInvariant, plus any SafetyInvariant or
strengthened inductive invariant the spec defines). The original
specifications themselves are not modified by this commit; the prior
commit names a few previously-anonymous `ASSUME` blocks that the
proofs cite by reference.
Specifications covered:
- KeyValueStore
- MultiCarElevator/Elevator
- PaxosHowToWinATuringAward/Voting
- SpecifyingSystems chapters: AsynchronousInterface, FIFO,
HourClock, Composing, Liveness, RealTime, CachingMemory, TLC
- TwoPhase
- allocator (Simple, Scheduling, Implementation)
- byihive/VoucherLifeCycle
- ewd687a/EWD687a
- ewd998/EWD998PCal and EWD998 (TerminationDetection lifted to
Spec => []...)
- transaction_commit (TCommit, TwoPhase, PaxosCommit)
- CoffeeCan, DieHard, MissionariesAndCannibals, SpanTree
(TypeInvariant / TypeOK)
- spanning (SntMsg) and glowingRaccoon clean+stages (TypeOK +
primerPositive + preservationInvariant)
- ReadersWriters (TypeOK + Safety: mutex + at-most-one-writer)
- CigaretteSmokers (TypeOK + AtMostOne)
- LamportMutex (BoundedNetwork, via NetworkInv pigeonhole)
- TeachingConcurrency/Simple and SimpleRegular (TypeOK and Inv
exposed as named theorems matching the .cfg invariants)
Proof-only assumptions added in `*_proof.tla` (not in the spec):
- CigaretteSmokers_proof: IngredientsFinite (Cardinality is
already used inside the spec's own ASSUME, so finiteness is
implicit).
- ReadersWriters_proof: NumActorsIsNat (NumActors \in Nat).
- Elevator_proof: ElevatorFloorDisjoint (Floor \cap Elevator = {};
a TLC modelling convention not stated in the spec).
- SchedulingAllocator_proof, AllocatorImplementation_proof:
ClientsFinite (the spec only assumes Resources finite).
- EWD687a_proof: ProcsFinite (finite process set).
- glowingRaccoon clean_proof and stages_proof: ConstantsAreNat
(DNA, PRIMER \in Nat; without this Spec => []TypeOK is false).
Spec ASSUMEs restated under a name in the proof file (no new fact):
- CigaretteSmokers_proof: OffersAssumption.
- spanning_proof: NoPrntFact.
- SpanTree_proof: ConstantsAssumption.
- CoffeeCan_proof: MaxBeanFact.
Non-trivial proof obligations discharged:
- PaxosCommit_proof: MaximumProp -- the recursive `Maximum` operator
is shown to return the largest element of its (non-empty, finite,
integer >= -1) input via well-founded induction on the strict-subset
ordering, going through a hand-proved recursion equation for the
inner CHOOSE'd recursive function.
- SchedulingAllocator_proof: PermSeqsType -- analogous well-founded
structural induction over `PermSeqs(S)`, plus an explicit
finiteness assumption on `Clients` (added in the proof file only).
- AllocatorImplementation_proof: PermSeqsType -- the same proof
threaded through the `Sched!` instance. One sub-step
(`Sched!PermSeqs(S) = PermsFn(S)[S]`) remains OMITTED because
tlapm's INSTANCE expansion currently mangles the inner LET binding
inside the LET-bound recursive function.
- EWD687a_proof: TreeNodesNonNeutral, TreeStructure, TreeIsTree,
Inv2GivesTreeBody, SpecGivesAlwaysTreeBody -- the structural half
of TreeWithRoot (graph + non-neutral conjuncts) discharged from the
existing Inv1 / Inv2 / NoCycle invariants.
- CRDT_proof: the four previously OMITTED Sum lemmas (SumType,
SumIsZero, SumWeaklyMonotonic, SumStronglyMonotonic) are reduced
to SumFunctionNat, SumFunctionZero, SumFunctionMonotonic, and
SumFunctionStrictlyMonotonic in the community-modules
FunctionTheorems (strengthened and CI-verified in
tlaplus/CommunityModules#124) via the
trivial unfolding Sum(f) = SumFunction(f); FiniteSetTheorems is
dropped from EXTENDS accordingly. The downstream Measure*/Gossip*
lemmas and the OGLiveness / Convergence theorems that already cited
these now check end-to-end (280 obligations).
Remaining OMITTED obligations:
- Elevator_proof: Inv2Next (the inductive step for the strengthened
Inv2; each of its ~10 conjuncts is proven preserved per-action
individually, only the full assembly is left), and four narrow
function-evaluation lemmas (GetDirectionEval, GetDistanceEval,
CanServiceCallEval, PeopleWaitingEval) that unfold a multi-arg
`f[a, b]` definition -- a known tlapm/SMT/Zenon/Isabelle gap,
cf. https://discuss.tlapl.us/msg01519.html.
- EWD687a_proof: AreConnectedToLeader (constructing the path to
Leader by iterating upEdge needs SimplePath/Cardinality
reasoning), Thm_TreeWithRoot's QED (bridges TreeWithRoot's
`LET ... IN [](...)` shape and the equivalent
`[](LET ... IN ...)` that PTL would consume), and Thm_DT2
(Spec => DT2; needs an inductive invariant over
msgs/rcvdUnacked/acks/sentUnacked).
- AllocatorImplementation_proof: PermSeqsIsPermsFn, the equality
`Sched!PermSeqs(S) = PermsFn(S)[S]`, blocked by tlapm rendering
the INSTANCE-expanded inner LET binding as a self-recursive
CHOOSE.
- EWD998PCal_proof: Refinement (Spec => EWD998Spec); per-disjunct
step-simulation requires bag-level lemmas plus the EWD998-level
invariant `B = Sum(counter, Node)` for the token-pass disjunct.
Also, the unique-token preservation conjunct of NetworkOK is
deferred in PCalTypeOKInductive.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to tlaplus/Examples
that referenced
this pull request
May 13, 2026
Each affected directory now has a `<Spec>_proof.tla` module that
mechanically checks the safety obligations of its TLA+ specification
(typically Spec => []TypeInvariant, plus any SafetyInvariant or
strengthened inductive invariant the spec defines). The original
specifications themselves are not modified by this commit; the prior
commit names a few previously-anonymous `ASSUME` blocks that the
proofs cite by reference.
Specifications covered:
- KeyValueStore
- MultiCarElevator/Elevator
- PaxosHowToWinATuringAward/Voting
- SpecifyingSystems chapters: AsynchronousInterface, FIFO,
HourClock, Composing, Liveness, RealTime, CachingMemory, TLC
- TwoPhase
- allocator (Simple, Scheduling, Implementation)
- byihive/VoucherLifeCycle
- ewd687a/EWD687a
- ewd998/EWD998PCal and EWD998 (TerminationDetection lifted to
Spec => []...)
- transaction_commit (TCommit, TwoPhase, PaxosCommit)
- CoffeeCan, DieHard, MissionariesAndCannibals, SpanTree
(TypeInvariant / TypeOK)
- spanning (SntMsg) and glowingRaccoon clean+stages (TypeOK +
primerPositive + preservationInvariant)
- ReadersWriters (TypeOK + Safety: mutex + at-most-one-writer)
- CigaretteSmokers (TypeOK + AtMostOne)
- LamportMutex (BoundedNetwork, via NetworkInv pigeonhole)
- TeachingConcurrency/Simple and SimpleRegular (TypeOK and Inv
exposed as named theorems matching the .cfg invariants)
Proof-only assumptions added in `*_proof.tla` (not in the spec):
- CigaretteSmokers_proof: IngredientsFinite (Cardinality is
already used inside the spec's own ASSUME, so finiteness is
implicit).
- ReadersWriters_proof: NumActorsIsNat (NumActors \in Nat).
- Elevator_proof: ElevatorFloorDisjoint (Floor \cap Elevator = {};
a TLC modelling convention not stated in the spec).
- SchedulingAllocator_proof, AllocatorImplementation_proof:
ClientsFinite (the spec only assumes Resources finite).
- EWD687a_proof: ProcsFinite (finite process set).
- glowingRaccoon clean_proof and stages_proof: ConstantsAreNat
(DNA, PRIMER \in Nat; without this Spec => []TypeOK is false).
Spec ASSUMEs restated under a name in the proof file (no new fact):
- CigaretteSmokers_proof: OffersAssumption.
- spanning_proof: NoPrntFact.
- SpanTree_proof: ConstantsAssumption.
- CoffeeCan_proof: MaxBeanFact.
Non-trivial proof obligations discharged:
- PaxosCommit_proof: MaximumProp -- the recursive `Maximum` operator
is shown to return the largest element of its (non-empty, finite,
integer >= -1) input via well-founded induction on the strict-subset
ordering, going through a hand-proved recursion equation for the
inner CHOOSE'd recursive function.
- SchedulingAllocator_proof: PermSeqsType -- analogous well-founded
structural induction over `PermSeqs(S)`, plus an explicit
finiteness assumption on `Clients` (added in the proof file only).
- AllocatorImplementation_proof: PermSeqsType -- the same proof
threaded through the `Sched!` instance. One sub-step
(`Sched!PermSeqs(S) = PermsFn(S)[S]`) remains OMITTED because
tlapm's INSTANCE expansion currently mangles the inner LET binding
inside the LET-bound recursive function.
- EWD687a_proof: TreeNodesNonNeutral, TreeStructure, TreeIsTree,
Inv2GivesTreeBody, SpecGivesAlwaysTreeBody -- the structural half
of TreeWithRoot (graph + non-neutral conjuncts) discharged from the
existing Inv1 / Inv2 / NoCycle invariants.
- CRDT_proof: the four previously OMITTED Sum lemmas (SumType,
SumIsZero, SumWeaklyMonotonic, SumStronglyMonotonic) are reduced
to SumFunctionNat, SumFunctionZero, SumFunctionMonotonic, and
SumFunctionStrictlyMonotonic in the community-modules
FunctionTheorems (strengthened and CI-verified in
tlaplus/CommunityModules#124) via the
trivial unfolding Sum(f) = SumFunction(f); FiniteSetTheorems is
dropped from EXTENDS accordingly. The downstream Measure*/Gossip*
lemmas and the OGLiveness / Convergence theorems that already cited
these now check end-to-end (280 obligations).
Remaining OMITTED obligations:
- Elevator_proof: Inv2Next (the inductive step for the strengthened
Inv2; each of its ~10 conjuncts is proven preserved per-action
individually, only the full assembly is left), and four narrow
function-evaluation lemmas (GetDirectionEval, GetDistanceEval,
CanServiceCallEval, PeopleWaitingEval) that unfold a multi-arg
`f[a, b]` definition -- a known tlapm/SMT/Zenon/Isabelle gap,
cf. https://discuss.tlapl.us/msg01519.html.
- EWD687a_proof: AreConnectedToLeader (constructing the path to
Leader by iterating upEdge needs SimplePath/Cardinality
reasoning), Thm_TreeWithRoot's QED (bridges TreeWithRoot's
`LET ... IN [](...)` shape and the equivalent
`[](LET ... IN ...)` that PTL would consume), and Thm_DT2
(Spec => DT2; needs an inductive invariant over
msgs/rcvdUnacked/acks/sentUnacked).
- AllocatorImplementation_proof: PermSeqsIsPermsFn, the equality
`Sched!PermSeqs(S) = PermsFn(S)[S]`, blocked by tlapm rendering
the INSTANCE-expanded inner LET binding as a self-recursive
CHOOSE.
- EWD998PCal_proof: Refinement (Spec => EWD998Spec); per-disjunct
step-simulation requires bag-level lemmas plus the EWD998-level
invariant `B = Sum(counter, Node)` for the token-pass disjunct.
Also, the unique-token preservation conjunct of NetworkOK is
deferred in PCalTypeOKInductive.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to tlaplus/Examples
that referenced
this pull request
May 13, 2026
Each affected directory now has a `<Spec>_proof.tla` module that
mechanically checks the safety obligations of its TLA+ specification
(typically Spec => []TypeInvariant, plus any SafetyInvariant or
strengthened inductive invariant the spec defines). The original
specifications themselves are not modified by this commit; the prior
commit names a few previously-anonymous `ASSUME` blocks that the
proofs cite by reference.
Specifications covered:
- KeyValueStore
- MultiCarElevator/Elevator
- PaxosHowToWinATuringAward/Voting
- SpecifyingSystems chapters: AsynchronousInterface, FIFO,
HourClock, Composing, Liveness, RealTime, CachingMemory, TLC
- TwoPhase
- allocator (Simple, Scheduling, Implementation)
- byihive/VoucherLifeCycle
- ewd687a/EWD687a
- ewd998/EWD998PCal and EWD998 (TerminationDetection lifted to
Spec => []...)
- transaction_commit (TCommit, TwoPhase, PaxosCommit)
- CoffeeCan, DieHard, MissionariesAndCannibals, SpanTree
(TypeInvariant / TypeOK)
- spanning (SntMsg) and glowingRaccoon clean+stages (TypeOK +
primerPositive + preservationInvariant)
- ReadersWriters (TypeOK + Safety: mutex + at-most-one-writer)
- CigaretteSmokers (TypeOK + AtMostOne)
- LamportMutex (BoundedNetwork, via NetworkInv pigeonhole)
- TeachingConcurrency/Simple and SimpleRegular (TypeOK and Inv
exposed as named theorems matching the .cfg invariants)
Proof-only assumptions added in `*_proof.tla` (not in the spec):
- CigaretteSmokers_proof: IngredientsFinite (Cardinality is
already used inside the spec's own ASSUME, so finiteness is
implicit).
- ReadersWriters_proof: NumActorsIsNat (NumActors \in Nat).
- Elevator_proof: ElevatorFloorDisjoint (Floor \cap Elevator = {};
a TLC modelling convention not stated in the spec).
- SchedulingAllocator_proof, AllocatorImplementation_proof:
ClientsFinite (the spec only assumes Resources finite).
- EWD687a_proof: ProcsFinite (finite process set).
- glowingRaccoon clean_proof and stages_proof: ConstantsAreNat
(DNA, PRIMER \in Nat; without this Spec => []TypeOK is false).
Spec ASSUMEs restated under a name in the proof file (no new fact):
- CigaretteSmokers_proof: OffersAssumption.
- spanning_proof: NoPrntFact.
- SpanTree_proof: ConstantsAssumption.
- CoffeeCan_proof: MaxBeanFact.
Non-trivial proof obligations discharged:
- PaxosCommit_proof: MaximumProp -- the recursive `Maximum` operator
is shown to return the largest element of its (non-empty, finite,
integer >= -1) input via well-founded induction on the strict-subset
ordering, going through a hand-proved recursion equation for the
inner CHOOSE'd recursive function.
- SchedulingAllocator_proof: PermSeqsType -- analogous well-founded
structural induction over `PermSeqs(S)`, plus an explicit
finiteness assumption on `Clients` (added in the proof file only).
- AllocatorImplementation_proof: PermSeqsType -- the same proof
threaded through the `Sched!` instance. One sub-step
(`Sched!PermSeqs(S) = PermsFn(S)[S]`) remains OMITTED because
tlapm's INSTANCE expansion currently mangles the inner LET binding
inside the LET-bound recursive function.
- EWD687a_proof: TreeNodesNonNeutral, TreeStructure, TreeIsTree,
Inv2GivesTreeBody, SpecGivesAlwaysTreeBody -- the structural half
of TreeWithRoot (graph + non-neutral conjuncts) discharged from the
existing Inv1 / Inv2 / NoCycle invariants.
- CRDT_proof: the four previously OMITTED Sum lemmas (SumType,
SumIsZero, SumWeaklyMonotonic, SumStronglyMonotonic) are reduced
to SumFunctionNat, SumFunctionZero, SumFunctionMonotonic, and
SumFunctionStrictlyMonotonic in the community-modules
FunctionTheorems (strengthened and CI-verified in
tlaplus/CommunityModules#124) via the
trivial unfolding Sum(f) = SumFunction(f); FiniteSetTheorems is
dropped from EXTENDS accordingly. The downstream Measure*/Gossip*
lemmas and the OGLiveness / Convergence theorems that already cited
these now check end-to-end (280 obligations).
Remaining OMITTED obligations:
- Elevator_proof: Inv2Next (the inductive step for the strengthened
Inv2; each of its ~10 conjuncts is proven preserved per-action
individually, only the full assembly is left), and four narrow
function-evaluation lemmas (GetDirectionEval, GetDistanceEval,
CanServiceCallEval, PeopleWaitingEval) that unfold a multi-arg
`f[a, b]` definition -- a known tlapm/SMT/Zenon/Isabelle gap,
cf. https://discuss.tlapl.us/msg01519.html.
- EWD687a_proof: AreConnectedToLeader (constructing the path to
Leader by iterating upEdge needs SimplePath/Cardinality
reasoning), Thm_TreeWithRoot's QED (bridges TreeWithRoot's
`LET ... IN [](...)` shape and the equivalent
`[](LET ... IN ...)` that PTL would consume), and Thm_DT2
(Spec => DT2; needs an inductive invariant over
msgs/rcvdUnacked/acks/sentUnacked).
- AllocatorImplementation_proof: PermSeqsIsPermsFn, the equality
`Sched!PermSeqs(S) = PermsFn(S)[S]`, blocked by tlapm rendering
the INSTANCE-expanded inner LET binding as a self-recursive
CHOOSE.
- EWD998PCal_proof: Refinement (Spec => EWD998Spec); per-disjunct
step-simulation requires bag-level lemmas plus the EWD998-level
invariant `B = Sum(counter, Node)` for the token-pass disjunct.
Also, the unique-token preservation conjunct of NetworkOK is
deferred in PCalTypeOKInductive.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds two new theorems to
FunctionTheoremsfor summing a constant function over a finite set:SumFunctionOnSetConst— for any finiteSand constantk,FoldFunctionOnSet(+, 0, [x \in S |-> k], S) = k * Cardinality(S).SumFunctionConst— the same fact stated forFoldFunctionon a function whose domain is finite.Both come with full TLAPS proofs in
FunctionTheorems_proofsand a short example in the doc comments.Supporting changes
To make sure these (and the other
*_proofs.tlamodules) stay valid as the library evolves, this PR also:tlapsGitHub Actions job tomain.ymlandpr.ymlthat downloads the TLAPS 1.6.0-pre release fromtlaplus/tlapmand runstlapmon everymodules/*_proofs.tlafile. The job runs as a matrix onubuntu-latest(x86_64-linux-gnu) andmacos-latest(arm64-darwin) and checks all proof files even when one fails, so a single regression doesn't mask others.Fun_NatBijSingleton(singleton case) inFunctionTheorems_proofsno longer asks the SMT pipeline to unfoldBijection/Surjectionand invent the existential witness in one step; it extracts typing/surjection facts, derivesf[1] \in S, proves uniqueness viaPICKon1..1, andWITNESSesf[1].MaxInterval/MinIntervalinFiniteSetsExtTheorems_proofsno longer rely on a backend reasoning about the rawCHOOSEfromMax/Minwhile doing arithmetic ona..b; they go through the existingMaxInt/MinIntintroduction rules with the trivial side conditions supplied explicitly.All 795 obligations of
FunctionTheorems_proofsand 419 obligations ofFiniteSetsExtTheorems_proofscontinue to check locally withtlapm --cleanfp.[Feature][Proofs][CI]