Skip to content

Support protobuf Timestamp and Duration Well-Known Types with nanosecond precision in CelVerifier. #1374

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
Oct 21, 2026
Merged

Support protobuf Timestamp and Duration Well-Known Types with nanosecond precision in CelVerifier. #1374

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
117 changes: 112 additions & 5 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Iterables;
import com.google.common.collect.Streams;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.ArrayExpr;
import com.microsoft.z3.BoolExpr;
Expand Down Expand Up @@ -83,6 +84,8 @@ final class CelAstToZ3Translator {
private static final String EMPTY_LIST_PREFIX = "!empty_list";
private static final String EMPTY_MAP_PREFIX = "!empty_map";
private static final String NULL_VALUE_FIELD = "null_value";
private static final String SECONDS_FIELD = "seconds";
private static final String NANOS_FIELD = "nanos";
private static final long MAX_UINT32 = 0xFFFFFFFFL;
private final Context ctx;
private final CelZ3TypeSystem typeSystem;
Expand Down Expand Up @@ -406,7 +409,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
if (CelTypes.isWrapperType(createStruct.messageName())) {
return translateWrapperWktStruct(celExpr, createStruct, ast);
}
// TODO: Support google.protobuf.Timestamp and google.protobuf.Duration.
if (createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE)) {
return translateTimestampWktStruct(celExpr, createStruct, ast);
}
if (createStruct.messageName().equals(CelTypes.DURATION_MESSAGE)) {
return translateDurationWktStruct(celExpr, createStruct, ast);
}

// Bypass SMT when the struct is empty (return the cached SMT default pointer)
if (createStruct.entries().isEmpty()) {
Expand Down Expand Up @@ -599,6 +607,105 @@ private TranslatedValue translateWrapperWktStruct(
return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
}

@FunctionalInterface
private interface TimeWktValueFactory {
Expr<?> create(IntExpr seconds, IntExpr nanos, IntExpr totalNanos);
}

private TranslatedValue translateTimestampWktStruct(
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
return translateTimeWktStruct(
celExpr,
createStruct,
ast,
/* minNanos= */ 0,
(seconds, nanos, totalNanos) ->
typeSystem.withRuntimeError(
typeSystem.wrapTimestamp(totalNanos),
typeSystem.checkTimestampOverflow(totalNanos)));
}

private TranslatedValue translateDurationWktStruct(
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
return translateTimeWktStruct(
celExpr,
createStruct,
ast,
CelZ3TypeSystem.MIN_DURATION_NANOS,
(seconds, nanos, totalNanos) -> {
BoolExpr signMismatch =
ctx.mkOr(
ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
return typeSystem.withRuntimeError(
typeSystem.wrapDuration(totalNanos),
signMismatch,
typeSystem.checkDurationOverflow(totalNanos));
});
}

private TranslatedValue translateTimeWktStruct(
CelExpr celExpr,
CelExpr.CelStruct createStruct,
CelAbstractSyntaxTree ast,
int minNanos,
TimeWktValueFactory valueFactory) {
List<TranslatedValue> entryTvs = new ArrayList<>();
Expr<?> secondsVal =
resolveStructFieldValue(createStruct, SECONDS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
Expr<?> nanosVal =
resolveStructFieldValue(createStruct, NANOS_FIELD, typeSystem.mkInt(0), ast, entryTvs);

IntExpr seconds = typeSystem.getInt(secondsVal);
IntExpr nanos = typeSystem.getInt(nanosVal);
IntExpr totalNanos =
(IntExpr)
ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos);

BoolExpr typeError =
ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal)));
BoolExpr nanosOutOfRange =
ctx.mkOr(
ctx.mkLt(nanos, ctx.mkInt(minNanos)),
ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));

Expr<?> result =
typeSystem.withRuntimeError(
valueFactory.create(seconds, nanos, totalNanos), typeError, nanosOutOfRange);
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
}

