From 3c5d875116c7dbc9b8f3dd9923bdf5d72fc07ee5 Mon Sep 17 00:00:00 2001
From: Sean Huh <sokwhan@google.com>
Date: Fri, 23 Oct 2026 11:28:24 -0700
Subject: [PATCH] Cover verifier behavior that no test exercised

PiperOrigin-RevId: 1005740706
---
 .../java/dev/cel/verifier/CelZ3Exprs.java     |  2 ++
 .../verifier/CelPolicyVerifierImplTest.java   | 25 +++++++++++++++++++
 .../cel/verifier/CelVerifierZ3ImplTest.java   | 11 ++++++++
 3 files changed, 38 insertions(+)

diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
index b2b4d86dd..de0460e3a 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
@@ -52,6 +52,7 @@ public static BoolExpr mkOrFlattened(Context ctx, List<BoolExpr> args) {
         filteredArgs.add(arg);
       }
     }
+    // Performance only: both shortcuts are equivalent to the mkOr below.
     if (filteredArgs.isEmpty()) {
       return ctx.mkFalse();
     }
@@ -82,6 +83,7 @@ public static BoolExpr mkAndFlattened(Context ctx, List<BoolExpr> args) {
         filteredArgs.add(arg);
       }
     }
+    // Performance only: both shortcuts are equivalent to the mkAnd below.
     if (filteredArgs.isEmpty()) {
       return ctx.mkTrue();
     }
diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
index 5a9eaea02..41af9ae8c 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
@@ -499,6 +499,31 @@ public void verifyInvariants_verificationVariablesAndMultiClauseLists_verified()
     assertThat(results).containsExactly("ergonomic_inv", CelVerificationResult.verified());
   }
 
+  @Test
+  public void verifyInvariants_literalListVariableBeyondUnrollLimit_verified() throws Exception {
+    String policySource =
+        "name: literal_list_policy\n" //
+            + "rule:\n" //
+            + "  variables:\n" //
+            + "    - xs: '[1, 2, 3, 4, 5, 6]'\n" //
+            + "  match:\n" //
+            + "    - output: 'true'\n" //
+            + "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: all_positive\n" //
+            + "      assert: variables.xs.all(x, x > 0)";
+    CelPolicy policy = PARSER.parse(policySource);
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                POLICY_COMPILER,
+                CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(5).build())
+            .build();
+
+    ImmutableMap<String, CelVerificationResult> results = verifier.verifyInvariants(policy);
+
+    assertThat(results).containsExactly("all_positive", CelVerificationResult.verified());
+  }
+
   @Test
   public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws Exception {
     Cel extendedCel =
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
index 217b2168e..f8c747452 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -742,6 +742,9 @@ private enum IsAlwaysTrueTestCase {
     OPTIONAL_VALUE_VAR("optional.of(x).value() == x"),
     OPTIONAL_HAS_VALUE_VAR("optional.of(x).hasValue()"),
     OPTIONAL_VAR_HAS_VALUE_IMPLIES_INT("opt_var.hasValue() ? type(opt_var.value()) == int : true"),
+    OPTIONAL_LIST_INDEX("size(int_list) > 0 ? int_list[?0].value() == int_list[0] : true"),
+    OPTIONAL_MAP_INDEX(
+        "'a' in string_int_map ? string_int_map[?'a'].value() == string_int_map['a'] : true"),
 
     IEEE_754_PROTO_NEG_ZERO_NEQ(
         "TestAllTypes{single_double: -0.0} != TestAllTypes{single_double: 0.0}"),
@@ -978,6 +981,7 @@ private enum IsAlwaysTrueTestCase {
         "size(int_list) > 15 ? type(int_list[dyn(15)]) == int : true"),
     MAP_INDEX_TYPE_CONSTRAINT(
         "'key' in string_int_map ? type(string_int_map['key']) == int : true"),
+    FIELD_SELECTION_TYPE_CONSTRAINT("type(test_all_types.single_int64) == int"),
     LITERAL_LIST_INDEX("[1, 2][0] == 1"),
     NESTED_LIST_VARIABLES_EQUALITY(
         "nested_list == [[1]] && nested_list_2 == [[1]] ? nested_list == nested_list_2 : true"),
@@ -1045,6 +1049,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown(
             "x == x",
             "[x] == [x]",
             "{1: x} == {1: x}",
+            "size(int_list) == 1 ? int_list.all(i, x == x) : true",
           })
           String expression)
       throws Exception {
@@ -1569,6 +1574,12 @@ private enum IsAlwaysTrueViolationTestCase {
         "[true, 1/0].exists(x, x) == true",
         "Condition is not always true\\.",
         "\\(The expression fails unconditionally, regardless of input state\\)"),
+    // The non-negative element can't make the step false, so only an error at 0 violates it.
+    DYNAMIC_LIST_ALL_STEP_ERROR_PROPAGATES(
+        "size(int_list) == 1 && int_list[0] >= 0 ? int_list.all(x, 10 / x >= 0) : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "int_list = \\[0\\]"),
     DYNAMIC_STRING_MACRO_TYPE_MISMATCH(
         "unknown_var == 1 ? !(unknown_var.contains('a') == true || unknown_var.contains('a') =="
             + " false) : true",