Make invariant violation messages policy-specific

verifier/BUILD.bazel

@@ -2,14 +2,25 @@ load("@rules_java//java:defs.bzl", "java_library")
 
 package(
     default_applicable_licenses = ["//:license"],
-    default_visibility = ["//:internal"],
+    default_visibility = [":verifier_allow_list"],
+)
+
+VERIFIER_ALLOW_LIST = [
+    "//...",
+]
+
+package_group(
+    name = "verifier_allow_list",
+    packages = VERIFIER_ALLOW_LIST,
+)
+
+package_group(
+    name = "verifier_internal",
+    packages = ["//verifier/..."],
 )
 
 java_library(
     name = "verifier",
-    visibility = [
-        "//:internal",
-    ],
     exports = ["//verifier/src/main/java/dev/cel/verifier"],
 )
 
@@ -27,22 +38,19 @@ java_library(
 java_library(
     name = "verifier_factory",
     compatible_with = [],
-    visibility = [
-        "//:internal",
-    ],
     exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"],
 )
 
 java_library(
     name = "type_system",
     compatible_with = [],
-    visibility = ["//:internal"],
+    visibility = [":verifier_internal"],
     exports = ["//verifier/src/main/java/dev/cel/verifier:type_system"],
 )
 
 java_library(
     name = "z3_impl",
     compatible_with = [],
-    visibility = ["//:internal"],
+    visibility = [":verifier_internal"],
     exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"],
 )

verifier/README.md

@@ -353,7 +353,7 @@ public class InvariantsExample {
         System.out.println("Invariant violated!");
         System.out.println(result.message());
         // Output:
-        // Implication violation detected. Counterexample input:
+        // Invariant 'always_secure' violation detected. Counterexample input:
         //   port = 80
         break;
       case INCONCLUSIVE:

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

@@ -145,10 +145,15 @@ public ImmutableMap<String, CelVerificationResult> verifyInvariants(CelPolicy po
         throw new UnsupportedOperationException(
             "Invariants verification requires Z3 verifier implementation.");
       }
+      String invariantId = invariant.invariantId().value();
       CelVerificationResult result =
           ((CelVerifierZ3Impl) astVerifier)
-              .verifyImplication(assumeAst, assertAst, boundSymbols);
-      resultsBuilder.put(invariant.invariantId().value(), result);
+              .verifyImplication(
+                  assumeAst,
+                  assertAst,
+                  boundSymbols,
+                  String.format("Invariant '%s'", invariantId));
+      resultsBuilder.put(invariantId, result);
     }
 
     return resultsBuilder.buildOrThrow();

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

@@ -33,26 +33,48 @@ public enum VerificationStatus {
   /** Returns the status of the verification check. */
   public abstract VerificationStatus status();
 
+  /**
+   * Returns the primary reason for the verification outcome.
+   */
+  public abstract String reason();
+
+  /**
+   * Returns a detailed counterexample or satisfying model assignment, if one was found.
+   */
+  public abstract String counterexample();
+
   /**
    * 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();
+  public String message() {
+    return reason() + counterexample();
+  }
 
   static CelVerificationResult verified() {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "");
+    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
+  }
+
+  static CelVerificationResult verified(String reason) {
+    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
+  }
+
+  static CelVerificationResult failed(String reason) {
+    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
   }
 
-  static CelVerificationResult verified(String message) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, message);
+  static CelVerificationResult failed(String reason, String counterexample) {
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VIOLATED, reason, counterexample);
   }
 
-  static CelVerificationResult failed(String message) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, message);
+  static CelVerificationResult inconclusive(String reason) {
+    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
   }
 
-  static CelVerificationResult inconclusive(String message) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, message);
+  static CelVerificationResult inconclusive(String reason, String counterexample) {
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.INCONCLUSIVE, reason, counterexample);
   }
 }

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

@@ -36,6 +36,7 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.List;
+import java.util.Locale;
 import java.util.Map;
 import java.util.Optional;
 import org.jspecify.annotations.Nullable;
@@ -193,23 +194,23 @@ 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.",
+              getCounterexampleString(
+                  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,
-                      /* isCounterexample= */ true));
+                  + " theories, or loop bounds.",
+              getCounterexampleString(
+                  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"
@@ -227,7 +228,8 @@ public CelVerificationResult verifyEquivalence(
   CelVerificationResult verifyImplication(
       CelAbstractSyntaxTree assumeAst,
       CelAbstractSyntaxTree assertAst,
-      Map<String, CelAbstractSyntaxTree> boundSymbols)
+      Map<String, CelAbstractSyntaxTree> boundSymbols,
+      String subjectName)
       throws CelVerificationException {
     Preconditions.checkArgument(assumeAst.isChecked(), "assumeAst must be type-checked.");
     Preconditions.checkArgument(assertAst.isChecked(), "assertAst must be type-checked.");
@@ -282,27 +284,27 @@ CelVerificationResult verifyImplication(
       switch (result.outcome) {
         case EXACT_MATCH:
           return CelVerificationResult.failed(
-              "Implication violation detected."
-                  + getCounterexampleString(
-                      ctx,
-                      translator.getTypeSystem(),
-                      result.model,
-                      /* isApproximate= */ false,
-                      /* isCounterexample= */ true));
+              String.format("%s violation detected.", subjectName),
+              getCounterexampleString(
+                  ctx,
+                  translator.getTypeSystem(),
+                  result.model,
+                  /* isApproximate= */ false,
+                  /* isCounterexample= */ true));
         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));
+                  + " theories, or loop bounds.",
+              getCounterexampleString(
+                  ctx,
+                  translator.getTypeSystem(),
+                  result.model,
+                  /* isApproximate= */ true,
+                  /* isCounterexample= */ true));
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
-              "Inconclusive: implication holds within the current loop unroll limit, but"
-                  + " may be violated for larger collections.");
+              String.format("Inconclusive: %s holds within the current loop unroll limit, but"
+                  + " may be violated for larger collections.", subjectName.toLowerCase(Locale.US)));
         case NO_MATCH:
           return CelVerificationResult.verified();
         case SOLVER_UNKNOWN:
