Level checking soundness proof

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,67 @@
+/-
+ 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 flatten_union {α} [LT α] [DecidableLT α] : List (Set α) → Set α :=
+  List.foldl (· ∪ ·) ∅
+
+def Value.sliceEUIDs (v : Value) : Set EntityUID :=
+  match v with
+  | .prim (.entityUID uid) => Set.singleton uid
+  -- TODO: You can't access these except by `in`, so maybe this could just be `Set.empty`
+  | .set s => flatten_union $ s.elts.attach.map λ e => e.val.sliceEUIDs
+  | .record r => flatten_union $ r.toList.attach.map λ e => e.val.snd.sliceEUIDs
+  | .prim _ | .ext _ => ∅
+  decreasing_by
+    · simp [←Nat.succ_eq_one_add, Nat.lt.step, Set.sizeOf_lt_of_mem e.property]
+    · simp only [Map.toList] at e
+      have _ := Map.sizeOf_lt_of_kvs r
+      have _ := List.sizeOf_lt_of_mem e.property
+      have _ : sizeOf e.val.snd < sizeOf e.val := by simp [sizeOf, Prod._sizeOf_1, Nat.one_add]
+      rw [record.sizeOf_spec] ; omega
+
+def EntityData.sliceEUIDs (ed : EntityData) : Set EntityUID :=
+  (flatten_union $ ed.attrs.values.map Value.sliceEUIDs) ∪
+  (flatten_union $ ed.tags.values.map 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) (level : Nat) : Option (Set EntityUID) :=
+    match level with
+    | 0 => some ∅
+    | Nat.succ level => do
+      let eds ← work.elts.mapM es.find?
+      let slice ← flatten_union <$> 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,62 @@
+/-
+ 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
+
+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).checked) :
+  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 => sorry -- inductive case, similar ast rewriting concerns as `if`, type annotation could be buggy
+  case or => sorry -- inductive case, similar ast rewriting concerns as `if`, type annotation could be buggy
+  case unaryApp => sorry -- trivial inductive cases
+  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/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).checked →
+  evaluate e request entities = evaluate e request slice

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

@@ -0,0 +1,86 @@
+/-
+ 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
+
+namespace Cedar.Thm
+
+/-!
+This file contains some simple lemmas about the `checkLevel` and `typedAtLevel`
+functions that do not need reason about the slicing functions.
+-/
+
+open Cedar.Validation
+
+theorem check_level_lit_inversion {p : Spec.Prim} {ty : CedarType} {n : Nat}
+  : (checkLevel (.lit p ty) n) = LevelCheckResult.mk true false
+:= by simp [checkLevel]
+
+theorem check_level_root_invariant (n n' : Nat) (e : TypedExpr)
+  : (checkLevel e n).root = (checkLevel e n').root
+:= by
+  unfold checkLevel
+  cases e <;> simp
+  case ite | unaryApp =>
+    simp [check_level_root_invariant n n']
+  case binaryApp op _ _ _ =>
+    cases op
+    case mem | getTag | hasTag =>
+      simp [check_level_root_invariant (n - 1) (n' - 1)]
+    all_goals { simp [check_level_root_invariant n n'] }
+  case getAttr e _ _ | hasAttr e _ _ =>
+    cases e.typeOf
+    case entity =>
+      simp [check_level_root_invariant (n - 1) (n' - 1)]
+    all_goals { simp [check_level_root_invariant n n'] }
+  -- Hopefully should be trivial
+  case set es _ | call es _ => sorry
+  case record a => sorry
+
+theorem check_level_checked_succ {e : TypedExpr} {n : Nat}
+  (h₁ : (checkLevel e n).checked)
+  : (checkLevel e (1 + n)).checked
+:= by
+  cases e <;> try (simp [checkLevel] at h₁ ; simp [checkLevel])
+  case ite | and | or | unaryApp =>
+    simp [h₁, check_level_checked_succ]
+  case binaryApp op e₀ _ _ =>
+    cases op <;> (
+      simp [checkLevel] at h₁
+      simp [checkLevel]
+      simp [h₁, check_level_checked_succ]
+    )
+    case mem | hasTag | getTag =>
+      repeat constructor
+      · have h₂ := check_level_root_invariant (1 + n - 1) (n - 1)
+        simp [h₂, h₁]
+      · omega
+      · have h₂ : (1 + n - 1) = (1 + (n - 1)) := by omega
+        simp [h₁, h₂, check_level_checked_succ]
+  case hasAttr e _ _ | getAttr e _ _ =>
+    split at h₁
+    · simp [checkLevel] at h₁
+      simp [checkLevel]
+      repeat constructor
+      · have h₂ := check_level_root_invariant (1 + n - 1) (n - 1)
+        simp [h₂, h₁]
+      · omega
+      · have h₂ : (1 + n - 1) = (1 + (n - 1)) := by omega
+        simp [h₁, h₂, check_level_checked_succ]
+    · simp [h₁, check_level_checked_succ]
+  -- should be trivial
+  case set | call => sorry
+  case record => sorry

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

@@ -0,0 +1,126 @@
+/-
+ 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.Data
+import Cedar.Thm.Validation.Typechecker.Basic
+
+namespace Cedar.Thm
+
+/-!
+This file contains lemma about data structures. These should move into
+appropriate files in the `Data` directory, or be replaced by calls to existing
+lemma where reasonable.
+-/
+
+open Cedar.Data
+open Cedar.Spec
+open Cedar.Validation
+
+theorem set_mem_flatten_union_iff_mem_any {α : Type} [LT α] [DecidableLT α] {ll : List (Set α)} {e : α}
+  : e ∈ flatten_union ll ↔ ∃ l ∈ ll, e ∈ l
+:= by sorry
+
+theorem map_find_then_value {α β : Type} [BEq α] {m : Map α β} {k : α} {v : β}
+  (hf : m.find? k = some v)
+  : v ∈ m.values
+:= by sorry
+
+theorem map_find_mapm_value {α β : Type} [LT α] [DecidableLT α] [BEq α] {ks : Set α} {k : α} {kvs : List (α × β)} {fn : α → Option β}
+  (h₁ : List.mapM (λ k => (fn k).bind λ v => (some (k, v))) ks.elts = some kvs)
+  (h₂ : k ∈ ks)
+  : (Map.make kvs).find? k = fn k
+:= by
+  cases h₃ : ks.elts
+  case nil =>
+    have hcontra : List.Mem k [] := by
+      simp only [Membership.mem, h₃] at h₂
+      exact h₂
+    contradiction
+  case cons h t =>
+    simp [h₃] at h₁
+    cases h₄ : ((fn h).bind λ v => some (h, v)) <;> simp [h₄] at h₁
+    cases h₅ : (List.mapM (λ k => (fn k).bind λ v => some (k, v)) t) <;> simp [h₅] at h₁
+    subst h₁
+    simp only [Membership.mem, h₃] at h₂
+    cases h₂
+    case head =>
+      cases h₆ : (fn k) <;> simp [h₆] at h₄
+      subst h₄
+      sorry
+    case tail h₂ =>
+      symm at h₅
+      sorry
+
+theorem mapm_pair_lookup  {α γ : Type} [BEq α] [LawfulBEq α] {l : List α} {l' : List (α × γ)} {f : α → Option (α × γ)} {e: α}
+  (h₁ : List.mapM f l = some l')
+  (h₂ : e ∈ l)
+  (hf : ∀ e, match f e with
+    | some e' => e'.fst = e
+    | none => True)
+  : ∃ e', f e = some e' ∧  l'.lookup e'.fst = some e'.snd
+:= by
+  cases l
+  case nil => contradiction
+  case cons h t =>
+    cases h₃ : f h <;>
+    cases h₄ : List.mapM f t <;>
+    simp only [h₃, h₄, List.mapM_cons, Option.pure_def, Option.bind_none_fun, Option.bind_some_fun, Option.some.injEq, reduceCtorEq] at h₁
+    subst h₁
+    simp only [List.mem_cons] at h₂
+    cases h₂
+    case _ h₂ =>
+      simp [h₂, h₃, List.lookup]
+    case _ h₂ =>
+      have ⟨ e'', ih₁, ih₂ ⟩ := mapm_pair_lookup h₄ h₂ hf
+      have fh₁ := hf h ; rw [h₃] at fh₁ ; subst fh₁
+      have fh₂ := hf e ; rw [ih₁] at fh₂ ; subst fh₂
+      simp only [ih₁,ih₂, Option.some.injEq, List.lookup, exists_eq_left']
+      split
+      · rename_i h₅
+        simp only [beq_iff_eq] at h₅
+        simp only [←h₅, ih₁, Option.some.injEq] at h₃
+        rw [h₃]
+      · simp
+
+theorem map_cons_find_none {α β : Type} [BEq α] [LT α] [DecidableLT α] {e₁ e₂ : α} {v : β} {t : List (α × β)}
+  (h₁ : e₁ ≠ e₂)
+  (h₂ : (Map.make t).find? e₁ = none) :
+  (Map.make ((e₂, v) :: t)).find? e₁ = none
+:= by sorry
+
+theorem mapm_none_find_none {α γ : Type} [BEq α] [LT α] [DecidableLT α] {l : List α} {l' : List (α × γ)} {f : α → Option γ} {e: α}
+  (h₂ : l.mapM (λ e => (f e).bind (λ e' => (e, e'))) = some l')
+  (h₁ : f e = none) :
+  (Map.make l').find? e = none
+:= by
+  cases l
+  case nil =>
+    simp at h₂
+    subst h₂
+    rw [Map.make_nil_is_empty]
+    simp [Map.find?, Map.empty, Map.kvs]
+  case cons h t =>
+    simp at h₂
+    cases h₃ : (f h) <;> simp [h₃] at h₂
+    cases h₄ : ((List.mapM (fun e => (f e).bind fun e' => some (e, e')) t)) <;> simp [h₄] at h₂
+    subst h₂
+    have ih := mapm_none_find_none h₄ h₁
+    have hne : e ≠ h := by
+      intros heq
+      subst heq
+      rw [h₁] at h₃
+      contradiction
+    apply map_cons_find_none hne ih