diff --git a/.github/workflows/unwanted_deps.sh b/.github/workflows/unwanted_deps.sh index c483f9730..a74ee003d 100755 --- a/.github/workflows/unwanted_deps.sh +++ b/.github/workflows/unwanted_deps.sh @@ -46,4 +46,8 @@ checkUnwantedDeps '//publish:cel' '@maven_android//:com_google_protobuf_protobuf # cel_runtime_android shouldn't depend on the full protobuf runtime or antlr checkUnwantedDeps '//publish:cel_runtime_android' '@maven//:com_google_protobuf_protobuf_java' checkUnwantedDeps '//publish:cel_runtime_android' '@maven//:org_antlr_antlr4_runtime' + +# cel shouldn't depend on the verifier +checkUnwantedDeps '//publish:cel' '//verifier/' + exit 0 diff --git a/publish/BUILD.bazel b/publish/BUILD.bazel index 185c7fb7d..69766290e 100644 --- a/publish/BUILD.bazel +++ b/publish/BUILD.bazel @@ -1,5 +1,5 @@ load("@bazel_common//tools/maven:pom_file.bzl", "pom_file") -load("@rules_jvm_external//:defs.bzl", "java_export") +load("@rules_jvm_external//:defs.bzl", "java_export", "maven_export") load("//publish:cel_version.bzl", "CEL_VERSION") # Note: These targets must reference the build targets in `src` directly in @@ -349,3 +349,22 @@ java_export( pom_template = ":cel_verifier_pom", exports = VERIFIER_TARGETS + [":cel"], ) + +pom_file( + name = "cel_verifier_cli_pom", + substitutions = { + "CEL_VERSION": CEL_VERSION, + "CEL_ARTIFACT_ID": "verifier-cli", + "PACKAGE_NAME": "CEL Java Verifier CLI", + "PACKAGE_DESC": "Formal verification CLI and REPL tool for Common Expression Language for Java.", + }, + targets = [], + template_file = "pom_template.xml", +) + +maven_export( + name = "cel_verifier_cli", + maven_coordinates = "dev.cel:verifier-cli:%s" % CEL_VERSION, + pom_template = ":cel_verifier_cli_pom", + target = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool_deploy.jar", +) diff --git a/publish/publish.sh b/publish/publish.sh index 28d0f0f53..d83016de3 100755 --- a/publish/publish.sh +++ b/publish/publish.sh @@ -26,7 +26,7 @@ # Note, to run script: Bazel and jq are required -ALL_TARGETS=("//publish:cel_common.publish" "//publish:cel.publish" "//publish:cel_compiler.publish" "//publish:cel_runtime.publish" "//publish:cel_v1alpha1.publish" "//publish:cel_protobuf.publish" "//publish:cel_runtime_android.publish") +ALL_TARGETS=("//publish:cel_common.publish" "//publish:cel.publish" "//publish:cel_compiler.publish" "//publish:cel_runtime.publish" "//publish:cel_v1alpha1.publish" "//publish:cel_protobuf.publish" "//publish:cel_runtime_android.publish" "//publish:cel_verifier.publish" "//publish:cel_verifier_cli.publish") JDK8_FLAGS="--java_language_version=8 --java_runtime_version=8" function publish_maven_remote() { diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index 9ec441ed4..ef1316ca2 100644 --- a/verifier/BUILD.bazel +++ b/verifier/BUILD.bazel @@ -61,3 +61,10 @@ java_library( visibility = [":verifier_internal"], exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"], ) + +java_library( + name = "canonicalization_optimizer", + compatible_with = [], + visibility = [":verifier_internal"], + exports = ["//verifier/src/main/java/dev/cel/verifier:canonicalization_optimizer"], +) diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index ab341fba2..a0de7948a 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -35,6 +35,12 @@ java_library( deps = [ ":verifier", ":z3_impl", + "//bundle:cel", + "//checker:checker_builder", + "//compiler", + "//compiler:compiler_builder", + "//parser:parser_builder", + "//runtime", ], ) @@ -119,6 +125,29 @@ java_library( ], ) +java_library( + name = "canonicalization_optimizer", + srcs = ["CanonicalizationOptimizer.java"], + tags = [ + ], + deps = [ + "//:auto_value", + "//bundle:cel", + "//common:cel_ast", + "//common:mutable_ast", + "//common:mutable_source", + "//common:operator", + "//common/ast", + "//common/ast:mutable_expr", + "//common/navigation:common", + "//common/navigation:mutable_navigation", + "//common/values:cel_byte_string", + "//optimizer:ast_optimizer", + "//optimizer:mutable_ast", + "@maven//:com_google_guava_guava", + ], +) + java_library( name = "z3_impl", srcs = [ @@ -135,10 +164,12 @@ java_library( tags = [ ], deps = [ + ":canonicalization_optimizer", ":numeric_bounds", ":type_system", ":verifier", "//:auto_value", + "//bundle:cel", "//common:cel_ast", "//common:compiler_common", "//common:operator", @@ -147,6 +178,9 @@ java_library( "//common/types", "//common/types:cel_types", "//common/types:type_providers", + "//optimizer", + "//optimizer:optimization_exception", + "//optimizer:optimizer_builder", "//verifier/axioms", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", diff --git a/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java new file mode 100644 index 000000000..990711263 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java @@ -0,0 +1,672 @@ +// 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 com.google.auto.value.AutoValue; +import com.google.common.collect.ComparisonChain; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.Iterables; +import dev.cel.bundle.Cel; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelMutableAst; +import dev.cel.common.CelMutableSource; +import dev.cel.common.Operator; +import dev.cel.common.ast.CelConstant; +import dev.cel.common.ast.CelExpr.ExprKind.Kind; +import dev.cel.common.ast.CelMutableExpr; +import dev.cel.common.ast.CelMutableExpr.CelMutableCall; +import dev.cel.common.ast.CelMutableExpr.CelMutableComprehension; +import dev.cel.common.ast.CelMutableExpr.CelMutableMap; +import dev.cel.common.ast.CelMutableExpr.CelMutableSelect; +import dev.cel.common.ast.CelMutableExpr.CelMutableStruct; +import dev.cel.common.navigation.CelNavigableMutableAst; +import dev.cel.common.navigation.CelNavigableMutableExpr; +import dev.cel.common.navigation.TraversalOrder; +import dev.cel.common.values.CelByteString; +import dev.cel.optimizer.AstMutator; +import dev.cel.optimizer.CelAstOptimizer; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Optional; + +/** + * Standalone AST canonicalization pass that normalizes commutative operator ordering and De Morgan + * quantifier/logical identities. + * + *

This optimizer performs: + * + *

+ * + *

