Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions

PiperOrigin-RevId: 957414761

Author: l46kok

common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

@@ -18,7 +18,6 @@
 import static com.google.common.math.LongMath.checkedMultiply;
 import static com.google.common.math.LongMath.checkedSubtract;
 
-import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.Strings;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import com.google.protobuf.Duration;
@@ -50,15 +49,11 @@
 public final class ProtoTimeUtils {
 
   // Timestamp for "0001-01-01T00:00:00Z"
-  @VisibleForTesting
-  static final long TIMESTAMP_SECONDS_MIN = -62135596800L;
+  public static final long TIMESTAMP_SECONDS_MIN = -62135596800L;
   // Timestamp for "9999-12-31T23:59:59Z"
-  @VisibleForTesting
-  static final long TIMESTAMP_SECONDS_MAX = 253402300799L;
-  @VisibleForTesting
-  static final long DURATION_SECONDS_MIN = -315576000000L;
-  @VisibleForTesting
-  static final long DURATION_SECONDS_MAX = 315576000000L;
+  public static final long TIMESTAMP_SECONDS_MAX = 253402300799L;
+  public static final long DURATION_SECONDS_MIN = -315576000000L;
+  public static final long DURATION_SECONDS_MAX = 315576000000L;
 
   private static final int MILLIS_PER_SECOND = 1000;
 

verifier/README.md

@@ -400,7 +400,7 @@ public class InvariantsExample {
 
 ### Timeouts
 
-SMT solving is NP-complete and can theoretically stop responding or take an
+SMT solving is NP-hard and can theoretically stop responding or take an
 exponential amount of time for complex formulas.
 The verifier uses a default timeout of 10 seconds. It is recommended to
 configure this to a reasonable duration for your specific use case using

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

@@ -98,6 +98,7 @@ java_library(
     tags = [
     ],
     deps = [
+        "//common/internal:proto_time_utils",
         "@maven//:com_google_errorprone_error_prone_annotations",
         "@maven//:com_google_guava_guava",
         "@maven//:tools_aqua_z3_turnkey",

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

@@ -533,6 +533,12 @@ private Expr<?> getDefaultValueForType(CelType type) {
     if (type.equals(SimpleType.UINT)) {
       return typeSystem.mkUint(0);
     }
+    if (type.equals(SimpleType.TIMESTAMP)) {
+      return typeSystem.wrapTimestamp(ctx.mkInt(0));
+    }
+    if (type.equals(SimpleType.DURATION)) {
+      return typeSystem.wrapDuration(ctx.mkInt(0));
+    }
     if (type instanceof ListType) {
       if (emptyListCache == null) {
         emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX);
@@ -1269,6 +1275,17 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
     if (type.equals(SimpleType.BYTES)) {
       return (BoolExpr) ctx.mkApp(typeSystem.bytesCons().getTesterDecl(), val);
     }
+    if (type.equals(SimpleType.TIMESTAMP)) {
+      IntExpr seconds = typeSystem.getTimestamp(val);
+      return ctx.mkAnd(
+          typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
+    }
+    if (type.equals(SimpleType.DURATION)) {
+      IntExpr seconds = typeSystem.getDuration(val);
+      return ctx.mkAnd(
+          typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
+    }
+
     if (type instanceof ListType) {
       // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers
       // here.

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

@@ -82,6 +82,10 @@ private static String formatExpr(
     // Handle CelType constructors wrapper unwrapping
     if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
       return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
+    } 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]) + ")";
     } 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/CelZ3OperatorTranslator.java

@@ -148,11 +148,11 @@ private BoolExpr mkTypeGuard(Expr<?> arg, CelType expectedType) {
         // These match everything structurally type-wise, although we might refine this later.
         return ctx.mkTrue();
       case INT:
+        return typeSystem.isInt(arg);
       case TIMESTAMP:
+        return typeSystem.isTimestamp(arg);
       case DURATION:
-        // Safe to map int, timestamp, and duration to IntSort because CEL's static checker prevents
-        // invalid cross-type usage and their operator axioms translate to identical Z3 ASTs.
-        return typeSystem.isInt(arg);
+        return typeSystem.isDuration(arg);
       case UINT:
         return typeSystem.isUint(arg);
       case DOUBLE:
@@ -386,7 +386,7 @@ private BoolExpr getNumericEqualityWithConstant(
             ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal))
             : ctx.mkFalse();
       } else if (symType.kind() == CelKind.DOUBLE) {
-        return ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
+        return ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
       }
     }
 
@@ -396,8 +396,7 @@ private BoolExpr getNumericEqualityWithConstant(
         (uintVal != null)
             ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal))
             : ctx.mkFalse();
-    BoolExpr doubleEq =
-        ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
+    BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
 
     return (BoolExpr)
         CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
@@ -435,18 +434,17 @@ private BoolExpr getStaticallyKnownNumericEquality(
       case UINT:
         return ctx.mkEq(typeSystem.getUint(z3Expr0), typeSystem.getUint(z3Expr1));
       case DOUBLE:
-        return ctx.mkFPEq(
-            (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1));
+        return ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1));
       default:
         return ctx.mkFalse();
     }
   }
 
   private BoolExpr mkIsFiniteDouble(Expr<?> z3Expr) {
-    Expr<?> fpVal = typeSystem.getDouble(z3Expr);
+    FPExpr fpVal = typeSystem.getDouble(z3Expr);
     return ctx.mkAnd(
         typeSystem.isDouble(z3Expr),
-        ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN((FPExpr) fpVal), ctx.mkFPIsInfinite((FPExpr) fpVal))));
+        ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN(fpVal), ctx.mkFPIsInfinite(fpVal))));
   }
 
   private BoolExpr getDynamicNumericEquality(Expr<?> z3Expr0, Expr<?> z3Expr1) {
@@ -475,25 +473,28 @@ private BoolExpr getDynamicNumericEquality(Expr<?> z3Expr0, Expr<?> z3Expr1) {
     BoolExpr isIntOrUintAndDouble = ctx.mkAnd(isIntOrUint0, typeSystem.isDouble(z3Expr1));
     BoolExpr isDoubleAndIntOrUint = ctx.mkAnd(typeSystem.isDouble(z3Expr0), isIntOrUint1);
 
-    Expr<?> fpVal1 = typeSystem.getDouble(z3Expr1);
+    FPExpr fpVal1 = typeSystem.getDouble(z3Expr1);
+    ArithExpr<?> realVal0 = ctx.mkInt2Real(val0);
     BoolExpr intDoubleEq =
         ctx.mkAnd(
             mkIsFiniteDouble(z3Expr1),
-            ctx.mkEq(ctx.mkInt2Real(val0), ctx.mkFPToReal((FPExpr) fpVal1)));
+            ctx.mkLe(realVal0, ctx.mkFPToReal(fpVal1)),
+            ctx.mkLe(ctx.mkFPToReal(fpVal1), realVal0));
 
-    Expr<?> fpVal0 = typeSystem.getDouble(z3Expr0);
+    FPExpr fpVal0 = typeSystem.getDouble(z3Expr0);
+    ArithExpr<?> realVal1 = ctx.mkInt2Real(val1);
     BoolExpr doubleIntEq =
         ctx.mkAnd(
             mkIsFiniteDouble(z3Expr0),
-            ctx.mkEq(ctx.mkFPToReal((FPExpr) fpVal0), ctx.mkInt2Real(val1)));
+            ctx.mkLe(realVal1, ctx.mkFPToReal(fpVal0)),
+            ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1));
 
     return (BoolExpr)
         CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
             .addCase(bothIntOrUint, ctx.mkEq(val0, val1))
             .addCase(
                 bothDouble,
-                ctx.mkFPEq(
-                    (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1)))
+                ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1)))
             .addCase(isIntOrUintAndDouble, intDoubleEq)
             .addCase(isDoubleAndIntOrUint, doubleIntEq)
             .build(ctx.mkFalse());

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

