diff --git a/cedar-lean/Cedar/Thm/Data/List/Basic.lean b/cedar-lean/Cedar/Thm/Data/List/Basic.lean index 63ac38924..5888bf04f 100644 --- a/cedar-lean/Cedar/Thm/Data/List/Basic.lean +++ b/cedar-lean/Cedar/Thm/Data/List/Basic.lean @@ -428,6 +428,41 @@ theorem filterMap_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β rw [← h₁ x hd' hgx] exact sortedBy_implies_head_lt_tail h₂ x hx +theorem mapM_key_id_sortedBy_key {α β : Type} [LT α] {ks : List α} {kvs : List (α × β)} {fn : α → Option β} + (hm : ks.mapM (λ k => do (some (k, ←fn k))) = some kvs) + (hs : ks.Sorted) : + kvs.SortedBy Prod.fst +:= by + cases hs + case nil => + have _ : kvs = [] := by simpa using hm + subst kvs + exact SortedBy.nil + case cons_nil head => + have ⟨_, _⟩ : ∃ kv, kvs = [kv] := by + cases hm₁ : fn head <;> + simp only [hm₁, List.mapM_cons, List.mapM_nil, Option.pure_def, Option.bind_none_fun, Option.bind_some_fun, Option.none_bind, Option.some_bind, Option.some.injEq, reduceCtorEq] at hm + simp [←hm] + subst kvs + exact SortedBy.cons_nil + case cons_cons head₀ head₁ tail hlt hs => + simp only [List.mapM_cons, Option.pure_def, Option.bind_eq_bind] at hm + cases hm₁ : (fn head₀) <;> simp only [hm₁, Option.none_bind, Option.some_bind, Option.some.injEq, reduceCtorEq] at hm + cases hm₂ : (fn head₁) <;> simp only [hm₂, Option.none_bind, Option.some_bind, Option.some.injEq, reduceCtorEq] at hm + cases hm₃ : (tail.mapM (λ k => (fn k).bind λ v => some (k, v))) <;> simp only [hm₃, Option.none_bind, Option.some_bind, Option.some.injEq, reduceCtorEq] at hm + rename_i v₀ v₁ kvs' + subst kvs + + replace hlt : (head₀, v₀).fst < (head₁, v₁).fst := by + simpa using hlt + + replace hs : ((head₁, v₁) :: kvs').SortedBy Prod.fst := by + have hm₄ : (head₁::tail).mapM (λ k => (fn k).bind λ v => some (k, v)) = some ((head₁, v₁) :: kvs') := by + simp [hm₂, hm₃] + exact mapM_key_id_sortedBy_key hm₄ hs + + exact List.SortedBy.cons_cons hlt hs + /-! ### Forallᵥ -/ def Forallᵥ {α β γ} (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : Prop := diff --git a/cedar-lean/Cedar/Thm/Data/List/Lemmas.lean b/cedar-lean/Cedar/Thm/Data/List/Lemmas.lean index 9bc289f68..540c88248 100644 --- a/cedar-lean/Cedar/Thm/Data/List/Lemmas.lean +++ b/cedar-lean/Cedar/Thm/Data/List/Lemmas.lean @@ -393,6 +393,29 @@ theorem mapM_head_tail {α β γ} {f : α → Except β γ} {x : α} {xs : List cases h₂ : mapM' f xs <;> simp [h₂, pure, Except.pure] +theorem not_mem_implies_not_mem_mapM_key_id {α β : Type} {ks : List α} {kvs : List (α × β)} {fn : α → Option β} {k: α} + (hm : ks.mapM (λ k => do (k, ←fn k)) = some kvs) + (hl : k ∉ ks) : + ∀ v, (k, v) ∉ kvs +:= by + intro v hl' + cases ks + case nil => + have : kvs = [] := by simpa using hm + subst kvs + cases hl' + case cons head tail => + simp only [List.mapM_cons, Option.pure_def, Option.bind_eq_bind] at hm + cases hm₁ : fn head <;> simp only [hm₁, Option.none_bind, Option.some_bind, reduceCtorEq] at hm + cases hm₂ : (tail.mapM (λ k => (fn k).bind λ v => some (k, v))) <;> simp only [hm₂, Option.none_bind, Option.some_bind, Option.some.injEq, reduceCtorEq] at hm + subst kvs + cases hl' + case head => + exact hl (List.Mem.head _) + case tail tail' ht' => + replace hl : k ∉ tail := (hl $ List.Mem.tail _ ·) + exact not_mem_implies_not_mem_mapM_key_id hm₂ hl _ ht' + theorem mapM'_ok_iff_forall₂ {α β γ} {f : α → Except γ β} {xs : List α} {ys : List β} : List.mapM' f xs = .ok ys ↔ List.Forall₂ (λ x y => f x = .ok y) xs ys diff --git a/cedar-lean/Cedar/Thm/Data/Map.lean b/cedar-lean/Cedar/Thm/Data/Map.lean index 40ac409eb..b6354f0bd 100644 --- a/cedar-lean/Cedar/Thm/Data/Map.lean +++ b/cedar-lean/Cedar/Thm/Data/Map.lean @@ -403,6 +403,46 @@ theorem find?_none_iff_all_absent [LT α] [DecidableLT α] [StrictLT α] [Decida m.find? k = none ↔ ∀ v, ¬ (k, v) ∈ m.kvs := Iff.intro find?_none_all_absent all_absent_find?_none +theorem find?_mapM_key_id {α β : Type} [BEq α] [LawfulBEq α] {ks : List α} {kvs : List (α × β)} {fn : α → Option β} {k: α} + (h₁ : ks.mapM (λ k => do (k, ←fn k)) = some kvs) + (h₂ : k ∈ ks) : + (Map.mk kvs).find? k = fn k +:= by + simp only [Map.find?, Map.kvs] + cases h₂ + case head l => + simp only [List.mapM_cons, Option.pure_def, Option.bind_eq_bind] at h₁ + cases hf : fn k <;> simp only [hf, Option.none_bind, Option.some_bind, reduceCtorEq] at h₁ + cases ht₁ : (l.mapM (λ k => (fn k).bind λ v => some (k, v))) <;> simp [ht₁ , Option.none_bind, Option.some_bind, reduceCtorEq, Option.some.injEq] at h₁ + subst h₁ + simp + case tail h t h₂ => + simp only [List.mapM_cons, Option.pure_def, Option.bind_eq_bind] at h₁ + cases hf : fn h <;> simp only [hf, Option.none_bind, Option.some_bind, reduceCtorEq] at h₁ + cases ht₁ : (t.mapM (λ k => (fn k).bind λ v => some (k, v))) <;> simp only [ht₁, Option.none_bind, Option.some_bind, reduceCtorEq, Option.some.injEq] at h₁ + subst h₁ + simp only [List.find?] + cases h₃ : (h == k) + · simp only + exact find?_mapM_key_id ht₁ h₂ + · simp only [beq_iff_eq] at h₃ + simp [h₃, ←hf] + +theorem mapM_key_id_key_none_implies_find?_none {α β : Type} [DecidableEq α] [LT α] [StrictLT α] [DecidableLT α] {ks : List α} {kvs : List (α × β)} {fn : α → Option β} {k: α} + (h₂ : ks.mapM (λ k => do (k, ←fn k)) = some kvs) + (h₁ : fn k = none) : + (Map.make kvs).find? k = none +:= by + by_cases h₃ : k ∈ ks + case pos => + have ⟨ _, _, h₄ ⟩ := List.mapM_some_implies_all_some h₂ k h₃ + simp [h₁] at h₄ + case neg => + simp only [Map.find?_none_iff_all_absent, Map.kvs, Map.make] + intro v hl' + have h₄ := List.in_canonicalize_in_list hl' + exact List.not_mem_implies_not_mem_mapM_key_id h₂ h₃ v h₄ + theorem mapOnValues_wf [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {f : β → γ} {m : Map α β} : m.WellFormed ↔ (m.mapOnValues f).WellFormed := by diff --git a/cedar-lean/Cedar/Thm/Data/Set.lean b/cedar-lean/Cedar/Thm/Data/Set.lean index 96a2dda19..53884eea1 100644 --- a/cedar-lean/Cedar/Thm/Data/Set.lean +++ b/cedar-lean/Cedar/Thm/Data/Set.lean @@ -432,11 +432,7 @@ theorem intersects_iff_exists {α} [LT α] [StrictLT α] [DecidableLT α] [Decid theorem union_wf [LT α] [DecidableLT α] [StrictLT α] (s₁ s₂ : Set α) : WellFormed (s₁ ∪ s₂) := by - unfold WellFormed - simp only [Union.union, union, toList] - rw [make_make_eqv] - apply List.Equiv.symm - exact elts_make_equiv + simp only [Union.union, union, make_wf] theorem mem_union_iff_mem_or [LT α] [DecidableLT α] [StrictLT α] (s₁ s₂ : Set α) : ∀ a, a ∈ s₁ ∪ s₂ ↔ (a ∈ s₁ ∨ a ∈ s₂) diff --git a/cedar-lean/Cedar/Thm/Validation.lean b/cedar-lean/Cedar/Thm/Validation.lean index fba88c011..07a21dcdb 100644 --- a/cedar-lean/Cedar/Thm/Validation.lean +++ b/cedar-lean/Cedar/Thm/Validation.lean @@ -17,6 +17,8 @@ import Cedar.Spec import Cedar.Data import Cedar.Validation +import Cedar.Thm.Validation.Levels +import Cedar.Thm.Validation.Slice import Cedar.Thm.Validation.Validator import Cedar.Thm.Validation.RequestEntityValidation import Cedar.Thm.Validation.Levels diff --git a/cedar-lean/Cedar/Thm/Validation/Levels.lean b/cedar-lean/Cedar/Thm/Validation/Levels.lean index 6b2cb892e..078ce2be7 100644 --- a/cedar-lean/Cedar/Thm/Validation/Levels.lean +++ b/cedar-lean/Cedar/Thm/Validation/Levels.lean @@ -14,4 +14,149 @@ limitations under the License. -/ +import Cedar.Spec +import Cedar.Data +import Cedar.Validation +import Cedar.Thm.Authorization.Authorizer +import Cedar.Thm.Validation.Typechecker +import Cedar.Thm.Validation.Typechecker.Types +import Cedar.Thm.Validation.Validator +import Cedar.Thm.Validation.RequestEntityValidation + +import Cedar.Thm.Validation.Levels.Basic 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.BinaryApp +import Cedar.Thm.Validation.Levels.And +import Cedar.Thm.Validation.Levels.Or +import Cedar.Thm.Validation.Levels.Record +import Cedar.Thm.Validation.Levels.Set +import Cedar.Thm.Validation.Levels.Call + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_expr {e : Expr} {n : Nat} {tx : TypedExpr} {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 e c env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env 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_expr c + have iht := @level_based_slicing_is_sound_expr t + have ihe := @level_based_slicing_is_sound_expr 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_expr e₁ + have ih₂ := @level_based_slicing_is_sound_expr 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_expr e₁ + have ih₂ := @level_based_slicing_is_sound_expr 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_expr e + exact level_based_slicing_is_sound_unary_app hs hc hr ht hl ihe + case binaryApp op e₁ e₂ => + have ihe₁ := @level_based_slicing_is_sound_expr e₁ + have ihe₂ := @level_based_slicing_is_sound_expr e₂ + exact level_based_slicing_is_sound_binary_app hs hc hr ht hl ihe₁ ihe₂ + case getAttr e _ => + have ihe := @level_based_slicing_is_sound_expr 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_expr e + exact level_based_slicing_is_sound_has_attr hs hc hr ht hl ihe + case set xs => + have ih : ∀ x ∈ xs, TypedAtLevelIsSound x := by + intro x hx + have _ : sizeOf x < sizeOf (Expr.set xs) := by + have h₁ := List.sizeOf_lt_of_mem hx + simp only [Expr.set.sizeOf_spec] + omega + exact @level_based_slicing_is_sound_expr x + exact level_based_slicing_is_sound_set hs hc hr ht hl ih + case call xfn xs => + have ih : ∀ x ∈ xs, TypedAtLevelIsSound x := by + intro x hx + have _ : sizeOf x < sizeOf (Expr.set xs) := by + have h₁ := List.sizeOf_lt_of_mem hx + simp only [Expr.set.sizeOf_spec] + omega + exact @level_based_slicing_is_sound_expr x + exact level_based_slicing_is_sound_call hs hc hr ht hl ih + case record rxs => + have ih : ∀ x ∈ rxs, TypedAtLevelIsSound x.snd := by + intro x hx + have _ : sizeOf x.snd < sizeOf (Expr.record rxs) := by + have h₁ := List.sizeOf_lt_of_mem hx + rw [Prod.mk.sizeOf_spec] at h₁ + simp only [Expr.record.sizeOf_spec] + omega + exact @level_based_slicing_is_sound_expr x.snd + exact level_based_slicing_is_sound_record hs hc hr ht hl ih +termination_by e + +theorem typecheck_policy_with_level_is_sound {p : Policy} {tx : TypedExpr} {n : Nat} {env : Environment} {request : Request} {entities slice : Entities} + (hs : slice = entities.sliceAtLevel request n) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (htl : typecheckPolicyWithLevel p n env = .ok tx) : + evaluate p.toExpr request entities = evaluate p.toExpr request slice +:= by + simp only [typecheckPolicyWithLevel, typecheckPolicy] at htl + split at htl <;> try contradiction + rename_i tx' _ htx' + cases htl₁ : tx'.typeOf ⊑ .bool .anyBool <;> simp only [htl₁, Bool.false_eq_true, ↓reduceIte, Except.bind_err, Except.bind_ok, reduceCtorEq] at htl + split at htl <;> simp only [reduceCtorEq, Except.ok.injEq] at htl + subst htl + rename_i htl' + have subst_action_preserves_entities := (@substitute_action_preserves_evaluation · · entities) + have subst_action_preserves_slice := (@substitute_action_preserves_evaluation · · slice) + rw [←subst_action_preserves_slice, ←subst_action_preserves_entities, action_matches_env hr] + rw [←level_spec] at htl' + have hc := empty_capabilities_invariant request entities + exact level_based_slicing_is_sound_expr hs hc hr htx' htl' + +theorem typecheck_policy_at_level_with_environments_is_sound {p : Policy} {envs : List Environment} {n : Nat} {request : Request} {entities slice : Entities} + (hs : slice = entities.sliceAtLevel request n) + (he : ∃ env ∈ envs, RequestAndEntitiesMatchEnvironment env request entities) + (htl : typecheckPolicyWithLevelWithEnvironments p n envs = .ok ()) : + evaluate p.toExpr request entities = evaluate p.toExpr request slice +:= by + replace htl : ∀ x ∈ envs, ∃ tx, typecheckPolicyWithLevel p n x = .ok tx := by + cases htl₁ : List.mapM (typecheckPolicyWithLevel p n) envs <;> + simp only [htl₁, typecheckPolicyWithLevelWithEnvironments, Except.bind_err, reduceCtorEq] at htl + replace htl₁ := List.forall₂_implies_all_left ∘ List.mapM_ok_iff_forall₂.mp $ htl₁ + intro env he + specialize htl₁ env he + simp only [htl₁.imp, and_imp, imp_self, implies_true] + have ⟨env, ⟨he₁, hr⟩⟩ := he + specialize htl env he₁ + replace ⟨_, htl⟩ := htl + exact typecheck_policy_with_level_is_sound hs hr htl + +theorem validate_with_level_is_sound {ps : Policies} {schema : Schema} {n : Nat} {request : Request} {entities slice : Entities} + (hr : validateRequest schema request = .ok ()) + (he : validateEntities schema entities = .ok ()) + (hs : slice = entities.sliceAtLevel request n) + (htl : validateWithLevel ps schema n = .ok ()) : + isAuthorized request entities ps = isAuthorized request slice ps +:= by + have hsound : ∀ p ∈ ps, evaluate p.toExpr request entities = evaluate p.toExpr request slice := by + have hre := request_and_entities_validate_implies_match_schema _ _ _ hr he + replace htl := List.forM_ok_implies_all_ok _ _ htl + intro p hp + exact typecheck_policy_at_level_with_environments_is_sound hs hre (htl p hp) + exact is_authorized_congr_evaluate hsound diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/And.lean b/cedar-lean/Cedar/Thm/Validation/Levels/And.lean new file mode 100644 index 000000000..868bc0686 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/And.lean @@ -0,0 +1,72 @@ + +/- + 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 : tx.AtLevel env n) + (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₁ + specialize ih₁ hs hc hr htx₁ hl + simp only [evaluate, ←ih₁] + rcases he₁ with he₁ | he₁ | he₁ | he₁ <;> + simp [he₁, Result.as, Coe.coe, Value.asBool] + case isFalse => + replace ⟨ bty, tx₂, bty₂, c₂, htx, htx₂, hty₂, ht ⟩ := ht + replace ⟨ b₁ , hv₁⟩ := instance_of_bool_is_bool hv₁ + subst v₁ tx + cases hl ; rename_i hl₁ hl₂ + specialize ih₁ hs hc hr htx₁ hl₁ + simp only [evaluate, ←ih₁] + rcases he₁ with he₁ | he₁ | he₁ | he₁ <;> + simp only [he₁, Result.as, Bool.not_eq_eq_eq_not, Bool.not_true, Coe.coe, Value.asBool, Except.bind_err] + cases b₁ <;> simp only [Except.bind_ok, ↓reduceIte] + specialize hgc he₁ + specialize ih₂ hs (capability_union_invariant hc hgc) hr htx₂ hl₂ + simp [ih₂] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean new file mode 100644 index 000000000..d78eb7a90 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/Basic.lean @@ -0,0 +1,35 @@ +/- + 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 +import Cedar.Thm.Validation.Levels.CheckLevel + +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₁) → + tx.AtLevel env n → + evaluate e request entities = evaluate e request slice diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean new file mode 100644 index 000000000..ba67b28fd --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/BinaryApp.lean @@ -0,0 +1,115 @@ +/- + 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.Types +import Cedar.Thm.Validation.Slice +import Cedar.Thm.Validation.Levels.Basic + +/-! +This file proves that level checking for `.binaryApp` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem not_dereferencing_apply₂_invariant_entities {op : BinaryOp} {entities entities' : Entities} {v₁ v₂ : Value} + (hop : ¬ DereferencingBinaryOp op) + : apply₂ op v₁ v₂ entities = apply₂ op v₁ v₂ entities' +:= by + cases op <;> simp only [DereferencingBinaryOp, not_true_eq_false] at hop + all_goals + cases v₁ <;> cases v₂ <;> + simp only [apply₂] <;> + ( + rename_i p₁ p₂ + cases p₁ <;> cases p₂ + ) <;> + simp only + +theorem level_based_slicing_is_sound_inₑ {e₁ : Expr} {euid₁ euid₂ : EntityUID} {n : Nat} {c₀ c₁ : Capabilities} {entities slice : Entities} + (hc : CapabilitiesInvariant c₀ request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf e₁ c₀ env = Except.ok (tx₁, c₁)) + (hl : tx₁.EntityAccessAtLevel env n (n + 1) []) + (he : evaluate e₁ request entities = .ok (Value.prim (Prim.entityUID euid₁))) + (hs : some slice = entities.sliceAtLevel request (n + 1)) + : inₑ euid₁ euid₂ entities = inₑ euid₁ euid₂ slice +:= by + simp only [inₑ] + cases heq : euid₁ == euid₂ <;> simp only [Bool.false_or, Bool.true_or] + have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl he hs + simp [hfeq, Entities.ancestorsOrEmpty] + +theorem level_based_slicing_is_sound_binary_app {op : BinaryOp} {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 (.binaryApp op e₁ e₂) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ihe₁ : TypedAtLevelIsSound e₁) + (ihe₂ : TypedAtLevelIsSound e₂) + : evaluate (.binaryApp op e₁ e₂) request entities = evaluate (.binaryApp op e₁ e₂) request slice +:= by + replace ⟨tx₁, c₁, tx₂, c₂, htx₁, htx₂, ty, htx⟩ := type_of_binaryApp_inversion ht + subst tx + simp only [evaluate] + cases hl + case getTag hel hl₁ hl₂ | hasTag hel hl₁ hl₂ => + specialize ihe₂ hs hc hr htx₂ hl₂ + rw [←ihe₂] + have hl₁' := entity_access_at_level_then_at_level hl₁ + specialize ihe₁ hs hc hr htx₁ hl₁' + rw [←ihe₁] + cases he₁ : evaluate e₁ request entities <;> simp only [Except.bind_ok, Except.bind_err] + cases he₂ : evaluate e₂ request entities <;> simp only [Except.bind_ok, Except.bind_err] + rename_i v₁ v₂ + cases v₁ <;> cases v₂ <;> simp only [apply₂] + rename_i p₁ p₂ + cases p₁ <;> cases p₂ <;> simp only + rename_i euid _ + have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr htx₁ hl₁ he₁ hs + simp only [hfeq, hasTag, getTag, Entities.tagsOrEmpty, Entities.tags, Map.findOrErr] + case mem hel hl₁ hl₂ => + specialize ihe₂ hs hc hr htx₂ hl₂ + rw [←ihe₂] + have hl₁' := entity_access_at_level_then_at_level hl₁ + specialize ihe₁ hs hc hr htx₁ hl₁' + rw [←ihe₁] + cases he₁ : evaluate e₁ request entities <;> simp only [Except.bind_ok, Except.bind_err] + cases he₂ : evaluate e₂ request entities <;> simp only [Except.bind_ok, Except.bind_err] + rename_i v₁ v₂ + cases v₁ <;> cases v₂ <;> simp only [apply₂] + case prim => + rename_i p₁ p₂ + cases p₁ <;> cases p₂ <;> simp only + simp [level_based_slicing_is_sound_inₑ hc hr htx₁ hl₁ he₁ hs] + case set => + rename_i p₁ sv + cases p₁ <;> simp only + simp [inₛ, level_based_slicing_is_sound_inₑ hc hr htx₁ hl₁ he₁ hs] + case binaryApp hop hl₁ hl₂ => + specialize ihe₁ hs hc hr htx₁ hl₁ + specialize ihe₂ hs hc hr htx₂ hl₂ + rw [ihe₁, ihe₂] + simp [(@not_dereferencing_apply₂_invariant_entities op entities slice · · hop)] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Call.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Call.lean new file mode 100644 index 000000000..52f0b8a27 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/Call.lean @@ -0,0 +1,52 @@ +/- + 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.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_call {xs : List 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 (.call xfn xs) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ih : ∀ x ∈ xs, TypedAtLevelIsSound x) : + evaluate (.call xfn xs) request entities = evaluate (.call xfn xs) request slice +:= by + replace ⟨ txs, ⟨ty, hty⟩, ht ⟩ := type_of_call_inversion ht + subst tx + cases hl ; rename_i hl + + have he : ∀ x ∈ xs, evaluate x request entities = evaluate x request slice := by + intros x hx + replace ⟨ tx, htxs, c', htx ⟩ := List.forall₂_implies_all_left ht x hx + specialize hl tx htxs + exact ih x hx hs hc hr htx hl + + simp only [evaluate, List.mapM₁, List.attach, List.attachWith] + simp only [List.mapM_pmap_subtype (λ x : Expr => evaluate x request entities) xs] + simp only [List.mapM_pmap_subtype (λ x : Expr => evaluate x request slice) xs] + rw [List.mapM_congr he] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean b/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean new file mode 100644 index 000000000..3c27e2068 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/GetAttr.lean @@ -0,0 +1,109 @@ +/- + 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.Slice +import Cedar.Thm.Validation.Levels.Basic +import Cedar.Thm.Validation.Levels.CheckLevel + +/-! +This file proves that level checking for `.getAttr` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_get_attr_entity {e : Expr} {tx₁: TypedExpr} {ty : CedarType} {a : Attr} {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) + (hl : (tx₁.getAttr a ty).AtLevel env n) + (ht : typeOf e c₀ env = Except.ok (tx₁, c₁)) + (hety : tx₁.typeOf = CedarType.entity ety) + (ihe : TypedAtLevelIsSound e) + : evaluate (.getAttr e a) request entities = evaluate (.getAttr e a) request slice +:= by + have ⟨ hgc, v, he, hv ⟩ := type_of_is_sound hc hr ht + rw [hety] at hv + replace ⟨ euid, hety', hv⟩ := instance_of_entity_type_is_entity hv + subst hety' hv + cases hl + case getAttrRecord hnety _ => + specialize hnety euid.ty + contradiction + rename_i n hel₁ hl₁ _ + simp only [evaluate] + have hl₁' := entity_access_at_level_then_at_level hl₁ + specialize ihe hs hc hr ht hl₁' + rw [←ihe] + unfold EvaluatesTo at he + rcases he with he | he | he | he <;> simp only [he, Except.bind_err] + have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl₁ he hs + simp [hfeq, getAttr, attrsOf, Entities.attrs, Map.findOrErr] + +theorem level_based_slicing_is_sound_get_attr_record {e : Expr} {tx : TypedExpr} {ty : CedarType} {a : Attr} {n : Nat} {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) + (hl : (tx.getAttr a ty).AtLevel env n) + (htx : typeOf e c₀ env = Except.ok (tx, c₁')) + (hrty : tx.typeOf = CedarType.record rty) + (ihe : TypedAtLevelIsSound e) + : evaluate (.getAttr e a) request entities = evaluate (.getAttr e a) request slice +:= by + cases hl + case getAttr hety => + simp [hety] at hrty + rename_i hl + have ih := ihe hs hc hr htx hl + simp only [evaluate, ←ih] + cases he₁ : evaluate e request entities <;> simp only [Except.bind_err, Except.bind_ok] + rename_i v + have ⟨avs, he⟩ : ∃ avs, v = .record avs := by + have ⟨ _, _, he, hty⟩ := type_of_is_sound hc hr htx + rw [hrty] at hty + have ⟨avs, hv⟩ := instance_of_record_type_is_record hty + exists avs + simpa [EvaluatesTo, hv, he₁] using he + simp [he, getAttr, attrsOf] + +theorem level_based_slicing_is_sound_get_attr {e : Expr} {tx : TypedExpr} {a : Attr} {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 (e.getAttr a) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ihe : TypedAtLevelIsSound e) + : evaluate (.getAttr e a) request entities = evaluate (.getAttr e a) request slice +:= by + have ⟨ h₇, ty₁, _, ht, h₅, h₆ ⟩ := type_of_getAttr_inversion ht + rw [h₅] at hl + cases h₆ + case _ hety => + replace ⟨ ety, hety ⟩ := hety + exact level_based_slicing_is_sound_get_attr_entity hs hc hr hl ht hety ihe + case _ hrty => + replace ⟨ rty, hrty ⟩ := hrty + exact level_based_slicing_is_sound_get_attr_record hs hc hr hl ht hrty ihe diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean b/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean new file mode 100644 index 000000000..e9bfdfa55 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/HasAttr.lean @@ -0,0 +1,93 @@ +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.Slice +import Cedar.Thm.Validation.Levels.Basic +import Cedar.Thm.Validation.Levels.CheckLevel + +/-! +This file proves that level checking for `.hasAttr` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_has_attr_entity {e : Expr} {tx₁: TypedExpr} {ty : CedarType} {a : Attr} {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) + (hl : (tx₁.hasAttr a ty).AtLevel env n) + (ht : typeOf e c₀ env = Except.ok (tx₁, c₁)) + (hety : tx₁.typeOf = CedarType.entity ety) + (ihe : TypedAtLevelIsSound e) + : evaluate (.hasAttr e a) request entities = evaluate (.hasAttr e a) request slice +:= by + have ⟨ hgc, v, he, hv ⟩ := type_of_is_sound hc hr ht + rw [hety] at hv + replace ⟨ euid, hety', hv⟩ := instance_of_entity_type_is_entity hv + subst hety' hv + cases hl + case hasAttrRecord hnety _ => + specialize hnety euid.ty + contradiction + rename_i n hel₁ hl₁ _ + simp only [evaluate] + have hl₁' := entity_access_at_level_then_at_level hl₁ + specialize ihe hs hc hr ht hl₁' + rw [←ihe] + unfold EvaluatesTo at he + rcases he with he | he | he | he <;> simp only [he, Except.bind_err] + have hfeq := checked_eval_entity_find_entities_eq_find_slice hc hr ht hl₁ he hs + simp [hfeq, hasAttr, attrsOf, Entities.attrsOrEmpty] + +theorem level_based_slicing_is_sound_has_attr_record {e : Expr} {tx : TypedExpr} {a : Attr} {n : Nat} {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) + (hl : (tx.hasAttr a ty).AtLevel env n) + (htx : typeOf e c₀ env = Except.ok (tx, c₁')) + (hrty : tx.typeOf = CedarType.record rty) + (ihe : TypedAtLevelIsSound e) + : evaluate (.hasAttr e a) request entities = evaluate (.hasAttr e a) request slice +:= by + cases hl + case hasAttr hety => + simp [hety] at hrty + rename_i hl + have ih := ihe hs hc hr htx hl + simp only [evaluate, ←ih] + cases he₁ : evaluate e request entities <;> simp only [Except.bind_err, Except.bind_ok] + rename_i v + have ⟨avs, he⟩ : ∃ avs, v = .record avs := by + have ⟨ _, _, he, hty⟩ := type_of_is_sound hc hr htx + rw [hrty] at hty + have ⟨avs, hv⟩ := instance_of_record_type_is_record hty + exists avs + simpa [EvaluatesTo, hv, he₁] using he + simp [he, hasAttr, attrsOf] + +theorem level_based_slicing_is_sound_has_attr {e : Expr} {tx : TypedExpr} {a : Attr} {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 (e.hasAttr a) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ihe : TypedAtLevelIsSound e) + : evaluate (.hasAttr e a) request entities = evaluate (.hasAttr e a) request slice +:= by + have ⟨ h₇, ty₁, _, ht, h₅, h₆ ⟩ := type_of_hasAttr_inversion ht + rw [h₅] at hl + cases h₆ + case _ hety => + replace ⟨ ety, hety ⟩ := hety + exact level_based_slicing_is_sound_has_attr_entity hs hc hr hl ht hety ihe + case _ hrty => + replace ⟨ rty, hrty ⟩ := hrty + exact level_based_slicing_is_sound_has_attr_record hs hc hr hl ht hrty ihe diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean b/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean new file mode 100644 index 000000000..d182b0c78 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/IfThenElse.lean @@ -0,0 +1,85 @@ +/- + 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 `.ite` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_if {x₁ x₂ x₃ : 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) + (htx : typeOf (.ite x₁ x₂ x₃) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ih₁ : TypedAtLevelIsSound x₁) + (ih₂ : TypedAtLevelIsSound x₂) + (ih₃ : TypedAtLevelIsSound x₃) + : evaluate (.ite x₁ x₂ x₃) request entities = evaluate (.ite x₁ x₂ x₃) request slice +:= by + replace ⟨tx₁, bty₁, c₁, tx₂, c₂, tx₃, c₃, htx, htx₁, hty₁, htx₂₃ ⟩ := type_of_ite_inversion htx + have ⟨ hgc, v₁, he₁, hv₁ ⟩ := type_of_is_sound hc hr htx₁ + rw [hty₁] at hv₁ + rw [htx] at hl + cases hl + rename_i hl₁ hl₂ hl₃ + specialize ih₁ hs hc hr htx₁ hl₁ + simp only [ih₁, evaluate] + cases he₁' : Result.as Bool (evaluate x₁ request slice) <;> simp only [Except.bind_err, Except.bind_ok] + rename_i b + replace he₁' : evaluate x₁ request slice = .ok (.prim (.bool b)) := by + simp only [Result.as, Coe.coe, Value.asBool] at he₁' + split at he₁' <;> try simp only [reduceCtorEq] at he₁' + split at he₁' <;> try simp only [reduceCtorEq, Except.ok.injEq] at he₁' + rw [←he₁'] + assumption + split at htx₂₃ + · replace he₁ : b = false := by + simpa [ih₁, he₁', instance_of_ff_is_false hv₁, EvaluatesTo] using he₁ + subst he₁ + specialize ih₃ hs hc hr htx₂₃.left hl₃ + simp [ih₃] + · replace he₁ : b = true := by + simpa [ih₁, he₁', instance_of_tt_is_true hv₁, EvaluatesTo] using he₁ + subst he₁ + replace hgc : CapabilitiesInvariant c₁ request entities := by + simpa [GuardedCapabilitiesInvariant, ih₁, he₁'] using hgc + specialize ih₂ hs (capability_union_invariant hc hgc) hr htx₂₃.left hl₂ + simp [ih₂] + · replace ⟨htx₂, htx₃, _, _⟩ := htx₂₃ + specialize ih₃ hs hc hr htx₃ hl₃ + simp only [ih₁, ih₃, evaluate] + cases b + case false => simp + case true => + replace hgc : CapabilitiesInvariant c₁ request entities := by + simpa [GuardedCapabilitiesInvariant, ih₁, he₁'] using hgc + specialize ih₂ hs (capability_union_invariant hc hgc) hr htx₂ hl₂ + simp [ih₂] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean new file mode 100644 index 000000000..7e653487f --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/Or.lean @@ -0,0 +1,70 @@ + +/- + 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 `.or` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_or {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 (.or e₁ e₂) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ih₁ : TypedAtLevelIsSound e₁) + (ih₂ : TypedAtLevelIsSound e₂) + : evaluate (.or e₁ e₂) request entities = evaluate (.or e₁ e₂) request slice +:= by + replace ⟨ tx₁, bty, c', htx₁, hty₁, ht ⟩ := type_of_or_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_tt_is_true hv₁ + subst v₁ + unfold EvaluatesTo at he₁ + simp only [evaluate] + 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 ⟨ bt, tx₂, bty₂, c₂, htx, htx₂, hty₂, ht ⟩ := ht + subst tx + cases hl + rename_i hl₁ hl₂ + specialize ih₁ hs hc hr htx₁ hl₁ + specialize ih₂ hs hc hr htx₂ hl₂ + simp only [evaluate] + rw [ih₁, ih₂] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean new file mode 100644 index 000000000..e3ee4e9aa --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/Record.lean @@ -0,0 +1,82 @@ +/- + 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 `.record` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_record_attrs {rxs : List (Attr × Expr)} {n : Nat} {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 : List.Forall₂ (AttrExprHasAttrType c env) rxs atxs) + (hl : ∀ atx ∈ atxs, atx.snd.AtLevel env n) + (ih : ∀ x ∈ rxs, TypedAtLevelIsSound x.snd) + : + (rxs.mapM₂ λ x => do + let v ← (evaluate x.1.snd request entities) + Except.ok (x.1.fst, v)) = + (rxs.mapM₂ λ x => do + let v ← (evaluate x.1.snd request slice) + Except.ok (x.1.fst, v)) +:= by + cases ht + case nil => + simp [List.attach₂, List.mapM₂] + case cons x tx rxs' txs' htx ht => + simp only [List.mem_cons, forall_eq_or_imp] at ih hl + replace ⟨ ihx, ih ⟩ := ih + replace ⟨ hlx, hl ⟩ := hl + replace ⟨ _, _, htx ⟩ := htx + specialize ihx hs hc hr htx hlx + simp only [←ihx, List.mapM₂, List.attach₂, List.pmap_cons, List.mapM_cons] + cases he₁ : evaluate x.snd request entities <;> simp only [Except.bind_err, Except.bind_ok] + have ih' := level_based_slicing_is_sound_record_attrs hs hc hr ht hl ih + simp only [List.mapM₂, List.attach₂] at ih' + simp only [List.mapM_pmap_subtype (λ x : (Attr × Expr) => do let v ← evaluate x.snd request entities; .ok (x.fst, v)) rxs'] at ih' ⊢ + simp only [List.mapM_pmap_subtype (λ x : (Attr × Expr) => do let v ← evaluate x.snd request slice; .ok (x.fst, v)) rxs'] at ih' ⊢ + rw [ih'] + +theorem level_based_slicing_is_sound_record {rxs : List (Attr × 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 (.record rxs) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ih : ∀ x ∈ rxs, TypedAtLevelIsSound x.snd) : + evaluate (.record rxs) request entities = evaluate (.record rxs) request slice +:= by + replace ⟨ hc₁, atxs, htx, hatxs ⟩ := type_of_record_inversion ht + subst htx + cases hl + rename_i hlatxs + have h := level_based_slicing_is_sound_record_attrs hs hc hr hatxs hlatxs ih + simp only [h, evaluate, bindAttr, pure, Except.pure] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/Set.lean b/cedar-lean/Cedar/Thm/Validation/Levels/Set.lean new file mode 100644 index 000000000..48e28aedf --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/Set.lean @@ -0,0 +1,52 @@ +/- + 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.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_set {xs : List 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 (.set xs) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ih : ∀ x ∈ xs, TypedAtLevelIsSound x) : + evaluate (.set xs) request entities = evaluate (.set xs) request slice +:= by + replace ⟨ _, txs, ty, htx, ht ⟩ := type_of_set_inversion ht + subst tx + cases hl ; rename_i hl + + have he : ∀ x ∈ xs, evaluate x request entities = evaluate x request slice := by + intros x hx + replace ⟨ tx, _, htxs, htx, _ ⟩ := ht x hx + specialize hl tx htxs + exact ih x hx hs hc hr htx hl + + simp only [evaluate, List.mapM₁, List.attach, List.attachWith] + simp only [List.mapM_pmap_subtype (λ x : Expr => evaluate x request entities) xs] + simp only [List.mapM_pmap_subtype (λ x : Expr => evaluate x request slice) xs] + rw [List.mapM_congr he] diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean new file mode 100644 index 000000000..a9e15f2f8 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Levels/UnaryApp.lean @@ -0,0 +1,49 @@ +/- + 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.Types +import Cedar.Thm.Validation.Levels.Basic + +/-! +This file proves that level checking for `.unaryApp` expressions is sound. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem level_based_slicing_is_sound_unary_app {op : UnaryOp} {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 (.unaryApp op e) c₀ env = Except.ok (tx, c₁)) + (hl : tx.AtLevel env n) + (ihe : TypedAtLevelIsSound e) + : evaluate (.unaryApp op e) request entities = evaluate (.unaryApp op e) request slice +:= by + replace ⟨hc₁, tx₁, ty, c₁', htx, htx₁, ht⟩ := type_of_unary_inversion ht + subst tx + cases hl + rename_i hl₁ + specialize ihe hs hc hr htx₁ hl₁ + simp [evaluate, ihe] diff --git a/cedar-lean/Cedar/Thm/Validation/Slice.lean b/cedar-lean/Cedar/Thm/Validation/Slice.lean new file mode 100644 index 000000000..02a45d4d3 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice.lean @@ -0,0 +1,117 @@ +/- + 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.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel +import Cedar.Thm.Validation.Validator + +import Cedar.Thm.Validation.Slice.Reachable + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem slice_at_level_inner_well_formed {entities : Entities} {work slice : Set EntityUID} {n : Nat} + (hs : Entities.sliceAtLevel.sliceAtLevel entities work n = some slice) : + slice.WellFormed +:= by + unfold Entities.sliceAtLevel.sliceAtLevel at hs + split at hs + · injections hs + subst hs + exact Set.empty_wf + · replace ⟨ _, _, hs⟩ : ∃ s₀ s₁, s₀ ∪ s₁ = slice := by + cases hs₁ : work.elts.mapM (Map.find? entities) <;> + simp only [hs₁, Option.map_eq_map, Option.bind_eq_bind, Option.bind_none_fun, Option.bind_some_fun, reduceCtorEq] at hs + rename_i n eds + cases hs₂ : eds.mapM (Entities.sliceAtLevel.sliceAtLevel entities ·.sliceEUIDs n) <;> + simp only [hs₂, Option.map_none', Option.map_some', Option.none_bind, Option.some_bind, reduceCtorEq, Option.some.injEq] at hs + rename_i slice' + exists work, (slice'.mapUnion id) + subst hs + simp only [Set.union_wf] + +theorem checked_eval_entity_in_slice {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {slice entities : Entities} {ed : EntityData} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf e c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax []) + (he : evaluate e request entities = .ok (Value.prim (Prim.entityUID euid))) + (hf : entities.find? euid = some ed) + (hs : slice = Entities.sliceAtLevel entities request (n + 1)) : + slice.find? euid = some ed +:= by + simp only [Entities.sliceAtLevel] at hs + cases hs₁ : Entities.sliceAtLevel.sliceAtLevel entities request.sliceEUIDs (n + 1) <;> + simp only [hs₁, Option.bind_none_fun, reduceCtorEq] at hs + rename_i eids + cases hs₂ : (eids.elts.mapM (λ e => (Map.find? entities e).bind λ ed => some (e, ed))) <;> + simp only [hs₂, Option.bind_eq_bind, Option.bind_some_fun, Option.none_bind, reduceCtorEq, Option.some_bind, Option.some.injEq] at hs + subst hs + have hf₁ : Map.contains entities euid := by simp [Map.contains, hf] + have hw : ReachableIn entities request.sliceEUIDs euid (n + 1) := + checked_eval_entity_reachable hc hr ht hl he (.euid euid) hf₁ + have hi := slice_contains_reachable hw hs₁ + rw [←hf] + rename_i eds + replace hmake : Map.mk eds = Map.make eds := by + have hsorted := eids.wf_iff_sorted.mp (slice_at_level_inner_well_formed hs₁) + have hsbfst := List.mapM_key_id_sortedBy_key hs₂ hsorted + have hwf : (Map.mk eds).WellFormed := by + simpa [Map.wf_iff_sorted] using hsbfst + simpa [Map.WellFormed] using hwf + have hmk := Map.find?_mapM_key_id hs₂ hi + simpa [hmake] using hmk + +theorem not_entities_then_not_slice {n: Nat} {request : Request} {uid : EntityUID} {entities slice : Entities} + (hs : some slice = Entities.sliceAtLevel entities request n) + (hse : entities.find? uid = none) + : slice.find? uid = none +:= by + simp only [Entities.sliceAtLevel] at hs + cases hs₁ : Entities.sliceAtLevel.sliceAtLevel entities request.sliceEUIDs n <;> + simp only [hs₁, Option.bind_none_fun, reduceCtorEq] at hs + rename_i eids + cases hs₂ : (eids.elts.mapM (λ e => (entities.find? e).bind λ ed => some (e, ed))) <;> + simp only [hs₂, Option.bind_eq_bind, Option.bind_some_fun, Option.none_bind, reduceCtorEq, Option.some_bind, Option.some.injEq] at hs + subst hs + exact Map.mapM_key_id_key_none_implies_find?_none hs₂ hse + +/-- +If an expression checks at level `n` and then evaluates to an entity, then the +data for that entity in the slice will be hte same as in the original entities. +-/ +theorem checked_eval_entity_find_entities_eq_find_slice {n nmax : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {slice entities : Entities} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf e c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax []) + (he : evaluate e request entities = .ok (Value.prim (Prim.entityUID euid))) + (hs : slice = Entities.sliceAtLevel entities request (n + 1)) : + slice.find? euid = entities.find? euid +:= by + cases hfe : Map.find? entities euid + case none => + exact not_entities_then_not_slice hs hfe + case some => + exact checked_eval_entity_in_slice hc hr ht hl he hfe hs diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable.lean new file mode 100644 index 000000000..d2be6e3ba --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable.lean @@ -0,0 +1,280 @@ +/- + 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.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel +import Cedar.Thm.Validation.Validator + +import Cedar.Thm.Validation.Slice.Reachable.Basic +import Cedar.Thm.Validation.Slice.Reachable.BinaryApp +import Cedar.Thm.Validation.Slice.Reachable.GetAttr +import Cedar.Thm.Validation.Slice.Reachable.IfThenElse +import Cedar.Thm.Validation.Slice.Reachable.Record +import Cedar.Thm.Validation.Slice.Reachable.Var + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + + +theorem checked_eval_entity_lit_is_action {p : Prim} {n nmax : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {entities : Entities} {path : List Attr} + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf (.lit p) c env = .ok (tx, c')) + (he : evaluate (.lit p) request entities = .ok v) + (hel : tx.EntityAccessAtLevel env n nmax path) + (ha : Value.EuidViaPath v path euid) : + request.action = euid +:= by + cases p + case entityUID => + replace he : euid = env.reqty.action := by + replace ⟨ _, ht ⟩ := type_of_lit_inversion ht + rw [←ht] at hel + cases hel + simp only [evaluate, Except.ok.injEq] at he + rw [←he] at ha + cases ha + rfl + simp only [action_matches_env hr, he] + all_goals + simp only [evaluate, Except.ok.injEq] at he + rw [←he] at ha + cases ha + +theorem and_not_euid_via_path {e₁ e₂: Expr} {entities : Entities} {path : List Attr} + (he : evaluate (.and e₁ e₂) request entities = .ok v) : + ¬ Value.EuidViaPath v path euid +:= by + have he' := and_produces_bool_or_error e₁ e₂ request entities + split at he' <;> + first + | contradiction + | rename_i he'' + simp only [he'', Except.ok.injEq, reduceCtorEq] at he + subst v + intro ha + cases ha + +theorem or_not_euid_via_path {e₁ e₂: Expr} {entities : Entities} {path : List Attr} + (he : evaluate (.or e₁ e₂) request entities = .ok v) : + ¬ Value.EuidViaPath v path euid +:= by + intro ha + simp only [evaluate] at he + cases he₁ : Result.as Bool (evaluate e₁ request entities) <;> + simp only [he₁, bind_pure_comp, Except.bind_err, Except.bind_ok, reduceCtorEq] at he + split at he + · simp only [Except.ok.injEq] at he + subst he ; cases ha + · cases he₂ : Result.as Bool (evaluate e₂ request entities) <;> + simp only [he₂, Except.map_error, reduceCtorEq, Except.map_ok, Except.ok.injEq] at he + subst he ; cases ha + +theorem unary_not_euid_via_path {op : UnaryOp} {e₁ : Expr} {entities : Entities} {path : List Attr} + (he : evaluate (.unaryApp op e₁) request entities = .ok v) : + ¬ Value.EuidViaPath v path euid +:= by + intro ha + simp only [evaluate] at he + cases he₁ : evaluate e₁ request entities <;> + simp only [he₁, intOrErr, apply₁, Except.bind_err, Except.bind_ok, reduceCtorEq] at he + (split at he <;> try split at he) <;> + try simp only [reduceCtorEq] at he + all_goals + simp only [Except.ok.injEq] at he + rw [←he] at ha + cases ha + +theorem has_attr_not_euid_via_path {e₁ : Expr} {a : Attr} {entities : Entities} {path : List Attr} + (he : evaluate (.hasAttr e₁ a) request entities = .ok v) : + ¬ Value.EuidViaPath v path euid +:= by + intro ha + simp only [evaluate] at he + cases he₁ : evaluate e₁ request entities <;> + simp only [he₁, Except.bind_err, reduceCtorEq, hasAttr, Except.bind_ok] at he + rename_i v₁ + cases he₂ : attrsOf v₁ λ uid => Except.ok (entities.attrsOrEmpty uid) <;> + simp only [he₂, Except.ok.injEq, Except.bind_ok, Except.bind_err, reduceCtorEq] at he + subst he ; cases ha + +theorem set_not_euid_via_path {xs : List Expr} {entities : Entities} {path : List Attr} + (he : evaluate (.set xs) request entities = .ok v) : + ¬ Value.EuidViaPath v path euid +:= by + intro ha + simp only [evaluate] at he + cases he₁ : (xs.mapM₁ (λ x => evaluate x.val request entities)) <;> + simp only [he₁, Except.bind_err, Except.bind_ok, Except.ok.injEq, reduceCtorEq] at he + subst he ; cases ha + +theorem call_not_euid_via_path {xfn : ExtFun} {xs : List Expr} {entities : Entities} {path : List Attr} + (he : evaluate (.call xfn xs) request entities = .ok v) : + ¬ Value.EuidViaPath v path euid +:= by + intro ha + simp only [evaluate] at he + cases he₁ : xs.mapM₁ fun x => evaluate x.val request entities <;> + simp only [he₁, Except.bind_err, reduceCtorEq] at he + + simp only [call, res, Except.bind_ok] at he + (split at he <;> try split at he) <;> + simp only [Except.ok.injEq, reduceCtorEq] at he + + all_goals + rw [←he] at ha + cases ha + +/-- +If an expression checks at level `n` and then evaluates an entity (or a record +containing an entity), then that entity must reachable in `n + 1` steps. +-/ +theorem checked_eval_entity_reachable {e : Expr} {n nmax: Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {request : Request} {entities : Entities} {v : Value} {path : List Attr} {euid : EntityUID} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf e c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax path) + (he : evaluate e request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (hf : entities.contains euid) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + cases e + case lit => + have hi : euid ∈ request.sliceEUIDs := by + have hact := checked_eval_entity_lit_is_action hr ht he hl ha + simp [hact, Request.sliceEUIDs, Set.mem_union_iff_mem_or, ←Set.make_mem] + exact ReachableIn.in_start hi + + case var => + exact var_entity_reachable he ha hf + + case ite e₁ e₂ e₃ => + have ih₂ := @checked_eval_entity_reachable e₂ + have ih₃ := @checked_eval_entity_reachable e₃ + exact checked_eval_entity_reachable_ite hc hr ht hl he ha hf ih₂ ih₃ + + case and => + exfalso + exact and_not_euid_via_path he ha + + case or e=> + exfalso + exact or_not_euid_via_path he ha + + case unaryApp op e => + exfalso + exact unary_not_euid_via_path he ha + + case binaryApp op e₁ e₂ => + have ih₁ := @checked_eval_entity_reachable e₁ + exact checked_eval_entity_reachable_binary hc hr ht hl he ha ih₁ + + case getAttr e _ => + have ih := @checked_eval_entity_reachable e + exact checked_eval_entity_reachable_get_attr hc hr ht hl he ha hf ih + + case hasAttr e a => + exfalso + exact has_attr_not_euid_via_path he ha + + case set es => + exfalso + exact set_not_euid_via_path he ha + + case record rxs => + have ih : ∀ a x, (Map.make rxs).find? a = some x → CheckedEvalEntityReachable x := by + intros a x hfx + have : sizeOf x < sizeOf (Expr.record rxs) := by + replace he := Map.make_mem_list_mem (Map.find?_mem_toList hfx) + have h₁ := List.sizeOf_lt_of_mem he + rw [Prod.mk.sizeOf_spec a x] at h₁ + simp only [Expr.record.sizeOf_spec, gt_iff_lt] + omega + exact @checked_eval_entity_reachable x + exact checked_eval_entity_reachable_record hc hr ht hl he ha hf ih + + case call xfn args => + exfalso + exact call_not_euid_via_path he ha +termination_by e + +theorem in_work_then_in_slice {entities : Entities} {work slice : Set EntityUID} {euid : EntityUID} {n : Nat} + (hw : euid ∈ work) + (hs : Entities.sliceAtLevel.sliceAtLevel entities work (n + 1) = some slice) + : euid ∈ slice +:= by + unfold Entities.sliceAtLevel.sliceAtLevel at hs + cases hs₁ : + List.mapM (Map.find? entities) work.elts + <;> simp only [hs₁, Option.map_eq_map, Option.bind_eq_bind, Option.bind_none_fun, reduceCtorEq] at hs + rename_i eds + cases hs₂ : + List.mapM (λ x => Entities.sliceAtLevel.sliceAtLevel entities x.sliceEUIDs n) eds + <;> simp only [hs₂, Option.map_none', Option.map_some', Option.none_bind, Option.some_bind, reduceCtorEq,Option.some.injEq] at hs + rename_i slice' + subst hs + have ⟨ _, hc ⟩ := Set.mem_union_iff_mem_or work (slice'.mapUnion id) euid + apply hc + simp [hw] + +/-- +If an entity is reachable in `n` steps, then it must be included in slice at +`n`. This lemma talks about the inner slicing function, so it's possible that +the entity isn't in the original entities if it's in `work`. +-/ +theorem slice_contains_reachable {n: Nat} {work : Set EntityUID} {euid : EntityUID} {entities : Entities} {slice : Set EntityUID} + (hw : ReachableIn entities work euid (n + 1)) + (hs : Entities.sliceAtLevel.sliceAtLevel entities work (n + 1) = some slice) : + euid ∈ slice +:= by + cases hw + case in_start hw => + exact in_work_then_in_slice hw hs + case step ed euid' hf hi hw => + unfold Entities.sliceAtLevel.sliceAtLevel at hs + cases hs₁ : (List.mapM (Map.find? entities) work.elts) <;> + simp only [hs₁, Option.bind_none_fun, reduceCtorEq] at hs + rename_i eds + cases hs₂ : Option.map (List.mapUnion id) (List.mapM (λ x => Entities.sliceAtLevel.sliceAtLevel entities x.sliceEUIDs n) eds) <;> + simp only [hs₂, Option.map_eq_map, Option.bind_eq_bind, Option.bind_some_fun, Option.none_bind, reduceCtorEq, Option.some_bind, Option.some.injEq] at hs + subst hs + rename_i slice' + cases hs₃ : List.mapM (λ x => Entities.sliceAtLevel.sliceAtLevel entities x.sliceEUIDs n) eds <;> + simp only [hs₃, Option.map_some', Option.some.injEq, Option.map_none', reduceCtorEq] at hs₂ + subst hs₂ + rw [Set.mem_union_iff_mem_or] + right + have ⟨ ed, hi₁, hf₁ ⟩ := List.mapM_some_implies_all_some hs₁ _ hi + have ⟨ slice, _, hs ⟩ := List.mapM_some_implies_all_some hs₃ _ hi₁ + rw [hf₁] at hf ; injections hf ; subst hf + cases hs₄ : Entities.sliceAtLevel.sliceAtLevel entities ed.sliceEUIDs n <;> + simp only [hs₄, reduceCtorEq, Option.some.injEq] at hs + match n with + | 0 => cases hw + | n + 1 => + have ih := slice_contains_reachable hw hs₄ + rw [Set.mem_mapUnion_iff_mem_exists] + subst hs + rename_i ed_slice _ + exists ed_slice diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Basic.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Basic.lean new file mode 100644 index 000000000..175bb8adb --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Basic.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.Spec +import Cedar.Data +import Cedar.Validation +import Cedar.Thm.Validation.Typechecker +import Cedar.Thm.Validation.Typechecker.Types +import Cedar.Thm.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +inductive ReachableIn : Entities → Set EntityUID → EntityUID → Nat → Prop where + | in_start {es : Entities} {start : Set EntityUID} {finish : EntityUID} {level : Nat} + (hs : finish ∈ start) : + ReachableIn es start finish (level + 1) + | step {es : Entities} {start : Set EntityUID} {finish : EntityUID} {level : Nat} {ed : EntityData} + (i : EntityUID) + (hi : i ∈ start) + (he : es.find? i = some ed) + (hr : ReachableIn es ed.sliceEUIDs finish level) : + ReachableIn es start finish (level + 1) + +inductive Value.EuidViaPath : Value → List Attr → EntityUID → Prop where + | euid (euid : EntityUID) : + EuidViaPath (.prim (.entityUID euid)) [] euid + | record {a : Attr} {path : List Attr} {attrs : Map Attr Value} + (ha : attrs.find? a = some v) + (hv : EuidViaPath v path euid) : + EuidViaPath (.record attrs) (a :: path) euid + +theorem in_val_then_val_slice + (hv : Value.EuidViaPath v path euid) + : euid ∈ v.sliceEUIDs +:= by + cases v + case prim p => + cases hv + simp [Value.sliceEUIDs, Set.mem_singleton] + case record attrs => + suffices h : ∃ kv ∈ attrs.kvs, euid ∈ kv.snd.sliceEUIDs by + unfold Value.sliceEUIDs List.attach₃ + simpa [ + Set.mem_mapUnion_iff_mem_exists, + List.mapUnion_pmap_subtype (λ e : (Attr × Value) => e.snd.sliceEUIDs) attrs.1 + ] using h + cases hv + rename_i v a _ ha hv + exists (a, v) + and_intros + · exact Map.find?_mem_toList ha + · exact in_val_then_val_slice hv + case set | ext => cases hv + +def CheckedEvalEntityReachable (e : Expr) := + ∀ {n nmax: Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {request : Request} {entities : Entities} {v: Value} {path : List Attr} {euid : EntityUID}, + CapabilitiesInvariant c request entities → + RequestAndEntitiesMatchEnvironment env request entities → + typeOf e c env = .ok (tx, c') → + tx.EntityAccessAtLevel env n nmax path → + evaluate e request entities = .ok v → + Value.EuidViaPath v path euid → + entities.contains euid → + ReachableIn entities request.sliceEUIDs euid (n + 1) + +theorem reachable_succ {n : Nat} {euid : EntityUID} {start : Set EntityUID} {entities : Entities} + (hr : ReachableIn entities start euid n) + : ReachableIn entities start euid (n + 1) +:= by + cases hr + case in_start hi => + exact ReachableIn.in_start hi + case step euid' hf hi hr => + exact ReachableIn.step euid' hi hf (reachable_succ hr) + +theorem entities_attrs_then_find? {entities: Entities} {attrs : Map Attr Value} {uid : EntityUID} + (he : entities.attrs uid = .ok attrs) + : ∃ ed, entities.find? uid = some ed ∧ ed.attrs = attrs +:= by + simp only [Entities.attrs, Map.findOrErr] at he + split at he <;> simp only [Except.bind_err, Except.bind_ok, reduceCtorEq, Except.ok.injEq] at he + rename_i ed h₁ + exists ed + +theorem entities_tags_then_find? {entities: Entities} {tags : Map Tag Value} {uid : EntityUID} + (he : entities.tags uid = .ok tags) + : ∃ ed, entities.find? uid = some ed ∧ ed.tags = tags +:= by + simp only [Entities.tags, Map.findOrErr] at he + split at he <;> simp only [Except.bind_err, Except.bind_ok, reduceCtorEq, Except.ok.injEq] at he + rename_i ed h₁ + exists ed diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/BinaryApp.lean new file mode 100644 index 000000000..207c904c5 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/BinaryApp.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.Spec +import Cedar.Data +import Cedar.Validation +import Cedar.Thm.Validation.Typechecker +import Cedar.Thm.Validation.Typechecker.Types +import Cedar.Thm.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel + +import Cedar.Thm.Validation.Slice.Reachable.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem reachable_tag_step {n : Nat} {euid euid' : EntityUID} {start : Set EntityUID} {entities : Entities} {ed : EntityData} {tag : Tag} {path : List Attr} + (hr : ReachableIn entities start euid n) + (he₁ : entities.find? euid = some ed) + (he₂ : ed.tags.find? tag = some tv) + (he₃ : Value.EuidViaPath tv path euid') : + ReachableIn entities start euid' (n + 1) +:= by + cases hr + case in_start n' hi => + have he₄ : euid' ∈ ed.sliceEUIDs := by + suffices h : ∃ v ∈ ed.tags.values, euid' ∈ v.sliceEUIDs by + simp [h, EntityData.sliceEUIDs, Set.mem_union_iff_mem_or, Set.mem_mapUnion_iff_mem_exists] + exists tv + constructor + · exact Map.find?_some_implies_in_values he₂ + · exact in_val_then_val_slice he₃ + have hr' : ReachableIn entities ed.sliceEUIDs euid' (n' + 1) := + ReachableIn.in_start he₄ + exact ReachableIn.step euid hi he₁ hr' + case step n' ed' euid'' he₁' hi hr' => + have ih := reachable_tag_step hr' he₁ he₂ he₃ + exact ReachableIn.step euid'' hi he₁' ih + +theorem checked_eval_entity_reachable_get_tag {e₁ e₂: Expr} {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {entities : Entities} {path : List Attr} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf (.binaryApp .getTag e₁ e₂) c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax path) + (he : evaluate (.binaryApp .getTag e₁ e₂) request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (ih₁ : CheckedEvalEntityReachable e₁) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + simp only [evaluate] at he + cases he₁ : evaluate e₁ request entities <;> simp only [he₁, Except.bind_err, Except.bind_ok, reduceCtorEq] at he + cases he₂ : evaluate e₂ request entities <;> simp only [he₂, Except.bind_err, Except.bind_ok, reduceCtorEq] at he + simp only [apply₂] at he + split at he <;> try contradiction + rename_i euid' _ _ + + have ⟨hc', ety, ty, tx₁, tx₂, c₁', c₂', htx₁, hty₁, htx₂, hty₂, ht, htx, hc₁⟩ := type_of_getTag_inversion ht + subst htx hc' + cases hl + rename_i hl₁ hl₂ + simp only [getTag] at he + cases he₃ : entities.tags euid' <;> simp only [he₃, Except.bind_ok, Except.bind_err, reduceCtorEq] at he + simp only [Map.findOrErr] at he + split at he <;> simp only [reduceCtorEq, Except.ok.injEq] at he + subst he + rename_i hv + + have ⟨ ed, hed, hed' ⟩ := entities_tags_then_find? he₃ + subst hed' + have hf' : entities.contains euid' := by simp [Map.contains, Option.isSome, hed] + + have ih := ih₁ hc hr htx₁ hl₁ he₁ (.euid euid') hf' + exact reachable_tag_step ih hed hv ha + +theorem binary_op_not_euid_via_path {op : BinaryOp} {e₁ e₂: Expr} {entities : Entities} {path : List Attr} + (hop : op ≠ .getTag) + (he : evaluate (.binaryApp op e₁ e₂) request entities = .ok v) : + ¬Value.EuidViaPath v path euid +:= by + intro ha + simp only [evaluate] at he + cases he₁ : evaluate e₁ request entities <;> simp only [he₁, Except.bind_err, Except.bind_ok, reduceCtorEq] at he + cases he₂ : evaluate e₂ request entities <;> simp only [he₂, Except.bind_err, Except.bind_ok, reduceCtorEq] at he + simp only [apply₂, intOrErr, inₛ, hasTag] at he + split at he <;> try split at he + all_goals first + | contradiction + | simp only [Except.ok.injEq] at he + rw [←he] at ha + cases ha + | rename_i vs + cases he₃ : Set.mapOrErr Value.asEntityUID vs Error.typeError <;> simp only [he₃, Except.bind_err, Except.bind_ok, reduceCtorEq, Except.ok.injEq] at he + rw [←he] at ha + cases ha + +theorem checked_eval_entity_reachable_binary {op : BinaryOp} {e₁ e₂: Expr} {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {entities : Entities} {path : List Attr} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf (.binaryApp op e₁ e₂) c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax path) + (he : evaluate (.binaryApp op e₁ e₂) request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (ih₁ : CheckedEvalEntityReachable e₁) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + cases hop : op == .getTag <;> simp only [beq_eq_false_iff_ne, beq_iff_eq] at hop + · exfalso + exact binary_op_not_euid_via_path hop he ha + · subst op + exact checked_eval_entity_reachable_get_tag hc hr ht hl he ha ih₁ diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/GetAttr.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/GetAttr.lean new file mode 100644 index 000000000..557fdfccd --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/GetAttr.lean @@ -0,0 +1,121 @@ +/- + 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.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel + +import Cedar.Thm.Validation.Slice.Reachable.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem reachable_attr_step {n : Nat} {euid euid' : EntityUID} {start : Set EntityUID} {entities : Entities} {ed : EntityData} {path : List Attr} + (hr : ReachableIn entities start euid n) + (he₁: entities.find? euid = some ed) + (he₂ : Value.EuidViaPath (.record ed.attrs) path euid' ) : + ReachableIn entities start euid' (n + 1) +:= by + cases hr + case in_start n' hi => + have he₄ : euid' ∈ ed.sliceEUIDs := by + suffices h : ∃ v ∈ ed.attrs.values, euid' ∈ v.sliceEUIDs by + simp [h, EntityData.sliceEUIDs, Set.mem_union_iff_mem_or, Set.mem_mapUnion_iff_mem_exists] + cases he₂ + rename_i v a path ha hv + exists v + constructor + · exact Map.find?_some_implies_in_values ha + · exact in_val_then_val_slice hv + have hr' : ReachableIn entities ed.sliceEUIDs euid' (n' + 1) := + ReachableIn.in_start he₄ + exact ReachableIn.step euid hi he₁ hr' + case step n' ed' euid'' he₁' hi hr' => + have ih := reachable_attr_step hr' he₁ he₂ + exact ReachableIn.step euid'' hi he₁' ih + +theorem checked_eval_entity_reachable_get_attr {e : Expr} {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {entities : Entities} {path : List Attr} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf (e.getAttr a) c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax path) + (he : evaluate (e.getAttr a) request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (hf : entities.contains euid) + (ih : CheckedEvalEntityReachable e) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + simp only [evaluate] at he + cases he₁ : evaluate e request entities <;> simp only [he₁, Except.bind_err, reduceCtorEq] at he + have ⟨ hc', tx', c₁', ht', htx, h₂ ⟩ := type_of_getAttr_inversion ht + rw [htx] at hl + have ⟨ hgc, v, he', hi ⟩ := type_of_is_sound hc hr ht' + cases hl + case getAttr v₁' ety n hety hl => + have ⟨euid', hv⟩ : ∃ euid', v = Value.prim (Prim.entityUID euid') := by + rw [hety] at hi + have ⟨ euid', hety, hv⟩ := instance_of_entity_type_is_entity hi + simp [hv] + subst hv + + have hv : v₁' = Value.prim (Prim.entityUID euid') := by + unfold EvaluatesTo at he' + rw [he₁] at he' + cases he' <;> rename_i he' <;> simp only [reduceCtorEq, Except.ok.injEq, false_or] at he' + exact he' + subst hv + + simp only [getAttr, attrsOf, Except.bind_ok] at he + cases he₂ : entities.attrs euid' <;> simp only [he₂, Except.bind_err, reduceCtorEq] at he + rename_i attrs + simp only [Map.findOrErr, Except.bind_ok] at he + split at he <;> simp only [reduceCtorEq, Except.bind_ok, Except.ok.injEq] at he + subst he + rename_i v hv + + have ⟨ ed, hed, hed' ⟩ := entities_attrs_then_find? he₂ + subst attrs + have hf' : entities.contains euid' := by simp [Map.contains, Option.isSome, hed] + have ih := ih hc hr ht' hl he₁ (.euid euid') hf' + have ha' : Value.EuidViaPath (Value.record ed.attrs) (a :: path) euid := .record hv ha + apply reachable_attr_step ih hed ha' + + case getAttrRecord hty hl => + cases h₂ <;> rename_i h₂ + · replace ⟨ ety, h₂ ⟩ := h₂ + specialize hty ety h₂ + contradiction + · replace ⟨ rty, h₂ ⟩ := h₂ + rw [h₂] at hi + have ⟨ attrs, hv⟩ := instance_of_record_type_is_record hi ; clear hi + subst hv + unfold EvaluatesTo at he' + rw [he₁] at he' + cases he' <;> rename_i he' <;> simp only [reduceCtorEq, Except.ok.injEq, false_or] at he' + subst he' + simp only [getAttr, attrsOf, Map.findOrErr, Except.bind_ok] at he + split at he <;> simp only [reduceCtorEq, Except.ok.injEq] at he + rename_i v hv + subst he + have ha' : Value.EuidViaPath (Value.record attrs) (a :: path) euid := .record hv ha + exact ih hc hr ht' hl he₁ ha' hf diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/IfThenElse.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/IfThenElse.lean new file mode 100644 index 000000000..f9812537e --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/IfThenElse.lean @@ -0,0 +1,85 @@ +/- + 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.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel + +import Cedar.Thm.Validation.Slice.Reachable.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem checked_eval_entity_reachable_ite {e₁ e₂ e₃: Expr} {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {entities : Entities} {path : List Attr} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf (.ite e₁ e₂ e₃) c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax path) + (he : evaluate (.ite e₁ e₂ e₃) request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (hf : entities.contains euid) + (ih₂ : CheckedEvalEntityReachable e₂) + (ih₃ : CheckedEvalEntityReachable e₃) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + have ⟨tx₁, bty₁, c₁, tx₂, c₂, tx₃, c₃, htx, htx₁, hty₁, hif ⟩ := type_of_ite_inversion ht + have ⟨ hgc, v, he₁, hi₁⟩ := type_of_is_sound hc hr htx₁ + + rw [htx] at hl + cases hl + rename_i hl₁ hl₂ hl₃ + + simp only [evaluate] at he + cases he₁' : Result.as Bool (evaluate e₁ request entities) <;> simp only [he₁', Except.bind_err, Except.bind_ok, reduceCtorEq] at he + rename_i b + replace he₁' : evaluate e₁ request entities = .ok (.prim (.bool b)) := by + simp only [Result.as, Coe.coe, Value.asBool] at he₁' + split at he₁' <;> try contradiction + split at he₁' <;> try contradiction + injections he₁' + subst he₁' + assumption + replace he₁ : .prim (.bool b) = v := by + simpa [EvaluatesTo, he₁'] using he₁ + subst he₁ + split at he + case isTrue hb => + subst hb + have htx₂ : typeOf e₂ (c ∪ c₁) env = .ok (tx₂, c₂) := by + split at hif <;> first + | simp only [hif] + | rw [hty₁] at hi₁ + contradiction + replace hgc : CapabilitiesInvariant c₁ request entities := by + simpa [he₁', GuardedCapabilitiesInvariant] using hgc + exact ih₂ (capability_union_invariant hc hgc) hr htx₂ hl₂ he ha hf + case isFalse hb => + replace hb : b = false := by + cases b <;> simp only [Bool.true_eq_false] <;> contradiction + subst hb + have htx₃ : typeOf e₃ c env = .ok (tx₃, c₃) := by + split at hif <;> first + | simp only [hif] + | rw [hty₁] at hi₁ + contradiction + exact ih₃ hc hr htx₃ hl₃ he ha hf diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Record.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Record.lean new file mode 100644 index 000000000..7a905fe9d --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Record.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.Authorization.Evaluator +import Cedar.Thm.Validation.Typechecker +import Cedar.Thm.Validation.Slice.Reachable.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem typed_record_contains_typed_attrs {rxs : List (Attr × Expr)} {a : Attr} {x : Expr} {c c' : Capabilities} {env : Environment} + (ht : typeOf (Expr.record rxs) c env = Except.ok (tx, c')) + (hx : (Map.make rxs).find? a = some x) : + ∃ rtxs ty atx, + tx = .record rtxs ty ∧ + (Map.make rtxs).find? a = some atx ∧ + ∃ c', typeOf x c env = .ok (atx, c') +:= by + have ⟨_, _, htx, hfat⟩ := type_of_record_inversion ht + have ⟨_, _, hatx, ht''⟩ := find_make_xs_find_make_txs hfat hx + simp [htx, hatx, ht''] + +theorem record_entity_access_implies_attr_entity_access {atx : TypedExpr} {rtxs : List (Attr × TypedExpr)} {ty : CedarType} {n nmax : Nat} {a : Attr} {path : List Attr} + (hl : (TypedExpr.record rtxs ty).EntityAccessAtLevel env n nmax (a :: path)) + (hatx : (Map.make rtxs).find? a = some atx) : + atx.EntityAccessAtLevel env n nmax path +:= by + cases hl + rename_i atx' _ hfatx' hl + have hatx : atx' = atx := by + simpa [hfatx'] using hatx + simpa [hatx] using hl + +theorem checked_eval_entity_reachable_record {rxs : List (Attr × Expr)} {n : Nat} {c c' : Capabilities} {tx : TypedExpr} {env : Environment} {entities : Entities} {path : List Attr} + (hc : CapabilitiesInvariant c request entities) + (hr : RequestAndEntitiesMatchEnvironment env request entities) + (ht : typeOf (.record rxs) c env = .ok (tx, c')) + (hl : tx.EntityAccessAtLevel env n nmax path) + (he : evaluate (.record rxs) request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (hf : entities.contains euid) + (ih : ∀ a x, (Map.make rxs).find? a = some x → CheckedEvalEntityReachable x) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + have ⟨ rvs, hv ⟩ := record_produces_record_value he + subst hv + cases ha + rename_i v a path' hfv hv + have ⟨ x, hfx, hex ⟩ := record_value_contains_evaluated_attrs he hfv + have ⟨ rtxs, _, atx, htx, hfatx, _, het⟩ := typed_record_contains_typed_attrs ht hfx + rw [htx] at hl + have hl' := record_entity_access_implies_attr_entity_access hl hfatx + exact ih a x hfx hc hr het hl' hex hv hf diff --git a/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Var.lean b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Var.lean new file mode 100644 index 000000000..72fdc4396 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Validation/Slice/Reachable/Var.lean @@ -0,0 +1,52 @@ +/- + 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.Data.MapUnion +import Cedar.Thm.Validation.Levels.CheckLevel + +import Cedar.Thm.Validation.Slice.Reachable.Basic + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +theorem var_entity_reachable {var : Var} {v : Value} {n : Nat} {request : Request} {entities : Entities} {euid : EntityUID} {path : List Attr} + (he : evaluate (.var var) request entities = .ok v) + (ha : Value.EuidViaPath v path euid) + (hf : entities.contains euid) : + ReachableIn entities request.sliceEUIDs euid (n + 1) +:= by + have hi : euid ∈ request.sliceEUIDs := by + rw [Request.sliceEUIDs, Set.mem_union_iff_mem_or, ←Set.make_mem] + cases var <;> simp only [evaluate, Except.ok.injEq] at he <;> subst he <;> cases ha + case principal | action | resource => simp [hf] + case context v a path hf' hv => + suffices h : ∃ kv ∈ request.context.kvs, euid ∈ kv.snd.sliceEUIDs by + unfold Value.sliceEUIDs List.attach₃ + right + simpa [List.mapUnion_pmap_subtype (·.snd.sliceEUIDs) request.context.kvs, Set.mem_mapUnion_iff_mem_exists] using h + exists (a, v) + constructor + · exact Map.find?_mem_toList hf' + · exact in_val_then_val_slice hv + exact ReachableIn.in_start hi