Deduplicate Z3 list references by sequence term and add policy conformance equivalence tests

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

@@ -76,7 +76,7 @@ final class CelAstToZ3Translator {
   private final CelZ3ComprehensionTranslator comprehensionTranslator;
   private final CelZ3StructTranslator structTranslator;
   private final ImmutableSet<String> unknownIdentifiers;
-  private final Map<Object, Expr<?>> listLiteralCache;
+  private final Map<SeqExpr<?>, Expr<?>> listLiteralCache;
 
   /**
    * Returns a set of Z3 boolean expressions representing type constraints for the translated AST.
@@ -268,51 +268,49 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as
 
   private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast) {
     CelList createList = celExpr.list();
-    Optional<Object> cacheKey = toCacheKey(celExpr);
     List<TranslatedValue> elementsTv = new ArrayList<>();
-    Expr<?> listRef = cacheKey.map(listLiteralCache::get).orElse(null);
-
-    // Cache list literals containing only constants. If the same list literal appears multiple
-    // times (e.g., in equality checks like `[1, 2] == [1, 2]`), caching allows us to reuse the
-    // same Z3 constant. This avoids expensive sequence equality reasoning in Z3 by reducing the
-    // check to a trivial identity check (e.g., `list_ref_0 == list_ref_0`).
-    if (listRef == null) {
-      SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));
-      List<Expr<?>> values = new ArrayList<>();
-      ImmutableList<Integer> optionalIndices = createList.optionalIndices();
-      ImmutableList<CelExpr> elements = createList.elements();
-      for (int i = 0; i < elements.size(); i++) {
-        CelExpr element = elements.get(i);
-        TranslatedValue elem = translateExpr(element, ast);
-
-        if (optionalIndices.contains(i)) {
-          Expr<?> checkedValue =
-              typeSystem.withRuntimeError(
-                  elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr())));
-          elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());
-
-          Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
-          Expr<?> value = typeSystem.getOptionalValue(optRef);
-          seq =
-              (SeqExpr)
-                  ctx.mkITE(
-                      typeSystem.optHasValue(optRef),
-                      typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)),
-                      seq);
-          values.add(value);
-        } else {
-          seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
-          values.add(elem.z3Expr());
-        }
-        elementsTv.add(elem);
+    SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));
+    List<Expr<?>> values = new ArrayList<>();
+    ImmutableList<Integer> optionalIndices = createList.optionalIndices();
+    ImmutableList<CelExpr> elements = createList.elements();
+    for (int i = 0; i < elements.size(); i++) {
+      CelExpr element = elements.get(i);
+      TranslatedValue elem = translateExpr(element, ast);
+
+      if (optionalIndices.contains(i)) {
+        Expr<?> checkedValue =
+            typeSystem.withRuntimeError(
+                elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr())));
+        elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());
+
+        Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
+        Expr<?> value = typeSystem.getOptionalValue(optRef);
+        seq =
+            (SeqExpr)
+                ctx.mkITE(
+                    typeSystem.optHasValue(optRef),
+                    typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)),
+                    seq);
+        values.add(value);
+      } else {
+        seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
+        values.add(elem.z3Expr());
       }
-      listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX);
-      context.addConstraint(ctx.mkEq(typeSystem.getSeq(listRef), seq));
-      propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values);
-      Expr<?> finalListRef = listRef;
-      cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef));
+      elementsTv.add(elem);
     }
 
+    // Reuse the same Z3 ListRef whenever two list constructions yield the exact same sequence term
+    // (e.g., identical constant lists or identical unrolled map/filter step lists across ASTs).
+    Expr<?> listRef =
+        listLiteralCache.computeIfAbsent(
+            seq,
+            s -> {
+              Expr<?> ref = typeSystem.mkListRefConst(LIST_REF_PREFIX);
+              context.addConstraint(ctx.mkEq(typeSystem.getSeq(ref), s));
+              propagateTruncatedTypeConstraint(typeSystem.wrapList(ref), values);
+              return ref;
+            });
+
     Expr<?> result = typeSystem.wrapList(listRef);
     return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
   }
@@ -481,31 +479,6 @@ private static boolean mayEmbedArgs(String functionName, CelType resultType) {
         && !functionName.equals(Operator.CONDITIONAL.getFunction());
   }
 
-  private Optional<Object> toCacheKey(CelExpr expr) {
-    switch (expr.exprKind().getKind()) {
-      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);
-          if (!elemKey.isPresent()) {
-            return Optional.empty(); // Contains non-constants
-          }
-          builder.add(elemKey.get());
-        }
-        return Optional.of(builder.build());
-      default:
-        return Optional.empty();
-    }
-  }
-
   CelAstToZ3Translator(
       Context ctx,
       int comprehensionUnrollLimit,

verifier/src/test/java/dev/cel/verifier/BUILD.bazel

@@ -14,9 +14,11 @@ java_library(
     compatible_with = [],
     data = [
         "//testing:policy_test_resources",
+        "@cel_policy//conformance:testdata",
     ],
     deps = [
         "//bundle:cel",
+        "//bundle:environment_yaml_parser",
         "//common:cel_ast",
         "//common:compiler_common",
         "//common:container",
@@ -25,6 +27,7 @@ java_library(
         "//common:options",
         "//common/ast",
         "//common/ast:mutable_expr",
+        "//common/resources/testdata/proto3:standalone_global_enum_java_proto",
         "//common/types",
         "//common/types:message_type_provider",
         "//compiler:compiler_builder",
@@ -43,6 +46,8 @@ java_library(
         "//policy:parser",
         "//policy:parser_factory",
         "//policy:validation_exception",
+        "//policy/testing:k8s_test_tag_handler",
+        "//testing/protos:single_file_java_proto",
         "@bazel_tools//tools/java/runfiles",
         "@maven//:junit_junit",
         "@maven//:com_google_testparameterinjector_test_parameter_injector",

verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java

@@ -18,10 +18,12 @@
 import static com.google.common.truth.Truth.assertWithMessage;
 import static org.junit.Assert.assertThrows;
 
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.testing.junit.testparameterinjector.TestParameter;
 import com.google.testing.junit.testparameterinjector.TestParameterInjector;
 import dev.cel.bundle.Cel;
+import dev.cel.bundle.CelEnvironmentYamlParser;
 import dev.cel.bundle.CelFactory;
 import dev.cel.common.CelAbstractSyntaxTree;
 import dev.cel.common.CelFunctionDecl;
@@ -31,6 +33,7 @@
 import dev.cel.common.types.StructTypeReference;
 import dev.cel.expr.conformance.proto3.TestAllTypes;
 import dev.cel.extensions.CelExtensions;
+import dev.cel.extensions.CelOptionalLibrary;
 import dev.cel.optimizer.CelOptimizer;
 import dev.cel.optimizer.CelOptimizerFactory;
 import dev.cel.optimizer.optimizers.SubexpressionOptimizer;
@@ -43,6 +46,9 @@
 import dev.cel.policy.CelPolicyParser;
 import dev.cel.policy.CelPolicyParserFactory;
 import dev.cel.policy.CelPolicyValidationException;
+import dev.cel.policy.testing.K8sTagHandler;
+import dev.cel.testing.testdata.SingleFile;
+import dev.cel.testing.testdata.proto3.StandaloneGlobalEnum;
 import dev.cel.verifier.CelVerificationResult.VerificationStatus;
 import org.junit.Before;
 import org.junit.Test;
@@ -80,7 +86,7 @@ public final class CelPolicyVerifierImplTest {
   private static final CelPolicyCompiler POLICY_COMPILER =
       CelPolicyCompilerFactory.newPolicyCompiler(CEL).build();
 
-  private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier().build();
+  private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier(CEL).build();
   private static final CelPolicyVerifier VERIFIER =
       CelPolicyVerifierFactory.newVerifier(POLICY_COMPILER, AST_VERIFIER).build();
 
@@ -722,4 +728,85 @@ public void verifyInvariants_boundedSymbolWithApproximation_returnsInconclusive(
     assertThat(results).containsKey("check_approx");
     assertThat(results.get("check_approx").status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
   }
+
+  private enum ConformancePolicyTestCase {
+    AGGREGATE("aggregate"),
+    AGGREGATE_EXPLICIT_LIST_OUTPUT("aggregate_explicit_list_output"),
+    AGGREGATE_EXPLICIT_OPTIONAL_NONE("aggregate_explicit_optional_none"),
+    AGGREGATE_NESTED_EXPLICIT_LIST_DOUBLE_WRAPPING(
+        "aggregate_nested_explicit_list_double_wrapping"),
+    AGGREGATE_SHADOWED_VARIABLES("aggregate_shadowed_variables"),
+    CONTEXT_PB("context_pb"),
+    FIRST_MATCH_NESTED_AGGREGATE("first_match_nested_aggregate"),
+    K8S("k8s"),
+    LIMITS("limits"),
+    NESTED_RULE("nested_rule"),
+    NESTED_RULE2("nested_rule2"),
+    NESTED_RULE3("nested_rule3"),
+    NESTED_RULE4("nested_rule4"),
+    NESTED_RULE5("nested_rule5"),
+    NESTED_RULE6("nested_rule6"),
+    NESTED_RULE7("nested_rule7"),
+    NESTED_RULES_VARIABLE_SHADOWING("nested_rules_variable_shadowing"),
+    PB("pb"),
+    REQUIRED_LABELS("required_labels"),
+    RESTRICTED_DESTINATIONS("restricted_destinations"),
+    UNCONDITIONAL_RULES("unconditional_rules"),
+    UNNEST("unnest"),
+    VARIABLE_TYPE_PROPAGATION("variable_type_propagation");
+
+    private final String policyDir;
+
+    ConformancePolicyTestCase(String policyDir) {
+      this.policyDir = policyDir;
+    }
+  }
+
+  @Test
+  public void verifyEquivalence_conformancePolicies_unoptimizedVsOptimized(
+      @TestParameter ConformancePolicyTestCase testCase) throws Exception {
+    CelPolicyParser policyParser =
+        CelPolicyParserFactory.newYamlParserBuilder().addTagVisitor(new K8sTagHandler()).build();
+    CelOptions options =
+        CelOptions.current()
+            .populateMacroCalls(true)
+            .enableHeterogeneousNumericComparisons(true)
+            .build();
+    Cel baseCel =
+        CelFactory.plannerCelBuilder()
+            .setOptions(options)
+            .setStandardMacros(CelStandardMacro.STANDARD_MACROS)
+            .addCompilerLibraries(CelOptionalLibrary.INSTANCE, CelExtensions.bindings())
+            .addRuntimeLibraries(CelOptionalLibrary.INSTANCE)
+            .addFileTypes(StandaloneGlobalEnum.getDescriptor().getFile())
+            .addMessageTypes(TestAllTypes.getDescriptor(), SingleFile.getDescriptor())
+            .build();
+    String configYaml =
+        VerifierTestHelper.maybeLoadConformanceConfigYaml(testCase.policyDir).orElse(null);
+    Cel cel =
+        configYaml != null
+            ? CelEnvironmentYamlParser.newInstance().parse(configYaml).extend(baseCel, options)
+            : baseCel;
+    CelPolicy policy =
+        policyParser.parse(VerifierTestHelper.loadConformancePolicyYaml(testCase.policyDir));
+    CelPolicyCompiler unoptimizedCompiler = CelPolicyCompilerFactory.newPolicyCompiler(cel).build();
+    CelPolicyCompiler optimizedCompiler =
+        CelPolicyCompilerFactory.newPolicyCompiler(cel)
+            .setOptimizers(
+                ImmutableList.of(
+                    SubexpressionOptimizer.newInstance(
+                        SubexpressionOptimizerOptions.newBuilder()
+                            .populateMacroCalls(true)
+                            .build())))
+            .build();
+    CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build();
+
+    CelAbstractSyntaxTree unoptimizedAst = unoptimizedCompiler.compile(policy);
+    CelAbstractSyntaxTree optimizedAst = optimizedCompiler.compile(policy);
+    CelVerificationResult result = verifier.verifyEquivalence(unoptimizedAst, optimizedAst);
+
+    assertWithMessage(result.message())
+        .that(result.status())
+        .isEqualTo(VerificationStatus.VERIFIED);
+  }
 }

verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java

@@ -22,28 +22,42 @@
 import com.google.devtools.build.runfiles.Runfiles;
 import java.io.File;
 import java.io.IOException;
+import java.util.Optional;
 
 /** Package-private class to assist with verifier testing and runfiles resolution. */
 @AutoBazelRepository
 final class VerifierTestHelper {
 
-  private static final Runfiles runfiles = createRunfiles();
+  private static final Runfiles RUNFILES = createRunfiles();
 
   static String loadVerificationPolicyYaml(String filename) throws IOException {
-    String rlocationPath =
-        "cel_java/testing/src/test/resources/policy/verification/" + filename;
-    String resolvedPath = runfiles.rlocation(Ascii.toLowerCase(rlocationPath));
-    if (resolvedPath == null) {
-      throw new IOException("Unmapped runfile path: " + rlocationPath);
-    }
-    File file = new File(resolvedPath);
-    if (!file.exists()) {
-      throw new IOException(
-          String.format(
-              "Runfile not found on disk at '%s' (unresolved path: '%s')",
-              resolvedPath, rlocationPath));
+    return loadRunfile(
+        "cel_java/testing/src/test/resources/policy/verification/" + filename);
+  }
+
+  static String loadConformancePolicyYaml(String policyDir) throws IOException {
+    return loadRunfile(
+        String.format(
+            "cel_policy/conformance/testdata/%s/policy.yaml", policyDir));
+  }
+
+  static Optional<String> maybeLoadConformanceConfigYaml(String policyDir) throws IOException {
+    return maybeLoadRunfile(
+        String.format(
+            "cel_policy/conformance/testdata/%s/config.yaml", policyDir));
+  }
+
+  private static String loadRunfile(String rlocationPath) throws IOException {
+    return maybeLoadRunfile(rlocationPath)
+        .orElseThrow(() -> new IOException("Runfile not found: " + rlocationPath));
+  }
+
+  private static Optional<String> maybeLoadRunfile(String rlocationPath) throws IOException {
+    String resolvedPath = RUNFILES.rlocation(Ascii.toLowerCase(rlocationPath));
+    if (resolvedPath == null || !new File(resolvedPath).exists()) {
+      return Optional.empty();
     }
-    return Files.asCharSource(file, UTF_8).read();
+    return Optional.of(Files.asCharSource(new File(resolvedPath), UTF_8).read());
   }
 
   private static Runfiles createRunfiles() {