Merge pull request #2813 from informalsystems/ro/fix_function_inclusion

Add support for infinite sets in set inclusion for the (fun)arrays encoding

.unreleased/bug-fixes/fixSetInclusionwithArrays.md

@@ -0,0 +1 @@
+fix crash on the arrays encoding when having a subset relation containing infinite sets, see #2810

test/tla/FunInInfiniteSubset.tla

@@ -0,0 +1,22 @@
+--------------- MODULE FunInInfiniteSubset -----------------
+
+EXTENDS Integers
+
+P == {"P1_OF_P"}
+
+VARIABLE
+    \* @type: P -> Set(Int);
+    myVariable
+
+Init ==
+    myVariable = [p \in P |-> {0}]
+
+Step(p) ==
+    myVariable' = [q \in P |-> {0}]
+
+Next == \E p \in P : Step(p)
+
+TypeOkay == myVariable \in [P -> SUBSET Int]
+TypeOkay_ == TypeOkay
+
+=============================================

test/tla/cli-integration-tests.md

@@ -2812,6 +2812,18 @@ $ apalache-mc check --inv=Sanity FunExcept3.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### check FunInInfiniteSubset (array-encoding)
+
+A regression test for function membership in the presence of infinite sets.
+
+See https://github.com/informalsystems/apalache/issues/2810
+
+```sh
+$ apalache-mc check --init=TypeOkay_ --inv=TypeOkay --length=1 FunInInfiniteSubset.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
 ### check ERC20.tla
 
 ```sh

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala

@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt.implicitConversions.Crossable
 import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt
-import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT, UnknownT}
+import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, InfSetT, PowSetT, UnknownT}
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, RewritingRule, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, RecT1, SetT1, TlaEx, TupT1}
 import at.forsyte.apalache.tla.lir.convenience._
@@ -35,6 +35,9 @@ class SetInclusionRuleWithArrays(rewriter: SymbStateRewriter) extends RewritingR
           case (CellTFrom(SetT1(_)), CellTFrom(SetT1(_))) =>
             subset(rightState, leftCell, rightCell, false)
 
+          case (CellTFrom(SetT1(_)), InfSetT(_)) =>
+            subset(rightState, leftCell, rightCell, false)
+
           case (CellTFrom(SetT1(SetT1(t1))), PowSetT(SetT1(t2))) =>
             if (t1 != t2) {
               throw new RewriterException("Unexpected set types: %s and %s in %s"

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala

@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt._
-import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT}
+import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, InfSetT, PowSetT}
 import at.forsyte.apalache.tla.lir.{OperEx, SetT1}
 import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.UntypedPredefs._
@@ -31,6 +31,9 @@ class SetInclusionRuleWithFunArrays(rewriter: SymbStateRewriter) extends Rewriti
           case (CellTFrom(SetT1(_)), CellTFrom(SetT1(_))) =>
             rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)
 
+          case (CellTFrom(SetT1(_)), InfSetT(_)) =>
+            rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)
+
           case (CellTFrom(SetT1(SetT1(t1))), PowSetT(SetT1(t2))) =>
             if (t1 != t2) {
               throw new RewriterException("Unexpected set types: %s and %s in %s"