increase validator precision for some Unspecified cases
#603
Conversation
|
The current version of this PR is wrong, because |
|
Revised, hopefully the new code is the correct/ideal behavior. Looking for review. To answer one of the questions from the PR description, this (should be) a backwards-compatible change, because the only edge cases it changes behavior for involve |
There was a problem hiding this comment.
Motivated by this PR, I spent some time looking through the Rust code vs. the spec and I think the fix is actually simpler than what you have here: the Dafny function tryGetEUIDs returns None for an empty list while the corresponding Rust function euids_from_euid_literals_or_action returns Some([]). I think you can fix the behavior difference by just adjusting one of these functions to match the other.
| @@ -1916,7 +1916,10 @@ impl<'a> Typechecker<'a> { | |||
|
|
|||
| // Given an expression, if that expression is a literal or the `action` | |||
| // variable, return it as an EntityUID. Return `None` otherwise. | |||
| fn euid_from_euid_literal_or_action(request_env: &RequestEnv, e: &Expr) -> Option<EntityUID> { | |||
| fn euid_from_euid_literal_or_action<T: Clone>( | |||
There was a problem hiding this comment.
No problem with this generalization, but I don't see where it's necessary.
| ) | ||
| } else { | ||
| // nothing on the RHS can be unspecified, so `unspecified in RHS` is always false | ||
| TypecheckAnswer::success( |
There was a problem hiding this comment.
This might change strict validation for something like principal in [resource.owner] when principal is unspecified and resource.owner is some entity type.
There was a problem hiding this comment.
I think you're right. That doesn't mean this precision increase is invalid, just that it's currently breaking (unless/until we change ImpossiblePolicy from error to warning)
There was a problem hiding this comment.
Actually I'm not sure if you're correct. I believe principal in [resource.owner] when principal is unspecified and resource.owner is some entity type, might short-circuit out here and never reach this function at all.
There was a problem hiding this comment.
Agreed that earlier handling handles this case. But I'm not sure this new definition matches the spec -- the Dafny code will always return AnyBool in the case where the RHS cannot be converted to a list of Entity UIDs.
Description of changes
Increases validator precision (typing
Falseinstead ofBool) in some edge cases involvingUnspecified. Also, change fromTypecheckFailtoTypecheckSuccessin one of these edge cases in particular.This is a backwards-incompatible change unless/until
ImpossiblePolicyis moved from an error to a warning. We should probably not merge this until we've decided whether that will happen.The change in this PR is (choose one, and delete the other options):
Breaking, unless we wait to merge this until
ImpossiblePolicyis moved from an error to a warning, in which case non-breaking. I also only observed the impact of this change inPermissivevalidation mode, which is an experimental feature in 3.x. I'm not sure (not qualified to determine) whether this change has any impact inStrictvalidation mode, ie, on the stable 3.x validator.I confirm that this PR (choose one, and delete the other options):
I confirm that
cedar-spec(choose one, and delete the other options):cedar-spec. (Post your PR anyways, and we'll discuss in the comments.)I'm not sure whether this behavior matches the Lean validator, which doesn't yet fully match the Rust validator anyway. I believe that neither before nor after this PR will the behavior exactly match the Dafny validator, but I propose that this is the correct/ideal behavior, which we want Dafny to match? (That's a point for discussion below)
Disclaimer
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.