Skip to content

Do not distribute instantiation over WF and SF. - #321

Merged
lemmy merged 1 commit into
mainfrom
mku-gh69
Oct 30, 2026
Merged

Do not distribute instantiation over WF and SF.#321
lemmy merged 1 commit into
mainfrom
mku-gh69

Conversation

@lemmy

@lemmy lemmy commented Oct 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Instantiation does not distribute over ENABLED, and hence not over WF and SF (Specifying Systems, Section 17.8). tlapm substituted into WF and SF directly. With x <- z, y <- z it proved
XY!Fair <=> WF_(XY!vars)(XY!Next), which is false, and from it Spec => XY!Spec. tlapm now expands WF and SF to their definitions in terms of ENABLED, as Section 8.9.4 suggests. Its handling of ENABLED under INSTANCE then binds the primed variables before the substitution.

issue69_instantiated_fairness_stest is no longer known. issue69_instantiated_strong_fairness_stest covers SF. Fairness_INSTANCE_test checks that tlapm still proves the correct unfolding of instantiated WF and SF. TLC confirms its lemmas and theorems on a finite model.

Fixes Github issue #69
#69

[Bug][Tests]

@lemmy lemmy self-assigned this Oct 29, 2026
@lemmy lemmy added bug An error, usually in the code. soundness Issues and PRs related to getting TLAPM to prove FALSE labels Oct 29, 2026
@lemmy
lemmy requested a review from muenchnerkindl October 29, 2026 02:25
@lemmy @muenchnerkindl @claude
Do not distribute instantiation over WF and SF.
56f0d68 
Instantiation does not distribute over ENABLED, and hence not over WF
and SF (Specifying Systems, Section 17.8). tlapm substituted into WF and
SF directly. With x <- z, y <- z it proved
XY!Fair <=> WF_(XY!vars)(XY!Next), which is false, and from it
Spec => XY!Spec. tlapm now expands WF and SF to their definitions in
terms of ENABLED, as Section 8.9.4 suggests. Its handling of ENABLED
under INSTANCE then binds the primed variables before the substitution.

issue69_instantiated_fairness_stest is no longer known.
issue69_instantiated_strong_fairness_stest covers SF.
Fairness_INSTANCE_test checks that tlapm still proves the correct
unfolding of instantiated WF and SF. TLC confirms its lemmas and
theorems on a finite model.

Fixes Github issue #69
#69

[Bug][Tests]

Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com>
Co-authored-by: Gemini 4 Argon <noreply@google.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
@lemmy lemmy mentioned this pull request Oct 29, 2026
Merged
@lemmy
lemmy removed the request for review from muenchnerkindl October 29, 2026 04:09
@lemmy
lemmy marked this pull request as draft October 29, 2026 04:09
@lemmy

lemmy commented Oct 29, 2026

Copy link
Copy Markdown
Member Author

CI failure: EWD840_proof.tla (tlaplus/Examples), 3 of 225 obligations fail.

  1. Lines 109 and 309: an older bug that this PR exposes. ExpandENABLED fails with Operator "EnabledWrapper" not found when a hidden definition from an INSTANCE in an EXTENDSed module contains ENABLED. Since this PR, every instantiated WF/SF contains ENABLED. Fix: have Expr.Anon leave EnabledWrapper/CdotWrapper in place, and add a regression test.
  2. Line 313: expected. The proof relies on WF_TD!vars(TD!DetectTermination) matching the fairness conjunct of TD!Spec, which is exactly the TLAPM identifies instantiated fairness condition with fairness of instantiated action #69 unsoundness. The example in tlaplus/Examples needs to change, for example by stating <1>3 in terms of a new TD!EnabledDT == ENABLED <<DetectTermination>>_vars. With fix 1, that version proves the theorem.

lemmy added a commit that referenced this pull request Oct 29, 2026
@lemmy @claude
Add a known soundness test for instantiated -+->.
941f894 
Instantiation does not distribute over -+->, but tlapm substitutes into
its arguments. issue320_instantiated_actplus_stest is the issue's
reproducer. The test is marked known.

