From 75e090067b4fcdbc69d9b65056d5323901d9bb17 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 5 Aug 2026 14:04:32 -0700 Subject: [PATCH] Add REPL for Verifier PiperOrigin-RevId: 959858257 --- BUILD.bazel | 8 + MODULE.bazel | 2 + .../java/dev/cel/verifier/tools/BUILD.bazel | 3 + .../cel/verifier/tools/CelVerifierRepl.java | 435 ++++++++++++++++++ .../cel/verifier/tools/CelVerifierTool.java | 14 +- .../verifier/tools/VerificationOptions.java | 4 + .../verifier/tools/CelVerifierReplTest.java | 188 ++++++++ verifier/tools/README.md | 84 ++++ 8 files changed, 736 insertions(+), 2 deletions(-) create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java diff --git a/BUILD.bazel b/BUILD.bazel index 024908625..d2bf2124b 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -95,6 +95,14 @@ java_library( ], ) +java_library( + name = "java_jline", + exports = [ + "@maven//:org_jline_jline_reader", + "@maven//:org_jline_jline_terminal", + ], +) + default_java_toolchain( name = "repository_default_toolchain", configuration = DEFAULT_TOOLCHAIN_CONFIGURATION, diff --git a/MODULE.bazel b/MODULE.bazel index ce9c67fde..3dcf8b0e5 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -95,6 +95,8 @@ maven.install( "info.picocli:picocli:4.7.7", "org.antlr:antlr4-runtime:4.13.2", "org.freemarker:freemarker:2.3.34", + "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/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel index e4339f857..28ce776cb 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -28,6 +28,7 @@ EOF java_library( name = "tools_lib", srcs = [ + "CelVerifierRepl.java", "CelVerifierTool.java", "CelVerifierToolCore.java", "FormatUtils.java", @@ -38,11 +39,13 @@ java_library( "alt_dep=//verifier/tools", ], deps = [ + "//:java_jline", "//bundle:cel", "//common:cel_ast", "//common:compiler_common", "//common:options", "//common/types", + "//common/types:cel_types", "//common/types:type_providers", "//compiler", "//compiler:compiler_builder", 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..25354480a --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -0,0 +1,435 @@ +// 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 java.nio.charset.StandardCharsets.UTF_8; + +import com.google.common.base.Ascii; +import com.google.common.collect.ImmutableList; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.common.types.CelTypes; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import java.io.BufferedReader; +import java.io.InputStreamReader; +import java.io.PrintStream; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.Optional; +import org.jline.reader.EndOfFileException; +import org.jline.reader.LineReader; +import org.jline.reader.LineReaderBuilder; +import org.jline.reader.UserInterruptException; +import org.jline.terminal.Terminal; +import org.jline.terminal.TerminalBuilder; + +/** Interactive REPL shell for CEL formal verification. */ +final class CelVerifierRepl { + + private CelVerifierRepl() {} + + static int runInteractiveRepl() { + LineReader lineReader = null; + BufferedReader fallbackReader = null; + try { + Terminal terminal = TerminalBuilder.builder().system(true).build(); + lineReader = LineReaderBuilder.builder().terminal(terminal).build(); + } catch (Exception e) { + fallbackReader = new BufferedReader(new InputStreamReader(System.in, UTF_8)); + } + return runReplInternal(lineReader, fallbackReader, System.out, System.err); + } + + static int runRepl(BufferedReader reader, PrintStream out, PrintStream err) { + return runReplInternal(null, reader, out, err); + } + + private static int runReplInternal( + LineReader lineReader, BufferedReader fallbackReader, PrintStream out, PrintStream err) { + out.println("============================================================"); + out.println(" CEL Verification REPL"); + out.println(" Type :help for commands, :quit to exit."); + out.println("============================================================"); + + Map sessionVars = new HashMap<>(); + List unknownIdentifiers = new ArrayList<>(); + int timeoutSeconds = 10; + int unrollLimit = 5; + + String prompt = FormatUtils.ANSI_CYAN + "cel-verifier> " + FormatUtils.ANSI_RESET; + + while (true) { + String line; + try { + if (lineReader != null) { + line = lineReader.readLine(prompt); + } else if (fallbackReader != null) { + out.print(prompt); + out.flush(); + line = fallbackReader.readLine(); + if (line == null) { + break; // EOF + } + } else { + break; + } + } catch (UserInterruptException | EndOfFileException e) { + out.println("Goodbye!"); + break; + } catch (Exception e) { + err.println("Error reading input: " + e.getMessage()); + break; + } + + line = line.trim(); + if (line.isEmpty()) { + continue; + } + + if (line.startsWith(":")) { + if (Ascii.equalsIgnoreCase(line, ":quit") || Ascii.equalsIgnoreCase(line, ":exit")) { + out.println("Goodbye!"); + break; + } + + Optional helpArg = extractCommandArg(line, ":help"); + if (helpArg.isPresent()) { + printHelp(helpArg.get(), out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":vars")) { + printVars(sessionVars, unknownIdentifiers, timeoutSeconds, unrollLimit, out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":clear")) { + sessionVars.clear(); + unknownIdentifiers.clear(); + out.println("Session state reset."); + continue; + } + + Optional varArg = extractCommandArg(line, ":var"); + if (varArg.isPresent()) { + String arg = varArg.get(); + if (arg.isEmpty()) { + err.println( + "Usage: :var (e.g. :var role string, :var scores map)"); + } else { + handleVarCommand(arg, sessionVars, out, err); + } + continue; + } + + Optional unknownArg = extractCommandArg(line, ":unknown"); + if (unknownArg.isPresent()) { + String arg = unknownArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unknown "); + } else { + unknownIdentifiers.add(arg); + out.println("Added unknown identifier: '" + arg + "'"); + } + continue; + } + + Optional timeoutArg = extractCommandArg(line, ":timeout"); + if (timeoutArg.isPresent()) { + String arg = timeoutArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :timeout "); + } else { + try { + int t = Integer.parseInt(arg); + if (t <= 0) { + err.println("Timeout must be a positive integer."); + } else { + timeoutSeconds = t; + out.println("Timeout set to " + timeoutSeconds + "s."); + } + } catch (NumberFormatException e) { + err.println("Invalid timeout value."); + } + } + continue; + } + + Optional unrollArg = extractCommandArg(line, ":unroll"); + if (unrollArg.isPresent()) { + String arg = unrollArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unroll "); + } else { + try { + int u = Integer.parseInt(arg); + if (u < 0) { + err.println("Unroll limit must be non-negative."); + } else { + unrollLimit = u; + out.println("Comprehension unroll limit set to " + unrollLimit + "."); + } + } catch (NumberFormatException e) { + err.println("Invalid unroll limit value."); + } + } + continue; + } + + err.println("Unknown command: " + line + ". Type :help for commands."); + continue; + } + + // Handle queries + VerificationOptions options = + VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(unrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .build(); + + try { + Optional satArg = extractCommandArg(line, "sat"); + Optional validArg = extractCommandArg(line, "valid"); + Optional equivArg = extractCommandArg(line, "equiv"); + + if (satArg.isPresent()) { + String arg = satArg.get(); + if (arg.isEmpty()) { + err.println("Usage: sat "); + } else { + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (validArg.isPresent()) { + String arg = validArg.get(); + if (arg.isEmpty()) { + err.println("Usage: valid "); + } else { + CelVerificationResult res = CelVerifierToolCore.checkValid(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (equivArg.isPresent()) { + String arg = equivArg.get(); + ImmutableList parts = splitEquivQuery(arg); + if (parts.size() != 2 || parts.get(0).isEmpty() || parts.get(1).isEmpty()) { + err.println("Equivalence query format: equiv <=> "); + } else { + String exprA = parts.get(0).trim(); + String exprB = parts.get(1).trim(); + CelVerificationResult res = + CelVerifierToolCore.verifyEquivalence(exprA, exprB, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else { + // Default: treat as sat query + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(line, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } catch (CelValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (CelPolicyValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Policy compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (Exception e) { + err.println( + FormatUtils.ANSI_RED + + "Verification failed: " + + e.getMessage() + + FormatUtils.ANSI_RESET); + } + } + return 0; + } + + private static void handleVarCommand( + String arg, Map sessionVars, PrintStream out, PrintStream err) { + String[] parts = arg.split("\\s+", 2); + if (parts.length != 2) { + 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); + out.println("Variable declared: " + name + " : " + CelTypes.format(type)); + } catch (IllegalArgumentException e) { + err.println(e.getMessage()); + } + } + + private static void printVars( + Map sessionVars, + List unknowns, + int timeoutSeconds, + int unrollLimit, + PrintStream out) { + out.println("--- Session State ---"); + out.println("Timeout: " + timeoutSeconds + "s | Unroll limit: " + unrollLimit); + out.println("Unknowns: " + (unknowns.isEmpty() ? "none" : unknowns)); + out.println("Variables (" + sessionVars.size() + "):"); + for (Map.Entry entry : sessionVars.entrySet()) { + out.println(" " + entry.getKey() + " : " + CelTypes.format(entry.getValue())); + } + } + + private static void printHelp(String topic, PrintStream out) { + String t = topic.toLowerCase(Locale.US).replace(":", "").trim(); + switch (t) { + case "var": + case "vars": + out.println("Command: :var "); + out.println("Declares a variable in the REPL session with a specific type."); + out.println(); + out.println("Supported Types:"); + out.println(" - Primitive types: int, uint, string, bool, double, bytes"); + out.println(" - List types: list (e.g., list, list)"); + out.println(" - Map types: map (e.g., map, map)"); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :var role string"); + out.println(" cel-verifier> :var port int"); + out.println(" cel-verifier> :var scores map"); + out.println(" cel-verifier> :var tags list"); + break; + case "unknown": + out.println("Command: :unknown "); + out.println( + "Marks an identifier path as 'Unknown' during verification (partial evaluation)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unknown request.headers"); + out.println(" cel-verifier> :unknown request.auth.claims"); + break; + case "timeout": + out.println("Command: :timeout "); + out.println("Configures the Z3 solver soft timeout duration in seconds (default: 10s)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :timeout 5"); + break; + case "unroll": + out.println("Command: :unroll "); + out.println("Configures the BMC loop unroll limit for comprehensions (default: 5)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unroll 3"); + break; + case "sat": + out.println("Query: sat "); + out.println( + "Checks if a CEL expression can evaluate to true for any possible input assignments."); + out.println("If satisfiable, outputs concrete satisfying witness values."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> sat role == 'editor' && port > 1024"); + out.println(" cel-verifier> sat scores['alice'] > 90"); + break; + case "valid": + out.println("Query: valid "); + out.println( + "Proves whether a CEL expression evaluates to true for ALL possible input" + + " assignments."); + out.println("If invalid, outputs a counterexample showing inputs causing it to fail."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> valid x > 10 || x <= 10"); + break; + case "equiv": + out.println("Query: equiv <=> "); + out.println( + "Proves whether two CEL expressions are semantically identical for all inputs."); + out.println( + "If not equivalent, outputs a counterexample showing inputs where they diverge."); + out.println(); + out.println("Use '<=>' as the recommended separator between expressions."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> equiv x > 10 <=> 10 < x"); + out.println(" cel-verifier> equiv (a && b) || (a && c) <=> a && (b || c)"); + 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: + out.println("REPL Commands:"); + out.println( + " :var Declare variable (e.g. :var role string, :var m" + + " map)"); + out.println(" :unknown Mark identifier as unknown"); + out.println(" :timeout Set solver timeout (default: 10s)"); + out.println(" :unroll Set comprehension unroll limit (default: 5)"); + out.println(" :vars List session variables & options"); + out.println(" :clear Reset session state"); + out.println( + " :help [command] Display help message or specific command details"); + out.println(" :quit Exit REPL"); + out.println(); + out.println("Verification Queries:"); + out.println(" sat Check satisfiability"); + out.println(" valid Check validity (always true)"); + out.println(" equiv <=> Prove logical equivalence"); + out.println(" Check satisfiability (default)"); + out.println(); + out.println( + "Type ':help ' (e.g. ':help var', ':help sat') for detailed usage and" + + " examples."); + break; + } + } + + private static ImmutableList splitEquivQuery(String rest) { + if (rest == null || rest.trim().isEmpty()) { + return ImmutableList.of(); + } + String input = rest.trim(); + if (input.contains(" <=> ")) { + return ImmutableList.copyOf(input.split(" <=> ", 2)); + } + if (input.contains("<=>")) { + return ImmutableList.copyOf(input.split("<=>", 2)); + } + return ImmutableList.of(); + } + + private static Optional extractCommandArg(String line, String prefix) { + if (Ascii.equalsIgnoreCase(line, prefix)) { + return Optional.of(""); + } + String prefixLower = Ascii.toLowerCase(prefix); + String lineLower = Ascii.toLowerCase(line); + if (lineLower.startsWith(prefixLower + " ") || lineLower.startsWith(prefixLower + "\t")) { + return Optional.of(line.substring(prefix.length()).trim()); + } + return Optional.empty(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java index 8289b9f77..963e966eb 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java @@ -43,12 +43,13 @@ name = "cel-verifier", mixinStandardHelpOptions = true, versionProvider = CelVerifierTool.VersionProvider.class, - description = "CEL-Java Formal Verification CLI Tool", + description = "CEL-Java Formal Verification CLI & REPL Tool", subcommands = { CelVerifierTool.CheckSatCommand.class, CelVerifierTool.CheckValidCommand.class, CelVerifierTool.VerifyEquivCommand.class, - CelVerifierTool.VerifyPolicyCommand.class + CelVerifierTool.VerifyPolicyCommand.class, + CelVerifierTool.ReplCommand.class }) public final class CelVerifierTool implements Runnable { @@ -296,6 +297,15 @@ private static int getPolicyExitCode(ImmutableMap } } + @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/VerificationOptions.java b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java index 91ec443a5..f2b3bf742 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -135,6 +135,10 @@ static ImmutableMap parseVariables(List varSpecs) { + "'. Expected format 'name:type' (e.g., 'x:int')."); } String name = parts[0].trim(); + if (name.isEmpty()) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + varSpec + "'. Variable name cannot be empty."); + } String typeStr = parts[1].trim().toLowerCase(Locale.US); CelType type = parseCelType(typeStr); vars.put(name, type); diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java new file mode 100644 index 000000000..52124c6ed --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -0,0 +1,188 @@ +// 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 static java.nio.charset.StandardCharsets.UTF_8; + +import java.io.BufferedReader; +import java.io.ByteArrayOutputStream; +import java.io.PrintStream; +import java.io.StringReader; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class CelVerifierReplTest { + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + @SuppressWarnings({"PreferCharsetOverload", "JdkObsolete"}) + private String[] runReplWithCommands(String... commands) throws Exception { + String input = String.join("\n", commands) + "\n"; + BufferedReader reader = new BufferedReader(new StringReader(input)); + ByteArrayOutputStream outStream = new ByteArrayOutputStream(); + ByteArrayOutputStream errStream = new ByteArrayOutputStream(); + PrintStream out = new PrintStream(outStream, true, UTF_8.name()); + PrintStream err = new PrintStream(errStream, true, UTF_8.name()); + + CelVerifierRepl.runRepl(reader, out, err); + + return new String[] { + new String(outStream.toByteArray(), UTF_8), new String(errStream.toByteArray(), UTF_8) + }; + } + + @Test + public void repl_quitAndExit() throws Exception { + String[] output1 = runReplWithCommands(":quit"); + assertThat(output1[0]).contains("Goodbye!"); + + String[] output2 = runReplWithCommands(":exit"); + assertThat(output2[0]).contains("Goodbye!"); + } + + @Test + public void repl_helpCommands() throws Exception { + String[] output = + runReplWithCommands( + ":help", + ":help var", + ":help unknown", + ":help timeout", + ":help unroll", + ":help sat", + ":help valid", + ":help equiv", + ":help non_existent_topic", + ":quit"); + assertThat(output[0]).contains("REPL Commands:"); + assertThat(output[0]).contains("Command: :var "); + assertThat(output[0]).contains("Command: :unknown "); + assertThat(output[0]).contains("Command: :timeout "); + assertThat(output[0]).contains("Command: :unroll "); + assertThat(output[0]).contains("Query: sat "); + assertThat(output[0]).contains("Query: valid "); + assertThat(output[0]).contains("Query: equiv <=> "); + } + + @Test + public void repl_varDeclarations() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", + ":var port int", + ":var scores map", + ":var tags list", + ":vars", + ":quit"); + assertThat(output[0]).contains("Variable declared: role : string"); + assertThat(output[0]).contains("Variable declared: port : int"); + assertThat(output[0]).contains("Variable declared: scores : map(string, int)"); + assertThat(output[0]).contains("Variable declared: tags : list(string)"); + assertThat(output[0]).contains("Variables (4):"); + } + + @Test + public void repl_unknownIdentifiers() throws Exception { + String[] output = + runReplWithCommands(":unknown request.headers", ":unknown request.auth", ":vars", ":quit"); + assertThat(output[0]).contains("Added unknown identifier: 'request.headers'"); + assertThat(output[0]).contains("Added unknown identifier: 'request.auth'"); + assertThat(output[0]).contains("Unknowns: [request.headers, request.auth]"); + } + + @Test + public void repl_timeoutConfiguration() throws Exception { + String[] output = + runReplWithCommands( + ":timeout 15", ":vars", ":timeout -5", ":timeout abc", ":timeout", ":quit"); + assertThat(output[0]).contains("Timeout set to 15s."); + assertThat(output[0]).contains("Timeout: 15s"); + assertThat(output[1]).contains("Timeout must be a positive integer."); + assertThat(output[1]).contains("Invalid timeout value."); + assertThat(output[1]).contains("Usage: :timeout "); + } + + @Test + public void repl_unrollConfiguration() throws Exception { + String[] output = + runReplWithCommands(":unroll 10", ":vars", ":unroll -1", ":unroll xyz", ":unroll", ":quit"); + assertThat(output[0]).contains("Comprehension unroll limit set to 10."); + assertThat(output[0]).contains("Unroll limit: 10"); + assertThat(output[1]).contains("Unroll limit must be non-negative."); + assertThat(output[1]).contains("Invalid unroll limit value."); + assertThat(output[1]).contains("Usage: :unroll "); + } + + @Test + public void repl_sessionStateAndClear() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", ":unknown req.headers", ":vars", ":clear", ":vars", ":quit"); + assertThat(output[0]).contains("Variables (1):"); + assertThat(output[0]).contains("Session state reset."); + assertThat(output[0]).contains("Variables (0):"); + assertThat(output[0]).contains("Unknowns: none"); + } + + @Test + public void repl_satQueries() throws Exception { + String[] output = + runReplWithCommands(":var port int", "sat port > 1024", "port > 1024", "sat", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Usage: sat "); + } + + @Test + public void repl_validQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "valid x > 0 || x <= 0", "valid x > 0", "valid", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[0]).contains("[VIOLATED]"); + assertThat(output[1]).contains("Usage: valid "); + } + + @Test + public void repl_equivQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "equiv x > 10 <=> 10 < x", "equiv x > 10", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Equivalence query format: equiv <=> "); + } + + @Test + public void repl_unknownCommandsAndErrors() throws Exception { + String[] output = + runReplWithCommands( + ":unknowncommand", + ":var", + ":var invalid_spec", + ":var x foo_type", + ":unknown", + "invalid + + syntax", + ":quit"); + assertThat(output[1]).contains("Unknown command: :unknowncommand"); + assertThat(output[1]).contains("Usage: :var "); + assertThat(output[1]).contains("Unsupported type"); + assertThat(output[1]).contains("Usage: :unknown "); + assertThat(output[1]).contains("Compilation error"); + } +} diff --git a/verifier/tools/README.md b/verifier/tools/README.md index f2cfa2528..398cbad74 100644 --- a/verifier/tools/README.md +++ b/verifier/tools/README.md @@ -105,3 +105,87 @@ Set CLI output format (`TEXT` or `JSON`, default: `TEXT`): * `1`: Violation or counterexample found. * `2`: Inconclusive result (solver unknown or timeout). * `3`: Error (syntax compilation error, missing file, or execution error). + +## Interactive REPL Shell + +The REPL shell provides an interactive, stateful environment to execute CEL +formal verification queries without re-declaring variables or re-running CLI +parameters for every query. + +### Launching the REPL + +```bash +bazel run //verifier/tools:cel_verifier_tool -- repl +``` + +### REPL Commands + +| Command | Description | Example | +|---|---|---| +| `:var ` | Declare a variable in session state | `:var role string` | +| `:unknown ` | Mark identifier as Unknown | `:unknown request.headers` | +| `:timeout ` | Set Z3 solver timeout in seconds (default: 10s) | `:timeout 5` | +| `:unroll ` | Set comprehension unroll limit (default: 5) | `:unroll 3` | +| `:vars` | Display declared session variables & config | `:vars` | +| `:clear` | Reset session state (clears variables & unknowns) | `:clear` | +| `:help [cmd]` | Display built-in help or command details | `:help var` | +| `:quit` / `:exit` | Exit the interactive REPL shell | `:quit` | + +### Verification Queries in REPL + +* **Satisfiability (`sat ` or ``):** Checks if the expression + can evaluate to `true` for any assignment of session variables. Outputs + satisfying witness inputs if satisfiable. +* **Validity (`valid `):** Proves whether the expression evaluates + to `true` for ALL possible variable assignments. Outputs a counterexample + if invalid. +* **Equivalence (`equiv <=> `):** Proves whether two + expressions are logically identical across all inputs. Outputs a + counterexample if not equivalent. + +### Example REPL Session + +```text +============================================================ + CEL Verification REPL + Type :help for commands, :quit to exit. +============================================================ +cel-verifier> :var port int +Variable declared: port : int + +cel-verifier> sat role == 'admin' && port > 1024 + +cel-verifier> :var role string +Variable declared: role : string + +cel-verifier> sat role == 'admin' && port > 1024 +[VERIFIED] Condition is satisfiable. Satisfying input: + role = "admin" + port = 1025 + +cel-verifier> valid port > 0 || port <= 0 +[VERIFIED] + +cel-verifier> valid port > 1024 +[VIOLATED] Condition is violated. Counterexample input: + port = 0 + +cel-verifier> equiv port > 10 <=> 10 < port +[VERIFIED] + +cel-verifier> :vars +--- Session State --- +Timeout: 10s | Unroll limit: 5 +Unknowns: none +Variables (2): + role : string + port : int + +cel-verifier> :quit +Goodbye! +``` + +> **Note:** Inline help is built into the REPL shell. Type `:help` or +> `:help ` (e.g. `:help var`, `:help equiv`) at any prompt for +> detailed usage instructions and examples. +