Add model for level checking and slicing

Signed-off-by: John Kastner <jkastner@amazon.com>

cedar-lean/Cedar/Spec.lean

@@ -22,6 +22,7 @@ import Cedar.Spec.Ext
 import Cedar.Spec.Policy
 import Cedar.Spec.Request
 import Cedar.Spec.Response
+import Cedar.Spec.Slice
 import Cedar.Spec.Template
 import Cedar.Spec.Value
 import Cedar.Spec.Wildcard

cedar-lean/Cedar/Spec/Slice.lean

@@ -0,0 +1,53 @@
+/-
+ 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.Entities
+import Cedar.Spec.Request
+import Cedar.Data.SizeOf
+
+/-!
+This file defines entity slicing at a level
+-/
+
+namespace Cedar.Spec
+
+open Cedar.Data
+
+def Value.sliceEUIDs : Value → Set EntityUID
+  | .prim (.entityUID uid) => Set.singleton uid
+  | .record (Map.mk avs) => avs.attach₃.mapUnion λ e => e.val.snd.sliceEUIDs
+  | .prim _ | set _ | .ext _ => ∅
+
+def EntityData.sliceEUIDs (ed : EntityData) : Set EntityUID :=
+  ed.attrs.values.mapUnion Value.sliceEUIDs ∪
+  ed.tags.values.mapUnion Value.sliceEUIDs
+
+def Request.sliceEUIDs (r : Request) : Set EntityUID :=
+  Set.make [r.principal, r.action, r.resource] ∪
+  (Value.record r.context).sliceEUIDs
+
+def Entities.sliceAtLevel (es : Entities) (r : Request) (level : Nat) : Option Entities := do
+  let slice ← sliceAtLevel r.sliceEUIDs level
+  let slice ← slice.elts.mapM λ e => do some (e, ←(es.find? e))
+  some (Map.make slice)
+where
+  sliceAtLevel (work : Set EntityUID) : Nat → Option (Set EntityUID)
+    | 0 => some ∅
+    | level + 1 => do
+      let eds ← work.elts.mapM es.find?
+      let slice ← List.mapUnion id <$> eds.mapM (λ ed => sliceAtLevel ed.sliceEUIDs level)
+      some (work ∪ slice)

cedar-lean/Cedar/Validation.lean

@@ -20,3 +20,4 @@ import Cedar.Validation.Subtyping
 import Cedar.Validation.Typechecker
 import Cedar.Validation.Validator
 import Cedar.Validation.RequestEntityValidator
+import Cedar.Validation.Levels

cedar-lean/Cedar/Validation/Levels.lean

@@ -0,0 +1,110 @@
+/-
+ 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.Validation.TypedExpr
+import Cedar.Validation.Typechecker
+import Cedar.Thm.Data.Map
+import Cedar.Spec.Policy
+
+/-!
+This file defines a level checking of a type-annotated AST. Level checking
+should behave as defined in RFC#76, although the implementation here is
+different from what was proposed because this implementation operates over a
+type-annotated AST instead of being built into the primary typechecking
+algorithm.
+-/
+
+namespace Cedar.Validation
+
+open Cedar.Data
+open Cedar.Spec
+
+mutual
+
+def checkEntityAccessLevel (tx : TypedExpr) (n nmax : Nat) (path : List Attr) : Bool :=
+  match tx, path with
+  | .var _ _, _ => true
+  | .ite tx₁ tx₂ tx₃ _, _ =>
+    checkLevel tx₁ nmax &&
+    checkEntityAccessLevel tx₂ n nmax path &&
+    checkEntityAccessLevel tx₃ n nmax path
+  | .getAttr x₁ a _, _ =>
+    match x₁.typeOf with
+    | .entity _ =>
+      n > 0 &&
+      checkEntityAccessLevel x₁ (n - 1) nmax []
+    | _ =>
+      checkEntityAccessLevel x₁ n nmax (a :: path)
+  | .binaryApp .getTag x₁ x₂ _, _ =>
+    n > 0 &&
+    checkEntityAccessLevel x₁ (n - 1) nmax [] &&
+    checkLevel x₂ nmax
+  | .record axs _, (a :: path) =>
+    match h₁ : (Map.make axs).find? a with
+    | some tx' =>
+      have : sizeOf tx' < sizeOf axs := by
+        replace h₁ := List.sizeOf_lt_of_mem ∘ Map.make_mem_list_mem ∘ Map.find?_mem_toList $ h₁
+        rw [Prod.mk.sizeOf_spec a tx'] at h₁
+        omega
+      checkEntityAccessLevel tx' n nmax path &&
+      axs.attach₂.all λ e =>
+        checkLevel e.val.snd nmax
+    | none => false
+  | _, _ => false
+
+def checkLevel (tx : TypedExpr) (n : Nat) : Bool :=
+  match tx with
+  | .lit _ _ => true
+  | .var _ _ => true
+  | .ite x₁ x₂ x₃ _ =>
+    checkLevel x₁ n &&
+    checkLevel x₂ n &&
+    checkLevel x₃ n
+  | .unaryApp _ x₁ _ =>
+    checkLevel x₁ n
+  | .binaryApp .mem x₁ x₂ _
+  | .binaryApp .getTag x₁ x₂ _
+  | .binaryApp .hasTag x₁ x₂ _ =>
+    n > 0 &&
+    checkEntityAccessLevel x₁ (n - 1) n [] &&
+    checkLevel x₂ n
+  | .and x₁ x₂ _
+  | .or x₁ x₂ _
+  | .binaryApp _ x₁ x₂ _ =>
+    checkLevel x₁ n &&
+    checkLevel x₂ n
+  | .hasAttr x₁ _ _
+  | .getAttr x₁ _ _ =>
+    match x₁.typeOf with
+    | .entity _ =>
+      n > 0 &&
+      checkEntityAccessLevel x₁ (n - 1) n []
+    | _ => checkLevel x₁ n
+  | .call _ xs _
+  | .set xs _ =>
+    xs.attach.all λ e =>
+      have := List.sizeOf_lt_of_mem e.property
+      checkLevel e n
+  | .record axs _ =>
+    axs.attach₂.all λ e =>
+      checkLevel e.val.snd n
+
+ end
+
+def typecheckAtLevel (policy : Policy) (env : Environment) (n : Nat) : Bool :=
+  match typeOf policy.toExpr ∅ env with
+  | .ok (tx, _) => checkLevel tx n
+  | _           => false