TPE: reduce has/hasTag/==/in/is using schema type information - #2503
TPE: reduce has/hasTag/==/in/is using schema type information#2503john-h-kastner-aws wants to merge 4 commits into
Conversation
Signed-off-by: jkastner <jkastner@amazon.com>
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 96.00% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 88.38% Status: PASSED ✅ Details
|
Signed-off-by: jkastner <jkastner@amazon.com>
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 96.00% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 88.39% Status: PASSED ✅ Details
|
| ResidualKind::BinaryApp { op, arg1, arg2 } => { | ||
| let arg1 = self.interpret(arg1); | ||
| let arg2 = self.interpret(arg2); | ||
| let must_be_false = match op { |
There was a problem hiding this comment.
This starts looking a lot like the abstract interpretation I was planning in #2122
There was a problem hiding this comment.
I think the difference is that here we determine that it must be a single value, allowing us to reduce to a concrete value instead of a residual. For #2122, we'll still be carrying around a residual so we can materialize the specific value of we need to
| _ => false, | ||
| }; | ||
| if must_be_false | ||
| && !arg1.can_error_assuming_well_formed() |
There was a problem hiding this comment.
One optimization that comes to mind here, would be to not interpret arg1 and arg2, but just check their can_error_assuming_well_formed in the original form, to potentially save some time.
It came to mind now, so I'll ponder about the soundness a bit more, but especially if I rename this to is_error_free_assuming_well_typed or similar, I believe it should be such that if the residual was error-free before interpretation (which is what we care about), then it necessarily also has to be error-free after interpretation (and thus interpretation is unnecessary if we can deduce this).
In other words, is_error_free_assuming_well_typed should be monotonic. This would be a pretty good theorem to add to the Lean code, unless we already have it.
There was a problem hiding this comment.
There's a trade off here: partial evaluation should very often give us back an error free expression where we didn't have one before. So, by checking on the residual we get to apply the reduction in more cases.
I suppose we could check it before and after reduction if that's a meaningful optimization.
There was a problem hiding this comment.
The monotonicity theorem, I think there would be something new to prove
We have (omitting welltypedness hypothesis)
∀ r req es, r.ErrorFree → (r.evaluate req es).isOk∀ r req es, (r.evaluate req es).toOption = ((TPE.evaluate r preq pes).evaluate req es).toOption
Given r.ErrorFree, we know ∀ r req es, ((TPE.evaluate r preq pes).evaluate req es).isOk. But ErrorFree isn't complete, so we'd need to show that ErrorFree actually holds for it.
Really, what we care about is the isOk result. That's what makes the reduction sound, so I don't think adding this theorem is particularly useful, but it could be fun if you want to try it out.
| } else if let Ok(uid) = value.get_as_entity() { | ||
| match self.entities.get_attrs(uid) { | ||
| Some(attrs) => mk_concrete(attrs.contains_key(attr).into()), | ||
| None => mk_residual(ResidualKind::HasAttr { |
There was a problem hiding this comment.
Add a comment here to follow-up on resolving the presence or non-presence of required attributes from the schema?
| @"false" | ||
| ); | ||
| assert_snapshot!( | ||
| interpret_typed_str_to_str(r#"E::"none_tags".hasTag("s") && E::"none_tags".getTag("s") == "bar" "#), |
There was a problem hiding this comment.
@luxas This demonstrates the && case for typechecking I commented on above.
E::"none_tags".hasTag("s") has type False, so we skip the RHS. The typechecker won't reduce it to false (due to error semantics, but also that's probably not the expected behavior for a typecheker), so we're left with the LHS, dropping the && RHS
Co-authored-by: Lucas Käldström <luxas@users.noreply.github.com>
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 96.00% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 88.39% Status: PASSED ✅ Details
|
Coverage ReportHead Commit: Base Commit: Download the full coverage report. Coverage of Added or Modified Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 95.95% Status: PASSED ✅ Details
Coverage of All Lines of Rust CodeRequired coverage: 80.00% Actual coverage: 88.39% Status: PASSED ✅ Details
|
2 participants
Description of changes
Fixes #2500
Lean model and proofs in cedar-policy/cedar-spec#997
Issue #, if available
Checklist for requesting a review
The change in this PR is (choose one, and delete the other options):
cedar-policy(e.g., changes to the signature of an existing API).cedar-policy(e.g., addition of a new API).cedar-policy.cedar-policy-core,cedar-validator, etc.)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, and how you have tested that your updates are correct.)cedar-spec. (Post your PR anyways, and we'll discuss in the comments.)I confirm that
docs.cedarpolicy.com(choose one, and delete the other options):cedar-docs. PRs should be targeted at astaging-X.Ybranch, notmain.)