Caveat: This is a structural normalizer intended for comparison purposes (such as + * formal equivalence verification) and as a pre-processor for helping other optimizers (such as + * Common Subexpression Elimination). It is not a runtime cost optimizer; lexicographical ordering + * of calls or Negation Normal Form expansions are not designed to optimize runtime execution or + * short-circuit latency. + */ +final class CanonicalizationOptimizer implements CelAstOptimizer { + + private final CanonicalizationOptions canonicalizationOptions; + + private static final Comparator EXPR_COMPARATOR = + new Comparator() { + @Override + public int compare(CelMutableExpr e1, CelMutableExpr e2) { + int kindCmp = + Integer.compare(getKindPriority(e1.getKind()), getKindPriority(e2.getKind())); + if (kindCmp != 0) { + return kindCmp; + } + switch (e1.getKind()) { + case CONSTANT: + return compareConstants(e1.constant(), e2.constant()); + case IDENT: + return e1.ident().name().compareTo(e2.ident().name()); + case SELECT: + return compareSelect(e1.select(), e2.select()); + case CALL: + return compareCall(e1.call(), e2.call()); + case LIST: + return compareList(e1.list().elements(), e2.list().elements()); + case MAP: + return compareMap(e1.map(), e2.map()); + case STRUCT: + return compareStruct(e1.struct(), e2.struct()); + case COMPREHENSION: + return compareComprehension(e1.comprehension(), e2.comprehension()); + case NOT_SET: + return 0; + default: + throw new UnsupportedOperationException( + "Unsupported expression kind: " + e1.getKind()); + } + } + + private int compareConstants(CelConstant c1, CelConstant c2) { + int constKindCmp = c1.getKind().name().compareTo(c2.getKind().name()); + if (constKindCmp != 0) { + return constKindCmp; + } + switch (c1.getKind()) { + case NULL_VALUE: + case NOT_SET: + return 0; + case BOOLEAN_VALUE: + return Boolean.compare(c1.booleanValue(), c2.booleanValue()); + case INT64_VALUE: + return Long.compare(c1.int64Value(), c2.int64Value()); + case UINT64_VALUE: + return c1.uint64Value().compareTo(c2.uint64Value()); + case DOUBLE_VALUE: + return Double.compare(c1.doubleValue(), c2.doubleValue()); + case STRING_VALUE: + return c1.stringValue().compareTo(c2.stringValue()); + case BYTES_VALUE: + return CelByteString.unsignedLexicographicalComparator() + .compare(c1.bytesValue(), c2.bytesValue()); + default: + throw new UnsupportedOperationException("Unsupported constant kind: " + c1.getKind()); + } + } + + private int compareSelect(CelMutableSelect s1, CelMutableSelect s2) { + return ComparisonChain.start() + .compare(s1.operand(), s2.operand(), this) + .compare(s1.field(), s2.field()) + .compareFalseFirst(s1.testOnly(), s2.testOnly()) + .result(); + } + + private int compareCall(CelMutableCall c1, CelMutableCall c2) { + int fnCmp = c1.function().compareTo(c2.function()); + if (fnCmp != 0) { + return fnCmp; + } + boolean hasT1 = c1.target().isPresent(); + boolean hasT2 = c2.target().isPresent(); + if (hasT1 != hasT2) { + return Boolean.compare(hasT1, hasT2); + } + if (hasT1) { + int tCmp = compare(c1.target().get(), c2.target().get()); + if (tCmp != 0) { + return tCmp; + } + } + return compareList(c1.args(), c2.args()); + } + + private int compareMap(CelMutableMap m1, CelMutableMap m2) { + int mapSizeCmp = Integer.compare(m1.entries().size(), m2.entries().size()); + if (mapSizeCmp != 0) { + return mapSizeCmp; + } + Iterator it2 = m2.entries().iterator(); + for (CelMutableMap.Entry entry1 : m1.entries()) { + CelMutableMap.Entry entry2 = it2.next(); + int cmp = + ComparisonChain.start() + .compare(entry1.key(), entry2.key(), this) + .compare(entry1.value(), entry2.value(), this) + .result(); + if (cmp != 0) { + return cmp; + } + } + return 0; + } + + private int compareStruct(CelMutableStruct s1, CelMutableStruct s2) { + int msgCmp = s1.messageName().compareTo(s2.messageName()); + if (msgCmp != 0) { + return msgCmp; + } + int structSizeCmp = Integer.compare(s1.entries().size(), s2.entries().size()); + if (structSizeCmp != 0) { + return structSizeCmp; + } + Iterator it2 = s2.entries().iterator(); + for (CelMutableStruct.Entry entry1 : s1.entries()) { + CelMutableStruct.Entry entry2 = it2.next(); + int cmp = + ComparisonChain.start() + .compare(entry1.fieldKey(), entry2.fieldKey()) + .compare(entry1.value(), entry2.value(), this) + .result(); + if (cmp != 0) { + return cmp; + } + } + return 0; + } + + private int compareComprehension(CelMutableComprehension c1, CelMutableComprehension c2) { + return ComparisonChain.start() + .compare(c1.iterVar(), c2.iterVar()) + .compare(c1.iterVar2(), c2.iterVar2()) + .compare(c1.accuVar(), c2.accuVar()) + .compare(c1.iterRange(), c2.iterRange(), this) + .compare(c1.accuInit(), c2.accuInit(), this) + .compare(c1.loopCondition(), c2.loopCondition(), this) + .compare(c1.loopStep(), c2.loopStep(), this) + .compare(c1.result(), c2.result(), this) + .result(); + } + + private int compareList(List l1, List l2) { + int sizeCmp = Integer.compare(l1.size(), l2.size()); + if (sizeCmp != 0) { + return sizeCmp; + } + Iterator it2 = l2.iterator(); + for (CelMutableExpr elem1 : l1) { + int cmp = compare(elem1, it2.next()); + if (cmp != 0) { + return cmp; + } + } + return 0; + } + + private int getKindPriority(Kind kind) { + switch (kind) { + case IDENT: + return 1; + case SELECT: + return 2; + case CALL: + return 3; + case LIST: + return 4; + case MAP: + return 5; + case STRUCT: + return 6; + case COMPREHENSION: + return 7; + case CONSTANT: + return 8; + default: + return 99; + } + } + }; + + /** + * Returns a new instance of canonicalization optimizer configured with the provided {@link + * CanonicalizationOptions}. + */ + static CanonicalizationOptimizer newInstance(CanonicalizationOptions canonicalizationOptions) { + return new CanonicalizationOptimizer(canonicalizationOptions); + } + + @Override + public OptimizationResult optimize(CelAbstractSyntaxTree ast, Cel cel) { + CelMutableAst mutableAst = CelMutableAst.fromCelAst(ast); + mutableAst = runCanonicalizationLoop(mutableAst); + for (Map.Entry entry : + new HashMap<>(mutableAst.source().getMacroCalls()).entrySet()) { + CelMutableExpr canonicalMacro = canonicalize(entry.getValue()); + mutableAst.source().addMacroCalls(entry.getKey(), canonicalMacro); + } + CelAbstractSyntaxTree optimizedAst = + AstMutator.newInstance(canonicalizationOptions.maxIterationLimit()) + .renumberIdsConsecutively(mutableAst) + .toParsedAst(); + return OptimizationResult.create(optimizedAst); + } + + /** Canonicalizes a single CelMutableExpr subtree. */ + private CelMutableExpr canonicalize(CelMutableExpr root) { + CelMutableAst mutableAst = CelMutableAst.of(root, CelMutableSource.newInstance()); + mutableAst = runCanonicalizationLoop(mutableAst); + return mutableAst.expr(); + } + + private CelMutableAst runCanonicalizationLoop(CelMutableAst mutableAst) { + AstMutator astMutator = AstMutator.newInstance(canonicalizationOptions.maxIterationLimit()); + int iterCount = 0; + boolean continueCanonicalizing = true; + while (continueCanonicalizing) { + if (iterCount >= canonicalizationOptions.maxIterationLimit()) { + throw new IllegalStateException( + "Max iteration count reached in CanonicalizationOptimizer."); + } + iterCount++; + continueCanonicalizing = false; + ImmutableList candidateExprs = + CelNavigableMutableAst.fromAst(mutableAst) + .getRoot() + .allNodes(TraversalOrder.POST_ORDER) + .filter(CanonicalizationOptimizer::canCanonicalize) + .collect(toImmutableList()); + for (CelNavigableMutableExpr candidate : candidateExprs) { + iterCount++; + Optional newExpr = maybeCanonicalize(mutableAst, candidate); + if (newExpr.isPresent()) { + continueCanonicalizing = true; + mutableAst = astMutator.replaceSubtree(mutableAst, newExpr.get(), candidate.id()); + break; + } + } + } + return mutableAst; + } + + private static boolean canCanonicalize(CelNavigableMutableExpr navigable) { + CelMutableExpr expr = navigable.expr(); + return isCallWithArgCount(expr, Operator.LOGICAL_AND.getFunction(), 2) + || isCallWithArgCount(expr, Operator.LOGICAL_OR.getFunction(), 2) + || isCallWithArgCount(expr, Operator.EQUALS.getFunction(), 2) + || isCallWithArgCount(expr, Operator.NOT_EQUALS.getFunction(), 2) + || isCallWithArgCount(expr, Operator.LOGICAL_NOT.getFunction(), 1); + } + + private static boolean isComprehensionAccuVar(CelNavigableMutableExpr expr) { + return expr.allNodes() + .filter(node -> node.getKind().equals(Kind.IDENT)) + .anyMatch( + identNode -> { + String identName = identNode.expr().ident().name(); + CelNavigableMutableExpr curr = identNode; + Optional maybeParent = curr.parent(); + while (maybeParent.isPresent()) { + CelNavigableMutableExpr parent = maybeParent.get(); + if (parent.getKind().equals(Kind.COMPREHENSION)) { + CelMutableComprehension compre = parent.expr().comprehension(); + if (compre.accuVar().equals(identName) + && curr.id() != compre.iterRange().id() + && curr.id() != compre.accuInit().id()) { + return true; + } + } + curr = parent; + maybeParent = parent.parent(); + } + return false; + }); + } + + private static Optional maybeCanonicalize( + CelMutableAst mutableAst, CelNavigableMutableExpr navigableExpr) { + CelMutableExpr expr = navigableExpr.expr(); + if (expr.getKind() != Kind.CALL) { + return Optional.empty(); + } + CelMutableCall call = expr.call(); + String functionName = call.function(); + List args = call.args(); + + if ((functionName.equals(Operator.LOGICAL_AND.getFunction()) + || functionName.equals(Operator.LOGICAL_OR.getFunction())) + && args.size() == 2) { + List navigableOperands = + flattenNavigableOperands(navigableExpr, functionName); + if (navigableOperands.stream().anyMatch(CanonicalizationOptimizer::isComprehensionAccuVar)) { + return Optional.empty(); + } + List operands = new ArrayList<>(); + for (CelNavigableMutableExpr navOp : navigableOperands) { + operands.add(navOp.expr()); + } + operands.sort(EXPR_COMPARATOR); + List uniqueSorted = new ArrayList<>(); + for (CelMutableExpr op : operands) { + if (uniqueSorted.isEmpty() + || EXPR_COMPARATOR.compare(op, Iterables.getLast(uniqueSorted)) != 0) { + uniqueSorted.add(op); + } + } + CelMutableExpr rebuilt = uniqueSorted.get(0); + for (int i = 1; i < uniqueSorted.size(); i++) { + rebuilt = + CelMutableExpr.ofCall( + expr.id(), CelMutableCall.create(functionName, rebuilt, uniqueSorted.get(i))); + } + if (EXPR_COMPARATOR.compare(rebuilt, expr) == 0) { + return Optional.empty(); + } + return Optional.of(rebuilt); + } + + if ((functionName.equals(Operator.EQUALS.getFunction()) + || functionName.equals(Operator.NOT_EQUALS.getFunction())) + && args.size() == 2) { + CelMutableExpr arg0 = args.get(0); + CelMutableExpr arg1 = args.get(1); + if (EXPR_COMPARATOR.compare(arg0, arg1) > 0) { + return Optional.of( + CelMutableExpr.ofCall(expr.id(), CelMutableCall.create(functionName, arg1, arg0))); + } + return Optional.empty(); + } + + if (functionName.equals(Operator.LOGICAL_NOT.getFunction()) && args.size() == 1) { + CelMutableExpr target = args.get(0); + if (isCallWithArgCount(target, Operator.LOGICAL_NOT.getFunction(), 1)) { + return Optional.of(target.call().args().get(0)); + } + if (isCallWithArgCount(target, Operator.LOGICAL_AND.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.LOGICAL_OR.getFunction(), + negate(subArgs.get(0)), + negate(subArgs.get(1))))); + } + if (isCallWithArgCount(target, Operator.LOGICAL_OR.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.LOGICAL_AND.getFunction(), + negate(subArgs.get(0)), + negate(subArgs.get(1))))); + } + if (isCallWithArgCount(target, Operator.EQUALS.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.NOT_EQUALS.getFunction(), subArgs.get(0), subArgs.get(1)))); + } + if (isCallWithArgCount(target, Operator.NOT_EQUALS.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.EQUALS.getFunction(), subArgs.get(0), subArgs.get(1)))); + } + if (target.getKind() == Kind.COMPREHENSION) { + CelMutableComprehension comp = target.comprehension(); + if (isExistsMacro(mutableAst, target.id(), comp)) { + return negateComprehension(mutableAst, target.id(), comp, true); + } else if (isAllMacro(mutableAst, target.id(), comp)) { + return negateComprehension(mutableAst, target.id(), comp, false); + } + } + } + + return Optional.empty(); + } + + private static Optional negateComprehension( + CelMutableAst mutableAst, long compId, CelMutableComprehension comp, boolean isExists) { + CelMutableCall stepCall = comp.loopStep().call(); + CelMutableExpr predicate = getPredicateFromLoopStep(stepCall); + CelMutableExpr newLoopStep = + CelMutableExpr.ofCall( + comp.loopStep().id(), + CelMutableCall.create( + (isExists ? Operator.LOGICAL_AND : Operator.LOGICAL_OR).getFunction(), + CelMutableExpr.ofIdent(comp.accuVar()), + negate(predicate))); + CelMutableExpr newAccuInit = CelMutableExpr.ofConstant(CelConstant.ofValue(isExists)); + CelMutableExpr newLoopCondition = + CelMutableExpr.ofCall( + comp.loopCondition().id(), + CelMutableCall.create( + Operator.NOT_STRICTLY_FALSE.getFunction(), + isExists + ? CelMutableExpr.ofIdent(comp.accuVar()) + : negate(CelMutableExpr.ofIdent(comp.accuVar())))); + CelMutableComprehension newComp = + CelMutableComprehension.create( + comp.iterVar(), + comp.iterVar2(), + comp.iterRange(), + comp.accuVar(), + newAccuInit, + newLoopCondition, + newLoopStep, + comp.result()); + updateMacroCallForQuantifier( + mutableAst, compId, (isExists ? Operator.ALL : Operator.EXISTS).getFunction()); + return Optional.of(CelMutableExpr.ofComprehension(compId, newComp)); + } + + private static CelMutableExpr negate(CelMutableExpr expr) { + return CelMutableExpr.ofCall( + expr.id(), CelMutableCall.create(Operator.LOGICAL_NOT.getFunction(), expr)); + } + + private static void updateMacroCallForQuantifier( + CelMutableAst mutableAst, long compId, String newFunctionName) { + if (!mutableAst.source().getMacroCalls().containsKey(compId)) { + return; + } + CelMutableExpr macroCall = mutableAst.source().getMacroCalls().get(compId); + if (macroCall.getKind() != Kind.CALL) { + throw new IllegalStateException( + "Expected macro call to be of kind CALL, but got: " + macroCall.getKind()); + } + CelMutableCall call = macroCall.call(); + if (call.args().size() < 2) { + throw new IllegalStateException( + "Expected macro call to have at least 2 arguments, but got: " + call.args().size()); + } + CelMutableExpr predicateArg = Iterables.getLast(call.args()); + CelMutableExpr notPredicate; + if (isCallWithArgCount(predicateArg, Operator.LOGICAL_NOT.getFunction(), 1)) { + notPredicate = predicateArg.call().args().get(0); + } else { + notPredicate = + CelMutableExpr.ofCall( + 0, CelMutableCall.create(Operator.LOGICAL_NOT.getFunction(), predicateArg)); + } + List newArgs = new ArrayList<>(call.args()); + newArgs.set(newArgs.size() - 1, notPredicate); + CelMutableCall newCall = + call.target().isPresent() + ? CelMutableCall.create(call.target().get(), newFunctionName, newArgs) + : CelMutableCall.create(newFunctionName, newArgs); + mutableAst.source().addMacroCalls(compId, CelMutableExpr.ofCall(macroCall.id(), newCall)); + } + + private static List flattenNavigableOperands( + CelNavigableMutableExpr expr, String functionName) { + List result = new ArrayList<>(); + flattenNavigableOperandsRec(expr, functionName, result); + return result; + } + + private static void flattenNavigableOperandsRec( + CelNavigableMutableExpr expr, String functionName, List result) { + if (expr.getKind() == Kind.CALL + && expr.expr().call().function().equals(functionName) + && expr.expr().call().args().size() == 2) { + ImmutableList children = expr.children().collect(toImmutableList()); + if (children.size() == 2) { + flattenNavigableOperandsRec(children.get(0), functionName, result); + flattenNavigableOperandsRec(children.get(1), functionName, result); + return; + } + } + result.add(expr); + } + + private static CelMutableExpr getPredicateFromLoopStep(CelMutableCall stepCall) { + return stepCall.args().get(1); + } + + private static boolean isExistsMacro( + CelMutableAst mutableAst, long compId, CelMutableComprehension comp) { + return isStandardMacroCall(mutableAst, compId, Operator.EXISTS.getFunction()) + && isBooleanAccuInit(comp, false) + && isNotStrictlyFalseLoopCondition(comp, true) + && isLoopStepWithAccuVar(comp, Operator.LOGICAL_OR.getFunction()); + } + + private static boolean isAllMacro( + CelMutableAst mutableAst, long compId, CelMutableComprehension comp) { + return isStandardMacroCall(mutableAst, compId, Operator.ALL.getFunction()) + && isBooleanAccuInit(comp, true) + && isNotStrictlyFalseLoopCondition(comp, false) + && isLoopStepWithAccuVar(comp, Operator.LOGICAL_AND.getFunction()); + } + + private static boolean isStandardMacroCall( + CelMutableAst mutableAst, long compId, String expectedMacroFunction) { + if (!mutableAst.source().getMacroCalls().containsKey(compId)) { + return true; + } + CelMutableExpr macroCall = mutableAst.source().getMacroCalls().get(compId); + return macroCall.getKind() == Kind.CALL + && macroCall.call().function().equals(expectedMacroFunction); + } + + private static boolean isBooleanAccuInit(CelMutableComprehension comp, boolean expectedValue) { + return comp.accuInit().getKind() == Kind.CONSTANT + && comp.accuInit().constant().getKind() == CelConstant.Kind.BOOLEAN_VALUE + && comp.accuInit().constant().booleanValue() == expectedValue; + } + + private static boolean isNotStrictlyFalseLoopCondition( + CelMutableComprehension comp, boolean expectNot) { + if (comp.loopCondition().getKind() != Kind.CALL) { + throw new IllegalStateException( + "Expected comprehension loopCondition to be a CALL, but got: " + + comp.loopCondition().getKind()); + } + CelMutableCall call = comp.loopCondition().call(); + if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction()) + && !call.function().equals(Operator.OLD_NOT_STRICTLY_FALSE.getFunction())) { + throw new IllegalStateException( + "Expected comprehension loopCondition to be @not_strictly_false, but got: " + + call.function()); + } + if (call.args().size() != 1) { + throw new IllegalStateException( + "Expected @not_strictly_false to have exactly 1 argument, but got: " + + call.args().size()); + } + CelMutableExpr arg = call.args().get(0); + if (expectNot) { + if (!isCallWithArgCount(arg, Operator.LOGICAL_NOT.getFunction(), 1)) { + return false; + } + arg = arg.call().args().get(0); + } + return isIdent(arg, comp.accuVar()); + } + + private static boolean isLoopStepWithAccuVar( + CelMutableComprehension comp, String expectedFunction) { + if (!isCallWithArgCount(comp.loopStep(), expectedFunction, 2)) { + return false; + } + List args = comp.loopStep().call().args(); + return isIdent(args.get(0), comp.accuVar()) || isIdent(args.get(1), comp.accuVar()); + } + + private static boolean isIdent(CelMutableExpr expr, String name) { + return expr.getKind() == Kind.IDENT && expr.ident().name().equals(name); + } + + private static boolean isCallWithArgCount( + CelMutableExpr expr, String functionName, int argCount) { + return expr.getKind() == Kind.CALL + && expr.call().function().equals(functionName) + && expr.call().args().size() == argCount; + } + + /** Options to configure how Canonicalization behaves. */ + @AutoValue + abstract static class CanonicalizationOptions { + abstract int maxIterationLimit(); + + /** Builder for configuring the {@link CanonicalizationOptions}. */ + @AutoValue.Builder + abstract static class Builder { + + /** + * Limit the number of iterations while performing canonicalization. An exception is thrown if + * the iteration count exceeds the set value. + */ + abstract Builder maxIterationLimit(int value); + + abstract CanonicalizationOptions build(); + + Builder() {} + } + + /** Returns a new options builder with recommended defaults pre-configured. */ + static Builder newBuilder() { + return new AutoValue_CanonicalizationOptimizer_CanonicalizationOptions.Builder() + .maxIterationLimit(500); + } + + CanonicalizationOptions() {} + } + + private CanonicalizationOptimizer(CanonicalizationOptions canonicalizationOptions) { + this.canonicalizationOptions = canonicalizationOptions; + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java index da48ec484..d761428d6 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java @@ -14,14 +14,43 @@ package dev.cel.verifier; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; +import dev.cel.checker.CelChecker; +import dev.cel.compiler.CelCompiler; +import dev.cel.compiler.CelCompilerFactory; +import dev.cel.parser.CelParser; +import dev.cel.runtime.CelRuntime; /** Factory class for producing AST verifiers using Z3. */ public final class CelVerifierFactory { - /** Create a builder for configuring a {@link CelVerifier}. */ + /** + * Create a builder for configuring a {@link CelVerifier}. + * + * @deprecated Prefer passing a {@link Cel} environment using {@link #newVerifier(Cel)} to enable + * canonicalization and expression re-typechecking during verification. + */ + @Deprecated public static CelVerifierBuilder newVerifier() { return CelVerifierZ3Impl.newBuilder(); } + /** Create a builder for configuring a {@link CelVerifier} with a CEL environment. */ + public static CelVerifierBuilder newVerifier(Cel cel) { + return CelVerifierZ3Impl.newBuilder(cel); + } + + /** Create a builder for configuring a {@link CelVerifier} with a CEL environment. */ + public static CelVerifierBuilder newVerifier(CelCompiler celCompiler, CelRuntime celRuntime) { + return newVerifier(CelFactory.combine(celCompiler, celRuntime)); + } + + /** Create a builder for configuring a {@link CelVerifier} with a CEL environment. */ + public static CelVerifierBuilder newVerifier( + CelParser celParser, CelChecker celChecker, CelRuntime celRuntime) { + return newVerifier(CelCompilerFactory.combine(celParser, celChecker), celRuntime); + } + private CelVerifierFactory() {} } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 90d7238c2..62b104afa 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -27,9 +27,14 @@ import com.microsoft.z3.Params; import com.microsoft.z3.Solver; import com.microsoft.z3.Status; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.types.CelType; import dev.cel.common.types.CelTypeProvider; +import dev.cel.optimizer.CelOptimizationException; +import dev.cel.optimizer.CelOptimizer; +import dev.cel.optimizer.CelOptimizerFactory; import dev.cel.verifier.axioms.CelZ3FunctionAxiom; import dev.cel.verifier.axioms.CelZ3StandardAxioms; import java.time.Duration; @@ -59,14 +64,25 @@ public Optional findType(String typeName) { } }; + private static final CanonicalizationOptimizer CANONICALIZATION_OPTIMIZER = + CanonicalizationOptimizer.newInstance( + CanonicalizationOptimizer.CanonicalizationOptions.newBuilder().build()); + private final Duration timeout; private final int comprehensionUnrollLimit; private final ImmutableSet unknownIdentifiers; private final CelZ3FunctionRegistry functionRegistry; private final CelTypeProvider typeProvider; + @SuppressWarnings("Immutable") // Cel environment is immutable, just not marked as such + private final Cel cel; + static Builder newBuilder() { - return new Builder(); + return new Builder(CelFactory.plannerCelBuilder().build()); + } + + static Builder newBuilder(Cel cel) { + return new Builder(Preconditions.checkNotNull(cel)); } static final class Builder implements CelVerifierBuilder { @@ -74,14 +90,16 @@ static final class Builder implements CelVerifierBuilder { private int comprehensionUnrollLimit; private final ImmutableSet.Builder unknownIdentifiers; private final ImmutableList.Builder functionAxioms; + private final Cel cel; private CelTypeProvider typeProvider; - private Builder() { + private Builder(Cel cel) { this.timeout = Duration.ofSeconds(10); this.comprehensionUnrollLimit = 5; this.unknownIdentifiers = ImmutableSet.builder(); this.functionAxioms = ImmutableList.builder(); this.typeProvider = EMPTY_TYPE_PROVIDER; + this.cel = cel; } @Override @@ -137,7 +155,12 @@ public CelVerifier build() { CelZ3FunctionRegistry registry = CelZ3FunctionRegistry.create(allFunctionAxioms); return new CelVerifierZ3Impl( - timeout, comprehensionUnrollLimit, unknownIdentifiers.build(), registry, typeProvider); + timeout, + comprehensionUnrollLimit, + unknownIdentifiers.build(), + registry, + typeProvider, + cel); } } @@ -160,6 +183,18 @@ public CelVerificationResult verifyEquivalence( CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB) throws CelVerificationException { Preconditions.checkArgument(astA.isChecked(), "astA must be type-checked."); Preconditions.checkArgument(astB.isChecked(), "astB must be type-checked."); + CelOptimizer optimizer = + CelOptimizerFactory.standardCelOptimizerBuilder(cel) + .addAstOptimizers( + CanonicalizationOptimizer.newInstance( + CanonicalizationOptimizer.CanonicalizationOptions.newBuilder().build())) + .build(); + try { + astA = optimizer.optimize(astA); + astB = optimizer.optimize(astB); + } catch (CelOptimizationException e) { + // Fall back to original ASTs if canonicalization or re-typechecking fails + } try (Context ctx = new Context(ImmutableMap.of("model", "true"))) { CelAstToZ3Translator translator = new CelAstToZ3Translator( @@ -487,12 +522,14 @@ private static String getCounterexampleString( int comprehensionUnrollLimit, ImmutableSet unknownIdentifiers, CelZ3FunctionRegistry functionRegistry, - CelTypeProvider typeProvider) { + CelTypeProvider typeProvider, + Cel cel) { this.timeout = timeout; this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.unknownIdentifiers = unknownIdentifiers; this.functionRegistry = functionRegistry; this.typeProvider = typeProvider; + this.cel = cel; } private enum SolverOutcome { diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel index 28ce776cb..1d2c7569e 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -6,6 +6,7 @@ package( "//:license", ], default_visibility = [ + "//publish:__pkg__", "//verifier:__subpackages__", ], ) diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java index 89e842fb1..51b7164e4 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -50,7 +50,7 @@ static CelVerificationResult checkSatisfiable( throws Exception { CelCompiler compiler = buildCompiler(variables); CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); - CelVerifier verifier = buildVerifier(options); + CelVerifier verifier = buildVerifier(variables, options); return verifier.isSatisfiable(ast); } @@ -60,7 +60,7 @@ static CelVerificationResult checkValid( throws Exception { CelCompiler compiler = buildCompiler(variables); CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); - CelVerifier verifier = buildVerifier(options); + CelVerifier verifier = buildVerifier(variables, options); return verifier.isAlwaysTrue(ast); } @@ -74,7 +74,7 @@ static CelVerificationResult verifyEquivalence( CelCompiler compiler = buildCompiler(variables); CelAbstractSyntaxTree astA = compiler.compile(expressionA).getAst(); CelAbstractSyntaxTree astB = compiler.compile(expressionB).getAst(); - CelVerifier verifier = buildVerifier(options); + CelVerifier verifier = buildVerifier(variables, options); return verifier.verifyEquivalence(astA, astB); } @@ -125,20 +125,7 @@ static CelCompiler buildCompiler(Map variables) { return builder.build(); } - static CelVerifier buildVerifier(VerificationOptions options) { - CelVerifierBuilder builder = - CelVerifierFactory.newVerifier() - .setTimeout(options.getTimeout()) - .setComprehensionUnrollLimit(options.getComprehensionUnrollLimit()); - - for (String unknown : options.getUnknownIdentifiers()) { - builder.addUnknownIdentifier(unknown); - } - return builder.build(); - } - - private static CelPolicyVerifier buildPolicyVerifier( - Map variables, VerificationOptions options) { + static Cel buildCel(Map variables) { CelBuilder celBuilder = CelFactory.plannerCelBuilder() .setStandardMacros(CelStandardMacro.STANDARD_MACROS) @@ -151,10 +138,27 @@ private static CelPolicyVerifier buildPolicyVerifier( for (Map.Entry entry : variables.entrySet()) { celBuilder.addVar(entry.getKey(), entry.getValue()); } - Cel celBundle = celBuilder.build(); + return celBuilder.build(); + } + + static CelVerifier buildVerifier(Map variables, VerificationOptions options) { + CelVerifierBuilder builder = + CelVerifierFactory.newVerifier(buildCel(variables)) + .setTimeout(options.getTimeout()) + .setComprehensionUnrollLimit(options.getComprehensionUnrollLimit()); + + for (String unknown : options.getUnknownIdentifiers()) { + builder.addUnknownIdentifier(unknown); + } + return builder.build(); + } + + private static CelPolicyVerifier buildPolicyVerifier( + Map variables, VerificationOptions options) { + Cel celBundle = buildCel(variables); CelPolicyCompiler policyCompiler = CelPolicyCompilerFactory.newPolicyCompiler(celBundle).build(); - CelVerifier astVerifier = buildVerifier(options); + CelVerifier astVerifier = buildVerifier(variables, options); return CelPolicyVerifierFactory.newVerifier(policyCompiler, astVerifier).build(); } diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index f1669c486..55b9c24be 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -20,9 +20,11 @@ java_library( "//common:cel_ast", "//common:compiler_common", "//common:container", + "//common:mutable_ast", "//common:operator", "//common:options", "//common/ast", + "//common/ast:mutable_expr", "//common/types", "//common/types:message_type_provider", "//compiler:compiler_builder", @@ -47,6 +49,7 @@ java_library( "//:java_truth", "@maven//:tools_aqua_z3_turnkey", "//verifier", + "//verifier:canonicalization_optimizer", "//verifier:numeric_bounds", "//verifier:policy_verifier", "//verifier:policy_verifier_factory", diff --git a/verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java b/verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java new file mode 100644 index 000000000..ead53d46f --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java @@ -0,0 +1,566 @@ +// 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.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.testing.junit.testparameterinjector.TestParameter; +import com.google.testing.junit.testparameterinjector.TestParameterInjector; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelContainer; +import dev.cel.common.CelMutableAst; +import dev.cel.common.CelOptions; +import dev.cel.common.ast.CelMutableExpr; +import dev.cel.common.ast.CelMutableExpr.CelMutableCall; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.OptionalType; +import dev.cel.common.types.SimpleType; +import dev.cel.common.types.StructTypeReference; +import dev.cel.expr.conformance.proto3.TestAllTypes; +import dev.cel.extensions.CelExtensions; +import dev.cel.extensions.CelOptionalLibrary; +import dev.cel.optimizer.CelOptimizer; +import dev.cel.optimizer.CelOptimizerFactory; +import dev.cel.parser.CelStandardMacro; +import dev.cel.parser.CelUnparser; +import dev.cel.parser.CelUnparserFactory; +import dev.cel.verifier.CanonicalizationOptimizer.CanonicalizationOptions; +import org.junit.Test; +import org.junit.runner.RunWith; + +@RunWith(TestParameterInjector.class) +public class CanonicalizationOptimizerTest { + + private static final Cel CEL = + CelFactory.plannerCelBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .setOptions( + CelOptions.current() + .populateMacroCalls(true) + .enableHeterogeneousNumericComparisons(true) + .build()) + .addMessageTypes(TestAllTypes.getDescriptor()) + .addCompilerLibraries( + CelExtensions.comprehensions(), CelExtensions.bindings(), CelOptionalLibrary.INSTANCE) + .addRuntimeLibraries(CelExtensions.comprehensions(), CelOptionalLibrary.INSTANCE) + // Abstract DYN variables for alphabetical ordering and precedence tests + .addVar("dyn_a", SimpleType.DYN) + .addVar("dyn_b", SimpleType.DYN) + .addVar("dyn_c", SimpleType.DYN) + .addVar("dyn_d", SimpleType.DYN) + // Explicit Primitive typed variables + .addVar("bool_var", SimpleType.BOOL) + .addVar("bool_var2", SimpleType.BOOL) + .addVar("int_var", SimpleType.INT) + .addVar("int_var2", SimpleType.INT) + .addVar("uint_var", SimpleType.UINT) + .addVar("uint_var2", SimpleType.UINT) + .addVar("double_var", SimpleType.DOUBLE) + .addVar("double_var2", SimpleType.DOUBLE) + .addVar("string_var", SimpleType.STRING) + .addVar("string_var2", SimpleType.STRING) + .addVar("bytes_var", SimpleType.BYTES) + .addVar("bytes_var2", SimpleType.BYTES) + .addVar("duration_var", SimpleType.DURATION) + .addVar("timestamp_var", SimpleType.TIMESTAMP) + .addVar("null_var", SimpleType.NULL_TYPE) + // Collection variables + .addVar("int_list", ListType.create(SimpleType.INT)) + .addVar("string_list", ListType.create(SimpleType.STRING)) + .addVar("bool_list", ListType.create(SimpleType.BOOL)) + .addVar("nested_list", ListType.create(ListType.create(SimpleType.INT))) + .addVar("opt_list", ListType.create(OptionalType.create(SimpleType.INT))) + .addVar("string_int_map", MapType.create(SimpleType.STRING, SimpleType.INT)) + .addVar("int_string_map", MapType.create(SimpleType.INT, SimpleType.STRING)) + .addVar( + "nested_map", + MapType.create(SimpleType.STRING, MapType.create(SimpleType.STRING, SimpleType.INT))) + .addVar("list_map", ListType.create(MapType.create(SimpleType.STRING, SimpleType.INT))) + .addVar("int_list_map", MapType.create(SimpleType.INT, ListType.create(SimpleType.INT))) + // Struct / proto message variables + .addVar("msg", StructTypeReference.create(TestAllTypes.getDescriptor().getFullName())) + .addVar("msg2", StructTypeReference.create(TestAllTypes.getDescriptor().getFullName())) + .build(); + + private static final CelOptimizer OPTIMIZER = + CelOptimizerFactory.standardCelOptimizerBuilder(CEL) + .addAstOptimizers( + CanonicalizationOptimizer.newInstance(CanonicalizationOptions.newBuilder().build())) + .build(); + + private static final CelUnparser UNPARSER = CelUnparserFactory.newUnparser(); + + private enum CanonicalizationTestCase { + // Commutative Logical Operators (&&, ||) across Simple Types + COMMUTATIVE_AND_BOOL( + "bool_var == true && bool_var2 == false", "bool_var == true && bool_var2 == false"), + COMMUTATIVE_AND_INT("int_var == 2 && int_var2 == 1", "int_var == 2 && int_var2 == 1"), + COMMUTATIVE_AND_UINT( + "uint_var == 20u && uint_var2 == 10u", "uint_var == 20u && uint_var2 == 10u"), + COMMUTATIVE_AND_DOUBLE( + "double_var == 3.14 && double_var2 == 1.41", "double_var == 3.14 && double_var2 == 1.41"), + COMMUTATIVE_AND_STRING( + "string_var == 'foo' && string_var2 == 'bar'", + "string_var == \"foo\" && string_var2 == \"bar\""), + COMMUTATIVE_AND_BYTES( + "bytes_var == b'foo' && bytes_var2 == b'bar'", + "bytes_var == b\"\\146\\157\\157\" && bytes_var2 == b\"\\142\\141\\162\""), + COMMUTATIVE_AND_NULL("null_var == null && dyn_a == null", "dyn_a == null && null_var == null"), + COMMUTATIVE_AND_MULTI_OPERAND( + "string_var == 'c' && string_var == 'a' && string_var == 'b'", + "string_var == \"a\" && string_var == \"b\" && string_var == \"c\""), + COMMUTATIVE_OR_MULTI_OPERAND( + "int_var == 30 || int_var == 10 || int_var == 20", + "int_var == 10 || int_var == 20 || int_var == 30"), + COMMUTATIVE_AND_DEDUPLICATION("int_var == 1 && int_var == 1", "int_var == 1"), + COMMUTATIVE_OR_DEDUPLICATION("string_var == 'a' || string_var == 'a'", "string_var == \"a\""), + COMMUTATIVE_AND_MIXED_TYPES( + "string_var == 'foo' && int_var == 1", "int_var == 1 && string_var == \"foo\""), + COMMUTATIVE_OR_MIXED_TYPES( + "bool_var == true || int_var == 1", "bool_var == true || int_var == 1"), + LIST_DIFFERENT_SIZES_EQUALITY("[1, 2] == [1]", "[1] == [1, 2]"), + ONE_ARG_CALL_WITH_LOGICAL_OPERANDS( + "type(bool_var == true && bool_var2 == false)", + "type(bool_var == true && bool_var2 == false)"), + COMMUTATIVE_AND_DURATION_TIMESTAMP( + "timestamp_var == timestamp('2026-01-01T00:00:00Z') && duration_var == duration('10s')", + "duration_var == duration(\"10s\") && timestamp_var ==" + + " timestamp(\"2026-01-01T00:00:00Z\")"), + COMMUTATIVE_AND_NESTED_LOGIC( + "(dyn_b || dyn_a) && (dyn_d || dyn_c)", "(dyn_a || dyn_b) && (dyn_c || dyn_d)"), + + // Symmetric Equality (==) and Inequality (!=) across Types + SYMMETRIC_EQUALS_BOOL("true == bool_var", "bool_var == true"), + SYMMETRIC_NOT_EQUALS_BOOL("false != bool_var", "bool_var != false"), + SYMMETRIC_EQUALS_INT("42 == int_var", "int_var == 42"), + SYMMETRIC_NOT_EQUALS_INT("0 != int_var", "int_var != 0"), + SYMMETRIC_EQUALS_UINT("100u == uint_var", "uint_var == 100u"), + SYMMETRIC_NOT_EQUALS_UINT("0u != uint_var", "uint_var != 0u"), + SYMMETRIC_EQUALS_DOUBLE("3.14159 == double_var", "double_var == 3.14159"), + SYMMETRIC_NOT_EQUALS_DOUBLE("0.0 != double_var", "double_var != 0.0"), + SYMMETRIC_EQUALS_STRING("'hello' == string_var", "string_var == \"hello\""), + SYMMETRIC_NOT_EQUALS_STRING("'' != string_var", "string_var != \"\""), + SYMMETRIC_EQUALS_BYTES("b'abc' == bytes_var", "bytes_var == b\"\\141\\142\\143\""), + SYMMETRIC_NOT_EQUALS_BYTES("b'' != bytes_var", "bytes_var != b\"\""), + SYMMETRIC_EQUALS_IDENT_ORDERING("dyn_c == dyn_a", "dyn_a == dyn_c"), + SYMMETRIC_EQUALS_CALL_VS_IDENT("size(int_list) == int_var", "int_var == size(int_list)"), + SYMMETRIC_EQUALS_SELECT_VS_IDENT("msg.single_int64 == dyn_a", "dyn_a == msg.single_int64"), + SYMMETRIC_EQUALS_GLOBAL_VS_MEMBER_CALL( + "int_list.size() == size(int_list)", "size(int_list) == int_list.size()"), + COMMUTATIVE_AND_GLOBAL_VS_MEMBER_CALL( + "int_list.size() == 1 && size(int_list) == 1", + "size(int_list) == 1 && int_list.size() == 1"), + + // De Morgan Transformations on Logical NOT (!) + DE_MORGAN_DOUBLE_NEGATION("!!bool_var", "bool_var"), + DE_MORGAN_QUADRUPLE_NEGATION("!!!!(int_var == 1)", "int_var == 1"), + DE_MORGAN_AND_TYPED( + "!(int_var == 1 && string_var == 'foo')", "int_var != 1 || string_var != \"foo\""), + DE_MORGAN_OR_TYPED( + "!(int_var == 1 || string_var == 'foo')", "int_var != 1 && string_var != \"foo\""), + DE_MORGAN_EQUALS_TYPED("!(int_var == 1)", "int_var != 1"), + DE_MORGAN_NOT_EQUALS_TYPED("!(int_var != 1)", "int_var == 1"), + DE_MORGAN_NESTED_AND_OR( + "!((dyn_a && dyn_b) || (dyn_c && dyn_d))", "(!dyn_a || !dyn_b) && (!dyn_c || !dyn_d)"), + DE_MORGAN_NESTED_OR_AND( + "!((dyn_a || dyn_b) && (dyn_c || dyn_d))", "!dyn_a && !dyn_b || !dyn_c && !dyn_d"), + DE_MORGAN_MIXED_TYPES( + "!(bool_var == true && double_var == 1.0)", "bool_var != true || double_var != 1.0"), + DE_MORGAN_ALL_NEGATED_PREDICATE("!int_list.all(e, !(e == 1))", "e == 1"), + DE_MORGAN_EXISTS_NEGATED_PREDICATE("!int_list.exists(e, !(e == 1))", "e == 1"), + DE_MORGAN_ALL_NEGATED_VAR_PREDICATE( + "!int_list.all(e, !bool_var)", "int_list.exists(e, bool_var)"), + DE_MORGAN_EXISTS_NEGATED_VAR_PREDICATE( + "!int_list.exists(e, !bool_var)", "int_list.all(e, bool_var)"), + DE_MORGAN_RELATIONAL_UNCHANGED("!(int_var > 5)", "!(int_var > 5)"), + DE_MORGAN_EXISTS_TYPED("!int_list.exists(e, e == 1)", "e != 1"), + DE_MORGAN_ALL_TYPED("!int_list.all(e, e == 1)", "e != 1"), + DE_MORGAN_EXISTS_COMPLEX_PREDICATE( + "!int_list.exists(e, !(e == 1 && e == 2))", "e == 1 && e == 2"), + DE_MORGAN_ALL_COMPLEX_PREDICATE("!int_list.all(e, !(e == 1 || e == 2))", "e == 1 || e == 2"), + DE_MORGAN_BOOL_VARIABLES("!(bool_var && bool_var2)", "!bool_var || !bool_var2"), + + // Extension Coverage - Optionals & Optional Indexing/Fields + OPTIONAL_OF_EQUALITY_SYMMETRY( + "optional.of(dyn_b) == optional.of(dyn_a)", "optional.of(dyn_a) == optional.of(dyn_b)"), + OPTIONAL_NONE_EQUALITY_SYMMETRY( + "optional.of(dyn_a) == optional.none()", "optional.none() == optional.of(dyn_a)"), + OPTIONAL_OF_NON_ZERO_VALUE_SYMMETRY( + "optional.ofNonZeroValue(dyn_b) == optional.ofNonZeroValue(dyn_a)", + "optional.ofNonZeroValue(dyn_a) == optional.ofNonZeroValue(dyn_b)"), + OPTIONAL_FIELD_SELECT_EQUALITY( + "msg.?single_int64 == optional.of(1)", "msg.?single_int64 == optional.of(1)"), + OPTIONAL_FIELD_SELECT_INEQUALITY( + "msg.?single_string != optional.none()", "msg.?single_string != optional.none()"), + OPTIONAL_FIELD_SELECT_OR_VALUE_EQUALITY( + "msg.?single_int64.orValue(0) == int_var", "int_var == msg.?single_int64.orValue(0)"), + OPTIONAL_LIST_ELEMENT_EQUALITY( + "[?optional.of(1)] == [?optional.of(int_var)]", + "[?optional.of(int_var)] == [?optional.of(1)]"), + OPTIONAL_MAP_ENTRY_EQUALITY( + "{?'key': optional.of(1)} == {?'key': optional.of(int_var)}", + "{?\"key\": optional.of(int_var)} == {?\"key\": optional.of(1)}"), + DE_MORGAN_OPTIONAL_EQUALITY( + "!(optional.of(dyn_a) == optional.of(dyn_b))", "optional.of(dyn_a) != optional.of(dyn_b)"), + DE_MORGAN_OPTIONAL_INEQUALITY( + "!(optional.of(dyn_a) != optional.none())", "optional.none() == optional.of(dyn_a)"), + COMMUTATIVE_AND_OPTIONAL_HAS_VALUE( + "optional.of(dyn_b).hasValue() && optional.of(dyn_a).hasValue()", + "optional.of(dyn_a).hasValue() && optional.of(dyn_b).hasValue()"), + COMMUTATIVE_OR_OPTIONAL_HAS_VALUE( + "optional.of(dyn_b).hasValue() || optional.of(dyn_a).hasValue()", + "optional.of(dyn_a).hasValue() || optional.of(dyn_b).hasValue()"), + COMMUTATIVE_AND_OPTIONAL_FIELD_SELECT( + "msg.?single_string.hasValue() && msg.?single_int64.hasValue()", + "msg.?single_int64.hasValue() && msg.?single_string.hasValue()"), + COMMUTATIVE_OR_OPTIONAL_FIELD_SELECT( + "msg.?single_string.hasValue() || msg.?single_int64.hasValue()", + "msg.?single_int64.hasValue() || msg.?single_string.hasValue()"), + DE_MORGAN_OPTIONAL_HAS_VALUE_AND( + "!(optional.of(dyn_a).hasValue() && optional.of(dyn_b).hasValue())", + "!optional.of(dyn_a).hasValue() || !optional.of(dyn_b).hasValue()"), + DE_MORGAN_OPTIONAL_HAS_VALUE_OR( + "!(optional.of(dyn_a).hasValue() || optional.of(dyn_b).hasValue())", + "!optional.of(dyn_a).hasValue() && !optional.of(dyn_b).hasValue()"), + OPTIONAL_IN_EXISTS_COMPREHENSION( + "!opt_list.exists(x, !(x.hasValue() && x.value() == 1))", "x.value() == 1 && x.hasValue()"), + OPTIONAL_IN_ALL_COMPREHENSION( + "!opt_list.all(x, !(x.hasValue() || x.value() == 1))", "x.value() == 1 || x.hasValue()"), + OPTIONAL_FIELD_CHAINING_EQUALITY( + "msg.?single_nested_message.?bb == optional.of(42)", + "msg.?single_nested_message.?bb == optional.of(42)"), + OPTIONAL_MAP_INDEXING_EQUALITY( + "string_int_map.?foo == optional.of(1)", "string_int_map.?foo == optional.of(1)"), + + // Extension Coverage - Two-Variable Comprehensions + DE_MORGAN_2VAR_EXISTS_MAP( + "!string_int_map.exists(k, v, k == 'foo' && v == 1)", "k != \"foo\" || v != 1"), + DE_MORGAN_2VAR_ALL_MAP( + "!string_int_map.all(k, v, !(k == 'foo' || v == 1))", "k == \"foo\" || v == 1"), + DE_MORGAN_2VAR_EXISTS_NEGATED_PREDICATE( + "!string_int_map.exists(k, v, !(v > 0 && k == 'foo'))", "k == \"foo\" && v > 0"), + DE_MORGAN_2VAR_ALL_NEGATED_PREDICATE( + "!string_int_map.all(k, v, !(v > 0 || k == 'foo'))", "k == \"foo\" || v > 0"), + TWO_VAR_EXISTS_COMMUTATIVE_AND( + "string_int_map.exists(k, v, v == 1 && k == 'foo')", + "string_int_map.exists(k, v, k == \"foo\" && v == 1)"), + TWO_VAR_ALL_COMMUTATIVE_OR( + "string_int_map.all(k, v, v == 1 || k == 'foo')", + "string_int_map.all(k, v, k == \"foo\" || v == 1)"), + TWO_VAR_EXISTS_SYMMETRIC_EQUALITY( + "string_int_map.exists(k, v, v == 1)", "string_int_map.exists(k, v, v == 1)"), + TWO_VAR_ALL_SYMMETRIC_INEQUALITY( + "string_int_map.all(k, v, v != 0)", "string_int_map.all(k, v, v != 0)"), + TWO_VAR_EXISTS_INT_STRING_MAP( + "int_string_map.exists(k, v, v == 'bar' && k == 1)", + "int_string_map.exists(k, v, k == 1 && v == \"bar\")"), + TWO_VAR_ALL_INT_STRING_MAP( + "!int_string_map.all(k, v, k == 1 || v == 'bar')", "k != 1 && v != \"bar\""), + TWO_VAR_EXISTS_LIST_INDEX_VALUE( + "!int_list.exists(i, v, i == 0 && v == 100)", "i != 0 || v != 100"), + TWO_VAR_ALL_LIST_INDEX_VALUE( + "!int_list.all(i, v, !(i == 0 || v == 100))", "i == 0 || v == 100"), + TWO_VAR_EXISTS_LIST_COMMUTATIVE_AND( + "int_list.exists(i, v, v == 100 && i == 0)", "int_list.exists(i, v, i == 0 && v == 100)"), + TWO_VAR_ALL_LIST_COMMUTATIVE_OR( + "int_list.all(i, v, v == 100 || i == 0)", "int_list.all(i, v, i == 0 || v == 100)"), + TWO_VAR_NESTED_COMPREHENSIONS( + "string_int_map.exists(k, v, k == 'foo' && int_list.all(i, e, e == v && i == 0))", + "string_int_map.exists(k, v, k == \"foo\" && int_list.all(i, e, e == v && i == 0))"), + DE_MORGAN_2VAR_NESTED_COMPREHENSIONS( + "string_int_map.exists(k, v, k == 'foo' && !int_list.exists(i, e, e == v))", + "string_int_map.exists(k, v, k == \"foo\" && e != v)"), + TWO_VAR_COMPREHENSION_WITH_OPTIONALS( + "!string_int_map.exists(k, v, optional.of(v).hasValue() && k == 'foo')", + "!optional.of(v).hasValue() || k != \"foo\""), + TWO_VAR_COMPREHENSION_STRUCT_FIELDS( + "!string_int_map.exists(k, v, !(k == msg.single_string && v == msg.single_int64))", + "k == msg.single_string && v == msg.single_int64"), + TWO_VAR_COMPREHENSION_DEDUPLICATION( + "string_int_map.exists(k, v, k == 'foo' && k == 'foo')", + "string_int_map.exists(k, v, k == \"foo\")"), + TWO_VAR_COMPREHENSION_DE_MORGAN_INEQUALITY( + "!string_int_map.exists(k, v, !(k != 'foo' && v != 1))", "k != \"foo\" && v != 1"), + + // Extension Coverage - cel.bind Macro + CEL_BIND_COMMUTATIVE_AND( + "cel.bind(x, int_var + 10, 1 == x && 2 == int_var2)", + "cel.bind(x, int_var + 10, int_var2 == 2 && x == 1)"), + CEL_BIND_COMMUTATIVE_OR( + "cel.bind(x, int_var + 10, 1 == x || 2 == int_var2)", + "cel.bind(x, int_var + 10, int_var2 == 2 || x == 1)"), + CEL_BIND_SYMMETRIC_EQUALITY( + "cel.bind(x, int_var + 10, 20 == x)", "cel.bind(x, int_var + 10, x == 20)"), + CEL_BIND_NESTED( + "cel.bind(x, int_var + 10, cel.bind(y, int_var2 + 20, 2 == y && 1 == x))", + "cel.bind(x, int_var + 10, cel.bind(y, int_var2 + 20, x == 1 && y == 2))"), + CEL_BIND_DE_MORGAN( + "cel.bind(x, int_var == 1, !(2 == int_var2 && x == true))", + "cel.bind(x, int_var == 1, int_var2 != 2 || x != true)"), + + // Nested Lists, Maps, and Structs + NESTED_LIST_EQUALITY_SYMMETRY( + "[[2, 1], [4, 3]] == [[1, 2], [3, 4]]", "[[1, 2], [3, 4]] == [[2, 1], [4, 3]]"), + NESTED_LIST_INEQUALITY_SYMMETRY("[[2, 1]] != [[1, 2]]", "[[1, 2]] != [[2, 1]]"), + LIST_ELEMENT_ORDERING_EQUALITY("int_list == [3, 2, 1]", "int_list == [3, 2, 1]"), + MAP_EQUALITY_ORDERING( + "string_int_map == {'b': 2, 'a': 1}", "string_int_map == {\"b\": 2, \"a\": 1}"), + MAP_DIFFERENT_SIZES_EQUALITY( + "{'b': 2, 'a': 1} == {'a': 1}", "{\"a\": 1} == {\"b\": 2, \"a\": 1}"), + COMMUTATIVE_AND_MAP_DIFFERENT_SIZES( + "string_int_map == {'a': 1, 'b': 2} && string_int_map == {'a': 1}", + "string_int_map == {\"a\": 1} && string_int_map == {\"a\": 1, \"b\": 2}"), + NESTED_MAP_EQUALITY( + "nested_map == {'b': {'d': 4, 'c': 3}, 'a': {'y': 2, 'x': 1}}", + "nested_map == {\"b\": {\"d\": 4, \"c\": 3}, \"a\": {\"y\": 2, \"x\": 1}}"), + LIST_OF_MAPS_EQUALITY( + "list_map == [{'y': 2, 'x': 1}, {'d': 4, 'c': 3}]", + "list_map == [{\"y\": 2, \"x\": 1}, {\"d\": 4, \"c\": 3}]"), + MAP_OF_LISTS_EQUALITY( + "int_list_map == {1: [2, 1], 2: [4, 3]}", "int_list_map == {1: [2, 1], 2: [4, 3]}"), + STRUCT_EQUALITY_ORDERING( + "msg == TestAllTypes{single_int64: 10, single_string: 'foo'}", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_int64: 10, single_string:" + + " \"foo\"}"), + NESTED_STRUCT_EQUALITY( + "msg == TestAllTypes{single_nested_message: TestAllTypes.NestedMessage{bb: 42}}", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_nested_message:" + + " cel.expr.conformance.proto3.TestAllTypes.NestedMessage{bb: 42}}"), + STRUCT_INEQUALITY( + "msg != TestAllTypes{single_int64: 0}", + "msg != cel.expr.conformance.proto3.TestAllTypes{single_int64: 0}"), + STRUCT_DIFFERENT_ENTRY_COUNTS_ORDERING( + "TestAllTypes{single_int64: 10, single_string: 'foo'} == TestAllTypes{single_int64: 10}", + "cel.expr.conformance.proto3.TestAllTypes{single_int64: 10} ==" + + " cel.expr.conformance.proto3.TestAllTypes{single_int64: 10, single_string:" + + " \"foo\"}"), + STRUCT_DIFFERENT_FIELD_VALUES_ORDERING( + "TestAllTypes{single_int64: 20} == TestAllTypes{single_int64: 10}", + "cel.expr.conformance.proto3.TestAllTypes{single_int64: 10} ==" + + " cel.expr.conformance.proto3.TestAllTypes{single_int64: 20}"), + DE_MORGAN_STRUCT_EQUALITY( + "!(msg == TestAllTypes{single_int64: 10})", + "msg != cel.expr.conformance.proto3.TestAllTypes{single_int64: 10}"), + DE_MORGAN_STRUCT_INEQUALITY( + "!(msg != TestAllTypes{single_int64: 10})", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_int64: 10}"), + COMMUTATIVE_AND_STRUCT_FIELDS( + "msg.single_string == 'foo' && msg.single_int64 == 10", + "msg.single_int64 == 10 && msg.single_string == \"foo\""), + COMMUTATIVE_OR_STRUCT_FIELDS( + "msg.single_int64 == 20 || msg.single_int64 == 10", + "msg.single_int64 == 10 || msg.single_int64 == 20"), + DE_MORGAN_STRUCT_FIELDS_AND( + "!(msg.single_int64 == 10 && msg.single_string == 'foo')", + "msg.single_int64 != 10 || msg.single_string != \"foo\""), + DE_MORGAN_STRUCT_FIELDS_OR( + "!(msg.single_int64 == 10 || msg.single_int64 == 20)", + "msg.single_int64 != 10 && msg.single_int64 != 20"), + STRUCT_SELECT_ORDERING("msg.single_int64 == int_var", "int_var == msg.single_int64"), + NESTED_STRUCT_SELECT_ORDERING( + "msg.single_nested_message.bb == int_var", "int_var == msg.single_nested_message.bb"), + MAP_LOOKUP_IN_LOGICAL_EXPR( + "string_int_map['foo'] == 1 && string_int_map['bar'] == 2", + "string_int_map[\"bar\"] == 2 && string_int_map[\"foo\"] == 1"), + LIST_INDEX_IN_LOGICAL_EXPR( + "int_list[1] == 20 && int_list[0] == 10", "int_list[0] == 10 && int_list[1] == 20"), + COMPREHENSIONS_IN_LIST_LITERALS( + "[int_list.exists(e, e == 2), int_list.exists(e, e == 1)] == [true, false]", + "[int_list.exists(e, e == 2), int_list.exists(e, e == 1)] == [true, false]"), + COMPREHENSIONS_IN_MAP_LITERALS( + "{'b': int_list.all(e, e > 0), 'a': int_list.exists(e, e == 1)} == {'a': true, 'b': false}", + "{\"a\": true, \"b\": false} == {\"b\": int_list.all(e, e > 0), \"a\": int_list.exists(e, e" + + " == 1)}"), + COMPREHENSIONS_IN_STRUCT_FIELDS( + "TestAllTypes{single_int64: int_list[0]} == msg", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_int64: int_list[0]}"), + NESTED_COMPREHENSIONS_IN_STRUCT_FIELDS( + "!int_list.exists(x, TestAllTypes{single_int64: x} == msg)", + "msg != cel.expr.conformance.proto3.TestAllTypes{single_int64: x}"), + DE_MORGAN_COLLECTION_LITERAL_EQUALITY("!([2, 1] == [1, 2])", "[1, 2] != [2, 1]"), + + // Cross-Type & Heterogeneous Comparisons + HETEROGENEOUS_INT_UINT_AND("int_var == 1 && uint_var == 1u", "int_var == 1 && uint_var == 1u"), + HETEROGENEOUS_INT_DOUBLE_OR( + "int_var == 1 || double_var == 1.0", "double_var == 1.0 || int_var == 1"), + HETEROGENEOUS_UINT_DOUBLE_EQUALITY( + "uint_var == 10u && double_var == 10.0", "double_var == 10.0 && uint_var == 10u"), + CROSS_TYPE_DURATION_TIMESTAMP_AND( + "timestamp_var == timestamp('2026-01-01T00:00:00Z') && duration_var == duration('10s')", + "duration_var == duration(\"10s\") && timestamp_var ==" + + " timestamp(\"2026-01-01T00:00:00Z\")"), + CROSS_TYPE_STRING_BYTES_OR( + "string_var == 'foo' || bytes_var == b'foo'", + "bytes_var == b\"\\146\\157\\157\" || string_var == \"foo\""), + NULL_VS_PRIMITIVE_EQUALITY("dyn_a == null", "dyn_a == null"), + NULL_VS_MESSAGE_EQUALITY("msg == null", "msg == null"), + NULL_VS_OPTIONAL_EQUALITY("optional.of(int_var) == null", "optional.of(int_var) == null"), + CROSS_TYPE_COMMUTATIVE_CHAIN( + "string_var == 'a' && double_var == 1.0 && int_var == 1 && bool_var == true", + "bool_var == true && double_var == 1.0 && int_var == 1 && string_var == \"a\""), + DE_MORGAN_CROSS_TYPE_CHAIN( + "!(string_var == 'a' && double_var == 1.0 && int_var == 1)", + "double_var != 1.0 || int_var != 1 || string_var != \"a\""), + HETEROGENEOUS_NUMERIC_DE_MORGAN( + "!(int_var != 1 || uint_var != 1u || double_var != 1.0)", + "double_var == 1.0 && int_var == 1 && uint_var == 1u"), + CROSS_TYPE_IN_2VAR_COMPREHENSION( + "!string_int_map.exists(k, v, !(int_var == 1 && double_var == 1.0))", + "double_var == 1.0 && int_var == 1"), + CROSS_TYPE_IN_LIST_COMPREHENSION( + "!int_list.exists(e, !(uint_var == 1u || double_var == 1.0))", + "double_var == 1.0 || uint_var == 1u"), + MIXED_SELECT_AND_CALLS_ACROSS_TYPES( + "msg.single_int64 == size(int_list) && msg.single_string == string(int_var)", + "msg.single_int64 == size(int_list) && msg.single_string == string(int_var)"), + DE_MORGAN_MIXED_SELECT_AND_CALLS( + "!(msg.single_int64 == size(int_list) && msg.single_string == 'foo')", + "msg.single_int64 != size(int_list) || msg.single_string != \"foo\""), + + // Edge Cases, Invariants, Non-Canonicalizable Expressions, and Precedence + RELATIONAL_OPERATORS_UNCHANGED("int_var < 10 && int_var > 5", "int_var < 10 && int_var > 5"), + DE_MORGAN_RELATIONAL_OPERATORS("!(int_var < 10)", "!(int_var < 10)"), + TERNARY_OPERATOR_UNCHANGED_COND( + "bool_var ? int_var == 1 : int_var == 2", "bool_var ? (int_var == 1) : (int_var == 2)"), + DE_MORGAN_TERNARY_OPERATOR( + "!(bool_var ? int_var == 1 : int_var == 2)", + "!(bool_var ? (int_var == 1) : (int_var == 2))"), + IN_OPERATOR_WITH_COMMUTATIVE_AND( + "int_var in int_list && bool_var == true", "int_var in int_list && bool_var == true"), + DE_MORGAN_IN_OPERATOR("!(int_var in int_list)", "!(int_var in int_list)"), + COMPREHENSION_ACCU_VAR_NOT_REORDERED( + "int_list.exists(e, e == 1 && e == 2)", "int_list.exists(e, e == 1 && e == 2)"), + COMPLEX_NESTED_DE_MORGAN_PRECEDENCE( + "!(dyn_a && dyn_b || dyn_c && dyn_d)", "(!dyn_a || !dyn_b) && (!dyn_c || !dyn_d)"), + COMPLEX_NESTED_DE_MORGAN_OR_AND( + "!((dyn_a || dyn_b) && (dyn_c || dyn_d))", "!dyn_a && !dyn_b || !dyn_c && !dyn_d"), + TRIPLE_AND_DEDUPLICATION("int_var == 1 && int_var == 1 && int_var == 1", "int_var == 1"), + TRIPLE_OR_DEDUPLICATION( + "string_var == 'x' || string_var == 'x' || string_var == 'x'", "string_var == \"x\""), + EMPTY_STRING_ZERO_CONSTANT_COMPARISONS( + "string_var == '' && int_var == 0 && bool_var == false", + "bool_var == false && int_var == 0 && string_var == \"\""), + IDENT_COMPARISON_SYMMETRY( + "dyn_b == dyn_a && dyn_d == dyn_c", "dyn_a == dyn_b && dyn_c == dyn_d"), + IDENT_INEQUALITY_SYMMETRY( + "dyn_b != dyn_a || dyn_d != dyn_c", "dyn_a != dyn_b || dyn_c != dyn_d"), + IDENT_SAME_NAME_DIFFERENT_OPERATORS( + "dyn_a != dyn_b && dyn_a == dyn_b", "dyn_a != dyn_b && dyn_a == dyn_b"); + + private final String input; + private final String expected; + + CanonicalizationTestCase(String input, String expected) { + this.input = input; + this.expected = expected; + } + } + + @Test + public void optimize_success(@TestParameter CanonicalizationTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.input).getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + String unparsed = UNPARSER.unparse(optimizedAst); + assertThat(unparsed).isEqualTo(testCase.expected); + } + + @Test + public void optimize_maxIterationLimitReached_throwsException() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_b == dyn_a && dyn_d == dyn_c").getAst(); + CanonicalizationOptimizer optimizer = + CanonicalizationOptimizer.newInstance( + CanonicalizationOptions.newBuilder().maxIterationLimit(1).build()); + + IllegalStateException e = + assertThrows(IllegalStateException.class, () -> optimizer.optimize(ast, CEL)); + assertThat(e).hasMessageThat().contains("Max iteration count reached."); + } + + @Test + public void optimize_deMorganAll_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.all(e, e == 1)").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isTrue(); + } + + @Test + public void optimize_deMorganExists_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, e == 1)").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isFalse(); + } + + @Test + public void optimize_deMorganAll_negatedPredicate_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.all(e, !(e == 1))").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isTrue(); + } + + @Test + public void optimize_deMorganExists_negatedPredicate_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, !(e == 1))").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isFalse(); + } + + @Test + public void optimize_customMacroWithExistsStructure_notCanonicalized() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, e == 1)").getAst(); + CelMutableAst mutableAst = CelMutableAst.fromCelAst(ast); + long macroKey = mutableAst.source().getMacroCalls().keySet().iterator().next(); + CelMutableExpr existingMacro = mutableAst.source().getMacroCalls().get(macroKey); + CelMutableCall customCall = + CelMutableCall.create( + existingMacro.call().target().get(), "my_custom_exists", existingMacro.call().args()); + mutableAst + .source() + .addMacroCalls(macroKey, CelMutableExpr.ofCall(existingMacro.id(), customCall)); + + CelAbstractSyntaxTree optimizedAst = + CanonicalizationOptimizer.newInstance(CanonicalizationOptions.newBuilder().build()) + .optimize(mutableAst.toParsedAst(), CEL) + .optimizedAst(); + assertThat(UNPARSER.unparse(optimizedAst)).isEqualTo("!int_list.my_custom_exists(e, e == 1)"); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index cea14e910..d7724ac91 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -131,7 +131,7 @@ public final class CelVerifierZ3ImplTest { .build(); private static final CelVerifier VERIFIER = - CelVerifierFactory.newVerifier().setTypeProvider(TYPE_PROVIDER).build(); + CelVerifierFactory.newVerifier(CEL).setTypeProvider(TYPE_PROVIDER).build(); @Before public void setUp() { @@ -380,7 +380,7 @@ public void isSatisfiable_maskedByBmcNested_inconclusive() throws Exception { CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); CelVerifier customVerifier = - CelVerifierFactory.newVerifier() + CelVerifierFactory.newVerifier(CEL) .setComprehensionUnrollLimit(3) .setTypeProvider(TYPE_PROVIDER) .build(); @@ -395,7 +395,8 @@ 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().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -956,7 +957,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown( CelAbstractSyntaxTree ast = CEL.compile(expression).getAst(); CelVerifier verifierWithUnknown = - CelVerifierFactory.newVerifier().addUnknownIdentifier("x").build(); + CelVerifierFactory.newVerifier(CEL).addUnknownIdentifier("x").build(); // 'x == x' is not a tautology if it can be unknown // i.e: CelUnknown == CelUnknown is unknown. @@ -978,7 +979,10 @@ 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().setComprehensionUnrollLimit(1).build().isAlwaysTrue(ast); + CelVerifierFactory.newVerifier(CEL) + .setComprehensionUnrollLimit(1) + .build() + .isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()) @@ -992,7 +996,8 @@ 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().setComprehensionUnrollLimit(2).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build(); CelVerificationResult verifiedValue = verifier.isAlwaysTrue(ast); // Truncated loops return Unknown, which negates to Unknown. @@ -1009,7 +1014,8 @@ 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().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); CelVerificationResult verifiedValue = verifier.isAlwaysTrue(ast); assertThat(verifiedValue.status()).isEqualTo(VerificationStatus.VERIFIED); @@ -1067,7 +1073,9 @@ public void verifyEquivalence_unknownPrecedenceOverError() throws Exception { CelAbstractSyntaxTree astB = celWithCustomFunc.compile("1 / 0").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().addUnknownIdentifier("unknown_var").build(); + CelVerifierFactory.newVerifier(celWithCustomFunc) + .addUnknownIdentifier("unknown_var") + .build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -1981,7 +1989,18 @@ private enum EquivalenceTestCase { HETEROGENEOUS_UINT_NEGATIVE_DOUBLE_EQUIVALENCE("dyn(u) == -1.0", "false"), HETEROGENEOUS_UINT_ZERO_DOUBLE_EQUIVALENCE("dyn(u) == 0.0", "u == 0u"), DYNAMIC_LIST_ELEMENT_NEVER_ERROR_EQUIVALENCE( - "size(dyn_list) > 0 ? (dyn_list[0] == 1 || dyn_list[0] != 1) : true", "true"); + "size(dyn_list) > 0 ? (dyn_list[0] == 1 || dyn_list[0] != 1) : true", "true"), + CANONICALIZE_MAP_TWO_VAR_PREDICATE_ORDER( + "string_int_map.exists(k, v, k == 'foo' && v == 1)", + "string_int_map.exists(k, v, v == 1 && k == 'foo')"), + CANONICALIZE_MAP_TWO_VAR_ALPHA_RENAME( + "string_int_map.exists(k, v, k == 'foo' && v == 1)", + "string_int_map.exists(key, val, key == 'foo' && val == 1)"), + CANONICALIZE_MAP_TWO_VAR_DE_MORGAN( + "!string_int_map.exists(k, v, !(v > 0))", "string_int_map.all(k, v, v > 0)"), + CANONICALIZE_LIST_PREDICATE_ORDER( + "int_list.all(e, e > 0 && e < 100)", "int_list.all(e, e < 100 && e > 0)"), + CANONICALIZE_LIST_ALPHA_RENAME("int_list.all(e, e > 0)", "int_list.all(elem, elem > 0)"); private final String exprA; private final String exprB; @@ -2367,7 +2386,7 @@ public void verifyEquivalence_functionError_equivalent() throws Exception { @Test @SuppressWarnings("GoodTime-ApiWithNumericTimeUnit") // Test only public void setTimeout_invalidDuration_throws(@TestParameter({"0", "-1"}) long timeoutSeconds) { - CelVerifierBuilder builder = CelVerifierFactory.newVerifier(); + CelVerifierBuilder builder = CelVerifierFactory.newVerifier(CEL); IllegalArgumentException exception = assertThrows( IllegalArgumentException.class, @@ -2386,9 +2405,6 @@ public void isSatisfiable_divisionByZero_failsInCelWithErrors() throws Exception @Test public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws Exception { - CelVerifier timeoutVerifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofMillis(1)).build(); - Cel customCel = CelFactory.plannerCelBuilder() .addVar("d1", SimpleType.DOUBLE) @@ -2396,6 +2412,8 @@ public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws .addVar("d3", SimpleType.DOUBLE) .addVar("d4", SimpleType.DOUBLE) .build(); + CelVerifier timeoutVerifier = + CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); // An overly complex double multiplication to guarantee Z3 FPA theory solver timeouts. CelAbstractSyntaxTree ast = @@ -2819,7 +2837,7 @@ public void isAlwaysTrue_largeListCounterexample_truncatesOutput() throws Except CelAbstractSyntaxTree ast = cel.compile("!(large_list == " + listLiteral + ")").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofSeconds(10)).build(); + CelVerifierFactory.newVerifier(cel).setTimeout(Duration.ofSeconds(10)).build(); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -2844,7 +2862,7 @@ public void isAlwaysTrue_largeMapCounterexample_truncatesOutput() throws Excepti CelAbstractSyntaxTree ast = cel.compile("!(large_map == " + mapLiteral + ")").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofSeconds(10)).build(); + CelVerifierFactory.newVerifier(cel).setTimeout(Duration.ofSeconds(10)).build(); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -2895,7 +2913,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().build(); + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -2910,7 +2928,8 @@ 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().setComprehensionUnrollLimit(3).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(3).build(); CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); @@ -2925,7 +2944,8 @@ public void verifyEquivalence_maskedByBmcButAlwaysEqual_returnsVerified() throws CelAbstractSyntaxTree astA = CEL.compile(exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(exprB).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(3).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(3).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); @@ -2952,7 +2972,8 @@ public void verifyEquivalence_zeroUnrollLimit_returnsInconclusive( CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -3001,7 +3022,8 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive() 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().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -3045,7 +3067,8 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus CelAbstractSyntaxTree astB = customCel.compile("cel.bind(x, 20, dyn_list.my_macro(1))").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -3053,9 +3076,6 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus @Test public void verifyEquivalence_timeoutReached_throwsCelVerificationException() throws Exception { - CelVerifier timeoutVerifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofMillis(1)).build(); - Cel customCel = CelFactory.plannerCelBuilder() .addVar("d1", SimpleType.DOUBLE) @@ -3064,6 +3084,9 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th .addVar("d4", SimpleType.DOUBLE) .build(); + CelVerifier timeoutVerifier = + CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); + CelAbstractSyntaxTree astA = customCel .compile( @@ -3085,7 +3108,7 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th CelAbstractSyntaxTree assertAst = CEL.compile("int_list.all(x, x > 0)").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build(); + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build(); CelVerificationResult result = ((CelVerifierZ3Impl) verifier) .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); @@ -3102,7 +3125,7 @@ public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() t // Assertion: x < d is false when d is NaN CelAbstractSyntaxTree assertAst = CEL.compile("!(x < d)").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().build(); + CelVerifier verifier = CelVerifierFactory.newVerifier(CEL).build(); CelVerificationResult result = ((CelVerifierZ3Impl) verifier) .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java index 5b289c39a..88cd62b88 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -174,6 +174,20 @@ public void repl_equivDoubleNegation() throws Exception { assertThat(output[0]).contains("[VERIFIED]"); } + @Test + public void repl_equivCanonicalization() throws Exception { + String[] output = + runReplWithCommands( + ":var map_string_int map", + ":var int_list list", + "equiv map_string_int.exists(k, v, k == 'foo' && v == 1) <=> map_string_int.exists(k," + + " v, v == 1 && k == 'foo')", + "equiv int_list.all(e, e > 0) <=> int_list.all(elem, elem > 0)", + ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).isEmpty(); + } + @Test public void repl_unknownCommandsAndErrors() throws Exception { String[] output = diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java index 383604aa0..e3b2a21a6 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -267,6 +267,23 @@ public void verifyEquivalence_equivalent() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } + @Test + public void verifyEquivalence_canonicalizedMapComprehension() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = + ImmutableMap.of("map_string_int", MapType.create(SimpleType.STRING, SimpleType.INT)); + + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence( + "map_string_int.exists(k, v, k == 'foo' && v == 1)", + "map_string_int.exists(k, v, v == 1 && k == 'foo')", + vars, + options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + @Test public void verifyPolicyInvariants_success() throws Exception { String yamlPolicy = diff --git a/verifier/tools/README.md b/verifier/tools/README.md index 398cbad74..b34422b27 100644 --- a/verifier/tools/README.md +++ b/verifier/tools/README.md @@ -6,6 +6,20 @@ and policy invariants without writing Java code. ## Running the CLI Tool +### Standalone Executable (Prebuilt JAR) + +You can download the standalone executable fat-JAR (`dev.cel:verifier-cli`) +directly from Maven Central and invoke it with `java -jar`: + + +```bash +# Download the latest CLI JAR +curl -LO https://repo1.maven.org/maven2/dev/cel/verifier-cli/0.13.1/verifier-cli-0.13.1.jar + +# Run the verifier CLI / REPL +java -jar verifier-cli-0.13.1.jar --help +``` + ### Running via Bazel ```bash @@ -27,11 +41,6 @@ bazel run //verifier/tools:cel_verifier_tool -- \ bazel run //verifier/tools:cel_verifier_tool -- repl ``` -### Running via Maven Central - -> **Note:** Executable binaries and Maven packages (`dev.cel:cel-verifier`) -> will be published to Maven Central in an upcoming release. - ## CLI Commands * `check-sat --expr "..."`: Verifies satisfiability of an expression and