Bump dev.cel:cel from 0.13.1 to 0.14.0

[dependabot]

Bumps dev.cel:cel from 0.13.1 to 0.14.0.

Release notes

Sourced from dev.cel:cel's releases.

v0.14.0

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.

• Read the Announcement Blog Post: Securing the Agentic Era: Introducing Formal Verification for CEL
• Watch the Video Demo: YouTube Video Walkthrough
• Read the Documentation: CEL Java Verifier README & CLI/REPL Guide

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

... (truncated)

Commits

• 5cf3ab3 Prepare 0.14.0 release
• 849cb3e Avoid concatenating superfluous empty list for aggregate semantics
• 05bf69c Add shorthand type specifier syntax for policy configs
• e13bec5 Add block_ext to conformance test suite, refactor to consolidate cel.block ov...
• e5c1466 Remove CelOptimizerOptions
• 496434e Handle custom functions returning unknowns in planner
• 1ba7cc7 Default enable AST validation in optimizers
• 30f8e6d Add a validation pass for ID uniqueness in optimizers
• 94ba8ad Consolidate emit to output for aggregate policies
• f847b0c Internal Changes
• Additional commits viewable in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)