TPE: Simplify <residual> && false to false when <residual> cannot error

[luxas]

Description of changes

Adds a method that determines if a residual can produce runtime errors that the validator would not already warn the user about (hence the "well-typed" assumption). See #1895 for further discussion. The function could be made slightly more precise by indicating what extension functions can and cannot error.

The "can error" method is used to simplify <residual> && false to false and <residual> || true to true when <residual> cannot error. Simplification cannot be done when the residual could error.

Reviewer Notes

Note that there are lots of typing errors that can be thrown by Evaluator.interpret on arbitrarily constructed Residuals. So do you prefer

a) Making Residual construction private, so it can only be constructed by the typechecker after a successful pass, or
b) Somehow trying to inline what the validator would do in Evaluator.interpret every time we need to know if a sub-expr is well-formed or not (complex and seems slow), or
c) Keep the behavior undefined for anyone that constructs semantically invalid Residuals (seems dangerous)

I guess I lean towards a), at least until we know if anyone needs those enums to be public.

In addition, I think it'd be a good idea to use separate Residual::Error in to Residual::TypeError and Residual::RuntimeError, where Residual::TypeErrorshould never happen (if validator is sound), butResidual::RuntimeErrorcould indeed. This might be a good time to add the same context toResidual::RuntimeError` as for normal evaluation (#1736).

Issue #, if available

Fixes: #1895
(or at least gets us some way towards that goal)

Checklist for requesting a review

The change in this PR is

• A change (breaking or otherwise) that only impacts unreleased or experimental code.

I confirm that this PR

• Updates the "Unreleased" section of the CHANGELOG with a description of this change.

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

• Requires updates, @john-h-kastner-aws was looking at those already.

I confirm that docs.cedarpolicy.com (choose one, and delete the other options):

• Does not require updates because my change does not impact the Cedar language specification.

[luxas]

Are there other cases than these, or gaps in the validator coverage that I'd need to know about?

[github-actions]

Coverage Report

Head Commit: 918bdc615d78a2b2d2317488ef8b1833f5923e0c

Base Commit: 2d6b09538777f874cc3c8d8eb1c1ad622afe37bc

Download the full coverage report.

Coverage of Added or Modified Lines of Rust Code

Required coverage: 80.00%

Actual coverage: 98.46%

Status: PASSED ✅

Details

File	Status	Covered	Coverage	Missed Lines
cedar-policy-core/src/tpe/evaluator.rs	🟢	30/30	100.00%
cedar-policy-core/src/tpe/residual.rs	🟢	34/35	97.14%	93

Coverage of All Lines of Rust Code

Required coverage: 80.00%

Actual coverage: 86.15%

Status: PASSED ✅

Details

Package	Status	Covered	Coverage	Base Coverage
cedar-language-server	🟢	4724/5106	92.52%	92.52%
cedar-policy	🟡	3765/5146	73.16%	73.16%
cedar-policy-cli	🔴	767/1193	64.29%	64.29%
cedar-policy-core	🟢	22062/25361	86.99%	86.96%
cedar-policy-formatter	🟢	906/1080	83.89%	83.89%
cedar-policy-symcc	🟢	6341/6853	92.53%	92.53%
cedar-wasm	🔴	0/28	0.00%	0.00%

[github-actions]

Coverage Report

Head Commit: 0ffea1fcd683ca4db41d34adf9d7393447806580

Base Commit: 2d6b09538777f874cc3c8d8eb1c1ad622afe37bc

Download the full coverage report.

Coverage of Added or Modified Lines of Rust Code

Required coverage: 80.00%

Actual coverage: 98.46%

Status: PASSED ✅

Details

File	Status	Covered	Coverage	Missed Lines
cedar-policy-core/src/tpe/evaluator.rs	🟢	30/30	100.00%
cedar-policy-core/src/tpe/residual.rs	🟢	34/35	97.14%	93

Coverage of All Lines of Rust Code

Required coverage: 80.00%

Actual coverage: 86.15%

Status: PASSED ✅

Details

Package	Status	Covered	Coverage	Base Coverage
cedar-language-server	🟢	4724/5106	92.52%	92.52%
cedar-policy	🟡	3765/5146	73.16%	73.16%
cedar-policy-cli	🔴	767/1193	64.29%	64.29%
cedar-policy-core	🟢	22062/25361	86.99%	86.96%
cedar-policy-formatter	🟢	906/1080	83.89%	83.89%
cedar-policy-symcc	🟢	6341/6853	92.53%	92.53%
cedar-wasm	🔴	0/28	0.00%	0.00%

[john-h-kastner-aws]

This and getTag are the other important cases. They will error if the target entity isn't in the entity data.

[john-h-kastner-aws]

