Prevent error values in map and list counterexamples

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

@@ -1247,9 +1247,10 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
       }
       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));
+      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 (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val);
@@ -1289,15 +1290,13 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
     }
 
     if (type instanceof ListType) {
-      // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers
-      // here.
+      // 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();
-      if (elemType.equals(SimpleType.DYN)) {
-        return isList;
-      }
 
-      // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i])
       Expr<?> listRef = typeSystem.getListRef(val);
       SeqExpr seq = typeSystem.getSeq(listRef);
       Expr length = ctx.mkLength(seq);
@@ -1307,20 +1306,58 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
       for (int i = 0; i < comprehensionUnrollLimit; i++) {
         IntExpr idx = ctx.mkInt(i);
         Expr elem = ctx.mkNth(seq, idx);
-        BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
         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));
-        BoolExpr outOfBounds = ctx.mkGe(idx, length);
-        boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown())));
       }
 
       return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type instanceof MapType) {
-      // Do NOT emit a for-all quantifier over map keys here.
-      // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is
-      // naturally constrained by the primitive key assertions in getStructuralEquality().
-      return typeSystem.isMap(val);
+      // 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<BoolExpr> boundsAndTypes = new ArrayList<>();
+      boundsAndTypes.add(isMap);
+
+      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.isError(mapVal));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
+      }
+
+      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type.kind() == CelKind.STRUCT) {
       return ctx.mkAnd(

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

@@ -127,6 +127,8 @@ private static String formatExpr(
       return "Error";
     } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) {
       return "Unknown";
+    } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) {
+      return "null";
     } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) {
       Expr<?> optRef = expr.getArgs()[0];
       Expr<?> hasValueExpr =

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

@@ -685,6 +685,11 @@ public Expr<?> getBytes(Expr<?> val) {
     return ctx.mkApp(bytesCons.getAccessorDecls()[0], val);
   }
 
+  /** Checks if the given CelValue is a valid primitive map key type. */
+  public BoolExpr isPrimitiveKey(Expr<?> val) {
+    return ctx.mkOr(isBool(val), isInt(val), isUint(val), isString(val), isBytes(val));
+  }
+
   /** Checks if the given CelValue is a struct (message). */
   public BoolExpr isStruct(Expr<?> val) {
     return isMessage(val);

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

@@ -197,6 +197,80 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception
     assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)");
   }
 
+  @Test
+  public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
+    assertThat(result.message()).contains("Condition is satisfiable.");
+    assertThat(result.message()).contains("Satisfying input:");
+    assertThat(result.message()).contains("string_int_map = {");
+    assertThat(result.message()).doesNotContain("Error");
+  }
+
+  @Test
+  public void isSatisfiable_listNoContainerError_returnsSatisfyingModel() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("dyn_list.size() == 1").getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
+    assertThat(result.message()).contains("Condition is satisfiable.");
+    assertThat(result.message()).contains("Satisfying input:");
+    assertThat(result.message()).contains("dyn_list = [");
+    assertThat(result.message()).doesNotContain("Error");
+  }
+
+  @Test
+  public void isSatisfiable_dynMapNoContainerError_returnsSatisfyingModel() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("dyn_map.size() == 1").getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
+    assertThat(result.message()).contains("Condition is satisfiable.");
+    assertThat(result.message()).contains("Satisfying input:");
+    assertThat(result.message()).contains("dyn_map = {");
+    assertThat(result.message()).doesNotContain("Error");
+  }
+
+  @Test
+  public void counterexample_nullValueFormattedAsNull() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("unknown_var == 3u && request == null").getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
+    assertThat(result.message()).contains("request = null");
+  }
+
+  private enum CounterexampleNeverErrorTestCase {
+    DYN_LIST_REFLEXIVITY("dyn_list.size() == 1 ? dyn_list[0] == dyn_list[0] : true"),
+    DYN_MAP_REFLEXIVITY("dyn_map.size() == 1 ? dyn_map[1] == dyn_map[1] : true"),
+    DYN_LIST_ELEMENT("size(dyn_list) == 1 && dyn_list[0] == 'impossible_value'"),
+    DYN_MAP_VALUE("size(dyn_map) == 1 && dyn_map['a'] == 'impossible_value'"),
+    ;
+
+    final String expr;
+
+    CounterexampleNeverErrorTestCase(String expr) {
+      this.expr = expr;
+    }
+  }
+
+  @Test
+  public void isAlwaysTrue_counterexampleNeverContainsError(
+      @TestParameter CounterexampleNeverErrorTestCase testCase) throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst();
+
+    CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED);
+    assertThat(result.message()).doesNotContain("Error");
+  }
+
   @Test
   public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exception {
     CelAbstractSyntaxTree ast = CEL.compile("1 + 1 == 2").getAst();
@@ -747,6 +821,9 @@ private enum IsAlwaysTrueTestCase {
     UINT64_BOUNDS_ALWAYS_TRUE("u <= 18446744073709551615u && u >= 0u"),
     MODULO_INT64_MIN_INT_BY_NEG_ONE_ALWAYS_ZERO(
         "x == -9223372036854775808 && y == -1 ? x % y == 0 : true"),
+    DYNAMIC_VAR_TYPE_IDENTITY("type(dyn_var) == type(dyn_var)"),
+    DYNAMIC_MAP_KEY_COMPREHENSION_TYPE_IDENTITY(
+        "size(dyn_map) > 0 && size(dyn_map) <= 5 ? dyn_map.all(k, type(k) == type(k)) : true"),
     ;
 
     final String expr;