Properties of interpretations on symbolic environments

This file proves basic lemmas about the interpret function on symbolic environments.

theorem Cedar.Thm.interpret_entities_find?_some {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ety : Spec.EntityType} {d : SymCC.SymEntityData} (h₁ : Data.Map.find? εs ety = some d) : Data.Map.find? (SymCC.SymEntities.interpret I εs) ety = some (SymCC.SymEntityData.interpret I d)

theorem Cedar.Thm.interpret_entities_find?_none {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ety : Spec.EntityType} (h₁ : Data.Map.find? εs ety = none) : Data.Map.find? (SymCC.SymEntities.interpret I εs) ety = none

theorem Cedar.Thm.interpret_entities_isValidEntityUID (εs : SymCC.SymEntities) (I : SymCC.Interpretation) (uid : Spec.EntityUID) : εs.isValidEntityUID uid = (SymCC.SymEntities.interpret I εs).isValidEntityUID uid

theorem Cedar.Thm.interpret_entities_isValidEntityType (εs : SymCC.SymEntities) (I : SymCC.Interpretation) (ety : Spec.EntityType) : εs.isValidEntityType ety = (SymCC.SymEntities.interpret I εs).isValidEntityType ety

theorem Cedar.Thm.interpret_entities_ancestors_none {εs : SymCC.SymEntities} {ety : Spec.EntityType} (I : SymCC.Interpretation) : εs.ancestors ety = none → (SymCC.SymEntities.interpret I εs).ancestors ety = none

theorem Cedar.Thm.interpret_entities_ancestors_some {εs : SymCC.SymEntities} {ety : Spec.EntityType} {ancs : Data.Map Spec.EntityType SymCC.UnaryFunction} (I : SymCC.Interpretation) : εs.ancestors ety = some ancs → (SymCC.SymEntities.interpret I εs).ancestors ety = some (Data.Map.mapOnValues (SymCC.UnaryFunction.interpret I) ancs)

theorem Cedar.Thm.interpret_entities_ancestorsOfType_none {εs : SymCC.SymEntities} {ety ancTy : Spec.EntityType} {I : SymCC.Interpretation} : εs.ancestorsOfType ety ancTy = none → (SymCC.SymEntities.interpret I εs).ancestorsOfType ety ancTy = none

theorem Cedar.Thm.interpret_entities_ancestorsOfType_some {εs : SymCC.SymEntities} {ety ancTy : Spec.EntityType} {I : SymCC.Interpretation} {f : SymCC.UnaryFunction} : εs.ancestorsOfType ety ancTy = some f → (SymCC.SymEntities.interpret I εs).ancestorsOfType ety ancTy = some (SymCC.UnaryFunction.interpret I f)

theorem Cedar.Thm.interpret_entities_tags_none {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ety : Spec.EntityType} : εs.tags ety = some none → (SymCC.SymEntities.interpret I εs).tags ety = some none

theorem Cedar.Thm.interpret_entities_tags_some {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ety : Spec.EntityType} {τs : SymCC.SymTags} : (εs.tags ety = do let a ← some τs pure (some a)) → (SymCC.SymEntities.interpret I εs).tags ety = do let a ← some (SymCC.SymTags.interpret I τs) pure (some a)

theorem Cedar.Thm.interpret_entities_same_domain (εs : SymCC.SymEntities) (I : SymCC.Interpretation) : SameDomain εs (SymCC.SymEntities.interpret I εs)

theorem Cedar.Thm.interpret_uf_wf {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {f : SymCC.UnaryFunction} : I.WellFormed εs → SymCC.UnaryFunction.WellFormed εs f → SymCC.UnaryFunction.WellFormed εs (SymCC.UnaryFunction.interpret I f) ∧ (SymCC.UnaryFunction.interpret I f).argType = f.argType ∧ (SymCC.UnaryFunction.interpret I f).outType = f.outType

theorem Cedar.Thm.interpret_εdata_wf {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {ety : Spec.EntityType} {εd : SymCC.SymEntityData} : I.WellFormed εs → SymCC.SymEntityData.WellFormed εs ety εd → SymCC.SymEntityData.WellFormed εs ety (SymCC.SymEntityData.interpret I εd)

theorem Cedar.Thm.interpret_εntities_wf {εs : SymCC.SymEntities} {I : SymCC.Interpretation} : εs.WellFormed → I.WellFormed εs → (SymCC.SymEntities.interpret I εs).WellFormed

theorem Cedar.Thm.interpret_ρeq_wf {εs : SymCC.SymEntities} {ρeq : SymCC.SymRequest} {I : SymCC.Interpretation} : I.WellFormed εs → SymCC.SymRequest.WellFormed εs ρeq → SymCC.SymRequest.WellFormed εs (SymCC.SymRequest.interpret I ρeq)

theorem Cedar.Thm.interpret_εnv_wf {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} : εnv.WellFormed → I.WellFormed εnv.entities → (SymCC.SymEnv.interpret I εnv).WellFormed

theorem Cedar.Thm.interpret_εnv_wf_for_expr {x : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} : εnv.WellFormedFor x → I.WellFormed εnv.entities → (SymCC.SymEnv.interpret I εnv).WellFormedFor x

theorem Cedar.Thm.interpret_εnv_wf_for_policies {ps : Spec.Policies} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} : εnv.WellFormedForPolicies ps → I.WellFormed εnv.entities → (SymCC.SymEnv.interpret I εnv).WellFormedForPolicies ps

theorem Cedar.Thm.interpret_uf_lit {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {f : SymCC.UnaryFunction} : I.WellFormed εs → SymCC.UnaryFunction.WellFormed εs f → (SymCC.UnaryFunction.interpret I f).isLiteral = true

theorem Cedar.Thm.interpret_εnv_lit {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} : εnv.WellFormed → I.WellFormed εnv.entities → (SymCC.SymEnv.interpret I εnv).isLiteral = true