Tracking issue: Collecting use-cases for `any` and `all` operators

[luxas]

Category

Cedar language or syntax features/changes

Describe the feature you'd like to request

Supporting any and all has been requested every now and then (e.g. #1920 and on Slack) and discussed in length in cedar-policy/rfcs#21, cedar-policy/rfcs#43, and cedar-policy/rfcs#65.

However, since those discussions, this FMCAD article was published, and initial support for a limited set.filter operator was added to cvc5 (although experimental), from which one can build all/any. Alternating quantifiers cannot be supported, but a single all or any quantifier or a list of all quantifiers might be supported (with no set terms in the predicate(s)).

This would still require extensive effort both in Cedar and most likely cvc5, and it might take some time before the SMT community feels like such a primitive could move out from experimental mode. However, there might be a little bit of a "chicken and egg" situation here where the SMT solvers/community need practical, realistic benchmarks and unit tests to gain confidence in the solving correctness and performance, but users like Cedar would hold off building on top of this feature until stable. Hence, let's discuss whether we can avoid such a dependency loop.

However, I open this issue as a tracking one in hope to collect user feedback on what practical use-cases would be useful to support, if this was added at some point in the future.

Describe alternatives you've considered

• Not implementing this in Cedar at all.
• Force users to wrap any such quantifiers through an extension function (Let users register their own extension functions? #2126) or some auxiliary boolean, at the expense of occasional false alarms in Cedar Analysis.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change