Resolve known mismatch in definitional validator

[khieta]

Category

Dafny formalization

Describe the feature you'd like to request

The cedar-policy validator will always return an error for an unrecognized entity or action, even if that part of the expression should be excluded from typechecking (e.g., true || Undefined::"foo" should be well typed due to short-circuiting). The definitional validator currently does not have this behavior. We should need to decide which behavior we think is correct and then fix either the cedar-policy validator or the definitional validator. We then also need to remove this piece of code that hides this difference during DRT.

Describe alternatives you've considered

No response

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