Wrong function sets counterexample?

[Kukovec]

Reported on Zulip by user "oggy":

Hi folks, I'm getting a very weird looking counterexample from Apalache. Given:

---- MODULE Apalache_Cex ----
EXTENDS Integers, Apalache

LIMIT == 3
DOM == 0..LIMIT
RAN == 0..LIMIT
VARIABLE
    \* @type: Int -> Int;
    f

Funs(part_dom, r) == UNION { [d -> r] : d \in SUBSET(part_dom) }

TypeInv ==
    f \in Funs(DOM, RAN)

Init ==
    f = SetAsFun({<<0, 1>>})

Next ==
    f' \in Funs(DOM, RAN)

====

Running

apalache-mc check --init=Init --inv=TypeInv --length=0 --no-deadlock Apalache_Cex.tla

Then yields the counterexample:

---------------------------- MODULE counterexample ----------------------------

EXTENDS Apalache_Cex

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 == f = SetAsFun({<<0, 1>>})

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation ==
  ~(f \in UNION ({ [d$3 -> (0 .. 3)]: d$3 \in Expand(SUBSET (0 .. 3)) }))

================================================================================
(* Created by Apalache on Wed Nov 01 15:29:14 CET 2023 *)
(* https://github.com/informalsystems/apalache *)

But that looks wrong? At least, TLC is happy to confirm that SetAsFun({<<0, 1>>}) \in Funs(DOM, RAN)

Is it a bug or am I doing something wrong? Is there a workaround?

Also, this variation:

---- MODULE Apalache_Cex ----
EXTENDS Integers, Apalache

LIMIT == 3
DOM == 0..LIMIT
RAN == 0..LIMIT
VARIABLE
    \* @type: Int -> Int;
    f

\* @type: (a -> b, Set(a)) => (a -> b);
Restrict(fun, S) == [ x \in DOMAIN fun \cap S |-> fun[x] ]
Funs(S, T) == { Restrict(g, S): g \in [S -> T], S2 \in SUBSET S}

TypeInv ==
    f \in Funs(DOM, RAN)

Init ==
    f = SetAsFun({<<0, 1>>})

Is_Cex == SetAsFun({<<0, 1>>}) \in UNION ({ [d -> (0 .. 3)]: d \in Expand(SUBSET (0 .. 3)) })

Next ==
    f' \in Funs(DOM, RAN)

====

Fails with:

Apalache_Cex.tla:13:39-13:46: rewriter error: Trying to expand a set of functions. This will blow up the solver. E@17:27:36.916
at.forsyte.apalache.infra.AdaptedException: Apalache_Cex.tla:13:39-13:46: rewriter error: Trying to expand a set of functions. This will blow up the solver.
        at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
        at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:129)
        at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
        at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: Apalache_Cex.tla:13:39-13:46: rewriter error: Trying to expand a set of functions. This will blow up the solver.
A bug report template has been generated at...

[Kukovec]

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.

[Kukovec]

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

[Kukovec]

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

[Kukovec]

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

[Kukovec]

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.

[Kukovec]

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