Strengthen testing of correctness of CST-AST desugarings

[mattmccutchen-amazon]

Category

New DRT target

Describe the feature you'd like to request

We should consider somehow strengthening our testing that the desugarings performed during CST-AST conversion have the semantic properties we want. The goal would be to prevent another issue like this one, where the desugaring messed up the evaluation order of > and >=. Whatever kinds of testing of these desugarings we currently have didn't seem to be sufficient. For example, we may have written a unit test that a > b desugars to b < a but not realized that our "expected output" didn't actually have all the properties we wanted.

Describe the solution you'd like

The most promising approach I can think of that would be able to catch evaluation-order issues with desugarings is to write another version of the evaluator that directly evaluates expressions in a format in which most of the desugarings have not yet been performed. The EST is probably close to what we want for this expression format. Then, for a given EST e, we could compare the result of directly evaluating e to the result of converting e to an AST and evaluating that.

There are a few ways that the components of this plan could be broken down between Rust and Dafny. A non-exhaustive list:

1. Do the whole thing in Rust and use DRT to compare the direct EST evaluation and the evaluation via EST-AST conversion.
2. Implement direct EST evaluation and EST-AST conversion in Dafny and prove that direct EST evaluation is equivalent to evaluation via EST-AST conversion. Then use DRT to test that the Dafny EST-AST conversion is equivalent to the production one.

Describe alternatives you've considered

Just fix cedar-policy/cedar#112, try to pay more careful attention when we add or change desugarings in the future, and hope for the best? I don't know how important the problem actually is.

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

[shaobo-he-aws]

One low hanging fruit we can do is to prove the equivalence after desugaring in Dafny. For instance, one proposed solution in #112 is to desguar a < b into !(a >= b), which we can prove something like eval(a < b) == eval(!(a >= b)).