Deprecate Dafny formalization

[khieta]

Issue #, if available:

Description of changes:

This PR completes the port to Lean proposed in rfc#32 🎉

In particular, it:

• Deletes the Dafny formalization, related CI, and build instructions
• Undoes the code duplication introduced in Lean fuzz targets #170. Example: this PR deletes abac.rs (the Dafny target) and merges abac_shared.rs and abac-lean.rs to become the new abac.rs.
• Deletes the DRT targets for permissive validation, which is an experimental feature that is not yet modeled in Lean.

The Dafny formalization will continue to live on in prior release/* branches of cedar-spec.

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

[cdisselkoen]

🎉

[cdisselkoen]

are we dropping the non-type-directed validation target? IMO this is an important target, because many categories of errors which we want to test the validator(s) on, cannot be generated by the type-directed generators

[shaobo-he-aws]

Another related question: Is our principle to use PBT when there's no formalization? If it is, we should remove any target about permissive validation.

[khieta]

The validation targets we currently have are:

• Type-directed DRT for permissive validation (Dafny only)
• Non-type-directed DRT for permissive validation (Dafny only)
• Type-directed DRT for strict validation (Dafny and Lean)
• Non-type-directed PBT for type soundness

The current PR proposes:

• Type-directed DRT for strict validation (Lean only)
• Non-type-directed PBT for type soundness

@cdisselkoen are you proposing we add a non-type-directed variant for strict validation? This seems fine, but I think the reason we didn't have it in the first place was that the non-directed variant didn't end up finding any bugs in the permissive case. Should we also add a type-directed variant for PBT?

@shaobo-he-aws are you suggesting we remove the PBT target? It sort of feels redundant since we have proved type soundness, but possibly this target could help find cases where the Rust validator is unsound (and thus different from the spec).

[shaobo-he-aws]

I meant we should remove any DRT targets related to permissive validation since it's not proved in Lean. We should keep the corresponding PBT targets. And the PBT target for strict validation is not needed, in my opinion.

[mwhicks1]

If we don't drop it, I think we should change the PBT for validator soundness to be type-directed instead. It doesn't make sense to test validator soundness using (mostly) invalid inputs. The property is "if validate(P) then evaluate(P) does not error". But the non type-directed generator is mostly going to be generating "P" such that "validate(P)" is false, which is not helpful at testing the property -- those inputs will be effectively thrown away. I realize it was this way with the Dafny, and it didn't make sense then either. :) This should be an easy change to make.

But I also agree with Shaobo we should think about why we even have this property, given that we have proved it sound in Lean and have DRT to check that Lean and Rust versions agree.

[khieta]

I'll lean towards "more testing is better" here, and update our code to include both type-directed and non-type-directed targets for both the DRT and PBT targets.

[shaobo-he-aws]

Maybe we should tag the version before completely deleting Dafny stuff. Just make it easier to look the Dafny code up.

[cdisselkoen]

Personally I think the 3.0.x branch is a good place to look the Dafny code up

[khieta]

Maybe we should tag the version before completely deleting Dafny stuff

I also think the release/3.0.x branch is sufficient. There is a small diff in the json parsing code between release/3.0.x and the current main, but everything else is unchanged.

[shaobo-he-aws]

Sounds good. Should we add it to the README as well?

[mwhicks1]

It seems a shame not to be diff-testing the permissive validation in Dafny, which was proved sound, against the permissive validation we have now in Rust. It is a feature that customers can use now. Why not test it? Put another way: What's the hurry to clear away the Dafny?

[khieta]

It seems a shame not to be diff-testing the permissive validation in Dafny

We will continue to test the Rust permissive validation against the Dafny spec for versions <= 3.0. It's true that this testing won't capture new changes to the Rust permissive validator, but it seems worth the tradeoff to not have to maintain the entire Dafny formalization. If we do end up making changes to the permissive validator in an effort to stabilize it, then it's worth modeling in Lean anyways 😉

[khieta]

Updated the PR to include both type-directed and non-type-directed targets for validation DRT and PBT.

While making this edit I introduced some additional code duplication in our targets, but we have similar duplication in other places, so I filed an issue to cleanup in the future (#220) rather than fixing in this PR.