Treat all uninterpreted function results as approximate

PiperOrigin-RevId: 1003496089

Author: l46kok

verifier/README.md

@@ -370,14 +370,12 @@ public class InvariantsExample {
 
 ### Limitations
 
-*   **Unsupported Standard Functions (Uninterpreted Functions):** Not all
-    CEL standard library functions have SMT axioms defined yet. Unsupported
-    functions are treated as *uninterpreted functions* by Z3 (the solver
-    only guarantees that identical inputs yield identical outputs, but does
-    not understand the function's internal logic or return types).
-    Consequently, verifications that rely on the specific semantics of
-    these functions may return `VerificationStatus.INCONCLUSIVE`. Support for
-    more standard library functions will be added incrementally.
+*   **Uninterpreted Functions:** Custom functions, and standard library
+    functions that don't have SMT axioms yet, are treated as uninterpreted:
+    the solver only knows that identical inputs yield identical outputs.
+    Results that depend on their return values are `INCONCLUSIVE`, and a
+    `VERIFIED` result assumes they return a value of their declared type
+    rather than an error.
 
 ### Best Practices & Performance
 

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

@@ -935,10 +935,15 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
               typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
               typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
 
-              boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
-              BoolExpr isApprox = ctx.mkBool(!isDynamic);
+              // The solver picks the result freely, so a model depending on it is never exact.
               return TranslatedValue.propagateStrict(
-                  ctx, typeSystem, functionName, callRes, Optional.of(expr), isApprox, args);
+                  ctx,
+                  typeSystem,
+                  functionName,
+                  callRes,
+                  Optional.of(expr),
+                  /* baseTaint= */ ctx.mkTrue(),
+                  args);
             });
   }
 

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

@@ -2750,9 +2750,9 @@ public void isAlwaysTrue_operationError_counterexampleFormat() throws Exception
   }
 
   @Test
-  public void isAlwaysTrue_dynamicFunction_nan_violated() throws Exception {
-    // request() == request() is a tautology only if request() does not evaluate to NaN.
-    // Since request() returns DYN, Z3 can assign NaN to its return value, and NaN == NaN is false.
+  public void isAlwaysTrue_dynamicFunction_inconclusive() throws Exception {
+    // request() == request() fails only if request() returns NaN. The solver may pick NaN for an
+    // uninterpreted function, but the actual function may never return it.
     CelCompiler celCompiler =
         CEL.toCompilerBuilder()
             .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))
@@ -2764,8 +2764,26 @@ public void isAlwaysTrue_dynamicFunction_nan_violated() throws Exception {
     CelAbstractSyntaxTree ast = celCompiler.compile("request() == request()").getAst();
     CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
 
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+    assertThat(result.message()).contains("depends on approximations");
+  }
+
+  @Test
+  public void isAlwaysTrue_dynamicFunctionShortCircuited_violated() throws Exception {
+    // x == 0 falsifies the condition regardless of request()'s value.
+    CelCompiler celCompiler =
+        CEL.toCompilerBuilder()
+            .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))
+            .addFunctionDeclarations(
+                CelFunctionDecl.newFunctionDeclaration(
+                    "request",
+                    CelOverloadDecl.newGlobalOverload("request_overload", SimpleType.DYN)))
+            .build();
+    CelAbstractSyntaxTree ast = celCompiler.compile("x != 0 && request() == 1").getAst();
+    CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
+
     assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED);
-    assertThat(result.message()).contains("request = NaN");
+    assertThat(result.message()).contains("x = 0");
   }
 
   @Test
@@ -2785,9 +2803,8 @@ public void isAlwaysTrue_boolFunction_verified() throws Exception {
   }
 
   @Test
-  public void verifyEquivalence_functionError_equivalent() throws Exception {
-    // request() and request() are equivalent, even if request() throws an Error,
-    // because Error == Error structurally in Z3 equivalence.
+  public void verifyEquivalence_identicalFunctionCalls_equivalent() throws Exception {
+    // Identical calls to an uninterpreted function always produce identical results.
     CelCompiler celCompiler =
         CEL.toCompilerBuilder()
             .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))