Add variable bounds for optionals

PiperOrigin-RevId: 952363986

Author: l46kok

verifier/README.md

@@ -47,17 +47,17 @@ properties about your expressions.
     counterexample showing the inputs that caused the violation. When checking
     satisfiability (`isSatisfiable`), it generates concrete variable assignments
     (satisfying model / witness) showing the inputs that satisfy the condition.
-*   **Partial Evaluation (Unknowns) Support:** Define variables that are
-    permitted to evaluate to `Unknown` during verification, mirroring CEL's
-    runtime partial evaluation.
 *   **Custom Invariants Verification:** Allows policy authors to define safety
     invariants (e.g., "port must always be secure if external access is
     allowed") and mathematically prove that the policy never violates them
     across all possible input states.
+*   **Partial Evaluation (Unknowns) Support:** Define variables that are
+    permitted to evaluate to `Unknown` during verification, mirroring CEL's
+    runtime partial evaluation.
 
 ```java
 CelVerifier verifier = CelVerifierFactory.newVerifier()
-    .addUnknownIdentifier("request.headers") // Exclude dynamic fields from failure paths
+    .addUnknownIdentifier("request.headers") // Exclude unknown fields from failure paths
     .build();
 ```
 

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

@@ -23,7 +23,6 @@
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FuncDecl;
 import com.microsoft.z3.IntExpr;
-import com.microsoft.z3.Pattern;
 import com.microsoft.z3.Quantifier;
 import com.microsoft.z3.SeqExpr;
 import com.microsoft.z3.Sort;
@@ -41,6 +40,7 @@
 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;
@@ -79,7 +79,6 @@ final class CelAstToZ3Translator {
   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 MAP_BIJECTION_PREFIX = "k_map_bijection";
   private final Context ctx;
   private final CelZ3TypeSystem typeSystem;
   private final CelZ3OperatorTranslator operatorTranslator;
@@ -289,9 +288,13 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
       for (int i = 0; i < elements.size(); i++) {
         CelExpr element = elements.get(i);
         TranslatedValue elem = translateExpr(element, ast);
-        elementsTv.add(elem);
 
         if (optionalIndices.contains(i)) {
+          Expr<?> checkedValue =
+              typeSystem.withRuntimeError(
+                  elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr())));
+          elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());
+
           Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
           seq =
               (SeqExpr)
@@ -302,6 +305,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
         } else {
           seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
         }
+        elementsTv.add(elem);
       }
       listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX);
       typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq));
@@ -329,15 +333,22 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
       elementsTv.add(keyTv);
       TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
       Expr<?> value = valueTv.z3Expr();
-      elementsTv.add(valueTv);
 
       Expr<?> finalValue = value;
       BoolExpr finalPresence = ctx.mkTrue();
       if (entryAst.optionalEntry()) {
+        Expr<?> checkedValue =
+            typeSystem.withRuntimeError(value, ctx.mkNot(typeSystem.isOptional(value)));
+        valueTv =
+            TranslatedValue.create(
+                checkedValue, entryAst.value(), typeSystem, valueTv.isApproximate());
+        value = checkedValue;
+
         Expr<?> optRef = typeSystem.getOptionalRef(value);
         finalPresence = typeSystem.optHasValue(optRef);
         finalValue = typeSystem.getOptionalValue(optRef);
       }
+      elementsTv.add(valueTv);
 
       BoolExpr keyAlreadyPresent = (BoolExpr) ctx.mkSelect(mapPresence, key);
       BoolExpr shouldInsertKey = ctx.mkAnd(ctx.mkNot(keyAlreadyPresent), finalPresence);
@@ -384,7 +395,6 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
       Expr<?> key = ctx.mkString(entryAst.fieldKey());
       TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
       Expr<?> value = valueTv.z3Expr();
-      elementsTv.add(valueTv);
 
       CelType fieldType =
           typeProvider
@@ -399,10 +409,18 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
       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());
+        value = checkedValue;
+
         Expr<?> optRef = typeSystem.getOptionalRef(value);
         optionalHasValue = typeSystem.optHasValue(optRef);
         finalValue = typeSystem.getOptionalValue(optRef);
       }
+      elementsTv.add(valueTv);
 
       // Canonicalization Trick:
       //
@@ -438,6 +456,9 @@ 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);
     }
@@ -819,36 +840,18 @@ private void applyBoundedMapBijection(
       }
     }
 
-    Expr<?> kVar = ctx.mkFreshConst(MAP_BIJECTION_PREFIX, typeSystem.celValueSort());
-    BoolExpr isValidKey =
-        ctx.mkOr(
-            typeSystem.isInt(kVar), typeSystem.isUint(kVar),
-            typeSystem.isBool(kVar), typeSystem.isString(kVar));
-    BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, kVar);
+    BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
 
-    List<BoolExpr> inSeqMatches = new ArrayList<>();
+    ArrayExpr seqMap = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse());
     for (int i = 0; i < comprehensionUnrollLimit; i++) {
-      BoolExpr match =
-          ctx.mkAnd(
-              ctx.mkLt(ctx.mkInt(i), lengthExpr), ctx.mkEq(kVar, ctx.mkNth(seq, ctx.mkInt(i))));
-      inSeqMatches.add(match);
+      seqMap =
+          (ArrayExpr)
+              ctx.mkITE(
+                  ctx.mkLt(ctx.mkInt(i), lengthExpr),
+                  ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
+                  seqMap);
     }
