TPE Lean model

cedar-lean/Cedar.lean

@@ -18,3 +18,4 @@ import Cedar.Data
 import Cedar.Spec
 import Cedar.Thm
 import Cedar.Validation
+import Cedar.TPE

cedar-lean/Cedar/TPE.lean

@@ -0,0 +1,19 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.TPE.Input
+import Cedar.TPE.Residual
+import Cedar.TPE.Evaluator

cedar-lean/Cedar/TPE/Evaluator.lean

@@ -0,0 +1,222 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.TPE.Input
+import Cedar.TPE.Residual
+
+namespace Cedar.TPE
+
+open Cedar.Data
+open Cedar.Spec
+open Cedar.Validation
+
+inductive Error where
+  | evaluation (err : Spec.Error)
+  | invalidPolicy (err : TypeError)
+  | noValidEnvironment
+  | invalidRequestOrEntities
+deriving Repr
+
+instance : Coe Spec.Error Error where
+  coe := Error.evaluation
+
+def inₑ (uid₁ uid₂ : EntityUID) (es : PartialEntities) (ty : CedarType): Residual :=
+  if uid₁ = uid₂
+    then .val true ty
+    else
+    match es.find? uid₁ with
+    | .some ⟨_, .some uids, _⟩ => .val (uids.contains uid₂) ty
+    | .some ⟨_, .none, _⟩ => .binaryApp .mem (.val (.prim (.entityUID uid₁)) (.entity uid₁.ty)) (.val (.prim (.entityUID uid₂)) (.entity uid₂.ty)) ty
+    | .none => .val false ty
+
+def apply₂ (op₂ : BinaryOp) (r₁ r₂ : Residual) (es : PartialEntities) (ty : CedarType): Result Residual :=
+  let self : Result Residual := .ok $ .binaryApp op₂ r₁ r₂ ty
+  match op₂, r₁, r₂ with
+  | .eq, (.val v₁ _), (.val v₂ _) => .ok $ .val (v₁ == v₂) ty
+  | .less, (.val (.prim (.int i)) _), (.val (.prim (.int j)) _) =>
+    .ok $ .val ((i < j): Bool) ty
+  | .lessEq, (.val (.prim (.int i)) _), (.val (.prim (.int j)) _) =>
+    .ok $ .val ((i ≤ j): Bool) ty
+  | .add, (.val (.prim (.int i)) _), (.val (.prim (.int j)) _) =>
+    (intOrErr (i.add? j)).map (Value.toResidual · ty)
+  | .sub, (.val (.prim (.int i)) _), (.val (.prim (.int j)) _) =>
+    (intOrErr (i.sub? j)).map (Value.toResidual · ty)
+  | .mul, (.val (.prim (.int i)) _), (.val (.prim (.int j)) _) =>
+    (intOrErr (i.mul? j)).map (Value.toResidual · ty)
+  | .contains, (.val (.set vs₁) _), (.val v₂ _) =>
+    .ok $ .val (vs₁.contains v₂) ty
+  | .containsAll, (.val (.set vs₁) _), (.val (.set vs₂) _) =>
+    .ok $ .val (vs₂.subset vs₁) ty
+  | .containsAny, (.val (.set vs₁) _), (.val (.set vs₂) _) =>
+    .ok $ .val (vs₁.intersects vs₂) ty
+  | .mem, (.val (.prim (.entityUID uid₁)) _), (.val (.prim (.entityUID uid₂)) _) =>
+    .ok $ inₑ uid₁ uid₂ es ty
+  | .mem, (.val (.prim (.entityUID uid₁)) _), (.val (.set vs) _) => do
+    let uids ← vs.mapOrErr Value.asEntityUID .typeError
+    let rs := uids.toList.map λ uid ↦ inₑ uid₁ uid es ty
+    if rs.any λ r ↦ match r with
+      | .val (.prim (.bool _)) _ => false
+      | _ => true
+    then self
+    else .ok $ (.val (.prim (.bool (rs.any λ r ↦ match r with
+      | .val (.prim (.bool true)) _ => true
+      | _ => false
+    ))) ty)
+  | .hasTag, (.val (.prim (.entityUID uid₁)) _), (.val (.prim (.string tag)) _) =>
+    match es.find? uid₁ with
+    | .some ⟨_, _, .some m⟩ => .ok $ .val (m.contains tag) ty
+    | .some ⟨_, _, .none⟩ => self
+    | .none => .ok $ .val false ty
+  | .getTag, (.val (.prim (.entityUID uid₁)) _), (.val (.prim (.string tag)) _) =>
+    match es.find? uid₁ with
+    | .some ⟨_, _, .some m⟩ => (m.findOrErr tag .tagDoesNotExist).map (Value.toResidual · ty)
+    | .some ⟨_, _, .none⟩ => self
+    | .none => .error .entityDoesNotExist
+  | _, _, _ => self
+
+def tpeExpr (x : TypedExpr)
+    (req : PartialRequest)
+    (es : PartialEntities)
+    : Result Residual :=
+  match x with
+  | .lit p ty => .ok $ .val p ty
+  | .var .principal ty =>
+    match req.principal.asEntityUID with
+    | .some uid => .ok $ .val (.prim (.entityUID uid)) ty
+    | .none => .ok $ .var .principal ty
+  | .var .resource ty =>
+    match req.resource.asEntityUID with
+    | .some uid => .ok $ .val (.prim (.entityUID uid)) ty
+    | .none => .ok $ .var .resource ty
+  | .var .action ty => .ok $ .val (.prim (.entityUID req.action)) ty
+  | .var .context ty =>
+    match req.context with
+    | .some m => .ok (.val (.record m) ty)
+    | .none => .ok $ .var .context ty
+  | .ite c t e ty => do
+    let c ← tpeExpr c req es
+    match c with
+    | .val (.prim (.bool b)) _ =>
+      if b then tpeExpr t req es else tpeExpr e req es
+    | _ =>
+      let t ← tpeExpr t req es
+      let e ← tpeExpr e req es
+      .ok $ .ite c t e ty
+  | .and l r ty => do
+    let l ← tpeExpr l req es
+    match l with
+    | .val (.prim (.bool b)) _ =>
+      if b then tpeExpr r req es else .ok $ .val (.prim (.bool b)) (.bool .ff)
+    | _ =>
+      let r ← tpeExpr r req es
+      match r with
+      | .val true _ => .ok l
+      | _ => .ok $ .and l r ty
+  | .or l r ty => do
+    let l ← tpeExpr l req es
+    match l with
+    | .val (.prim (.bool b)) _ =>
+      if !b then tpeExpr r req es else .ok $ .val (.prim (.bool b)) (.bool .tt)
+    | _ =>
+      let r ← tpeExpr r req es
+      match r with
+      | .val false _ => .ok l
+      | _ => .ok $ .or l r ty
+  | .unaryApp op e ty => do
+    let r ← tpeExpr e req es
+    match r.asValue with
+    | .some v => (apply₁ op v).map (Value.toResidual · ty)
+    | .none => .ok $ .unaryApp op r ty
+  | .binaryApp op x y ty => do
+    let x ← tpeExpr x req es
+    let y ← tpeExpr y req es
+    apply₂ op x y es ty
+  | .getAttr e a ty => do
+    let r ← tpeExpr e req es
+    match r with
+    | .val (.record xs) _ =>
+      (xs.findOrErr a .attrDoesNotExist).map
+        (Value.toResidual · ty)
+    | .val (.prim (.entityUID uid)) _ =>
+      let data ← es.findOrErr uid .entityDoesNotExist
+      match data.attrs with
+      | .some m =>
+        (m.findOrErr a .attrDoesNotExist).map
+          (Value.toResidual · ty)
+      | .none => .ok $ .getAttr r a ty
+    | _ => .ok $ .getAttr r a ty
+  | .hasAttr e a ty => do
+    let r ← tpeExpr e req es
+    match r with
+    | .val (.record xs) _ =>
+      .ok $ .val (xs.contains a) ty
+    | .val (.prim (.entityUID uid)) _ =>
+      match es.find? uid with
+      | .some ⟨ .some m, _ , _⟩  =>
+        .ok $ .val (m.contains a) ty
+      | .some ⟨ .none, _ , _⟩  => .ok $ .hasAttr r a ty
+      | .none => .ok $ .val false ty
+    | _ => .ok $ .getAttr r a ty
+  | .set xs ty => do
+    let rs ← xs.mapM₁ (λ ⟨x₁, _⟩ ↦ tpeExpr x₁ req es)
+    match rs.mapM Residual.asValue with
+    | .some vs => .ok $ .val (.set (Set.mk vs)) ty
+    | .none => .ok $ .set rs ty
+  | .record m ty => do
+    let m₁ ← m.mapM₁ (λ ⟨(a, x₁), _⟩ ↦ do
+      let v ← tpeExpr x₁ req es
+      pure (a, v))
+    match m₁.mapM λ (a, r₁) ↦ do
+      let v₁ ← r₁.asValue
+      pure (a, v₁) with
+    | .some xs => .ok $ .val (.record (Map.mk xs)) ty
+    | .none => .ok $ .record m₁ ty
+  | .call f args ty => do
+    let rs ← args.mapM₁ (λ ⟨x₁, _⟩ ↦ tpeExpr x₁ req es)
+    match rs.mapM Residual.asValue with
+    | .some vs => (Spec.call f vs).map (Value.toResidual · ty)
+    | .none => .ok $ .call f rs ty
+termination_by x
+decreasing_by
+  all_goals
+    simp_wf
+    try omega
+  case _ h =>
+    have := List.sizeOf_lt_of_mem h
+    omega
+  case _ h =>
+    have h₁ := List.sizeOf_lt_of_mem h
+    simp at h₁
+    omega
+  case _ h =>
+    have := List.sizeOf_lt_of_mem h
+    omega
+
+def tpePolicy (schema : Schema)
+  (p : Policy)
+  (req : PartialRequest)
+  (es : PartialEntities)
+  : Except Error Residual :=
+  match schema.environment? req.principal.ty req.resource.ty req.action with
+    | .some env => if RequestAndEntitiesIsValid env req es then
+      do
+        let expr := substituteAction env.reqty.action p.toExpr
+        let (te, _) ← (typeOf expr ∅ env).mapError Error.invalidPolicy
+        (tpeExpr te req es).mapError Error.evaluation
+      else .error .invalidRequestOrEntities
+    | .none => .error Error.noValidEnvironment
+
+end Cedar.TPE

