Add axioms for comparison operators for booleans

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

@@ -85,6 +85,14 @@ Optional<TranslatedValue> 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();

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) ->

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) ->

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) ->

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) ->

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) {