From 16cf13d0454ee076d4535caff7ba31ce8f7a76ab Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 29 Jul 2026 22:26:48 +0000 Subject: [PATCH] Verifier REPL --- MODULE.bazel | 3 + verifier/BUILD.bazel | 6 + verifier/README.md | 27 ++ .../java/dev/cel/verifier/tools/BUILD.bazel | 55 +++ .../cel/verifier/tools/CelVerifierRepl.java | 335 ++++++++++++++++++ .../cel/verifier/tools/CelVerifierTool.java | 291 +++++++++++++++ .../verifier/tools/CelVerifierToolCore.java | 160 +++++++++ .../dev/cel/verifier/tools/FormatUtils.java | 147 ++++++++ .../verifier/tools/VerificationOptions.java | 217 ++++++++++++ .../test/java/dev/cel/verifier/BUILD.bazel | 2 + .../verifier/tools/CelVerifierToolTest.java | 118 ++++++ 11 files changed, 1361 insertions(+) create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java diff --git a/MODULE.bazel b/MODULE.bazel index ce9c67fde..5664936ba 100644 --- a/MODULE.bazel +++ b/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", diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index cc2f01810..661de05ed 100644 --- a/verifier/BUILD.bazel +++ b/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"], +) + diff --git a/verifier/README.md b/verifier/README.md index db797a283..c92eebdae 100644 --- a/verifier/README.md +++ b/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 <=> ` to test expression equivalence. + +--- + ## Usage ### 1. AST Equivalence Verification diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..92177e57b --- /dev/null +++ b/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", + ], +) diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java new file mode 100644 index 000000000..6b0e54369 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -0,0 +1,335 @@ +// 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. + +package dev.cel.verifier.tools; + +import dev.cel.common.types.CelType; +import dev.cel.common.types.CelTypes; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelVerificationResult; +import java.io.BufferedReader; +import java.io.InputStreamReader; +import java.nio.charset.StandardCharsets; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; + +/** Interactive REPL shell for CEL formal verification. */ +public final class CelVerifierRepl { + + private CelVerifierRepl() {} + + public static int runInteractiveRepl() { + System.out.println("============================================================"); + System.out.println(" CEL Verification REPL (cel-java v0.14.0)"); + System.out.println(" Type :help for commands, :quit to exit."); + System.out.println("============================================================"); + + Map sessionVars = new HashMap<>(); + List unknownIdentifiers = new ArrayList<>(); + int timeoutSeconds = 10; + int unrollLimit = 5; + + org.jline.reader.LineReader lineReader = null; + BufferedReader fallbackReader = null; + try { + org.jline.terminal.Terminal terminal = org.jline.terminal.TerminalBuilder.builder().system(true).build(); + lineReader = org.jline.reader.LineReaderBuilder.builder().terminal(terminal).build(); + } catch (Exception e) { + fallbackReader = + new BufferedReader(new InputStreamReader(System.in, StandardCharsets.UTF_8)); + } + + String prompt = FormatUtils.ANSI_CYAN + "cel-verifier> " + FormatUtils.ANSI_RESET; + + while (true) { + String line; + try { + if (lineReader != null) { + line = lineReader.readLine(prompt); + } else { + System.out.print(prompt); + System.out.flush(); + line = fallbackReader.readLine(); + if (line == null) { + break; // EOF + } + } + } catch (org.jline.reader.UserInterruptException | org.jline.reader.EndOfFileException e) { + System.out.println("Goodbye!"); + break; + } catch (Exception e) { + System.err.println("Error reading input: " + e.getMessage()); + break; + } + + line = line.trim(); + if (line.isEmpty()) { + continue; + } + + if (line.equalsIgnoreCase(":quit") || line.equalsIgnoreCase(":exit")) { + System.out.println("Goodbye!"); + break; + } + + if (line.startsWith(":help")) { + String sub = line.substring(5).trim(); + printHelp(sub); + continue; + } + + if (line.equalsIgnoreCase(":vars")) { + printVars(sessionVars, unknownIdentifiers, timeoutSeconds, unrollLimit); + continue; + } + + if (line.equalsIgnoreCase(":clear")) { + sessionVars.clear(); + unknownIdentifiers.clear(); + System.out.println("Session state reset."); + continue; + } + + if (line.startsWith(":var ")) { + handleVarCommand(line.substring(5).trim(), sessionVars); + continue; + } + + if (line.startsWith(":unknown ")) { + String ident = line.substring(9).trim(); + if (!ident.isEmpty()) { + unknownIdentifiers.add(ident); + System.out.println("Added unknown identifier: '" + ident + "'"); + } + continue; + } + + if (line.startsWith(":timeout ")) { + try { + timeoutSeconds = Integer.parseInt(line.substring(9).trim()); + System.out.println("Timeout set to " + timeoutSeconds + "s."); + } catch (NumberFormatException e) { + System.err.println("Invalid timeout value."); + } + continue; + } + + if (line.startsWith(":unroll ")) { + try { + unrollLimit = Integer.parseInt(line.substring(8).trim()); + System.out.println("Comprehension unroll limit set to " + unrollLimit + "."); + } catch (NumberFormatException e) { + System.err.println("Invalid unroll limit value."); + } + continue; + } + + // Handle queries + VerificationOptions options = + VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(unrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .build(); + + try { + if (line.startsWith("sat ")) { + String expr = line.substring(4).trim(); + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(expr, sessionVars, options); + System.out.println(FormatUtils.formatTextResult(res)); + } else if (line.startsWith("valid ")) { + String expr = line.substring(6).trim(); + CelVerificationResult res = + CelVerifierToolCore.checkValid(expr, sessionVars, options); + System.out.println(FormatUtils.formatTextResult(res)); + } else if (line.startsWith("equiv ")) { + String rest = line.substring(6).trim(); + String[] parts = splitEquivQuery(rest); + if (parts.length != 2 || parts[0].isEmpty() || parts[1].isEmpty()) { + System.err.println( + "Equivalence query format: equiv <=> "); + } else { + String exprA = parts[0].trim(); + String exprB = parts[1].trim(); + CelVerificationResult res = + CelVerifierToolCore.verifyEquivalence(exprA, exprB, sessionVars, options); + System.out.println(FormatUtils.formatTextResult(res)); + } + } else { + // Default: treat as sat query + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(line, sessionVars, options); + System.out.println(FormatUtils.formatTextResult(res)); + } + } catch (dev.cel.common.CelValidationException e) { + System.err.println(FormatUtils.ANSI_RED + "Compilation error:\n" + e.getMessage() + FormatUtils.ANSI_RESET); + } catch (dev.cel.policy.CelPolicyValidationException e) { + System.err.println(FormatUtils.ANSI_RED + "Policy compilation error:\n" + e.getMessage() + FormatUtils.ANSI_RESET); + } catch (Exception e) { + System.err.println(FormatUtils.ANSI_RED + "Verification failed: " + e.getMessage() + FormatUtils.ANSI_RESET); + } + } + return 0; + } + + private static void handleVarCommand(String arg, Map sessionVars) { + String[] parts = arg.split("\\s+", 2); + if (parts.length != 2) { + System.err.println("Usage: :var (e.g. :var role string, :var scores map)"); + return; + } + String name = parts[0].trim(); + String typeStr = parts[1].trim(); + try { + CelType type = VerificationOptions.parseCelType(typeStr); + sessionVars.put(name, type); + System.out.println("Variable declared: " + name + " : " + CelTypes.format(type)); + } catch (IllegalArgumentException e) { + System.err.println(e.getMessage()); + } + } + + private static void printVars( + Map sessionVars, + List unknowns, + int timeoutSeconds, + int unrollLimit) { + System.out.println("--- Session State ---"); + System.out.println("Timeout: " + timeoutSeconds + "s | Unroll limit: " + unrollLimit); + System.out.println("Unknowns: " + (unknowns.isEmpty() ? "none" : unknowns)); + System.out.println("Variables (" + sessionVars.size() + "):"); + for (Map.Entry entry : sessionVars.entrySet()) { + System.out.println(" " + entry.getKey() + " : " + CelTypes.format(entry.getValue())); + } + } + + private static void printHelp() { + printHelp(""); + } + + private static void printHelp(String topic) { + String t = topic.toLowerCase(Locale.US).replace(":", "").trim(); + switch (t) { + case "var": + case "vars": + System.out.println("Command: :var "); + System.out.println("Declares a variable in the REPL session with a specific type."); + System.out.println(); + System.out.println("Supported Types:"); + System.out.println(" - Primitive types: int, uint, string, bool, double, bytes"); + System.out.println(" - List types: list (e.g., list, list)"); + System.out.println(" - Map types: map (e.g., map, map)"); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> :var role string"); + System.out.println(" cel-verifier> :var port int"); + System.out.println(" cel-verifier> :var scores map"); + System.out.println(" cel-verifier> :var tags list"); + break; + case "unknown": + System.out.println("Command: :unknown "); + System.out.println("Marks an identifier path as 'Unknown' during verification (partial evaluation)."); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> :unknown request.headers"); + System.out.println(" cel-verifier> :unknown request.auth.claims"); + break; + case "timeout": + System.out.println("Command: :timeout "); + System.out.println("Configures the Z3 solver soft timeout duration in seconds (default: 10s)."); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> :timeout 5"); + break; + case "unroll": + System.out.println("Command: :unroll "); + System.out.println("Configures the BMC loop unroll limit for comprehensions (default: 5)."); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> :unroll 3"); + break; + case "sat": + System.out.println("Query: sat "); + System.out.println("Checks if a CEL expression can evaluate to true for any possible input assignments."); + System.out.println("If satisfiable, outputs concrete satisfying witness values."); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> sat role == 'editor' && port > 1024"); + System.out.println(" cel-verifier> sat scores['alice'] > 90"); + break; + case "valid": + System.out.println("Query: valid "); + System.out.println("Proves whether a CEL expression evaluates to true for ALL possible input assignments."); + System.out.println("If invalid, outputs a counterexample showing inputs causing it to fail."); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> valid x > 10 || x <= 10"); + break; + case "equiv": + System.out.println("Query: equiv <=> "); + System.out.println("Proves whether two CEL expressions are semantically identical for all inputs."); + System.out.println("If not equivalent, outputs a counterexample showing inputs where they diverge."); + System.out.println(); + System.out.println("Use '<=>' as the recommended separator between expressions."); + System.out.println(); + System.out.println("Examples:"); + System.out.println(" cel-verifier> equiv x > 10 <=> 10 < x"); + System.out.println(" cel-verifier> equiv (a && b) || (a && c) <=> a && (b || c)"); + System.out.println(" cel-verifier> equiv string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k == 'a') : true <=> string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k == 'a') : true"); + break; + default: + System.out.println("REPL Commands:"); + System.out.println(" :var Declare variable (e.g. :var role string, :var m map)"); + System.out.println(" :unknown Mark identifier as unknown"); + System.out.println(" :timeout Set solver timeout (default: 10s)"); + System.out.println(" :unroll Set comprehension unroll limit (default: 5)"); + System.out.println(" :vars List session variables & options"); + System.out.println(" :clear Reset session state"); + System.out.println(" :help [command] Display help message or specific command details"); + System.out.println(" :quit Exit REPL"); + System.out.println(); + System.out.println("Verification Queries:"); + System.out.println(" sat Check satisfiability"); + System.out.println(" valid Check validity (always true)"); + System.out.println(" equiv <=> Prove logical equivalence"); + System.out.println(" Check satisfiability (default)"); + System.out.println(); + System.out.println("Type ':help ' (e.g. ':help var', ':help sat') for detailed usage and examples."); + break; + } + } + + public static String[] splitEquivQuery(String rest) { + if (rest == null || rest.trim().isEmpty()) { + return new String[0]; + } + String input = rest.trim(); + if (input.contains(" <=> ")) { + return input.split(" <=> ", 2); + } + if (input.contains(" === ")) { + return input.split(" === ", 2); + } + if (input.contains(" , ")) { + return input.split(" , ", 2); + } + return new String[0]; + } +} + diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java new file mode 100644 index 000000000..62fe0aeec --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java @@ -0,0 +1,291 @@ +// 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. + +package dev.cel.verifier.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.CelType; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import dev.cel.verifier.tools.VerificationOptions.OutputFormat; +import java.io.File; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.ArrayList; +import java.util.List; +import java.util.concurrent.Callable; +import picocli.CommandLine; +import picocli.CommandLine.Command; +import picocli.CommandLine.Option; + +/** Main Picocli entrypoint for the CEL Formal Verification CLI. */ +@Command( + name = "cel-verifier", + mixinStandardHelpOptions = true, + version = "cel-verifier 0.14.0", + description = "CEL-Java Formal Verification CLI & REPL Tool", + subcommands = { + CelVerifierTool.CheckSatCommand.class, + CelVerifierTool.CheckValidCommand.class, + CelVerifierTool.VerifyEquivCommand.class, + CelVerifierTool.VerifyPolicyCommand.class, + CelVerifierTool.ReplCommand.class + }) +public final class CelVerifierTool implements Runnable { + + @Override + public void run() { + CommandLine.usage(this, System.out); + } + + /** Options shared across all verification commands. */ + abstract static class BaseVerificationCommand implements Callable { + + @Option( + names = {"--var", "-v"}, + description = "Declared variable in 'name:type' format (e.g., --var role:string --var port:int)") + List variables = new ArrayList<>(); + + @Option( + names = {"--unknown", "-u"}, + description = "Identifier to permit evaluating to Unknown (e.g., --unknown request.headers)") + List unknownIdentifiers = new ArrayList<>(); + + @Option( + names = {"--timeout"}, + description = "Solver timeout in seconds (default: 10)") + int timeoutSeconds = 10; + + @Option( + names = {"--unroll-limit"}, + description = "Comprehension unroll limit for BMC (default: 5)") + int comprehensionUnrollLimit = 5; + + @Option( + names = {"--output_format", "-fmt"}, + description = "Output format: TEXT or JSON (default: TEXT)") + String outputFormatStr = "TEXT"; + + protected VerificationOptions getOptions() { + OutputFormat format = OutputFormat.TEXT; + try { + format = OutputFormat.valueOf(outputFormatStr.toUpperCase()); + } catch (IllegalArgumentException e) { + System.err.println("Invalid output format '" + outputFormatStr + "'. Defaulting to TEXT."); + } + return VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(comprehensionUnrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .setOutputFormat(format) + .build(); + } + + protected int handleSingleResult(CelVerificationResult result, OutputFormat format) { + if (format == OutputFormat.JSON) { + System.out.println(FormatUtils.formatJsonResult(result)); + } else { + System.out.println(FormatUtils.formatTextResult(result)); + } + + if (result.status() == VerificationStatus.VERIFIED) { + return 0; + } else if (result.status() == VerificationStatus.VIOLATED) { + return 1; + } else { + return 2; + } + } + } + + @Command( + name = "check-sat", + description = "Verify satisfiability of a CEL expression & generate witness model") + static class CheckSatCommand extends BaseVerificationCommand { + + @Option( + names = {"--expr", "-e"}, + required = true, + description = "CEL expression string to verify") + String expression = ""; + + @Override + public Integer call() { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable(expression, vars, options); + return handleSingleResult(result, options.getOutputFormat()); + } catch (dev.cel.common.CelValidationException e) { + System.err.println("Compilation error:\n" + e.getMessage()); + return 3; + } catch (dev.cel.policy.CelPolicyValidationException e) { + System.err.println("Policy compilation error:\n" + e.getMessage()); + return 3; + } catch (Exception e) { + System.err.println("Verification error: " + e.getMessage()); + return 3; + } + } + } + + @Command( + name = "check-valid", + description = "Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample") + static class CheckValidCommand extends BaseVerificationCommand { + + @Option( + names = {"--expr", "-e"}, + required = true, + description = "CEL expression string to verify") + String expression = ""; + + @Override + public Integer call() { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + CelVerificationResult result = + CelVerifierToolCore.checkValid(expression, vars, options); + return handleSingleResult(result, options.getOutputFormat()); + } catch (dev.cel.common.CelValidationException e) { + System.err.println("Compilation error:\n" + e.getMessage()); + return 3; + } catch (dev.cel.policy.CelPolicyValidationException e) { + System.err.println("Policy compilation error:\n" + e.getMessage()); + return 3; + } catch (Exception e) { + System.err.println("Verification error: " + e.getMessage()); + return 3; + } + } + } + + @Command( + name = "verify-equiv", + description = "Prove logical equivalence between two CEL expressions") + static class VerifyEquivCommand extends BaseVerificationCommand { + + @Option( + names = {"--expr1"}, + required = true, + description = "First CEL expression") + String expressionA = ""; + + @Option( + names = {"--expr2"}, + required = true, + description = "Second CEL expression") + String expressionB = ""; + + @Override + public Integer call() { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence(expressionA, expressionB, vars, options); + return handleSingleResult(result, options.getOutputFormat()); + } catch (dev.cel.common.CelValidationException e) { + System.err.println("Compilation error:\n" + e.getMessage()); + return 3; + } catch (dev.cel.policy.CelPolicyValidationException e) { + System.err.println("Policy compilation error:\n" + e.getMessage()); + return 3; + } catch (Exception e) { + System.err.println("Verification error: " + e.getMessage()); + return 3; + } + } + } + + @Command( + name = "verify-policy", + description = "Verify policy invariants defined in a YAML policy file") + static class VerifyPolicyCommand extends BaseVerificationCommand { + + @Option( + names = {"--file", "-f"}, + required = true, + description = "Path to policy YAML file") + String filePath = ""; + + @Override + public Integer call() { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + File file = new File(filePath); + if (!file.exists()) { + System.err.println("File not found: " + filePath); + return 3; + } + String yamlContent = new String(Files.readAllBytes(file.toPath()), StandardCharsets.UTF_8); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlContent, vars, options); + + if (options.getOutputFormat() == OutputFormat.JSON) { + System.out.println(FormatUtils.formatJsonPolicyResults(file.getName(), results)); + } else { + System.out.println(FormatUtils.formatTextPolicyResults(file.getName(), results)); + } + + boolean anyViolated = false; + boolean anyInconclusive = false; + for (CelVerificationResult res : results.values()) { + if (res.status() == VerificationStatus.VIOLATED) { + anyViolated = true; + } else if (res.status() == VerificationStatus.INCONCLUSIVE) { + anyInconclusive = true; + } + } + + if (anyViolated) { + return 1; + } else if (anyInconclusive) { + return 2; + } + return 0; + } catch (dev.cel.common.CelValidationException e) { + System.err.println("Compilation error:\n" + e.getMessage()); + return 3; + } catch (dev.cel.policy.CelPolicyValidationException e) { + System.err.println("Policy compilation error:\n" + e.getMessage()); + return 3; + } catch (Exception e) { + System.err.println("Policy verification error: " + e.getMessage()); + return 3; + } + } + } + + @Command( + name = "repl", + description = "Launch interactive CEL Formal Verification REPL shell") + static class ReplCommand implements Callable { + + @Override + public Integer call() { + return CelVerifierRepl.runInteractiveRepl(); + } + } + + public static void main(String[] args) { + int exitCode = new CommandLine(new CelVerifierTool()).execute(args); + System.exit(exitCode); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java new file mode 100644 index 000000000..8e757ede6 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -0,0 +1,160 @@ +// 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. + +package dev.cel.verifier.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelBuilder; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.types.CelType; +import dev.cel.compiler.CelCompiler; +import dev.cel.compiler.CelCompilerBuilder; +import dev.cel.compiler.CelCompilerFactory; +import dev.cel.extensions.CelExtensions; +import dev.cel.parser.CelStandardMacro; +import dev.cel.policy.CelPolicy; +import dev.cel.policy.CelPolicyCompiler; +import dev.cel.policy.CelPolicyCompilerFactory; +import dev.cel.policy.CelPolicyParser; +import dev.cel.policy.CelPolicyParserFactory; +import dev.cel.verifier.CelPolicyVerifier; +import dev.cel.verifier.CelPolicyVerifierFactory; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerifier; +import dev.cel.verifier.CelVerifierBuilder; +import dev.cel.verifier.CelVerifierFactory; +import java.util.Map; + +/** Core decoupled engine that executes formal verification operations. */ +public final class CelVerifierToolCore { + + private CelVerifierToolCore() {} + + /** Checks if a single CEL expression is satisfiable. */ + public static CelVerificationResult checkSatisfiable( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.isSatisfiable(ast); + } + + /** Checks if a single CEL expression is valid (always true). */ + public static CelVerificationResult checkValid( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.isAlwaysTrue(ast); + } + + /** Proves logical equivalence between two CEL expressions. */ + public static CelVerificationResult verifyEquivalence( + String expressionA, + String expressionB, + Map variables, + VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree astA = compiler.compile(expressionA).getAst(); + CelAbstractSyntaxTree astB = compiler.compile(expressionB).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.verifyEquivalence(astA, astB); + } + + /** Verifies custom invariants in a YAML policy content string. */ + public static ImmutableMap verifyPolicyInvariants( + String yamlContent, Map variables, VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policy = parser.parse(yamlContent); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyInvariants(policy); + } + + /** Verifies equivalence between two YAML policy content strings. */ + public static CelVerificationResult verifyPolicyEquivalence( + String yamlContentA, + String yamlContentB, + Map variables, + VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policyA = parser.parse(yamlContentA); + CelPolicy policyB = parser.parse(yamlContentB); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyEquivalence(policyA, policyB); + } + + public static CelCompiler buildCompiler(Map variables) { + CelCompilerBuilder builder = + CelCompilerFactory.standardCelCompilerBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addLibraries( + CelExtensions.optional(), + CelExtensions.bindings(), + CelExtensions.encoders(), + CelExtensions.math(), + CelExtensions.strings()); + if (variables != null) { + for (Map.Entry entry : variables.entrySet()) { + builder.addVar(entry.getKey(), entry.getValue()); + } + } + return builder.build(); + } + + public static CelVerifier buildVerifier(VerificationOptions options) { + CelVerifierBuilder builder = + CelVerifierFactory.newVerifier() + .setTimeout(options.getTimeout()) + .setComprehensionUnrollLimit(options.getComprehensionUnrollLimit()); + + for (String unknown : options.getUnknownIdentifiers()) { + builder.addUnknownIdentifier(unknown); + } + return builder.build(); + } + + private static CelPolicyVerifier buildPolicyVerifier( + Map variables, VerificationOptions options) { + CelBuilder celBuilder = + CelFactory.plannerCelBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addCompilerLibraries( + CelExtensions.optional(), + CelExtensions.bindings(), + CelExtensions.encoders(), + CelExtensions.math(), + CelExtensions.strings()); + if (variables != null) { + for (Map.Entry entry : variables.entrySet()) { + celBuilder.addVar(entry.getKey(), entry.getValue()); + } + } + Cel celBundle = celBuilder.build(); + CelPolicyCompiler policyCompiler = + CelPolicyCompilerFactory.newPolicyCompiler(celBundle).build(); + CelVerifier astVerifier = buildVerifier(options); + + return CelPolicyVerifierFactory.newVerifier(policyCompiler, astVerifier).build(); + } +} + diff --git a/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java new file mode 100644 index 000000000..b1e25f0ac --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java @@ -0,0 +1,147 @@ +// 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. + +package dev.cel.verifier.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.util.Map; + +/** Utilities for formatting verification output (ANSI text & JSON). */ +public final class FormatUtils { + + // ANSI Escape Codes for formatting text + public static final String ANSI_RESET = "\u001B[0m"; + public static final String ANSI_BOLD = "\u001B[1m"; + public static final String ANSI_GREEN = "\u001B[32m"; + public static final String ANSI_RED = "\u001B[31m"; + public static final String ANSI_YELLOW = "\u001B[33m"; + public static final String ANSI_CYAN = "\u001B[36m"; + + private FormatUtils() {} + + /** Formats a single CelVerificationResult for human-readable console display with ANSI color. */ + public static String formatTextResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + String statusColor = getStatusColor(result.status()); + sb.append(statusColor) + .append(ANSI_BOLD) + .append("[") + .append(result.status()) + .append("]") + .append(ANSI_RESET); + + if (result.message() != null && !result.message().isEmpty()) { + sb.append(" ").append(result.message()); + } + + return sb.toString(); + } + + /** Formats policy invariant verification results for human-readable console display. */ + public static String formatTextPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append(ANSI_BOLD) + .append("Policy Invariant Verification for '") + .append(policyName) + .append("':\n") + .append(ANSI_RESET); + + for (Map.Entry entry : results.entrySet()) { + String id = entry.getKey(); + CelVerificationResult result = entry.getValue(); + String symbol = result.status() == VerificationStatus.VERIFIED ? "✓" : "✗"; + String color = getStatusColor(result.status()); + + sb.append(" ") + .append(color) + .append(symbol) + .append(" Invariant '") + .append(id) + .append("': ") + .append(result.status()) + .append(ANSI_RESET); + + if (result.message() != null && !result.message().isEmpty()) { + sb.append("\n ").append(result.message().replace("\n", "\n ")); + } + sb.append("\n"); + } + return sb.toString().trim(); + } + + /** Formats a single CelVerificationResult as structured JSON. */ + public static String formatJsonResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"status\": \"").append(result.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(result.message())).append("\"\n"); + sb.append("}"); + return sb.toString(); + } + + /** Formats policy invariant verification results as structured JSON. */ + public static String formatJsonPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"policyName\": \"").append(escapeJson(policyName)).append("\",\n"); + sb.append(" \"invariants\": [\n"); + + int count = 0; + for (Map.Entry entry : results.entrySet()) { + count++; + String id = entry.getKey(); + CelVerificationResult res = entry.getValue(); + sb.append(" {\n"); + sb.append(" \"id\": \"").append(escapeJson(id)).append("\",\n"); + sb.append(" \"status\": \"").append(res.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(res.message())).append("\"\n"); + sb.append(" }").append(count < results.size() ? "," : "").append("\n"); + } + + sb.append(" ]\n"); + sb.append("}"); + return sb.toString(); + } + + private static String getStatusColor(VerificationStatus status) { + switch (status) { + case VERIFIED: + return ANSI_GREEN; + case VIOLATED: + return ANSI_RED; + case INCONCLUSIVE: + return ANSI_YELLOW; + default: + return ANSI_RESET; + } + } + + private static String escapeJson(String input) { + if (input == null) { + return ""; + } + return input + .replace("\\", "\\\\") + .replace("\"", "\\\"") + .replace("\b", "\\b") + .replace("\f", "\\f") + .replace("\n", "\\n") + .replace("\r", "\\r") + .replace("\t", "\\t"); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java new file mode 100644 index 000000000..08d8524f6 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -0,0 +1,217 @@ +// 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. + +package dev.cel.verifier.tools; + +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.CelType; +import dev.cel.common.types.SimpleType; +import java.time.Duration; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; + +/** Configuration options for CEL verification CLI operations. */ +public final class VerificationOptions { + + public enum OutputFormat { + TEXT, + JSON + } + + public enum VerificationMode { + SAT, + VALID, + EQUIVALENCE, + POLICY_INVARIANTS + } + + private final Duration timeout; + private final int comprehensionUnrollLimit; + private final ImmutableList unknownIdentifiers; + private final OutputFormat outputFormat; + + public Duration getTimeout() { + return timeout; + } + + public int getComprehensionUnrollLimit() { + return comprehensionUnrollLimit; + } + + public ImmutableList getUnknownIdentifiers() { + return unknownIdentifiers; + } + + public OutputFormat getOutputFormat() { + return outputFormat; + } + + public static Builder builder() { + return new Builder(); + } + + public static final class Builder { + private Duration timeout = Duration.ofSeconds(10); + private int comprehensionUnrollLimit = 5; + private ImmutableList unknownIdentifiers = ImmutableList.of(); + private OutputFormat outputFormat = OutputFormat.TEXT; + + public Builder setTimeout(Duration timeout) { + this.timeout = Preconditions.checkNotNull(timeout); + return this; + } + + public Builder setComprehensionUnrollLimit(int unrollLimit) { + Preconditions.checkArgument(unrollLimit >= 0, "unrollLimit must be non-negative"); + this.comprehensionUnrollLimit = unrollLimit; + return this; + } + + public Builder setUnknownIdentifiers(List unknownIdentifiers) { + this.unknownIdentifiers = ImmutableList.copyOf(unknownIdentifiers); + return this; + } + + public Builder setOutputFormat(OutputFormat outputFormat) { + this.outputFormat = Preconditions.checkNotNull(outputFormat); + return this; + } + + public VerificationOptions build() { + return new VerificationOptions( + timeout, comprehensionUnrollLimit, unknownIdentifiers, outputFormat); + } + } + + private VerificationOptions( + Duration timeout, + int comprehensionUnrollLimit, + ImmutableList unknownIdentifiers, + OutputFormat outputFormat) { + this.timeout = timeout; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.unknownIdentifiers = unknownIdentifiers; + this.outputFormat = outputFormat; + } + + /** + * Helper utility to parse CLI variable definitions formatted as "name:type" (e.g. "x:int", + * "role:string", "is_admin:bool"). + */ + public static ImmutableMap parseVariables(List varSpecs) { + if (varSpecs == null || varSpecs.isEmpty()) { + return ImmutableMap.of(); + } + Map vars = new HashMap<>(); + for (String varSpec : varSpecs) { + if (varSpec == null || varSpec.trim().isEmpty()) { + continue; + } + String[] parts = varSpec.split(":", 2); + if (parts.length != 2) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + + varSpec + + "'. Expected format 'name:type' (e.g., 'x:int')."); + } + String name = parts[0].trim(); + String typeStr = parts[1].trim().toLowerCase(Locale.US); + CelType type = parseCelType(typeStr); + vars.put(name, type); + } + return ImmutableMap.copyOf(vars); + } + + public static CelType parseCelType(String typeStr) { + if (typeStr == null) { + throw new IllegalArgumentException("Type string cannot be null."); + } + String str = typeStr.trim().toLowerCase(Locale.US); + + if (str.startsWith("list<") && str.endsWith(">")) { + String inner = str.substring(5, str.length() - 1).trim(); + CelType elemType = parseCelType(inner); + return dev.cel.common.types.ListType.create(elemType); + } + + if (str.startsWith("map<") && str.endsWith(">")) { + String inner = str.substring(4, str.length() - 1).trim(); + List parts = splitGenericArgs(inner); + if (parts.size() != 2) { + throw new IllegalArgumentException( + "Invalid map type format: '" + + typeStr + + "'. Expected format 'map' (e.g., 'map')."); + } + CelType keyType = parseCelType(parts.get(0)); + CelType valueType = parseCelType(parts.get(1)); + return dev.cel.common.types.MapType.create(keyType, valueType); + } + + switch (str) { + case "int": + return SimpleType.INT; + case "uint": + return SimpleType.UINT; + case "string": + return SimpleType.STRING; + case "bool": + case "boolean": + return SimpleType.BOOL; + case "double": + case "float": + return SimpleType.DOUBLE; + case "bytes": + return SimpleType.BYTES; + case "dyn": + case "any": + return SimpleType.DYN; + default: + throw new IllegalArgumentException( + "Unsupported type for CLI variable declaration: '" + + typeStr + + "'. Supported types: int, uint, string, bool, double, bytes, list, map."); + } + } + + private static List splitGenericArgs(String inner) { + List result = new java.util.ArrayList<>(); + int depth = 0; + StringBuilder current = new StringBuilder(); + for (int i = 0; i < inner.length(); i++) { + char c = inner.charAt(i); + if (c == '<') { + depth++; + current.append(c); + } else if (c == '>') { + depth--; + current.append(c); + } else if (c == ',' && depth == 0) { + result.add(current.toString().trim()); + current.setLength(0); + } else { + current.append(c); + } + } + if (current.length() > 0) { + result.add(current.toString().trim()); + } + return result; + } +} + diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 9e7f0ed15..4f4e4de2d 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -24,6 +24,7 @@ java_library( "//common:options", "//common/ast", "//common/types", + "//common/types:type_providers", "//common/types:message_type_provider", "//compiler:compiler_builder", "//extensions", @@ -47,6 +48,7 @@ java_library( "//:java_truth", "@maven//:tools_aqua_z3_turnkey", "//verifier", + "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", "//verifier:policy_verifier", "//verifier:policy_verifier_factory", "//verifier:type_system", diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java new file mode 100644 index 000000000..754adc1a8 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -0,0 +1,118 @@ +// 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. + +package dev.cel.verifier.tools; + +import static com.google.common.truth.Truth.assertThat; + +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.CelType; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.time.Duration; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class CelVerifierToolTest { + + @Test + public void parseVariables_success() { + ImmutableMap vars = + VerificationOptions.parseVariables( + java.util.Arrays.asList( + "x:int", + "role:string", + "is_admin:bool", + "tags:list", + "scores:map")); + assertThat(vars).containsEntry("x", SimpleType.INT); + assertThat(vars).containsEntry("role", SimpleType.STRING); + assertThat(vars).containsEntry("is_admin", SimpleType.BOOL); + assertThat(vars).containsEntry("tags", dev.cel.common.types.ListType.create(SimpleType.STRING)); + assertThat(vars).containsEntry("scores", dev.cel.common.types.MapType.create(SimpleType.STRING, SimpleType.INT)); + } + + @Test + public void checkSatisfiable_satisfiable() throws Exception { + VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("role", SimpleType.STRING, "port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("role == 'editor' && port > 1024", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("satisfiable"); + } + + @Test + public void checkValid_valid() throws Exception { + VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkValid("x > 10 || x <= 10", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyEquivalence_equivalent() throws Exception { + VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence("x > 10", "10 < x", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyInvariants_success() throws Exception { + String yamlPolicy = + "name: secure_access_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + + VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlPolicy, vars, options); + + assertThat(results).containsKey("port_check"); + assertThat(results.get("port_check").status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void formatUtils_jsonResult() throws Exception { + VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + String json = FormatUtils.formatJsonResult(result); + assertThat(json).contains("\"status\": \"VERIFIED\""); + assertThat(json).contains("satisfiable"); + } +} + +