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",
     ],
 )
 
@@ -112,7 +114,10 @@ java_library(
 
 java_library(
     name = "type_system",
-    srcs = ["CelZ3TypeSystem.java"],
+    srcs = [
+        "CelZ3Exprs.java",
+        "CelZ3TypeSystem.java",
+    ],
     compatible_with = [],
     tags = [
     ],
@@ -157,10 +162,14 @@ java_library(
         "CelAstAlphaHasher.java",
         "CelAstToZ3Translator.java",
         "CelVerifierZ3Impl.java",
+        "CelZ3ComprehensionTranslator.java",
         "CelZ3CounterexampleGenerator.java",
         "CelZ3ExtensionalityAxioms.java",
         "CelZ3FunctionRegistry.java",
         "CelZ3OperatorTranslator.java",
+        "CelZ3StructTranslator.java",
+        "CelZ3TranslationContext.java",
+        "CelZ3TypeConstraintGenerator.java",
         "TranslatedValue.java",
     ],
     compatible_with = [],
@@ -179,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",