Generate satisfiable model for isSatisfiable

PiperOrigin-RevId: 950258249

Author: l46kok

verifier/README.md

@@ -229,16 +229,6 @@ public class PolicyVerifierExample {
 
 ### Limitations
 
-*   **Cross-Type Numeric Comparisons:**
-    *   **Equality (`==`, `!=`):** Equality comparisons between different
-        numeric types (e.g., `int` vs `double` or `uint` vs `double`) are
-        currently not supported and will evaluate to `false` during
-        verification, even if they have the same mathematical value (e.g.,
-        `dyn(1) == dyn(1.0)` is false). Note that `int` vs `uint` equality *is*
-        supported.
-    *   **Relational Operators (`<`, `>`, `<=`, `>=`):** Cross-type relational
-        comparisons are fully supported mathematically across all numeric
-        combinations (`int`, `uint`, and `double`).
 *   **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

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

@@ -564,7 +564,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a
     typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast));
 
     return TranslatedValue.propagateStrict(
-        ctx, typeSystem, fieldAccess, celExpr, Arrays.asList(operandTv));
+        ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv));
   }
 
   private TranslatedValue translateBlock(

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

@@ -34,15 +34,20 @@ public enum VerificationStatus {
   public abstract VerificationStatus status();
 
   /**
-   * Returns a message detailing why the verification failed or was inconclusive (e.g., the
-   * counterexample input or truncation reason). Empty if status is VERIFIED.
+   * Returns a message detailing the outcome of the verification check, such as a counterexample
+   * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
+   * and no model inputs apply (e.g., when verifying isAlwaysTrue without counterexamples).
    */
   public abstract String message();
 
   static CelVerificationResult verified() {
     return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "");
   }
 
+  static CelVerificationResult verified(String message) {
+    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, message);
+  }
+
   static CelVerificationResult failed(String message) {
     return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, message);
   }

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

@@ -22,7 +22,9 @@
 public interface CelVerifier {
 
   /**
-   * Returns verified if there is at least one input combination where the AST evaluates to true.
+   * Returns verified if there is at least one input combination where the AST evaluates to true. If
+   * the expression is satisfiable and depends on input variables, the result message will contain a
+   * satisfying model (witness) with concrete variable assignments.
    *
    * @param ast The input expression to verify. Must be a type-checked AST.
    */

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

@@ -192,13 +192,21 @@ public CelVerificationResult verifyEquivalence(
           return CelVerificationResult.failed(
               "Equivalence violation detected."
                   + getCounterexampleString(
-                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ false));
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ false,
+                      /* isCounterexample= */ true));
         case APPROXIMATE_MATCH:
           return CelVerificationResult.inconclusive(
               "Inconclusive: a divergence may exist, but it depends on approximations, missing"
                   + " theories, or loop bounds."
                   + getCounterexampleString(
-                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ true));
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ true,
+                      /* isCounterexample= */ true));
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               "Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -250,8 +258,16 @@ private CelVerificationResult checkSatisfiability(
                           ctx,
                           translator.getTypeSystem(),
                           result.model,
-                          /* isApproximate= */ false))
-              : CelVerificationResult.verified();
+                          /* isApproximate= */ false,
+                          /* isCounterexample= */ true))
+              : CelVerificationResult.verified(
+                  "Condition is satisfiable."
+                      + getCounterexampleString(
+                          ctx,
+                          translator.getTypeSystem(),
+                          result.model,
+                          /* isApproximate= */ false,
+                          /* isCounterexample= */ false));
 
         case APPROXIMATE_MATCH:
           String prefix =
@@ -263,7 +279,11 @@ private CelVerificationResult checkSatisfiability(
           return CelVerificationResult.inconclusive(
               prefix
                   + getCounterexampleString(
-                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ true));
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ true,
+                      /* isCounterexample= */ searchForCounterexample));
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
@@ -357,8 +377,13 @@ private Solver newSolver(Context ctx) {
   }
 
   private static String getCounterexampleString(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, boolean isApproximate) {
-    return CelZ3CounterexampleGenerator.generate(ctx, typeSystem, model, isApproximate);
+      Context ctx,
+      CelZ3TypeSystem typeSystem,
+      Model model,
+      boolean isApproximate,
+      boolean isCounterexample) {
+    return CelZ3CounterexampleGenerator.generate(
+        ctx, typeSystem, model, isApproximate, isCounterexample);
   }
 
   CelVerifierZ3Impl(

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

@@ -36,7 +36,11 @@ final class CelZ3CounterexampleGenerator {
   private CelZ3CounterexampleGenerator() {}
 
   static String generate(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, boolean isApproximate) {
+      Context ctx,
+      CelZ3TypeSystem typeSystem,
+      Model model,
+      boolean isApproximate,
+      boolean isCounterexample) {
     FuncDecl[] constDecls = model.getConstDecls();
 
     List<String> bindings = new ArrayList<>();
@@ -55,10 +59,17 @@ static String generate(
     }
 
     if (bindings.isEmpty()) {
-      return " (The expression fails unconditionally, regardless of input state)";
+      return isCounterexample
+          ? " (The expression fails unconditionally, regardless of input state)"
+          : " (The expression is satisfiable unconditionally, regardless of input state)";
     }
 
-    String prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:";
+    String prefix;
+    if (isCounterexample) {
+      prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:";
+    } else {
+      prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:";
+    }
     return prefix + String.join("", bindings);
   }
 
@@ -228,6 +239,9 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
       if (++iterations > 100_000) {
         throw new IllegalStateException("Exceeded maximum number of extractKeys iterations.");
       }
+      if (!arrayExpr.isApp()) {
+        break;
+      }
       FuncDecl<?> decl = arrayExpr.getFuncDecl();
       String declName = decl.getName().toString();