cel-expr · copybara-service · Aug 5, 2026 · Aug 5, 2026
diff --git a/verifier/BUILD.bazel b/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 = [],

diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/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",

diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java b/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) {

diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
@@ -1228,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) {
@@ -1257,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);
@@ -1351,7 +1351,10 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
         BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
 
         Expr mapVal = ctx.mkSelect(mapValues, key);
-        BoolExpr valNotError = ctx.mkNot(typeSystem.isError(mapVal));
+        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)));
       }
@@ -1409,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);

diff --git a/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java b/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java
@@ -0,0 +1,105 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.auto.value.AutoValue;
+import com.google.common.primitives.UnsignedLong;
+import dev.cel.common.annotations.Internal;
+import java.util.Optional;
+
+/**
+ * Utility for computing matching integer and unsigned integer ranges for IEEE-754 double-precision
+ * floating-point constants in Z3 verification.
+ */
+@Internal
+public final class CelNumericBounds {
+
+  /** Minimum representable signed 64-bit integer string. */
+  public static final String MIN_INT64 = "-9223372036854775808";
+
+  /** Maximum representable signed 64-bit integer string. */
+  public static final String MAX_INT64 = "9223372036854775807";
+
+  /** Maximum representable unsigned 64-bit integer string. */
+  public static final String MAX_UINT64 = "18446744073709551615";
+
+  private static final double TWO_TO_63 = Math.scalb(1.0, 63);
+  private static final double TWO_TO_64 = Math.scalb(1.0, 64);
+
+  @AutoValue
+  abstract static class IntRange {
+    abstract long min();
+
+    abstract long max();
+
+    static IntRange of(long min, long max) {
+      return new AutoValue_CelNumericBounds_IntRange(min, max);
+    }
+  }
+
+  @AutoValue
+  abstract static class UintRange {
+    abstract String min();
+
+    abstract String max();
+
+    static UintRange of(String min, String max) {
+      return new AutoValue_CelNumericBounds_UintRange(min, max);
+    }
+  }
+
+  private static boolean isMathematicalInteger(double vDouble) {
+    return Double.isFinite(vDouble) && vDouble == Math.rint(vDouble);
+  }
+
+  static Optional<IntRange> getMatchingIntRange(double vDouble) {
+    if (!isMathematicalInteger(vDouble) || vDouble < -TWO_TO_63 || vDouble > TWO_TO_63) {
+      return Optional.empty();
+    }
+    long minL = (long) vDouble;
+    while (minL > Long.MIN_VALUE && (double) (minL - 1) == vDouble) {
+      minL--;
+    }
+    long maxL = (long) vDouble;
+    while (maxL < Long.MAX_VALUE && (double) (maxL + 1) == vDouble) {
+      maxL++;
+    }
+    return Optional.of(IntRange.of(minL, maxL));
+  }
+
+  static Optional<UintRange> getMatchingUintRange(double vDouble) {
+    if (!isMathematicalInteger(vDouble) || vDouble < 0 || vDouble > TWO_TO_64) {
+      return Optional.empty();
+    }
+    // XOR with Long.MIN_VALUE (0x8000000000000000L) flips bit 63 to 1, encoding unsigned values
+    // >= 2^63 into Java's two's-complement signed long representation.
+    long uBits =
+        vDouble < TWO_TO_63 ? (long) vDouble : (long) (vDouble - TWO_TO_63) ^ Long.MIN_VALUE;
+    UnsignedLong uVal = UnsignedLong.fromLongBits(uBits);
+    UnsignedLong minU = uVal;
+    while (!minU.equals(UnsignedLong.ZERO)
+        && minU.minus(UnsignedLong.ONE).doubleValue() == vDouble) {
+      minU = minU.minus(UnsignedLong.ONE);
+    }
+    UnsignedLong maxU = uVal;
+    while (!maxU.equals(UnsignedLong.MAX_VALUE)
+        && maxU.plus(UnsignedLong.ONE).doubleValue() == vDouble) {
+      maxU = maxU.plus(UnsignedLong.ONE);
+    }
+    return Optional.of(UintRange.of(minU.toString(), maxU.toString()));
+  }
+
+  private CelNumericBounds() {}
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
@@ -24,14 +24,17 @@
 import com.microsoft.z3.Model;
 import com.microsoft.z3.RatNum;
 import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Set;
 import org.jspecify.annotations.Nullable;
 
 /** Generates human-readable counterexample strings from Z3 models. */
 @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
 final class CelZ3CounterexampleGenerator {
 
-  private static final int MAX_LIST_ELEMENTS_TO_PRINT = 15;
+  private static final int MAX_ELEMENTS_TO_PRINT = 15;
 
   private CelZ3CounterexampleGenerator() {}
 
@@ -158,8 +161,10 @@ private static String reconstructList(
             model,
             ctx.mkLength(typeSystem.getSeq(listRef)),
             String.format("Z3 failed to evaluate length for list %s", listRef));
-    int length = ((IntNum) lenExpr).getInt();
-    int printLimit = Math.min(length, MAX_LIST_ELEMENTS_TO_PRINT);
+    Preconditions.checkState(
+        lenExpr instanceof IntNum, "Expected IntNum length for list %s, got %s", listRef, lenExpr);
+    long length = ((IntNum) lenExpr).getInt64();
+    int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT);
     List<String> elements = new ArrayList<>();
     for (int i = 0; i < printLimit; i++) {
       Expr<?> elem =
@@ -179,36 +184,33 @@ private static String reconstructList(
 
   private static String reconstructMap(
       Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
-    List<Expr<?>> keys = new ArrayList<>();
     Expr<?> lenExpr =
         evaluateStrict(
             model,
             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);
-        }
-      }
-    }
+    Preconditions.checkState(
+        lenExpr instanceof IntNum, "Expected IntNum length for map %s, got %s", mapRef, lenExpr);
 
+    long length = ((IntNum) lenExpr).getInt64();
+    int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT);
     List<String> entries = new ArrayList<>();
-    for (Expr<?> key : keys) {
+    Set<Expr<?>> seenKeys = new HashSet<>();
+    for (int i = 0; i < printLimit; i++) {
+      Expr<?> key =
+          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 (!seenKeys.add(key)) {
+        continue;
+      }
       Expr<?> presence =
           evaluateStrict(
               model,
               ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key),
               String.format(
                   "Z3 failed to evaluate map presence for key %s in map %s", key, mapRef));
-
       if (presence.isTrue()) {
         Expr<?> value =
             evaluateStrict(
@@ -221,6 +223,9 @@ private static String reconstructMap(
                 + formatExpr(ctx, typeSystem, model, value));
       }
     }
+    if (length > printLimit) {
+      entries.add("... (" + (length - printLimit) + " more entries)");
+    }
 
     return "{" + String.join(", ", entries) + "}";
   }
@@ -241,7 +246,7 @@ private static String reconstructMessage(
 
     String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");
 
-    List<Expr<?>> keys = new ArrayList<>();
+    Set<Expr<?>> keys = new LinkedHashSet<>();
     extractKeys(presenceArray, keys);
 
     List<String> entries = new ArrayList<>();
@@ -268,7 +273,7 @@ private static String reconstructMessage(
     return typeName + "{" + String.join(", ", entries) + "}";
   }
 
-  private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
+  private static void extractKeys(Expr<?> arrayExpr, Set<Expr<?>> keys) {
     int iterations = 0;
     while (true) {
       if (++iterations > 100_000) {
@@ -284,9 +289,7 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
         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]);
-        }
+        keys.add(args[1]);
         arrayExpr = args[0];
         continue;
       }