increase validator precision in an edge case

[cdisselkoen]

Description of changes

This PR is an alternate way to address the problem in #603. Instead of changing type_of_var_in_entity_literals() and type_of_entity_literal_in_entity_literals(), we merely change the definition of Type::must_be_specified_entity(), which will cause cases of X in [] to be short-circuited out (here) and never reach those functions in the first place. This causes X in [] to be typed False for all X, including unspecified X. This matches the behavior of the Dafny as far as I understand it.

The edge case where this changes validator behavior is only possible when [] is a valid expression, which is only true under Permissive validation, which is only an experimental feature in Cedar 3.x, so this is not considered a breaking change from semver perspective, and could be released in a patch or minor of Cedar 3.x.

Checklist for requesting a review

The change in this PR is (choose one, and delete the other options):

• A bug fix or other functionality change requiring a patch to cedar-policy.

I confirm that this PR (choose one, and delete the other options):

• Does not update the CHANGELOG because my change does not significantly impact released code.

I confirm that cedar-spec (choose one, and delete the other options):

• Does not require updates because my change does not impact the Cedar Dafny model or DRT infrastructure.

Disclaimer

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[khieta]

Unless I'm missing something, I don't think this does the same thing as #603 -- the must_be_specified_entity function is only used to type == expressions, not in expressions. I think what you want to update is the function euids_from_euid_literals_or_action.

[cdisselkoen]

must_be_specified_entity() is used in typecheck_in() here

[khieta]

Thanks, I was indeed missing something 🤦‍♀️

[khieta]

Approving now that my confusion is resolved.

I agree that this change adjusts the precision as expected & only affects permissive validation. I prefer this PR over #603 because it's easier to audit, but I think we also want some of the changes from #603. In particular, returning TypecheckFail in type_of_var_in_entity_literals seems unintentional & I think we should change it to TypecheckSuccess with a general Bool type.

[john-h-kastner-aws]

I agree with Kesha. This change is a nicer fix to the particular difference we saw with in DRT, but we should look at pulling in some of the changes from the other PR.

[cdisselkoen]

I will merge this, and iterate on #603 to keep only the changes that we want.