Support cross-type numeric equality in verifier

PiperOrigin-RevId: 949058814

Author: l46kok

verifier/README.md

@@ -229,16 +229,6 @@ public class PolicyVerifierExample {
 
 ### Limitations
 
-*   **Cross-Type Numeric Comparisons:**
-    *   **Equality (`==`, `!=`):** Equality comparisons between different
-        numeric types (e.g., `int` vs `double` or `uint` vs `double`) are
-        currently not supported and will evaluate to `false` during
-        verification, even if they have the same mathematical value (e.g.,
-        `dyn(1) == dyn(1.0)` is false). Note that `int` vs `uint` equality *is*
-        supported.
-    *   **Relational Operators (`<`, `>`, `<=`, `>=`):** Cross-type relational
-        comparisons are fully supported mathematically across all numeric
-        combinations (`int`, `uint`, and `double`).
 *   **Unsupported Standard Functions (Uninterpreted Functions):** Not all
     CEL standard library functions have SMT axioms defined yet. Unsupported
     functions are treated as *uninterpreted functions* by Z3 (the solver

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

@@ -47,6 +47,7 @@
 import dev.cel.common.types.TypeType;
 import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
@@ -564,7 +565,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a
     typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast));
 
     return TranslatedValue.propagateStrict(
-        ctx, typeSystem, fieldAccess, celExpr, Arrays.asList(operandTv));
+        ctx, typeSystem, fieldAccess, celExpr, Collections.singletonList(operandTv));
   }
 
   private TranslatedValue translateBlock(