Prevent spurious counterexamples on maps by tightening its domain

PiperOrigin-RevId: 956295539

Author: l46kok

BUILD.bazel

@@ -95,6 +95,14 @@ java_library(
     ],
 )
 
+java_library(
+    name = "java_jline",
+    exports = [
+        "@maven//:org_jline_jline_reader",
+        "@maven//:org_jline_jline_terminal",
+    ],
+)
+
 default_java_toolchain(
     name = "repository_default_toolchain",
     configuration = DEFAULT_TOOLCHAIN_CONFIGURATION,

MODULE.bazel

@@ -95,6 +95,8 @@ maven.install(
         "info.picocli:picocli:4.7.7",
         "org.antlr:antlr4-runtime:4.13.2",
         "org.freemarker:freemarker:2.3.34",
+        "org.jline:jline-reader:3.26.1",
+        "org.jline:jline-terminal:3.26.1",
         "org.jspecify:jspecify:1.0.0",
         "org.threeten:threeten-extra:1.8.0",
         "org.yaml:snakeyaml:2.5",

common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

@@ -18,7 +18,6 @@
 import static com.google.common.math.LongMath.checkedMultiply;
 import static com.google.common.math.LongMath.checkedSubtract;
 
-import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.Strings;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import com.google.protobuf.Duration;
@@ -50,15 +49,11 @@
 public final class ProtoTimeUtils {
 
   // Timestamp for "0001-01-01T00:00:00Z"
-  @VisibleForTesting
-  static final long TIMESTAMP_SECONDS_MIN = -62135596800L;
+  public static final long TIMESTAMP_SECONDS_MIN = -62135596800L;
   // Timestamp for "9999-12-31T23:59:59Z"
-  @VisibleForTesting
-  static final long TIMESTAMP_SECONDS_MAX = 253402300799L;
-  @VisibleForTesting
-  static final long DURATION_SECONDS_MIN = -315576000000L;
-  @VisibleForTesting
-  static final long DURATION_SECONDS_MAX = 315576000000L;
+  public static final long TIMESTAMP_SECONDS_MAX = 253402300799L;
+  public static final long DURATION_SECONDS_MIN = -315576000000L;
+  public static final long DURATION_SECONDS_MAX = 315576000000L;
 
   private static final int MILLIS_PER_SECOND = 1000;
 

verifier/README.md

@@ -400,7 +400,7 @@ public class InvariantsExample {
 
 ### Timeouts
 
-SMT solving is NP-complete and can theoretically stop responding or take an
+SMT solving is NP-hard and can theoretically stop responding or take an
 exponential amount of time for complex formulas.
 The verifier uses a default timeout of 10 seconds. It is recommended to
 configure this to a reasonable duration for your specific use case using
@@ -433,3 +433,7 @@ What this means for verification:
     default unless you have a specific need and bounded inputs.
 
 ---
+
+## Tools & CLI
+
+For command-line verification and interactive execution, see the [CLI Tool documentation](tools/README.md).

verifier/src/main/java/dev/cel/verifier/BUILD.bazel

@@ -98,6 +98,7 @@ java_library(
     tags = [
     ],
     deps = [
+        "//common/internal:proto_time_utils",
         "@maven//:com_google_errorprone_error_prone_annotations",
         "@maven//:com_google_guava_guava",
         "@maven//:tools_aqua_z3_turnkey",

verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

@@ -533,6 +533,12 @@ private Expr<?> getDefaultValueForType(CelType type) {
     if (type.equals(SimpleType.UINT)) {
       return typeSystem.mkUint(0);
     }
+    if (type.equals(SimpleType.TIMESTAMP)) {
+      return typeSystem.wrapTimestamp(ctx.mkInt(0));
+    }
+    if (type.equals(SimpleType.DURATION)) {
+      return typeSystem.wrapDuration(ctx.mkInt(0));
+    }
     if (type instanceof ListType) {
       if (emptyListCache == null) {
         emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX);
@@ -735,8 +741,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
               typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
               typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
 
+              boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
+              BoolExpr isApprox = ctx.mkBool(!isDynamic);
               return TranslatedValue.propagateStrict(
-                  ctx, typeSystem, callRes, Optional.of(expr), ctx.mkTrue(), args);
+                  ctx, typeSystem, callRes, Optional.of(expr), isApprox, args);
             });
   }
 
@@ -869,10 +877,6 @@ private TranslatedValue translateDynamicComprehension(
     ArrayExpr mapPresence =
         isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null;
 
-    if (isMap) {
-      applyBoundedMapBijection(mapPresence, seq, lengthExpr);
-    }
-
     BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
     truncationConditions.add(isTruncated);
 
@@ -885,14 +889,15 @@ private TranslatedValue translateDynamicComprehension(
     }
   }
 
-  private void applyBoundedMapBijection(
+  private BoolExpr getBoundedMapBijection(
       ArrayExpr mapPresence, SeqExpr<?> seq, ArithExpr lengthExpr) {
+    List<BoolExpr> constraints = new ArrayList<>();
     for (int i = 0; i < comprehensionUnrollLimit; i++) {
       for (int j = i + 1; j < comprehensionUnrollLimit; j++) {
         BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr);
         BoolExpr notEqual =
             ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j))));
-        typeConstraints.add(ctx.mkImplies(validPair, notEqual));
+        constraints.add(ctx.mkImplies(validPair, notEqual));
       }
     }
 
@@ -907,7 +912,8 @@ private void applyBoundedMapBijection(
                   ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
                   seqMap);
     }
