Updates for cedar-spec#219

[khieta]

Description of changes

Updates comments to use "formal model" in places where we previously used "Dafny model". cedar-spec#219 deprecates the Dafny model in favor of a model in Lean.

I'm not sure if the alternate serialization used in cedar-policy-core/src/ast/pattern.rs is still needed now that we've switched Lean, but what we have now works so I'm hesitant to change it.

There is one other place we refer to "Dafny" in the code -- I've made an issue (#638) to follow up on that later.

Issue #, if available

Checklist for requesting a review

The change in this PR is (choose one, and delete the other options):

• A change "invisible" to users (e.g., documentation, changes to "internal" crates like cedar-policy-core, cedar-validator, etc.)

I confirm that this PR (choose one, and delete the other options):

• Does not update the CHANGELOG because my change does not significantly impact released code.

I confirm that cedar-spec (choose one, and delete the other options):

• Does not require updates because my change does not impact the Cedar Dafny model or DRT infrastructure.

Disclaimer

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

[shaobo-he-aws]

I'm not sure if the alternate serialization used in cedar-policy-core/src/ast/pattern.rs is still needed now that we've switched Lean, but what we have now works so I'm hesitant to change it.

We should keep it unless we change the deserializer in Lean, which I doubt will be an easy task given JSON doesn't have a character type.