closes #985: do not skolemize let-definitions that are used as values

UNRELEASED.md

@@ -12,4 +12,5 @@
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
 ### Bug fixes
 
-* Fixed a heisenbug caused by EXCEPT on records, which used unsorted keys, see #987
+ * Fixed a heisenbug caused by EXCEPT on records, which used unsorted keys, see #987
+ * Fixed unsound skolemization that applied to let-definitions, see #985

test/tla/Bug985.tla

@@ -0,0 +1,30 @@
+-------------------------------- MODULE Bug985 --------------------------------
+\* This is a regression test
+\* for unsound Skolemization of expressions under LET-IN:
+\*
+\* https://github.com/informalsystems/apalache/issues/985
+VARIABLES
+    \* @type: Set(Int);
+    S,
+    \* @type: Bool;
+    tx_fail
+
+Init ==
+    /\ S = { 1, 2 }
+    /\ tx_fail = TRUE
+
+Next ==
+    LET fail ==
+        \* This should be true since S = { 1, 2 }.
+        \* However, if we Skolemize x and then negate fail,
+        \* the solver is free to use 1 as a value.
+        \E x \in S:
+            x /= 1
+    IN
+    /\ tx_fail' = fail
+    /\ UNCHANGED S
+
+\* This invariant should hold true. However, it fails in #985.
+Inv ==
+    tx_fail
+===============================================================================

test/tla/cli-integration-tests.md

@@ -1071,11 +1071,21 @@ $ apalache-mc check RecordExcept987.tla | sed 's/I@.*//'
 EXITCODE: OK
 ```
 
+### check Bug985 succeeds
+
+Regression test for https://github.com/informalsystems/apalache/issues/985
+Skolemization should be sound.
+
+```sh
+$ apalache-mc check Bug985.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
 ## configure the check command
 
-Testing various flags that are set via command-line options and the TLC
-configuration file. The CLI has priority over the TLC config. So we have to
-test that it all works together.
+Testing various flags that are set via command-line options and the TLC configuration file. The CLI has priority over
+the TLC config. So we have to test that it all works together.
 
 ### configure default Init and Next
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/analyses/SkolemizationMarker.scala

@@ -3,13 +3,12 @@ package at.forsyte.apalache.tla.bmcmt.analyses
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TransformationTracker}
+import at.forsyte.apalache.tla.lir.values.TlaInt
 import com.google.inject.Inject
 import com.typesafe.scalalogging.LazyLogging
