From 71b992f598d4ea845502d7baa01076fd16e8055e Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Thu, 5 Nov 2026 13:34:46 -0800 Subject: [PATCH] Introduce RuntimeOracle to check verifier witnesses PiperOrigin-RevId: 1014956575 --- .../test/java/dev/cel/verifier/BUILD.bazel | 3 + .../cel/verifier/CelVerifierZ3ImplTest.java | 101 +++++------ .../java/dev/cel/verifier/RuntimeOracle.java | 145 +++++++++++++++ .../dev/cel/verifier/RuntimeOracleTest.java | 165 ++++++++++++++++++ 4 files changed, 360 insertions(+), 54 deletions(-) create mode 100644 verifier/src/test/java/dev/cel/verifier/RuntimeOracle.java create mode 100644 verifier/src/test/java/dev/cel/verifier/RuntimeOracleTest.java diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 11477ee45..ed7f9a6c2 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -47,8 +47,11 @@ java_library( "//policy:parser_factory", "//policy:validation_exception", "//policy/testing:k8s_test_tag_handler", + "//runtime", + "//runtime:evaluation_exception", "//testing/protos:single_file_java_proto", "@bazel_tools//tools/java/runfiles", + "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:junit_junit", "@maven//:com_google_testparameterinjector_test_parameter_injector", "//:java_truth", diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 8c84a915a..fc8f55105 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -70,6 +70,7 @@ import java.util.List; import java.util.Optional; import java.util.function.Consumer; +import java.util.function.UnaryOperator; import java.util.stream.IntStream; import org.junit.Before; import org.junit.Test; @@ -86,7 +87,7 @@ public final class CelVerifierZ3ImplTest { .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) .addCompilerLibraries( CelExtensions.bindings(), CelOptionalLibrary.INSTANCE, CelExtensions.comprehensions()) - .addRuntimeLibraries(CelOptionalLibrary.INSTANCE) + .addRuntimeLibraries(CelOptionalLibrary.INSTANCE, CelExtensions.comprehensions()) .addMessageTypes(TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor()) .addVar("x", SimpleType.INT) .addVar("u", SimpleType.UINT) @@ -138,7 +139,16 @@ public final class CelVerifierZ3ImplTest { TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor())) .build(); - private static final CelVerifier VERIFIER = CelVerifierFactory.newVerifier(CEL).build(); + private static final CelVerifier VERIFIER = withRuntimeOracle(CEL, b -> b); + + // For ASTs with functions the runtime can't plan. + private static final CelVerifier VERIFIER_WITHOUT_ORACLE = + CelVerifierFactory.newVerifier(CEL).build(); + + // Builds a verifier whose exact witnesses are checked against the runtime of the same `cel`. + private static CelVerifier withRuntimeOracle(Cel cel, UnaryOperator config) { + return RuntimeOracle.wrap(cel, config.apply(CelVerifierFactory.newVerifier(cel)).build()); + } @Before public void setUp() { @@ -457,8 +467,7 @@ public void isSatisfiable_listAtDisplayLimit_displaysAllElements() throws Except @Test public void isSatisfiable_listPastDisplayLimit_elidesRemainingElements() throws Exception { // Within the unroll limit the whole list is extracted, so the display must still elide it. - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(16).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(16)); CelAbstractSyntaxTree ast = CEL.compile("int_list == [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]").getAst(); @@ -678,10 +687,8 @@ public void isSatisfiable_maskedByBmcNested_inconclusive() throws Exception { CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); CelVerifier customVerifier = - CelVerifierFactory.newVerifier(CEL) - .setComprehensionUnrollLimit(3) - .setTypeProvider(TYPE_PROVIDER) - .build(); + withRuntimeOracle( + CEL, b -> b.setComprehensionUnrollLimit(3).setTypeProvider(TYPE_PROVIDER)); CelVerificationResult result = customVerifier.isSatisfiable(ast); @@ -693,8 +700,7 @@ public void isSatisfiable_comprehensionZeroUnrollLimit_inconclusive() throws Exc String expr = "int_list == [1] ? int_list.exists(x, x == 1) : false"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(0)); CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -1291,8 +1297,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown( throws Exception { CelAbstractSyntaxTree ast = CEL.compile(expression).getAst(); - CelVerifier verifierWithUnknown = - CelVerifierFactory.newVerifier(CEL).addUnknownIdentifier("x").build(); + CelVerifier verifierWithUnknown = withRuntimeOracle(CEL, b -> b.addUnknownIdentifier("x")); // 'x == x' is not a tautology if it can be unknown // i.e: CelUnknown == CelUnknown is unknown. @@ -1308,8 +1313,7 @@ public void isAlwaysTrue_approximateOperandWithUnknown_inconclusive() throws Exc // The truncated `all` may really be false, which absorbs the unknown, so this is always true. CelAbstractSyntaxTree ast = CEL.compile("!(int_list.all(x, x > 0) && unknown_var) || int_list.all(x, x > 0)").getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).addUnknownIdentifier("unknown_var").build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.addUnknownIdentifier("unknown_var")); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -1329,10 +1333,7 @@ public void isAlwaysTrue_dynamicComprehensionNonBoolYieldsError() throws Excepti + " dyn_list.all(x, x.not_a_bool) == false) : true"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); CelVerificationResult result = - CelVerifierFactory.newVerifier(CEL) - .setComprehensionUnrollLimit(1) - .build() - .isAlwaysTrue(ast); + withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(1)).isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()) @@ -1346,8 +1347,7 @@ public void isAlwaysTrue_comprehensionExceedsMaxIterations_returnsUnknown() thro String expr = "int_list == [1, 2, 3] ? int_list.all(x, x > 0) : true"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(2)); CelVerificationResult verifiedValue = verifier.isAlwaysTrue(ast); // Truncated loops return Unknown, which negates to Unknown. @@ -1364,8 +1364,7 @@ public void isAlwaysTrue_comprehensionZeroUnrollLimit_emptyList() throws Excepti String expr = "int_list == [] ? int_list.all(x, x > 0) : true"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(0)); CelVerificationResult verifiedValue = verifier.isAlwaysTrue(ast); assertThat(verifiedValue.status()).isEqualTo(VerificationStatus.VERIFIED); @@ -1395,7 +1394,7 @@ public void isAlwaysTrue_strictCustomFunction_errorPropagates() throws Exception CelAbstractSyntaxTree ast = celWithCustomFunc.compile("custom_func(1 / 0) == 5 || !(custom_func(1 / 0) == 5)").getAst(); - CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isAlwaysTrue(ast); // Should fail verification because the error propagates through custom_func, // so the whole expression evaluates to an error, not true. @@ -1460,11 +1459,12 @@ public void verifyEquivalence_withUnknownIdentifiers_inconclusive( CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL) - .addUnknownIdentifier("a") - .addUnknownIdentifier("x") - .addUnknownIdentifier("unknown_var") - .build(); + withRuntimeOracle( + CEL, + b -> + b.addUnknownIdentifier("a") + .addUnknownIdentifier("x") + .addUnknownIdentifier("unknown_var")); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -1498,7 +1498,7 @@ public void isSatisfiable_approximateIterRangeInMap_inconclusive() throws Except CelAbstractSyntaxTree ast = celWithCustomFunc.compile("approx_list(1).map(x, x * 2) == []").getAst(); - CelVerificationResult result = VERIFIER.isSatisfiable(ast); + CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); } @@ -1518,7 +1518,7 @@ public void isSatisfiable_mapWithUnusedApproximateIteration_verified() throws Ex CelAbstractSyntaxTree ast = celWithCustomFunc.compile("y == [] && y.map(x, approx_func(1)) == y").getAst(); - CelVerificationResult result = VERIFIER.isSatisfiable(ast); + CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } @@ -3035,7 +3035,8 @@ public void isAlwaysTrue_dynamicFunctionShortCircuited_violated() throws Excepti CelOverloadDecl.newGlobalOverload("request_overload", SimpleType.DYN))) .build(); CelAbstractSyntaxTree ast = celCompiler.compile("x != 0 && request() == 1").getAst(); - CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()).contains("x = 0"); @@ -3052,7 +3053,7 @@ public void isAlwaysTrue_boolFunction_verified() throws Exception { CelOverloadDecl.newGlobalOverload("bool_func_overload", SimpleType.BOOL))) .build(); CelAbstractSyntaxTree ast = celCompiler.compile("bool_func() == bool_func()").getAst(); - CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } @@ -3177,7 +3178,7 @@ public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws .addVar("d4", SimpleType.DOUBLE) .build(); CelVerifier timeoutVerifier = - CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); + withRuntimeOracle(customCel, b -> b.setTimeout(Duration.ofMillis(1))); // An overly complex double multiplication to guarantee Z3 FPA theory solver timeouts. CelAbstractSyntaxTree ast = @@ -3602,8 +3603,7 @@ public void isAlwaysTrue_largeListCounterexample_truncatesOutput() throws Except listLiteral.append("]"); CelAbstractSyntaxTree ast = cel.compile("!(large_list == " + listLiteral + ")").getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(cel).setTimeout(Duration.ofSeconds(10)).build(); + CelVerifier verifier = withRuntimeOracle(cel, b -> b.setTimeout(Duration.ofSeconds(10))); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -3627,8 +3627,7 @@ public void isAlwaysTrue_largeMapCounterexample_truncatesOutput() throws Excepti mapLiteral.append("}"); CelAbstractSyntaxTree ast = cel.compile("!(large_map == " + mapLiteral + ")").getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(cel).setTimeout(Duration.ofSeconds(10)).build(); + CelVerifier verifier = withRuntimeOracle(cel, b -> b.setTimeout(Duration.ofSeconds(10))); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -3648,7 +3647,7 @@ public void counterexample_messageTwoFieldsFormatted() throws Exception { CelAbstractSyntaxTree ast = cel.compile("!(msg == TestAllTypes{single_int32: 1, single_int64: 2})").getAst(); - CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + CelVerificationResult result = withRuntimeOracle(cel, b -> b).isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()).contains("single_int32: 1"); @@ -3679,7 +3678,7 @@ public void isAlwaysTrue_customComprehensionWithTrueAccuInit() throws Exception .build(); CelAbstractSyntaxTree ast = cel.compile("dyn_list == [1, 2] ? dyn_list.custom_fold(x) == true : true").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerifier verifier = withRuntimeOracle(cel, b -> b); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -3714,7 +3713,7 @@ public void isAlwaysTrue_customComprehensionWithLoopCondition_inconclusive() thr .build(); CelAbstractSyntaxTree ast = cel.compile("int_list == [1, 2] ? int_list.first_elem() == 2 : true").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerifier verifier = withRuntimeOracle(cel, b -> b); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -3730,8 +3729,7 @@ public void isSatisfiable_maskedByBmcButAlwaysFalse_returnsFailed() throws Excep String expr = "int_list == [1, 2, 3, 4] ? int_list.exists(x, x == 42) && false : false"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(3).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(3)); CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); @@ -3746,8 +3744,7 @@ public void verifyEquivalence_maskedByBmcButAlwaysEqual_returnsVerified() throws CelAbstractSyntaxTree astA = CEL.compile(exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(exprB).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(3).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(3)); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); @@ -3773,8 +3770,7 @@ public void verifyEquivalence_zeroUnrollLimit_returnsInconclusive( @TestParameter EquivalenceZeroUnrollLimitTestCase testCase) throws Exception { CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(0)); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -3812,8 +3808,7 @@ public void verifyEquivalence_zeroUnrollLimit_twoVarComprehensions_returnsVerifi @TestParameter EquivalenceZeroUnrollLimitVerifiedTestCase testCase) throws Exception { CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setComprehensionUnrollLimit(0)); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -3861,8 +3856,7 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive() .build(); CelAbstractSyntaxTree astA = customCel.compile("dyn_list.my_macro_1(true)").getAst(); CelAbstractSyntaxTree astB = customCel.compile("dyn_list.my_macro_2(true)").getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = withRuntimeOracle(customCel, b -> b.setComprehensionUnrollLimit(0)); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -3904,8 +3898,7 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus customCel.compile("cel.bind(x, 10, dyn_list.my_macro(1))").getAst(); CelAbstractSyntaxTree astB = customCel.compile("cel.bind(x, 20, dyn_list.my_macro(1))").getAst(); - CelVerifier verifier = - CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = withRuntimeOracle(customCel, b -> b.setComprehensionUnrollLimit(0)); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -3922,7 +3915,7 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th .addVar("d4", SimpleType.DOUBLE) .build(); CelVerifier timeoutVerifier = - CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); + withRuntimeOracle(customCel, b -> b.setTimeout(Duration.ofMillis(1))); CelAbstractSyntaxTree astA = customCel .compile( @@ -3982,7 +3975,7 @@ public void isAlwaysTrue_constantVarDecl_verified() throws Exception { .setConstant(CelConstant.ofValue(42L)) .build()) .build(); - CelVerifier verifier = CelVerifierFactory.newVerifier(celWithConstVar).build(); + CelVerifier verifier = withRuntimeOracle(celWithConstVar, b -> b); CelAbstractSyntaxTree ast = celWithConstVar .compile("CONST_INT == 42 && [1, 2].all(x, .CONST_INT == 42 && x > 0)") diff --git a/verifier/src/test/java/dev/cel/verifier/RuntimeOracle.java b/verifier/src/test/java/dev/cel/verifier/RuntimeOracle.java new file mode 100644 index 000000000..67d746a6f --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/RuntimeOracle.java @@ -0,0 +1,145 @@ +// 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 static com.google.common.collect.ImmutableList.toImmutableList; +import static java.util.Arrays.stream; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.common.collect.Maps; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.runtime.CelEvaluationException; +import dev.cel.runtime.CelRuntime; +import dev.cel.runtime.CelRuntime.Program; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.util.List; +import java.util.Optional; +import java.util.function.Predicate; + +/** + * Evaluates every exact witness a verifier returns with the CEL runtime, and fails if the runtime + * disagrees with the verdict. + */ +final class RuntimeOracle implements CelVerifier { + + // All errors compare equal, matching the verifier's single error value. + private enum EvaluationError { + ERROR + } + + @SuppressWarnings("Immutable") // CelRuntime is immutable, just not marked as such + private final CelRuntime runtime; + + private final CelVerifier delegate; + + static CelVerifier wrap(CelRuntime runtime, CelVerifier delegate) { + return new RuntimeOracle(runtime, delegate); + } + + @Override + public CelVerificationResult isSatisfiable(CelAbstractSyntaxTree ast) + throws CelVerificationException { + return check( + delegate.isSatisfiable(ast), VerificationStatus.VERIFIED, r -> r.get(0).equals(true), ast); + } + + @Override + public CelVerificationResult isAlwaysTrue(CelAbstractSyntaxTree ast) + throws CelVerificationException { + return check( + delegate.isAlwaysTrue(ast), VerificationStatus.VIOLATED, r -> !r.get(0).equals(true), ast); + } + + @Override + public CelVerificationResult verifyEquivalence( + CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB) throws CelVerificationException { + return check( + delegate.verifyEquivalence(astA, astB), + VerificationStatus.VIOLATED, + r -> !r.get(0).equals(r.get(1)), + astA, + astB); + } + + @CanIgnoreReturnValue + private CelVerificationResult check( + CelVerificationResult result, + VerificationStatus checkedStatus, + Predicate> agrees, + CelAbstractSyntaxTree... asts) { + Optional> inputs = exactInputs(result); + if (result.status() != checkedStatus || !inputs.isPresent()) { + return result; + } + ImmutableList results = + stream(asts).map(ast -> evaluate(ast, inputs.get())).collect(toImmutableList()); + if (agrees.test(results)) { + return result; + } + StringBuilder message = + new StringBuilder("The CEL runtime disagrees with ") + .append(result.status()) + .append(" for inputs ") + .append(inputs.get()) + .append(':'); + for (int i = 0; i < asts.length; i++) { + message + .append("\n ") + .append(asts[i].getSource().getContent()) + .append(" evaluates to ") + .append(results.get(i)); + } + throw new AssertionError(message.append('\n').append(result.message()).toString()); + } + + // The witness's inputs, if every value is exact. + private static Optional> exactInputs(CelVerificationResult result) { + return result + .witness() + .map(CelWitness::variables) + .filter(vars -> vars.values().stream().allMatch(v -> v.value().isPresent())) + .map(vars -> ImmutableMap.copyOf(Maps.transformValues(vars, v -> v.value().get()))); + } + + private Object evaluate(CelAbstractSyntaxTree ast, ImmutableMap inputs) { + Program program; + try { + program = runtime.createProgram(ast); + } catch (CelEvaluationException e) { + throw new AssertionError( + "Can't plan " + + ast.getSource().getContent() + + "; verify it with a verifier for its own environment", + e); + } + try { + return program.eval(inputs); + } catch (CelEvaluationException e) { + // A witness missing a variable would otherwise pass as an error result. + if (e.getMessage().contains("No such attribute(s): ")) { + throw new AssertionError( + "Incomplete witness " + inputs + " for " + ast.getSource().getContent(), e); + } + return EvaluationError.ERROR; + } + } + + private RuntimeOracle(CelRuntime runtime, CelVerifier delegate) { + this.runtime = runtime; + this.delegate = delegate; + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/RuntimeOracleTest.java b/verifier/src/test/java/dev/cel/verifier/RuntimeOracleTest.java new file mode 100644 index 000000000..0bc3a36b9 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/RuntimeOracleTest.java @@ -0,0 +1,165 @@ +// 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 static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; + +import com.google.common.collect.ImmutableMap; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelFunctionDecl; +import dev.cel.common.CelOverloadDecl; +import dev.cel.common.types.SimpleType; +import dev.cel.runtime.CelEvaluationException; +import java.util.Optional; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class RuntimeOracleTest { + + private static final Cel CEL = CelFactory.plannerCelBuilder().addVar("x", SimpleType.INT).build(); + + @Test + public void isSatisfiable_runtimeRefutesSatisfyingInput_throws() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("x == 1").getAst(); + CelVerifier verifier = + checking(CelVerificationResult.verified("Condition is satisfiable.", witness(2L))); + + AssertionError e = assertThrows(AssertionError.class, () -> verifier.isSatisfiable(ast)); + + assertThat(e).hasMessageThat().contains("x == 1 evaluates to false"); + } + + @Test + public void isAlwaysTrue_runtimeRefutesCounterexample_throws() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("x == 1").getAst(); + CelVerifier verifier = checking(CelVerificationResult.failed("Violated.", witness(1L))); + + AssertionError e = assertThrows(AssertionError.class, () -> verifier.isAlwaysTrue(ast)); + + assertThat(e).hasMessageThat().contains("x == 1 evaluates to true"); + } + + @Test + public void verifyEquivalence_runtimeRefutesDivergence_throws() throws Exception { + CelAbstractSyntaxTree astA = CEL.compile("x + 0").getAst(); + CelAbstractSyntaxTree astB = CEL.compile("x").getAst(); + CelVerifier verifier = checking(CelVerificationResult.failed("Violated.", witness(1L))); + + AssertionError e = + assertThrows(AssertionError.class, () -> verifier.verifyEquivalence(astA, astB)); + + assertThat(e).hasMessageThat().contains("x + 0 evaluates to 1"); + assertThat(e).hasMessageThat().contains("\n x evaluates to 1"); + } + + @Test + public void isSatisfiable_inexactSatisfyingInput_notChecked() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("x == 1").getAst(); + CelVerificationResult result = + CelVerificationResult.verified( + "Condition is satisfiable.", + CelWitness.create( + ImmutableMap.of("x", CelWitness.Variable.create(Optional.empty(), "Unknown")))); + + assertThat(checking(result).isSatisfiable(ast)).isSameInstanceAs(result); + } + + @Test + public void verifyEquivalence_bothExpressionsError_throws() throws Exception { + CelAbstractSyntaxTree astA = CEL.compile("1 / x").getAst(); + CelAbstractSyntaxTree astB = CEL.compile("2 / x").getAst(); + CelVerifier verifier = checking(CelVerificationResult.failed("Violated.", witness(0L))); + + AssertionError e = + assertThrows(AssertionError.class, () -> verifier.verifyEquivalence(astA, astB)); + + assertThat(e).hasMessageThat().contains("1 / x evaluates to ERROR"); + assertThat(e).hasMessageThat().contains("2 / x evaluates to ERROR"); + } + + @Test + public void isSatisfiable_inconclusiveResult_notChecked() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("x == 1").getAst(); + CelVerificationResult result = + CelVerificationResult.inconclusive( + "Inconclusive.", witness(2L), /* isCounterexample= */ false); + + assertThat(checking(result).isSatisfiable(ast)).isSameInstanceAs(result); + } + + @Test + public void isSatisfiable_unplannableExpression_throws() throws Exception { + Cel celWithFunction = + CEL.toCelBuilder() + .addFunctionDeclarations( + CelFunctionDecl.newFunctionDeclaration( + "f", + CelOverloadDecl.newGlobalOverload("f_int", SimpleType.BOOL, SimpleType.INT))) + .build(); + CelAbstractSyntaxTree ast = celWithFunction.compile("f(x)").getAst(); + CelVerifier verifier = + checking(CelVerificationResult.verified("Condition is satisfiable.", witness(1L))); + + AssertionError e = assertThrows(AssertionError.class, () -> verifier.isSatisfiable(ast)); + + assertThat(e).hasMessageThat().contains("Can't plan f(x)"); + assertThat(e).hasCauseThat().isInstanceOf(CelEvaluationException.class); + } + + @Test + public void isAlwaysTrue_missingVariableInWitness_throws() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("x == 1").getAst(); + CelVerifier verifier = + checking(CelVerificationResult.failed("Violated.", CelWitness.create(ImmutableMap.of()))); + + AssertionError e = assertThrows(AssertionError.class, () -> verifier.isAlwaysTrue(ast)); + + assertThat(e).hasMessageThat().contains("Incomplete witness {} for x == 1"); + assertThat(e).hasCauseThat().isInstanceOf(CelEvaluationException.class); + } + + private static CelWitness witness(long x) { + return CelWitness.create( + ImmutableMap.of("x", CelWitness.Variable.create(Optional.of(x), Long.toString(x)))); + } + + @SuppressWarnings("Immutable") // Test fake; the result is never mutated. + private static CelVerifier checking(CelVerificationResult result) { + return RuntimeOracle.wrap( + CEL, + new CelVerifier() { + @Override + public CelVerificationResult isSatisfiable(CelAbstractSyntaxTree ast) { + return result; + } + + @Override + public CelVerificationResult isAlwaysTrue(CelAbstractSyntaxTree ast) { + return result; + } + + @Override + public CelVerificationResult verifyEquivalence( + CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB) { + return result; + } + }); + } +}