@@ -31,6 +31,7 @@
 import com.microsoft.z3.SeqExpr;
 import com.microsoft.z3.SeqSort;
 import com.microsoft.z3.Sort;
+import dev.cel.common.internal.ProtoTimeUtils;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collection;
@@ -82,6 +83,14 @@ public final class CelZ3TypeSystem {
   private static final String IS_BYTES = "isBytes";
   private static final String GET_BYTES = "getBytes";
 
+  private static final String CONS_TIMESTAMP = "Timestamp";
+  private static final String IS_TIMESTAMP = "isTimestamp";
+  private static final String GET_TIMESTAMP = "getTimestamp";
+
+  private static final String CONS_DURATION = "Duration";
+  private static final String IS_DURATION = "isDuration";
+  private static final String GET_DURATION = "getDuration";
+
   private static final String CONS_ERROR = "CelError";
   private static final String IS_ERROR = "isError";
 
@@ -170,6 +179,8 @@ public int hashCode() {
   private final Constructor doubleCons;
   private final Constructor stringCons;
   private final Constructor bytesCons;
+  private final Constructor timestampCons;
+  private final Constructor durationCons;
   private final Constructor errorCons;
   private final Constructor unknownCons;
   private final Constructor nullCons;
@@ -233,30 +244,38 @@ public Sort listRefSort() {
     return listRefSort;
   }
 
-  Constructor boolCons() {
+  public Constructor boolCons() {
     return boolCons;
   }
 
-  Constructor intCons() {
+  public Constructor intCons() {
     return intCons;
   }
 
-  Constructor uintCons() {
+  public Constructor uintCons() {
     return uintCons;
   }
 
-  Constructor doubleCons() {
+  public Constructor doubleCons() {
     return doubleCons;
   }
 
-  Constructor stringCons() {
+  public Constructor stringCons() {
     return stringCons;
   }
 
-  Constructor bytesCons() {
+  public Constructor bytesCons() {
     return bytesCons;
   }
 
+  public Constructor timestampCons() {
+    return timestampCons;
+  }
+
+  public Constructor durationCons() {
+    return durationCons;
+  }
+
   Constructor optionalCons() {
     return optionalCons;
   }
@@ -296,6 +315,16 @@ public Expr<?> wrapBytes(Expr<?> expr) {
     return ctx.mkApp(bytesCons.ConstructorDecl(), expr);
   }
 
+  /** Wraps a Z3 integer expression into a timestamp CelValue. */
+  public Expr<?> wrapTimestamp(IntExpr expr) {
+    return ctx.mkApp(timestampCons.ConstructorDecl(), expr);
+  }
+
+  /** Wraps a Z3 integer expression into a duration CelValue. */
+  public Expr<?> wrapDuration(IntExpr expr) {
+    return ctx.mkApp(durationCons.ConstructorDecl(), expr);
+  }
+
   /** Creates a CelValue containing an integer. */
   public Expr<?> mkInt(long val) {
     return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val));
@@ -326,8 +355,8 @@ public BoolExpr isDouble(Expr<?> val) {
   }
 
   /** Extracts the double reference from a double CelValue. */
-  public Expr<?> getDouble(Expr<?> val) {
-    return ctx.mkApp(doubleCons.getAccessorDecls()[0], val);
+  public FPExpr getDouble(Expr<?> val) {
+    return (FPExpr) ctx.mkApp(doubleCons.getAccessorDecls()[0], val);
   }
 
   /**
@@ -372,7 +401,7 @@ public BoolExpr getStructuralEquality(Expr<?> arg0, Expr<?> arg1) {
     // Doubles must be compared using native floating-point equality to follow IEEE-754.
     // Z3's structural mkEq evaluates NaN == NaN as true and 0.0 == -0.0 as false.
     BoolExpr isDoubleEq = ctx.mkAnd(isDouble(arg0), isDouble(arg1));
-    BoolExpr doubleEq = ctx.mkFPEq((FPExpr) getDouble(arg0), (FPExpr) getDouble(arg1));
+    BoolExpr doubleEq = ctx.mkFPEq(getDouble(arg0), getDouble(arg1));
 
     // For primitives, generic equality matches the direct Z3 datatype wrapper.
     BoolExpr genericEq = ctx.mkEq(arg0, arg1);
@@ -409,10 +438,14 @@ public Expr<?> mkNull() {
     return ctx.mkConst(nullCons.ConstructorDecl());
   }
 
-  Constructor errorCons() {
+  public Constructor errorCons() {
     return errorCons;
   }
 
+  public Constructor nullCons() {
+    return nullCons;
+  }
+
   /** Creates a CelValue representing an unknown value. */
   public Expr<?> mkUnknown() {
     return mkUnknown(ctx.mkConst(GENERIC_UNKNOWN_ID, unknownIdSort));
@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
     return ctx.mkITE(condition, mkError(), result);
   }
 
-  Constructor unknownCons() {
+  public Constructor unknownCons() {
     return unknownCons;
   }
 
@@ -582,6 +615,26 @@ public IntExpr getUint(Expr<?> val) {
     return (IntExpr) ctx.mkApp(uintCons.getAccessorDecls()[0], val);
   }
 
+  /** Checks if the given CelValue is a timestamp. */
+  public BoolExpr isTimestamp(Expr<?> val) {
+    return (BoolExpr) ctx.mkApp(timestampCons.getTesterDecl(), val);
+  }
+
+  /** Extracts the integer expression from a timestamp CelValue. */
+  public IntExpr getTimestamp(Expr<?> val) {
+    return (IntExpr) ctx.mkApp(timestampCons.getAccessorDecls()[0], val);
+  }
+
+  /** Checks if the given CelValue is a duration. */
+  public BoolExpr isDuration(Expr<?> val) {
+    return (BoolExpr) ctx.mkApp(durationCons.getTesterDecl(), val);
+  }
+
+  /** Extracts the integer expression from a duration CelValue. */
+  public IntExpr getDuration(Expr<?> val) {
+    return (IntExpr) ctx.mkApp(durationCons.getAccessorDecls()[0], val);
+  }
+
   /** Checks if the given CelValue is a string. */
   public BoolExpr isString(Expr<?> val) {
     return (BoolExpr) ctx.mkApp(stringCons.getTesterDecl(), val);
@@ -719,6 +772,20 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
     return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64)));
   }
 
+  /** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
+  public BoolExpr checkTimestampOverflow(ArithExpr result) {
+    return ctx.mkOr(
+        ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)),
+        ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)));
+  }
+
+  /** Checks if the given arithmetic expression overflows CEL Duration bounds. */
+  public BoolExpr checkDurationOverflow(ArithExpr result) {
+    return ctx.mkOr(
+        ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MAX)),
+        ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MIN)));
+  }
+
   /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */
   public BoolExpr checkUintOverflow(ArithExpr result) {
     return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0)));
@@ -890,6 +957,20 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
     this.bytesCons =
         ctx.mkConstructor(
             CONS_BYTES, IS_BYTES, new String[] {GET_BYTES}, new Sort[] {ctx.getStringSort()}, null);
+    this.timestampCons =
+        ctx.mkConstructor(
+            CONS_TIMESTAMP,
+            IS_TIMESTAMP,
+            new String[] {GET_TIMESTAMP},
+            new Sort[] {ctx.getIntSort()},
+            null);
+    this.durationCons =
+        ctx.mkConstructor(
+            CONS_DURATION,
+            IS_DURATION,
+            new String[] {GET_DURATION},
+            new Sort[] {ctx.getIntSort()},
+            null);
     this.errorCons = ctx.mkConstructor(CONS_ERROR, IS_ERROR, null, null, null);
 
     this.unknownIdSort = ctx.mkUninterpretedSort("UnknownId");
@@ -936,6 +1017,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
               this.doubleCons,
               this.stringCons,
               this.bytesCons,
+              this.timestampCons,
+              this.durationCons,
               this.errorCons,
               this.unknownCons,
               this.optionalCons,