-    BoolExpr inSeq = CelZ3TypeSystem.mkOrFlattened(ctx, inSeqMatches);
-
-    BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
-
-    Pattern inMapPattern = ctx.mkPattern(inMap);
-
-    BoolExpr completeness =
-        ctx.mkForall(
-            new Expr<?>[] {kVar},
-            ctx.mkImplies(ctx.mkAnd(isNotTruncated, isValidKey, inMap), inSeq),
-            1,
-            new Pattern[] {inMapPattern},
-            null,
-            null,
-            null);
-    typeConstraints.add(completeness);
+    typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
   }
 
   private TranslatedValue[] evaluateLoopCondAndStep(
@@ -1167,6 +1170,24 @@ private BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSynta
   }
 
   private 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 (paramType.kind().isDyn() || paramType.kind().isTypeParam()) {
+        return isOpt;
+      }
+      Expr<?> optRef = typeSystem.getOptionalRef(val);
+      BoolExpr hasValue = typeSystem.optHasValue(optRef);
+      BoolExpr valConstraint =
+          createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType);
+      return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint));
+    }
     if (type.equals(SimpleType.BOOL)) {
       return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val);
     }

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

@@ -42,6 +42,7 @@
 import dev.cel.common.ast.CelExpr.CelCall;
 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.ProtoMessageTypeProvider;
 import dev.cel.common.types.SimpleType;
@@ -102,6 +103,8 @@ public final class CelVerifierZ3ImplTest {
           .addVar("dyn_var", SimpleType.DYN)
           .addVar("dyn_var2", SimpleType.DYN)
           .addVar("opt_var", OptionalType.create(SimpleType.INT))
+          .addVar("opt_dyn_var", OptionalType.create(SimpleType.DYN))
+          .addVar("nullable_int", NullableType.create(SimpleType.INT))
           .addVar("string_int_map", MapType.create(SimpleType.STRING, SimpleType.INT))
           .addVar("bytes_val", SimpleType.BYTES)
           .addVar(
@@ -147,7 +150,8 @@ private enum IsSatisfiableTestCase {
         "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"),
     CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"),
     MACRO_LIMIT("dyn_list.all(x, x == 1)"),
-    STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field");
+    STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"),
+    NULLABLE_INT_SATISFIABLE("nullable_int == 123");
 
     final String expr;
 
@@ -463,6 +467,8 @@ private enum IsAlwaysTrueTestCase {
     OPTIONAL_OR_NONE_IS_NONE("optional.none().or(optional.none()) == optional.none()"),
     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"),
+    
     IEEE_754_PROTO_NEG_ZERO_NEQ(
         "TestAllTypes{single_double: -0.0} != TestAllTypes{single_double: 0.0}"),
     IEEE_754_ROUND_NEAREST_TIES_TO_EVEN_DOWN("1.0 + 1.1102230246251565e-16 == 1.0"),
@@ -637,6 +643,7 @@ private enum IsAlwaysTrueTestCase {
     WRAPPER_SET_NULL_IS_NULL(
         "TestAllTypes{single_int64_wrapper: null}.single_int64_wrapper == null"),
     WRAPPER_SET_NULL_EQ_UNSET("TestAllTypes{single_int64_wrapper: null} == TestAllTypes{}"),
+    WRAPPER_SET_NON_NULL_EQ("TestAllTypes{single_int64_wrapper: 123}.single_int64_wrapper == 123"),
     STRING_CONTAINS_EMPTY("role.contains('')"),
     STRING_STARTS_WITH_EMPTY("role.startsWith('')"),
     STRING_ENDS_WITH_EMPTY("role.endsWith('')"),
@@ -1031,6 +1038,26 @@ private enum IsAlwaysTrueViolationTestCase {
         "!(request == unknown_var && type(request) == int && type(unknown_var) == double)",
         "Condition is not always true.",
         "Counterexample input:"),
+    OPTIONAL_DYN_VAR_HAS_VALUE_NOT_IMPLIES_INT(
+        "opt_dyn_var.hasValue() ? type(opt_dyn_var.value()) == int : true",
+        "Condition is not always true.",
+        "Counterexample input:",
+        "opt_dyn_var ="),
+    OPTIONAL_ENTRY_DYN_VAR_TYPE_MISMATCH(
+        "[?dyn_var] == [?dyn_var] ? true : true",
+        "Condition is not always true.",
+        "Counterexample input:",
+        "dyn_var ="),
+    OPTIONAL_MAP_ENTRY_DYN_VAR_TYPE_MISMATCH(
+        "{?1: dyn_var} == {?1: dyn_var} ? true : true",
+        "Condition is not always true.",
+        "Counterexample input:",
+        "dyn_var ="),
+    OPTIONAL_STRUCT_ENTRY_DYN_VAR_TYPE_MISMATCH(
+        "cel.expr.conformance.proto3.TestAllTypes{?single_int32: dyn_var} == cel.expr.conformance.proto3.TestAllTypes{?single_int32: dyn_var} ? true : true",
+        "Condition is not always true.",
+        "Counterexample input:",
+        "dyn_var ="),
     DYNAMIC_MAP_ALL_VIOLATION(
         "string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k == 'a') : true",
         "Condition is not always true.",
@@ -1430,8 +1457,9 @@ private enum EquivalenceTestCase {
         "TestAllTypes{?repeated_int32: optional.of([1, 2])}",
         "cel.expr.conformance.proto3.TestAllTypes{repeated_int32: [1, 2]}"),
     OPTIONAL_PRUNE_LIST_EQUALITY("[?optional.none(), 1] == [1]", "true"),
-    OPTIONAL_PRUNE_LIST_COMPREHENSION("[1, ?optional.none()].all(x, x > 0)", "true");
-
+    OPTIONAL_PRUNE_LIST_COMPREHENSION("[1, ?optional.none()].all(x, x > 0)", "true"),
+    MAP_COMPREHENSION(
+        "{'a': 1, 'b': 2}.exists(k, k == 'a')", "{'a': 1, 'b': 2}.exists(k, k == 'a')");
     private final String exprA;
     private final String exprB;