From c69c355877ea306e38eaf53212ba779efa14318b Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Mon, 2 Sep 2024 00:37:19 -0700
Subject: [PATCH] Bogus safety violation checking if a set is a subset of Nat.
 (#2971)

Keramelizer:
A \in SUBSET B  ~~>  \A a \in A: a \in B

Part of Github issue #2948
https://github.com/apalache-mc/apalache/issues/2948
---
 .../forsyte/apalache/tla/pp/Keramelizer.scala |  9 +++++++++
 .../apalache/tla/pp/TestKeramelizer.scala     | 20 +++++++++++++++++++
 2 files changed, 29 insertions(+)

diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala
index 6798860e5a..b85e6a87ba 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala
@@ -105,6 +105,15 @@ class Keramelizer(gen: UniqueNameGenerator, tracker: TransformationTracker)
         .forall(tla.name(tempName).as(elemType), setX, tla.in(tla.name(tempName).as(elemType), setY).as(BoolT1))
         .as(BoolT1)
 
+    // rewrite A \in SUBSET B
+    // into \A a \in A: a \in B
+    case OperEx(TlaSetOper.in, setX, OperEx(TlaSetOper.powerset, setY)) =>
+      val elemType = getElemType(setX)
+      val tempName = gen.newName()
+      tla
+        .forall(tla.name(tempName).as(elemType), setX, tla.in(tla.name(tempName).as(elemType), setY).as(BoolT1))
+        .as(BoolT1)
+
     // rewrite f \in [S -> SUBSET T]
     // into DOMAIN f = S /\ \A x \in S: \A y \in f[x]: y \in T
     case OperEx(TlaSetOper.in, fun, OperEx(TlaSetOper.funSet, dom, OperEx(TlaSetOper.powerset, powSetDom))) =>
diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestKeramelizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestKeramelizer.scala
index c46d77d90e..e61250896a 100644
--- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestKeramelizer.scala
+++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestKeramelizer.scala
@@ -339,6 +339,26 @@ class TestKeramelizer extends AnyFunSuite with Checkers with BeforeAndAfterEach
     assert(expected == output)
   }
 
+  test("""A \in SUBSET B ~~> \A a \in A: a \in B""") {
+    val types = Map("BOOL" -> BoolT1, "POWSET" -> SetT1(SetT1(IntT1)), "SET" -> SetT1(IntT1), "INT" -> IntT1)
+    def A = tla.name("A") ? "SET"
+    def B = tla.name("B") ? "SET"
+    val input =
+      tla
+        .in(A, tla.powSet(B) ? "POWSET")
+        .typed(types, "BOOL")
+    val output = keramelizer.apply(input)
+
+    val isExpected = output match {
+      // \A element \in A: element \in B
+      case OperEx(TlaBoolOper.forall, NameEx(boundName), NameEx("A"),
+              OperEx(TlaSetOper.in, NameEx(inName), NameEx("B"))) =>
+        boundName == inName
+      case _ => false
+    }
+    assert(isExpected, s"Input $input and got $output")
+  }
+
   test("""A \subseteq B ~~> \A a \in A: a \in B""") {
     val types = Map("BOOL" -> BoolT1, "SET" -> SetT1(IntT1), "INT" -> IntT1)
     def A = tla.name("A") ? "SET"