Cover verifier behavior that no test exercised

PiperOrigin-RevId: 1004364292

Author: l46kok

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();
     }

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 =

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",