Tighten the counterexample domain for double/int and parameterized unknown

PiperOrigin-RevId: 957339001

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",

verifier/BUILD.bazel

@@ -41,6 +41,13 @@ java_library(
     exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"],
 )
 
+java_library(
+    name = "numeric_bounds",
+    compatible_with = [],
+    visibility = [":verifier_internal"],
+    exports = ["//verifier/src/main/java/dev/cel/verifier:numeric_bounds"],
+)
+
 java_library(
     name = "type_system",
     compatible_with = [],

verifier/README.md

@@ -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

@@ -91,13 +91,27 @@ java_library(
     ],
 )
 
+java_library(
+    name = "numeric_bounds",
+    srcs = ["CelNumericBounds.java"],
+    compatible_with = [],
+    tags = [
+    ],
+    deps = [
+        "//:auto_value",
+        "//common/annotations",
+        "@maven//:com_google_guava_guava",
+    ],
+)
+
 java_library(
     name = "type_system",
     srcs = ["CelZ3TypeSystem.java"],
     compatible_with = [],
     tags = [
     ],
     deps = [
+        ":numeric_bounds",
         "//common/internal:proto_time_utils",
         "@maven//:com_google_errorprone_error_prone_annotations",
         "@maven//:com_google_guava_guava",
@@ -121,6 +135,7 @@ java_library(
     tags = [
     ],
     deps = [
+        ":numeric_bounds",
         ":type_system",
         ":verifier",
         "//:auto_value",

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

@@ -24,7 +24,9 @@
 import dev.cel.common.ast.CelConstant;
 import dev.cel.common.ast.CelExpr;
 import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import org.jspecify.annotations.Nullable;
 
 /**
@@ -83,29 +85,22 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c
           context.hasher.putByte((byte) 0); // 0 = bound
           context.hasher.putInt(bIdx);
         } else {
-          int fIdx = -1;
-          for (int i = 0; i < context.freeVars.size(); i++) {
-            if (context.freeVars.get(i).ident().name().equals(name)) {
-              fIdx = i;
-              break;
-            }
-          }
-          if (fIdx == -1) {
+          Integer fIdx = context.freeVarIndices.get(name);
+          if (fIdx == null) {
             context.freeVars.add(expr);
             fIdx = context.freeVars.size() - 1;
+            context.freeVarIndices.put(name, fIdx);
           }
           context.hasher.putByte((byte) 1); // 1 = free
           context.hasher.putInt(fIdx);
         }
         break;
       case SELECT:
         hashAst(expr.select().operand(), scope, context);
-        context.hasher.putInt(expr.select().field().length());
         context.hasher.putString(expr.select().field(), UTF_8);
         context.hasher.putBoolean(expr.select().testOnly());
         break;
       case CALL:
-        context.hasher.putInt(expr.call().function().length());
         context.hasher.putString(expr.call().function(), UTF_8);
         context.hasher.putBoolean(expr.call().target().isPresent());
         if (expr.call().target().isPresent()) {
@@ -210,6 +205,7 @@ private static void hashConstant(CelConstant constant, HasherContext context) {
 
   private static final class HasherContext {
     final Hasher hasher;
+    final Map<String, Integer> freeVarIndices = new HashMap<>();
     final List<CelExpr> freeVars = new ArrayList<>();
 
     HasherContext(HashFunction hashFunction) {

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

@@ -741,7 +741,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
               typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
               typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
 
-              boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true);
+              boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
               BoolExpr isApprox = ctx.mkBool(!isDynamic);
               return TranslatedValue.propagateStrict(
                   ctx, typeSystem, callRes, Optional.of(expr), isApprox, args);
@@ -877,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);
 
@@ -893,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));
       }
     }
 
@@ -915,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(
@@ -1230,7 +1228,7 @@ private BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSynta
             .orElseThrow(
                 () -> new IllegalArgumentException("Type not found for expr ID: " + exprId));
     BoolExpr typeConstraint = createTypeConstraintForType(val, type);
-    return ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val), typeConstraint);
+    return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint);
   }
 
   private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
@@ -1247,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);
@@ -1258,15 +1257,15 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
       Expr<?> unwrapped = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], val);
       return ctx.mkAnd(
           ctx.mkApp(typeSystem.intCons().getTesterDecl(), val),
-          ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MIN_INT64)),
-          ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_INT64)));
+          ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MIN_INT64)),
+          ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_INT64)));
     }
     if (type.equals(SimpleType.UINT)) {
       Expr<?> unwrapped = ctx.mkApp(typeSystem.uintCons().getAccessorDecls()[0], val);
       return ctx.mkAnd(
           ctx.mkApp(typeSystem.uintCons().getTesterDecl(), val),
           ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(0)),
-          ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_UINT64)));
+          ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_UINT64)));
     }
     if (type.equals(SimpleType.DOUBLE)) {
       return (BoolExpr) ctx.mkApp(typeSystem.doubleCons().getTesterDecl(), val);
@@ -1289,15 +1288,13 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
     }
 
     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);
@@ -1307,20 +1304,62 @@ 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);
+        // 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))));
+        BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
         boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
-        BoolExpr outOfBounds = ctx.mkGe(idx, length);
-        boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown())));
       }
 
       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)));
+        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 =
+            unknownIdentifiers.isEmpty()
+                ? ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal))
+                : ctx.mkNot(typeSystem.isError(mapVal));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
+      }
+
+      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type.kind() == CelKind.STRUCT) {
       return ctx.mkAnd(
@@ -1373,6 +1412,12 @@ private Optional<Object> toCacheKey(CelExpr expr) {
       case CONSTANT:
         return Optional.of(expr.constant());
       case LIST:
+        if (!expr.list().optionalIndices().isEmpty()) {
+          // Do not cache lists with optional elements. Optional elements conditionally alter
+          // sequence length and presence via ITE branches at runtime; caching would collide
+          // [1, 2] with [?1, 2] and freeze conditional evaluations to a static reference.
+          return Optional.empty();
+        }
         ImmutableList.Builder<Object> builder = ImmutableList.builder();
         for (CelExpr elem : expr.list().elements()) {
           Optional<Object> elemKey = toCacheKey(elem);