CEL-Java: Common Expression Language for Java

The verifier provides several advanced formal verification capabilities:

• Satisfiability & Validity Proving: Check if an expression can evaluate to true (isSatisfiable) or if it is guaranteed to always be true (isAlwaysTrue).
• Logical Equivalence: Prove that two different ASTs or Policies are semantically identical.
• Bounded Model Checking (BMC): Verifies list and map comprehensions (all, exists, map, filter) by unrolling them up to a configurable limit.
• Counterexample & Witness Generation: Generates human-readable counterexamples when validity or equivalence checks fail. For satisfiability checks, it produces a 'witness' (concrete variable assignments) that makes the expression true.
• Custom Invariants Verification: Allows you to define safety invariants and prove they are never violated across all possible input states.
• Partial Evaluation (Unknowns) Support: Allows defining variables that can evaluate to Unknown, mirroring CEL's runtime partial evaluation behavior.

CEL provides a fluent API to traverse a compiled AST via CelNavigableAst. This is essential for writing custom validators that need to inspect specific parts of an expression.

Key Navigation Methods

• .getRoot(): Starts navigation from the root of the AST.
• .allNodes(): Returns a stream of all nodes in the tree.
• .descendants(): Returns a stream of all descendant nodes of a specific node.
• .filter(Predicate): Filters nodes based on criteria (e.g., node.getKind().equals(Kind.STRUCT)).
• .map(Function): Transforms nodes into other types (e.g., mapping a node to its underlying CelStruct).
• .anyMatch(Predicate): Checks if any descendant matches a condition (useful for finding specific function calls within a macro).

Pro-tips

• Kind Checking: Use node.getKind() to identify the type of node (e.g., Kind.STRUCT, Kind.COMPREHENSION).
• Convenience Methods: Use (kind)OrDefault methods like callOrDefault() to consolidate checking for an expression kind and retrieving the underlying expression in one step.
• Human-Readable AST: Call .toString() on a CelExpr object to get a human-readable representation of the AST for debugging.

CEL features unique commutative logical operators (|| and &&) designed for robustness. The engine attempts to find an evaluation order that yields a result even if some branches contain errors (like division by zero) or missing data.

Short-circuiting and Error Handling

• Success via Short-circuiting: If a logical operation can determine its result without evaluating an erroneous branch, it will return the logical result instead of propagating the error. For example, true || (1 / 0 > 2) returns true because the first operand satisfies the OR condition.
• Error Propagation: An exception (specifically a CelEvaluationException wrapped in an IllegalArgumentException) is only surfaced if all branches of the logical operator resolve to an error. For example, false || (1 / 0 > 2) will throw an error because the second branch cannot be resolved.

This behavior is particularly useful for systems like IAM (Identity and Access Management), where it allows the engine to minimize the cost of evaluation by deferring or skipping expensive or failing inputs if a result is already reachable.

```java
// Example of short-circuiting an error
// Returns true, does NOT throw division by zero error
Object result = exercise3.compileAndEvaluate("true || (1 / 0 > 2)");

// Example of error propagation
// Throws IllegalArgumentException (caused by CelEvaluationException: / by zero)
Object errorResult = exercise3.compileAndEvaluate("false || (1 / 0 > 2)");
```埋

CEL applications evaluate expressions against an Environment. The standard environment supports all types, operators, functions, and macros defined in the CEL specification.

Environments are customized using CelOptions and are constructed via factories:

1. CelCompiler: Used to parse and type-check expressions. It is immutable and thread-safe, making it suitable for static initialization and caching.
2. CelRuntime: Takes a compiled AST and produces an evaluable instance. Like the compiler, it is immutable and can be cached.

Customization (such as disabling macros or declaring custom variables) is handled through fluent APIs on the builders provided by CelCompilerFactory and CelRuntimeFactory.

// Setup an environment for expression compilation and evaluation.

// Breaking behavior changes and optional features are controlled by CelOptions
private static final CelOptions CEL_OPTIONS = CelOptions.current().build();

// CelCompiler is used to parse and type-check expressions.
private static final CelCompiler CEL_COMPILER = 
        CelCompilerFactory.standardCelCompilerBuilder()
             .setOptions(CEL_OPTIONS)
             .build();

// CelRuntime takes in a compiled expression and produces an evaluable instance.
private static final CelRuntime CEL_RUNTIME = 
        CelRuntimeFactory.plannerRuntimeBuilder()
             .setOptions(CEL_OPTIONS)
             .build();

The TwoVarComprehensions extension introduces support for comprehensions that use two variables (typically an index/key and a value). This allows for more complex transformations and predicates on lists and maps.

all

Tests if all elements satisfy a predicate. Short-circuits on false.

• <list>.all(indexVar, valueVar, <predicate>) -> bool
• <map>.all(keyVar, valueVar, <predicate>) -> bool

exists

Tests if any element satisfies a predicate. Short-circuits on true.

• <list>.exists(indexVar, valueVar, <predicate>) -> bool
• <map>.exists(keyVar, valueVar, <predicate>) -> bool

exists_one

Tests if exactly one element satisfies a predicate. Does not short-circuit.

• <list>.existsOne(indexVar, valueVar, <predicate>)
• <map>.existsOne(keyVar, valueVar, <predicate>)

transformList

Converts a list or map into a new list. Supports optional filtering.

• <list>.transformList(indexVar, valueVar, <transform>)
• <list>.transformList(indexVar, valueVar, <filter>, <transform>)
• <map>.transformList(keyVar, valueVar, <transform>)
• <map>.transformList(keyVar, valueVar, <filter>, <transform>)

transformMap

Converts a list or map into a new map. The key remains fixed from the source, while the value is transformed. Supports optional filtering.

• <list>.transformMap(indexVar, valueVar, <transform>)
• <list>.transformMap(indexVar, valueVar, <filter>, <transform>)
• <map>.transformMap(keyVar, valueVar, <transform>)
• <map>.transformMap(keyVar, valueVar, <filter>, <transform>)

transformMapEntry

Converts a list or map into a new map where the transform expression must be a map literal (e.g., {key: value}). If the transform produces duplicate keys, it will error.

• <list>.transformMapEntry(indexVar, valueVar, <transform>)
• <list>.transformMapEntry(indexVar, valueVar, <filter>, <transform>)
• <map>.transformMapEntry(keyVar, valueVar, <transform>)
• <map>.transformMapEntry(keyVar, valueVar, <filter>, <transform>)

// all example
[1, 2, 3].all(i, j, i < j) // true

// transformList example
[1, 2, 3].transformList(i, v, (i * v) + v) // [1, 4, 9]

// transformMapEntry example
{'greeting': 'hello'}.transformMapEntry(k, v, {v: k}) // {'hello': 'greeting'}