Soundness: a term under a binder that tlapm does not translate is abstracted as a nullary constant, so false theorems prove

Summary

When tlapm hands a backend a term it does not translate (an ENABLED that has not been expanded, a temporal
formula such as <>(x = t), presumably \cdot too), it abstracts the term as a nullary opaque constant. The
constant does not depend on the variable bound around the term, so \E t \in S : F(t) and \A t \in S : F(t)
become the same proposition and

(\E t \in S : ENABLED A(t)) => (\A t \in S : ENABLED A(t))

proves by OBVIOUS, BY SMT, BY Zenon and BY Isa. The same shape with <>(x = t) in place of ENABLED A(t)
proves under Spec. Both are false, and TLC refutes both at S = {1, 2}. The control, the same quantifier shape
over a term tlapm does translate (x = t), correctly fails on all three backends, so the problem is specifically
the abstraction step. LS4 (PTL) is not affected: it receives atoms for state predicates, not for these terms.

Module

---------------------------- MODULE BinderUnsound ----------------------------
(* Minimal reproduction: tlapm abstracts a term it does not translate (an    *)
(* unexpanded ENABLED, or a temporal formula) as a nullary constant, so the  *)
(* variable bound around it is dropped and a false theorem proves.           *)
EXTENDS Naturals, TLAPS

CONSTANT S
VARIABLE x

Init == x \in S
A(t) == x = t /\ x' = t + 1
Next == \E t \in S : A(t)
Spec == Init /\ [][Next]_x

(* State predicate. With S = {1, 2} and x = 1: ENABLED A(1) holds and        *)
(* ENABLED A(2) does not, so this is FALSE. TLC refutes it in the initial    *)
(* state. tlapm proves it.                                                   *)
BadEnabled == (\E t \in S : ENABLED A(t)) => (\A t \in S : ENABLED A(t))

THEOREM BadEnabled_OBVIOUS == BadEnabled BY DEF BadEnabled
THEOREM BadEnabled_SMT     == BadEnabled BY SMT DEF BadEnabled
THEOREM BadEnabled_Zenon   == BadEnabled BY Zenon DEF BadEnabled
THEOREM BadEnabled_Isa     == BadEnabled BY Isa DEF BadEnabled

(* Same shape with a temporal body instead of ENABLED. Under Spec with       *)
(* S = {1, 2} and x = 2 initially, <>(x = 2) holds and <>(x = 1) does not.   *)
BadEventuallyProp == (\E t \in S : <>(x = t)) => (\A t \in S : <>(x = t))

THEOREM BadEventually == Spec => BadEventuallyProp
BY DEF BadEventuallyProp

(* Control: the same quantifier shape over a term tlapm does translate.      *)
(* This is equally false and must NOT prove. It does not.                    *)
THEOREM Control == (\E t \in S : x = t) => (\A t \in S : x = t)
OBVIOUS
=============================================================================

TLC configs: SPECIFICATION Spec, CONSTANT S = {1, 2}, with INVARIANT BadEnabled and separately
PROPERTY BadEventuallyProp (plus CHECK_DEADLOCK FALSE).

Result

  line 20  proved   smt        BadEnabled_OBVIOUS
  line 21  proved   smt        BadEnabled_SMT
  line 22  proved   zenon      BadEnabled_Zenon
  line 23  proved   isabelle   BadEnabled_Isa
  line 30  proved   smt        BadEventually        (Spec => BadEventuallyProp)
  line 35  failed   smt, zenon, isabelle   Control  (correct)

TLC:

Error: Invariant BadEnabled is violated by the initial state:
x = 1

Error: Temporal properties were violated.
State 1: <Initial predicate>  x = 1
State 2: Stuttering

Mechanism

The SMT query tlapm writes for BadEnabled_SMT (901ae51; 7824dab's is identical apart from comments). The
abstraction of ENABLED A(t) is declared with no arguments:

(declare-fun smt__TLA____Anon__OPAQUE__h32f0e () Idv)

and the same constant stands under both the exists and the forall:

;; Goal
(assert
  (!
    (not
      (=>
        (exists ((smt__CONSTANT__t__ Idv))
          (and (smt__TLA____Mem smt__CONSTANT__t__ smt__CONSTANT__S__)
            (= smt__TLA____Anon__OPAQUE__h32f0e smt__TLA____Tt__Idv)))
        (forall ((smt__CONSTANT__t__ Idv))
          (=> (smt__TLA____Mem smt__CONSTANT__t__ smt__CONSTANT__S__)
            (= smt__TLA____Anon__OPAQUE__h32f0e smt__TLA____Tt__Idv)))))
    :named |Goal|))

(check-sat)
(exit)

So the solver is asked whether (\E t \in S : c) => (\A t \in S : c) holds for a constant c, which it does,
and cvc5's proof of that is a valid proof of the wrong obligation. The sound abstraction is a function of the bound
variables, (declare-fun h32f0e (Idv) Idv) applied to t, which is what coalescing is meant to produce.

The shapes a real proof is likely to write are the dangerous ones: citing a lemma proved for one instance to discharge
the general statement (ASSUME NEW t \in {"a"} PROVE F(t) cited for F(t) over all t), or deriving []InvBig
from []InvSmall when both bodies begin with \A, since tlapm moves a leading \A out of a [] body before it
abstracts. Each step starts from a true, soundly proved fact and reaches a false one through a single SMT step.

Environment

arm64-darwin, backends as bundled in the asset (Z3 4.8.9, Zenon 0.8.4, Isabelle2025, LS4). Both builds behave
identically on everything below. Not tested on Linux.

Full reproduction, run script, TLC configs and the backend inputs tlapm wrote (--debug tempfiles) for both builds:
https://github.com/scottcochran/TLAPS-issues

Related

• Coalescing has issues with abstracting bound variables #197 reports the same abstraction failing to prove true theorems. This is the soundness side of that defect: the
  abstraction drops the bound variable, so it both blocks valid proofs and admits invalid ones. The hidden-operator
  workaround given there is also the mitigation for this.
• ENABLED is not coalesced #75 is the same mechanism for ENABLED, reported as a gap in what proves.
• TLAPM identifies instantiated fairness condition with fairness of instantiated action #69 is a different soundness defect in ENABLED/fairness handling; a fix to the ENABLED translation touches both.