@@ -345,13 +347,13 @@ private CelVerificationResult checkSatisfiability(
         case EXACT_MATCH:
           return searchForCounterexample
               ? CelVerificationResult.failed(
-                  "Condition is not always true."
-                      + getCounterexampleString(
-                          ctx,
-                          translator.getTypeSystem(),
-                          result.model,
-                          /* isApproximate= */ false,
-                          /* isCounterexample= */ true))
+                  "Condition is not always true.",
+                  getCounterexampleString(
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ false,
+                      /* isCounterexample= */ true))
               : CelVerificationResult.verified(
                   "Condition is satisfiable."
                       + getCounterexampleString(
@@ -369,13 +371,13 @@ private CelVerificationResult checkSatisfiability(
                   : "Inconclusive: a satisfying model may exist, but it depends on"
                       + " approximations, missing theories, or loop bounds.";
           return CelVerificationResult.inconclusive(
-              prefix
-                  + getCounterexampleString(
-                      ctx,
-                      translator.getTypeSystem(),
-                      result.model,
-                      /* isApproximate= */ true,
-                      /* isCounterexample= */ searchForCounterexample));
+              prefix,
+              getCounterexampleString(
+                  ctx,
+                  translator.getTypeSystem(),
+                  result.model,
+                  /* isApproximate= */ true,
+                  /* isCounterexample= */ searchForCounterexample));
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(

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

@@ -526,7 +526,8 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws
         .isEqualTo(VerificationStatus.VIOLATED);
     assertThat(results.get("universal_no_unapproved_privileged_prod").message())
         .isEqualTo(
-            "Implication violation detected. Counterexample input:\n"
+            "Invariant 'universal_no_unapproved_privileged_prod' violation detected."
+                + " Counterexample input:\n"
                 + "  is_owner = false\n"
                 + "  is_privileged = true\n"
                 + "  is_prod = true\n"

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

@@ -2604,7 +2604,7 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th
         CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build();
     CelVerificationResult result =
         ((CelVerifierZ3Impl) verifier)
-            .verifyImplication(assumeAst, assertAst, ImmutableMap.of());
+            .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication");
 
     assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
     assertThat(result.message())