-import at.forsyte.apalache.tla.lir.convenience._
-import at.forsyte.apalache.tla.lir.values.TlaInt
 
 /**
- * <p>The skolemization analysis finds the existential quantifiers that can be safely replace by constants
+ * <p>The skolemization analysis finds the existential quantifiers that can be safely replaced by constants
  * (Skolemizable). This class is not a pure analysis but a transformer, that is, it modifies an argument expression.
  * Additionally, this analysis finds the cardinality comparisons like Cardinality(S) >= 4 that can be checked
  * more optimally than the direct computation of the cardinalities.</p>
@@ -22,7 +21,6 @@ import at.forsyte.apalache.tla.lir.values.TlaInt
  * @author Igor Konnov
  */
 class SkolemizationMarker @Inject() (tracker: TransformationTracker) extends TlaExTransformation with LazyLogging {
-
   override def apply(e: TlaEx): TlaEx = {
     transform(e)
   }
@@ -58,17 +56,50 @@ class SkolemizationMarker @Inject() (tracker: TransformationTracker) extends Tla
     // Effectively, IF-THEN-ELSE requires both \E and \A forms
 
     case ex @ LetInEx(body, defs @ _*) =>
-      // at this point, we only have nullary let-in definitions
-      def mapDef(df: TlaOperDecl) = df.copy(body = transform(df.body))
+      // At this point, we only have nullary let-in definitions of the form: `LET A == e1 in e2`
+      //
+      // There are two important cases to distinguish (bugfix for #985):
+      //   1. Expression e1 contains `\E x \in S: P` and `A` is used in a positive form in `e2` (as a non-value).
+      //   2. Expression e1 contains `\E x \in S: P` and `A` is used in a negative form or as a value in `e2`.
+      //
+      // Hence, we create copies of A for the both cases: one that could be skolemized and one that could not be.
+      def skolemizeDef(df: TlaOperDecl): Option[TlaOperDecl] = {
+        df.typeTag match {
+          case Typed(OperT1(Seq(), BoolT1())) =>
+            // Only if the let-definition returns a Boolean value, we have to worry about skolemization
+            Some(df.copy(body = transform(df.body), name = mkSkolemName(df.name)))
+
+          case _ =>
+            None
+        }
+
+      }
 
-      LetInEx(transform(body), defs map mapDef: _*)(ex.typeTag)
+      // introduce skolemized copies of the operators that return a Boolean, if needed
+      LetInEx(transform(body), defs ++ defs.flatMap(skolemizeDef): _*)(ex.typeTag)
 
-    case ex @ OperEx(oper, args @ _*) =>
+    case ex @ OperEx(TlaOper.apply, nm @ NameEx(operName)) =>
+      ex.typeTag match {
+        case Typed(BoolT1()) =>
+          // An application of a let-definition that returns a Boolean value.
+          // As Skolemization is allowed in this context, we use the Skolemizable version of the definition.
+          OperEx(TlaOper.apply, NameEx(mkSkolemName(operName))(nm.typeTag))(ex.typeTag)
+
+        case _ =>
+          // non-Boolean values are kept as they are
+          ex
+      }
+
+    case ex @ OperEx(_, _ @_*) =>
       // bugfix for #148: do not descend into value expressions, as Skolemization of non-formulas is unsound
       ex
 
     case terminal =>
       terminal // terminal expression, stop here
   }
 
+  private def mkSkolemName(name: String): String = {
+    "%s$_skolem".format(name)
+  }
+
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/analyses/TestSkolemizationMarker.scala

@@ -1,8 +1,9 @@
-package at.forsyte.apalache.tla.bmcmt.analyses
+package at.forsyte.apalache.bmcmt.analyses
 
-import at.forsyte.apalache.tla.lir.OperEx
-import at.forsyte.apalache.tla.lir.convenience.tla
-import at.forsyte.apalache.tla.lir.oper.ApalacheOper
+import at.forsyte.apalache.tla.bmcmt.analyses.SkolemizationMarker
+import at.forsyte.apalache.tla.bmcmt.types.BoolT
+import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, OperT1, SetT1}
+import at.forsyte.apalache.tla.lir.TypedPredefs.{BuilderExAsTyped, BuilderOperDeclAsTyped}
 import at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners
 import at.forsyte.apalache.tla.lir.UntypedPredefs._
 import org.junit.runner.RunWith
