fix: No unguarded reverse casts in the arguments type encoding

Source/VCExpr/TypeErasure/TypeErasureArguments.cs

@@ -47,16 +47,28 @@ public override Object Clone()
 
     ///////////////////////////////////////////////////////////////////////////////    
 
-    // generate axioms of the kind "forall x:U. {Int2U(U2Int(x))} Int2U(U2Int(x))==x"
-    // (this makes use of the assumption that only well-typed terms are generated
-    // by the SMT-solver, i.e., that U2Int is only applied to terms that actually
-    // are of type int)
+    // This encoding emits NO reverse cast axiom.  The axiom it used to emit,
+    //   forall x:U. {U2Int(x)} Int2U(U2Int(x)) == x,
+    // says that every value of U is an int; its bool instance says that U has at
+    // most two elements, while the left inverse axiom U2Int(Int2U(n)) == n
+    // (GenLeftInverseAxiom, emitted for every cast) makes U infinite, so the two
+    // have no model together (boogie-org/boogie#1168).  It relied on "only
+    // well-typed terms are generated by the SMT-solver", which a solver does not
+    // promise.  A guard in terms of the explicit type arguments of polymorphic
+    // functions (f(intType, ...) is always an int) is not true either: an axiom
+    //   forall<T> x: T :: Id(x) == x
+    // is erased to forall t: T, x: U :: Id(t, x) == x, which makes Id(intType, x)
+    // equal to x for EVERY x in U.
+    // What relied on the reverse cast: quantifiers whose int (bool, ...)
+    // variables were retyped to U for the sake of their triggers, which this
+    // encoding no longer does (TypeEraserArguments.Visit(VCExprQuantifier)); and
+    // an int reaching a U position as a U term in one formula and as a cast in
+    // another, which the normal form of OpTypeEraserArguments.AssembleOpExpression
+    // rules out.
     protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU)
     {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
-      VCExpr
-        eq = GenReverseCastEq(castToU, castFromU, out var var, out var triggers);
-      return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, 1, eq);
+      return VCExpressionGenerator.True;
     }
 
     protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU)
@@ -510,23 +522,17 @@ public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings
 
       // type variables are replaced with ordinary quantified variables
       GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings);
-      VCExpr
-        newNode = HandleQuantifier(node, newBoundVars, bindings);
-      Contract.Assert(newNode != null);
-
-      if (!(newNode is VCExprQuantifier) || !IsUniversalQuantifier(node))
-      {
-        return newNode;
-      }
 
-      if (!RedoQuantifier(node, (VCExprQuantifier) newNode, node.BoundVars, oldBindings,
-        out var bindings2, out newBoundVars))
-      {
-        return newNode;
-      }
-
-      GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings2);
-      return HandleQuantifier(node, newBoundVars, bindings2);
+      // The quantifier is NOT redone with its int (bool, ...) variables retyped to
+      // U when they occur in the triggers only under a cast (RedoQuantifier, which
+      // the predicates encoding still uses, with a type premise on each retyped
+      // variable).  Here the redone body spoke of every value x of U where the
+      // original speaks of the ints, and the two agreed only under the reverse
+      // cast axiom Int2U(U2Int(x)) == x, which this encoding no longer emits (see
+      // GenReverseCastAxiom).  A trigger Int2U(n) still matches every U term the
+      // solver knows to be a cast, and under the normal form of
+      // AssembleOpExpression a value of type int reaches a U position as a cast.
+      return HandleQuantifier(node, newBoundVars, bindings);
     }
 
     private void GenBoundVarsForTypeParams(List<TypeVariable> typeParams,
@@ -623,8 +629,21 @@ private VCExpr AssembleOpExpression(OpTypesPair opTypes, IEnumerable<VCExpr> old
       foreach (VCExpr arg in oldArgs)
       {
         Contract.Assert(arg != null);
-        newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings),
-          Cce.NonNull(newFun.InParams[i]).TypedIdent.Type));
+        VCExpr newArg = Eraser.Mutate(arg, bindings);
+        Type paramType = Cce.NonNull(newFun.InParams[i]).TypedIdent.Type;
+        // A value whose type is int (bool, ...) is passed to a U parameter as the
+        // cast of an int, Int2U(U2Int(t)), also when its translation t is already
+        // a U term -- the result of a polymorphic function or of a map select at
+        // int.  In Boogie's semantics this is the identity.  Without the reverse
+        // cast axiom (see GenReverseCastAxiom) t and Int2U(U2Int(t)) are no
+        // longer known to be equal, and without this normal form the same int
+        // would reach a U position in two forms, as t in one formula and as
+        // Int2U(U2Int(t)) in another.
+        if (paramType.Equals(AxBuilder.U) && newArg.Type.Equals(AxBuilder.U) && AxBuilder.UnchangedType(arg.Type))
+        {
+          newArg = AxBuilder.Cast(newArg, arg.Type);
+        }
+        newArgs.Add(AxBuilder.Cast(newArg, paramType));
         i = i + 1;
       }
 