cedar-lean/Cedar/TPE/Input.lean

@@ -0,0 +1,94 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.Spec.Value
+import Cedar.Spec.Expr
+import Cedar.Spec.Request
+import Cedar.Validation.TypedExpr
+import Cedar.Validation.RequestEntityValidator
+
+namespace Cedar.TPE
+
+open Cedar.Data
+open Cedar.Spec
+open Cedar.Validation
+
+structure PartialEntityUID where
+  ty : EntityType                    -- Entity type is always known,
+  id : Option String                 -- but entity id may not be.
+
+def PartialEntityUID.asEntityUID (self : PartialEntityUID) : Option EntityUID :=
+  self.id.map λ x ↦ ⟨ self.ty, x⟩
+
+structure PartialRequest where
+  principal : PartialEntityUID
+  action : EntityUID
+  resource : PartialEntityUID
+  -- no type annotation is needed here because this value can only be accessed
+  -- via evaluating a `TypedExpr`, which allows us to obtain a (typed)
+  -- `Residual`
+  context :  Option (Map Attr Value)
+
+-- no type annotation is needed here following the rationale above
+structure PartialEntityData where
+  attrs : Option (Map Attr Value)
+  ancestors : Option (Set EntityUID)
+  tags : Option (Map Attr Value)
+
+abbrev PartialEntities := Map EntityUID PartialEntityData
+
+def NoneIsTrue {α} (o : Option α) (f : α → Bool) : Bool :=
+  match o with
+  | .some v => f v
+  | .none => true
+
+def RequestIsValid (env : Environment) (req : PartialRequest) : Bool :=
+  (NoneIsTrue req.principal.asEntityUID λ principal ↦
+    instanceOfEntityType principal principal.ty env.ets.entityTypeMembers?) &&
+  (NoneIsTrue req.resource.asEntityUID λ resource ↦
+    instanceOfEntityType resource resource.ty env.ets.entityTypeMembers?) &&
+  (NoneIsTrue req.context λ m ↦
+    instanceOfType (.record m) (.record env.reqty.context) env.ets)
+
+def EntitiesIsValid (env : Environment) (es : PartialEntities) : Bool :=
+  (es.toList.all EntityIsValid) && (env.acts.toList.all instanceOfActionSchema)
+where
+  EntityIsValid p :=
+  let (uid, ⟨attrs, ancestors, tags⟩) := p
+  match env.ets.find? uid.ty with
+  | .some entry =>
+    entry.isValidEntityEID uid.eid &&
+    (NoneIsTrue ancestors λ ancestors ↦
+      ancestors.all (λ ancestor =>
+      entry.ancestors.contains ancestor.ty &&
+      instanceOfEntityType ancestor ancestor.ty env.ets.entityTypeMembers?)) &&
+    (NoneIsTrue attrs λ attrs ↦
+      instanceOfType attrs (.record entry.attrs) env.ets) &&
+    (NoneIsTrue tags λ tags ↦
+      match entry.tags? with
+    | .some tty => tags.values.all (instanceOfType · tty env.ets)
+    | .none     => tags == Map.empty)
+  | .none => false
+  instanceOfActionSchema p :=
+    let (uid, entry) := p
+    match es.find? uid with
+      | .some entry₁ => entry.ancestors == entry₁.ancestors
+      | _ => false
+
+def RequestAndEntitiesIsValid (env : Environment) (req : PartialRequest) (es : PartialEntities) : Bool :=
+  RequestIsValid env req && EntitiesIsValid env es
+
+end Cedar.TPE