From efeafc51de32bd5201b479570b079a4f77f1dd30 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 21 Oct 2026 17:18:17 -0700 Subject: [PATCH] Add axioms for comparison operators for booleans PiperOrigin-RevId: 1004349459 --- .../cel/verifier/CelZ3OperatorTranslator.java | 8 ++++++ .../dev/cel/verifier/axioms/GreaterAxiom.java | 9 +++++++ .../verifier/axioms/GreaterEqualsAxiom.java | 9 +++++++ .../dev/cel/verifier/axioms/LessAxiom.java | 9 +++++++ .../cel/verifier/axioms/LessEqualsAxiom.java | 9 +++++++ .../cel/verifier/CelVerifierZ3ImplTest.java | 25 +++++++++++++++++++ 6 files changed, 69 insertions(+) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 8d8c34aec..d4fd31962 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -85,6 +85,14 @@ Optional translateFunctionCall( return opOpt.isPresent() ? Optional.of(resultChain) : Optional.empty(); } + // A candidate overload without an axiom (e.g. a custom overload of a standard operator) is + // treated as an uninterpreted call, rather than falling through to the type-mismatch error. + if (reference != null + && reference.overloadIds().stream() + .anyMatch(id -> !functionRegistry.getTranslator(id).isPresent())) { + return Optional.empty(); + } + boolean matchedAny = false; Expr currentZ3Result = resultChain.z3Expr(); BoolExpr currentApprox = resultChain.isApproximate(); diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java index 2ccb1543a..11c038bb0 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -15,6 +15,7 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; +import com.microsoft.z3.BoolExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -26,6 +27,14 @@ final class GreaterAxiom { static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER.functionDecl()) + .addBinaryOverloadTranslator( + Comparison.GREATER_BOOL.celOverloadDecl(), + (ctx, typeSystem, constraintSink, lhs, rhs) -> + Optional.of( + typeSystem.wrapBool( + ctx.mkAnd( + (BoolExpr) typeSystem.unwrapBool(lhs), + ctx.mkNot((BoolExpr) typeSystem.unwrapBool(rhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java index d71f0f248..fad75bf3e 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -15,6 +15,7 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; +import com.microsoft.z3.BoolExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -26,6 +27,14 @@ final class GreaterEqualsAxiom { static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER_EQUALS.functionDecl()) + .addBinaryOverloadTranslator( + Comparison.GREATER_EQUALS_BOOL.celOverloadDecl(), + (ctx, typeSystem, constraintSink, lhs, rhs) -> + Optional.of( + typeSystem.wrapBool( + ctx.mkImplies( + (BoolExpr) typeSystem.unwrapBool(rhs), + (BoolExpr) typeSystem.unwrapBool(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java index 31b1d3a21..63dad8b58 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -15,6 +15,7 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; +import com.microsoft.z3.BoolExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -26,6 +27,14 @@ final class LessAxiom { static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.LESS.functionDecl()) + .addBinaryOverloadTranslator( + Comparison.LESS_BOOL.celOverloadDecl(), + (ctx, typeSystem, constraintSink, lhs, rhs) -> + Optional.of( + typeSystem.wrapBool( + ctx.mkAnd( + ctx.mkNot((BoolExpr) typeSystem.unwrapBool(lhs)), + (BoolExpr) typeSystem.unwrapBool(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java index c2466cf1b..d5e5c24bb 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -15,6 +15,7 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; +import com.microsoft.z3.BoolExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -26,6 +27,14 @@ final class LessEqualsAxiom { static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.LESS_EQUALS.functionDecl()) + .addBinaryOverloadTranslator( + Comparison.LESS_EQUALS_BOOL.celOverloadDecl(), + (ctx, typeSystem, constraintSink, lhs, rhs) -> + Optional.of( + typeSystem.wrapBool( + ctx.mkImplies( + (BoolExpr) typeSystem.unwrapBool(lhs), + (BoolExpr) typeSystem.unwrapBool(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 6906038b6..12cd5fa4d 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -554,6 +554,10 @@ public void isSatisfiable_timeout_throwsException() throws Exception { private enum IsAlwaysTrueTestCase { LOGICAL_OR_CONSTANTS("true || false"), + BOOL_ORDERING( + "false < true && !(true < false) && false <= true && !(true <= false) && true > false" + + " && !(false > true) && true >= false && !(false >= true)"), + BOOL_ORDERING_REFLEXIVE("a <= a && a >= a && !(a < a) && !(a > a)"), TIMESTAMP_GREATER_EQUALS("timestamp(200) >= timestamp(100)"), DURATION_GREATER_EQUALS( "(timestamp(200) - timestamp(100)) >= (timestamp(150) - timestamp(100))"), @@ -2853,6 +2857,27 @@ public void verifyEquivalence_identicalFunctionCalls_equivalent() throws Excepti assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } + @Test + public void isSatisfiable_customOperatorOverload_inconclusive() throws Exception { + // The custom overload has no axiom, so it must not fall through to the type-mismatch error. + CelCompiler celCompiler = + CEL.toCompilerBuilder() + .addFunctionDeclarations( + CelFunctionDecl.newFunctionDeclaration( + Operator.LESS.getFunction(), + CelOverloadDecl.newGlobalOverload( + "less_list_int", + SimpleType.BOOL, + ListType.create(SimpleType.INT), + ListType.create(SimpleType.INT)))) + .build(); + CelAbstractSyntaxTree ast = celCompiler.compile("!(int_list < int_list_2)").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + @Test @SuppressWarnings("GoodTime-ApiWithNumericTimeUnit") // Test only public void setTimeout_invalidDuration_throws(@TestParameter({"0", "-1"}) long timeoutSeconds) {