Updates for cedar-spec#219 (#639)

.github/PULL_REQUEST_TEMPLATE.md

@@ -19,7 +19,7 @@ I confirm that this PR (choose one, and delete the other options):
 
 I confirm that [`cedar-spec`](https://github.com/cedar-policy/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.
+- [ ] Does not require updates because my change does not impact the Cedar formal model or DRT infrastructure.
 - [ ] Requires updates, and I have made / will make these updates myself. (Please include in your description a timeline or link to the relevant PR in `cedar-spec`, and how you have tested that your updates are correct.)
 - [ ] Requires updates, but I do not plan to make them in the near future. (Make sure that your changes are hidden behind a feature flag to mark them as experimental.)
 - [ ] I'm not sure how my change impacts `cedar-spec`. (Post your PR anyways, and we'll discuss in the comments.)

cedar-policy-core/src/ast/pattern.rs

@@ -20,11 +20,10 @@ use serde::{Deserialize, Serialize};
 
 /// Represent an element in a pattern literal (the RHS of the like operation)
 #[derive(Deserialize, Hash, Debug, Clone, Copy, PartialEq, Eq)]
-// We need special serialization implementation for CedarDRT because Rust's
-// unicode escape sequences (e.g., `\u{1234}`) can appear in serialized strings
-// and it's difficult to parse them into Dafny characters.
-// Instead we serialize the unicode values of Rust characters and leverage
-// Dafny's type conversion to retrieve the characters.
+// We need special serialization for patterns because Rust's unicode escape
+// sequences (e.g., `\u{1234}`) can appear in serialized strings and it's difficult
+// to parse these into characters in the formal model. Instead we serialize the
+// unicode values of Rust characters.
 #[cfg_attr(not(feature = "arbitrary"), derive(Serialize))]
 #[cfg_attr(feature = "arbitrary", derive(arbitrary::Arbitrary))]
 pub enum PatternElem {
@@ -42,13 +41,13 @@ impl Serialize for PatternElem {
     {
         // Helper enum for serialization
         #[derive(Debug, Serialize)]
-        enum PatternElemForDafny {
+        enum PatternElemU32 {
             Char(u32),
             Wildcard,
         }
         match self {
-            Self::Char(c) => PatternElemForDafny::Char(*c as u32).serialize(serializer),
-            Self::Wildcard => PatternElemForDafny::Wildcard.serialize(serializer),
+            Self::Char(c) => PatternElemU32::Char(*c as u32).serialize(serializer),
+            Self::Wildcard => PatternElemU32::Wildcard.serialize(serializer),
         }
     }
 }

cedar-policy-core/src/authorizer.rs

@@ -91,7 +91,7 @@ impl Authorizer {
 
     /// Returns an authorization response for `q` with respect to the given `Slice`.
     ///
-    /// The language spec and Dafny model give a precise definition of how this is
+    /// The language spec and formal model give a precise definition of how this is
     /// computed.
     pub fn is_authorized(&self, q: Request, pset: &PolicySet, entities: &Entities) -> Response {
         match self.is_authorized_core(q, pset, entities) {
@@ -157,7 +157,7 @@ impl Authorizer {
     /// Returns an authorization response for `q` with respect to the given `Slice`.
     /// Partial Evaluation of is_authorized
     ///
-    /// The language spec and Dafny model give a precise definition of how this is
+    /// The language spec and formal model give a precise definition of how this is
     /// computed.
     pub fn is_authorized_core(
         &self,

cedar-policy-validator/src/schema.rs

@@ -49,7 +49,7 @@ pub use namespace_def::ValidatorNamespaceDef;
 #[cfg(test)]
 pub(crate) use namespace_def::ACTION_ENTITY_TYPE;
 
-// We do not have a dafny model for action attributes, so we disable them by defualt.
+// We do not have a formal model for action attributes, so we disable them by default.
 #[derive(Eq, PartialEq, Copy, Clone, Default)]
 pub enum ActionBehavior {
     /// Action entities cannot have attributes. Attempting to declare attributes

cedar-policy/src/api.rs

@@ -660,7 +660,7 @@ impl Authorizer {
     /// Returns an authorization response for `r` with respect to the given
     /// `PolicySet` and `Entities`.
     ///
-    /// The language spec and Dafny model give a precise definition of how this
+    /// The language spec and formal model give a precise definition of how this
     /// is computed.
     /// ```
     /// # use cedar_policy::{Authorizer,Context,Decision,Entities,EntityId,EntityTypeName, EntityUid, Request,PolicySet};