[lemmy]

A term that tlapm does not translate (ENABLED, a temporal formula) is abstracted as a nullary constant, dropping the variables it depends on. Each test is a false theorem that tlapm currently proves (by SMT, Zenon, or Isabelle).

---

When tlapm sends an obligation to a back-end, coalesce_modal_visitor in src/frontend/coalesce.ml replaces each subterm built from ENABLED, <>,
[], \cdot, Prime, or UNCHANGED by an opaque operator, because the back-ends cannot reason about these operators. The opaque operator must be applied to the free constants and free variables of the subterm, so that the abstraction still depends on everything the subterm depends on.

To find them, coalesce_modal_visitor calls vars_visitor#compute. compute starts a traversal of the subterm with the method expr. Whenever expr meets a constant or variable that is not bound inside the subterm, it adds it to the instance variable vars of vars_visitor. When the traversal ends, compute should return that set.

Instead, compute began with let vars = ref IxSet.empty in. That created a second, local vars with the same name, which expr never added to, and compute returned it. So:

• The traversal collected the right constants and variables, into the instance variable.
• compute never read that variable. It returned the empty local set, so every abstraction got no arguments.
• The instance variable was never reset either, so it kept growing across calls. Nothing read it, so that did no harm.

As a result, a subterm under a binder, such as <>(x = t) in \E t : <>(x = t), became a constant h that does not depend on t. A back-end could then treat <>(x = t) as the same formula for every t and prove false theorems.

---

#309

[lemmy]

❯ git log -n1
commit 07bc9dbf930e10d62ace069914e3c1bb7a74c25c (HEAD -> main, origin/main, origin/HEAD)
Author: Markus Alexander Kuppe <github.com@lemmster.de>
Date:   Mon Nov 9 14:39:56 2026 -0800

    Add soundness tests.

    Each test is a false theorem that tlapm currently proves.

    Related:
    * Some tests were found by agentic bug finding
    * https://github.com/tlaplus/tlapm/issues/309
    * https://github.com/tlaplus/tlapm/issues/310

    [Tests]

    Co-Authored-By: Scott Cochran <5066685+scottcochran@users.noreply.github.com>
    Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
    Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com>
    Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

 ~/.opam/5.5.2/bin/tlapm --version
07bc9db

❯ dune exec --no-build -- tlapm --strict --cleanfp --nofp test/soundness_tests/BinderUnsound.tla
(* fingerprints file ".tlacache/BinderUnsound.tlaps/fingerprints" removed *)
Zenon error: exhausted search space without finding a proof
(* created new ".tlacache/BinderUnsound.tlaps/BinderUnsound.thy" *)
(* fingerprints written in ".tlacache/BinderUnsound.tlaps/fingerprints" *)
File "./test/soundness_tests/BinderUnsound.tla", line 35, characters 1-7:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x
           PROVE  (\E t \in S : x = t) => (\A t \in S : x = t)
File "./test/soundness_tests/BinderUnsound.tla", line 1, character 1 to line 36, character 77:
[ERROR]: 1/9 obligations failed.
There were backend errors processing module `"BinderUnsound"`.

❯ git log -n1
commit 7eeb85651c3ed248f60f57c3b8642eebb36de2c5 (HEAD, origin/mku-gh309)
Author: Markus Alexander Kuppe <github.com@lemmster.de>
Date:   Mon Nov 9 16:10:37 2026 -0800

    Report unsupported operator values during type synthesis

    Catch Invalid_type_downcast when an operator reference appears where
    an ordinary expression is expected. Report "Operator-valued expression
    is not supported here" through the normal error path, replacing the
    generic unexpected SMT backend exception and backtrace.

    Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com>
    Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

~/src/TLA/tlapm remotes/origin/mku-gh309*
❯ ~/.opam/5.5.2/bin/tlapm --version
7eeb856

❯ dune exec --no-build -- tlapm --strict --cleanfp --nofp test/soundness_tests/BinderUnsound.tla
(* fingerprints file ".tlacache/BinderUnsound.tlaps/fingerprints" removed *)
Zenon error: exhausted search space without finding a proof
Zenon error: exhausted search space without finding a proof
Zenon error: exhausted search space without finding a proof
Zenon error: exhausted search space without finding a proof
(* created new ".tlacache/BinderUnsound.tlaps/BinderUnsound.thy" *)
(* fingerprints written in ".tlacache/BinderUnsound.tlaps/fingerprints" *)
File "./test/soundness_tests/BinderUnsound.tla", line 35, characters 1-7:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x
           PROVE  (\E t \in S : x = t) => (\A t \in S : x = t)
File "./test/soundness_tests/BinderUnsound.tla", line 30, characters 1-2:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x,
                  BadEventuallyProp ==
                    (\E t \in S : <>(x = t)) => (\A t \in S : <>(x = t))
           PROVE  Spec => BadEventuallyProp
File "./test/soundness_tests/BinderUnsound.tla", line 23, characters 42-43:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x,
                  BadEnabled ==
                    (\E t \in S : ENABLED A(t))
                    => (\A t \in S : ENABLED A(t)),
                  Isa
           PROVE  BadEnabled
File "./test/soundness_tests/BinderUnsound.tla", line 22, characters 42-43:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x,
                  BadEnabled ==
                    (\E t \in S : ENABLED A(t))
                    => (\A t \in S : ENABLED A(t)),
                  Zenon
           PROVE  BadEnabled
File "./test/soundness_tests/BinderUnsound.tla", line 21, characters 42-43:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x,
                  BadEnabled ==
                    (\E t \in S : ENABLED A(t))
                    => (\A t \in S : ENABLED A(t)),
                  SMT
           PROVE  BadEnabled
File "./test/soundness_tests/BinderUnsound.tla", line 20, characters 42-43:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT S,
                  NEW VARIABLE x,
                  BadEnabled ==
                    (\E t \in S : ENABLED A(t))
                    => (\A t \in S : ENABLED A(t))
           PROVE  BadEnabled
File "./test/soundness_tests/BinderUnsound.tla", line 1, character 1 to line 36, character 77:
[ERROR]: 6/9 obligations failed.
There were backend errors processing module `"BinderUnsound"`.