Wrong function sets counterexample? about apalache HOT 6 CLOSED

Debug log: So far, I've discovered that

UNION { [d -> r] : d \in {{0}} }

finds a "counterexample",

Funs(part_dom, r) == UNION { [{0} -> r] }

triggers the rewriter error, but

Funs(part_dom, r) == [{0} -> r]

does not, even though they are all semantically equivalent. This is definitely some sort of bug. Investigating further.

from apalache.

Found the following (potentially related) issue:
When trying to evaluate

Inv == [{0} -> {1}] = UNION { [d -> {1}] : d \in {{0}} }

Apalache reports

...
PASS #13: BoundedChecker                                          I@16:12:47.639
State 0: Checking 1 state invariants                              I@16:12:48.574
<unknown>: checker error: Unexpected equality test over types FinFunSet[CellTFrom(Set(Int)), CellTFrom(Set(Int))] and CellTFrom(Set((Int -> Int))) E@16:12:48.608
at.forsyte.apalache.infra.AdaptedException: <unknown>: checker error: Unexpected equality test over types FinFunSet[CellTFrom(Set(Int)), CellTFrom(Set(Int))] and CellTFrom(Set((Int -> Int)))
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
        ...

See #1946, #1808, #1801

from apalache.

Rewriting the above as X = Y \iff \A x \in X: x \in Y /\ \A x \in Y: x \in X, we see that Apalache finds a violation of

Inv ==
    LET X == [{0} -> {1}]
        Y == UNION { [d -> {1}] : d \in {{0}} }
    IN 
        /\ \A f \in X: f \in Y
        /\ \A f \in Y: f \in X

Which is 100% inceorrect

from apalache.

Interestingly, Apalache agrees that Y \subseteq X, but not X \subseteq Y. Hypothesis: \A f \in Y is treated as the empty forall.

from apalache.

Got it down to a minimal problematic input:

---- MODULE test ----
EXTENDS Integers, Apalache

Inv == [x \in {0} |-> 1] \in UNION { [d -> {1}] : d \in {{0}} }
Init == TRUE
Next == TRUE
====

The fundamental issue, is that { [d -> {1}] : d \in {{0}} } creates symbolic function sets (Which Apalache does not handle, unless they're being selected from, or quantified over). These sets' contents are unconstrained cells.

Inv ==  \A S \in { [d -> {1}] : d \in {{0}} }: \A f \in S: f[0] = 1

does not trigger the incorrect violation, so it's likely that UNION is a key contributor to this bug.

from apalache.

Note that #2778 closes this issue, but the original input should still fail with an error instead of producing bogus CEs.

from apalache.