Skip to content

v0.14.0

Latest
Latest

Choose a tag to compare

View all tags
@l46kok l46kok released this 18 Aug 18:44
· 2 commits to main since this release
v0.14.0
5cf3ab3

This release officially introduces formal verification capabilities to CEL-Java, adds aggregate evaluation semantics to the CEL Policy Compiler, advances runtime modernization with the Program Planner, and brings key optimizer performance gains, conformance updates, and bug fixes.

🛡️ Formal Verification Framework

We are proud to announce the open-sourcing of the CEL Java Verifier (dev.cel:verifier and dev.cel:verifier-cli) (#1123, #1166). The verifier allows users to mathematically prove safety invariants, logical equivalence, satisfiability, and validity across CEL expressions and structured CEL Policies.

Key Verifier Capabilities

  • Logical Equivalence & Safe Refactoring: Statically prove that two ASTs or CEL Policies are semantically identical for all possible input states (#1123, #1125, #1164).
  • Satisfiability & Validity with Counterexample / Witness Generation:
    • isSatisfiable: Determines if an expression can ever evaluate to true and generates a concrete satisfying model (witness input) (#1127).
    • isAlwaysTrue: Mathematically proves validity and generates human-readable counterexamples when violations are detected (#1126, #1136, #1156, #1161, #1163).
  • Custom Policy Invariants Verification: Allows policy authors to declare assume preconditions and assert clauses in CEL YAML policies and prove that safety invariants are never violated (#1128, #1144).
  • Bounded Model Checking (BMC): Unrolls and verifies list and map comprehensions (all, exists, map, filter) up to configurable unroll limits (#1129, #1132, #1174).
  • Rich Type Reasoning: Supports cross-type numeric comparisons (#1124), timestamp and duration arithmetic/axioms (#1153), optional types and traversal (#1131, #1135, #1138, #1146), uninterpreted conversions (#1154, #1155), and JSON unwrapping (#1147).
  • Interactive CLI & REPL Tool: Available as a standalone executable JAR (dev.cel:verifier-cli) and interactive REPL shell for ad-hoc inspection and CI/CD validation (#1159, #1160, #1168).

🚀 Highlights & New Features

  • Aggregate Semantics in CEL Policy: Added support for aggregate policy rules to the CEL Policy Compiler according to the CEL Policy Specification (#1052, #1175), #1187). Aggregate rules evaluate all matching rules (including nested subrules) and collect results into a flattened list with support for optional pruning.
  • Shorthand Type Specifiers for Policy Configurations: Added support for inline shorthand type specifiers in CEL environment YAML configs (#1185), allowing parameterized types such as map<string, int>, list<string>, and optional<T> to be declared as compact strings rather than verbose nested YAML structures.
  • Protobuf Message Constant Folding: ConstantFoldingOptimizer now supports inlining evaluated Protobuf messages into structured message literal AST nodes, preserving field values and nested messages (#1116).
  • Parser Expression Node Limits: Added configurable node limits during parsing to prevent deeply nested or malicious expressions from exhausting resources (#1148).

⚙️ Runtime & Optimizer Improvements

  • Planner Migration & Default Documentation: Documentation and CEL-Java codelabs have been updated to make the Program Planner the default recommendation (#1109). Standard CEL builders have shifted to proxy the legacy runtime (#1110), and the Lite Runtime has also been migrated to the Program Planner (#1119).

    ⚠️ Deprecation Notice: The legacy runtime will be deprecated in the next release. Callers are strongly urged to migrate to the Program Planner.

  • Pre-Order Constant Folding: Switched constant folding optimizer traversal from post-order to pre-order (#1097). By traversing top-down, the optimizer avoids evaluating and visiting subtrees that can already be folded or pruned at higher ancestor nodes, resulting in significant performance speedups on large ASTs.
  • Optional Macro & Aggregate Literal Folding: Added constant folding support for optional macro calls (#1105) and aggregate literal pruning (#1106).
  • Optimization Helpers & Validation: Introduced common helpers for fixed-point optimization passes and AST navigation (#1170, #1176), and added a validation pass to ensure AST ID uniqueness across optimizers (#1178).

🐛 Bug Fixes & Correctness

  • Program Planner Partial Evaluation: Fixed a bug in the execution plan to properly handle AccumulatedUnknowns during partial evaluation (#1158).
  • Constant Folding Fixes:
    • Fixed ConstantFoldingOptimizer to not treat true && dyn_x as a tautology (#1133).
    • Prevented folding x in [x] for dynamic and double-typed variables to preserve correct numeric equivalence semantics (#1162).
  • Macro Iteration Variable Validation: Stricter validation for iteration variables in standard macros (all, exists, map, filter) to disallow identifiers starting with . and prevent collisions with internal __result__ accumulator variables (#1096).
  • Conformance & Type Fixes:
    • Fixed conformance issues around type conversion overflows and duration subtractions (#1151).
    • Fixed parsed-only conformance test cases for receiver function names containing reserved keywords (#1152).
  • Optional Target Handling: Avoided unnecessary copying of complex targets in optMap and optFlatMap (#1149).

👏 New Contributors

  • @stanleyhy made their first contribution adding Protobuf constant folding (#1116) and fixing AccumulatedUnknowns handling in the planner (#1158).

Full Changelog: v0.13.1...v0.14.0

Assets 2
Loading