These also gets at some tricky cases around optional attributes. The type annotated AST doesn't carry the capability information used to check that optional attributes will be present, so just having a locally well typed resdiual isn't enough to guarantee that there will never be an unknown attribute error. (the residuals resulting from typechecking will satisfy this property, but it's trickier to show that is holds for the residual resulting from partial eval).

[luxas]

This is why I was suggesting that the only way to construct a Residual (even in cedar-policy-core) would be from an Expr that has been validated. For such a Residual, the validator made sure through its capabilities that any getAttr or getTag present (in any sub-expr of the root) cannot error, right? Even (and especially) if the attribute is optional.

This is why I am suggesting to narrow down how Residuals can be constructed (even in cedar-policy-core), so that we can uphold the invariant that getAttr or getTag can never error, as any Residual instance had to necessarily pass validation even before becoming constructed.

[john-h-kastner-aws]

The optional attribute point is just an aside. It doesn't impact correctness, just makes it a pain to prove.

The real issue is that getTag and getAttr will both error whenever the entity they access doesn't exist. This is slightly subtle for TPE since the missing entity is initially treated as an unknown value (resulting in a non-concrete residual rather than an error), but when we go to concretely evaluate the residual, it's still an error if the data for the entity isn't present.

Validation doesn't do anything to guard against this sort of error. It's just one of the gaps in it's soundness theorem.

[luxas]

Right, you were thinking about errors from concrete reauthorization too; I was only thinking about whether TPE itself could produce errors, which getTag and getAttr would not (a missing entity would just yield another residual). Good catch. That limits the usefulness of this rewrite quite a bit, hmm...

To some extent, that type of error "feels different" though, in that the schema "promised" that all entity references could be followed, but the implementation did not live up to that promise. Maybe one way to find a middle-ground here would be to let the implementation (the TPE Evaluator) provide (or not) explicitly whether it guarantees that all referenced entities exist, or if it cannot guarantee this.

However, this PR (even if I add that these operators can error too) gets us some of the way, and most likely the possible_bool_outcomes described in #1895 (comment) gets us the rest of the way for those users that do not care about the error precision between false and error for permit policies, for example.

[john-h-kastner-aws]

The fact that getAttr can error definitely limits the usefulness of this optimization since it folding away an attribute access to eliminate the need to fetch that entity data is exactly what I'd ideally want it to do.

I guess this just points us towards looking at the PossibleBoolOutcome idea or changing the auth algorithm to account for the possibility of errors.

[john-h-kastner-aws]

To some extent, that type of error "feels different" though, in that the schema "promised" that all entity references could be followed, but the implementation did not live up to that promise. Maybe one way to find a middle-ground here would be to let the implementation (the TPE Evaluator) provide (or not) explicitly whether it guarantees that all referenced entities exist, or if it cannot guarantee this.

There's a possibility of something like this, probably by using level-based policy validation and entity slicing as a pre-condition, but I don't think we'll want to make this change too quickly.

[luxas]

folding away an attribute access to eliminate the need to fetch that entity data is exactly what I'd ideally want it to do

Yes, this exactly 👍

There's a possibility of something like this, probably by using level-based policy validation and entity slicing as a pre-condition, but I don't think we'll want to make this change too quickly.

Cool, let's discuss this separately then in #1895 or a new after we've merged this initial optimization.

I'll make the change for getAttr and getTag next. Should I also rename the From<Expr<Option<Type>>> for Residual "constructor" and make Residual(Kind) private (as per option a above), and instead add the constructor tpe::make_residual(e: Expr, req: &PartialRequest, s: &ValidatorSchema) -> Result<Residual, TpeError> that makes sure Evaluator::interpret is always sound? (If not, the interpret function would be unsound on Residuals that are not validated)

[john-h-kastner-aws]

Note that there are lots of typing errors that can be thrown by Evaluator.interpret on arbitrarily constructed Residuals. So do you prefer

...
c) Keep the behavior undefined for anyone that constructs semantically invalid Residuals (seems dangerous)

We're fine with (c) so long as you're talking about the behavior when calling cedar-policy-core directly. The cedar-policy API should rule out this sort of error, and to my knowledge it does.

In other words, our point of view is that we're doing (a) (keeping the constructor private) as long as it's not exported from cedar-policy.

[john-h-kastner-aws]

for other reviewers: a partial Lean proof of this simplification is in this branch https://github.com/cedar-policy/cedar-spec/tree/tpe_and_false

The proof is complete (no sorrys) for the part of this optimization it implements, but it only implements the simplification for &&, and it has a narrower definition of non-erroring expressions. We'll need to extend it to match this PR, but it's enough to be confident that the simplification is correct (up to the issue with GetAttr and GetTag)

[john-h-kastner-aws]

looks like this line isn't covered by any tests. Seems worth writing one

[luxas]

In other words, our point of view is that we're doing (a) (keeping the constructor private) as long as it's not exported from cedar-policy.

See my comment #2091 (comment); I was thinking to make the Residual constructor even more private (even in cedar-policy-core), such that it can only be constructed from an Expr, PartialRequest and a Schema, e.g. tpe::make_residual(e: Expr, req: &PartialRequest, s: &ValidatorSchema) -> Result<Residual, TpeError>. The validator thus ensures that getAttr and getTag can never error at anywhere in the residual constructed this way. Could this be proved to be the case also in the Lean model?