From d01369a22eda6c25f8c6dde303e67ed835304a75 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Thu, 30 Jul 2026 14:17:55 -0700 Subject: [PATCH] Add REPL for Verifier PiperOrigin-RevId: 956732382 --- BUILD.bazel | 8 + MODULE.bazel | 2 + .../cel/common/internal/ProtoTimeUtils.java | 13 +- verifier/README.md | 6 +- .../main/java/dev/cel/verifier/BUILD.bazel | 1 + .../cel/verifier/CelAstToZ3Translator.java | 103 +++- .../CelZ3CounterexampleGenerator.java | 6 + .../cel/verifier/CelZ3OperatorTranslator.java | 36 +- .../dev/cel/verifier/CelZ3TypeSystem.java | 140 ++++- .../dev/cel/verifier/axioms/AddAxiom.java | 57 +- .../verifier/axioms/CelZ3FunctionAxiom.java | 3 +- .../dev/cel/verifier/axioms/GreaterAxiom.java | 16 +- .../verifier/axioms/GreaterEqualsAxiom.java | 16 +- .../dev/cel/verifier/axioms/LessAxiom.java | 16 +- .../cel/verifier/axioms/LessEqualsAxiom.java | 16 +- .../cel/verifier/axioms/SubtractAxiom.java | 57 +- .../dev/cel/verifier/axioms/TypeAxiom.java | 2 + .../verifier/axioms/TypeConversionAxioms.java | 161 ++--- .../java/dev/cel/verifier/tools/BUILD.bazel | 80 +++ .../cel/verifier/tools/CelVerifierRepl.java | 435 +++++++++++++ .../cel/verifier/tools/CelVerifierTool.java | 313 ++++++++++ .../verifier/tools/CelVerifierToolCore.java | 165 +++++ .../dev/cel/verifier/tools/FormatUtils.java | 146 +++++ .../verifier/tools/VerificationOptions.java | 223 +++++++ .../test/java/dev/cel/verifier/BUILD.bazel | 3 +- .../cel/verifier/CelVerifierZ3ImplTest.java | 244 ++++++-- .../java/dev/cel/verifier/tools/BUILD.bazel | 31 + .../verifier/tools/CelVerifierReplTest.java | 188 ++++++ .../verifier/tools/CelVerifierToolTest.java | 578 ++++++++++++++++++ verifier/tools/BUILD.bazel | 19 + verifier/tools/README.md | 191 ++++++ 31 files changed, 3038 insertions(+), 237 deletions(-) create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java create mode 100644 verifier/tools/BUILD.bazel create mode 100644 verifier/tools/README.md diff --git a/BUILD.bazel b/BUILD.bazel index 024908625..d2bf2124b 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -95,6 +95,14 @@ java_library( ], ) +java_library( + name = "java_jline", + exports = [ + "@maven//:org_jline_jline_reader", + "@maven//:org_jline_jline_terminal", + ], +) + default_java_toolchain( name = "repository_default_toolchain", configuration = DEFAULT_TOOLCHAIN_CONFIGURATION, diff --git a/MODULE.bazel b/MODULE.bazel index ce9c67fde..3dcf8b0e5 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -95,6 +95,8 @@ maven.install( "info.picocli:picocli:4.7.7", "org.antlr:antlr4-runtime:4.13.2", "org.freemarker:freemarker:2.3.34", + "org.jline:jline-reader:3.26.1", + "org.jline:jline-terminal:3.26.1", "org.jspecify:jspecify:1.0.0", "org.threeten:threeten-extra:1.8.0", "org.yaml:snakeyaml:2.5", diff --git a/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java b/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java index a6e98c571..124f9dbe1 100644 --- a/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java +++ b/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java @@ -18,7 +18,6 @@ import static com.google.common.math.LongMath.checkedMultiply; import static com.google.common.math.LongMath.checkedSubtract; -import com.google.common.annotations.VisibleForTesting; import com.google.common.base.Strings; import com.google.errorprone.annotations.CanIgnoreReturnValue; import com.google.protobuf.Duration; @@ -50,15 +49,11 @@ public final class ProtoTimeUtils { // Timestamp for "0001-01-01T00:00:00Z" - @VisibleForTesting - static final long TIMESTAMP_SECONDS_MIN = -62135596800L; + public static final long TIMESTAMP_SECONDS_MIN = -62135596800L; // Timestamp for "9999-12-31T23:59:59Z" - @VisibleForTesting - static final long TIMESTAMP_SECONDS_MAX = 253402300799L; - @VisibleForTesting - static final long DURATION_SECONDS_MIN = -315576000000L; - @VisibleForTesting - static final long DURATION_SECONDS_MAX = 315576000000L; + public static final long TIMESTAMP_SECONDS_MAX = 253402300799L; + public static final long DURATION_SECONDS_MIN = -315576000000L; + public static final long DURATION_SECONDS_MAX = 315576000000L; private static final int MILLIS_PER_SECOND = 1000; diff --git a/verifier/README.md b/verifier/README.md index db797a283..bd9979390 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -400,7 +400,7 @@ public class InvariantsExample { ### Timeouts -SMT solving is NP-complete and can theoretically stop responding or take an +SMT solving is NP-hard and can theoretically stop responding or take an exponential amount of time for complex formulas. The verifier uses a default timeout of 10 seconds. It is recommended to configure this to a reasonable duration for your specific use case using @@ -433,3 +433,7 @@ What this means for verification: default unless you have a specific need and bounded inputs. --- + +## Tools & CLI + +For command-line verification and interactive execution, see the [CLI Tool documentation](tools/README.md). diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index b9ac88687..4ca9794cc 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -98,6 +98,7 @@ java_library( tags = [ ], deps = [ + "//common/internal:proto_time_utils", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", "@maven//:tools_aqua_z3_turnkey", diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 8c0239efd..407f896a0 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -533,6 +533,12 @@ private Expr getDefaultValueForType(CelType type) { if (type.equals(SimpleType.UINT)) { return typeSystem.mkUint(0); } + if (type.equals(SimpleType.TIMESTAMP)) { + return typeSystem.wrapTimestamp(ctx.mkInt(0)); + } + if (type.equals(SimpleType.DURATION)) { + return typeSystem.wrapDuration(ctx.mkInt(0)); + } if (type instanceof ListType) { if (emptyListCache == null) { emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX); @@ -735,8 +741,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); + boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true); + BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( - ctx, typeSystem, callRes, Optional.of(expr), ctx.mkTrue(), args); + ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); }); } @@ -1239,9 +1247,10 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } Expr optRef = typeSystem.getOptionalRef(val); BoolExpr hasValue = typeSystem.optHasValue(optRef); - BoolExpr valConstraint = - createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType); - return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint)); + Expr optVal = typeSystem.getOptionalValue(optRef); + BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal)); + BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType); + return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); } if (type.equals(SimpleType.BOOL)) { return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val); @@ -1269,16 +1278,25 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { if (type.equals(SimpleType.BYTES)) { return (BoolExpr) ctx.mkApp(typeSystem.bytesCons().getTesterDecl(), val); } + if (type.equals(SimpleType.TIMESTAMP)) { + IntExpr seconds = typeSystem.getTimestamp(val); + return ctx.mkAnd( + typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds))); + } + if (type.equals(SimpleType.DURATION)) { + IntExpr seconds = typeSystem.getDuration(val); + return ctx.mkAnd( + typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds))); + } + if (type instanceof ListType) { - // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers - // here. + // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather + // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops. + // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ + // typeConstraint(seq[i]) BoolExpr isList = typeSystem.isList(val); CelType elemType = ((ListType) type).elemType(); - if (elemType.equals(SimpleType.DYN)) { - return isList; - } - // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i]) Expr listRef = typeSystem.getListRef(val); SeqExpr seq = typeSystem.getSeq(listRef); Expr length = ctx.mkLength(seq); @@ -1288,20 +1306,69 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { for (int i = 0; i < comprehensionUnrollLimit; i++) { IntExpr idx = ctx.mkInt(i); Expr elem = ctx.mkNth(seq, idx); - BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); BoolExpr validIndex = ctx.mkLt(idx, length); - boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); - BoolExpr outOfBounds = ctx.mkGe(idx, length); - boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown()))); + // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in + // list(dyn). For concrete types, this is already implied by createTypeConstraintForType. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem)))); + // Short-circuit DYN element types to prevent generating redundant validIndex ⇒ TRUE + // clauses. + if (!elemType.equals(SimpleType.DYN)) { + BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); + boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); + } } return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type instanceof MapType) { - // Do NOT emit a for-all quantifier over map keys here. - // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is - // naturally constrained by the primitive key assertions in getStructuralEquality(). - return typeSystem.isMap(val); + // Do NOT emit a for-all quantifier over map keys or values here. + // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using + // bounded unrolling over the key sequence up to comprehensionUnrollLimit. + // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key) + // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val)) + BoolExpr isMap = typeSystem.isMap(val); + MapType mapType = (MapType) type; + CelType keyType = mapType.keyType(); + CelType valType = mapType.valueType(); + + Expr mapRef = typeSystem.getMapRef(val); + SeqExpr seq = typeSystem.getMapKeys(mapRef); + Expr length = ctx.mkLength(seq); + ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); + ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); + + List boundsAndTypes = new ArrayList<>(); + boundsAndTypes.add(isMap); + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + Expr key = ctx.mkNth(seq, idx); + BoolExpr validIndex = ctx.mkLt(idx, length); + + BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key); + BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key)); + // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in + // map(dyn, ...). For concrete map types, this is already implied by keyType constraints. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError))); + // Short-circuit DYN key types to prevent generating redundant validIndex ⇒ TRUE clauses. + if (!keyType.equals(SimpleType.DYN)) { + boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType))); + } + + BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key); + BoolExpr validEntry = ctx.mkAnd(validIndex, presence); + + Expr mapVal = ctx.mkSelect(mapValues, key); + BoolExpr valNotError = ctx.mkNot(typeSystem.isError(mapVal)); + boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); + // Short-circuit DYN value types to prevent generating redundant validEntry ⇒ TRUE clauses. + if (!valType.equals(SimpleType.DYN)) { + boundsAndTypes.add( + ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); + } + } + + return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type.kind() == CelKind.STRUCT) { return ctx.mkAnd( diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index f7d47635f..f52886a42 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -82,6 +82,10 @@ private static String formatExpr( // Handle CelType constructors wrapper unwrapping if (decl.equals(typeSystem.intCons().ConstructorDecl())) { return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]); + } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) { + return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")"; + } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { + return "duration(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")"; } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) { return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u"; } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) { @@ -123,6 +127,8 @@ private static String formatExpr( return "Error"; } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) { return "Unknown"; + } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) { + return "null"; } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) { Expr optRef = expr.getArgs()[0]; Expr hasValueExpr = diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index effa91c2b..3051fbd87 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -148,11 +148,11 @@ private BoolExpr mkTypeGuard(Expr arg, CelType expectedType) { // These match everything structurally type-wise, although we might refine this later. return ctx.mkTrue(); case INT: + return typeSystem.isInt(arg); case TIMESTAMP: + return typeSystem.isTimestamp(arg); case DURATION: - // Safe to map int, timestamp, and duration to IntSort because CEL's static checker prevents - // invalid cross-type usage and their operator axioms translate to identical Z3 ASTs. - return typeSystem.isInt(arg); + return typeSystem.isDuration(arg); case UINT: return typeSystem.isUint(arg); case DOUBLE: @@ -386,7 +386,7 @@ private BoolExpr getNumericEqualityWithConstant( ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) : ctx.mkFalse(); } else if (symType.kind() == CelKind.DOUBLE) { - return ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); + return ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); } } @@ -396,8 +396,7 @@ private BoolExpr getNumericEqualityWithConstant( (uintVal != null) ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) : ctx.mkFalse(); - BoolExpr doubleEq = - ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); + BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); return (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) @@ -435,18 +434,17 @@ private BoolExpr getStaticallyKnownNumericEquality( case UINT: return ctx.mkEq(typeSystem.getUint(z3Expr0), typeSystem.getUint(z3Expr1)); case DOUBLE: - return ctx.mkFPEq( - (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1)); + return ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1)); default: return ctx.mkFalse(); } } private BoolExpr mkIsFiniteDouble(Expr z3Expr) { - Expr fpVal = typeSystem.getDouble(z3Expr); + FPExpr fpVal = typeSystem.getDouble(z3Expr); return ctx.mkAnd( typeSystem.isDouble(z3Expr), - ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN((FPExpr) fpVal), ctx.mkFPIsInfinite((FPExpr) fpVal)))); + ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN(fpVal), ctx.mkFPIsInfinite(fpVal)))); } private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { @@ -475,25 +473,28 @@ private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { BoolExpr isIntOrUintAndDouble = ctx.mkAnd(isIntOrUint0, typeSystem.isDouble(z3Expr1)); BoolExpr isDoubleAndIntOrUint = ctx.mkAnd(typeSystem.isDouble(z3Expr0), isIntOrUint1); - Expr fpVal1 = typeSystem.getDouble(z3Expr1); + FPExpr fpVal1 = typeSystem.getDouble(z3Expr1); + ArithExpr realVal0 = ctx.mkInt2Real(val0); BoolExpr intDoubleEq = ctx.mkAnd( mkIsFiniteDouble(z3Expr1), - ctx.mkEq(ctx.mkInt2Real(val0), ctx.mkFPToReal((FPExpr) fpVal1))); + ctx.mkLe(realVal0, ctx.mkFPToReal(fpVal1)), + ctx.mkLe(ctx.mkFPToReal(fpVal1), realVal0)); - Expr fpVal0 = typeSystem.getDouble(z3Expr0); + FPExpr fpVal0 = typeSystem.getDouble(z3Expr0); + ArithExpr realVal1 = ctx.mkInt2Real(val1); BoolExpr doubleIntEq = ctx.mkAnd( mkIsFiniteDouble(z3Expr0), - ctx.mkEq(ctx.mkFPToReal((FPExpr) fpVal0), ctx.mkInt2Real(val1))); + ctx.mkLe(realVal1, ctx.mkFPToReal(fpVal0)), + ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1)); return (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) .addCase(bothIntOrUint, ctx.mkEq(val0, val1)) .addCase( bothDouble, - ctx.mkFPEq( - (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1))) + ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1))) .addCase(isIntOrUintAndDouble, intDoubleEq) .addCase(isDoubleAndIntOrUint, doubleIntEq) .build(ctx.mkFalse()); @@ -593,7 +594,8 @@ private TranslatedValue translateEquality( // because X == X is a tautology (or propagates errors/unknowns exactly). if (z3Arg0.equals(z3Arg1)) { Expr finalResult = typeSystem.propagateErrorAndUnknown(equalityExpr, z3Arg0); - return TranslatedValue.create(finalResult, typeSystem, ctx.mkFalse()); + return TranslatedValue.create( + finalResult, typeSystem, ctx.mkOr(arg0.isApproximate(), arg1.isApproximate())); } return TranslatedValue.propagateStrict(ctx, typeSystem, equalityExpr, arg0, arg1) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index af1a4688b..1c1435e3b 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -26,11 +26,13 @@ import com.microsoft.z3.DatatypeSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; +import com.microsoft.z3.FPNum; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.SeqExpr; import com.microsoft.z3.SeqSort; import com.microsoft.z3.Sort; +import dev.cel.common.internal.ProtoTimeUtils; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -82,6 +84,14 @@ public final class CelZ3TypeSystem { private static final String IS_BYTES = "isBytes"; private static final String GET_BYTES = "getBytes"; + private static final String CONS_TIMESTAMP = "Timestamp"; + private static final String IS_TIMESTAMP = "isTimestamp"; + private static final String GET_TIMESTAMP = "getTimestamp"; + + private static final String CONS_DURATION = "Duration"; + private static final String IS_DURATION = "isDuration"; + private static final String GET_DURATION = "getDuration"; + private static final String CONS_ERROR = "CelError"; private static final String IS_ERROR = "isError"; @@ -170,6 +180,8 @@ public int hashCode() { private final Constructor doubleCons; private final Constructor stringCons; private final Constructor bytesCons; + private final Constructor timestampCons; + private final Constructor durationCons; private final Constructor errorCons; private final Constructor unknownCons; private final Constructor nullCons; @@ -233,34 +245,71 @@ public Sort listRefSort() { return listRefSort; } - Constructor boolCons() { + public Constructor boolCons() { return boolCons; } - Constructor intCons() { + public Constructor intCons() { return intCons; } - Constructor uintCons() { + public Constructor uintCons() { return uintCons; } - Constructor doubleCons() { + public Constructor doubleCons() { return doubleCons; } - Constructor stringCons() { + public Constructor stringCons() { return stringCons; } - Constructor bytesCons() { + public Constructor bytesCons() { return bytesCons; } + public Constructor timestampCons() { + return timestampCons; + } + + public Constructor durationCons() { + return durationCons; + } + Constructor optionalCons() { return optionalCons; } + /** + * Checks if the given CelValue expression represents a statically known primitive constant. + * + *

This is useful for determining whether an uninterpreted function's result should be treated + * as an approximation. If the argument is a known constant, any resulting error is an + * approximation (e.g., parsing a literal string). If it's a variable, the error is an exact + * runtime failure. + */ + public boolean isPrimitiveConstant(Expr expr) { + if (!expr.isApp()) { + return false; + } + FuncDecl decl = expr.getFuncDecl(); + if (decl.equals(stringCons.ConstructorDecl()) || decl.equals(bytesCons.ConstructorDecl())) { + return expr.getArgs()[0].isString(); + } else if (decl.equals(intCons.ConstructorDecl()) + || decl.equals(uintCons.ConstructorDecl()) + || decl.equals(timestampCons.ConstructorDecl()) + || decl.equals(durationCons.ConstructorDecl())) { + return expr.getArgs()[0].isNumeral(); + } else if (decl.equals(doubleCons.ConstructorDecl())) { + return expr.getArgs()[0] instanceof FPNum; + } else if (decl.equals(boolCons.ConstructorDecl())) { + Expr inner = expr.getArgs()[0]; + return inner.isTrue() || inner.isFalse(); + } + return false; + } + /** Creates a CelValue containing a boolean. */ public Expr mkBool(boolean val) { return ctx.mkApp(boolCons.ConstructorDecl(), ctx.mkBool(val)); @@ -296,6 +345,16 @@ public Expr wrapBytes(Expr expr) { return ctx.mkApp(bytesCons.ConstructorDecl(), expr); } + /** Wraps a Z3 integer expression into a timestamp CelValue. */ + public Expr wrapTimestamp(IntExpr expr) { + return ctx.mkApp(timestampCons.ConstructorDecl(), expr); + } + + /** Wraps a Z3 integer expression into a duration CelValue. */ + public Expr wrapDuration(IntExpr expr) { + return ctx.mkApp(durationCons.ConstructorDecl(), expr); + } + /** Creates a CelValue containing an integer. */ public Expr mkInt(long val) { return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val)); @@ -326,8 +385,8 @@ public BoolExpr isDouble(Expr val) { } /** Extracts the double reference from a double CelValue. */ - public Expr getDouble(Expr val) { - return ctx.mkApp(doubleCons.getAccessorDecls()[0], val); + public FPExpr getDouble(Expr val) { + return (FPExpr) ctx.mkApp(doubleCons.getAccessorDecls()[0], val); } /** @@ -372,7 +431,7 @@ public BoolExpr getStructuralEquality(Expr arg0, Expr arg1) { // Doubles must be compared using native floating-point equality to follow IEEE-754. // Z3's structural mkEq evaluates NaN == NaN as true and 0.0 == -0.0 as false. BoolExpr isDoubleEq = ctx.mkAnd(isDouble(arg0), isDouble(arg1)); - BoolExpr doubleEq = ctx.mkFPEq((FPExpr) getDouble(arg0), (FPExpr) getDouble(arg1)); + BoolExpr doubleEq = ctx.mkFPEq(getDouble(arg0), getDouble(arg1)); // For primitives, generic equality matches the direct Z3 datatype wrapper. BoolExpr genericEq = ctx.mkEq(arg0, arg1); @@ -409,10 +468,14 @@ public Expr mkNull() { return ctx.mkConst(nullCons.ConstructorDecl()); } - Constructor errorCons() { + public Constructor errorCons() { return errorCons; } + public Constructor nullCons() { + return nullCons; + } + /** Creates a CelValue representing an unknown value. */ public Expr mkUnknown() { return mkUnknown(ctx.mkConst(GENERIC_UNKNOWN_ID, unknownIdSort)); @@ -498,7 +561,7 @@ public Expr withRuntimeError( return ctx.mkITE(condition, mkError(), result); } - Constructor unknownCons() { + public Constructor unknownCons() { return unknownCons; } @@ -582,6 +645,26 @@ public IntExpr getUint(Expr val) { return (IntExpr) ctx.mkApp(uintCons.getAccessorDecls()[0], val); } + /** Checks if the given CelValue is a timestamp. */ + public BoolExpr isTimestamp(Expr val) { + return (BoolExpr) ctx.mkApp(timestampCons.getTesterDecl(), val); + } + + /** Extracts the integer expression from a timestamp CelValue. */ + public IntExpr getTimestamp(Expr val) { + return (IntExpr) ctx.mkApp(timestampCons.getAccessorDecls()[0], val); + } + + /** Checks if the given CelValue is a duration. */ + public BoolExpr isDuration(Expr val) { + return (BoolExpr) ctx.mkApp(durationCons.getTesterDecl(), val); + } + + /** Extracts the integer expression from a duration CelValue. */ + public IntExpr getDuration(Expr val) { + return (IntExpr) ctx.mkApp(durationCons.getAccessorDecls()[0], val); + } + /** Checks if the given CelValue is a string. */ public BoolExpr isString(Expr val) { return (BoolExpr) ctx.mkApp(stringCons.getTesterDecl(), val); @@ -602,6 +685,11 @@ public Expr getBytes(Expr val) { return ctx.mkApp(bytesCons.getAccessorDecls()[0], val); } + /** Checks if the given CelValue is a valid primitive map key type. */ + public BoolExpr isPrimitiveKey(Expr val) { + return ctx.mkOr(isBool(val), isInt(val), isUint(val), isString(val), isBytes(val)); + } + /** Checks if the given CelValue is a struct (message). */ public BoolExpr isStruct(Expr val) { return isMessage(val); @@ -719,6 +807,20 @@ public BoolExpr checkIntOverflow(ArithExpr result) { return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64))); } + /** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */ + public BoolExpr checkTimestampOverflow(ArithExpr result) { + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)), + ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN))); + } + + /** Checks if the given arithmetic expression overflows CEL Duration bounds. */ + public BoolExpr checkDurationOverflow(ArithExpr result) { + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MAX)), + ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MIN))); + } + /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ public BoolExpr checkUintOverflow(ArithExpr result) { return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0))); @@ -890,6 +992,20 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { this.bytesCons = ctx.mkConstructor( CONS_BYTES, IS_BYTES, new String[] {GET_BYTES}, new Sort[] {ctx.getStringSort()}, null); + this.timestampCons = + ctx.mkConstructor( + CONS_TIMESTAMP, + IS_TIMESTAMP, + new String[] {GET_TIMESTAMP}, + new Sort[] {ctx.getIntSort()}, + null); + this.durationCons = + ctx.mkConstructor( + CONS_DURATION, + IS_DURATION, + new String[] {GET_DURATION}, + new Sort[] {ctx.getIntSort()}, + null); this.errorCons = ctx.mkConstructor(CONS_ERROR, IS_ERROR, null, null, null); this.unknownIdSort = ctx.mkUninterpretedSort("UnknownId"); @@ -936,6 +1052,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { this.doubleCons, this.stringCons, this.bytesCons, + this.timestampCons, + this.durationCons, this.errorCons, this.unknownCons, this.optionalCons, diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java index 072f75088..bff6b1edb 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java @@ -14,30 +14,67 @@ package dev.cel.verifier.axioms; +import com.microsoft.z3.ArithExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.SeqExpr; import com.microsoft.z3.Sort; import dev.cel.checker.CelStandardDeclarations.StandardFunction; +import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; +import java.util.function.BiFunction; /** Axiomatization for CEL's addition operator (+). */ final class AddAxiom { + @SuppressWarnings("Immutable") // Actually immutable -- BiFunction just isn't annotated as such. + private static CelZ3FunctionAxiom.BinaryTranslator createAddTranslator( + BiFunction, IntExpr> getLeft, + BiFunction, IntExpr> getRight, + BiFunction> wrapResult, + BiFunction, BoolExpr> overflowChecker) { + return (ctx, ts, sink, l, r) -> { + IntExpr a1 = getLeft.apply(ts, l); + IntExpr a2 = getRight.apply(ts, r); + ArithExpr addition = ctx.mkAdd(a1, a2); + Expr result = wrapResult.apply(ts, (IntExpr) addition); + BoolExpr overflow = overflowChecker.apply(ts, addition); + return Optional.of(ts.withRuntimeError(result, overflow)); + }; + } + static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.ADD.functionDecl()) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.ADD_INT64.celOverloadDecl(), - (ctx, ts, sink, l, r) -> { - IntExpr a1 = ts.getInt(l); - IntExpr a2 = ts.getInt(r); - Expr result = ts.wrapInt((IntExpr) ctx.mkAdd(a1, a2)); - BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2)); - return Optional.of(ts.withRuntimeError(result, overflow)); - }) + createAddTranslator( + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::wrapInt, + CelZ3TypeSystem::checkIntOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.ADD_TIMESTAMP_DURATION.celOverloadDecl(), + createAddTranslator( + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapTimestamp, + CelZ3TypeSystem::checkTimestampOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.ADD_DURATION_TIMESTAMP.celOverloadDecl(), + createAddTranslator( + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::wrapTimestamp, + CelZ3TypeSystem::checkTimestampOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.ADD_DURATION_DURATION.celOverloadDecl(), + createAddTranslator( + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapDuration, + CelZ3TypeSystem::checkDurationOverflow)) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.ADD_UINT64.celOverloadDecl(), (ctx, ts, sink, l, r) -> { @@ -53,9 +90,7 @@ final class AddAxiom { Optional.of( ts.wrapDouble( ctx.mkFPAdd( - ctx.mkFPRoundNearestTiesToEven(), - (FPExpr) ts.getDouble(l), - (FPExpr) ts.getDouble(r))))) + ctx.mkFPRoundNearestTiesToEven(), ts.getDouble(l), ts.getDouble(r))))) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.ADD_STRING.celOverloadDecl(), (ctx, ts, sink, l, r) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java index 2d1129618..06d797d4d 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java @@ -110,8 +110,7 @@ public Builder addUnaryOverloadTranslator( Expr val = res.get(); BoolExpr approx = argApproximations.get(0); if (isApproximated) { - BoolExpr isErrorOrUnknown = ctx.mkOr(ts.isError(val), ts.isUnknown(val)); - approx = (BoolExpr) ctx.mkITE(isErrorOrUnknown, approx, ctx.mkTrue()); + approx = (BoolExpr) ctx.mkITE(ts.isUnknown(val), approx, ctx.mkTrue()); } return Optional.of(CelZ3OverloadResult.create(val, approx)); }; 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 527ef70ad..292b86135 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -32,33 +32,25 @@ final class GreaterAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGt(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGt(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGt(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkGt(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE.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 ec3ffa69a..4be0c23e2 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -32,33 +32,25 @@ final class GreaterEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGe(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGe(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGe(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkGe(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE.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 429aee284..e09484f28 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -32,33 +32,25 @@ final class LessAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLt(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLt(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLt(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkLt(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE.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 5099850dd..e27b47631 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -32,33 +32,25 @@ final class LessEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLe(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLe(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLe(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkLe(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java index bd0ecf882..3bedacf8c 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java @@ -14,27 +14,64 @@ package dev.cel.verifier.axioms; +import com.microsoft.z3.ArithExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.IntExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; +import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; +import java.util.function.BiFunction; /** Axiomatization for CEL's subtraction operator (-). */ final class SubtractAxiom { + @SuppressWarnings("Immutable") // Actually immutable -- BiFunction just isn't annotated as such. + private static CelZ3FunctionAxiom.BinaryTranslator createSubtractTranslator( + BiFunction, IntExpr> getLeft, + BiFunction, IntExpr> getRight, + BiFunction> wrapResult, + BiFunction, BoolExpr> overflowChecker) { + return (ctx, ts, sink, l, r) -> { + IntExpr a1 = getLeft.apply(ts, l); + IntExpr a2 = getRight.apply(ts, r); + ArithExpr subtraction = ctx.mkSub(a1, a2); + Expr result = wrapResult.apply(ts, (IntExpr) subtraction); + BoolExpr overflow = overflowChecker.apply(ts, subtraction); + return Optional.of(ts.withRuntimeError(result, overflow)); + }; + } + static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.SUBTRACT.functionDecl()) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.SUBTRACT_INT64.celOverloadDecl(), - (ctx, ts, sink, l, r) -> { - IntExpr a1 = ts.getInt(l); - IntExpr a2 = ts.getInt(r); - Expr result = ts.wrapInt((IntExpr) ctx.mkSub(a1, a2)); - BoolExpr overflow = ts.checkIntOverflow(ctx.mkSub(a1, a2)); - return Optional.of(ts.withRuntimeError(result, overflow)); - }) + createSubtractTranslator( + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::wrapInt, + CelZ3TypeSystem::checkIntOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.SUBTRACT_TIMESTAMP_TIMESTAMP.celOverloadDecl(), + createSubtractTranslator( + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::wrapDuration, + CelZ3TypeSystem::checkDurationOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.SUBTRACT_TIMESTAMP_DURATION.celOverloadDecl(), + createSubtractTranslator( + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapTimestamp, + CelZ3TypeSystem::checkTimestampOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.SUBTRACT_DURATION_DURATION.celOverloadDecl(), + createSubtractTranslator( + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapDuration, + CelZ3TypeSystem::checkDurationOverflow)) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.SUBTRACT_UINT64.celOverloadDecl(), (ctx, ts, sink, l, r) -> { @@ -50,9 +87,7 @@ final class SubtractAxiom { Optional.of( ts.wrapDouble( ctx.mkFPSub( - ctx.mkFPRoundNearestTiesToEven(), - (FPExpr) ts.getDouble(l), - (FPExpr) ts.getDouble(r))))) + ctx.mkFPRoundNearestTiesToEven(), ts.getDouble(l), ts.getDouble(r))))) .build(); private SubtractAxiom() {} diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java index fc4757686..9c49ef958 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java @@ -61,6 +61,8 @@ private static Expr getTypeExpression(Context ctx, CelZ3TypeSystem typeSystem typeSystem.wrapString(typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)))) .addCase(typeSystem.isOptional(val), typeSystem.mkString(OptionalType.NAME)) .addCase(typeSystem.isNull(val), typeSystem.mkString(SimpleType.NULL_TYPE.name())) + .addCase(typeSystem.isTimestamp(val), typeSystem.mkString(SimpleType.TIMESTAMP.name())) + .addCase(typeSystem.isDuration(val), typeSystem.mkString(SimpleType.DURATION.name())) .addCase(typeSystem.isMap(val), typeSystem.mkString(TYPE_NAME_MAP)) .addCase(typeSystem.isList(val), typeSystem.mkString(TYPE_NAME_LIST)) .addCase(typeSystem.isBytes(val), typeSystem.mkString(SimpleType.BYTES.name())) diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index 94bdf0651..8cd844214 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -25,6 +25,7 @@ import com.microsoft.z3.Sort; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions; +import dev.cel.common.types.SimpleType; import java.util.Optional; /** Axiomatization for CEL's type conversion functions. */ @@ -43,18 +44,16 @@ final class TypeConversionAxioms { return Optional.of( typeSystem.withRuntimeError(typeSystem.wrapInt(uintVal), outOfBounds)); }) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.DOUBLE_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_INT64), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_INT64)) + .addOverloadTranslator( Conversions.STRING_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_INT64), - true) + createUninterpretedConversion(Conversions.STRING_TO_INT64)) .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.TIMESTAMP_TO_INT64), - true) + (ctx, typeSystem, sink, arg) -> + Optional.of(typeSystem.wrapInt(typeSystem.getTimestamp(arg)))) .build(); private static final CelZ3FunctionAxiom UINT_AXIOM = @@ -70,14 +69,12 @@ final class TypeConversionAxioms { return Optional.of( typeSystem.withRuntimeError(typeSystem.wrapUint(intVal), outOfBounds)); }) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.DOUBLE_TO_UINT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64)) + .addOverloadTranslator( Conversions.STRING_TO_UINT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_UINT64), - true) + createUninterpretedConversion(Conversions.STRING_TO_UINT64)) .build(); private static final CelZ3FunctionAxiom DOUBLE_AXIOM = @@ -85,15 +82,13 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DOUBLE_TO_DOUBLE.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.INT64_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_DOUBLE), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.INT64_TO_DOUBLE)) + .addOverloadTranslator( Conversions.UINT64_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE)) + .addOverloadTranslator( Conversions.STRING_TO_DOUBLE.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_DOUBLE)) .build(); @@ -103,34 +98,27 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_STRING.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.INT64_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.INT64_TO_STRING)) + .addOverloadTranslator( Conversions.UINT64_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.UINT64_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.UINT64_TO_STRING)) + .addOverloadTranslator( Conversions.DOUBLE_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_STRING)) + .addOverloadTranslator( Conversions.BOOL_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.BOOL_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.BOOL_TO_STRING)) + .addOverloadTranslator( Conversions.BYTES_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.BYTES_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.BYTES_TO_STRING)) + .addOverloadTranslator( Conversions.TIMESTAMP_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING)) + .addOverloadTranslator( Conversions.DURATION_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.DURATION_TO_STRING), - true) + createUninterpretedConversion(Conversions.DURATION_TO_STRING)) .build(); private static final CelZ3FunctionAxiom BYTES_AXIOM = @@ -138,10 +126,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.BYTES_TO_BYTES.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_BYTES.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_BYTES), - true) + createUninterpretedConversion(Conversions.STRING_TO_BYTES)) .build(); private static final CelZ3FunctionAxiom DYN_AXIOM = @@ -156,10 +143,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DURATION_TO_DURATION.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_DURATION.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_DURATION), - true) + createUninterpretedConversion(Conversions.STRING_TO_DURATION)) .build(); private static final CelZ3FunctionAxiom TIMESTAMP_AXIOM = @@ -167,14 +153,17 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_TIMESTAMP.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP), - true) + createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP)) .addUnaryOverloadTranslator( Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_TIMESTAMP), - true) + (ctx, typeSystem, sink, arg) -> { + IntExpr intVal = typeSystem.getInt(arg); + BoolExpr overflow = typeSystem.checkTimestampOverflow(intVal); + return Optional.of( + typeSystem.withRuntimeError(typeSystem.wrapTimestamp(intVal), overflow)); + }) .build(); private static final CelZ3FunctionAxiom BOOL_AXIOM = @@ -182,10 +171,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.BOOL_TO_BOOL.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_BOOL.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_BOOL), - true) + createUninterpretedConversion(Conversions.STRING_TO_BOOL)) .build(); static final ImmutableList ALL_AXIOMS = @@ -200,9 +188,11 @@ final class TypeConversionAxioms { TIMESTAMP_AXIOM, BOOL_AXIOM); - private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( - Conversions conversion) { - return (ctx, typeSystem, sink, arg) -> { + private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions conversion) { + return (ctx, typeSystem, sink, unwrappedArgs, argApproximations) -> { + Expr arg = unwrappedArgs.get(0); + BoolExpr baseApprox = argApproximations.get(0); + FuncDecl funcDecl = typeSystem.internFuncDecl( conversion.celOverloadDecl().overloadId(), @@ -212,32 +202,63 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( switch (conversion.celOverloadDecl().resultType().kind()) { case INT: + sink.accept(ctx.mkOr(typeSystem.isInt(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isInt(res), + ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res))))); + break; case TIMESTAMP: + sink.accept(ctx.mkOr(typeSystem.isTimestamp(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isTimestamp(res), + ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res))))); + break; case DURATION: - sink.accept(typeSystem.isInt(res)); - sink.accept(ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))); + sink.accept(ctx.mkOr(typeSystem.isDuration(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isDuration(res), + ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res))))); break; case UINT: - sink.accept(typeSystem.isUint(res)); - sink.accept(ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))); + sink.accept(ctx.mkOr(typeSystem.isUint(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isUint(res), + ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res))))); break; case DOUBLE: - sink.accept(typeSystem.isDouble(res)); - sink.accept(ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res)))); + sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isDouble(res), + ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res))))); break; case STRING: - sink.accept(typeSystem.isString(res)); + sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res))); break; case BYTES: - sink.accept(typeSystem.isBytes(res)); + sink.accept(ctx.mkOr(typeSystem.isBytes(res), typeSystem.isError(res))); break; case BOOL: - sink.accept(typeSystem.isBool(res)); + sink.accept(ctx.mkOr(typeSystem.isBool(res), typeSystem.isError(res))); break; default: - break; + throw new IllegalArgumentException( + "Unsupported uninterpreted conversion result type: " + + conversion.celOverloadDecl().resultType()); } - return Optional.of(res); + + boolean isArgConstant = typeSystem.isPrimitiveConstant(arg); + boolean isStringParseConversion = + conversion.celOverloadDecl().parameterTypes().get(0).equals(SimpleType.STRING); + + BoolExpr finalApprox = + (!isArgConstant && isStringParseConversion) ? baseApprox : ctx.mkTrue(); + + return Optional.of(CelZ3OverloadResult.create(res, finalApprox)); }; } diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..28ce776cb --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,80 @@ +load("@rules_java//java:defs.bzl", "java_binary", "java_library") +load("//publish:cel_version.bzl", "CEL_VERSION") + +package( + default_applicable_licenses = [ + "//:license", + ], + default_visibility = [ + "//verifier:__subpackages__", + ], +) + +genrule( + name = "generate_version", + outs = ["CelVersion.java"], + cmd = """cat << 'EOF' > $@ +package dev.cel.verifier.tools; + +final class CelVersion { + static final String VERSION = "%s"; + + private CelVersion() {} +} +EOF +""" % CEL_VERSION, +) + +java_library( + name = "tools_lib", + srcs = [ + "CelVerifierRepl.java", + "CelVerifierTool.java", + "CelVerifierToolCore.java", + "FormatUtils.java", + "VerificationOptions.java", + ":generate_version", + ], + tags = [ + "alt_dep=//verifier/tools", + ], + deps = [ + "//:java_jline", + "//bundle:cel", + "//common:cel_ast", + "//common:compiler_common", + "//common:options", + "//common/types", + "//common/types:cel_types", + "//common/types:type_providers", + "//compiler", + "//compiler:compiler_builder", + "//extensions", + "//parser:macro", + "//policy", + "//policy:compiler", + "//policy:compiler_factory", + "//policy:parser", + "//policy:parser_factory", + "//policy:validation_exception", + "//verifier", + "//verifier:policy_verifier", + "//verifier:policy_verifier_factory", + "//verifier:verifier_factory", + "@maven//:com_google_errorprone_error_prone_annotations", + "@maven//:com_google_guava_guava", + "@maven//:info_picocli_picocli", + ], +) + +java_binary( + name = "cel_verifier_tool", + jvm_flags = ["-Dz3.skipLibraryLoad=true"], + main_class = "dev.cel.verifier.tools.CelVerifierTool", + tags = [ + "alt_dep=//verifier/tools:cel_verifier_tool", + ], + runtime_deps = [ + ":tools_lib", + ], +) diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java new file mode 100644 index 000000000..25354480a --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -0,0 +1,435 @@ +// 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.tools; + +import static java.nio.charset.StandardCharsets.UTF_8; + +import com.google.common.base.Ascii; +import com.google.common.collect.ImmutableList; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.common.types.CelTypes; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import java.io.BufferedReader; +import java.io.InputStreamReader; +import java.io.PrintStream; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.Optional; +import org.jline.reader.EndOfFileException; +import org.jline.reader.LineReader; +import org.jline.reader.LineReaderBuilder; +import org.jline.reader.UserInterruptException; +import org.jline.terminal.Terminal; +import org.jline.terminal.TerminalBuilder; + +/** Interactive REPL shell for CEL formal verification. */ +final class CelVerifierRepl { + + private CelVerifierRepl() {} + + static int runInteractiveRepl() { + LineReader lineReader = null; + BufferedReader fallbackReader = null; + try { + Terminal terminal = TerminalBuilder.builder().system(true).build(); + lineReader = LineReaderBuilder.builder().terminal(terminal).build(); + } catch (Exception e) { + fallbackReader = new BufferedReader(new InputStreamReader(System.in, UTF_8)); + } + return runReplInternal(lineReader, fallbackReader, System.out, System.err); + } + + static int runRepl(BufferedReader reader, PrintStream out, PrintStream err) { + return runReplInternal(null, reader, out, err); + } + + private static int runReplInternal( + LineReader lineReader, BufferedReader fallbackReader, PrintStream out, PrintStream err) { + out.println("============================================================"); + out.println(" CEL Verification REPL"); + out.println(" Type :help for commands, :quit to exit."); + out.println("============================================================"); + + Map sessionVars = new HashMap<>(); + List unknownIdentifiers = new ArrayList<>(); + int timeoutSeconds = 10; + int unrollLimit = 5; + + String prompt = FormatUtils.ANSI_CYAN + "cel-verifier> " + FormatUtils.ANSI_RESET; + + while (true) { + String line; + try { + if (lineReader != null) { + line = lineReader.readLine(prompt); + } else if (fallbackReader != null) { + out.print(prompt); + out.flush(); + line = fallbackReader.readLine(); + if (line == null) { + break; // EOF + } + } else { + break; + } + } catch (UserInterruptException | EndOfFileException e) { + out.println("Goodbye!"); + break; + } catch (Exception e) { + err.println("Error reading input: " + e.getMessage()); + break; + } + + line = line.trim(); + if (line.isEmpty()) { + continue; + } + + if (line.startsWith(":")) { + if (Ascii.equalsIgnoreCase(line, ":quit") || Ascii.equalsIgnoreCase(line, ":exit")) { + out.println("Goodbye!"); + break; + } + + Optional helpArg = extractCommandArg(line, ":help"); + if (helpArg.isPresent()) { + printHelp(helpArg.get(), out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":vars")) { + printVars(sessionVars, unknownIdentifiers, timeoutSeconds, unrollLimit, out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":clear")) { + sessionVars.clear(); + unknownIdentifiers.clear(); + out.println("Session state reset."); + continue; + } + + Optional varArg = extractCommandArg(line, ":var"); + if (varArg.isPresent()) { + String arg = varArg.get(); + if (arg.isEmpty()) { + err.println( + "Usage: :var (e.g. :var role string, :var scores map)"); + } else { + handleVarCommand(arg, sessionVars, out, err); + } + continue; + } + + Optional unknownArg = extractCommandArg(line, ":unknown"); + if (unknownArg.isPresent()) { + String arg = unknownArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unknown "); + } else { + unknownIdentifiers.add(arg); + out.println("Added unknown identifier: '" + arg + "'"); + } + continue; + } + + Optional timeoutArg = extractCommandArg(line, ":timeout"); + if (timeoutArg.isPresent()) { + String arg = timeoutArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :timeout "); + } else { + try { + int t = Integer.parseInt(arg); + if (t <= 0) { + err.println("Timeout must be a positive integer."); + } else { + timeoutSeconds = t; + out.println("Timeout set to " + timeoutSeconds + "s."); + } + } catch (NumberFormatException e) { + err.println("Invalid timeout value."); + } + } + continue; + } + + Optional unrollArg = extractCommandArg(line, ":unroll"); + if (unrollArg.isPresent()) { + String arg = unrollArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unroll "); + } else { + try { + int u = Integer.parseInt(arg); + if (u < 0) { + err.println("Unroll limit must be non-negative."); + } else { + unrollLimit = u; + out.println("Comprehension unroll limit set to " + unrollLimit + "."); + } + } catch (NumberFormatException e) { + err.println("Invalid unroll limit value."); + } + } + continue; + } + + err.println("Unknown command: " + line + ". Type :help for commands."); + continue; + } + + // Handle queries + VerificationOptions options = + VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(unrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .build(); + + try { + Optional satArg = extractCommandArg(line, "sat"); + Optional validArg = extractCommandArg(line, "valid"); + Optional equivArg = extractCommandArg(line, "equiv"); + + if (satArg.isPresent()) { + String arg = satArg.get(); + if (arg.isEmpty()) { + err.println("Usage: sat "); + } else { + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (validArg.isPresent()) { + String arg = validArg.get(); + if (arg.isEmpty()) { + err.println("Usage: valid "); + } else { + CelVerificationResult res = CelVerifierToolCore.checkValid(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (equivArg.isPresent()) { + String arg = equivArg.get(); + ImmutableList parts = splitEquivQuery(arg); + if (parts.size() != 2 || parts.get(0).isEmpty() || parts.get(1).isEmpty()) { + err.println("Equivalence query format: equiv <=> "); + } else { + String exprA = parts.get(0).trim(); + String exprB = parts.get(1).trim(); + CelVerificationResult res = + CelVerifierToolCore.verifyEquivalence(exprA, exprB, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else { + // Default: treat as sat query + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(line, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } catch (CelValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (CelPolicyValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Policy compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (Exception e) { + err.println( + FormatUtils.ANSI_RED + + "Verification failed: " + + e.getMessage() + + FormatUtils.ANSI_RESET); + } + } + return 0; + } + + private static void handleVarCommand( + String arg, Map sessionVars, PrintStream out, PrintStream err) { + String[] parts = arg.split("\\s+", 2); + if (parts.length != 2) { + err.println("Usage: :var (e.g. :var role string, :var scores map)"); + return; + } + String name = parts[0].trim(); + String typeStr = parts[1].trim(); + try { + CelType type = VerificationOptions.parseCelType(typeStr); + sessionVars.put(name, type); + out.println("Variable declared: " + name + " : " + CelTypes.format(type)); + } catch (IllegalArgumentException e) { + err.println(e.getMessage()); + } + } + + private static void printVars( + Map sessionVars, + List unknowns, + int timeoutSeconds, + int unrollLimit, + PrintStream out) { + out.println("--- Session State ---"); + out.println("Timeout: " + timeoutSeconds + "s | Unroll limit: " + unrollLimit); + out.println("Unknowns: " + (unknowns.isEmpty() ? "none" : unknowns)); + out.println("Variables (" + sessionVars.size() + "):"); + for (Map.Entry entry : sessionVars.entrySet()) { + out.println(" " + entry.getKey() + " : " + CelTypes.format(entry.getValue())); + } + } + + private static void printHelp(String topic, PrintStream out) { + String t = topic.toLowerCase(Locale.US).replace(":", "").trim(); + switch (t) { + case "var": + case "vars": + out.println("Command: :var "); + out.println("Declares a variable in the REPL session with a specific type."); + out.println(); + out.println("Supported Types:"); + out.println(" - Primitive types: int, uint, string, bool, double, bytes"); + out.println(" - List types: list (e.g., list, list)"); + out.println(" - Map types: map (e.g., map, map)"); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :var role string"); + out.println(" cel-verifier> :var port int"); + out.println(" cel-verifier> :var scores map"); + out.println(" cel-verifier> :var tags list"); + break; + case "unknown": + out.println("Command: :unknown "); + out.println( + "Marks an identifier path as 'Unknown' during verification (partial evaluation)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unknown request.headers"); + out.println(" cel-verifier> :unknown request.auth.claims"); + break; + case "timeout": + out.println("Command: :timeout "); + out.println("Configures the Z3 solver soft timeout duration in seconds (default: 10s)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :timeout 5"); + break; + case "unroll": + out.println("Command: :unroll "); + out.println("Configures the BMC loop unroll limit for comprehensions (default: 5)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unroll 3"); + break; + case "sat": + out.println("Query: sat "); + out.println( + "Checks if a CEL expression can evaluate to true for any possible input assignments."); + out.println("If satisfiable, outputs concrete satisfying witness values."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> sat role == 'editor' && port > 1024"); + out.println(" cel-verifier> sat scores['alice'] > 90"); + break; + case "valid": + out.println("Query: valid "); + out.println( + "Proves whether a CEL expression evaluates to true for ALL possible input" + + " assignments."); + out.println("If invalid, outputs a counterexample showing inputs causing it to fail."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> valid x > 10 || x <= 10"); + break; + case "equiv": + out.println("Query: equiv <=> "); + out.println( + "Proves whether two CEL expressions are semantically identical for all inputs."); + out.println( + "If not equivalent, outputs a counterexample showing inputs where they diverge."); + out.println(); + out.println("Use '<=>' as the recommended separator between expressions."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> equiv x > 10 <=> 10 < x"); + out.println(" cel-verifier> equiv (a && b) || (a && c) <=> a && (b || c)"); + out.println( + " cel-verifier> equiv string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k ==" + + " 'a') : true <=> string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k ==" + + " 'a') : true"); + break; + default: + out.println("REPL Commands:"); + out.println( + " :var Declare variable (e.g. :var role string, :var m" + + " map)"); + out.println(" :unknown Mark identifier as unknown"); + out.println(" :timeout Set solver timeout (default: 10s)"); + out.println(" :unroll Set comprehension unroll limit (default: 5)"); + out.println(" :vars List session variables & options"); + out.println(" :clear Reset session state"); + out.println( + " :help [command] Display help message or specific command details"); + out.println(" :quit Exit REPL"); + out.println(); + out.println("Verification Queries:"); + out.println(" sat Check satisfiability"); + out.println(" valid Check validity (always true)"); + out.println(" equiv <=> Prove logical equivalence"); + out.println(" Check satisfiability (default)"); + out.println(); + out.println( + "Type ':help ' (e.g. ':help var', ':help sat') for detailed usage and" + + " examples."); + break; + } + } + + private static ImmutableList splitEquivQuery(String rest) { + if (rest == null || rest.trim().isEmpty()) { + return ImmutableList.of(); + } + String input = rest.trim(); + if (input.contains(" <=> ")) { + return ImmutableList.copyOf(input.split(" <=> ", 2)); + } + if (input.contains("<=>")) { + return ImmutableList.copyOf(input.split("<=>", 2)); + } + return ImmutableList.of(); + } + + private static Optional extractCommandArg(String line, String prefix) { + if (Ascii.equalsIgnoreCase(line, prefix)) { + return Optional.of(""); + } + String prefixLower = Ascii.toLowerCase(prefix); + String lineLower = Ascii.toLowerCase(line); + if (lineLower.startsWith(prefixLower + " ") || lineLower.startsWith(prefixLower + "\t")) { + return Optional.of(line.substring(prefix.length()).trim()); + } + return Optional.empty(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java new file mode 100644 index 000000000..963e966eb --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java @@ -0,0 +1,313 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import dev.cel.verifier.tools.VerificationOptions.OutputFormat; +import java.io.File; +import java.io.OutputStreamWriter; +import java.io.PrintWriter; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.ArrayList; +import java.util.List; +import java.util.Locale; +import java.util.concurrent.Callable; +import picocli.CommandLine; +import picocli.CommandLine.Command; +import picocli.CommandLine.IVersionProvider; +import picocli.CommandLine.Model.CommandSpec; +import picocli.CommandLine.Option; +import picocli.CommandLine.Spec; + +/** Main Picocli entrypoint for the CEL Formal Verification CLI. */ +@Command( + name = "cel-verifier", + mixinStandardHelpOptions = true, + versionProvider = CelVerifierTool.VersionProvider.class, + description = "CEL-Java Formal Verification CLI & REPL Tool", + subcommands = { + CelVerifierTool.CheckSatCommand.class, + CelVerifierTool.CheckValidCommand.class, + CelVerifierTool.VerifyEquivCommand.class, + CelVerifierTool.VerifyPolicyCommand.class, + CelVerifierTool.ReplCommand.class + }) +public final class CelVerifierTool implements Runnable { + + static final int EXIT_CODE_VERIFIED = 0; + static final int EXIT_CODE_VIOLATED = 1; + static final int EXIT_CODE_INCONCLUSIVE = 2; + static final int EXIT_CODE_ERROR = 3; + + static final class VersionProvider implements IVersionProvider { + @Override + public String[] getVersion() { + return new String[] {"cel-verifier " + CelVersion.VERSION}; + } + } + + @Spec private CommandSpec spec; + + @Override + public void run() { + spec.commandLine().usage(spec.commandLine().getOut()); + } + + /** Options shared across all verification commands. */ + abstract static class BaseVerificationCommand implements Callable { + + @Spec private CommandSpec spec; + + PrintWriter out() { + return spec != null + ? spec.commandLine().getOut() + : new PrintWriter(new OutputStreamWriter(System.out, StandardCharsets.UTF_8), true); + } + + PrintWriter err() { + return spec != null + ? spec.commandLine().getErr() + : new PrintWriter(new OutputStreamWriter(System.err, StandardCharsets.UTF_8), true); + } + + @Option( + names = {"--var", "-v"}, + description = + "Declared variable in 'name:type' format (e.g., --var role:string --var port:int)") + List variables = new ArrayList<>(); + + @Option( + names = {"--unknown", "-u"}, + description = + "Identifier to permit evaluating to Unknown (e.g., --unknown request.headers)") + List unknownIdentifiers = new ArrayList<>(); + + @Option( + names = {"--timeout"}, + description = "Solver timeout in seconds (default: 10)") + int timeoutSeconds = (int) VerificationOptions.DEFAULT_TIMEOUT.getSeconds(); + + @Option( + names = {"--unroll-limit"}, + description = "Comprehension unroll limit for BMC (default: 5)") + int comprehensionUnrollLimit = VerificationOptions.DEFAULT_COMPREHENSION_UNROLL_LIMIT; + + @Option( + names = {"--output_format", "-fmt"}, + description = "Output format: TEXT or JSON (default: TEXT)") + String outputFormatStr = VerificationOptions.DEFAULT_OUTPUT_FORMAT.name(); + + @FunctionalInterface + protected interface CommandAction { + int execute(VerificationOptions options, ImmutableMap vars) throws Exception; + } + + protected int executeCommand(CommandAction action) { + return executeCommand("Verification error", action); + } + + protected int executeCommand(String errorPrefix, CommandAction action) { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + return action.execute(options, vars); + } catch (CelValidationException e) { + err().println("Compilation error:\n" + e.getMessage()); + return EXIT_CODE_ERROR; + } catch (CelPolicyValidationException e) { + err().println("Policy compilation error:\n" + e.getMessage()); + return EXIT_CODE_ERROR; + } catch (Exception e) { + err().println(errorPrefix + ": " + e.getMessage()); + return EXIT_CODE_ERROR; + } + } + + protected VerificationOptions getOptions() { + OutputFormat format = OutputFormat.TEXT; + try { + format = OutputFormat.valueOf(outputFormatStr.toUpperCase(Locale.US)); + } catch (IllegalArgumentException e) { + err().println("Invalid output format '" + outputFormatStr + "'. Defaulting to TEXT."); + } + return VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(comprehensionUnrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .setOutputFormat(format) + .build(); + } + + protected int handleSingleResult(CelVerificationResult result, OutputFormat format) { + if (format == OutputFormat.JSON) { + out().println(FormatUtils.formatJsonResult(result)); + } else { + out().println(FormatUtils.formatTextResult(result)); + } + + if (result.status() == VerificationStatus.VERIFIED) { + return EXIT_CODE_VERIFIED; + } else if (result.status() == VerificationStatus.VIOLATED) { + return EXIT_CODE_VIOLATED; + } else { + return EXIT_CODE_INCONCLUSIVE; + } + } + } + + /** Base command for commands operating on a single CEL expression. */ + abstract static class SingleExpressionCommand extends BaseVerificationCommand { + @Option( + names = {"--expr", "-e"}, + required = true, + description = "CEL expression string to verify") + String expression = ""; + } + + @Command( + name = "check-sat", + description = "Verify satisfiability of a CEL expression & generate witness model") + static class CheckSatCommand extends SingleExpressionCommand { + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.checkSatisfiable(expression, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "check-valid", + description = "Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample") + static class CheckValidCommand extends SingleExpressionCommand { + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.checkValid(expression, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "verify-equiv", + description = "Prove logical equivalence between two CEL expressions") + static class VerifyEquivCommand extends BaseVerificationCommand { + + @Option( + names = {"--expr1"}, + required = true, + description = "First CEL expression") + String expressionA = ""; + + @Option( + names = {"--expr2"}, + required = true, + description = "Second CEL expression") + String expressionB = ""; + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.verifyEquivalence(expressionA, expressionB, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "verify-policy", + description = "Verify policy invariants defined in a YAML policy file") + static class VerifyPolicyCommand extends BaseVerificationCommand { + + @Option( + names = {"--file", "-f"}, + required = true, + description = "Path to policy YAML file") + String filePath = ""; + + @Override + public Integer call() { + return executeCommand( + "Policy verification error", + (options, vars) -> { + File file = new File(filePath); + if (!file.exists()) { + err().println("File not found: " + filePath); + return EXIT_CODE_ERROR; + } + String yamlContent = + new String(Files.readAllBytes(file.toPath()), StandardCharsets.UTF_8); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlContent, vars, options); + + if (options.getOutputFormat() == OutputFormat.JSON) { + out().println(FormatUtils.formatJsonPolicyResults(file.getName(), results)); + } else { + out().println(FormatUtils.formatTextPolicyResults(file.getName(), results)); + } + + return getPolicyExitCode(results); + }); + } + + private static int getPolicyExitCode(ImmutableMap results) { + boolean anyViolated = false; + boolean anyInconclusive = false; + for (CelVerificationResult res : results.values()) { + if (res.status() == VerificationStatus.VIOLATED) { + anyViolated = true; + } else if (res.status() == VerificationStatus.INCONCLUSIVE) { + anyInconclusive = true; + } + } + + if (anyViolated) { + return EXIT_CODE_VIOLATED; + } else if (anyInconclusive) { + return EXIT_CODE_INCONCLUSIVE; + } + return EXIT_CODE_VERIFIED; + } + } + + @Command(name = "repl", description = "Launch interactive CEL Formal Verification REPL shell") + static class ReplCommand implements Callable { + + @Override + public Integer call() { + return CelVerifierRepl.runInteractiveRepl(); + } + } + + public static void main(String[] args) { + int exitCode = new CommandLine(new CelVerifierTool()).execute(args); + System.exit(exitCode); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java new file mode 100644 index 000000000..75fa5b635 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -0,0 +1,165 @@ +// Copyright 2026 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +package dev.cel.verifier.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelBuilder; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelOptions; +import dev.cel.common.types.CelType; +import dev.cel.compiler.CelCompiler; +import dev.cel.compiler.CelCompilerBuilder; +import dev.cel.compiler.CelCompilerFactory; +import dev.cel.extensions.CelExtensions; +import dev.cel.parser.CelStandardMacro; +import dev.cel.policy.CelPolicy; +import dev.cel.policy.CelPolicyCompiler; +import dev.cel.policy.CelPolicyCompilerFactory; +import dev.cel.policy.CelPolicyParser; +import dev.cel.policy.CelPolicyParserFactory; +import dev.cel.verifier.CelPolicyVerifier; +import dev.cel.verifier.CelPolicyVerifierFactory; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerifier; +import dev.cel.verifier.CelVerifierBuilder; +import dev.cel.verifier.CelVerifierFactory; +import java.util.Map; + +/** Core decoupled engine that executes formal verification operations. */ +final class CelVerifierToolCore { + + private CelVerifierToolCore() {} + + /** Checks if a single CEL expression is satisfiable. */ + static CelVerificationResult checkSatisfiable( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.isSatisfiable(ast); + } + + /** Checks if a single CEL expression is valid (always true). */ + static CelVerificationResult checkValid( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.isAlwaysTrue(ast); + } + + /** Proves logical equivalence between two CEL expressions. */ + static CelVerificationResult verifyEquivalence( + String expressionA, + String expressionB, + Map variables, + VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree astA = compiler.compile(expressionA).getAst(); + CelAbstractSyntaxTree astB = compiler.compile(expressionB).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.verifyEquivalence(astA, astB); + } + + /** Verifies custom invariants in a YAML policy content string. */ + static ImmutableMap verifyPolicyInvariants( + String yamlContent, Map variables, VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policy = parser.parse(yamlContent); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyInvariants(policy); + } + + /** Verifies equivalence between two YAML policy content strings. */ + static CelVerificationResult verifyPolicyEquivalence( + String yamlContentA, + String yamlContentB, + Map variables, + VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policyA = parser.parse(yamlContentA); + CelPolicy policyB = parser.parse(yamlContentB); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyEquivalence(policyA, policyB); + } + + static CelCompiler buildCompiler(Map variables) { + CelCompilerBuilder builder = + CelCompilerFactory.standardCelCompilerBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addLibraries( + CelExtensions.bindings(), + CelExtensions.comprehensions(), + CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.lists(), + CelExtensions.math(), + CelExtensions.optional(), + CelExtensions.protos(), + CelExtensions.regex(), + CelExtensions.sets(CelOptions.DEFAULT), + CelExtensions.strings()); + if (variables != null) { + for (Map.Entry entry : variables.entrySet()) { + builder.addVar(entry.getKey(), entry.getValue()); + } + } + 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) { + CelBuilder celBuilder = + CelFactory.plannerCelBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addCompilerLibraries( + CelExtensions.optional(), + CelExtensions.bindings(), + CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.math(), + CelExtensions.strings()); + if (variables != null) { + for (Map.Entry entry : variables.entrySet()) { + celBuilder.addVar(entry.getKey(), entry.getValue()); + } + } + Cel celBundle = celBuilder.build(); + CelPolicyCompiler policyCompiler = + CelPolicyCompilerFactory.newPolicyCompiler(celBundle).build(); + CelVerifier astVerifier = buildVerifier(options); + + return CelPolicyVerifierFactory.newVerifier(policyCompiler, astVerifier).build(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java new file mode 100644 index 000000000..d1666cd55 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java @@ -0,0 +1,146 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.util.Map; + +/** Utilities for formatting verification output (ANSI text & JSON). */ +final class FormatUtils { + + // ANSI Escape Codes for formatting text + static final String ANSI_RESET = "\u001B[0m"; + static final String ANSI_BOLD = "\u001B[1m"; + static final String ANSI_GREEN = "\u001B[32m"; + static final String ANSI_RED = "\u001B[31m"; + static final String ANSI_YELLOW = "\u001B[33m"; + static final String ANSI_CYAN = "\u001B[36m"; + + private FormatUtils() {} + + /** Formats a single CelVerificationResult for human-readable console display with ANSI color. */ + static String formatTextResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + String statusColor = getStatusColor(result.status()); + sb.append(statusColor) + .append(ANSI_BOLD) + .append("[") + .append(result.status()) + .append("]") + .append(ANSI_RESET); + + if (result.message() != null && !result.message().isEmpty()) { + sb.append(" ").append(result.message()); + } + + return sb.toString(); + } + + /** Formats policy invariant verification results for human-readable console display. */ + static String formatTextPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append(ANSI_BOLD) + .append("Policy Invariant Verification for '") + .append(policyName) + .append("':\n") + .append(ANSI_RESET); + + for (Map.Entry entry : results.entrySet()) { + String id = entry.getKey(); + CelVerificationResult result = entry.getValue(); + String symbol = result.status() == VerificationStatus.VERIFIED ? "✓" : "✗"; + String color = getStatusColor(result.status()); + + sb.append(" ") + .append(color) + .append(symbol) + .append(" Invariant '") + .append(id) + .append("': ") + .append(result.status()) + .append(ANSI_RESET); + + if (result.message() != null && !result.message().isEmpty()) { + sb.append("\n ").append(result.message().replace("\n", "\n ")); + } + sb.append("\n"); + } + return sb.toString().trim(); + } + + /** Formats a single CelVerificationResult as structured JSON. */ + static String formatJsonResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"status\": \"").append(result.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(result.message())).append("\"\n"); + sb.append("}"); + return sb.toString(); + } + + /** Formats policy invariant verification results as structured JSON. */ + static String formatJsonPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"policyName\": \"").append(escapeJson(policyName)).append("\",\n"); + sb.append(" \"invariants\": [\n"); + + int count = 0; + for (Map.Entry entry : results.entrySet()) { + count++; + String id = entry.getKey(); + CelVerificationResult res = entry.getValue(); + sb.append(" {\n"); + sb.append(" \"id\": \"").append(escapeJson(id)).append("\",\n"); + sb.append(" \"status\": \"").append(res.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(res.message())).append("\"\n"); + sb.append(" }").append(count < results.size() ? "," : "").append("\n"); + } + + sb.append(" ]\n"); + sb.append("}"); + return sb.toString(); + } + + private static String getStatusColor(VerificationStatus status) { + switch (status) { + case VERIFIED: + return ANSI_GREEN; + case VIOLATED: + return ANSI_RED; + case INCONCLUSIVE: + return ANSI_YELLOW; + } + return ANSI_RESET; + } + + private static String escapeJson(String input) { + if (input == null) { + return ""; + } + return input + .replace("\\", "\\\\") + .replace("\"", "\\\"") + .replace("\b", "\\b") + .replace("\f", "\\f") + .replace("\n", "\\n") + .replace("\r", "\\r") + .replace("\t", "\\t"); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java new file mode 100644 index 000000000..f2b3bf742 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -0,0 +1,223 @@ +// 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.tools; + +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; + +/** Configuration options for CEL verification CLI operations. */ +final class VerificationOptions { + + /** Output format for verification CLI results. */ + enum OutputFormat { + TEXT, + JSON + } + + static final Duration DEFAULT_TIMEOUT = Duration.ofSeconds(10); + static final int DEFAULT_COMPREHENSION_UNROLL_LIMIT = 5; + static final OutputFormat DEFAULT_OUTPUT_FORMAT = OutputFormat.TEXT; + + private final Duration timeout; + private final int comprehensionUnrollLimit; + private final ImmutableList unknownIdentifiers; + private final OutputFormat outputFormat; + + Duration getTimeout() { + return timeout; + } + + int getComprehensionUnrollLimit() { + return comprehensionUnrollLimit; + } + + ImmutableList getUnknownIdentifiers() { + return unknownIdentifiers; + } + + OutputFormat getOutputFormat() { + return outputFormat; + } + + static Builder builder() { + return new Builder(); + } + + /** A builder for {@link VerificationOptions}. */ + static final class Builder { + private Duration timeout = DEFAULT_TIMEOUT; + private int comprehensionUnrollLimit = DEFAULT_COMPREHENSION_UNROLL_LIMIT; + private ImmutableList unknownIdentifiers = ImmutableList.of(); + private OutputFormat outputFormat = DEFAULT_OUTPUT_FORMAT; + + @CanIgnoreReturnValue + Builder setTimeout(Duration timeout) { + this.timeout = Preconditions.checkNotNull(timeout); + return this; + } + + @CanIgnoreReturnValue + Builder setComprehensionUnrollLimit(int unrollLimit) { + Preconditions.checkArgument(unrollLimit >= 0, "unrollLimit must be non-negative"); + this.comprehensionUnrollLimit = unrollLimit; + return this; + } + + @CanIgnoreReturnValue + Builder setUnknownIdentifiers(List unknownIdentifiers) { + this.unknownIdentifiers = ImmutableList.copyOf(unknownIdentifiers); + return this; + } + + @CanIgnoreReturnValue + Builder setOutputFormat(OutputFormat outputFormat) { + this.outputFormat = Preconditions.checkNotNull(outputFormat); + return this; + } + + VerificationOptions build() { + return new VerificationOptions( + timeout, comprehensionUnrollLimit, unknownIdentifiers, outputFormat); + } + } + + private VerificationOptions( + Duration timeout, + int comprehensionUnrollLimit, + ImmutableList unknownIdentifiers, + OutputFormat outputFormat) { + this.timeout = timeout; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.unknownIdentifiers = unknownIdentifiers; + this.outputFormat = outputFormat; + } + + /** + * Helper utility to parse CLI variable definitions formatted as "name:type" (e.g. "x:int", + * "role:string", "is_admin:bool"). + */ + static ImmutableMap parseVariables(List varSpecs) { + if (varSpecs == null || varSpecs.isEmpty()) { + return ImmutableMap.of(); + } + Map vars = new HashMap<>(); + for (String varSpec : varSpecs) { + Preconditions.checkNotNull(varSpec, "Variable specification cannot be null."); + String[] parts = varSpec.split(":", 2); + if (parts.length != 2) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + + varSpec + + "'. Expected format 'name:type' (e.g., 'x:int')."); + } + String name = parts[0].trim(); + if (name.isEmpty()) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + varSpec + "'. Variable name cannot be empty."); + } + String typeStr = parts[1].trim().toLowerCase(Locale.US); + CelType type = parseCelType(typeStr); + vars.put(name, type); + } + return ImmutableMap.copyOf(vars); + } + + static CelType parseCelType(String typeStr) { + Preconditions.checkNotNull(typeStr, "Type string cannot be null."); + String str = typeStr.trim().toLowerCase(Locale.US); + + if (str.startsWith("list<") && str.endsWith(">")) { + String inner = str.substring(5, str.length() - 1).trim(); + CelType elemType = parseCelType(inner); + return ListType.create(elemType); + } + + if (str.startsWith("map<") && str.endsWith(">")) { + String inner = str.substring(4, str.length() - 1).trim(); + List parts = splitGenericArgs(inner); + if (parts.size() != 2) { + throw new IllegalArgumentException( + "Invalid map type format: '" + + typeStr + + "'. Expected format 'map' (e.g., 'map')."); + } + CelType keyType = parseCelType(parts.get(0)); + CelType valueType = parseCelType(parts.get(1)); + return MapType.create(keyType, valueType); + } + + switch (str) { + case "int": + return SimpleType.INT; + case "uint": + return SimpleType.UINT; + case "string": + return SimpleType.STRING; + case "bool": + case "boolean": + return SimpleType.BOOL; + case "double": + case "float": + return SimpleType.DOUBLE; + case "bytes": + return SimpleType.BYTES; + case "dyn": + return SimpleType.DYN; + default: + throw new IllegalArgumentException( + "Unsupported type for CLI variable declaration: '" + + typeStr + + "'. Supported types: int, uint, string, bool, double, bytes, dyn, list, map."); + } + } + + private static List splitGenericArgs(String inner) { + List result = new ArrayList<>(); + int depth = 0; + StringBuilder current = new StringBuilder(); + for (int i = 0; i < inner.length(); i++) { + char c = inner.charAt(i); + if (c == '<') { + depth++; + current.append(c); + } else if (c == '>') { + depth--; + current.append(c); + } else if (c == ',' && depth == 0) { + result.add(current.toString().trim()); + current.setLength(0); + } else { + current.append(c); + } + } + if (current.length() > 0) { + result.add(current.toString().trim()); + } + return result; + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 9e7f0ed15..de788ca5c 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -9,7 +9,7 @@ java_library( name = "tests", testonly = True, srcs = glob( - ["**/*.java"], + ["*.java"], ), compatible_with = [], data = [ @@ -53,6 +53,7 @@ java_library( "//verifier:verifier_factory", "//verifier:z3_impl", "//verifier/axioms", + "//verifier/tools", "@cel_spec//proto/cel/expr/conformance/proto3:test_all_types_java_proto", "@maven//:com_google_guava_guava", ], diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 59a5e8438..a64ff72f1 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -93,7 +93,10 @@ public final class CelVerifierZ3ImplTest { .addVar("b", SimpleType.BOOL) .addVar("role", SimpleType.STRING) .addVar("country", SimpleType.STRING) + .addVar("string_var", SimpleType.STRING) .addVar("port", SimpleType.INT) + .addVar("dur", SimpleType.DURATION) + .addVar("ts", SimpleType.TIMESTAMP) .addVar("request", SimpleType.DYN) .addVar("unknown_var", SimpleType.DYN) .addVar("int_list", ListType.create(SimpleType.INT)) @@ -151,8 +154,6 @@ private enum IsSatisfiableTestCase { NULL_SATISFIABLE("unknown_var == null"), DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0"), DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5"), - TIMESTAMP_EQUALITY_TAUTOLOGY( - "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"), MACRO_LIMIT("dyn_list.all(x, x == 1)"), STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"), @@ -196,6 +197,80 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)"); } + @Test + public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("string_int_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_listNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_list.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_list = ["); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_dynMapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void counterexample_nullValueFormattedAsNull() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("unknown_var == 3u && request == null").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("request = null"); + } + + private enum CounterexampleNeverErrorTestCase { + DYN_LIST_REFLEXIVITY("dyn_list.size() == 1 ? dyn_list[0] == dyn_list[0] : true"), + DYN_MAP_REFLEXIVITY("dyn_map.size() == 1 ? dyn_map[1] == dyn_map[1] : true"), + DYN_LIST_ELEMENT("size(dyn_list) == 1 && dyn_list[0] == 'impossible_value'"), + DYN_MAP_VALUE("size(dyn_map) == 1 && dyn_map['a'] == 'impossible_value'"), + ; + + final String expr; + + CounterexampleNeverErrorTestCase(String expr) { + this.expr = expr; + } + } + + @Test + public void isAlwaysTrue_counterexampleNeverContainsError( + @TestParameter CounterexampleNeverErrorTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).doesNotContain("Error"); + } + @Test public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exception { CelAbstractSyntaxTree ast = CEL.compile("1 + 1 == 2").getAst(); @@ -288,7 +363,9 @@ private enum IsUnsatisfiableTestCase { TYPE_CONVERSION_UNSATISFIABLE_DOUBLE_TO_STRING("type(string(1.5)) == int"), EMPTY_MAP_SIZE_NOT_ZERO("size({}) != 0"), TIMESTAMP_INEQUALITY_CONTRADICTION( - "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"); + "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"), + TYPE_TIMESTAMP_NOT_INT("type(timestamp('1970-01-01T00:00:00Z')) == int"), + DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"); final String expr; @@ -321,6 +398,15 @@ public void isSatisfiable_timeout_throwsException() throws Exception { private enum IsAlwaysTrueTestCase { LOGICAL_OR_CONSTANTS("true || false"), + TIMESTAMP_GREATER_EQUALS("timestamp(200) >= timestamp(100)"), + DURATION_GREATER_EQUALS( + "(timestamp(200) - timestamp(100)) >= (timestamp(150) - timestamp(100))"), + DURATION_GREATER("(timestamp(200) - timestamp(100)) > (timestamp(150) - timestamp(100))"), + TIMESTAMP_LESS("timestamp(100) < timestamp(200)"), + DURATION_LESS("(timestamp(150) - timestamp(100)) < (timestamp(200) - timestamp(100))"), + TIMESTAMP_VARIABLE_TYPE("type(ts) == type(timestamp(0))"), + DURATION_VARIABLE_TYPE("type(dur) == type(timestamp(1) - timestamp(0))"), + TIMESTAMP_VARIABLE_BOUNDS("ts >= timestamp(-62135596800) && ts <= timestamp(253402300799)"), CYCLIC_MACRO_SHADOWING_SAFETY("[1].all(x, [x].all(x, x == 1))"), TAUTOLOGY("x > 5 || x <= 5"), LIST_VARIABLE_CONSTRAINED("1 in int_list || !(1 in int_list)"), @@ -655,29 +741,7 @@ private enum IsAlwaysTrueTestCase { TYPE_CONVERSION_DYN_IDENTITY("dyn(1) == 1"), TYPE_CONVERSION_UINT_TO_INT("int(1u) == 1"), TYPE_CONVERSION_INT_TO_UINT("uint(1) == 1u"), - TYPE_CONVERSION_INT_FROM_DOUBLE("int(1.0) == int(1.0)"), - TYPE_CONVERSION_INT_FROM_STRING("int('1') == int('1')"), - TYPE_CONVERSION_INT_FROM_TIMESTAMP( - "int(timestamp('1970-01-01T00:00:00Z')) == int(timestamp('1970-01-01T00:00:00Z'))"), - TYPE_CONVERSION_UINT_FROM_DOUBLE("uint(1.0) == uint(1.0)"), - TYPE_CONVERSION_UINT_FROM_STRING("uint('1') == uint('1')"), - TYPE_CONVERSION_DOUBLE_FROM_INT("double(1) == double(1)"), - TYPE_CONVERSION_DOUBLE_FROM_UINT("double(1u) == double(1u)"), - TYPE_CONVERSION_DOUBLE_FROM_STRING("double('1.0') == double('1.0')"), - TYPE_CONVERSION_STRING_FROM_INT("string(1) == string(1)"), - TYPE_CONVERSION_STRING_FROM_UINT("string(1u) == string(1u)"), - TYPE_CONVERSION_STRING_FROM_DOUBLE("string(1.0) == string(1.0)"), - TYPE_CONVERSION_STRING_FROM_BOOL("string(true) == string(true)"), - TYPE_CONVERSION_STRING_FROM_BYTES("string(b'foo') == string(b'foo')"), - TYPE_CONVERSION_STRING_FROM_TIMESTAMP( - "string(timestamp('1970-01-01T00:00:00Z')) == string(timestamp('1970-01-01T00:00:00Z'))"), - TYPE_CONVERSION_STRING_FROM_DURATION("string(duration('1s')) == string(duration('1s'))"), - TYPE_CONVERSION_BYTES_FROM_STRING("bytes('foo') == bytes('foo')"), - TYPE_CONVERSION_DURATION_FROM_STRING("duration('1s') == duration('1s')"), - TYPE_CONVERSION_TIMESTAMP_FROM_STRING( - "timestamp('1970-01-01T00:00:00Z') == timestamp('1970-01-01T00:00:00Z')"), TYPE_CONVERSION_TIMESTAMP_FROM_INT("timestamp(1) == timestamp(1)"), - TYPE_CONVERSION_BOOL_FROM_STRING("bool('true') == bool('true')"), TYPE_CONVERSION_INT_TO_UINT_ZERO("uint(0) == 0u"), TYPE_AXIOM_OPTIONAL("type(optional.of(1)) == optional_type"), @@ -757,6 +821,9 @@ private enum IsAlwaysTrueTestCase { UINT64_BOUNDS_ALWAYS_TRUE("u <= 18446744073709551615u && u >= 0u"), MODULO_INT64_MIN_INT_BY_NEG_ONE_ALWAYS_ZERO( "x == -9223372036854775808 && y == -1 ? x % y == 0 : true"), + DYNAMIC_VAR_TYPE_IDENTITY("type(dyn_var) == type(dyn_var)"), + DYNAMIC_MAP_KEY_COMPREHENSION_TYPE_IDENTITY( + "size(dyn_map) > 0 && size(dyn_map) <= 5 ? dyn_map.all(k, type(k) == type(k)) : true"), ; final String expr; @@ -954,7 +1021,11 @@ private enum UnconditionalErrorTestCase { COLLECTION_ERROR("{'a': 1 / 0} == {'a': 1 / 0}"), LIST_ERROR("[1 / 0] == [1 / 0]"), STRICT_LITERAL_ERROR("{'a': 1/0}.exists(k, k == 'a') == {'a': 1/0}.exists(k, k == 'a')"), - STRICT_LITERAL_ERROR_KEY("{1/0: 'a'}.exists(k, k == 1) == {1/0: 'a'}.exists(k, k == 1)"); + STRICT_LITERAL_ERROR_KEY("{1/0: 'a'}.exists(k, k == 1) == {1/0: 'a'}.exists(k, k == 1)"), + TIMESTAMP_INT_CONVERSION_OUT_OF_BOUNDS( + "timestamp(999999999999999) == timestamp(999999999999999)"), + TIMESTAMP_INT_CONVERSION_UNDERFLOW( + "timestamp(-999999999999999) == timestamp(-999999999999999)"); final String expr; @@ -1075,6 +1146,58 @@ public void verifyEquivalence_infinityConstants_notEquivalent() throws Exception private enum IsAlwaysTrueViolationTestCase { NOT_ALWAYS_TRUE( "x > 5", "Condition is not always true\\.", "Counterexample input:", "x = -?\\d+"), + UNINTERPRETED_CONVERSION_CAN_ERROR_INT( + "int(request) == int(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_UINT( + "uint(request) == uint(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DOUBLE( + "double(request) == double(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP( + "timestamp(request) == timestamp(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL( + "bool(request) == bool(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_STRING( + "string(request) == string(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_BYTES( + "bytes(request) == bytes(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION( + "duration(request) == duration(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + DURATION_VARIABLE_COUNTEREXAMPLE( + "dur != dur", + "Condition is not always true\\.", + "Counterexample input:", + "dur = duration\\(-?\\d+\\)"), + TIMESTAMP_VARIABLE_COUNTEREXAMPLE( + "ts != ts", + "Condition is not always true\\.", + "Counterexample input:", + "ts = timestamp\\(-?\\d+\\)"), + UNINTERPRETED_CONVERSION_NULL_FAILS_WITH_ERRORS( + "string(null) == string(null)", "Condition is not always true\\."), LAW_OF_EXCLUDED_MIDDLE_FAILS_WITH_ERRORS( "(1 / 0 == 5) || !(1 / 0 == 5)", "Condition is not always true\\."), INTEGER_OVERFLOW_FAILS_WITH_ERRORS( @@ -1087,6 +1210,12 @@ private enum IsAlwaysTrueViolationTestCase { "Condition is not always true\\.", "Counterexample input:", "u = \\d+u?"), + CROSS_TYPE_DYNAMIC_EQUALITY_NOT_ALWAYS_UNEQUAL_INT_DOUBLE( + "!(request == unknown_var && type(request) == int && type(unknown_var) == double)", + "Condition is not always true\\.", + "Counterexample input:", + "unknown_var = -?\\d+\\.\\d+", + "request = -?\\d+"), NEGATE_MIN_INT_FAILS_WITH_ERRORS( "-(-x) == x", "Condition is not always true\\.", "Counterexample input:", "x = -?\\d+"), HETEROGENEOUS_ARITHMETIC_FAILS("dyn(1) + 1u == 2u", "Condition is not always true\\."), @@ -1102,12 +1231,6 @@ private enum IsAlwaysTrueViolationTestCase { "Counterexample input:", "x = -?\\d+", "u = \\d+u?"), - CROSS_TYPE_DYNAMIC_EQUALITY_NOT_ALWAYS_UNEQUAL_INT_DOUBLE( - "!(request == unknown_var && type(request) == int && type(unknown_var) == double)", - "Condition is not always true\\.", - "Counterexample input:", - "unknown_var = -?\\d+\\.\\d+", - "request = -?\\d+"), OPTIONAL_DYN_VAR_HAS_VALUE_NOT_IMPLIES_INT( "opt_dyn_var.hasValue() ? type(opt_dyn_var.value()) == int : true", "Condition is not always true\\.", @@ -1117,18 +1240,18 @@ private enum IsAlwaysTrueViolationTestCase { "[?dyn_var] == [?dyn_var] ? true : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), OPTIONAL_MAP_ENTRY_DYN_VAR_TYPE_MISMATCH( "{?1: dyn_var} == {?1: dyn_var} ? true : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), OPTIONAL_STRUCT_ENTRY_DYN_VAR_TYPE_MISMATCH( "cel.expr.conformance.proto3.TestAllTypes{?single_int32: dyn_var} ==" + " cel.expr.conformance.proto3.TestAllTypes{?single_int32: dyn_var} ? true : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"(!0!|i)\""), + "dyn_var = .*"), OPTIONAL_NONE_COUNTEREXAMPLE( "opt_dyn_var.hasValue()", "Condition is not always true\\.", @@ -1235,7 +1358,7 @@ private enum IsAlwaysTrueViolationTestCase { "dyn_var == 1.0", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), DYNAMIC_NOT_TYPE_MISMATCH( "!dyn_var", "Condition is not always true\\.", @@ -1245,7 +1368,7 @@ private enum IsAlwaysTrueViolationTestCase { "dyn_var ? true : false", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), DYNAMIC_NOT_TYPE_MISMATCH_SURVIVOR( "type(dyn_var) == int ? (!dyn_var == !dyn_var) : true", "Condition is not always true\\.", @@ -1292,6 +1415,22 @@ private enum IsAlwaysTrueViolationTestCase { "Counterexample input:", "x = -9223372036854775808", "y = -1"), + UNINTERPRETED_CONVERSION_CAN_ERROR_INT_FROM_STRING( + "int(string_var) == int(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP_FROM_STRING( + "timestamp(string_var) == timestamp(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION_FROM_STRING( + "duration(string_var) == duration(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL_FROM_STRING( + "bool(string_var) == bool(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), ; final String expr; @@ -1317,6 +1456,17 @@ public void isAlwaysTrue_violation_returnsFalse( } private enum IsInconclusiveTestCase { + // TODO: Implement RFC 3339 spec in conversion + TIMESTAMP_STRING_CONVERSION_VALID( + "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), + DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"), + BOOL_STRING_UNINTERPRETED("bool('true') == true"), + TIMESTAMP_ADD_DURATION_OVERFLOW("timestamp(253402300799) + duration('100s') > timestamp(0)"), + DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION( + "type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :" + + " true"), + // TODO: Implement RFC 3339 spec in conversion + TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"), UNINTERPRETED_FUNCTION("request.matches('^[a-z]+$')"), INT_STRING_UNINTERPRETED("int('123') == 123"), LIST_WITH_APPROXIMATE_ELEMENT("[request.matches('a')]"), @@ -1398,7 +1548,18 @@ private enum EquivalenceInconclusiveTestCase { "size(int_list) == 6 ? int_list.map(x, 2.0) : [1.0]"), TRUNCATION_DIVERGENCE_DIFFERENT_BYTES( "size(int_list) == 6 ? int_list.map(x, b'a') : [b'a']", - "size(int_list) == 6 ? int_list.map(x, b'b') : [b'a']"); + "size(int_list) == 6 ? int_list.map(x, b'b') : [b'a']"), + TIMESTAMP_MATH_ADD_DUR_TS("timestamp(100) + duration('100s')", "timestamp(200)"), + TIMESTAMP_MATH_ADD_TS_DUR("duration('100s') + timestamp(100)", "timestamp(200)"), + TIMESTAMP_MATH_SUBTRACT_DUR("timestamp(900000) - duration('100s')", "timestamp(899900)"), + DURATION_MATH_ADD_DUR_DUR("duration('100s') + duration('200s')", "duration('300s')"), + DURATION_MATH_SUBTRACT_DUR_DUR("duration('300s') - duration('100s')", "duration('200s')"), + DURATION_MATH_ASSOCIATIVITY( + "(duration('10s') + duration('20s')) + duration('30s')", + "duration('10s') + (duration('20s') + duration('30s'))"), + TIMESTAMP_DURATION_MATH_ASSOCIATIVITY( + "(timestamp(10) + duration('20s')) + duration('30s')", + "timestamp(10) + (duration('20s') + duration('30s'))"); final String exprA; final String exprB; @@ -1421,6 +1582,7 @@ public void verifyEquivalence_inconclusive( } private enum EquivalenceTestCase { + STRUCT_UNSET_TIMESTAMP_DEFAULT("TestAllTypes{}.single_timestamp", "timestamp(0)"), TRUNCATION_STRICT_PROPAGATION_EQUIVALENT( "size(int_list) == 6 ? size(int_list.filter(x, x > 2)) : 0", "size(int_list) == 6 ? size(int_list.filter(y, y > 2)) : 0"), @@ -1438,6 +1600,12 @@ private enum EquivalenceTestCase { MACRO_EXISTS_ONE_EQUIVALENT( "[1, 2, 3].exists_one(x, x == 2)", "(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"), + TIMESTAMP_MATH_SUBTRACT_TS( + "timestamp(900000) - timestamp(100)", "timestamp(899900) - timestamp(0)"), + TIMESTAMP_MATH_COMMUTATIVITY( + "duration('10s') + timestamp(50)", "timestamp(50) + duration('10s')"), + DURATION_MATH_COMMUTATIVITY( + "duration('10s') + duration('20s')", "duration('20s') + duration('10s')"), MACRO_MAP_EQUIVALENT("{1: true, 2: true, 3: true}.all(k, k > 0)", "1 > 0 && 2 > 0 && 3 > 0"), MACRO_BIND_EQUIVALENT("cel.bind(x, 10, x > 0)", "10 > 0"), NESTED_MACRO( diff --git a/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..6077e4950 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,31 @@ +load("@rules_java//java:defs.bzl", "java_library") +load("//:testing.bzl", "junit4_test_suites") + +package( + default_applicable_licenses = ["//:license"], +) + +java_library( + name = "tests", + testonly = True, + srcs = glob(["*.java"]), + deps = [ + "//:java_truth", + "//common/types", + "//common/types:type_providers", + "//verifier", + "//verifier/tools", + "@maven//:com_google_guava_guava", + "@maven//:info_picocli_picocli", + "@maven//:junit_junit", + ], +) + +junit4_test_suites( + name = "test_suites", + sizes = [ + "small", + ], + src_dir = "src/test/java", + deps = [":tests"], +) diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java new file mode 100644 index 000000000..52124c6ed --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -0,0 +1,188 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; +import static java.nio.charset.StandardCharsets.UTF_8; + +import java.io.BufferedReader; +import java.io.ByteArrayOutputStream; +import java.io.PrintStream; +import java.io.StringReader; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class CelVerifierReplTest { + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + @SuppressWarnings({"PreferCharsetOverload", "JdkObsolete"}) + private String[] runReplWithCommands(String... commands) throws Exception { + String input = String.join("\n", commands) + "\n"; + BufferedReader reader = new BufferedReader(new StringReader(input)); + ByteArrayOutputStream outStream = new ByteArrayOutputStream(); + ByteArrayOutputStream errStream = new ByteArrayOutputStream(); + PrintStream out = new PrintStream(outStream, true, UTF_8.name()); + PrintStream err = new PrintStream(errStream, true, UTF_8.name()); + + CelVerifierRepl.runRepl(reader, out, err); + + return new String[] { + new String(outStream.toByteArray(), UTF_8), new String(errStream.toByteArray(), UTF_8) + }; + } + + @Test + public void repl_quitAndExit() throws Exception { + String[] output1 = runReplWithCommands(":quit"); + assertThat(output1[0]).contains("Goodbye!"); + + String[] output2 = runReplWithCommands(":exit"); + assertThat(output2[0]).contains("Goodbye!"); + } + + @Test + public void repl_helpCommands() throws Exception { + String[] output = + runReplWithCommands( + ":help", + ":help var", + ":help unknown", + ":help timeout", + ":help unroll", + ":help sat", + ":help valid", + ":help equiv", + ":help non_existent_topic", + ":quit"); + assertThat(output[0]).contains("REPL Commands:"); + assertThat(output[0]).contains("Command: :var "); + assertThat(output[0]).contains("Command: :unknown "); + assertThat(output[0]).contains("Command: :timeout "); + assertThat(output[0]).contains("Command: :unroll "); + assertThat(output[0]).contains("Query: sat "); + assertThat(output[0]).contains("Query: valid "); + assertThat(output[0]).contains("Query: equiv <=> "); + } + + @Test + public void repl_varDeclarations() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", + ":var port int", + ":var scores map", + ":var tags list", + ":vars", + ":quit"); + assertThat(output[0]).contains("Variable declared: role : string"); + assertThat(output[0]).contains("Variable declared: port : int"); + assertThat(output[0]).contains("Variable declared: scores : map(string, int)"); + assertThat(output[0]).contains("Variable declared: tags : list(string)"); + assertThat(output[0]).contains("Variables (4):"); + } + + @Test + public void repl_unknownIdentifiers() throws Exception { + String[] output = + runReplWithCommands(":unknown request.headers", ":unknown request.auth", ":vars", ":quit"); + assertThat(output[0]).contains("Added unknown identifier: 'request.headers'"); + assertThat(output[0]).contains("Added unknown identifier: 'request.auth'"); + assertThat(output[0]).contains("Unknowns: [request.headers, request.auth]"); + } + + @Test + public void repl_timeoutConfiguration() throws Exception { + String[] output = + runReplWithCommands( + ":timeout 15", ":vars", ":timeout -5", ":timeout abc", ":timeout", ":quit"); + assertThat(output[0]).contains("Timeout set to 15s."); + assertThat(output[0]).contains("Timeout: 15s"); + assertThat(output[1]).contains("Timeout must be a positive integer."); + assertThat(output[1]).contains("Invalid timeout value."); + assertThat(output[1]).contains("Usage: :timeout "); + } + + @Test + public void repl_unrollConfiguration() throws Exception { + String[] output = + runReplWithCommands(":unroll 10", ":vars", ":unroll -1", ":unroll xyz", ":unroll", ":quit"); + assertThat(output[0]).contains("Comprehension unroll limit set to 10."); + assertThat(output[0]).contains("Unroll limit: 10"); + assertThat(output[1]).contains("Unroll limit must be non-negative."); + assertThat(output[1]).contains("Invalid unroll limit value."); + assertThat(output[1]).contains("Usage: :unroll "); + } + + @Test + public void repl_sessionStateAndClear() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", ":unknown req.headers", ":vars", ":clear", ":vars", ":quit"); + assertThat(output[0]).contains("Variables (1):"); + assertThat(output[0]).contains("Session state reset."); + assertThat(output[0]).contains("Variables (0):"); + assertThat(output[0]).contains("Unknowns: none"); + } + + @Test + public void repl_satQueries() throws Exception { + String[] output = + runReplWithCommands(":var port int", "sat port > 1024", "port > 1024", "sat", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Usage: sat "); + } + + @Test + public void repl_validQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "valid x > 0 || x <= 0", "valid x > 0", "valid", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[0]).contains("[VIOLATED]"); + assertThat(output[1]).contains("Usage: valid "); + } + + @Test + public void repl_equivQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "equiv x > 10 <=> 10 < x", "equiv x > 10", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Equivalence query format: equiv <=> "); + } + + @Test + public void repl_unknownCommandsAndErrors() throws Exception { + String[] output = + runReplWithCommands( + ":unknowncommand", + ":var", + ":var invalid_spec", + ":var x foo_type", + ":unknown", + "invalid + + syntax", + ":quit"); + assertThat(output[1]).contains("Unknown command: :unknowncommand"); + assertThat(output[1]).contains("Usage: :var "); + assertThat(output[1]).contains("Unsupported type"); + assertThat(output[1]).contains("Usage: :unknown "); + assertThat(output[1]).contains("Compilation error"); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java new file mode 100644 index 000000000..bfc794c28 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -0,0 +1,578 @@ +// 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.tools; + +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 dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.io.File; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.Arrays; +import org.junit.Before; +import org.junit.Rule; +import org.junit.Test; +import org.junit.rules.TemporaryFolder; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; +import picocli.CommandLine; + +@RunWith(JUnit4.class) +public final class CelVerifierToolTest { + + @Rule public TemporaryFolder tempFolder = new TemporaryFolder(); + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + private String executeToolWithOutput(String... args) { + StringWriter out = new StringWriter(); + PrintWriter pw = new PrintWriter(out); + CommandLine cmd = new CommandLine(new CelVerifierTool()); + cmd.setOut(pw); + cmd.setErr(pw); + cmd.execute(args); + return out.toString(); + } + + @Test + public void celVerifierTool_checkSat_jsonOutputFormat() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x > 0", "--var", "x:int", "--output_format", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + assertThat(output).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_textOutputFormat() { + String output = + executeToolWithOutput("check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "text"); + assertThat(output).contains("[VERIFIED]"); + assertThat(output).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_withDynVariable() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x == 'hello'", "--var", "x:dyn", "-fmt", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withUnknownOption() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "request.headers != null", + "--var", + "request:map", + "-u", + "request.headers", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withTimeoutAndUnrollLimit() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "[1, 2, 3].all(x, x > 0)", + "--timeout", + "5", + "--unroll-limit", + "5", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_fileNotFound() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", "non_existent_policy.yaml"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_ERROR); + } + + @Test + public void parseVariables_success() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "x:int", + "role:string", + "is_admin:bool", + "tags:list", + "scores:map")); + assertThat(vars).containsEntry("x", SimpleType.INT); + assertThat(vars).containsEntry("role", SimpleType.STRING); + assertThat(vars).containsEntry("is_admin", SimpleType.BOOL); + assertThat(vars).containsEntry("tags", ListType.create(SimpleType.STRING)); + assertThat(vars).containsEntry("scores", MapType.create(SimpleType.STRING, SimpleType.INT)); + } + + @Test + public void parseVariables_allTypesIncludingDyn() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "u:uint", + "d:double", + "fl:float", + "b:bytes", + "dyn_val:dyn", + "flag:boolean", + "nested_list:list", + "nested_map:map")); + assertThat(vars).containsEntry("u", SimpleType.UINT); + assertThat(vars).containsEntry("d", SimpleType.DOUBLE); + assertThat(vars).containsEntry("fl", SimpleType.DOUBLE); + assertThat(vars).containsEntry("b", SimpleType.BYTES); + assertThat(vars).containsEntry("dyn_val", SimpleType.DYN); + assertThat(vars).containsEntry("flag", SimpleType.BOOL); + assertThat(vars).containsEntry("nested_list", ListType.create(SimpleType.DYN)); + assertThat(vars).containsEntry("nested_map", MapType.create(SimpleType.STRING, SimpleType.DYN)); + } + + @Test + public void parseVariables_invalidFormat_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x_no_colon"))); + } + + @Test + public void parseVariables_unsupportedType_throws() { + IllegalArgumentException ex = + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x:foo_bar"))); + assertThat(ex) + .hasMessageThat() + .contains("Supported types: int, uint, string, bool, double, bytes, dyn"); + } + + @Test + public void parseVariables_invalidMapFormat_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x:map"))); + } + + @Test + public void parseVariables_emptyOrNull_returnsEmptyMap() { + assertThat(VerificationOptions.parseVariables(null)).isEmpty(); + assertThat(VerificationOptions.parseVariables(ImmutableList.of())).isEmpty(); + } + + @Test + public void parseVariables_nestedTypes() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "nested_map:map>", + "nested_list_map:map>")); + assertThat(vars) + .containsEntry( + "nested_map", + MapType.create(SimpleType.STRING, MapType.create(SimpleType.STRING, SimpleType.INT))); + assertThat(vars) + .containsEntry( + "nested_list_map", MapType.create(SimpleType.STRING, ListType.create(SimpleType.INT))); + } + + @Test + public void parseVariables_emptyString_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList(""))); + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList(" "))); + } + + @Test + public void parseVariables_nullElement_throws() { + assertThrows( + NullPointerException.class, + () -> VerificationOptions.parseVariables(Arrays.asList((String) null))); + } + + @Test + public void checkSatisfiable_satisfiable() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = + ImmutableMap.of("role", SimpleType.STRING, "port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("role == 'editor' && port > 1024", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("satisfiable"); + } + + @Test + public void checkValid_valid() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkValid("x > 10 || x <= 10", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyEquivalence_equivalent() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence("x > 10", "10 < x", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyInvariants_success() throws Exception { + String yamlPolicy = + "name: secure_access_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlPolicy, vars, options); + + assertThat(results).containsKey("port_check"); + assertThat(results.get("port_check").status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyEquivalence_equivalent() throws Exception { + String policyA = + "name: policy_a\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + + String policyB = + "name: policy_b\n" + + "rule:\n" + + " match:\n" + + " - condition: 80 == port\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyPolicyEquivalence(policyA, policyB, vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void formatTextPolicyResults_verifiedAndViolated() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult verifiedRes = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + CelVerificationResult violatedRes = + CelVerifierToolCore.checkValid("x > 0", ImmutableMap.of("x", SimpleType.INT), options); + + ImmutableMap results = + ImmutableMap.of("inv_1", verifiedRes, "inv_2", violatedRes); + + String text = FormatUtils.formatTextPolicyResults("test_policy", results); + assertThat(text).contains("Policy Invariant Verification for 'test_policy':"); + assertThat(text).contains("✓ Invariant 'inv_1': VERIFIED"); + assertThat(text).contains("✗ Invariant 'inv_2': VIOLATED"); + } + + @Test + public void formatJsonPolicyResults_structuredJson() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + + ImmutableMap results = ImmutableMap.of("inv_1", result); + + String json = FormatUtils.formatJsonPolicyResults("my_policy", results); + assertThat(json).contains("\"policyName\": \"my_policy\""); + assertThat(json).contains("\"id\": \"inv_1\""); + assertThat(json).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_success() throws Exception { + File policyFile = tempFolder.newFile("test_policy.yaml"); + String yamlContent = + "name: test_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + String output = + executeToolWithOutput( + "verify-policy", + "--file", + policyFile.getAbsolutePath(), + "--var", + "port:int", + "-fmt", + "json"); + + assertThat(output).contains("\"policyName\": \"test_policy.yaml\""); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_violated() throws Exception { + File policyFile = tempFolder.newFile("violated_policy.yaml"); + String yamlContent = + "name: violated_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: invalid_check\n" + + " assert:\n" + + " - port > 1024\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyPolicy_multipleInvariants_oneViolated() throws Exception { + File policyFile = tempFolder.newFile("multi_invariant_policy.yaml"); + String yamlContent = + "name: multi_invariant_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: valid_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n" + + " - id: invalid_check\n" + + " assert:\n" + + " - port > 1024\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyPolicy_multipleInvariants_allVerified() throws Exception { + File policyFile = tempFolder.newFile("multi_verified_policy.yaml"); + String yamlContent = + "name: multi_verified_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: check_1\n" + + " assert:\n" + + " - port == 80 || port != 80\n" + + " - id: check_2\n" + + " assert:\n" + + " - port > 0 || port <= 0\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void formatUtils_jsonResult() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + String json = FormatUtils.formatJsonResult(result); + assertThat(json).contains("\"status\": \"VERIFIED\""); + assertThat(json).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_verified() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-sat", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void celVerifierTool_checkValid_violated() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyEquiv_verified() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-equiv", "--expr1", "x > 10", "--expr2", "10 < x", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void celVerifierTool_checkSat_compilationError() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-sat", "--expr", "invalid + + syntax", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_ERROR); + } + + @Test + public void celVerifierTool_checkValid_inconclusive() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "int('123') == 123"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); + } + + @Test + public void celVerifierTool_verifyPolicy_inconclusive() throws Exception { + File policyFile = tempFolder.newFile("inconclusive_policy.yaml"); + String yamlContent = + "name: inconclusive_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: approx_check\n" + + " assert:\n" + + " - int('123') == 123\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); + } + + @Test + public void celVerifierTool_invalidOutputFormat_defaultsToText() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "invalid_fmt"); + assertThat(output).contains("[VERIFIED]"); + } + + @Test + public void formatTextPolicyResults_inconclusive() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult res = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + + String text = FormatUtils.formatTextPolicyResults("test_policy", ImmutableMap.of("inv_1", res)); + assertThat(text).contains("Invariant 'inv_1': INCONCLUSIVE"); + } + + @Test + public void formatJson_escapesSpecialCharacters() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult res = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + String json = + FormatUtils.formatJsonPolicyResults( + "policy_with_\"quote\"\nand_newline", ImmutableMap.of("inv\ttab", res)); + assertThat(json).contains("policy_with_\\\"quote\\\"\\nand_newline"); + assertThat(json).contains("inv\\ttab"); + } + + @Test + public void celVerifierTool_version() { + int exitCode = new CommandLine(new CelVerifierTool()).execute("--version"); + assertThat(exitCode).isEqualTo(0); + } +} diff --git a/verifier/tools/BUILD.bazel b/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..a547c15b2 --- /dev/null +++ b/verifier/tools/BUILD.bazel @@ -0,0 +1,19 @@ +package( + default_applicable_licenses = ["//:license"], + default_visibility = ["//verifier:verifier_internal"], +) + +alias( + name = "tools", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", +) + +alias( + name = "tools_lib", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", +) + +alias( + name = "cel_verifier_tool", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool", +) diff --git a/verifier/tools/README.md b/verifier/tools/README.md new file mode 100644 index 000000000..398cbad74 --- /dev/null +++ b/verifier/tools/README.md @@ -0,0 +1,191 @@ +# CEL Java Verifier CLI & Interactive REPL Tool + +The CEL Java Verifier comes with a command-line tool (`cel-verifier`) and an +interactive REPL shell for testing satisfiability, validity, equivalence, +and policy invariants without writing Java code. + +## Running the CLI Tool + +### Running via Bazel + +```bash +# Run CLI verification commands +bazel run //verifier/tools:cel_verifier_tool -- \ + check-sat \ + --expr "role == 'editor' && port > 1024" \ + --var "role:string" \ + --var "port:int" + +# Run with JSON output format for CI/CD integrations +bazel run //verifier/tools:cel_verifier_tool -- \ + check-sat \ + --expr "role == 'editor'" \ + --var "role:string" \ + --output_format=json + +# Launch interactive REPL shell +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 + prints witness inputs if satisfiable. +* `check-valid --expr "..."`: Proves validity (`isAlwaysTrue`) and prints + a counterexample if invalid. +* `verify-equiv --expr1 "..." --expr2 "..."`: Proves logical equivalence + between two CEL expressions. +* `verify-policy --file policy.yaml`: Verifies policy invariants defined + in a YAML policy file. +* `repl`: Enters interactive verification shell mode. + +## Command Options + +The verification commands (`check-sat`, `check-valid`, `verify-equiv`, +`verify-policy`) accept the following options: + +### Variable Declarations (`--var`, `-v`) + +Declare variables in `name:type` format. Multiple variables can be declared by +repeating the `--var` option. + +Supported types: + +* Primitive types: `int`, `uint`, `string`, `bool`, `double`, `bytes`, `dyn` +* List types: `list` (e.g., `--var "tags:list"`) +* Map types: `map` (e.g., `--var "scores:map"`) + +Examples: +```bash +--var "role:string" --var "port:int" --var "tags:list" +``` + +### Unknown Identifiers (`--unknown`, `-u`) + +Permit specific identifiers or attributes (e.g., `request.headers`) to +evaluate to `Unknown` during verification: + +```bash +--unknown "request.headers" --unknown "auth.credentials" +``` + +### Solver Timeout (`--timeout`) + +Set maximum Z3 SMT solver timeout in seconds (default: `10`): + +```bash +--timeout 15 +``` + +### Comprehension Unroll Limit (`--unroll-limit`) + +Set bounded unroll limit for comprehensions and loop macros like `.all()` and +`.exists()` (default: `5`): + +```bash +--unroll-limit 10 +``` + +### Output Format (`--output_format`, `-fmt`) + +Set CLI output format (`TEXT` or `JSON`, default: `TEXT`): + +```bash +--output_format json +``` + +## Exit Codes + +* `0`: Verification succeeded / condition verified. +* `1`: Violation or counterexample found. +* `2`: Inconclusive result (solver unknown or timeout). +* `3`: Error (syntax compilation error, missing file, or execution error). + +## Interactive REPL Shell + +The REPL shell provides an interactive, stateful environment to execute CEL +formal verification queries without re-declaring variables or re-running CLI +parameters for every query. + +### Launching the REPL + +```bash +bazel run //verifier/tools:cel_verifier_tool -- repl +``` + +### REPL Commands + +| Command | Description | Example | +|---|---|---| +| `:var ` | Declare a variable in session state | `:var role string` | +| `:unknown ` | Mark identifier as Unknown | `:unknown request.headers` | +| `:timeout ` | Set Z3 solver timeout in seconds (default: 10s) | `:timeout 5` | +| `:unroll ` | Set comprehension unroll limit (default: 5) | `:unroll 3` | +| `:vars` | Display declared session variables & config | `:vars` | +| `:clear` | Reset session state (clears variables & unknowns) | `:clear` | +| `:help [cmd]` | Display built-in help or command details | `:help var` | +| `:quit` / `:exit` | Exit the interactive REPL shell | `:quit` | + +### Verification Queries in REPL + +* **Satisfiability (`sat ` or ``):** Checks if the expression + can evaluate to `true` for any assignment of session variables. Outputs + satisfying witness inputs if satisfiable. +* **Validity (`valid `):** Proves whether the expression evaluates + to `true` for ALL possible variable assignments. Outputs a counterexample + if invalid. +* **Equivalence (`equiv <=> `):** Proves whether two + expressions are logically identical across all inputs. Outputs a + counterexample if not equivalent. + +### Example REPL Session + +```text +============================================================ + CEL Verification REPL + Type :help for commands, :quit to exit. +============================================================ +cel-verifier> :var port int +Variable declared: port : int + +cel-verifier> sat role == 'admin' && port > 1024 + +cel-verifier> :var role string +Variable declared: role : string + +cel-verifier> sat role == 'admin' && port > 1024 +[VERIFIED] Condition is satisfiable. Satisfying input: + role = "admin" + port = 1025 + +cel-verifier> valid port > 0 || port <= 0 +[VERIFIED] + +cel-verifier> valid port > 1024 +[VIOLATED] Condition is violated. Counterexample input: + port = 0 + +cel-verifier> equiv port > 10 <=> 10 < port +[VERIFIED] + +cel-verifier> :vars +--- Session State --- +Timeout: 10s | Unroll limit: 5 +Unknowns: none +Variables (2): + role : string + port : int + +cel-verifier> :quit +Goodbye! +``` + +> **Note:** Inline help is built into the REPL shell. Type `:help` or +> `:help ` (e.g. `:help var`, `:help equiv`) at any prompt for +> detailed usage instructions and examples. +