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,6 +183,7 @@ java_library(
         "//common/types",
         "//common/types:cel_types",
         "//common/types:type_providers",
+        "//common/values:cel_byte_string",
         "//optimizer",
         "//optimizer:optimization_exception",
         "//optimizer:optimizer_builder",

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

@@ -0,0 +1,109 @@
+// 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
+@SuppressWarnings("Immutable")
+public abstract class CelCounterexample {
+
+  /** Represents a single variable binding within a counterexample. */
+  @AutoValue
+  @AutoValue.CopyAnnotations
+  @Immutable
+  @SuppressWarnings("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 null if unassigned or null.
+     */
+    public abstract @Nullable 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, 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 b : bindings().values()) {
+      if (b.nativeValue() != null) {
+        builder.put(b.name(), b.nativeValue());
+      }
+    }
+    return builder.buildOrThrow();
+  }
+
+  public static CelCounterexample create(
+      Map<String, Binding> bindings,
+      boolean isApproximate,
+      boolean isSatisfyingInput,
+      String displayString) {
+    return new AutoValue_CelCounterexample(
+        ImmutableMap.copyOf(bindings), isApproximate, isSatisfyingInput, displayString);
+  }
+
+  public static CelCounterexample empty() {
+    return new AutoValue_CelCounterexample(
+        ImmutableMap.of(),
+        /* isApproximate= */ false,
+        /* isSatisfyingInput= */ false,
+        /* displayString= */ "");
+  }
+}

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

@@ -15,9 +15,13 @@
 package dev.cel.verifier;
 
 import com.google.auto.value.AutoValue;
+import com.google.common.collect.ImmutableMap;
+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 +42,24 @@ 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 the variable bindings as a map of variable name to stringified CEL literal syntax. */
+  public ImmutableMap<String, String> counterexampleBindings() {
+    return counterexampleModel()
+        .map(
+            model -> {
+              ImmutableMap.Builder<String, String> builder = ImmutableMap.builder();
+              model.bindings().forEach((k, v) -> builder.put(k, v.celString()));
+              return builder.buildOrThrow();
+            })
+        .orElseGet(ImmutableMap::of);
+  }
+
   /**
    * 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 +70,56 @@ 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) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.VIOLATED, reason, counterexample);
+        VerificationStatus.VIOLATED, reason, counterexample, Optional.empty());
+  }
+
+  static CelVerificationResult failed(String reason, CelCounterexample counterexample) {
+    return new AutoValue_CelVerificationResult(
+        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) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.INCONCLUSIVE, reason, counterexample);
+        VerificationStatus.INCONCLUSIVE, reason, counterexample, Optional.empty());
+  }
+
+  static CelVerificationResult inconclusive(String reason, CelCounterexample counterexample) {
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.INCONCLUSIVE,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 }

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

@@ -82,6 +82,20 @@ 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
+  default CelVerifierBuilder setEnableCegarRefinement(boolean enableCegarRefinement) {
+    return this;
+  }
+
   /** Builds the {@link CelVerifier} instance. */
   CelVerifier build();
 }