Verifier REPL

Author: l46kok

MODULE.bazel

@@ -95,6 +95,9 @@ maven.install(
         "info.picocli:picocli:4.7.7",
         "org.antlr:antlr4-runtime:4.13.2",
         "org.freemarker:freemarker:2.3.34",
+        # CLI tool only dependencies (must never be referenced in core CEL-Java libraries)
+        "org.jline:jline-reader:3.26.1",
+        "org.jline:jline-terminal:3.26.1",
         "org.jspecify:jspecify:1.0.0",
         "org.threeten:threeten-extra:1.8.0",
         "org.yaml:snakeyaml:2.5",

verifier/BUILD.bazel

@@ -54,3 +54,9 @@ java_library(
     visibility = [":verifier_internal"],
     exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"],
 )
+
+java_library(
+    name = "tools",
+    exports = ["//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool"],
+)
+

verifier/README.md

@@ -77,6 +77,33 @@ The following features are planned for future releases:
 
 ---
 
+## CLI & Interactive REPL Tool
+
+The CEL Java Verifier comes with a command-line tool (`cel-verifier`) and an interactive REPL shell for testing satisfiability, validity, equivalence, and policy invariants without writing Java code.
+
+### Running via Bazel
+
+```bash
+# Run CLI verification commands
+bazel run //verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool -- check-sat --expr "role == 'editor' && port > 1024" --var "role:string" --var "port:int"
+
+# Run with JSON output format for CI/CD integrations
+bazel run //verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool -- check-sat --expr "role == 'editor'" --var "role:string" --output_format=json
+
+# Launch interactive REPL shell
+bazel run //verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool -- repl
+```
+
+### CLI Commands
+
+*   `check-sat --expr "..." --var "name:type"`: Verifies satisfiability of an expression and prints witness inputs.
+*   `check-valid --expr "..." --var "name:type"`: Proves validity (`isAlwaysTrue`) and prints counterexample if invalid.
+*   `verify-equiv --expr1 "..." --expr2 "..." --var "name:type"`: Proves logical equivalence between two CEL expressions.
+*   `verify-policy --file policy.yaml`: Verifies custom policy invariants defined in a policy YAML file.
+*   `repl`: Enters interactive verification shell. In the REPL, use `equiv <expr1> <=> <expr2>` to test expression equivalence.
+
+---
+
 ## Usage
 
 ### 1. AST Equivalence Verification

verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel

@@ -0,0 +1,55 @@
+load("@rules_java//java:defs.bzl", "java_binary", "java_library")
+
+package(
+    default_applicable_licenses = [
+        "//:license",
+    ],
+    default_visibility = [
+        "//verifier:__subpackages__",
+    ],
+)
+
+java_library(
+    name = "tools_lib",
+    srcs = [
+        "CelVerifierRepl.java",
+        "CelVerifierTool.java",
+        "CelVerifierToolCore.java",
+        "FormatUtils.java",
+        "VerificationOptions.java",
+    ],
+    deps = [
+        "//bundle:cel",
+        "//common:cel_ast",
+        "//common:compiler_common",
+        "//common/types",
+        "//common/types:cel_types",
+        "//common/types:type_providers",
+        "//compiler",
+        "//compiler:compiler_builder",
+        "//extensions",
+        "//parser:macro",
+        "//policy",
+        "//policy:compiler",
+        "//policy:compiler_factory",
+        "//policy:parser",
+        "//policy:parser_factory",
+        "//policy:validation_exception",
+        "//verifier",
+        "//verifier:policy_verifier",
+        "//verifier:policy_verifier_factory",
+        "//verifier:verifier_factory",
+        "@maven//:com_google_guava_guava",
+        "@maven//:info_picocli_picocli",
+        "@maven//:org_jline_jline_reader",
+        "@maven//:org_jline_jline_terminal",
+    ],
+)
+
+java_binary(
+    name = "cel_verifier_tool",
+    main_class = "dev.cel.verifier.tools.CelVerifierTool",
+    runtime_deps = [
+        ":tools_lib",
+    ],
+)