copybara-service · Oct 29, 2026 · Oct 29, 2026
diff --git a/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java
@@ -476,7 +476,11 @@ private static int compareIdent(String name1, String name2, CanonicalizationScop
       if (bIdx2 >= 0) {
         return 1; // Free variable comes after bound variable
       }
-      return name1.compareTo(name2);
+      return stripLeadingDot(name1).compareTo(stripLeadingDot(name2));
+    }
+
+    private static String stripLeadingDot(String name) {
+      return name.startsWith(".") ? name.substring(1) : name;
     }
 
     private int compareSelect(CelMutableSelect s1, CelMutableSelect s2) {

diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java
@@ -21,8 +21,10 @@
 import com.google.common.hash.HashFunction;
 import com.google.common.hash.Hasher;
 import com.google.common.hash.Hashing;
+import dev.cel.common.CelAbstractSyntaxTree;
 import dev.cel.common.ast.CelConstant;
 import dev.cel.common.ast.CelExpr;
+import dev.cel.common.ast.CelReference;
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
@@ -65,14 +67,21 @@ static AlphaSignature create(long staticHash, ImmutableList<CelExpr> freeVariabl
     }
   }
 
-  static AlphaSignature computeSignature(CelExpr expr) {
-    HasherContext context = new HasherContext(HASH_FUNCTION);
+  static AlphaSignature computeSignature(CelExpr expr, CelAbstractSyntaxTree ast) {
+    HasherContext context = new HasherContext(HASH_FUNCTION, ast);
     hashAst(expr, /* scope= */ null, context);
     return AlphaSignature.create(
         context.hasher.hash().asLong(), ImmutableList.copyOf(context.freeVars));
   }
 
   private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext context) {
+    CelConstant refValue =
+        context.ast.getReference(expr.id()).flatMap(CelReference::value).orElse(null);
+    if (refValue != null) {
+      context.hasher.putString(CelExpr.ExprKind.Kind.CONSTANT.name(), UTF_8);
+      hashConstant(refValue, context);
+      return;
+    }
     context.hasher.putString(expr.exprKind().getKind().name(), UTF_8);
     switch (expr.exprKind().getKind()) {
       case CONSTANT:
@@ -85,11 +94,12 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c
           context.hasher.putByte((byte) 0); // 0 = bound
           context.hasher.putInt(bIdx);
         } else {
-          Integer fIdx = context.freeVarIndices.get(name);
+          String freeName = name.startsWith(".") ? name.substring(1) : name;
+          Integer fIdx = context.freeVarIndices.get(freeName);
           if (fIdx == null) {
             context.freeVars.add(expr);
             fIdx = context.freeVars.size() - 1;
-            context.freeVarIndices.put(name, fIdx);
+            context.freeVarIndices.put(freeName, fIdx);
           }
           context.hasher.putByte((byte) 1); // 1 = free
           context.hasher.putInt(fIdx);
@@ -205,11 +215,13 @@ private static void hashConstant(CelConstant constant, HasherContext context) {
 
   private static final class HasherContext {
     final Hasher hasher;
+    final CelAbstractSyntaxTree ast;
     final Map<String, Integer> freeVarIndices = new HashMap<>();
     final List<CelExpr> freeVars = new ArrayList<>();
 
-    HasherContext(HashFunction hashFunction) {
+    HasherContext(HashFunction hashFunction, CelAbstractSyntaxTree ast) {
       this.hasher = hashFunction.newHasher();
+      this.ast = ast;
     }
   }
 

diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
@@ -33,6 +33,7 @@
 import dev.cel.common.ast.CelExpr;
 import dev.cel.common.ast.CelExpr.CelList;
 import dev.cel.common.ast.CelExpr.ExprKind;
+import dev.cel.common.ast.CelReference;
 import dev.cel.common.types.CelKind;
 import dev.cel.common.types.CelType;
 import dev.cel.common.types.CelTypeProvider;
@@ -223,6 +224,10 @@ private TranslatedValue translateConstant(CelExpr celExpr) {
   private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree ast) {
     CelExpr.CelIdent ident = celExpr.ident();
     long exprId = celExpr.id();
+    CelConstant refValue = ast.getReference(exprId).flatMap(CelReference::value).orElse(null);
+    if (refValue != null) {
+      return translateConstant(CelExpr.ofConstant(exprId, refValue));
+    }
     String name = ident.name();
     CelType type = ast.getTypeOrThrow(exprId);
     if (type instanceof TypeType) {
@@ -244,7 +249,7 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as
               context.addConstraint(ctx.mkNot(typeSystem.isError(v)));
 
               BoolExpr constraint = typeConstraintGenerator.createTypeConstraint(v, exprId, ast);
-              if (unknownIdentifiers.contains(name)) {
+              if (unknownIdentifiers.contains(n)) {
                 context.addConstraint(ctx.mkOr(typeSystem.isUnknown(v), constraint));
               } else {
                 context.addConstraint(ctx.mkNot(typeSystem.isUnknown(v)));

diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
@@ -508,7 +508,7 @@ private IterationElement(Expr<?> keyOrIndex, Expr<?> value) {
   }
 
   private Expr<?> mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) {
-    CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr);
+    CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr, ast);
 
     ImmutableList.Builder<Expr<?>> smtArgs = ImmutableList.builder();
     for (CelExpr freeVar : sig.freeVariables()) {

diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
@@ -42,6 +42,7 @@ final class CelZ3TranslationContext {
   private final Map<Expr<?>, CelType> inputVariableTypes;
   private final List<BoolExpr> truncationConditions;
   private final Map<String, TranslatedValue> symbolTable;
+  private final Map<String, TranslatedValue> localScope;
 
   Context ctx() {
     return ctx;
@@ -108,28 +109,32 @@ BoolExpr hasTruncation() {
   }
 
   void bindSymbol(String name, TranslatedValue value) {
-    symbolTable.put(name, value);
+    localScope.put(name, value);
   }
 
   Optional<TranslatedValue> lookupSymbol(String name) {
-    return Optional.ofNullable(symbolTable.get(name));
+    return Optional.ofNullable(localScope.get(name));
   }
 
   TranslatedValue computeSymbolIfAbsent(
-      String name, Function<String, TranslatedValue> mappingFunction) {
-    return symbolTable.computeIfAbsent(name, mappingFunction);
+      String rawName, Function<String, TranslatedValue> mappingFunction) {
+    if (!rawName.startsWith(".") && localScope.containsKey(rawName)) {
+      return localScope.get(rawName);
+    }
+    return symbolTable.computeIfAbsent(
+        rawName.startsWith(".") ? rawName.substring(1) : rawName, mappingFunction);
   }
 
   /** Binds {@code varName} to {@code value} while running {@code action}, then restores it. */
   <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
-    TranslatedValue prev = symbolTable.put(varName, value);
+    TranslatedValue prev = localScope.put(varName, value);
     try {
       return action.get();
     } finally {
       if (prev != null) {
-        symbolTable.put(varName, prev);
+        localScope.put(varName, prev);
       } else {
-        symbolTable.remove(varName);
+        localScope.remove(varName);
       }
     }
   }
@@ -144,5 +149,6 @@ <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
     this.inputVariableTypes = new LinkedHashMap<>();
     this.truncationConditions = new ArrayList<>();
     this.symbolTable = new HashMap<>();
+    this.localScope = new HashMap<>();
   }
 }
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -36,6 +36,7 @@
 import dev.cel.common.CelFunctionDecl;
 import dev.cel.common.CelOptions;
 import dev.cel.common.CelOverloadDecl;
+import dev.cel.common.CelVarDecl;
 import dev.cel.common.Operator;
 import dev.cel.common.ast.CelConstant;
 import dev.cel.common.ast.CelExpr;
@@ -613,6 +614,8 @@ private enum IsUnsatisfiableTestCase {
         "size(string_int_map) == 6 && dyn(1) in string_int_map"),
     LIST_INDEX_DYN_STRING_KEY("int_list[dyn('0')] == 1"),
     NON_BOOL_LOGICAL_OPERAND("dyn(1) && true"),
+    ENUM_CONSTANTS_DISTINCT("TestAllTypes.NestedEnum.FOO == TestAllTypes.NestedEnum.BAR"),
+    LEADING_DOT_GLOBAL_DISAMBIGUATION_CONTRADICTION("x == 5 && [1, 2].all(x, x > .x)"),
     ;
 
     private final String expr;
@@ -1114,6 +1117,9 @@ private enum IsAlwaysTrueTestCase {
         "size(string_int_map) > 0 && size(string_int_map) <= 5 ?"
             + " string_int_map.all(k, v, v >= -9223372036854775808 &&"
             + " v <= 9223372036854775807) : true"),
+    ENUM_CONSTANT_EQUALITY("TestAllTypes.NestedEnum.BAR == 1"),
+    ENUM_CONSTANT_INEQUALITY("TestAllTypes.NestedEnum.FOO != TestAllTypes.NestedEnum.BAR"),
+    LEADING_DOT_GLOBAL_DISAMBIGUATION_IN_COMPREHENSION("x == 0 ? [1, 2].all(x, x > .x) : true"),
     ;
 
     final String expr;
@@ -2452,7 +2458,19 @@ private enum EquivalenceTestCase {
             + " && z_key == 'foo')"),
     CANONICALIZE_CEL_BIND_ALPHA_RENAME_PREDICATE_ORDER(
         "cel.bind(a, x + 10, cel.bind(b, x + 20, 2 == b && 1 == a))",
-        "cel.bind(c, x + 10, cel.bind(d, x + 20, c == 1 && d == 2))");
+        "cel.bind(c, x + 10, cel.bind(d, x + 20, c == 1 && d == 2))"),
+    ENUM_FIELD_COMPARE_VS_INT_LITERAL(
+        "test_all_types.single_nested_enum == TestAllTypes.NestedEnum.BAR",
+        "test_all_types.single_nested_enum == 1"),
+    LEADING_DOT_GLOBAL_DISAMBIGUATION("[1, 2].all(x, x > .x) && x == 0", "x == 0"),
+    TRUNCATED_COMPREHENSION_ENUM_VS_INT_LITERAL(
+        "dyn_list.all(e, e == TestAllTypes.NestedEnum.BAR)", "dyn_list.all(e, e == 1)"),
+    TRUNCATED_COMPREHENSION_LEADING_DOT_VS_UNSHADOWED(
+        "int_list.all(y, (.y == x) && y > 0 && [1].all(x, .x > 0 && .y > 0))",
+        "int_list.all(z, (y == x) && z > 0 && [1].all(w, x > 0 && y > 0))"),
+    TRUNCATED_COMPREHENSION_SHADOWED_CEL_BIND(
+        "cel.bind(x, x + 1, int_list.all(e, e > x && a))",
+        "cel.bind(x, x + 1, int_list.all(v, a && v > x))");
 
     private final String exprA;
     private final String exprB;
@@ -3593,8 +3611,8 @@ private enum EquivalenceZeroUnrollLimitTestCase {
     DIFFERENT_CONSTANTS("dyn_list.exists(i, i == 1)", "dyn_list.exists(i, i == 2)"),
     DIFFERENT_VARIABLES("dyn_list.exists(i, i == x)", "dyn_list.exists(i, i == y)");
 
-    final String exprA;
-    final String exprB;
+    private final String exprA;
+    private final String exprB;
 
     EquivalenceZeroUnrollLimitTestCase(String exprA, String exprB) {
       this.exprA = exprA;
@@ -3607,9 +3625,9 @@ public void verifyEquivalence_zeroUnrollLimit_returnsInconclusive(
       @TestParameter EquivalenceZeroUnrollLimitTestCase testCase) throws Exception {
     CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst();
     CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst();
-
     CelVerifier verifier =
         CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build();
+
     CelVerificationResult result = verifier.verifyEquivalence(astA, astB);
 
     assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
@@ -3632,8 +3650,8 @@ private enum EquivalenceZeroUnrollLimitVerifiedTestCase {
         "string_int_map.exists(z_key, a_val, int_list.all(idx, elem, idx == 0 && elem == a_val)"
             + " && z_key == 'foo')");
 
-    final String exprA;
-    final String exprB;
+    private final String exprA;
+    private final String exprB;
 
     EquivalenceZeroUnrollLimitVerifiedTestCase(String exprA, String exprB) {
       this.exprA = exprA;
@@ -3646,9 +3664,9 @@ public void verifyEquivalence_zeroUnrollLimit_twoVarComprehensions_returnsVerifi
       @TestParameter EquivalenceZeroUnrollLimitVerifiedTestCase testCase) throws Exception {
     CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst();
     CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst();
-
     CelVerifier verifier =
         CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build();
+
     CelVerificationResult result = verifier.verifyEquivalence(astA, astB);
 
     assertWithMessage(result.message())
@@ -3673,7 +3691,6 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive()
                         exprFactory.newBoolLiteral(true),
                         /* step= */ exprFactory.newIdentifier("x"),
                         /* result= */ exprFactory.newIdentifier("x"))));
-
     CelMacro macro2 =
         CelMacro.newReceiverMacro(
             "my_macro_2",
@@ -3689,18 +3706,16 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive()
                         exprFactory.newBoolLiteral(true),
                         /* step= */ exprFactory.newIdentifier("y"),
                         /* result= */ exprFactory.newIdentifier("x"))));
-
     Cel customCel =
         CelFactory.plannerCelBuilder()
             .addVar("dyn_list", ListType.create(SimpleType.DYN))
             .addMacros(macro1, macro2)
             .build();
-
     CelAbstractSyntaxTree astA = customCel.compile("dyn_list.my_macro_1(true)").getAst();
     CelAbstractSyntaxTree astB = customCel.compile("dyn_list.my_macro_2(true)").getAst();
-
     CelVerifier verifier =
         CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build();
+
     CelVerificationResult result = verifier.verifyEquivalence(astA, astB);
 
     assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
@@ -3730,22 +3745,20 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus
                                 exprFactory.newIntLiteral(0L)),
                             exprFactory.newIntLiteral(0L),
                             exprFactory.newIdentifier("x")))));