private Expr<?> resolveStructFieldValue(
CelExpr.CelStruct createStruct,
String fieldName,
Expr<?> defaultValue,
CelAbstractSyntaxTree ast,
List<TranslatedValue> entryTvs) {
return Streams.findLast(
createStruct.entries().stream().filter(entry -> entry.fieldKey().equals(fieldName)))
.<Expr<?>>map(
entry -> {
TranslatedValue entryTv = translateExpr(entry.value(), ast);
Expr<?> val = entryTv.z3Expr();
if (entry.optionalEntry()) {
Expr<?> checkedVal =
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
entryTv =
TranslatedValue.create(
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
val =
ctx.mkITE(
typeSystem.optHasValue(optRef),
typeSystem.getOptionalValue(optRef),
defaultValue);
}
entryTvs.add(entryTv);
return val;
})
.orElse(defaultValue);
}

private Expr<?> getDefaultValueForType(CelType type) {
if (type instanceof NullableType) {
return typeSystem.mkNull();
Expand Down Expand Up @@ -1392,14 +1499,14 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
return typeSystem.isBytes(val);
}
if (type.equals(SimpleType.TIMESTAMP)) {
IntExpr seconds = typeSystem.getTimestamp(val);
IntExpr nanos = typeSystem.getTimestamp(val);
return ctx.mkAnd(
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
}
if (type.equals(SimpleType.DURATION)) {
IntExpr seconds = typeSystem.getDuration(val);
IntExpr nanos = typeSystem.getDuration(val);
return ctx.mkAnd(
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
}

if (type instanceof ListType) {
Expand Down
3 changes: 2 additions & 1 deletion verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,10 +70,11 @@ public Optional<CelType> findType(String typeName) {

private static final ImmutableList<Descriptor> WELL_KNOWN_DESCRIPTORS =
ImmutableList.of(
// TODO: Support WellKnownProto.DURATION and WellKnownProto.TIMESTAMP.
WellKnownProto.DURATION,
WellKnownProto.JSON_LIST_VALUE,
WellKnownProto.JSON_STRUCT_VALUE,
WellKnownProto.JSON_VALUE,
WellKnownProto.TIMESTAMP,
WellKnownProto.FLOAT_VALUE,
WellKnownProto.INT32_VALUE,
WellKnownProto.INT64_VALUE,
Expand Down
31 changes: 29 additions & 2 deletions verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
import com.microsoft.z3.IntNum;
import com.microsoft.z3.Model;
import com.microsoft.z3.RatNum;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.LinkedHashSet;
Expand Down Expand Up @@ -86,9 +87,9 @@ private static String formatExpr(
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]) + ")";
return formatTimestamp(expr.getArgs()[0]);
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
return formatDuration(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 Expand Up @@ -154,6 +155,32 @@ private static String formatExpr(
return expr.toString();
}

private static String formatTimestamp(Expr<?> nanosExpr) {
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
BigInteger seconds = divRem[0];
BigInteger nanos = divRem[1];
if (nanos.signum() < 0) {
seconds = seconds.subtract(BigInteger.ONE);
nanos = nanos.add(nanosPerSecond);
}
if (nanos.equals(BigInteger.ZERO)) {
return "timestamp(" + seconds + ")";
}
return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}";
}

private static String formatDuration(Expr<?> nanosExpr) {
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
if (divRem[1].equals(BigInteger.ZERO)) {
return "duration('" + divRem[0] + "s')";
}
return "duration('" + totalNanos + "ns')";
}

private static String reconstructList(
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef) {
Expr<?> lenExpr =
Expand Down
38 changes: 31 additions & 7 deletions verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
import com.microsoft.z3.SeqSort;
import com.microsoft.z3.Sort;
import dev.cel.common.internal.ProtoTimeUtils;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
Expand All @@ -56,6 +57,25 @@
@SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types.
public final class CelZ3TypeSystem {

/** Number of nanoseconds per second. */
public static final long NANOS_PER_SECOND = 1_000_000_000L;

/** Minimum valid nanosecond component for a protobuf Duration. */
public static final int MIN_DURATION_NANOS = -999_999_999;

private static final long MAX_TIMESTAMP_NANOS_PART = 999_999_999L;

private static final String MIN_TIMESTAMP_NANOS =
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
.toString();

private static final String MAX_TIMESTAMP_NANOS =
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
.add(BigInteger.valueOf(MAX_TIMESTAMP_NANOS_PART))
.toString();

private static final String TYPE_CEL_VALUE = "CelValue";
private static final String CONS_BOOL = "Bool";
private static final String IS_BOOL = "isBool";
Expand Down Expand Up @@ -777,18 +797,22 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64)));
}

/** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
/**
* Checks if the given nanosecond arithmetic expression overflows CEL Timestamp bounds
* ({@code [0001-01-01T00:00:00Z, 9999-12-31T23:59:59.999999999Z]}).
*/
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)));
ctx.mkGt(result, ctx.mkInt(MAX_TIMESTAMP_NANOS)),
ctx.mkLt(result, ctx.mkInt(MIN_TIMESTAMP_NANOS)));
}

