This file contains helper lemmas that are shared by concretization proofs.

theorem Cedar.Thm.concretize?_ρ_some_eq {ρ : SymCC.SymRequest} {r : Spec.Request} : ρ.concretize? = some r → ∃ (uidₚ : Spec.EntityUID), ∃ (uidₐ : Spec.EntityUID), ∃ (uidᵣ : Spec.EntityUID), ∃ (ctx : Data.Map Spec.Attr Spec.Value), ρ.principal.entityUID? = some uidₚ ∧ ρ.action.entityUID? = some uidₐ ∧ ρ.resource.entityUID? = some uidᵣ ∧ ρ.context.recordValue? = some ctx ∧ r = { principal := uidₚ, action := uidₐ, resource := uidᵣ, context := ctx }

theorem Cedar.Thm.concretize?_εs_some_eq {uids : Data.Set Spec.EntityUID} {εs : SymCC.SymEntities} {es : Spec.Entities} : SymCC.SymEntities.concretize? uids εs = some es → ∃ (eds : List (Spec.EntityUID × Spec.EntityData)), List.mapM (SymCC.SymEntities.concretize?.entityData? εs) (uids ∪ εs.entityUIDs).elts = some eds ∧ Data.Map.make eds = es

theorem Cedar.Thm.concretize?_entityData?_some_eq {uid : Spec.EntityUID} {ed : Spec.EntityUID × Spec.EntityData} {εs : SymCC.SymEntities} : SymCC.SymEntities.concretize?.entityData? εs uid = some ed → ∃ (δ : SymCC.SymEntityData), ∃ (d : Spec.EntityData), Data.Map.find? εs uid.ty = some δ ∧ SymCC.SymEntityData.concretize? uid δ = some d ∧ (uid, d) = ed

theorem Cedar.Thm.concretize?_δ_isValidEntityUID_implies_wfl {uid : Spec.EntityUID} {δ : SymCC.SymEntityData} {εs : SymCC.SymEntities} : Data.Map.find? εs uid.ty = some δ → SymCC.SymEntityData.concretize?.isValidEntityUID uid δ = true → SymCC.Term.WellFormedLiteral εs (SymCC.Term.entity uid)

theorem Cedar.Thm.wf_δ_implies_wf_app_attrs {uid : Spec.EntityUID} {δ : SymCC.SymEntityData} {εs : SymCC.SymEntities} : SymCC.SymEntityData.WellFormed εs uid.ty δ → SymCC.Term.WellFormed εs (SymCC.Term.entity uid) → SymCC.Term.WellFormed εs (SymCC.Factory.app δ.attrs (SymCC.Term.entity uid)) ∧ (SymCC.Factory.app δ.attrs (SymCC.Term.entity uid)).typeOf = δ.attrs.outType

theorem Cedar.Thm.wf_δ_implies_wf_app_ancs {uid : Spec.EntityUID} {δ : SymCC.SymEntityData} {εs : SymCC.SymEntities} {ancTy : Spec.EntityType} {ancUF : SymCC.UnaryFunction} : SymCC.SymEntityData.WellFormed εs uid.ty δ → SymCC.Term.WellFormed εs (SymCC.Term.entity uid) → δ.ancestors.find? ancTy = some ancUF → SymCC.Term.WellFormed εs (SymCC.Factory.app ancUF (SymCC.Term.entity uid)) ∧ (SymCC.Factory.app ancUF (SymCC.Term.entity uid)).typeOf = (SymCC.TermType.entity ancTy).set

theorem Cedar.Thm.wf_δ_implies_wf_app_tags_keys {εs : SymCC.SymEntities} {uid : Spec.EntityUID} {δ : SymCC.SymEntityData} {τs : SymCC.SymTags} : SymCC.SymEntityData.WellFormed εs uid.ty δ → SymCC.Term.WellFormed εs (SymCC.Term.entity uid) → δ.tags = some τs → SymCC.Term.WellFormed εs (SymCC.Factory.app τs.keys (SymCC.Term.entity uid)) ∧ (SymCC.Factory.app τs.keys (SymCC.Term.entity uid)).typeOf = SymCC.TermType.string.set

theorem Cedar.Thm.lit_tagOf (uid : Spec.EntityUID) (tag : Spec.Tag) : (SymCC.Factory.tagOf (SymCC.Term.entity uid) (SymCC.Term.string tag)).isLiteral = true

TODO: is there a better place for this lemma? It's very unrelated to the other lemmas in this file. If we move it we can also remove the Factory import from this file.