@@ -11,25 +12,33 @@ import org.scalatest.{BeforeAndAfterEach, FunSuite}
 
 @RunWith(classOf[JUnitRunner])
 class TestSkolemizationMarker extends FunSuite with BeforeAndAfterEach {
+
+  import at.forsyte.apalache.tla.lir.convenience.tla._
+
+  private val Int = IntT1()
+  private val Bool = BoolT1()
+  private val BoolOper0 = OperT1(Seq(), BoolT1())
+  private val IntSet = SetT1(IntT1())
+
   private var marker = new SkolemizationMarker(TrackerWithListeners())
 
   override def beforeEach(): Unit = {
     marker = new SkolemizationMarker(TrackerWithListeners())
   }
 
   test("""mark: \E y \in S: P""") {
-    val input = tla.exists(tla.name("y"), tla.name("S"), tla.name("P")).untyped()
-    val expected = tla.apalacheSkolem(input).untyped()
+    val input = exists(name("y"), name("S"), name("P")).untyped()
+    val expected = apalacheSkolem(input).untyped()
 
     val output = marker(input)
     assert(expected == output)
   }
 
   test("""mark: \E y \in S: P /\ \E z \in S: Q""") {
-    val left = tla.exists(tla.name("y"), tla.name("S"), tla.name("P"))
-    val right = tla.exists(tla.name("z"), tla.name("S"), tla.name("Q"))
-    val input = tla.and(left, right).untyped()
-    val expected = tla.and(tla.apalacheSkolem(left), tla.apalacheSkolem(right)).untyped()
+    val left = exists(name("y"), name("S"), name("P"))
+    val right = exists(name("z"), name("S"), name("Q"))
+    val input = and(left, right).untyped()
+    val expected = and(apalacheSkolem(left), apalacheSkolem(right)).untyped()
 
     val output = marker(input)
     assert(expected == output)
@@ -38,27 +47,66 @@ class TestSkolemizationMarker extends FunSuite with BeforeAndAfterEach {
   // see the issue #148
   test("""no mark: x' <- \E y \in S: P""") {
     val input =
-      tla.assignPrime(tla.name("x"), tla.exists(tla.name("y"), tla.name("S"), tla.name("P"))).untyped()
+      assignPrime(name("x"), exists(name("y"), name("S"), name("P"))).untyped()
 
     val output = marker(input)
     assert(input == output)
   }
 
+  // skolemize let-definitions, if they are used positively as part of a formula, see the issue #985
+  test("""mark: LET A == \E y \in S: P IN A \/ TRUE""") {
+    val bodyOfA = exists(name("y") as Int, name("S") as IntSet, name("P") as Bool) as Bool
+    val declOfA = declOp("A", bodyOfA) as BoolOper0
+    val A = name("A") as BoolOper0
+    val B = bool(true).typed()
+    val input = letIn(or(appOp(A) as Bool, B) as Bool, declOfA) as Bool
+
+    // the body of A is skolemized
+    val bodyOfAskolem = apalacheSkolem(bodyOfA) as Bool
+    // the skolemized copy of A is used
+    val declOfAskolem = declOp("A$_skolem", bodyOfAskolem) as BoolOper0
+    // note that we have two let-in definitions now: one that is skolemized and one that is not skolemized
+    val skolemA = name("A$_skolem") as BoolOper0
+    val expected = letIn(or(appOp(skolemA) as Bool, B) as Bool, declOfA, declOfAskolem) as Bool
+
+    val output = marker(input)
+    assert(expected == output)
+  }
+
+  // do not skolemize let-definitions, if they are used as a value, see the issue #985
+  test("""mark: LET A == \E y \in S: P IN A = FALSE""") {
+    val bodyOfA = exists(name("y") as Int, name("S") as IntSet, name("P") as Bool) as Bool
+    val declOfA = declOp("A", bodyOfA) as BoolOper0
+    val A = name("A") as BoolOper0
+    val B = bool(false).typed()
+    val input = letIn(eql(appOp(A) as Bool, B) as Bool, declOfA) as Bool
+
+    // the body of A is skolemized
+    val bodyOfAskolem = apalacheSkolem(bodyOfA) as Bool
+    // the skolemized copy of A is used
+    val declOfAskolem = declOp("A$_skolem", bodyOfAskolem) as BoolOper0
+    // note that we have two let-in definitions now: one that is skolemized and one that is not skolemized
+    val expected = letIn(eql(appOp(A) as Bool, B) as Bool, declOfA, declOfAskolem) as Bool
+
+    val output = marker(input)
+    assert(expected == output)
+  }
+
   test("""mark: Cardinality(S) >= 3""") {
-    val input = tla.ge(tla.card(tla.name("S")), tla.int(3)).untyped()
-    val expected = tla.apalacheConstCard(input).untyped()
+    val input = ge(card(name("S")), int(3)).untyped()
+    val expected = apalacheConstCard(input).untyped()
     val output = marker(input)
     assert(expected == output)
   }
 
   test("""no mark: ~(Cardinality(S) >= 3)""") {
-    val input = tla.not(tla.ge(tla.card(tla.name("S")), tla.int(3))).untyped()
+    val input = not(ge(card(name("S")), int(3))).untyped()
     val output = marker(input)
     assert(input == output)
   }
 
   test("""no mark: Cardinality(S) < 3""") {
-    val input = tla.lt(tla.card(tla.name("S")), tla.int(3)).untyped()
+    val input = lt(card(name("S")), int(3)).untyped()
     val output = marker(input)
     assert(input == output)
   }