Structured counterexample and CEGAR

PiperOrigin-RevId: 965286727

Author: l46kok

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

@@ -11,6 +11,7 @@ package(
 java_library(
     name = "verifier",
     srcs = [
+        "CelCounterexample.java",
         "CelVerificationException.java",
         "CelVerificationResult.java",
         "CelVerifier.java",
@@ -23,6 +24,8 @@ java_library(
         "//common:cel_ast",
         "//common/types:type_providers",
         "@maven//:com_google_errorprone_error_prone_annotations",
+        "@maven//:com_google_guava_guava",
+        "@maven//:org_jspecify_jspecify",
     ],
 )
 
@@ -180,9 +183,11 @@ java_library(
         "//common/types",
         "//common/types:cel_types",
         "//common/types:type_providers",
+        "//common/values:cel_byte_string",
         "//optimizer",
         "//optimizer:optimization_exception",
         "//optimizer:optimizer_builder",
+        "//runtime:evaluation_exception",
         "//verifier/axioms",
         "@maven//:com_google_errorprone_error_prone_annotations",
         "@maven//:com_google_guava_guava",

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

@@ -0,0 +1,99 @@
+// 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 com.google.errorprone.annotations.Immutable;
+import dev.cel.common.types.CelType;
+import java.util.Map;
+import java.util.Optional;
+import org.jspecify.annotations.Nullable;
+
+/** Encapsulates a structured variable assignment model produced by formal verification. */
+@AutoValue
+@AutoValue.CopyAnnotations
+@Immutable
+public abstract class CelCounterexample {
+
+  /** Represents a single variable binding within a counterexample. */
+  @AutoValue
+  @AutoValue.CopyAnnotations
+  @Immutable
+  @SuppressWarnings("Immutable") // Values are deeply immutable.
+  public abstract static class Binding {
+    /** Returns the name of the variable. */
+    public abstract String name();
+
+    /** Returns the inferred CEL type of the variable. */
+    public abstract CelType type();
+
+    /**
+     * Returns the native Java representation of the value (e.g., Long, Boolean, String, Instant,
+     * Duration, ImmutableList, ImmutableMap, Message, etc.), or empty if unassigned or unavailable.
+     */
+    public abstract Optional<Object> nativeValue();
+
+    /**
+     * Returns the CEL literal representation of the value (e.g., "80", "\"admin\"", "true", "[1,
+     * 2]").
+     */
+    public abstract String celString();
+
+    public static Binding of(
+        String name, CelType type, @Nullable Object nativeValue, String celString) {
+      return new AutoValue_CelCounterexample_Binding(
+          name, type, Optional.ofNullable(nativeValue), celString);
+    }
+  }
+
+  /** Returns all variable bindings keyed by variable name. */
+  public abstract ImmutableMap<String, Binding> bindings();
+
+  /** Returns true if this counterexample was derived from an approximate solver model. */
+  public abstract boolean isApproximate();
+
+  /** Returns true if this model represents a satisfying assignment rather than a counterexample. */
+  public abstract boolean isSatisfyingInput();
+
+  /** Returns the formatted display string representation. */
+  public abstract String toDisplayString();
+
+  /** Looks up a variable binding by name. */
+  public Optional<Binding> get(String variableName) {
+    return Optional.ofNullable(bindings().get(variableName));
+  }
+
+  /**
+   * Returns a native Java variable map suitable for evaluating expressions in CelRuntime (e.g.,
+   * Cel.createProgram().eval(toEvaluationContext())).
+   */
+  public ImmutableMap<String, Object> toEvaluationContext() {
+    ImmutableMap.Builder<String, Object> builder = ImmutableMap.builder();
+    for (Binding binding : bindings().values()) {
+      binding.nativeValue().ifPresent(value -> builder.put(binding.name(), value));
+    }
+    return builder.buildOrThrow();
+  }
+
+  public static CelCounterexample create(
+      Map<String, Binding> bindings,
+      boolean isApproximate,
+      boolean isSatisfyingInput,
+      String toDisplayString) {
+    return new AutoValue_CelCounterexample(
+        ImmutableMap.copyOf(bindings), isApproximate, isSatisfyingInput, toDisplayString);
+  }
+}

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

@@ -15,9 +15,12 @@
 package dev.cel.verifier;
 
 import com.google.auto.value.AutoValue;
+import com.google.errorprone.annotations.Immutable;
+import java.util.Optional;
 
 /** Result object containing the outcome of a CEL AST verification check. */
 @AutoValue
+@Immutable
 public abstract class CelVerificationResult {
 
   /** Represents the outcome of the verification process. */
@@ -38,11 +41,12 @@ public enum VerificationStatus {
    */
   public abstract String reason();
 
-  /**
-   * Returns a detailed counterexample or satisfying model assignment, if one was found.
-   */
+  /** Returns a detailed counterexample or satisfying model assignment string, if one was found. */
   public abstract String counterexample();
 
+  /** Returns the structured counterexample or satisfying model assignment, if one was found. */
+  public abstract Optional<CelCounterexample> counterexampleModel();
+
   /**
    * 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 +57,46 @@ public String message() {
   }
 
   static CelVerificationResult verified() {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VERIFIED, "", "", Optional.empty());
   }
 
   static CelVerificationResult verified(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VERIFIED, reason, "", Optional.empty());
+  }
+
+  static CelVerificationResult verified(String reason, CelCounterexample counterexample) {
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VERIFIED,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 
   static CelVerificationResult failed(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VIOLATED, reason, "", Optional.empty());
   }
 
-  static CelVerificationResult failed(String reason, String counterexample) {
+  static CelVerificationResult failed(String reason, CelCounterexample counterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.VIOLATED, reason, counterexample);
+        VerificationStatus.VIOLATED,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 
   static CelVerificationResult inconclusive(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.INCONCLUSIVE, reason, "", Optional.empty());
   }
 
-  static CelVerificationResult inconclusive(String reason, String counterexample) {
+  static CelVerificationResult inconclusive(String reason, CelCounterexample counterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.INCONCLUSIVE, reason, counterexample);
+        VerificationStatus.INCONCLUSIVE,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 }

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

@@ -82,6 +82,18 @@ public interface CelVerifierBuilder {
   @CanIgnoreReturnValue
   CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit);
 
+  /**
+   * Enables or disables Counterexample-Guided Abstraction Refinement (CEGAR).
+   *
+   * <p>When enabled, if the SMT solver returns an approximate model (e.g., due to unmodeled custom
+   * functions, approximations, or bounded loops), the candidate inputs are validated using concrete
+   * {@link dev.cel.bundle.Cel} program execution. If concrete evaluation confirms an invariant
+   * violation or equivalence divergence, the result is upgraded from {@code INCONCLUSIVE} to {@code
+   * VIOLATED}.
+   */
+  @CanIgnoreReturnValue
+  CelVerifierBuilder setEnableCegarRefinement(boolean enableCegarRefinement);
+
   /** Builds the {@link CelVerifier} instance. */
   CelVerifier build();
 }