-    typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
+    constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
+    return CelZ3TypeSystem.mkAndFlattened(ctx, constraints);
   }
 
   private TranslatedValue[] evaluateLoopCondAndStep(
@@ -1239,9 +1245,10 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
       }
       Expr<?> optRef = typeSystem.getOptionalRef(val);
       BoolExpr hasValue = typeSystem.optHasValue(optRef);
-      BoolExpr valConstraint =
-          createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType);
-      return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint));
+      Expr<?> optVal = typeSystem.getOptionalValue(optRef);
+      BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal));
+      BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType);
+      return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint)));
     }
     if (type.equals(SimpleType.BOOL)) {
       return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val);
@@ -1269,16 +1276,25 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
     if (type.equals(SimpleType.BYTES)) {
       return (BoolExpr) ctx.mkApp(typeSystem.bytesCons().getTesterDecl(), val);
     }
+    if (type.equals(SimpleType.TIMESTAMP)) {
+      IntExpr seconds = typeSystem.getTimestamp(val);
+      return ctx.mkAnd(
+          typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
+    }
+    if (type.equals(SimpleType.DURATION)) {
+      IntExpr seconds = typeSystem.getDuration(val);
+      return ctx.mkAnd(
+          typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
+    }
+
     if (type instanceof ListType) {
-      // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers
-      // here.
+      // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather
+      // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops.
+      // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧
+      // typeConstraint(seq[i])
       BoolExpr isList = typeSystem.isList(val);
       CelType elemType = ((ListType) type).elemType();
-      if (elemType.equals(SimpleType.DYN)) {
-        return isList;
-      }
 
-      // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i])
       Expr<?> listRef = typeSystem.getListRef(val);
       SeqExpr seq = typeSystem.getSeq(listRef);
       Expr length = ctx.mkLength(seq);
@@ -1288,20 +1304,70 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
       for (int i = 0; i < comprehensionUnrollLimit; i++) {
         IntExpr idx = ctx.mkInt(i);
         Expr elem = ctx.mkNth(seq, idx);
-        BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
         BoolExpr validIndex = ctx.mkLt(idx, length);
-        boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
-        BoolExpr outOfBounds = ctx.mkGe(idx, length);
-        boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown())));
+        // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in
+        // list(dyn). For concrete types, this is already implied by createTypeConstraintForType.
+        boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem))));
+        // Short-circuit DYN element types to prevent generating redundant validIndex ⇒ TRUE
+        // clauses.
+        if (!elemType.equals(SimpleType.DYN)) {
+          BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
+          boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
+        }
       }
 
       return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type instanceof MapType) {
-      // Do NOT emit a for-all quantifier over map keys here.
-      // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is
-      // naturally constrained by the primitive key assertions in getStructuralEquality().
-      return typeSystem.isMap(val);
+      // Do NOT emit a for-all quantifier over map keys or values here.
+      // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using
+      // bounded unrolling over the key sequence up to comprehensionUnrollLimit.
+      // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key)
+      //         ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val))
+      BoolExpr isMap = typeSystem.isMap(val);
+      MapType mapType = (MapType) type;
+      CelType keyType = mapType.keyType();
+      CelType valType = mapType.valueType();
+
+      Expr<?> mapRef = typeSystem.getMapRef(val);
+      SeqExpr seq = typeSystem.getMapKeys(mapRef);
+      Expr length = ctx.mkLength(seq);
+      ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
+      ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
+
+      List<BoolExpr> boundsAndTypes = new ArrayList<>();
+      boundsAndTypes.add(isMap);
+      boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
+
+      for (int i = 0; i < comprehensionUnrollLimit; i++) {
+        IntExpr idx = ctx.mkInt(i);
+        Expr key = ctx.mkNth(seq, idx);
+        BoolExpr validIndex = ctx.mkLt(idx, length);
+
+        BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key);
+        BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key));
+        // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in
+        // map(dyn, ...). For concrete map types, this is already implied by keyType constraints.
+        boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError)));
+        // Short-circuit DYN key types to prevent generating redundant validIndex ⇒ TRUE clauses.
+        if (!keyType.equals(SimpleType.DYN)) {
+          boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType)));
+        }
+
+        BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key);
+        BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
+
+        Expr mapVal = ctx.mkSelect(mapValues, key);
+        BoolExpr valNotError = ctx.mkNot(typeSystem.isError(mapVal));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
+        // Short-circuit DYN value types to prevent generating redundant validEntry ⇒ TRUE clauses.
+        if (!valType.equals(SimpleType.DYN)) {
+          boundsAndTypes.add(
+              ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
+        }
+      }
+
+      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type.kind() == CelKind.STRUCT) {
       return ctx.mkAnd(

verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java

@@ -303,8 +303,10 @@ CelVerificationResult verifyImplication(
                   /* isCounterexample= */ true));
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
-              String.format("Inconclusive: %s holds within the current loop unroll limit, but"
-                  + " may be violated for larger collections.", subjectName.toLowerCase(Locale.US)));
+              String.format(
+                  "Inconclusive: %s holds within the current loop unroll limit, but"
+                      + " may be violated for larger collections.",
+                  subjectName.toLowerCase(Locale.US)));
         case NO_MATCH:
           return CelVerificationResult.verified();
         case SOLVER_UNKNOWN:

verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

@@ -82,6 +82,10 @@ private static String formatExpr(
     // Handle CelType constructors wrapper unwrapping
     if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
       return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
+    } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
+      return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
+    } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
+      return "duration(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
     } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
       return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
     } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {
@@ -123,6 +127,8 @@ private static String formatExpr(
       return "Error";
     } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) {
       return "Unknown";
+    } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) {
+      return "null";
     } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) {
       Expr<?> optRef = expr.getArgs()[0];
       Expr<?> hasValueExpr =
@@ -173,14 +179,26 @@ private static String reconstructList(
 
   private static String reconstructMap(
       Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
-    Expr<?> presenceArray =
+    List<Expr<?>> keys = new ArrayList<>();
+    Expr<?> lenExpr =
         evaluateStrict(
             model,
-            typeSystem.getMapPresence(mapRef),
-            String.format("Z3 failed to evaluate presence array natively for map %s", mapRef));
-
-    List<Expr<?>> keys = new ArrayList<>();
-    extractKeys(presenceArray, keys);
+            ctx.mkLength(typeSystem.getMapKeys(mapRef)),
+            String.format("Z3 failed to evaluate length for map %s", mapRef));
+    if (lenExpr instanceof IntNum) {
+      int length = ((IntNum) lenExpr).getInt();
+      int printLimit = Math.min(length, 100);
+      for (int i = 0; i < printLimit; i++) {
+        Expr<?> elem =
+            evaluateStrict(
+                model,
+                ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)),
+                String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef));
+        if (!keys.contains(elem)) {
+          keys.add(elem);
+        }
+      }
+    }
 
     List<String> entries = new ArrayList<>();
     for (Expr<?> key : keys) {
@@ -209,11 +227,11 @@ private static String reconstructMap(
 
   private static String reconstructMessage(
       Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> msgRef) {
-    Expr<?> valuesArray =
+    Expr<?> presenceArray =
         evaluateStrict(
             model,
-            typeSystem.getMsgValues(msgRef),
-            String.format("Z3 failed to evaluate values array natively for msg %s", msgRef));
+            typeSystem.getMsgPresence(msgRef),
+            String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef));
 
     Expr<?> typeNameExpr =
         evaluateStrict(
@@ -224,7 +242,7 @@ private static String reconstructMessage(
     String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");
 
     List<Expr<?>> keys = new ArrayList<>();
-    extractKeys(valuesArray, keys);
+    extractKeys(presenceArray, keys);
 
     List<String> entries = new ArrayList<>();
     for (Expr<?> key : keys) {
@@ -262,16 +280,17 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
       FuncDecl<?> decl = arrayExpr.getFuncDecl();
       String declName = decl.getName().toString();
 
-      if (!declName.equals("store")) {
-        break;
+      if (declName.equals("store")) {
+        Expr<?>[] args = arrayExpr.getArgs();
+        Preconditions.checkState(
+            args.length == 3, "Z3 store array operation must have exactly 3 arguments");
+        if (!keys.contains(args[1])) {
+          keys.add(args[1]);
+        }
+        arrayExpr = args[0];
+        continue;
       }
-
-      Expr<?>[] args = arrayExpr.getArgs();
-      Preconditions.checkState(
-          args.length == 3, "Z3 store array operation must have exactly 3 arguments");
-      keys.add(args[1]);
-
-      arrayExpr = args[0];
+      break;
     }
   }