From 733f005ccfdae0bf230732bb0e7a362de7386ba1 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 13 Feb 2024 18:34:52 +0000 Subject: [PATCH] updates --- .github/PULL_REQUEST_TEMPLATE.md | 2 +- cedar-policy-core/src/ast/pattern.rs | 15 +++++++-------- cedar-policy-core/src/authorizer.rs | 4 ++-- cedar-policy-validator/src/schema.rs | 2 +- cedar-policy/src/api.rs | 2 +- 5 files changed, 12 insertions(+), 13 deletions(-) diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index e42bd580b..f7820fe97 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.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.) diff --git a/cedar-policy-core/src/ast/pattern.rs b/cedar-policy-core/src/ast/pattern.rs index ff1a69d49..f8da7ba08 100644 --- a/cedar-policy-core/src/ast/pattern.rs +++ b/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), } } } diff --git a/cedar-policy-core/src/authorizer.rs b/cedar-policy-core/src/authorizer.rs index 3c2453488..b08bb45f1 100644 --- a/cedar-policy-core/src/authorizer.rs +++ b/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, diff --git a/cedar-policy-validator/src/schema.rs b/cedar-policy-validator/src/schema.rs index 7bda32018..14d63e4b2 100644 --- a/cedar-policy-validator/src/schema.rs +++ b/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 diff --git a/cedar-policy/src/api.rs b/cedar-policy/src/api.rs index ef764561f..3b56733a1 100644 --- a/cedar-policy/src/api.rs +++ b/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};