TPE: Further simplify error-free residual expressions whose value can be deducted

[luxas]

Category

Internal refactors/changes -- consider "Internal improvement" instead of "Feature request"

Describe the feature you'd like to request

As a follow-up to #2091, I'm wondering if it's possible and/or worth it to further simplify TPE error-free expressions, even in presence of partially-known data.

For example,

• After the validator has done its pass, it might assign the singleton True or False types to (sub-)expressions. However, we don't use this information when converting from Expr<Option<Type>> to Residual today, although that could prune some part of the residual in a sound manner, right?
  • As a concrete example, the validator is able to deduce that e.g. principal has nonexistentfield is False (and its negation true). However, one can replace this with false/true, again, only when we know the expression is error-free, as e.g. also principal.num + 1 == 2 && principal has nonexistentfield has singleton type False, but could error.
• If the ancestors of entity1 in <entity1> in [<entity2>, <entity3>, ...] is not known, only equality between entity1 and entity2 is checked, and not e.g. whether entity1 and entity3 are equal. This means that User::"alice" in [User::"bob", User::"alice"] is not reduced to true when the ancestors of User::"alice" are not known, even if that information is not needed to assign a truth value. Note that this is done only when all <entity_i> are concrete, so no errors can happen.
• Right now, it seems like type information is not at all used in the Evaluator (see this PoC). Maybe one place it could be used, is to fold <error-free-t1> == <error-free-t2> of distinct types into false. This would not work if the LHS or RHS could error, as then the error would need to be propagated upwards instead and thus cannot be replaced.
• Similarly, it seems like the following special cases could be reduced (although not super likely):
  • <error-free> in [] => false
  • [].contains(<error-free>) => false
  • <error-free>.containsAny([]) => false
  • [].containsAny(<error-free>) => false
  • <error-free>.containsAll([]) => true
  • [].containsAll(<error-free>) cannot be deduced, as <error-free> could evaluate into [] => true or [a, b, c, ...] => false.
• Not very likely to happen, and maybe not worth implementing, but if <error-free> then <res> else <res> is <res>, if both Residual cases (concrete or partial) are equal. Eq is not implemented for Residual at the moment, was this due to some specific reason or just not needed so far? Are there worries that expression comparisons could be too expensive to perform in this case?
• <error-free> like "*" => true

Any thoughts on the following? These are some of the rewrites I came to think of, but maybe there are more.
Would be interesting to hear your thoughts @emina @john-h-kastner-aws

Describe alternatives you've considered

Not implement these in core, defer to downstream users. I already implemented <error-free> like "*" => true for the Kubernetes use-case (right now, by disallowing users to write such expressions), as that would otherwise be a pretty big gotcha for users, given how I implemented things right now.

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

[john-h-kastner-aws]

After the validator has done its pass, it might assign the singleton True or False types to (sub-)expressions.

This might be annoying to prove correct because the current Lean model of TPE "lifts" boolean singletons to the regular boolean type. I'm not aware of the reason for this design, but it could get tricky.

If the ancestors of entity1 in in [, , ...] is not known, only equality between entity1 and entity2 is checked, and not e.g. whether entity1 and entity3 are equal.

This sounds like it should be correct, and feels reasonably likely to be a useful simplification in practice if anyone is using entity in [e1, e2...] as a short hand for entity == e1 || entity == e2 ...

Right now, it seems like type information is not at all used in the Evaluator (see this PoC). Maybe one place it could be used, is to fold == of distinct types into false.

This feels like a simplification TPE really ought to be doing.

Given a partial request for an Application type entity, we really should be eliminate this whole policy.

permit(principal == User::"Alice", action, resource);

It's somewhat counter intuitive that this policy can't be reduced but we can reduce

permit(principal is User, action, resource);

This would be a subset of your first point on singleton boolean types, but could be handled separately if the "type lifting" done in the Lean model can't be worked around.

[john-h-kastner-aws]

Another simplification: getting an attribute of an error-free record-type residual is error free. (records don't have any issues with entity existence)

I don't think this is practically useful for current TPE because it should be very uncommon to have an attribute access on a record residual. It should only be possible given a record-literal in the policy text. E.g., {foo: resource has bar, baz: principal has buz}.baz[1]. If the record came from an entity or context attribute, then it currently must be value, so we can reduce it without applying any reasoning about error-free residuals.

However, I think this simplification becomes useful depending on how we implement #1735. If we implement it as an extension to TPE rather than a rewriting pass (which is the current preference), then we could have principal.foo.bar where principal is provided with an unknown foo attribute, so we would reduce to <r : {bar: Bool}>.bar which is an error-free expression, allowing us to eliminate the need to fetch foo at all if the policy can be reduced based on the existing && or || rules.

[1]: We could actually reduce this by noting that the residual in the foo attribute is error-free, giving us principal has buz, but I don't think this simplification is useful even with the extension to TPE.