-
     Cel customCel =
         CelFactory.plannerCelBuilder()
             .addVar("dyn_list", ListType.create(SimpleType.DYN))
             .addVar("x", SimpleType.INT)
             .addMacros(macro)
             .addCompilerLibraries(CelExtensions.bindings())
             .build();
-
     CelAbstractSyntaxTree astA =
         customCel.compile("cel.bind(x, 10, dyn_list.my_macro(1))").getAst();
     CelAbstractSyntaxTree astB =
         customCel.compile("cel.bind(x, 20, dyn_list.my_macro(1))").getAst();
-
     CelVerifier verifier =
         CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build();
+
     CelVerificationResult result = verifier.verifyEquivalence(astA, astB);
 
     assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
@@ -3760,10 +3773,8 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th
             .addVar("d3", SimpleType.DOUBLE)
             .addVar("d4", SimpleType.DOUBLE)
             .build();
-
     CelVerifier timeoutVerifier =
         CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build();
-
     CelAbstractSyntaxTree astA =
         customCel
             .compile(
@@ -3775,6 +3786,7 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th
     CelVerificationException e =
         assertThrows(
             CelVerificationException.class, () -> timeoutVerifier.verifyEquivalence(astA, astB));
+
     assertThat(e).hasMessageThat().containsMatch("timeout|canceled");
   }
 