/** Checks if the given arithmetic expression overflows CEL Duration bounds. */
/**
* Checks if the given nanosecond arithmetic expression overflows CEL Duration bounds, which are
* confined to a signed 64-bit integer of nanoseconds (matching Go's {@code time.Duration}).
*/
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)));
return checkIntOverflow(result);
}

/** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */
Expand Down
2 changes: 2 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,8 @@ private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr<?> val
ctx.mkAnd(ts.isInt(val), ctx.mkEq(ts.getInt(val), ctx.mkInt(0))),
ctx.mkAnd(ts.isUint(val), ctx.mkEq(ts.getUint(val), ctx.mkInt(0))),
ctx.mkAnd(ts.isDouble(val), ctx.mkFPIsZero((FPExpr) ts.getDouble(val))),
ctx.mkAnd(ts.isTimestamp(val), ctx.mkEq(ts.getTimestamp(val), ctx.mkInt(0))),
ctx.mkAnd(ts.isDuration(val), ctx.mkEq(ts.getDuration(val), ctx.mkInt(0))),
ctx.mkAnd(ts.isString(val), ctx.mkEq(ts.getString(val), ctx.mkString(""))),
ctx.mkAnd(
ts.isBytes(val), ctx.mkEq(ctx.mkLength((SeqExpr) ts.getBytes(val)), ctx.mkInt(0))),
Expand Down
14 changes: 11 additions & 3 deletions verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions;
import dev.cel.common.types.SimpleType;
import dev.cel.verifier.CelZ3TypeSystem;
import java.util.Optional;

/** Axiomatization for CEL's type conversion functions. */
Expand Down Expand Up @@ -52,7 +53,12 @@ final class TypeConversionAxioms {
.addUnaryOverloadTranslator(
Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(),
(ctx, typeSystem, sink, arg) ->
Optional.of(typeSystem.wrapInt(typeSystem.getTimestamp(arg))))
Optional.of(
typeSystem.wrapInt(
(IntExpr)
ctx.mkDiv(
typeSystem.getTimestamp(arg),
ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)))))
.build();

private static final CelZ3FunctionAxiom UINT_AXIOM =
Expand Down Expand Up @@ -159,9 +165,11 @@ final class TypeConversionAxioms {
Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(),
(ctx, typeSystem, sink, arg) -> {
IntExpr intVal = typeSystem.getInt(arg);
BoolExpr overflow = typeSystem.checkTimestampOverflow(intVal);
IntExpr nanosVal =
(IntExpr) ctx.mkMul(intVal, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND));
BoolExpr overflow = typeSystem.checkTimestampOverflow(nanosVal);
return Optional.of(
typeSystem.withRuntimeError(typeSystem.wrapTimestamp(intVal), overflow));
typeSystem.withRuntimeError(typeSystem.wrapTimestamp(nanosVal), overflow));
})
.build();

Expand Down
Loading
Loading