Test typechecking for expressions in addition to policy validation

[john-h-kastner-aws]

Category

DRT target(s)

Describe the feature you'd like to request

Our current validation test targets looks at the whole validation routine, but this might not as effective at testing the details of the expression typechecking function as a target that tested it directly. The proposed test target would be similar to the eval-type-directed target, but testing validation instead of evaluation.

• Property Test Target: We generate an arbitrary schema, expression, and request. If the expression has type T, then when can evaluate it to a value which has type T.
• Differential test target: We generate an arbitrary schema, expression, and request. We then assert that the Rust and Lean implementations agree on the type for the expression.

If we add these targets we might be able to substantially simplify the existing validation targets in the style of rbac-authorizer. The validation targets would not need to test the details of expression typechecking and could instead focus on testing the validation logic for combining typechecking results between different policies and request type environments.

Describe alternatives you've considered

.

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