From 2df939119c7fbd9882ff0f41351e737696c4d401 Mon Sep 17 00:00:00 2001
From: Muhammad Askri <askrim@google.com>
Date: Tue, 8 Sep 2026 09:05:20 -0700
Subject: [PATCH] Introduce cel_verifier_test Bazel macro for CEL verification.

PiperOrigin-RevId: 977944120
---
 .../java/dev/cel/verifier/tools/BUILD.bazel   |   3 +
 verifier/tools/BUILD.bazel                    |  19 +++
 verifier/tools/cel_verifier.bzl               | 125 ++++++++++++++++++
 verifier/tools/run_verifier.sh                |  23 ++++
 4 files changed, 170 insertions(+)
 create mode 100644 verifier/tools/cel_verifier.bzl
 create mode 100755 verifier/tools/run_verifier.sh

diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel
index 1d2c7569e..e01874c84 100644
--- a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel
+++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel
@@ -75,6 +75,9 @@ java_binary(
     tags = [
         "alt_dep=//verifier/tools:cel_verifier_tool",
     ],
+    visibility = [
+        "//verifier:__subpackages__",
+    ],
     runtime_deps = [
         ":tools_lib",
     ],
diff --git a/verifier/tools/BUILD.bazel b/verifier/tools/BUILD.bazel
index a547c15b2..c3a192a3c 100644
--- a/verifier/tools/BUILD.bazel
+++ b/verifier/tools/BUILD.bazel
@@ -1,8 +1,13 @@
+load("//tools/build_defs/testing:bzl_library.bzl", "bzl_library")
+load(":cel_verifier.bzl", "cel_verifier_test")
+
 package(
     default_applicable_licenses = ["//:license"],
     default_visibility = ["//verifier:verifier_internal"],
 )
 
+exports_files(["run_verifier.sh"])
+
 alias(
     name = "tools",
     actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib",
@@ -17,3 +22,17 @@ alias(
     name = "cel_verifier_tool",
     actual = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool",
 )
+
+cel_verifier_test(
+    name = "test_sat_simple_test",
+    command = "check-sat",
+    expression = "x > 10",
+    variables = {"x": "int"},
+)
+
+bzl_library(
+    name = "cel_verifier_bzl",
+    srcs = ["cel_verifier.bzl"],
+    parse_tests = False,
+    visibility = ["//visibility:private"],
+)
diff --git a/verifier/tools/cel_verifier.bzl b/verifier/tools/cel_verifier.bzl
new file mode 100644
index 000000000..49b2bf63e
--- /dev/null
+++ b/verifier/tools/cel_verifier.bzl
@@ -0,0 +1,125 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""Macros for CEL Formal Verifier."""
+
+load("@rules_shell//shell:sh_test.bzl", "sh_test")
+load("@bazel_skylib//lib:shell.bzl", "shell")
+
+def _make_verifier_args(
+        command,
+        expression = None,
+        expression_b = None,
+        policy_file = None,
+        variables = {},
+        unknowns = [],
+        timeout = 10,
+        unroll_limit = 5):
+    args = []
+    srcs = []
+
+    if command not in ["check-sat", "check-valid", "verify-equiv", "verify-policy"]:
+        fail("Unsupported command: " + command)
+
+    args.append(command)
+
+    if command in ["check-sat", "check-valid"]:
+        if not expression:
+            fail("expression is required for " + command)
+        args.append("--expr")
+        args.append(expression)
+    elif command == "verify-equiv":
+        if not expression or not expression_b:
+            fail("expression and expression_b are required for verify-equiv")
+        args.append("--expr1")
+        args.append(expression)
+        args.append("--expr2")
+        args.append(expression_b)
+    elif command == "verify-policy":
+        if not policy_file:
+            fail("policy_file is required for verify-policy")
+        args.append("--file")
+        args.append("$(rootpath %s)" % policy_file)
+        srcs.append(policy_file)
+
+    for var_name, var_type in variables.items():
+        args.append("--var")
+        args.append("%s:%s" % (var_name, var_type))
+
+    for unknown in unknowns:
+        args.append("--unknown")
+        args.append(unknown)
+
+    args.append("--timeout")
+    args.append(str(timeout))
+
+    args.append("--unroll-limit")
+    args.append(str(unroll_limit))
+
+    args.append("--output_format")
+    args.append("TEXT")
+
+    return args, srcs
+
+def cel_verifier_test(
+        name,
+        command,
+        expression = None,
+        expression_b = None,
+        policy_file = None,
+        variables = {},
+        unknowns = [],
+        timeout = 10,
+        unroll_limit = 5,
+        **kwargs):
+    """Verifies a CEL expression or policy via a test rule.
+
+    Args:
+      name: str name for the test
+      command: str verification command ('check-sat', 'check-valid', 'verify-equiv', 'verify-policy')
+      expression: str CEL expression to verify (required for check-sat, check-valid, verify-equiv)
+      expression_b: str second CEL expression for equivalence check (required for verify-equiv)
+      policy_file: label of a YAML policy file to verify (required for verify-policy)
+      variables: dict of var_name -> type_string (e.g., {"port": "int"})
+      unknowns: list of str unknown identifiers
+      timeout: int solver timeout in seconds (default 10)
+      unroll_limit: int comprehension unroll limit (default 5)
+      **kwargs: other standard Bazel attributes
+    """
+
+    args, srcs = _make_verifier_args(
+        command = command,
+        expression = expression,
+        expression_b = expression_b,
+        policy_file = policy_file,
+        variables = variables,
+        unknowns = unknowns,
+        timeout = timeout,
+        unroll_limit = unroll_limit,
+    )
+
+    tags = kwargs.pop("tags", [])
+    if "nomsan" not in tags:
+        tags = tags + ["nomsan"]
+
+    sh_test(
+        name = name,
+        srcs = ["//verifier/tools:run_verifier.sh"],
+        args = [shell.quote(a) for a in args],
+        data = [
+            "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool",
+        ] + srcs,
+        tags = tags,
+        **kwargs
+    )
diff --git a/verifier/tools/run_verifier.sh b/verifier/tools/run_verifier.sh
new file mode 100755
index 000000000..3d4bf39cc
--- /dev/null
+++ b/verifier/tools/run_verifier.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+# Path: //third_party/java/cel/verifier/tools/run_verifier.sh
+#
+# This script is used by the cel_verifier_test macro to invoke the
+# underlying Java binary (CelVerifierTool) with the arguments passed to the macro.
+# It uses 'find' to locate the binary in the runfiles directory, which works
+# in both Google3 and Bazel environments.
+
+die() {
+  echo "ERROR: $*" >&2
+  exit 1
+}
+
+# Find the cel_verifier_tool executable (wrapper script).
+# We use -L to follow symlinks, as blaze-bin usually contains symlinks.
+VERIFIER_BINARY="$(find -L "${TEST_SRCDIR}" -name "cel_verifier_tool" -type f -executable)"
+
+if [ -z "$VERIFIER_BINARY" ]; then
+  die "Verifier binary cel_verifier_tool not found in runfiles."
+fi
+
+# Execute the verifier binary with all passed arguments.
+exec "$VERIFIER_BINARY" "$@"