Open source the CEL formal verification framework

PiperOrigin-RevId: 945772608

Author: l46kok

.github/workflows/cross_artifact_dependencies_check.sh

@@ -22,6 +22,7 @@ TARGETS=(
   "//publish:cel_runtime"
   "//publish:cel_protobuf"
   "//publish:cel_v1alpha1"
+  "//publish:cel_verifier"
 )
 
 echo "------------------------------------------------"

MODULE.bazel

@@ -98,6 +98,7 @@ maven.install(
         "org.jspecify:jspecify:1.0.0",
         "org.threeten:threeten-extra:1.8.0",
         "org.yaml:snakeyaml:2.5",
+        "tools.aqua:z3-turnkey:4.14.1",
     ],
     repositories = [
         "https://maven.google.com",

publish/BUILD.bazel

@@ -130,6 +130,18 @@ BUNDLE_TARGETS = [
 
 CEL_MISC_TARGETS = BUNDLE_TARGETS + EXTENSION_TARGETS + OPTIMIZER_TARGETS + VALIDATOR_TARGETS + POLICY_COMPILER_TARGETS
 
+# keep sorted
+VERIFIER_TARGETS = [
+    "//verifier/src/main/java/dev/cel/verifier",
+    "//verifier/src/main/java/dev/cel/verifier:policy_verifier",
+    "//verifier/src/main/java/dev/cel/verifier:policy_verifier_factory",
+    "//verifier/src/main/java/dev/cel/verifier:policy_verifier_impl",
+    "//verifier/src/main/java/dev/cel/verifier:type_system",
+    "//verifier/src/main/java/dev/cel/verifier:verifier_factory",
+    "//verifier/src/main/java/dev/cel/verifier:z3_impl",
+    "//verifier/src/main/java/dev/cel/verifier/axioms",
+]
+
 # Excluded from the JAR as their source of truth is elsewhere
 EXCLUDED_TARGETS = [
     "@com_google_googleapis//google/api/expr/v1alpha1:expr_java_proto",
@@ -316,3 +328,24 @@ java_export(
     pom_template = ":cel_runtime_android_pom",
     exports = LITE_RUNTIME_TARGETS,
 )
+
+pom_file(
+    name = "cel_verifier_pom",
+    substitutions = {
+        "CEL_VERSION": CEL_VERSION,
+        "CEL_ARTIFACT_ID": "verifier",
+        "PACKAGE_NAME": "CEL Java Verifier",
+        "PACKAGE_DESC": "Formal verification tools for Common Expression Language for Java.",
+    },
+    targets = VERIFIER_TARGETS,
+    template_file = "pom_template.xml",
+)
+
+java_export(
+    name = "cel_verifier",
+    deploy_env = EXCLUDED_TARGETS,
+    javadocopts = JAVA_DOC_OPTIONS,
+    maven_coordinates = "dev.cel:verifier:%s" % CEL_VERSION,
+    pom_template = ":cel_verifier_pom",
+    exports = VERIFIER_TARGETS + [":cel"],
+)

verifier/BUILD.bazel

@@ -0,0 +1,41 @@
+load("@rules_java//java:defs.bzl", "java_library")
+
+package(
+    default_applicable_licenses = ["//:license"],
+    default_visibility = ["//:internal"],
+)
+
+java_library(
+    name = "verifier",
+    exports = ["//verifier/src/main/java/dev/cel/verifier"],
+)
+
+java_library(
+    name = "policy_verifier",
+    exports = ["//verifier/src/main/java/dev/cel/verifier:policy_verifier"],
+)
+
+java_library(
+    name = "policy_verifier_factory",
+    exports = ["//verifier/src/main/java/dev/cel/verifier:policy_verifier_factory"],
+)
+
+java_library(
+    name = "verifier_factory",
+    compatible_with = [],
+    exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"],
+)
+
+java_library(
+    name = "type_system",
+    compatible_with = [],
+    visibility = ["//:internal"],
+    exports = ["//verifier/src/main/java/dev/cel/verifier:type_system"],
+)
+
+java_library(
+    name = "z3_impl",
+    compatible_with = [],
+    visibility = ["//:internal"],
+    exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"],
+)