@@ -3783,9 +3795,9 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th
     CelAbstractSyntaxTree assumeAst =
         CEL.compile("size(int_list) <= 2 && int_list[0] > 0 && int_list[1] > 0").getAst();
     CelAbstractSyntaxTree assertAst = CEL.compile("int_list.all(x, x > 0)").getAst();
-
     CelVerifier verifier =
         CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build();
+
     CelVerificationResult result =
         ((CelVerifierZ3Impl) verifier)
             .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication");
@@ -3801,12 +3813,38 @@ public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() t
     CelAbstractSyntaxTree assumeAst = CEL.compile("d != d").getAst();
     // Assertion: x < d is false when d is NaN
     CelAbstractSyntaxTree assertAst = CEL.compile("!(x < d)").getAst();
-
     CelVerifier verifier = CelVerifierFactory.newVerifier(CEL).build();
+
     CelVerificationResult result =
         ((CelVerifierZ3Impl) verifier)
             .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication");
+
     assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
   }
+
+  @Test
+  public void isAlwaysTrue_constantVarDecl_verified() throws Exception {
+    Cel celWithConstVar =
+        CelFactory.plannerCelBuilder()
+            .setStandardMacros(CelStandardMacro.STANDARD_MACROS)
+            .addVarDeclarations(
+                CelVarDecl.newBuilder()
+                    .setName("CONST_INT")
+                    .setType(SimpleType.INT)
+                    .setConstant(CelConstant.ofValue(42L))
+                    .build())
+            .build();
+    CelVerifier verifier = CelVerifierFactory.newVerifier(celWithConstVar).build();
+    CelAbstractSyntaxTree ast =
+        celWithConstVar
+            .compile("CONST_INT == 42 && [1, 2].all(x, .CONST_INT == 42 && x > 0)")
+            .getAst();
+
+    CelVerificationResult result = verifier.isAlwaysTrue(ast);
+
+    assertWithMessage(result.message())
+        .that(result.status())
+        .isEqualTo(VerificationStatus.VERIFIED);
+  }
 }