exprTranslator) {
+ this.context = context;
+ this.ctx = context.ctx();
+ this.typeSystem = context.typeSystem();
+ this.comprehensionUnrollLimit = context.comprehensionUnrollLimit();
+ this.exprTranslator = exprTranslator;
+ }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
new file mode 100644
index 000000000..de0460e3a
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java
@@ -0,0 +1,162 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.common.collect.Lists;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+
+/** Helpers for building Z3 expressions that are independent of the CEL encoding. */
+public final class CelZ3Exprs {
+
+ /**
+ * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
+ *
+ * Returns {@code false} if the list is empty.
+ */
+ public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) {
+ return mkOrFlattened(ctx, Arrays.asList(args));
+ }
+
+ /**
+ * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
+ *
+ *
Returns {@code false} if the list is empty.
+ */
+ public static BoolExpr mkOrFlattened(Context ctx, List args) {
+ // Pruning true/false constants in Java is significantly faster than building
+ // larger ASTs and letting Z3 process them natively.
+ List filteredArgs = new ArrayList<>();
+ for (BoolExpr arg : args) {
+ if (arg.isTrue()) {
+ return ctx.mkTrue();
+ }
+ if (!arg.isFalse()) {
+ filteredArgs.add(arg);
+ }
+ }
+ // Performance only: both shortcuts are equivalent to the mkOr below.
+ if (filteredArgs.isEmpty()) {
+ return ctx.mkFalse();
+ }
+ if (filteredArgs.size() == 1) {
+ return filteredArgs.get(0);
+ }
+ return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0]));
+ }
+
+ /**
+ * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs.
+ *
+ * Returns {@code true} if the list is empty.
+ */
+ public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) {
+ return mkAndFlattened(ctx, Arrays.asList(args));
+ }
+
+ public static BoolExpr mkAndFlattened(Context ctx, List args) {
+ // Pruning true/false constants in Java is significantly faster than building
+ // larger ASTs and letting Z3 process them natively.
+ List filteredArgs = new ArrayList<>();
+ for (BoolExpr arg : args) {
+ if (arg.isFalse()) {
+ return ctx.mkFalse();
+ }
+ if (!arg.isTrue()) {
+ filteredArgs.add(arg);
+ }
+ }
+ // Performance only: both shortcuts are equivalent to the mkAnd below.
+ if (filteredArgs.isEmpty()) {
+ return ctx.mkTrue();
+ }
+ if (filteredArgs.size() == 1) {
+ return filteredArgs.get(0);
+ }
+ return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0]));
+ }
+
+ /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */
+ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
+ if (arg.isTrue()) {
+ return ctx.mkFalse();
+ }
+ if (arg.isFalse()) {
+ return ctx.mkTrue();
+ }
+ return ctx.mkNot(arg);
+ }
+
+ /**
+ * Helper to build a chain of nested ITE (If-Then-Else) conditions.
+ *
+ * Conditions are evaluated in the order they are added. Branches with {@code isFalse()}
+ * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to
+ * avoid allocating dead AST paths in Z3.
+ */
+ public static final class SwitchBuilder {
+
+ private static final class SwitchCase {
+ private final BoolExpr condition;
+ private final Expr value;
+
+ private SwitchCase(BoolExpr condition, Expr value) {
+ this.condition = condition;
+ this.value = value;
+ }
+ }
+
+ private final Context ctx;
+ private final List cases;
+
+ public static SwitchBuilder newBuilder(Context ctx) {
+ return new SwitchBuilder(ctx);
+ }
+
+ @CanIgnoreReturnValue
+ public SwitchBuilder addCase(BoolExpr condition, Expr value) {
+ // Skip branches that can never be hit (e.g. `isFalse()` probes).
+ if (condition.isFalse()) {
+ return this;
+ }
+ cases.add(new SwitchCase(condition, value));
+ return this;
+ }
+
+ public Expr build(Expr defaultFallback) {
+ Expr result = defaultFallback;
+ for (SwitchCase c : Lists.reverse(cases)) {
+ // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite.
+ if (c.value.equals(result)) {
+ continue;
+ }
+ result = ctx.mkITE(c.condition, c.value, result);
+ }
+ return result;
+ }
+
+ private SwitchBuilder(Context ctx) {
+ this.ctx = ctx;
+ this.cases = new ArrayList<>();
+ }
+ }
+
+ private CelZ3Exprs() {}
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
index d4fd31962..55aa62882 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
@@ -47,18 +47,14 @@
import java.util.Arrays;
import java.util.List;
import java.util.Optional;
-import java.util.function.BiFunction;
-import java.util.function.Consumer;
-import java.util.function.Function;
/** Handles mapping CEL Operators to Z3 SMT logic. */
@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
final class CelZ3OperatorTranslator {
private final Context ctx;
private final CelZ3TypeSystem typeSystem;
- private final Consumer constraintSink;
- private final BiFunction, CelType, BoolExpr> typeConstraintGenerator;
- private final Function, CelType> guaranteedTypes;
+ private final CelZ3TranslationContext context;
+ private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
private final CelZ3FunctionRegistry functionRegistry;
private final int comprehensionUnrollLimit;
@@ -117,7 +113,7 @@ Optional translateFunctionCall(
}
Optional evaluatedResultOpt =
- translator.translate(ctx, typeSystem, constraintSink, z3Args, argApproximations);
+ translator.translate(ctx, typeSystem, context::addConstraint, z3Args, argApproximations);
if (!evaluatedResultOpt.isPresent()) {
continue;
@@ -131,7 +127,7 @@ Optional translateFunctionCall(
typeGuards.add(mkTypeGuard(z3Args.get(i), overload.parameterTypes().get(i)));
}
- BoolExpr typeGuard = CelZ3TypeSystem.mkAndFlattened(ctx, typeGuards);
+ BoolExpr typeGuard = CelZ3Exprs.mkAndFlattened(ctx, typeGuards);
currentZ3Result = ctx.mkITE(typeGuard, evaluatedResult.z3Expr(), currentZ3Result);
currentApprox =
(BoolExpr) ctx.mkITE(typeGuard, evaluatedResult.isApproximate(), currentApprox);
@@ -144,7 +140,7 @@ Optional translateFunctionCall(
Operator op = opOpt.orElse(null);
if (op == Operator.IN) {
currentApprox =
- CelZ3TypeSystem.mkOrFlattened(
+ CelZ3Exprs.mkOrFlattened(
ctx, currentApprox, constrainInWitnessTypes(args.get(0), args.get(1), ast));
} else if (op == Operator.OPTIONAL_SELECT) {
// A chained optional select (e.g. `a.?b.?c`) selects from the value of an optional operand.
@@ -154,7 +150,7 @@ Optional translateFunctionCall(
typeSystem.isOptional(operand),
typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)),
operand);
- currentApprox = CelZ3TypeSystem.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target));
+ currentApprox = CelZ3Exprs.mkOrFlattened(ctx, currentApprox, context.isTruncatedMap(target));
}
return Optional.of(
@@ -197,10 +193,10 @@ private BoolExpr constrainInWitnessTypes(
SeqExpr seq = typeSystem.getSeq(typeSystem.getListRef(rhs));
for (Expr cand : candidates) {
BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(cand));
- constraintSink.accept(
+ context.addConstraint(
ctx.mkImplies(
ctx.mkAnd(typeSystem.isList(rhs), structContains),
- typeConstraintGenerator.apply(cand, elemType)));
+ typeConstraintGenerator.createTypeConstraintForType(cand, elemType)));
}
// With a concrete element type, the constraints above cover any match in rhs.
return isConcrete(elemType)
@@ -210,14 +206,16 @@ private BoolExpr constrainInWitnessTypes(
// IN_MAP only probes the presence of lhs itself.
ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs));
BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, lhs);
- constraintSink.accept(
+ context.addConstraint(
ctx.mkImplies(
ctx.mkAnd(typeSystem.isMap(rhs), inMap),
- typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType())));
- return isTruncatedMap(rhs);
+ context
+ .typeConstraintGenerator()
+ .createTypeConstraintForType(lhs, ((MapType) rhsType).keyType())));
+ return context.isTruncatedMap(rhs);
}
- return CelZ3TypeSystem.mkOrFlattened(
- ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
+ return CelZ3Exprs.mkOrFlattened(
+ ctx, context.isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
}
private BoolExpr mkTypeGuard(Expr arg, CelType expectedType) {
@@ -385,7 +383,7 @@ private TranslatedValue translateBinaryLogicalAndOr(
: ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr());
Expr resultZ3 =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(hasMatch, typeSystem.mkBool(!isAnd))
.addCase(hasUnknown, unknownResult)
.addCase(hasError, typeSystem.mkError())
@@ -394,10 +392,10 @@ private TranslatedValue translateBinaryLogicalAndOr(
// An exact short-circuiting operand alone decides the result. Otherwise, an approximate operand
// may really be the absorbing value (e.g. `unknown && false` is false).
BoolExpr resultTaint =
- CelZ3TypeSystem.mkAndFlattened(
+ CelZ3Exprs.mkAndFlattened(
ctx,
- CelZ3TypeSystem.mkNotFlattened(ctx, hasSafeMatch),
- CelZ3TypeSystem.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate()));
+ CelZ3Exprs.mkNotFlattened(ctx, hasSafeMatch),
+ CelZ3Exprs.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate()));
return TranslatedValue.create(resultZ3, typeSystem, resultTaint);
}
@@ -435,7 +433,7 @@ private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTr
typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg));
Expr doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr)));
result =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(typeSystem.isInt(z3Expr), intResult)
.addCase(typeSystem.isDouble(z3Expr), doubleResult)
.build(typeSystem.mkError());
@@ -498,7 +496,7 @@ private BoolExpr getNumericEqualityWithConstant(
BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
return (BoolExpr)
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(typeSystem.isInt(symVal), intEq)
.addCase(typeSystem.isUint(symVal), uintEq)
.addCase(typeSystem.isDouble(symVal), doubleEq)
@@ -610,7 +608,7 @@ private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) {
ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1));
return (BoolExpr)
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(bothIntOrUint, ctx.mkEq(val0, val1))
.addCase(
bothDouble,
@@ -672,15 +670,17 @@ private BoolExpr unrollListEquality(
taints.add(elemEquality.isApproximate());
}
- return CelZ3TypeSystem.mkAndFlattened(ctx, equalities);
+ return CelZ3Exprs.mkAndFlattened(ctx, equalities);
}
private void constrainListElement(SeqExpr seq, IntExpr idx, Expr elem, CelType listType) {
if (listType instanceof ListType) {
- constraintSink.accept(
+ context.addConstraint(
ctx.mkImplies(
ctx.mkLt(idx, ctx.mkLength(seq)),
- typeConstraintGenerator.apply(elem, ((ListType) listType).elemType())));
+ context
+ .typeConstraintGenerator()
+ .createTypeConstraintForType(elem, ((ListType) listType).elemType())));
}
}
@@ -740,7 +740,7 @@ private TranslatedValue translateEquality(
String opName = isEquals ? Operator.EQUALS.getFunction() : Operator.NOT_EQUALS.getFunction();
return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1)
- .withApproximation(CelZ3TypeSystem.mkOrFlattened(ctx, taints));
+ .withApproximation(CelZ3Exprs.mkOrFlattened(ctx, taints));
}
private Expr buildListIndex(
@@ -754,12 +754,12 @@ private Expr buildListIndex(
ctx.mkLt((ArithExpr) index, ctx.mkLength(seq)));
Expr val = ctx.mkNth(seq, (ArithExpr) index);
- constrainValidElement(ctx.mkAnd(typeGuard, inBounds), val);
+ context.constrainValidValue(ctx.mkAnd(typeGuard, inBounds), val);
if (isOptional) {
Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val);
- constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
- constraintSink.accept(typeSystem.optHasValue(resultOptRef));
+ context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
+ context.addConstraint(typeSystem.optHasValue(resultOptRef));
return ctx.mkITE(
inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
}
@@ -767,10 +767,6 @@ private Expr buildListIndex(
return ctx.mkITE(inBounds, val, typeSystem.mkError());
}
- private void constrainValidElement(BoolExpr guard, Expr val) {
- constraintSink.accept(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(val))));
- }
-
private Optional extractIntNumSafe(Expr expr) {
Expr simplified = expr.simplify();
@@ -814,12 +810,12 @@ private ProbeResult createProbeResult(
BoolExpr inMap2 = (BoolExpr) ctx.mkSelect(mapPresence, key2);
Expr val2 = ctx.mkSelect(mapValues, key2);
- BoolExpr condMap1 = CelZ3TypeSystem.mkAndFlattened(ctx, cond1, inMap1);
- BoolExpr condMap2 = CelZ3TypeSystem.mkAndFlattened(ctx, cond2, inMap2);
+ BoolExpr condMap1 = CelZ3Exprs.mkAndFlattened(ctx, cond1, inMap1);
+ BoolExpr condMap2 = CelZ3Exprs.mkAndFlattened(ctx, cond2, inMap2);
- BoolExpr altInMap = CelZ3TypeSystem.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2);
+ BoolExpr altInMap = CelZ3Exprs.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2);
Expr altVal =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(inMapOrig, valOrig)
.addCase(condMap1, val1)
.addCase(condMap2, val2)
@@ -912,25 +908,25 @@ private Expr buildMapIndex(
BoolExpr finalInMap =
(BoolExpr)
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(isInt, intProbe.altInMap)
.addCase(isUint, uintProbe.altInMap)
.addCase(isDouble, doubleProbe.altInMap)
.build(inMapOrig);
Expr finalVal =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(isInt, intProbe.altVal)
.addCase(isUint, uintProbe.altVal)
.addCase(isDouble, doubleProbe.altVal)
.build(valOrig);
- constrainValidElement(ctx.mkAnd(typeGuard, finalInMap), finalVal);
+ context.constrainValidValue(ctx.mkAnd(typeGuard, finalInMap), finalVal);
if (isOptional) {
Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal);
- constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
- constraintSink.accept(typeSystem.optHasValue(resultOptRef));
+ context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
+ context.addConstraint(typeSystem.optHasValue(resultOptRef));
return ctx.mkITE(
finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
}
@@ -989,10 +985,10 @@ private TranslatedValue translateIndex(
ctx.mkLt(
typeSystem.getInt(rhsTrans),
ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(lhsTrans)))));
- BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, isTruncatedMap(lhsTrans));
+ BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, context.isTruncatedMap(lhsTrans));
return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args)
.withApproximation(
- CelZ3TypeSystem.mkOrFlattened(
+ CelZ3Exprs.mkOrFlattened(
ctx, isListIndexTruncated, isMapIndexTruncated, element.isApproximate()));
}
@@ -1030,9 +1026,10 @@ private TranslatedValue buildAndConstrainIndex(
CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType;
BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue)));
- BoolExpr typeConstraint = typeConstraintGenerator.apply(actualValue, finalType);
+ BoolExpr typeConstraint =
+ typeConstraintGenerator.createTypeConstraintForType(actualValue, finalType);
if (isLhsTypeGuaranteed) {
- constraintSink.accept(ctx.mkImplies(isDefined, typeConstraint));
+ context.addConstraint(ctx.mkImplies(isDefined, typeConstraint));
return TranslatedValue.create(actualValue, typeSystem, ctx.mkFalse());
}
// The type checker may narrow other static types (e.g. `(['a'] + dyn_var)[1]` is typed
@@ -1040,8 +1037,8 @@ private TranslatedValue buildAndConstrainIndex(
return TranslatedValue.create(
actualValue,
typeSystem,
- CelZ3TypeSystem.mkAndFlattened(
- ctx, isDefined, CelZ3TypeSystem.mkNotFlattened(ctx, typeConstraint)));
+ CelZ3Exprs.mkAndFlattened(
+ ctx, isDefined, CelZ3Exprs.mkNotFlattened(ctx, typeConstraint)));
}
BoolExpr isListGuard =
@@ -1049,7 +1046,7 @@ private TranslatedValue buildAndConstrainIndex(
BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans));
return TranslatedValue.create(
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
.build(typeSystem.mkError()),
@@ -1080,7 +1077,7 @@ private TranslatedValue translateConditional(
: cond.z3Expr();
Expr resultZ3 =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(hasUnknown, unknownResult)
.addCase(hasError, typeSystem.mkError())
.addCase(condTrue, trueBranch.z3Expr())
@@ -1091,7 +1088,7 @@ private TranslatedValue translateConditional(
BoolExpr resultTaint =
(BoolExpr)
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(hasUnknown, ctx.mkNot(hasSafeUnknown))
.addCase(hasError, ctx.mkNot(hasSafeError))
.addCase(condTrue, ctx.mkOr(cond.isApproximate(), trueBranch.isApproximate()))
@@ -1118,7 +1115,7 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS
* so constraints derived from those could exclude valid inputs.
*/
private CelType guaranteedType(TranslatedValue val) {
- return guaranteedTypes.apply(val.z3Expr());
+ return context.guaranteedType(val.z3Expr());
}
/**
@@ -1141,18 +1138,6 @@ private static boolean isNumericType(CelType type) {
return kind == CelKind.INT || kind == CelKind.UINT || kind == CelKind.DOUBLE;
}
- /**
- * Whether {@code val} is a map with more keys than the unroll limit, beyond which its presence is
- * not linked to its keys.
- */
- BoolExpr isTruncatedMap(Expr val) {
- return ctx.mkAnd(
- typeSystem.isMap(val),
- ctx.mkGt(
- ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))),
- ctx.mkInt(comprehensionUnrollLimit)));
- }
-
/**
* Whether observing {@code args} together may expose a value beyond a truncated type constraint
* in any of them. Type constraints at the point of observation rule this out only if every arg
@@ -1163,27 +1148,19 @@ private BoolExpr mayObserveTruncatedTypeConstraint(
if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) {
return ctx.mkFalse();
}
- return CelZ3TypeSystem.mkOrFlattened(
+ return CelZ3Exprs.mkOrFlattened(
ctx,
Arrays.stream(args)
.map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr()))
.collect(toImmutableList()));
}
- CelZ3OperatorTranslator(
- Context ctx,
- CelZ3TypeSystem typeSystem,
- Consumer constraintSink,
- BiFunction, CelType, BoolExpr> typeConstraintGenerator,
- Function, CelType> guaranteedTypes,
- CelZ3FunctionRegistry functionRegistry,
- int comprehensionUnrollLimit) {
- this.ctx = ctx;
- this.typeSystem = typeSystem;
- this.constraintSink = constraintSink;
- this.typeConstraintGenerator = typeConstraintGenerator;
- this.guaranteedTypes = guaranteedTypes;
+ CelZ3OperatorTranslator(CelZ3TranslationContext context, CelZ3FunctionRegistry functionRegistry) {
+ this.ctx = context.ctx();
+ this.typeSystem = context.typeSystem();
+ this.context = context;
+ this.typeConstraintGenerator = context.typeConstraintGenerator();
this.functionRegistry = functionRegistry;
- this.comprehensionUnrollLimit = comprehensionUnrollLimit;
+ this.comprehensionUnrollLimit = context.comprehensionUnrollLimit();
}
}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
new file mode 100644
index 000000000..c98877185
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
@@ -0,0 +1,560 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.Iterables;
+import com.google.common.collect.Streams;
+import com.microsoft.z3.ArrayExpr;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.FPExpr;
+import com.microsoft.z3.IntExpr;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.ast.CelExpr;
+import dev.cel.common.types.CelKind;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.CelTypeProvider;
+import dev.cel.common.types.CelTypes;
+import dev.cel.common.types.ListType;
+import dev.cel.common.types.MapType;
+import dev.cel.common.types.NullableType;
+import dev.cel.common.types.OptionalType;
+import dev.cel.common.types.SimpleType;
+import dev.cel.common.types.StructType;
+import dev.cel.common.types.StructTypeReference;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.function.BiFunction;
+
+/** Translates CEL message construction and field selection to Z3. */
+@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
+final class CelZ3StructTranslator {
+ private static final String MSG_REF_PREFIX = "!msg_ref";
+ private static final String EMPTY_MSG_REF_PREFIX = "!empty_msg_ref_";
+ 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 CelZ3TranslationContext context;
+ private final Context ctx;
+ private final CelZ3TypeSystem typeSystem;
+ private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
+ private final CelTypeProvider typeProvider;
+ private final BiFunction exprTranslator;
+ private final Map> emptyMessageCache;
+ private Expr emptyListCache;
+ private Expr emptyMapCache;
+
+ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
+ CelExpr.CelStruct createStruct = celExpr.struct();
+ if (isJsonWkt(createStruct.messageName())) {
+ return translateJsonWktStruct(celExpr, createStruct, ast);
+ }
+ if (CelTypes.isWrapperType(createStruct.messageName())) {
+ return translateWrapperWktStruct(celExpr, createStruct, ast);
+ }
+ 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()) {
+ return TranslatedValue.create(
+ getDefaultValueForType(StructTypeReference.create(createStruct.messageName())),
+ celExpr,
+ typeSystem,
+ ctx.mkFalse());
+ }
+
+ Expr msgRef = typeSystem.mkMessageRefConst(MSG_REF_PREFIX);
+
+ // Initialize the values array with Unknown. Missing fields and explicit primitive defaults
+ // will both bypass the store and fall back to this Unknown base. However, their msgPresence
+ // will evaluate to false, allowing translateSelect to properly return the default value.
+ ArrayExpr msgValues = ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown());
+ ArrayExpr msgPresence = ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse());
+
+ List elementsTv = new ArrayList<>();
+
+ for (CelExpr.CelStruct.Entry entryAst : createStruct.entries()) {
+ Expr key = ctx.mkString(entryAst.fieldKey());
+ TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
+ Expr value = valueTv.z3Expr();
+
+ CelType fieldType =
+ typeProvider
+ .findType(createStruct.messageName())
+ .filter(t -> t instanceof StructType)
+ .map(t -> (StructType) t)
+ .flatMap(t -> t.findField(entryAst.fieldKey()))
+ .map(StructType.Field::type)
+ .orElseGet(() -> extractAstTypeOrDefault(ast, entryAst.value().id()));
+ Expr defaultVal = getDefaultValueForType(fieldType);
+
+ Expr finalValue = value;
+ BoolExpr optionalHasValue = ctx.mkTrue();
+ if (entryAst.optionalEntry()) {
+ Expr checkedValue =
+ typeSystem.withRuntimeError(value, ctx.mkNot(typeSystem.isOptional(value)));
+ valueTv =
+ TranslatedValue.create(
+ checkedValue, entryAst.value(), typeSystem, valueTv.isApproximate());
+ Expr optRef = typeSystem.getOptionalRef(checkedValue);
+ optionalHasValue = typeSystem.optHasValue(optRef);
+ finalValue = typeSystem.getOptionalValue(optRef);
+ }
+ elementsTv.add(valueTv);
+
+ // Canonicalization Trick:
+ //
+ // We avoid storing explicit default values (e.g. `single_int32: 0`)
+ // in `msgValues`, leaving them as `Unknown` (identical to missing fields).
+ // This structurally aligns defaults with missing fields, allowing Z3's native array equality
+ // (`msg1 == msg2`) to work without using quantifiers (which avoids MBQI loops).
+ // Because proto3 singular primitives do not have field presence, we also skip setting
+ // `msgPresence`.
+ BoolExpr isDefaultPrimitive =
+ fieldType.kind().isPrimitive() ? ctx.mkEq(finalValue, defaultVal) : ctx.mkFalse();
+
+ BoolExpr shouldBypass = ctx.mkOr(ctx.mkNot(optionalHasValue), isDefaultPrimitive);
+
+ msgValues =
+ (ArrayExpr) ctx.mkITE(shouldBypass, msgValues, ctx.mkStore(msgValues, key, finalValue));
+
+ msgPresence =
+ (ArrayExpr)
+ ctx.mkITE(shouldBypass, msgPresence, ctx.mkStore(msgPresence, key, ctx.mkTrue()));
+ }
+
+ context.addConstraint(
+ ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString(createStruct.messageName())));
+ context.addConstraint(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues));
+ context.addConstraint(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence));
+
+ Expr result = typeSystem.wrapMessage(msgRef);
+ return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
+ }
+
+ private static boolean isJsonWkt(String messageName) {
+ return messageName.equals(CelTypes.VALUE_MESSAGE)
+ || messageName.equals(CelTypes.LIST_VALUE_MESSAGE)
+ || messageName.equals(CelTypes.STRUCT_MESSAGE);
+ }
+
+ // Concretize JSON WKT unwrapping directly into native Z3 primitives to avoid
+ // sort incompatibilities (Message == String) and solver performance penalties (quantifiers).
+ private TranslatedValue translateJsonWktStruct(
+ CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+ Expr fallback;
+ if (createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)) {
+ fallback = typeSystem.mkNull();
+ } else if (createStruct.messageName().equals(CelTypes.LIST_VALUE_MESSAGE)) {
+ fallback = getDefaultValueForType(ListType.create(SimpleType.DYN));
+ } else {
+ fallback = getDefaultValueForType(MapType.create(SimpleType.STRING, SimpleType.DYN));
+ }
+
+ if (createStruct.entries().isEmpty()) {
+ return TranslatedValue.create(fallback, celExpr, typeSystem, ctx.mkFalse());
+ }
+
+ // JSON WKT messages (gp.Struct, gp.Value, gp.ListValue) can only have a single top-level
+ // field entry in non-empty creation literals (e.g., 'fields' for Struct, 'values' for
+ // ListValue, or a single 'oneof' field for Value).
+ CelExpr.CelStruct.Entry entry = Iterables.getOnlyElement(createStruct.entries());
+
+ // Translate the value to properly capture approximations and Optionals
+ TranslatedValue entryTv = translateExpr(entry.value(), ast);
+ Expr finalVal = entryTv.z3Expr();
+
+ boolean isNullValueField =
+ createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)
+ && entry.fieldKey().equals(NULL_VALUE_FIELD);
+
+ if (entry.optionalEntry()) {
+ Expr checkedVal =
+ typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal)));
+ entryTv =
+ TranslatedValue.create(checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
+ Expr optRef = typeSystem.getOptionalRef(checkedVal);
+ BoolExpr hasValue = typeSystem.optHasValue(optRef);
+
+ Expr unpackedVal = typeSystem.getOptionalValue(optRef);
+ if (isNullValueField) {
+ unpackedVal = typeSystem.mkNull();
+ }
+ finalVal = ctx.mkITE(hasValue, unpackedVal, fallback);
+ } else if (isNullValueField) {
+ finalVal = typeSystem.mkNull();
+ }
+
+ return TranslatedValue.propagateStrict(
+ ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
+ }
+
+ private TranslatedValue translateWrapperWktStruct(
+ CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+ String typeName = createStruct.messageName();
+ CelType wrapperType =
+ CelTypes.getWellKnownCelType(typeName)
+ .orElseThrow(
+ () -> new IllegalArgumentException("Unexpected wrapper type: " + typeName));
+ CelType targetType = ((NullableType) wrapperType).targetType();
+ Expr currentVal = getDefaultValueForType(targetType);
+
+ List entryTvs = new ArrayList<>();
+ for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
+ 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);
+ BoolExpr hasValue = typeSystem.optHasValue(optRef);
+ currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal);
+ } else {
+ currentVal = val;
+ }
+ entryTvs.add(entryTv);
+ }
+ BoolExpr validValue =
+ typeConstraintGenerator.createTypeConstraintForType(currentVal, targetType);
+ if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) {
+ IntExpr intVal = typeSystem.getInt(currentVal);
+ validValue =
+ ctx.mkAnd(
+ validValue,
+ ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)),
+ ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE)));
+ } else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) {
+ IntExpr uintVal = typeSystem.getUint(currentVal);
+ validValue =
+ ctx.mkAnd(
+ validValue,
+ ctx.mkGe(uintVal, ctx.mkInt(0)),
+ ctx.mkLe(uintVal, ctx.mkInt(MAX_UINT32)));
+ } else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) {
+ FPExpr doubleVal = typeSystem.getDouble(currentVal);
+ FPExpr narrowedFloat =
+ ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), doubleVal, ctx.mkFPSortSingle());
+ FPExpr widenedDouble =
+ ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), narrowedFloat, ctx.mkFPSortDouble());
+ currentVal = typeSystem.wrapDouble(widenedDouble);
+ }
+ currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue));
+ 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 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 entryTvs) {
+ return Streams.findLast(
+ createStruct.entries().stream().filter(entry -> entry.fieldKey().equals(fieldName)))
+ .>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();
+ }
+ if (type instanceof OptionalType) {
+ return typeSystem.mkOptionalNone();
+ }
+ if (type.equals(SimpleType.INT)) {
+ return typeSystem.mkInt(0);
+ }
+ if (type.equals(SimpleType.BOOL)) {
+ return typeSystem.wrapBool(ctx.mkFalse());
+ }
+ if (type.equals(SimpleType.STRING)) {
+ return typeSystem.mkString("");
+ }
+ if (type.equals(SimpleType.BYTES)) {
+ return typeSystem.mkBytes("");
+ }
+ if (type.equals(SimpleType.DOUBLE)) {
+ return typeSystem.mkDouble(0.0);
+ }
+ 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);
+ context.addConstraint(
+ ctx.mkEq(
+ typeSystem.getSeq(emptyListCache),
+ ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()))));
+ }
+ return typeSystem.wrapList(emptyListCache);
+ }
+ if (type instanceof MapType) {
+ if (emptyMapCache == null) {
+ emptyMapCache = typeSystem.mkMapRefConst(EMPTY_MAP_PREFIX);
+ context.addConstraint(
+ ctx.mkEq(
+ typeSystem.getMapPresence(emptyMapCache),
+ ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse())));
+ context.addConstraint(
+ ctx.mkEq(
+ typeSystem.getMapValues(emptyMapCache),
+ ctx.mkConstArray(typeSystem.celValueSort(), typeSystem.mkUnknown())));
+ context.addConstraint(
+ ctx.mkEq(
+ typeSystem.getMapKeys(emptyMapCache),
+ ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()))));
+ }
+ return typeSystem.wrapMap(emptyMapCache);
+ }
+ if (type.kind() == CelKind.STRUCT) {
+ String messageName = type.name();
+ Expr msgRef =
+ emptyMessageCache.computeIfAbsent(
+ messageName,
+ name -> {
+ Expr ref = typeSystem.mkMessageRefConst(EMPTY_MSG_REF_PREFIX + name);
+ context.addConstraint(
+ ctx.mkEq(
+ typeSystem.getMsgPresence(ref),
+ ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse())));
+ context.addConstraint(
+ ctx.mkEq(
+ typeSystem.getMsgValues(ref),
+ ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown())));
+ context.addConstraint(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name)));
+ return ref;
+ });
+ return typeSystem.wrapMessage(msgRef);
+ }
+ return typeSystem.mkUnknown();
+ }
+
+ private static final class FieldAccess {
+ private final BoolExpr presence;
+ private final Expr value;
+
+ private FieldAccess(BoolExpr presence, Expr value) {
+ this.presence = presence;
+ this.value = value;
+ }
+ }
+
+ private FieldAccess getMapAccess(Expr operand, String field, BoolExpr typeGuard) {
+ Expr mapRef = typeSystem.getMapRef(operand);
+ Expr mapFieldZ3Str = typeSystem.mkString(field);
+ BoolExpr presence =
+ (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str);
+ Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str);
+ context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
+ return new FieldAccess(presence, value);
+ }
+
+ private FieldAccess getMsgAccess(Expr operand, String field, BoolExpr typeGuard) {
+ Expr msgRef = typeSystem.getMessageRef(operand);
+ Expr msgFieldZ3Str = ctx.mkString(field);
+ BoolExpr presence =
+ (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str);
+ Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str);
+ context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
+ return new FieldAccess(presence, value);
+ }
+
+ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
+ CelExpr.CelSelect select = celExpr.select();
+ long exprId = celExpr.id();
+ TranslatedValue operandTv = translateExpr(select.operand(), ast);
+ Expr operand = operandTv.z3Expr();
+ String field = select.field();
+ CelType operandType = extractAstTypeOrDefault(ast, select.operand().id());
+
+ Expr presenceResult;
+ Expr valueResult;
+
+ if (operandType instanceof MapType) {
+ FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue());
+ presenceResult = mapAcc.presence;
+ valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
+ } else if (operandType.kind() == CelKind.STRUCT) {
+ FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue());
+ presenceResult = msgAcc.presence;
+ Expr defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
+ valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
+ } else {
+ // Dynamic type: generate the full SMT decision tree
+ BoolExpr isMap = typeSystem.isMap(operand);
+ BoolExpr isMessage = typeSystem.isMessage(operand);
+
+ FieldAccess mapAcc = getMapAccess(operand, field, isMap);
+ FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
+
+ presenceResult =
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+ .addCase(isMessage, msgAcc.presence)
+ .addCase(isMap, mapAcc.presence)
+ .build(ctx.mkFalse());
+
+ Expr defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
+ Expr msgRead = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
+ Expr mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
+
+ valueResult =
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+ .addCase(isMessage, msgRead)
+ .addCase(isMap, mapRead)
+ .build(typeSystem.mkError());
+ }
+
+ Expr fieldAccess = select.testOnly() ? typeSystem.wrapBool(presenceResult) : valueResult;
+
+ context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast));
+
+ TranslatedValue result =
+ TranslatedValue.propagateStrict(
+ ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv));
+ // Map presence is only linked to the keys up to the unroll limit.
+ return operandType.kind() == CelKind.STRUCT
+ ? result
+ : result.withApproximation(context.isTruncatedMap(operand));
+ }
+
+ private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) {
+ return ast.getType(id).orElse(SimpleType.DYN);
+ }
+
+ private TranslatedValue translateExpr(CelExpr expr, CelAbstractSyntaxTree ast) {
+ return exprTranslator.apply(expr, ast);
+ }
+
+ CelZ3StructTranslator(
+ CelZ3TranslationContext context,
+ CelTypeProvider typeProvider,
+ BiFunction exprTranslator) {
+ this.context = context;
+ this.ctx = context.ctx();
+ this.typeSystem = context.typeSystem();
+ this.typeConstraintGenerator = context.typeConstraintGenerator();
+ this.typeProvider = typeProvider;
+ this.exprTranslator = exprTranslator;
+ this.emptyMessageCache = new HashMap<>();
+ }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
new file mode 100644
index 000000000..4024e1ff5
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
@@ -0,0 +1,142 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.SimpleType;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Optional;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.function.Supplier;
+
+/** State shared by the translators of a single verification query. */
+final class CelZ3TranslationContext {
+
+ private final Context ctx;
+ private final CelZ3TypeSystem typeSystem;
+ private final CelZ3TypeConstraintGenerator typeConstraintGenerator;
+ private final int comprehensionUnrollLimit;
+ private final Set constraints;
+ private final Map, CelType> inputVariableTypes;
+ private final List truncationConditions;
+ private final Map symbolTable;
+
+ Context ctx() {
+ return ctx;
+ }
+
+ CelZ3TypeSystem typeSystem() {
+ return typeSystem;
+ }
+
+ CelZ3TypeConstraintGenerator typeConstraintGenerator() {
+ return typeConstraintGenerator;
+ }
+
+ int comprehensionUnrollLimit() {
+ return comprehensionUnrollLimit;
+ }
+
+ /** Returns the constraints asserted so far, in insertion order. */
+ Set constraints() {
+ return Collections.unmodifiableSet(constraints);
+ }
+
+ void addConstraint(BoolExpr constraint) {
+ constraints.add(constraint);
+ }
+
+ /** Constrains {@code value} to be neither an error nor unknown whenever {@code guard} holds. */
+ void constrainValidValue(BoolExpr guard, Expr value) {
+ addConstraint(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value))));
+ }
+
+ void addInputVariable(Expr variable, CelType declaredType) {
+ inputVariableTypes.put(variable, declaredType);
+ }
+
+ /** Returns the declared type of an input variable, or dyn for any other value. */
+ CelType guaranteedType(Expr value) {
+ return inputVariableTypes.getOrDefault(value, SimpleType.DYN);
+ }
+
+ /**
+ * Whether {@code val} is a map with more keys than the unroll limit, beyond which its presence is
+ * not linked to its keys.
+ */
+ BoolExpr isTruncatedMap(Expr val) {
+ return ctx.mkAnd(
+ typeSystem.isMap(val),
+ ctx.mkGt(
+ ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))),
+ ctx.mkInt(comprehensionUnrollLimit)));
+ }
+
+ void addTruncationCondition(BoolExpr condition) {
+ truncationConditions.add(condition);
+ }
+
+ BoolExpr hasTruncation() {
+ return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions);
+ }
+
+ void bindSymbol(String name, TranslatedValue value) {
+ symbolTable.put(name, value);
+ }
+
+ Optional lookupSymbol(String name) {
+ return Optional.ofNullable(symbolTable.get(name));
+ }
+
+ TranslatedValue computeSymbolIfAbsent(
+ String name, Function mappingFunction) {
+ return symbolTable.computeIfAbsent(name, mappingFunction);
+ }
+
+ /** Binds {@code varName} to {@code value} while running {@code action}, then restores it. */
+ T withScope(String varName, TranslatedValue value, Supplier action) {
+ TranslatedValue prev = symbolTable.put(varName, value);
+ try {
+ return action.get();
+ } finally {
+ if (prev != null) {
+ symbolTable.put(varName, prev);
+ } else {
+ symbolTable.remove(varName);
+ }
+ }
+ }
+
+ CelZ3TranslationContext(Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) {
+ this.ctx = ctx;
+ this.typeSystem = typeSystem;
+ this.typeConstraintGenerator =
+ new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit);
+ this.comprehensionUnrollLimit = comprehensionUnrollLimit;
+ this.constraints = new LinkedHashSet<>();
+ this.inputVariableTypes = new HashMap<>();
+ this.truncationConditions = new ArrayList<>();
+ this.symbolTable = new HashMap<>();
+ }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java
new file mode 100644
index 000000000..1f6e86475
--- /dev/null
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java
@@ -0,0 +1,231 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.microsoft.z3.ArithExpr;
+import com.microsoft.z3.ArrayExpr;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.IntExpr;
+import com.microsoft.z3.SeqExpr;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.types.CelKind;
+import dev.cel.common.types.CelType;
+import dev.cel.common.types.ListType;
+import dev.cel.common.types.MapType;
+import dev.cel.common.types.NullableType;
+import dev.cel.common.types.OptionalType;
+import dev.cel.common.types.SimpleType;
+import java.util.ArrayList;
+import java.util.List;
+
+/** Generates Z3 constraints restricting a value to the values of a CEL type. */
+@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
+final class CelZ3TypeConstraintGenerator {
+
+ private final Context ctx;
+ private final CelZ3TypeSystem typeSystem;
+ private final int comprehensionUnrollLimit;
+
+ BoolExpr createTypeConstraint(Expr val, long exprId, CelAbstractSyntaxTree ast) {
+ CelType type =
+ ast.getType(exprId)
+ .orElseThrow(
+ () -> new IllegalArgumentException("Type not found for expr ID: " + exprId));
+ BoolExpr typeConstraint = createTypeConstraintForType(val, type);
+ return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint);
+ }
+
+ BoolExpr createTypeConstraintForType(Expr val, CelType type) {
+ if (type instanceof NullableType) {
+ NullableType nullableType = (NullableType) type;
+ return ctx.mkOr(
+ typeSystem.isNull(val), createTypeConstraintForType(val, nullableType.targetType()));
+ }
+ if (type instanceof OptionalType) {
+ BoolExpr isOpt = typeSystem.isOptional(val);
+ CelType paramType = type.parameters().get(0);
+ if (!CelZ3OperatorTranslator.isStaticallyKnown(paramType)) {
+ return isOpt;
+ }
+ Expr optRef = typeSystem.getOptionalRef(val);
+ BoolExpr hasValue = typeSystem.optHasValue(optRef);
+ Expr optVal = typeSystem.getOptionalValue(optRef);
+ BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal));
+ BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType);
+ return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint)));
+ }
+ if (type.equals(SimpleType.BOOL)) {
+ return typeSystem.isBool(val);
+ }
+ if (type.equals(SimpleType.INT)) {
+ IntExpr unwrapped = typeSystem.getInt(val);
+ return ctx.mkAnd(typeSystem.isInt(val), ctx.mkNot(typeSystem.checkIntOverflow(unwrapped)));
+ }
+ if (type.equals(SimpleType.UINT)) {
+ IntExpr unwrapped = typeSystem.getUint(val);
+ return ctx.mkAnd(typeSystem.isUint(val), ctx.mkNot(typeSystem.checkUintOverflow(unwrapped)));
+ }
+ if (type.equals(SimpleType.DOUBLE)) {
+ return typeSystem.isDouble(val);
+ }
+ if (type.equals(SimpleType.STRING)) {
+ return typeSystem.isString(val);
+ }
+ if (type.equals(SimpleType.BYTES)) {
+ return typeSystem.isBytes(val);
+ }
+ if (type.equals(SimpleType.TIMESTAMP)) {
+ IntExpr nanos = typeSystem.getTimestamp(val);
+ return ctx.mkAnd(
+ typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
+ }
+ if (type.equals(SimpleType.DURATION)) {
+ IntExpr nanos = typeSystem.getDuration(val);
+ return ctx.mkAnd(
+ typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
+ }
+
+ if (type instanceof ListType) {
+ // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather
+ // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops.
+ // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧
+ // typeConstraint(seq[i]).
+ BoolExpr isList = typeSystem.isList(val);
+ CelType elemType = ((ListType) type).elemType();
+
+ Expr listRef = typeSystem.getListRef(val);
+ SeqExpr seq = typeSystem.getSeq(listRef);
+ Expr length = ctx.mkLength(seq);
+
+ List boundsAndTypes = new ArrayList<>();
+ boundsAndTypes.add(isList);
+ // Elements beyond the limit are unconstrained, which only matters if elemType is known.
+ if (CelZ3OperatorTranslator.isStaticallyKnown(elemType)) {
+ boundsAndTypes.add(
+ ctx.mkImplies(
+ ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
+ typeSystem.hasTruncatedTypeConstraint(val)));
+ }
+ for (int i = 0; i < comprehensionUnrollLimit; i++) {
+ IntExpr idx = ctx.mkInt(i);
+ Expr elem = ctx.mkNth(seq, idx);
+ BoolExpr validIndex = ctx.mkLt(idx, length);
+ // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in
+ // list(dyn). For concrete types, this is already implied by createTypeConstraintForType.
+ boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem))));
+ BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
+ boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
+ }
+
+ return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
+ }
+ if (type instanceof MapType) {
+ // Do NOT emit a for-all quantifier over map keys or values here.
+ // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using
+ // bounded unrolling over the key sequence up to comprehensionUnrollLimit.
+ // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key)
+ // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val))
+ BoolExpr isMap = typeSystem.isMap(val);
+ MapType mapType = (MapType) type;
+ CelType keyType = mapType.keyType();
+ CelType valType = mapType.valueType();
+
+ Expr mapRef = typeSystem.getMapRef(val);
+ SeqExpr seq = typeSystem.getMapKeys(mapRef);
+ Expr length = ctx.mkLength(seq);
+ ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
+ ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
+
+ List boundsAndTypes = new ArrayList<>();
+ boundsAndTypes.add(isMap);
+ boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
+ // Entries beyond the limit are unconstrained, which matters if keyType or valType is known.
+ if (CelZ3OperatorTranslator.isStaticallyKnown(keyType)
+ || CelZ3OperatorTranslator.isStaticallyKnown(valType)) {
+ boundsAndTypes.add(
+ ctx.mkImplies(
+ ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)),
+ typeSystem.hasTruncatedTypeConstraint(val)));
+ }
+
+ for (int i = 0; i < comprehensionUnrollLimit; i++) {
+ IntExpr idx = ctx.mkInt(i);
+ Expr key = ctx.mkNth(seq, idx);
+ BoolExpr validIndex = ctx.mkLt(idx, length);
+
+ BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key);
+ BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key));
+ // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in
+ // map(dyn, ...). For concrete map types, this is already implied by keyType constraints.
+ boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError)));
+ boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType)));
+
+ BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key);
+ BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
+
+ Expr mapVal = ctx.mkSelect(mapValues, key);
+ BoolExpr valNotError = ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal));
+ boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
+ boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
+ }
+
+ return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
+ }
+ if (type.kind() == CelKind.STRUCT) {
+ return ctx.mkAnd(
+ typeSystem.isMessage(val),
+ ctx.mkEq(
+ typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)), ctx.mkString(type.name())));
+ }
+ // Fallback: no type constraint
+ return ctx.mkTrue();
+ }
+
+ private BoolExpr getBoundedMapBijection(
+ ArrayExpr mapPresence, SeqExpr seq, ArithExpr lengthExpr) {
+ List constraints = new ArrayList<>();
+ for (int i = 0; i < comprehensionUnrollLimit; i++) {
+ for (int j = i + 1; j < comprehensionUnrollLimit; j++) {
+ BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr);
+ BoolExpr notEqual =
+ ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j))));
+ constraints.add(ctx.mkImplies(validPair, notEqual));
+ }
+ }
+
+ BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
+
+ ArrayExpr seqMap = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse());
+ for (int i = 0; i < comprehensionUnrollLimit; i++) {
+ seqMap =
+ (ArrayExpr)
+ ctx.mkITE(
+ ctx.mkLt(ctx.mkInt(i), lengthExpr),
+ ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
+ seqMap);
+ }
+ constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
+ return CelZ3Exprs.mkAndFlattened(ctx, constraints);
+ }
+
+ CelZ3TypeConstraintGenerator(
+ Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) {
+ this.ctx = ctx;
+ this.typeSystem = typeSystem;
+ this.comprehensionUnrollLimit = comprehensionUnrollLimit;
+ }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
index 7defbc706..d164505c4 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
@@ -16,10 +16,8 @@
import com.google.auto.value.AutoValue;
import com.google.common.collect.ImmutableList;
-import com.google.common.collect.Lists;
import com.google.common.collect.ObjectArrays;
import com.google.common.primitives.UnsignedLongs;
-import com.google.errorprone.annotations.CanIgnoreReturnValue;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.ArrayExpr;
import com.microsoft.z3.BoolExpr;
@@ -35,7 +33,6 @@
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;
import java.util.List;
@@ -404,7 +401,7 @@ public BoolExpr getStructuralEquality(Expr arg0, Expr arg1) {
// For primitives, generic equality matches the direct Z3 datatype wrapper.
BoolExpr genericEq = ctx.mkEq(arg0, arg1);
return (BoolExpr)
- SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(isListEq, seqEq)
.addCase(isMapEq, mapEq)
.addCase(isMsgEq, msgEq)
@@ -489,7 +486,7 @@ Expr propagateErrorAndUnknown(
BoolExpr hasError = ctx.mkOr(errors);
BoolExpr hasUnknown = ctx.mkOr(unknowns);
// Unknowns have higher precedence than error
- return SwitchBuilder.newBuilder(ctx)
+ return CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(hasUnknown, unknownResult)
.addCase(hasError, mkError())
.build(result);
@@ -797,60 +794,6 @@ public SeqExpr mkConcatSafe(Expr arg1, Expr arg2) {
return ctx.mkConcat((Expr>) arg1, (Expr>) arg2);
}
- /**
- * Helper to build a chain of nested ITE (If-Then-Else) conditions.
- *
- * Conditions are evaluated in the order they are added. Branches with {@code isFalse()}
- * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to
- * avoid allocating dead AST paths in Z3.
- */
- public static final class SwitchBuilder {
-
- private static final class SwitchCase {
- private final BoolExpr condition;
- private final Expr value;
-
- private SwitchCase(BoolExpr condition, Expr value) {
- this.condition = condition;
- this.value = value;
- }
- }
-
- private final Context ctx;
- private final List cases;
-
- public static SwitchBuilder newBuilder(Context ctx) {
- return new SwitchBuilder(ctx);
- }
-
- @CanIgnoreReturnValue
- public SwitchBuilder addCase(BoolExpr condition, Expr value) {
- // Skip branches that can never be hit (e.g. `isFalse()` probes).
- if (condition.isFalse()) {
- return this;
- }
- cases.add(new SwitchCase(condition, value));
- return this;
- }
-
- public Expr build(Expr defaultFallback) {
- Expr result = defaultFallback;
- for (SwitchCase c : Lists.reverse(cases)) {
- // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite.
- if (c.value.equals(result)) {
- continue;
- }
- result = ctx.mkITE(c.condition, c.value, result);
- }
- return result;
- }
-
- private SwitchBuilder(Context ctx) {
- this.ctx = ctx;
- this.cases = new ArrayList<>();
- }
- }
-
@AutoValue
abstract static class FuncDeclKey {
abstract String name();
@@ -864,82 +807,6 @@ private static FuncDeclKey create(String name, Sort[] domain, Sort range) {
}
}
- /**
- * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
- *
- * Returns {@code false} if the list is empty.
- */
- public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) {
- return mkOrFlattened(ctx, Arrays.asList(args));
- }
-
- /**
- * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
- *
- *
Returns {@code false} if the list is empty.
- */
- public static BoolExpr mkOrFlattened(Context ctx, List args) {
- // Pruning true/false constants in Java is significantly faster than building
- // larger ASTs and letting Z3 process them natively.
- List filteredArgs = new ArrayList<>();
- for (BoolExpr arg : args) {
- if (arg.isTrue()) {
- return ctx.mkTrue();
- }
- if (!arg.isFalse()) {
- filteredArgs.add(arg);
- }
- }
- if (filteredArgs.isEmpty()) {
- return ctx.mkFalse();
- }
- if (filteredArgs.size() == 1) {
- return filteredArgs.get(0);
- }
- return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0]));
- }
-
- /**
- * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs.
- *
- * Returns {@code true} if the list is empty.
- */
- public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) {
- return mkAndFlattened(ctx, Arrays.asList(args));
- }
-
- public static BoolExpr mkAndFlattened(Context ctx, List args) {
- // Pruning true/false constants in Java is significantly faster than building
- // larger ASTs and letting Z3 process them natively.
- List filteredArgs = new ArrayList<>();
- for (BoolExpr arg : args) {
- if (arg.isFalse()) {
- return ctx.mkFalse();
- }
- if (!arg.isTrue()) {
- filteredArgs.add(arg);
- }
- }
- if (filteredArgs.isEmpty()) {
- return ctx.mkTrue();
- }
- if (filteredArgs.size() == 1) {
- return filteredArgs.get(0);
- }
- return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0]));
- }
-
- /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */
- public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
- if (arg.isTrue()) {
- return ctx.mkFalse();
- }
- if (arg.isFalse()) {
- return ctx.mkTrue();
- }
- return ctx.mkNot(arg);
- }
-
CelZ3TypeSystem(Context ctx, boolean parameterizeUnknowns) {
this.ctx = ctx;
this.funcDeclCache = new HashMap<>();
diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
index 7172a6a4f..7ea52abc8 100644
--- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
+++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
@@ -160,14 +160,14 @@ static TranslatedValue propagateStrict(
BoolExpr isError = ts.isError(z3Expr);
BoolExpr isUnknown = ts.isUnknown(z3Expr);
- BoolExpr isExact = CelZ3TypeSystem.mkNotFlattened(ctx, isApprox);
+ BoolExpr isExact = CelZ3Exprs.mkNotFlattened(ctx, isApprox);
unknowns.add(isUnknown);
- exactErrors.add(CelZ3TypeSystem.mkAndFlattened(ctx, isError, isExact));
- exactUnknowns.add(CelZ3TypeSystem.mkAndFlattened(ctx, isUnknown, isExact));
+ exactErrors.add(CelZ3Exprs.mkAndFlattened(ctx, isError, isExact));
+ exactUnknowns.add(CelZ3Exprs.mkAndFlattened(ctx, isUnknown, isExact));
}
- BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints);
+ BoolExpr anyTaint = CelZ3Exprs.mkOrFlattened(ctx, taints);
if (nonConstZ3Args.isEmpty()) {
return create(baseResult, celExpr, ts, anyTaint);
}
@@ -175,19 +175,19 @@ static TranslatedValue propagateStrict(
Expr finalResult =
ts.propagateErrorAndUnknown(opName, baseResult, nonConstZ3Args, allZ3Args);
- BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors);
- BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns);
- BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns);
+ BoolExpr hasExactError = CelZ3Exprs.mkOrFlattened(ctx, exactErrors);
+ BoolExpr hasExactUnknown = CelZ3Exprs.mkOrFlattened(ctx, exactUnknowns);
+ BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, unknowns);
BoolExpr isSafe =
- CelZ3TypeSystem.mkOrFlattened(
+ CelZ3Exprs.mkOrFlattened(
ctx,
hasExactUnknown,
- CelZ3TypeSystem.mkAndFlattened(
- ctx, hasExactError, CelZ3TypeSystem.mkNotFlattened(ctx, hasUnknown)),
- CelZ3TypeSystem.mkNotFlattened(ctx, anyTaint));
+ CelZ3Exprs.mkAndFlattened(
+ ctx, hasExactError, CelZ3Exprs.mkNotFlattened(ctx, hasUnknown)),
+ CelZ3Exprs.mkNotFlattened(ctx, anyTaint));
- return create(finalResult, celExpr, ts, CelZ3TypeSystem.mkNotFlattened(ctx, isSafe));
+ return create(finalResult, celExpr, ts, CelZ3Exprs.mkNotFlattened(ctx, isSafe));
}
/**
@@ -228,7 +228,7 @@ TranslatedValue withApproximation(BoolExpr approxCondition) {
z3Expr(),
celExpr(),
typeSystem(),
- CelZ3TypeSystem.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition));
+ CelZ3Exprs.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition));
}
}
diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
index 35f96b7ef..dd983d36b 100644
--- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
+++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
@@ -33,6 +33,7 @@
import com.microsoft.z3.SeqExpr;
import dev.cel.common.CelFunctionDecl;
import dev.cel.common.CelOverloadDecl;
+import dev.cel.verifier.CelZ3Exprs;
import dev.cel.verifier.CelZ3TypeSystem;
import java.util.Optional;
@@ -107,7 +108,7 @@ final class OptionalAxioms {
Expr mapRef = ts.getMapRef(actualOperand);
Expr presence =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(
isMsg,
ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str))
@@ -117,7 +118,7 @@ final class OptionalAxioms {
.build(ctx.mkFalse());
Expr value =
- CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(
isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str))
.addCase(
@@ -129,7 +130,7 @@ final class OptionalAxioms {
BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue());
sink.accept(
ctx.mkImplies(
- CelZ3TypeSystem.mkAndFlattened(
+ CelZ3Exprs.mkAndFlattened(
ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence),
valNotError));
diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java
index 0d8698518..baebfff60 100644
--- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java
+++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java
@@ -22,6 +22,7 @@
import dev.cel.common.types.MapType;
import dev.cel.common.types.OptionalType;
import dev.cel.common.types.SimpleType;
+import dev.cel.verifier.CelZ3Exprs;
import dev.cel.verifier.CelZ3TypeSystem;
import java.util.Optional;
@@ -48,7 +49,7 @@ final class TypeAxiom {
.build();
private static Expr getTypeExpression(Context ctx, CelZ3TypeSystem typeSystem, Expr val) {
- return CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+ return CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(
typeSystem.isStruct(val),
typeSystem.wrapString(typeSystem.getMsgTypeName(typeSystem.getMessageRef(val))))
diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
index 5a9eaea02..41af9ae8c 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
@@ -499,6 +499,31 @@ public void verifyInvariants_verificationVariablesAndMultiClauseLists_verified()
assertThat(results).containsExactly("ergonomic_inv", CelVerificationResult.verified());
}
+ @Test
+ public void verifyInvariants_literalListVariableBeyondUnrollLimit_verified() throws Exception {
+ String policySource =
+ "name: literal_list_policy\n" //
+ + "rule:\n" //
+ + " variables:\n" //
+ + " - xs: '[1, 2, 3, 4, 5, 6]'\n" //
+ + " match:\n" //
+ + " - output: 'true'\n" //
+ + "verification:\n" //
+ + " invariants:\n" //
+ + " - id: all_positive\n" //
+ + " assert: variables.xs.all(x, x > 0)";
+ CelPolicy policy = PARSER.parse(policySource);
+ CelPolicyVerifier verifier =
+ CelPolicyVerifierFactory.newVerifier(
+ POLICY_COMPILER,
+ CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(5).build())
+ .build();
+
+ ImmutableMap results = verifier.verifyInvariants(policy);
+
+ assertThat(results).containsExactly("all_positive", CelVerificationResult.verified());
+ }
+
@Test
public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws Exception {
Cel extendedCel =
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
index 217b2168e..f8c747452 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -742,6 +742,9 @@ private enum IsAlwaysTrueTestCase {
OPTIONAL_VALUE_VAR("optional.of(x).value() == x"),
OPTIONAL_HAS_VALUE_VAR("optional.of(x).hasValue()"),
OPTIONAL_VAR_HAS_VALUE_IMPLIES_INT("opt_var.hasValue() ? type(opt_var.value()) == int : true"),
+ OPTIONAL_LIST_INDEX("size(int_list) > 0 ? int_list[?0].value() == int_list[0] : true"),
+ OPTIONAL_MAP_INDEX(
+ "'a' in string_int_map ? string_int_map[?'a'].value() == string_int_map['a'] : true"),
IEEE_754_PROTO_NEG_ZERO_NEQ(
"TestAllTypes{single_double: -0.0} != TestAllTypes{single_double: 0.0}"),
@@ -978,6 +981,7 @@ private enum IsAlwaysTrueTestCase {
"size(int_list) > 15 ? type(int_list[dyn(15)]) == int : true"),
MAP_INDEX_TYPE_CONSTRAINT(
"'key' in string_int_map ? type(string_int_map['key']) == int : true"),
+ FIELD_SELECTION_TYPE_CONSTRAINT("type(test_all_types.single_int64) == int"),
LITERAL_LIST_INDEX("[1, 2][0] == 1"),
NESTED_LIST_VARIABLES_EQUALITY(
"nested_list == [[1]] && nested_list_2 == [[1]] ? nested_list == nested_list_2 : true"),
@@ -1045,6 +1049,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown(
"x == x",
"[x] == [x]",
"{1: x} == {1: x}",
+ "size(int_list) == 1 ? int_list.all(i, x == x) : true",
})
String expression)
throws Exception {
@@ -1569,6 +1574,12 @@ private enum IsAlwaysTrueViolationTestCase {
"[true, 1/0].exists(x, x) == true",
"Condition is not always true\\.",
"\\(The expression fails unconditionally, regardless of input state\\)"),
+ // The non-negative element can't make the step false, so only an error at 0 violates it.
+ DYNAMIC_LIST_ALL_STEP_ERROR_PROPAGATES(
+ "size(int_list) == 1 && int_list[0] >= 0 ? int_list.all(x, 10 / x >= 0) : true",
+ "Condition is not always true\\.",
+ "Counterexample input:",
+ "int_list = \\[0\\]"),
DYNAMIC_STRING_MACRO_TYPE_MISMATCH(
"unknown_var == 1 ? !(unknown_var.contains('a') == true || unknown_var.contains('a') =="
+ " false) : true",