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/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/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,16 +85,11 @@ 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);
@@ -125,9 +122,11 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c
         }
         break;
       case STRUCT:
+        context.hasher.putInt(expr.struct().messageName().length());
         context.hasher.putString(expr.struct().messageName(), UTF_8);
         context.hasher.putInt(expr.struct().entries().size());
         for (CelExpr.CelStruct.Entry entry : expr.struct().entries()) {
+          context.hasher.putInt(entry.fieldKey().length());
           context.hasher.putString(entry.fieldKey(), UTF_8);
           context.hasher.putBoolean(entry.optionalEntry());
           hashAst(entry.value(), scope, context);
@@ -210,6 +209,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,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);
             });
   }
 
@@ -875,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);
 
@@ -891,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));
       }
     }
 
@@ -913,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(
@@ -1245,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);
@@ -1287,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);
@@ -1305,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(
@@ -1371,6 +1420,9 @@ private Optional<Object> toCacheKey(CelExpr expr) {
       case CONSTANT:
         return Optional.of(expr.constant());
       case LIST:
+        if (!expr.list().optionalIndices().isEmpty()) {
+          return Optional.empty(); // Safely skip caching lists with optional elements
+        }
         ImmutableList.Builder<Object> builder = ImmutableList.builder();
         for (CelExpr elem : expr.list().elements()) {
           Optional<Object> elemKey = toCacheKey(elem);

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: