Level checking implementation and proof (WIP)

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/Thm/Validation.lean

@@ -17,6 +17,7 @@
 import Cedar.Spec
 import Cedar.Data
 import Cedar.Validation
+import Cedar.Thm.Validation.Levels
 import Cedar.Thm.Validation.Validator
 import Cedar.Thm.Validation.RequestEntityValidation
 

cedar-lean/Cedar/Thm/Validation/Levels.lean

@@ -0,0 +1,73 @@
+/-
+ 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
+import Cedar.Data
+import Cedar.Validation
+import Cedar.Thm.Validation.Typechecker
+import Cedar.Thm.Validation.Typechecker.Types
+
+import Cedar.Thm.Validation.Levels.CheckLevel
+import Cedar.Thm.Validation.Levels.IfThenElse
+import Cedar.Thm.Validation.Levels.GetAttr
+import Cedar.Thm.Validation.Levels.HasAttr
+import Cedar.Thm.Validation.Levels.UnaryApp
+import Cedar.Thm.Validation.Levels.And
+import Cedar.Thm.Validation.Levels.Or
+
+namespace Cedar.Thm
+
+open Cedar.Data
+open Cedar.Spec
+open Cedar.Validation
+
+theorem level_based_slicing_is_sound {e : Expr} {tx : TypedExpr} {n : Nat} {c c₁ : Capabilities} {env : Environment} {request : Request} {slice entities : Entities}
+  (hs : slice = entities.sliceAtLevel request n)
+  (hc : CapabilitiesInvariant c request entities)
+  (hr : RequestAndEntitiesMatchEnvironment env request entities)
+  (ht : typeOf e c env = Except.ok (tx, c₁))
+  (hl : checkLevel tx n) :
+  evaluate e request entities = evaluate e request slice
+:= by
+  cases e
+  case lit => simp [evaluate]
+  case var v => cases v <;> simp [evaluate]
+  case ite c t e =>
+    have ihc := @level_based_slicing_is_sound c
+    have iht := @level_based_slicing_is_sound t
+    have ihe := @level_based_slicing_is_sound e
+    exact level_based_slicing_is_sound_if hs hc hr ht hl ihc iht ihe
+  case and e₁ e₂ =>
+    have ih₁ := @level_based_slicing_is_sound e₁
+    have ih₂ := @level_based_slicing_is_sound e₂
+    exact level_based_slicing_is_sound_and hs hc hr ht hl ih₁ ih₂
+  case or e₁ e₂ =>
+    have ih₁ := @level_based_slicing_is_sound e₁
+    have ih₂ := @level_based_slicing_is_sound e₂
+    exact level_based_slicing_is_sound_or hs hc hr ht hl ih₁ ih₂
+  case unaryApp op e =>
+    have ihe := @level_based_slicing_is_sound e
+    exact level_based_slicing_is_sound_unary_app hs hc hr ht hl ihe
+  case binaryApp => sorry -- includes tags cases which should follow the attr cases and `in` case which might be tricky
+  case getAttr e _ =>
+    have ihe := @level_based_slicing_is_sound e
+    exact level_based_slicing_is_sound_get_attr hs hc hr ht hl ihe
+  case hasAttr e _ =>
+    have ihe := @level_based_slicing_is_sound e
+    exact level_based_slicing_is_sound_has_attr hs hc hr ht hl ihe
+  case set => sorry -- trivial recursive case maybe a little tricky
+  case record => sorry -- likely to be tricky. Record cases are always hard, and here there might be an odd interaction with attribute access
+  case call => sorry -- should be the same as set

cedar-lean/Cedar/Thm/Validation/Levels/And.lean

@@ -0,0 +1,80 @@
+
+/-
+ 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
+import Cedar.Data
+import Cedar.Validation
+import Cedar.Thm.Validation.Typechecker
+import Cedar.Thm.Validation.Typechecker.Basic
+import Cedar.Thm.Validation.Typechecker.IfThenElse
+import Cedar.Thm.Validation.Typechecker.Types
+import Cedar.Thm.Validation.Levels.Basic
+
+/-!
+This file proves that level checking for `.and` expressions is sound.
+-/
+
+namespace Cedar.Thm
+
+open Cedar.Data
+open Cedar.Spec
+open Cedar.Validation
+
+theorem level_based_slicing_is_sound_and {e₁ e₂ : Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
+  (hs : slice = entities.sliceAtLevel request n)
+  (hc : CapabilitiesInvariant c₀ request entities)
+  (hr : RequestAndEntitiesMatchEnvironment env request entities)
+  (ht : typeOf (.and e₁ e₂) c₀ env = Except.ok (tx, c₁))
+  (hl : checkLevel tx n = true)
+  (ih₁ : TypedAtLevelIsSound e₁)
+  (ih₂ : TypedAtLevelIsSound e₂)
+  : evaluate (.and e₁ e₂) request entities = evaluate (.and e₁ e₂) request slice
+:= by
+  replace ⟨ tx₁, bty, c', htx₁, hty₁, ht ⟩ := type_of_and_inversion ht
+  have ⟨ hgc, v₁, he₁, hv₁⟩  := type_of_is_sound hc hr htx₁
+  rw [hty₁] at hv₁
+  split at ht
+  case isTrue =>
+    replace ⟨ ht, _ ⟩ := ht
+    subst tx bty
+    replace hv₁ := instance_of_ff_is_false hv₁
+    subst v₁
+    unfold EvaluatesTo at he₁
+    simp [evaluate]
+    simp [checkLevel] at hl
+    specialize ih₁ hs hc hr htx₁ hl
+    rw [←ih₁]
+    rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
+    simp [he₁, Result.as, Coe.coe, Value.asBool]
+  case isFalse =>
+    replace ⟨ tx₂, bty₂, c₂, htx₂, hty₂, ht ⟩ := ht
+    replace ⟨ b₁ , hv₁⟩  := instance_of_bool_is_bool hv₁
+    subst v₁
+    split at ht
+    all_goals
+      replace ⟨ ht, _ ⟩ := ht
+      subst tx
+      simp [evaluate]
+      simp [checkLevel] at hl
+      specialize ih₁ hs hc hr htx₁ (by simp [hl])
+      rw [←ih₁]
+      rcases he₁ with he₁ | he₁ | he₁ | he₁ <;>
+      simp [he₁, Result.as, Coe.coe, Value.asBool]
+      cases b₁ <;> simp
+      specialize hgc he₁
+      specialize ih₂ hs (capability_union_invariant hc hgc) hr htx₂ (by simp [hl])
+      simp [ih₂]

cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean

@@ -0,0 +1,34 @@
+/-
+ 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.Thm.Validation.Typechecker.Basic
+
+namespace Cedar.Thm
+
+/-!
+Basic definitions for levels proof
+-/
+
+open Cedar.Spec
+open Cedar.Validation
+
+def TypedAtLevelIsSound (e : Expr) : Prop := ∀ {n : Nat} {tx : TypedExpr} {c c₁ : Capabilities} {env :Environment} {request : Request} {entities slice : Entities},
+  slice = entities.sliceAtLevel request n →
+  CapabilitiesInvariant c request entities →
+  RequestAndEntitiesMatchEnvironment env request entities →
+  typeOf e c env = Except.ok (tx, c₁) →
+  checkLevel tx n →
+  evaluate e request entities = evaluate e request slice