Basic properties of well-formed symbolic environments

This file proves basic lemmas about well-formedness predicate on environments.

theorem Cedar.Thm.validEntityUID_implies_validEntityType {εs : SymCC.SymEntities} {uid : Spec.EntityUID} : εs.isValidEntityUID uid = true → εs.isValidEntityType uid.ty = true

theorem Cedar.Thm.wf_εnv_for_policies_cons {εnv : SymCC.SymEnv} {p : Spec.Policy} {ps : Spec.Policies} : εnv.WellFormedForPolicies (p :: ps) → εnv.WellFormedFor p.toExpr ∧ εnv.WellFormedForPolicies ps

theorem Cedar.Thm.wf_εnv_for_policies_implies_wf_for_filter (f : Spec.Policy → Bool) {εnv : SymCC.SymEnv} {ps : Spec.Policies} : εnv.WellFormedForPolicies ps → εnv.WellFormedForPolicies (List.filter f ps)

theorem Cedar.Thm.wf_εnv_all_policies_implies_wf_all {εnv : SymCC.SymEnv} {ps : Spec.Policies} : εnv.WellFormedForPolicies ps → ∀ (p : Spec.Policy), p ∈ ps → εnv.WellFormedFor p.toExpr

theorem Cedar.Thm.wf_env_all_policies_implies_wf_all {env : Spec.Env} {ps : Spec.Policies} : env.WellFormedForPolicies ps → ∀ (p : Spec.Policy), p ∈ ps → env.WellFormedFor p.toExpr

theorem Cedar.Thm.wf_εnv_valid_refs_implies_wf_εnv_for_set {xs : List Spec.Expr} {εnv : SymCC.SymEnv} (hwε : εnv.WellFormed) (hvr : ∀ (x : Spec.Expr), x ∈ xs → εnv.entities.ValidRefsFor x) : εnv.WellFormedFor (Spec.Expr.set xs)

theorem Cedar.Thm.wf_εnv_for_policies_iff_wf_εnv_for_set {ps : Spec.Policies} {εnv : SymCC.SymEnv} : εnv.WellFormedForPolicies ps ↔ εnv.WellFormedFor (Spec.Expr.set (List.map Spec.Policy.toExpr ps))

theorem Cedar.Thm.wf_env_valid_refs_implies_wf_env_for_set {xs : List Spec.Expr} {env : Spec.Env} (hwε : env.WellFormed) (hvr : ∀ (x : Spec.Expr), x ∈ xs → env.entities.ValidRefsFor x) : env.WellFormedFor (Spec.Expr.set xs)

theorem Cedar.Thm.wf_env_for_policies_iff_wf_env_for_set {ps : Spec.Policies} {env : Spec.Env} : env.WellFormedForPolicies ps ↔ env.WellFormedFor (Spec.Expr.set (List.map Spec.Policy.toExpr ps))

theorem Cedar.Thm.wf_εnv_implies_wf_ρeq {εnv : SymCC.SymEnv} : εnv.WellFormed → SymCC.SymRequest.WellFormed εnv.entities εnv.request

theorem Cedar.Thm.wf_εs_implies_wf_attrs {ety : Spec.EntityType} {fₐ : SymCC.UnaryFunction} {εs : SymCC.SymEntities} (hwε : εs.WellFormed) (hf : εs.attrs ety = some fₐ) : SymCC.UnaryFunction.WellFormed εs fₐ ∧ fₐ.argType = SymCC.TermType.entity ety ∧ fₐ.outType.isCedarRecordType = true

theorem Cedar.Thm.wf_εs_implies_wf_ancs {ety₁ ety₂ : Spec.EntityType} {fₐ : SymCC.UnaryFunction} {εs : SymCC.SymEntities} (hwε : εs.WellFormed) (hf : εs.ancestorsOfType ety₁ ety₂ = some fₐ) : SymCC.UnaryFunction.WellFormed εs fₐ ∧ fₐ.argType = SymCC.TermType.entity ety₁ ∧ fₐ.outType = (SymCC.TermType.entity ety₂).set

theorem Cedar.Thm.wf_εs_implies_wf_tags {ety : Spec.EntityType} {τs : SymCC.SymTags} {εs : SymCC.SymEntities} (hwε : εs.WellFormed) (hτs : εs.tags ety = some (some τs)) : SymCC.SymTags.WellFormed εs ety τs

theorem Cedar.Thm.wf_udf_implies_lit {f : SymCC.UDF} {εs : SymCC.SymEntities} : SymCC.UDF.WellFormed εs f → f.isLiteral = true

