Add timestamp, duration and optional types to CEL Verifier CLI

PiperOrigin-RevId: 960433430

Author: l46kok

verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

@@ -88,7 +88,7 @@ private static String formatExpr(
     } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
       return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
     } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
-      return "duration(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
+      return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
     } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
       return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
     } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {

verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java

@@ -314,15 +314,21 @@ private static void printHelp(String topic, PrintStream out) {
         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<T> (e.g., list<int>, list<string>)");
-        out.println("  - Map types:       map<K,V> (e.g., map<string,int>, map<string,string>)");
+        out.println("  - Primitive types:  int, uint, string, bool, double, bytes, dyn");
+        out.println("  - Well-known types: timestamp, duration");
+        out.println("  - List types:       list<T> (e.g., list<int>, list<string>)");
+        out.println("  - Map types:        map<K,V> (e.g., map<string,int>, map<string,string>)");
+        out.println("  - Optional types:   optional<T> (e.g., optional<string>, optional<int>)");
+        out.println("  - Protobuf types:   coming soon");
         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<string,int>");
         out.println("  cel-verifier> :var tags list<string>");
+        out.println("  cel-verifier> :var created_at timestamp");
+        out.println("  cel-verifier> :var timeout duration");
+        out.println("  cel-verifier> :var opt_flag optional<bool>");
         break;
       case "unknown":
         out.println("Command: :unknown <identifier>");

verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java

@@ -21,6 +21,7 @@
 import dev.cel.common.types.CelType;
 import dev.cel.common.types.ListType;
 import dev.cel.common.types.MapType;
+import dev.cel.common.types.OptionalType;
 import dev.cel.common.types.SimpleType;
 import java.time.Duration;
 import java.util.ArrayList;
@@ -147,17 +148,20 @@ static ImmutableMap<String, CelType> parseVariables(List<String> varSpecs) {
   }
 
   static CelType parseCelType(String typeStr) {
+    // TODO: Replace with shorthand type parser once it is available.
     Preconditions.checkNotNull(typeStr, "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();
+      // Strip "list<" prefix and trailing ">" to extract the element type "T".
+      String inner = str.substring("list<".length(), str.length() - 1).trim();
       CelType elemType = parseCelType(inner);
       return ListType.create(elemType);
     }
 
     if (str.startsWith("map<") && str.endsWith(">")) {
-      String inner = str.substring(4, str.length() - 1).trim();
+      // Strip "map<" prefix and trailing ">" to extract the key and value types "K, V".
+      String inner = str.substring("map<".length(), str.length() - 1).trim();
       List<String> parts = splitGenericArgs(inner);
       if (parts.size() != 2) {
         throw new IllegalArgumentException(
@@ -170,6 +174,20 @@ static CelType parseCelType(String typeStr) {
       return MapType.create(keyType, valueType);
     }
 
+    if (str.startsWith("optional<") && str.endsWith(">")) {
+      // Strip "optional<" prefix and trailing ">" to extract the wrapped type "T".
+      String inner = str.substring("optional<".length(), str.length() - 1).trim();
+      CelType elemType = parseCelType(inner);
+      return OptionalType.create(elemType);
+    }
+
+    if (str.startsWith("optional_type<") && str.endsWith(">")) {
+      // Strip "optional_type<" prefix and trailing ">" to extract the wrapped type "T".
+      String inner = str.substring("optional_type<".length(), str.length() - 1).trim();
+      CelType elemType = parseCelType(inner);
+      return OptionalType.create(elemType);
+    }
+
     switch (str) {
       case "int":
         return SimpleType.INT;
@@ -187,12 +205,19 @@ static CelType parseCelType(String typeStr) {
         return SimpleType.BYTES;
       case "dyn":
         return SimpleType.DYN;
+      case "timestamp":
+      case "google.protobuf.timestamp":
+        return SimpleType.TIMESTAMP;
+      case "duration":
+      case "google.protobuf.duration":
+        return SimpleType.DURATION;
       default:
+        // TODO: Support protobuf message types (coming soon).
         throw new IllegalArgumentException(
             "Unsupported type for CLI variable declaration: '"
                 + typeStr
-                + "'. Supported types: int, uint, string, bool, double, bytes, dyn, list<T>, map<K,"
-                + " V>.");
+                + "'. Supported types: int, uint, string, bool, double, bytes, dyn, timestamp,"
+                + " duration, list<T>, map<K, V>, optional<T>.");
     }
   }
 

verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java

@@ -1312,7 +1312,7 @@ private enum IsAlwaysTrueViolationTestCase {
         "dur != dur",
         "Condition is not always true\\.",
         "Counterexample input:",
-        "dur = duration\\(-?\\d+\\)"),
+        "dur = duration\\('-?\\d+s'\\)"),
     TIMESTAMP_VARIABLE_COUNTEREXAMPLE(
         "ts != ts",
         "Condition is not always true\\.",

verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java

@@ -53,9 +53,11 @@ private String[] runReplWithCommands(String... commands) throws Exception {
   @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!");
   }
 
@@ -73,6 +75,7 @@ public void repl_helpCommands() throws Exception {
             ":help equiv",
             ":help non_existent_topic",
             ":quit");
+
     assertThat(output[0]).contains("REPL Commands:");
     assertThat(output[0]).contains("Command: :var <name> <type>");
     assertThat(output[0]).contains("Command: :unknown <identifier>");
@@ -81,6 +84,9 @@ public void repl_helpCommands() throws Exception {
     assertThat(output[0]).contains("Query: sat <expression>");
     assertThat(output[0]).contains("Query: valid <expression>");
     assertThat(output[0]).contains("Query: equiv <expression1> <=> <expression2>");
+    assertThat(output[0]).contains("Well-known types: timestamp, duration");
+    assertThat(output[0]).contains("Optional types:   optional<T>");
+    assertThat(output[0]).contains("Protobuf types:   coming soon");
   }
 
   @Test
@@ -91,19 +97,27 @@ public void repl_varDeclarations() throws Exception {
             ":var port int",
             ":var scores map<string,int>",
             ":var tags list<string>",
+            ":var created_at timestamp",
+            ":var timeout duration",
+            ":var opt_user optional<string>",
             ":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):");
+    assertThat(output[0]).contains("Variable declared: created_at : google.protobuf.Timestamp");
+    assertThat(output[0]).contains("Variable declared: timeout : google.protobuf.Duration");
+    assertThat(output[0]).contains("Variable declared: opt_user : optional_type(string)");
+    assertThat(output[0]).contains("Variables (7):");
   }
 
   @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]");
@@ -114,6 +128,7 @@ 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.");
@@ -125,6 +140,7 @@ public void repl_timeoutConfiguration() throws Exception {
   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.");
@@ -137,6 +153,7 @@ 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):");
@@ -147,6 +164,7 @@ public void repl_sessionStateAndClear() throws Exception {
   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 <expression>");
   }
@@ -155,6 +173,7 @@ public void repl_satQueries() throws Exception {
   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 <expression>");
@@ -164,13 +183,15 @@ public void repl_validQueries() throws Exception {
   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 <expr1> <=> <expr2>");
   }
 
   @Test
   public void repl_equivDoubleNegation() throws Exception {
     String[] output = runReplWithCommands(":var x int", "equiv !!(x == 10) <=> (x == 10)", ":quit");
+
     assertThat(output[0]).contains("[VERIFIED]");
   }
 
@@ -184,6 +205,45 @@ public void repl_equivCanonicalization() throws Exception {
                 + " v, v == 1 && k == 'foo')",
             "equiv int_list.all(e, e > 0) <=> int_list.all(elem, elem > 0)",
             ":quit");
+
+    assertThat(output[0]).contains("[VERIFIED]");
+    assertThat(output[1]).isEmpty();
+  }
+
+  @Test
+  public void repl_timestampAndDurationQueries() throws Exception {
+    String[] output =
+        runReplWithCommands(
+            ":var t timestamp",
+            ":var d duration",
+            "sat t > timestamp(1000)",
+            "sat d > duration('60s')",
+            "sat t + d > timestamp(2000)",
+            ":quit");
+
+    assertThat(output[0]).contains("[VERIFIED]");
+    assertThat(output[1]).isEmpty();
+  }
+
+  @Test
+  public void repl_durationSatisfyingInputFormat() throws Exception {
+    String[] output =
+        runReplWithCommands(":var dur duration", "timestamp(100) - timestamp(50) == dur", ":quit");
+
+    assertThat(output[0]).contains("[VERIFIED]");
+    assertThat(output[0]).contains("dur = duration('50s')");
+    assertThat(output[1]).isEmpty();
+  }
+
+  @Test
+  public void repl_optionalQueries() throws Exception {
+    String[] output =
+        runReplWithCommands(
+            ":var opt_val optional<int>",
+            "sat opt_val.hasValue() && opt_val.value() > 100",
+            "sat !opt_val.hasValue()",
+            ":quit");
+
     assertThat(output[0]).contains("[VERIFIED]");
     assertThat(output[1]).isEmpty();
   }
@@ -199,6 +259,7 @@ public void repl_unknownCommandsAndErrors() throws Exception {
             ":unknown",
             "invalid + + syntax",
             ":quit");
+
     assertThat(output[1]).contains("Unknown command: :unknowncommand");
     assertThat(output[1]).contains("Usage: :var <name> <type>");
     assertThat(output[1]).contains("Unsupported type");