Bogus safety violation checking if a set is a subset of Nat. (#2960)

* Bogus safety violation checking if a set is a subset of Nat.

Fixes Github issue #2948
#2948

* Bogus safety violation checking if a set is a subset of Nat.

Fixes Github issue #2948
#2948

* Bogus safety violation checking if a set is a subset of Nat.

All encoding are affected.

Fixes Github issue #2948
#2948

* Bogus safety violation checking if a set is a subset of Nat.

Part of Github issue $2948
#2948

* Add issue number in changelog

---------

Co-authored-by: Igor Konnov <igor@konnov.phd>
Co-authored-by: Thomas Pani <thomas.pani@gmail.com>

.unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md

@@ -0,0 +1 @@
+Show note that expression is unsupported instead of reporting a counterexample claiming that e.g. `{42} \in SUBSET Nat` is false, see #2690

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

@@ -298,9 +298,11 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val leftElems = state.arena.getHas(left)
     val rightElems = state.arena.getHas(right)
     if (leftElems.isEmpty) {
+      assert(left.cellType != InfSetT(CellTFrom(IntT1)))
       // SE-SUBSETEQ1
       state.setRex(state.arena.cellTrue().toBuilder)
     } else if (rightElems.isEmpty) {
+      assert(right.cellType != InfSetT(CellTFrom(IntT1)))
       // SE-SUBSETEQ2
       def notIn(le: ArenaCell) = {
         tla.not(tla.selectInSet(le.toBuilder, left.toBuilder))

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

@@ -29,7 +29,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule {
   }
 
   // TODO: x \in S should be equivalent to SkolemExists(\E t \in S: x = t)
-  // This is only true for the positive occurences of x \in S!
+  // This is only true for the positive occurrences of x \in S!
   override def apply(state: SymbState): SymbState = {
     state.ex match {
       // a common pattern x \in {y} that is equivalent to x = y, e.g., the assignment solver creates it
@@ -72,6 +72,20 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule {
   }
 
   protected def powSetIn(state: SymbState, powsetCell: ArenaCell, elemCell: ArenaCell): SymbState = {
+    // Check that the powsetCell.cellType is not an infinite set.
+    state.arena.getDom(powsetCell).cellType match {
+      case InfSetT(ct) =>
+        throw new RewriterException("SetInRule.powSetIn is not implemented for infinite type %s (found in %s)"
+              .format(InfSetT(ct), state.ex), state.ex)
+      case _ =>
+    }
+    elemCell.cellType match {
+      case InfSetT(_) =>
+        throw new RewriterException("SetInRule.powSetIn is not implemented for infinite type %s (found in %s)"
+              .format(elemCell.cellType, state.ex), state.ex)
+      case _ =>
+    }
+
     def checkType: PartialFunction[(CellT, CellT), Unit] = {
       case (PowSetT(SetT1(expectedType)), CellTFrom(SetT1(actualType))) =>
         if (expectedType != actualType) {

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

@@ -18,6 +18,20 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite
   private val simplifier = new ConstSimplifierForSmt
 
   override protected def powSetIn(state: SymbState, powsetCell: ArenaCell, elemCell: ArenaCell): SymbState = {
+    // Check that the powsetCell.cellType is not an infinite set.
+    state.arena.getDom(powsetCell).cellType match {
+      case InfSetT(ct) =>
+        throw new RewriterException("SetInRule.powSetIn is not implemented for infinite type %s (found in %s)"
+              .format(InfSetT(ct), state.ex), state.ex)
+      case _ =>
+    }
+    elemCell.cellType match {
+      case InfSetT(_) =>
+        throw new RewriterException("SetInRule.powSetIn is not implemented for infinite type %s (found in %s)"
+              .format(elemCell.cellType, state.ex), state.ex)
+      case _ =>
+    }
+
     def checkType: PartialFunction[(CellT, CellT), Unit] = {
       case (PowSetT(SetT1(expectedType)), CellTFrom(SetT1(actualType))) =>
         assert(expectedType == actualType)

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterPowerset.scala

@@ -5,7 +5,8 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.PowSetCtor
 import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT}
 import at.forsyte.apalache.tla.lir.TypedPredefs._
 import at.forsyte.apalache.tla.lir.convenience.tla._
-import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, NameEx, SetT1}
+import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet}
+import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, NameEx, SetT1, Typed, ValEx}
 
 trait TestSymbStateRewriterPowerset extends RewriterBase {
   private val types = Map(
@@ -76,6 +77,91 @@ trait TestSymbStateRewriterPowerset extends RewriterBase {
     assertTlaExAndRestore(create(rewriterType), state)
   }
 
+  test("""SSE-SUBSETEQ: {1, 2, 3, 4} \in SUBSET Nat""") { rewriterType: SMTEncoding =>
+    def setTo(k: Int) = enumSet((1 to k).map(int): _*)
+
+    val set1to4 = setTo(4) ? "I"
+    val powset = powSet(ValEx(TlaNatSet)(Typed(SetT1(IntT1)))) ? "II"
+    val inEx = in(set1to4, powset)
+      .typed(types, "b")
+    val state = new SymbState(inEx, arena, Binding())
+
+    val rewriter = create(rewriterType)
+    try {
+      val _ = rewriter.rewriteUntilDone(state)
+      fail("expected an error message about subseteq over infinite sets being unsupported")
+    } catch {
+      case _: RewriterException => () // OK
+    }
+  }
+
+  test("""SSE-SUBSETEQ: Nat \in SUBSET {1, 2, 3, 4}""") { rewriterType: SMTEncoding =>
+    def setTo(k: Int) = enumSet((1 to k).map(int): _*)
+
+    val set1to4 = setTo(4) ? "I"
+    val powset = powSet(set1to4) ? "II"
+    val nat = ValEx(TlaNatSet)(Typed(SetT1(IntT1))) ? "I"
+    val inEx = in(nat, powset)
+      .typed(types, "b")
+    val state = new SymbState(inEx, arena, Binding())
+
+    val rewriter = create(rewriterType)
+    try {
+      val _ = rewriter.rewriteUntilDone(state)
+      fail("expected an error message about subseteq over infinite sets being unsupported")
+    } catch {
+      case _: RewriterException => () // OK
+    }
+  }
+
+  test("""SSE-SUBSETEQ: Nat \in SUBSET Nat""") { rewriterType: SMTEncoding =>
+    val nat = ValEx(TlaNatSet)(Typed(SetT1(IntT1))) ? "I"
+    val powset = powSet(ValEx(TlaNatSet)(Typed(SetT1(IntT1)))) ? "II"
+    val inEx = in(nat, powset)
+      .typed(types, "b")
+    val state = new SymbState(inEx, arena, Binding())
+
+    val rewriter = create(rewriterType)
+    try {
+      val _ = rewriter.rewriteUntilDone(state)
+      fail("expected an error message about subseteq over infinite sets being unsupported")
+    } catch {
+      case _: RewriterException => () // OK
+    }
+  }
+
+  test("""SSE-SUBSETEQ: Nat \in SUBSET Int""") { rewriterType: SMTEncoding =>
+    val nat = ValEx(TlaNatSet)(Typed(SetT1(IntT1))) ? "I"
+    val powset = powSet(ValEx(TlaIntSet)(Typed(SetT1(IntT1)))) ? "II"
+    val inEx = in(nat, powset)
+      .typed(types, "b")
+    val state = new SymbState(inEx, arena, Binding())
+
+    val rewriter = create(rewriterType)
+    try {
+      val _ = rewriter.rewriteUntilDone(state)
+      fail("expected an error message about subseteq over infinite sets being unsupported")
+    } catch {
+      case _: RewriterException => () // OK
+    }
+  }
+
+  test("""SSE-SUBSETEQ: Int \in SUBSET Nat""") { rewriterType: SMTEncoding =>
+    val nat = ValEx(TlaIntSet)(Typed(SetT1(IntT1))) ? "I"
+    val powset = powSet(ValEx(TlaNatSet)(Typed(SetT1(IntT1)))) ? "II"
+    val inEx = in(nat, powset)
+      .typed(types, "b")
+    val state = new SymbState(inEx, arena, Binding())
+
+    val rewriter = create(rewriterType)
+    try {
+      val _ = rewriter.rewriteUntilDone(state)
+      fail("expected an error message about subseteq over infinite sets being unsupported")
+    } catch {
+      case _: RewriterException => () // OK
+    }
+  }
+
   test("""SE-SUBSET: \E X \in SUBSET {1, 2}: TRUE (sat)""") { rewriterType: SMTEncoding =>
     // a regression test that failed in the previous versions
     val set = enumSet(int(1), int(2)) ? "I"