Formalize the desugaring of when/unless clauses

[aaronjeline]

Category

Dafny formalization, Lean formalization

Describe the feature you'd like to request

Currently a Cedar policy is represented with its condition clause being an arbitrary expression. This is not how users write policies, they break the expression up into (potentially multiple) when/unless clauses. Currently the spec does not detail how that desugaring happens, so it's implicit whether multiple clauses are anded or ored together. This should be a part of the formal spec.

Describe alternatives you've considered

Leave as is

Additional context

Due the engineering details on the DRT, it's not possible at the moment to test this, however, if in the future DRT moves to using the EST format, it will be.

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

[john-h-kastner-aws]

Sub task for #42