Updates to Lean validator spec

[khieta]

Issue #, if available:

Description of changes:

The Lean formalization of strict validation has been out of sync with the Rust definition since release. This PR aims to resolve this by

1. Fixing two small issues in the Lean spec: adding a special "Unspecified" entity to the type store that has no attributes or ancestors, and encoding that actions cannot have ancestors attributes.
2. Changing the property tested by the strict-validation-drt-* targets. Now instead of testing whether the spec returns a validation error iff the Rust does, it will check that if the Rust validates, then the spec also validates (ignoring impossiblePolicy errors). This allows the Lean spec to be more precise than the Rust, which means that it may return the error impossiblePolicy where the Rust successfully validates, or may successfully validate when the Rust returns an error (e.g., because short-circuiting determined that some invalid code is unreachable).

The second change is the controversial one: we're weakening the property tested. See my comments in the code for why I think this is reasonable.

It may be possible to further edit the Lean to make it match the Rust, though some work is required. I've found at lease two other issues (listed below) through DRT. There are likely others.

• Lean typechecking of == is more precise than Rust (fixed in this branch).
• Rust returns a HierarchyNotRespected for some in expressions that the Lean successfully validates. Appears to be related to unspecified entities.

---

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[cdisselkoen]

Before I review in detail, one comment about the description: You say that we're weakening the strict-validation-drt property from

spec returns validation error iff Rust does

to

if Rust validates then spec does, ignoring ImpossiblePolicy

Why not a middle ground,

Rust validates iff spec does, ignoring ImpossiblePolicy

[cdisselkoen]

In particular, the middle property would be satisfied by a spec validator that always passes

[emina]

Two quick clarifications:

1. Fixing two small issues in the Lean spec: adding a special "Unspecified" entity to the type store that has no attributes or ancestors, and encoding that actions cannot have ancestors.

The code is not adding the Unspecified entity type to the spec but rather to the diff testing harness (DiffTest/Parser). I think this is right (we should indeed not add it to the spec), and want to confirm that we'll keep it this way :)

The code is preventing actions from having attributes. They can still have ancestors. I'm guessing this is a typo in the description.

2. Changing the property tested by the strict-validation-drt-* targets. Now instead of testing whether the spec returns a validation error iff the Rust does, it will check that if the Rust validates, then the spec also validates (ignoring impossiblePolicy errors). This allows the Lean spec to be more precise than the Rust, which means that it may return the error impossiblePolicy where the Rust successfully validates, or may successfully validate when the Rust returns an error (e.g., because short-circuiting determined that some invalid code is unreachable).

The second change is the controversial one: we're weakening the property tested. See my comments in the code for why I think this is reasonable.

I think this is quite reasonable. It gives us the freedom to eventually make the Rust validator as precise as the Lean validator, which seems more desirable than making Lean less precise to match Rust. If we instead make the Lean validator less precise to force equivalence with Rust today, then we'd have to change both Rust and Lean to recover that precision in the future.

[khieta]

Why not a middle ground,
Rust validates iff spec does, ignoring ImpossiblePolicy

Unfortunately precision differences affect more than just ImpossiblePolicy errors. Consider an expression like if ?? then 1 else (2 + true) If the Rust types ?? as Bool then it will flag the type error in the else branch. If the (more precise) Lean spec types ?? as True, then it will not flag the type error since it can guarantee that then branch will be taken.

So in general, the additional precision in Lean will result in fewer non-ImpossiblePolicy errors being reported.

[khieta]

The code is not adding the Unspecified entity type to the spec but rather to the diff testing harness (DiffTest/Parser). I think this is right (we should indeed not add it to the spec), and want to confirm that we'll keep it this way :)

Yes, I should have been more clear. This PR adds a special unspecified entity when parsing in the schema to match how the parser currently handles an unspecified principal/resource in requests. It does not add unspecified entities to the core formalization.

[khieta]

Last comment for now: the strict-validation-drt-type-directed-lean target ran successfully overnight on my local machine with these changes, so I have some confidence that this resolves the DRT target failure.

[mwhicks1]

This PR adds a special unspecified entity when parsing in the schema to match how the parser currently handles an unspecified principal/resource in requests. It does not add unspecified entities to the core formalization.

I don't understand why it should not be part of the formalization. Rust Cedar's semantics includes the notion of an "unspecified" entity. I don't think it's going anywhere. Not having it in the Lean spec implies it's not part of the "essence" of Cedar, e.g., a different implementation would not have to support it. Maybe that's fine, but then we miss an opportunity to vet the design of the Rust code via proof in Lean, to make sure that it's sensible, e.g., that validation is still sound in the presence of Unspecified entities in requests.