Test/test21/issue-1168-redo.bpl

@@ -0,0 +1,36 @@
+// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:a "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:p "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Issue #1168, continued (see issue-1168.bpl).  The last two axioms below are
+// quantifiers whose int (bool) variable occurs in the trigger only under a cast,
+// Box(intType, int_2_U(n)).  The arguments encoding used to redo such a
+// quantifier with the variable retyped to U, so that the trigger matches boxed
+// values that are not casts; the redone body is then stated for every value of U,
+// not only the ints (bools), and only the reverse casts made the two readings
+// agree.  So dropping the reverse casts is not enough: with the retyping kept,
+// the bool axiom says that every value boxed at bool is a bool, and with
+// Unbox(Box(x)) == x that bounds U to two elements again.  Every axiom here is
+// true in Boogie's semantics, and no encoding may prove "assert false".
+
+type Box;
+function Box<T>(x: T): Box;
+function Unbox<T>(b: Box): T;
+axiom (forall<T> x: T :: { Box(x) } Unbox(Box(x)): T == x);
+
+function IdI(n: int): int;
+axiom (forall n: int :: { IdI(n) } IdI(n) == n);
+function IdB(b: bool): bool;
+axiom (forall b: bool :: { IdB(b) } IdB(b) == b);
+
+axiom (forall n: int :: { Box(n) } Box(n) == Box(IdI(n)));
+axiom (forall b: bool :: { Box(b) } Box(b) == Box(IdB(b)));
+
+procedure P(n: int)
+{
+  assert Unbox(Box(n)): int == n;
+  assert false;  // not provable
+}

Test/test21/issue-1168-redo.bpl.expect

@@ -0,0 +1,5 @@
+issue-1168-redo.bpl(35,3): Error: this assertion could not be proved
+Execution trace:
+    issue-1168-redo.bpl(34,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error

Test/test21/issue-1168.bpl

@@ -0,0 +1,29 @@
+// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:a "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:p "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Issue #1168.  The arguments encoding erases every non-built-in type to one
+// sort U, with casts in and out of U for each built-in type.  Beside the left
+// inverse U_2_int(int_2_U(n)) == n, which makes U infinite, it used to emit
+// reverse casts such as
+//   forall x: U :: bool_2_U(U_2_bool(x)) == x
+// which say that every value of U is a bool, so that U has at most two
+// elements.  Together they have no model, and model-based quantifier
+// instantiation found that out: it proved "assert false" below under
+// /typeEncoding:a.  No encoding may prove it.  The iteration bound keeps the
+// search short: when the solver reaches it, it answers unknown, and the
+// assertion is reported as not proved.
+
+type Box;
+function Box<T>(x: T): Box;
+function Unbox<T>(b: Box): T;
+axiom (forall<T> x: T :: { Box(x) } Unbox(Box(x)): T == x);
+
+procedure P(b: bool, n: int)
+{
+  assert Unbox(Box(b)): bool == b && Unbox(Box(n)): int == n;
+  assert false;  // not provable
+}

Test/test21/issue-1168.bpl.expect

@@ -0,0 +1,5 @@
+issue-1168.bpl(28,3): Error: this assertion could not be proved
+Execution trace:
+    issue-1168.bpl(27,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error