Expose the verifier's counterexamples as structured CelWitness values

PiperOrigin-RevId: 1004026905

Author: l46kok

verifier/README.md

@@ -224,8 +224,8 @@ public class PolicyVerifierExample {
         System.out.println(result.message());
         // Output:
         // Equivalence violation detected. Counterexample input:
-        //   country = "a"
         //   role = "editor"
+        //   country = "a"
         //   port = 443
         break;
       case INCONCLUSIVE:
@@ -241,7 +241,8 @@ public class PolicyVerifierExample {
 When checking whether an expression is satisfiable using `isSatisfiable`, the
 verifier returns `VERIFIED` if there exists at least one input combination
 where the expression evaluates to `true`. Furthermore, `result.message()`
-provides concrete satisfying model assignments (witness/test case generation).
+provides concrete satisfying model assignments (witness/test case generation),
+and `result.witness()` exposes them as CEL runtime values.
 
 ```java
 import dev.cel.common.CelAbstractSyntaxTree;

verifier/src/main/java/dev/cel/verifier/BUILD.bazel

@@ -15,6 +15,7 @@ java_library(
         "CelVerificationResult.java",
         "CelVerifier.java",
         "CelVerifierBuilder.java",
+        "CelWitness.java",
     ],
     tags = [
     ],
@@ -23,6 +24,7 @@ java_library(
         "//common:cel_ast",
         "//common/types:type_providers",
         "@maven//:com_google_errorprone_error_prone_annotations",
+        "@maven//:com_google_guava_guava",
     ],
 )
 
@@ -186,10 +188,13 @@ java_library(
         "//common/ast",
         "//common/ast:cel_block",
         "//common/internal:cel_descriptor_pools",
+        "//common/internal:proto_time_utils",
         "//common/internal:well_known_proto",
         "//common/types",
         "//common/types:cel_types",
         "//common/types:type_providers",
+        "//common/values",
+        "//common/values:cel_byte_string",
         "//optimizer",
         "//optimizer:optimization_exception",
         "//optimizer:optimizer_builder",

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

@@ -92,6 +92,11 @@ CelZ3TypeSystem getTypeSystem() {
     return typeSystem;
   }
 
+  /** Returns the input variables, in order of first appearance. */
+  Set<Expr<?>> getInputVariables() {
+    return context.inputVariables();
+  }
+
   /**
    * Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true.
    */

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

@@ -15,6 +15,8 @@
 package dev.cel.verifier;
 
 import com.google.auto.value.AutoValue;
+import java.util.Map;
+import java.util.Optional;
 
 /** Result object containing the outcome of a CEL AST verification check. */
 @AutoValue
@@ -43,6 +45,12 @@ public enum VerificationStatus {
    */
   public abstract String counterexample();
 
+  /**
+   * Returns the counterexample or satisfying input found by the solver, if any. Its variables are
+   * empty when the outcome doesn't depend on any input.
+   */
+  public abstract Optional<CelWitness> witness();
+
   /**
    * 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
@@ -53,28 +61,65 @@ public String message() {
   }
 
   static CelVerificationResult verified() {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
+    return create(VerificationStatus.VERIFIED, "");
   }
 
-  static CelVerificationResult verified(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
+  static CelVerificationResult verified(String reason, CelWitness satisfyingInput) {
+    return create(
+        VerificationStatus.VERIFIED, reason, satisfyingInput, /* isCounterexample= */ false);
   }
 
   static CelVerificationResult failed(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
+    return create(VerificationStatus.VIOLATED, reason);
   }
 
-  static CelVerificationResult failed(String reason, String counterexample) {
-    return new AutoValue_CelVerificationResult(
-        VerificationStatus.VIOLATED, reason, counterexample);
+  static CelVerificationResult failed(String reason, CelWitness counterexample) {
+    return create(
+        VerificationStatus.VIOLATED, reason, counterexample, /* isCounterexample= */ true);
   }
 
   static CelVerificationResult inconclusive(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
+    return create(VerificationStatus.INCONCLUSIVE, reason);
+  }
+
+  static CelVerificationResult inconclusive(
+      String reason, CelWitness witness, boolean isCounterexample) {
+    return create(VerificationStatus.INCONCLUSIVE, reason, witness, isCounterexample);
   }
 
-  static CelVerificationResult inconclusive(String reason, String counterexample) {
+  private static CelVerificationResult create(VerificationStatus status, String reason) {
+    return new AutoValue_CelVerificationResult(status, reason, "", Optional.empty());
+  }
+
+  private static CelVerificationResult create(
+      VerificationStatus status, String reason, CelWitness witness, boolean isCounterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.INCONCLUSIVE, reason, counterexample);
+        status,
+        reason,
+        describe(witness, status == VerificationStatus.INCONCLUSIVE, isCounterexample),
+        Optional.of(witness));
+  }
+
+  private static String describe(
+      CelWitness witness, boolean isApproximate, boolean isCounterexample) {
+    if (witness.variables().isEmpty()) {
+      return isCounterexample
+          ? " (The expression fails unconditionally, regardless of input state)"
+          : " (The expression is satisfiable unconditionally, regardless of input state)";
+    }
+
+    StringBuilder sb = new StringBuilder();
+    if (isCounterexample) {
+      sb.append(isApproximate ? " Potential counterexample input:" : " Counterexample input:");
+    } else {
+      sb.append(isApproximate ? " Potential satisfying input:" : " Satisfying input:");
+    }
+    for (Map.Entry<String, CelWitness.Variable> variable : witness.variables().entrySet()) {
+      sb.append("\n  ")
+          .append(variable.getKey())
+          .append(" = ")
+          .append(variable.getValue().displayValue());
+    }
+    return sb.toString();
   }
 }

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

@@ -256,23 +256,13 @@ public CelVerificationResult verifyEquivalence(
       switch (result.outcome) {
         case EXACT_MATCH:
           return CelVerificationResult.failed(
-              "Equivalence violation detected.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ false,
-                  /* isCounterexample= */ true));
+              "Equivalence violation detected.", extractWitness(ctx, translator, result.model));
         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,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ true);
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               "Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -343,22 +333,13 @@ CelVerificationResult verifyImplication(
         case EXACT_MATCH:
           return CelVerificationResult.failed(
               String.format("%s violation detected.", subjectName),
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ false,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model));
         case APPROXIMATE_MATCH:
           return CelVerificationResult.inconclusive(
               "Inconclusive: a counterexample may exist, but it depends on approximations, missing"
                   + " theories, or loop bounds.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ true);
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               String.format(
@@ -403,23 +384,10 @@ private CelVerificationResult checkSatisfiability(
 
       switch (result.outcome) {
         case EXACT_MATCH:
+          CelWitness witness = extractWitness(ctx, translator, result.model);
           return searchForCounterexample
-              ? CelVerificationResult.failed(
-                  "Condition is not always true.",
-                  getCounterexampleString(
-                      ctx,
-                      translator.getTypeSystem(),
-                      result.model,
-                      /* isApproximate= */ false,
-                      /* isCounterexample= */ true))
-              : CelVerificationResult.verified(
-                  "Condition is satisfiable."
-                      + getCounterexampleString(
-                          ctx,
-                          translator.getTypeSystem(),
-                          result.model,
-                          /* isApproximate= */ false,
-                          /* isCounterexample= */ false));
+              ? CelVerificationResult.failed("Condition is not always true.", witness)
+              : CelVerificationResult.verified("Condition is satisfiable.", witness);
 
         case APPROXIMATE_MATCH:
           String prefix =
@@ -430,12 +398,8 @@ private CelVerificationResult checkSatisfiability(
                       + " approximations, missing theories, or loop bounds.";
           return CelVerificationResult.inconclusive(
               prefix,
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ searchForCounterexample));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ searchForCounterexample);
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
@@ -538,14 +502,13 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn
         parameterizeUnknowns);
   }
 
-  private static String getCounterexampleString(
-      Context ctx,
-      CelZ3TypeSystem typeSystem,
-      Model model,
-      boolean isApproximate,
-      boolean isCounterexample) {
+  private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) {
     return CelZ3CounterexampleGenerator.generate(
-        ctx, typeSystem, model, isApproximate, isCounterexample);
+        ctx,
+        translator.getTypeSystem(),
+        model,
+        comprehensionUnrollLimit,
+        translator.getInputVariables());
   }
 
   private enum SolverOutcome {

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

@@ -0,0 +1,52 @@
+// 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.auto.value.AutoValue;
+import com.google.common.collect.ImmutableMap;
+import java.util.Optional;
+
+/** An input assignment found by the solver: a counterexample or a satisfying input. */
+@AutoValue
+public abstract class CelWitness {
+
+  /** The value the solver assigned to one input variable. */
+  @AutoValue
+  public abstract static class Variable {
+
+    /**
+     * Returns the value in its CEL runtime representation ({@code Long}, {@code UnsignedLong},
+     * {@code Double}, {@code Boolean}, {@code String}, {@code CelByteString}, {@code Instant},
+     * {@code Duration}, {@code NullValue}, {@code ImmutableList}, {@code ImmutableMap} or {@code
+     * Optional}, nested accordingly), or empty if it has no exact runtime equivalent (e.g. an
+     * unknown).
+     */
+    public abstract Optional<Object> value();
+
+    // The value as a CEL literal where one exists, for display.
+    abstract String displayValue();
+
+    static Variable create(Optional<Object> value, String displayValue) {
+      return new AutoValue_CelWitness_Variable(value, displayValue);
+    }
+  }
+
+  /** Returns the variables keyed by name, in order of first appearance. */
+  public abstract ImmutableMap<String, Variable> variables();
+
+  static CelWitness create(ImmutableMap<String, Variable> variables) {
+    return new AutoValue_CelWitness(variables);
+  }
+}