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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
copybara-service merged 1 commit into from
Aug 1, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 4 additions & 9 deletions common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down
2 changes: 1 addition & 1 deletion verifier/README.md
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down
1 change: 1 addition & 0 deletions verifier/src/main/java/dev/cel/verifier/BUILD.bazel
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down
17 changes: 17 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down
4 changes: 4 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down
33 changes: 17 additions & 16 deletions verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
}
}

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down
105 changes: 94 additions & 11 deletions verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
}
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
}

/**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
return ctx.mkITE(condition, mkError(), result);
}

Constructor unknownCons() {
public Constructor unknownCons() {
return unknownCons;
}

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

copybara-service
merged 1 commit into

from

Aug 1, 2026
 Merged


Introduce timestamp/duration as first class types in verifier. Add arithmetic axioms for the two types along with type conversions
#1153
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


13 changes: 4 additions & 9 deletions
common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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;

Expand Down

2 changes: 1 addition & 1 deletion
verifier/README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand Down

1 change: 1 addition & 0 deletions
verifier/src/main/java/dev/cel/verifier/BUILD.bazel

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

17 changes: 17 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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);
Expand DownExpand Up@@ -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.
Expand Down

4 changes: 4 additions & 0 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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())) {
Expand Down

33 changes: 17 additions & 16 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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:
Expand DownExpand Up@@ -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));
 }
 }

Expand All@@ -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)
Expand DownExpand Up@@ -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) {
Expand DownExpand Up@@ -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());
Expand Down

105 changes: 94 additions & 11 deletions
verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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;
Expand DownExpand Up@@ -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";

Expand DownExpand Up@@ -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;
Expand DownExpand Up@@ -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;
 }
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -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);
 }

 /**
Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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));
Expand DownExpand Up@@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
 return ctx.mkITE(condition, mkError(), result);
 }

 Constructor unknownCons() {
public Constructor unknownCons() {
 return unknownCons;
 }

Expand DownExpand Up@@ -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);
Expand DownExpand Up@@ -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)));
Expand DownExpand Up@@ -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");
Expand DownExpand Up@@ -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,
Expand Down
Loading
Loading