Related to Github issue #320
#320

Related to Github issue #69
#69

Related to Github pull request #321
#321

[Tests]

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
@lemmy lemmy mentioned this pull request Oct 29, 2026
Merged
@muenchnerkindl

muenchnerkindl commented Oct 30, 2026

Copy link
Copy Markdown
Contributor

LGTM, thanks!

lemmy added a commit to tlaplus/Examples that referenced this pull request Oct 30, 2026
@lemmy @claude
EWD840: extend TLAPS to work around a tlapm bug.
a3f882d 
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it
instantiates a module. If the module with the INSTANCE does not extend
TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found".
With tlapm#321, every instantiated WF contains ENABLED, so EWD840_proof
hits this bug through TD == INSTANCE SyncTerminationDetection.

tlaplus/tlapm#250
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @claude
EWD840_proof: do not rely on instantiation distributing over WF.
120998f 
Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. SyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
SyncTerminationDetection_proof!Fairness, as suggested by Stephan Merz.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @claude
EWD840: extend TLAPS to work around a tlapm bug.
ab4979e 
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it
instantiates a module. If the module with the INSTANCE does not extend
TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found".
With tlapm#321, every instantiated WF contains ENABLED, so EWD840_proof
hits this bug through TD == INSTANCE SyncTerminationDetection.

tlaplus/tlapm#250
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @claude
EWD840_proof: do not rely on instantiation distributing over WF.
48ea628 
Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. SyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
SyncTerminationDetection_proof!Fairness, as suggested by Stephan Merz.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @muenchnerkindl @claude
EWD840_proof: do not rely on instantiation distributing over WF.
affe258 
Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. SyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
SyncTerminationDetection_proof!Fairness.

Apalache accepts only fairness written out in Spec, so
APSyncTerminationDetection.cfg now names Init and Next instead.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com>
Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @claude
EWD998: extend TLAPS to work around a tlapm bug.
61973f6 
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it
instantiates a module. If the module with the INSTANCE does not extend
TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found".
With tlapm#321, every instantiated WF contains ENABLED, so EWD998_proof
hits this bug through TD == INSTANCE AsyncTerminationDetection.

tlaplus/tlapm#250
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @muenchnerkindl @claude
EWD998_proof: do not rely on instantiation distributing over WF.
8e320b3 
Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. AsyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
AsyncTerminationDetection_proof!Fairness.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com>
Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @claude
EWD840: extend TLAPS to work around a tlapm bug.
2eef3e8 
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it
instantiates a module. If the module with the INSTANCE does not extend
TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found".
With tlapm#321, every instantiated WF contains ENABLED, so EWD840_proof
hits this bug through TD == INSTANCE SyncTerminationDetection.

tlaplus/tlapm#250
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @muenchnerkindl @claude
EWD840_proof: do not rely on instantiation distributing over WF.
b08bbe3 
Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. SyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
SyncTerminationDetection_proof!Fairness.

Apalache accepts only fairness written out in Spec, so
APSyncTerminationDetection.cfg now names Init and Next instead.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com>
Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @claude
EWD998: extend TLAPS to work around a tlapm bug.
9c65f31 
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it
instantiates a module. If the module with the INSTANCE does not extend
TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found".
With tlapm#321, every instantiated WF contains ENABLED, so EWD998_proof
hits this bug through TD == INSTANCE AsyncTerminationDetection.

tlaplus/tlapm#250
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <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 Oct 30, 2026
@lemmy @muenchnerkindl @claude
EWD998_proof: do not rely on instantiation distributing over WF.
0e32a03 
Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. AsyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
AsyncTerminationDetection_proof!Fairness.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
@lemmy
lemmy marked this pull request as ready for review October 30, 2026 18:34
@lemmy
lemmy merged commit 4744c0f into main Oct 30, 2026
5 of 9 checks passed
@lemmy
lemmy deleted the mku-gh69 branch October 30, 2026 19:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@lemmy lemmy

Labels

bug An error, usually in the code. soundness Issues and PRs related to getting TLAPM to prove FALSE

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@lemmy @muenchnerkindl