theorem Cedar.Thm.wf_εnv_for_ite_implies {x₁ x₂ x₃ : Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (x₁.ite x₂ x₃) → εnv.WellFormedFor x₁ ∧ εnv.WellFormedFor x₂ ∧ εnv.WellFormedFor x₃

theorem Cedar.Thm.wf_env_for_ite_implies {x₁ x₂ x₃ : Spec.Expr} {env : Spec.Env} (h₁ : env.WellFormedFor (x₁.ite x₂ x₃)) : env.WellFormedFor x₁ ∧ env.WellFormedFor x₂ ∧ env.WellFormedFor x₃

theorem Cedar.Thm.wf_εnv_for_and_implies {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (x₁.and x₂) → εnv.WellFormedFor x₁ ∧ εnv.WellFormedFor x₂

theorem Cedar.Thm.wf_env_for_and_implies {x₁ x₂ : Spec.Expr} {env : Spec.Env} : env.WellFormedFor (x₁.and x₂) → env.WellFormedFor x₁ ∧ env.WellFormedFor x₂

theorem Cedar.Thm.wf_εnv_for_or_implies {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (x₁.or x₂) → εnv.WellFormedFor x₁ ∧ εnv.WellFormedFor x₂

theorem Cedar.Thm.wf_env_for_or_implies {x₁ x₂ : Spec.Expr} {env : Spec.Env} : env.WellFormedFor (x₁.or x₂) → env.WellFormedFor x₁ ∧ env.WellFormedFor x₂

theorem Cedar.Thm.wf_εnv_for_binaryApp_implies {op : Spec.BinaryOp} {x₁ x₂ : Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (Spec.Expr.binaryApp op x₁ x₂) → εnv.WellFormedFor x₁ ∧ εnv.WellFormedFor x₂

theorem Cedar.Thm.wf_env_for_binaryApp_implies {op : Spec.BinaryOp} {x₁ x₂ : Spec.Expr} {env : Spec.Env} : env.WellFormedFor (Spec.Expr.binaryApp op x₁ x₂) → env.WellFormedFor x₁ ∧ env.WellFormedFor x₂

theorem Cedar.Thm.wf_εnv_for_hasAttr_implies {x₁ : Spec.Expr} {a : Spec.Attr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (x₁.hasAttr a) → εnv.WellFormedFor x₁

theorem Cedar.Thm.wf_env_for_hasAttr_implies {x₁ : Spec.Expr} {a : Spec.Attr} {env : Spec.Env} : env.WellFormedFor (x₁.hasAttr a) → env.WellFormedFor x₁

theorem Cedar.Thm.wf_εnv_for_getAttr_implies {x₁ : Spec.Expr} {a : Spec.Attr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (x₁.getAttr a) → εnv.WellFormedFor x₁

theorem Cedar.Thm.wf_env_for_getAttr_implies {x₁ : Spec.Expr} {a : Spec.Attr} {env : Spec.Env} : env.WellFormedFor (x₁.getAttr a) → env.WellFormedFor x₁

theorem Cedar.Thm.wf_εnv_for_unaryApp_implies {op : Spec.UnaryOp} {x₁ : Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (Spec.Expr.unaryApp op x₁) → εnv.WellFormedFor x₁

theorem Cedar.Thm.wf_env_for_unaryApp_implies {op : Spec.UnaryOp} {x₁ : Spec.Expr} {env : Spec.Env} : env.WellFormedFor (Spec.Expr.unaryApp op x₁) → env.WellFormedFor x₁

theorem Cedar.Thm.wf_εnv_for_set_implies {xs : List Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (Spec.Expr.set xs) → ∀ (x : Spec.Expr), x ∈ xs → εnv.WellFormedFor x

theorem Cedar.Thm.wf_env_for_set_implies {xs : List Spec.Expr} {env : Spec.Env} : env.WellFormedFor (Spec.Expr.set xs) → ∀ (x : Spec.Expr), x ∈ xs → env.WellFormedFor x

theorem Cedar.Thm.wf_εnv_for_record_implies {axs : List (Spec.Attr × Spec.Expr)} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (Spec.Expr.record axs) → ∀ (ax : Spec.Attr × Spec.Expr), ax ∈ axs → εnv.WellFormedFor ax.snd

theorem Cedar.Thm.wf_env_for_record_implies {axs : List (Spec.Attr × Spec.Expr)} {env : Spec.Env} : env.WellFormedFor (Spec.Expr.record axs) → ∀ (ax : Spec.Attr × Spec.Expr), ax ∈ axs → env.WellFormedFor ax.snd

theorem Cedar.Thm.wf_εnv_for_call_implies {f : Spec.ExtFun} {xs : List Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedFor (Spec.Expr.call f xs) → ∀ (x : Spec.Expr), x ∈ xs → εnv.WellFormedFor x

theorem Cedar.Thm.wf_env_for_call_implies {f : Spec.ExtFun} {xs : List Spec.Expr} {env : Spec.Env} : env.WellFormedFor (Spec.Expr.call f xs) → ∀ (x : Spec.Expr), x ∈ xs → env.WellFormedFor x

def Cedar.Thm.SameDomain (εs₁ εs₂ : SymCC.SymEntities) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.same_domain_symmetric {εs₁ εs₂ : SymCC.SymEntities} : SameDomain εs₁ εs₂ → SameDomain εs₂ εs₁

theorem Cedar.Thm.wf_term_type_same_domain {εs₁ εs₂ : SymCC.SymEntities} {ty : SymCC.TermType} : SameDomain εs₁ εs₂ → SymCC.TermType.WellFormed εs₁ ty → SymCC.TermType.WellFormed εs₂ ty

theorem Cedar.Thm.wf_term_var_same_domain {εs₁ εs₂ : SymCC.SymEntities} {v : SymCC.TermVar} : SameDomain εs₁ εs₂ → SymCC.TermVar.WellFormed εs₁ v → SymCC.TermVar.WellFormed εs₂ v

theorem Cedar.Thm.wf_term_prim_same_domain {εs₁ εs₂ : SymCC.SymEntities} {p : SymCC.TermPrim} : SameDomain εs₁ εs₂ → SymCC.TermPrim.WellFormed εs₁ p → SymCC.TermPrim.WellFormed εs₂ p

theorem Cedar.Thm.wf_uuf_same_domain {εs₁ εs₂ : SymCC.SymEntities} {f : SymCC.UUF} : SameDomain εs₁ εs₂ → SymCC.UUF.WellFormed εs₁ f → SymCC.UUF.WellFormed εs₂ f

theorem Cedar.Thm.wt_op_same_domain {εs₁ εs₂ : SymCC.SymEntities} {op : SymCC.Op} {ts : List SymCC.Term} {ty : SymCC.TermType} : SameDomain εs₁ εs₂ → SymCC.Op.WellTyped εs₁ op ts ty → SymCC.Op.WellTyped εs₂ op ts ty

theorem Cedar.Thm.wf_term_same_domain {εs₁ εs₂ : SymCC.SymEntities} {t : SymCC.Term} : SameDomain εs₁ εs₂ → SymCC.Term.WellFormed εs₁ t → SymCC.Term.WellFormed εs₂ t

theorem Cedar.Thm.wfl_term_same_domain {εs₁ εs₂ : SymCC.SymEntities} {t : SymCC.Term} : SameDomain εs₁ εs₂ → SymCC.Term.WellFormedLiteral εs₁ t → SymCC.Term.WellFormedLiteral εs₂ t

theorem Cedar.Thm.wf_udf_same_domain {εs₁ εs₂ : SymCC.SymEntities} {f : SymCC.UDF} : SameDomain εs₁ εs₂ → SymCC.UDF.WellFormed εs₁ f → SymCC.UDF.WellFormed εs₂ f

theorem Cedar.Thm.wfp_term_app_same_domain {εs₁ εs₂ : SymCC.SymEntities} {t : SymCC.Term} : SameDomain εs₁ εs₂ → SymCC.Term.WellFormedPartialApp εs₁ t → SymCC.Term.WellFormedPartialApp εs₂ t

theorem Cedar.Thm.wf_interpretation_same_domain {εs₁ εs₂ : SymCC.SymEntities} {I : SymCC.Interpretation} : SameDomain εs₁ εs₂ → I.WellFormed εs₁ → I.WellFormed εs₂

theorem Cedar.Thm.wf_ρeq_same_domain {εs₁ εs₂ : SymCC.SymEntities} {ρeq : SymCC.SymRequest} : SameDomain εs₁ εs₂ → SymCC.SymRequest.WellFormed εs₁ ρeq → SymCC.SymRequest.WellFormed εs₂ ρeq

theorem Cedar.Thm.wf_uf_same_domain {εs₁ εs₂ : SymCC.SymEntities} {f : SymCC.UnaryFunction} : SameDomain εs₁ εs₂ → SymCC.UnaryFunction.WellFormed εs₁ f → SymCC.UnaryFunction.WellFormed εs₂ f

theorem Cedar.Thm.wf_εdata_same_domain {εs₁ εs₂ : SymCC.SymEntities} {ety : Spec.EntityType} {εd : SymCC.SymEntityData} : SameDomain εs₁ εs₂ → SymCC.SymEntityData.WellFormed εs₁ ety εd → SymCC.SymEntityData.WellFormed εs₂ ety εd

theorem Cedar.Thm.prim_valid_refs_same_domain {εs₁ εs₂ : SymCC.SymEntities} {p : Spec.Prim} : SameDomain εs₁ εs₂ → Spec.Prim.ValidRef (fun (x : Spec.EntityUID) => εs₁.isValidEntityUID x = true) p → Spec.Prim.ValidRef (fun (x : Spec.EntityUID) => εs₂.isValidEntityUID x = true) p

theorem Cedar.Thm.expr_valid_refs_same_domain {εs₁ εs₂ : SymCC.SymEntities} {x : Spec.Expr} : SameDomain εs₁ εs₂ → Spec.Expr.ValidRefs (fun (x : Spec.EntityUID) => εs₁.isValidEntityUID x = true) x → Spec.Expr.ValidRefs (fun (x : Spec.EntityUID) => εs₂.isValidEntityUID x = true) x

theorem Cedar.Thm.wf_εnv_implies_attrs_wf {εnv : SymCC.SymEnv} {ety : Spec.EntityType} {attrs : SymCC.UnaryFunction} (hwf : εnv.WellFormed) (hattrs_exists : εnv.entities.attrs ety = some attrs) : SymCC.UnaryFunction.WellFormed εnv.entities attrs ∧ attrs.argType = SymCC.TermType.entity ety ∧ attrs.outType.isCedarRecordType = true

SymEnv being well-formed implies that any attribute function is well-formed