This file contains some facts about SymEnv.ofEnv.
theorem
Cedar.Thm.ofEnv_preserves_entity
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
{ety : Spec.EntityType}
{entry : Validation.EntitySchemaEntry}
(hεnv : εnv = SymCC.SymEnv.ofEnv Γ)
(hfind : Data.Map.find? Γ.ets ety = some entry)
:
If some entity exists in Γ, then it must
also exists in SymEnv.ofEnv Γ with the corresponding SymEntityData
theorem
Cedar.Thm.ofEnv_preserves_action_entity
{Γ : Validation.TypeEnv}
{uid : Spec.EntityUID}
(hwf : Γ.WellFormed)
(hmem : Data.Map.contains Γ.acts uid = true)
:
Data.Map.find? (SymCC.SymEnv.ofEnv Γ).entities uid.ty = some
(SymCC.SymEntityData.ofActionType uid.ty
(List.map
(fun (x : Spec.EntityUID × Validation.ActionSchemaEntry) =>
match x with
| (act, snd) => act.ty)
(Data.Map.toList Γ.acts)).eraseDups
Γ.acts)
An action entity type is compiled correctly
theorem
Cedar.Thm.ofActionType_contains_act
{Γ : Validation.TypeEnv}
{uid : Spec.EntityUID}
(hwf : Γ.WellFormed)
(hmem : Data.Map.contains Γ.acts uid = true)
:
theorem
Cedar.Thm.ofEnv_entity_exists
{Γ : Validation.TypeEnv}
{ety : Spec.EntityType}
(hmem : Data.Map.contains Γ.ets ety = true)
:
A variant of ofEnv_preserves_entity
theorem
Cedar.Thm.ofEnv_action_entity_exists
{Γ : Validation.TypeEnv}
{uid : Spec.EntityUID}
(hwf : Γ.WellFormed)
(hmem : Data.Map.contains Γ.acts uid = true)
:
Similar to ofEnv_entity_exists but for action entities
theorem
Cedar.Thm.ofSchema_find?_ets
{Γ : Validation.TypeEnv}
{ety : Spec.EntityType}
{entry : Validation.EntitySchemaEntry}
(hfind_ety : Data.Map.find? Γ.ets ety = some entry)
:
Data.Map.find? (SymCC.SymEntities.ofSchema Γ.ets Γ.acts) ety = some (SymCC.SymEntityData.ofEntityType ety entry)
theorem
Cedar.Thm.ofSchema_find?_acts
{Γ : Validation.TypeEnv}
{uid : Spec.EntityUID}
{entry : Validation.ActionSchemaEntry}
(hwf_Γ : Γ.WellFormed)
(hfind_uid : Data.Map.find? Γ.acts uid = some entry)
:
Data.Map.find? (SymCC.SymEntities.ofSchema Γ.ets Γ.acts) uid.ty = some
(SymCC.SymEntityData.ofActionType uid.ty
(List.map
(fun (x : Spec.EntityUID × Validation.ActionSchemaEntry) =>
match x with
| (act, snd) => act.ty)
(Data.Map.toList Γ.acts)).eraseDups
Γ.acts)
theorem
Cedar.Thm.ofEnv_wf_entity
{Γ : Validation.TypeEnv}
{ety : Spec.EntityType}
(hwf : Γ.WellFormed)
(hwf_ety : Validation.EntityType.WellFormed Γ ety)
:
theorem
Cedar.Thm.ofEnv_preserves_tags
{Γ : Validation.TypeEnv}
{ety : Spec.EntityType}
{ty : Validation.CedarType}
(h : Γ.ets.tags? ety = some (some ty))
:
Lemma that if a concrete Γ : TypeEnv has tags for
a particular entity type, then SymEnv.ofEnv Γ must also
have tags for it
theorem
Cedar.Thm.ofEnv_preserves_entity_attr
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
{rty : Validation.RecordType}
{ety : Spec.EntityType}
(hεnv : εnv = SymCC.SymEnv.ofEnv Γ)
(hattrs_exists : Γ.ets.attrs? ety = some rty)
(hwf : εnv.WellFormed)
:
∃ (attrs : SymCC.UnaryFunction), εnv.entities.attrs ety = some attrs ∧ SymCC.UnaryFunction.WellFormed εnv.entities attrs ∧ attrs.argType = SymCC.TermType.entity ety ∧ attrs.outType = SymCC.TermType.record (Data.Map.mk (SymCC.TermType.ofRecordType (Data.Map.toList rty)))
Show that SymEnv.ofEnv Γ preserves the result of attribute lookup
theorem
Cedar.Thm.ofRecordType_eq_map
{rty : List (Spec.Attr × Validation.QualifiedType)}
:
SymCC.TermType.ofRecordType rty = List.map (fun (x : Spec.Attr × Validation.QualifiedType) => (x.fst, SymCC.TermType.ofQualifiedType x.snd)) rty
@[irreducible]
theorem
Cedar.Thm.ofType_wf
{Γ : Validation.TypeEnv}
{ty : Validation.CedarType}
(hwf : Γ.WellFormed)
(hwf_ty : Validation.CedarType.WellFormed Γ ty)
:
TermType.ofType of well-formed CedarType is well-formed
(under the compiled SymEnv).
@[irreducible]
theorem
Cedar.Thm.wf_ofType_right_inverse_cedarType?
{Γ : Validation.TypeEnv}
{ty : Validation.CedarType}
(hwf : Γ.WellFormed)
(hwf_ty : Validation.CedarType.WellFormed Γ ty)
:
TermType.ofType is a right inverse of CedarType.cedarType?
when applied to a well-formed CedarType.
@[irreducible]
theorem
Cedar.Thm.wf_ofType_right_inverse_cedarType?.ofRecordType_forall₂
{Γ : Validation.TypeEnv}
(hwf : Γ.WellFormed)
(rty : List (Spec.Attr × Validation.QualifiedType))
:
Validation.CedarType.WellFormed Γ (Validation.CedarType.record (Data.Map.mk rty)) →
List.Forall₂
(fun (x : Spec.Attr × SymCC.TermType) (y : Spec.Attr × Validation.QualifiedType) =>
((SymCC.TermType.cedarType?.qualifiedType? x.snd).bind fun (t : Validation.QualifiedType) => some (x.fst, t)) = some y)
(SymCC.TermType.ofRecordType rty)
(List.map
(fun (x : Spec.Attr × Validation.QualifiedType) =>
match x with
| (k, v) => (k, v.liftBoolTypes))
rty)
theorem
Cedar.Thm.ofStandardEntityType_is_wf
{ety : Spec.EntityType}
{Γ : Validation.TypeEnv}
{entry : Validation.StandardSchemaEntry}
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? Γ.ets ety = some (Validation.EntitySchemaEntry.standard entry))
:
theorem
Cedar.Thm.ofEnumEntityType_is_wf
{ety : Spec.EntityType}
{Γ : Validation.TypeEnv}
{eids : Data.Set String}
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? Γ.ets ety = some (Validation.EntitySchemaEntry.enum eids))
:
theorem
Cedar.Thm.ofEntityType_is_wf
{ety : Spec.EntityType}
{Γ : Validation.TypeEnv}
{entry : Validation.EntitySchemaEntry}
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? Γ.ets ety = some entry)
:
SymCC.SymEntityData.WellFormed (SymCC.SymEnv.ofEnv Γ).entities ety (SymCC.SymEntityData.ofEntityType ety entry)
theorem
Cedar.Thm.ofActionType_ancsUDF_is_wf
{uid : Spec.EntityUID}
{Γ : Validation.TypeEnv}
{anc : Spec.EntityType}
{anc_f : SymCC.UnaryFunction}
(hwf : Γ.WellFormed)
(hanc :
(SymCC.SymEntityData.ofActionType uid.ty
(List.map (fun (x : Spec.EntityUID × Validation.ActionSchemaEntry) => x.fst.ty)
(Data.Map.toList Γ.acts)).eraseDups
Γ.acts).ancestors.find?
anc = some anc_f)
:
SymCC.UnaryFunction.WellFormed (SymCC.SymEnv.ofEnv Γ).entities
(SymCC.SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts anc) ∧ (SymCC.SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts anc).argType = SymCC.TermType.entity uid.ty ∧ (SymCC.SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts anc).outType = (SymCC.TermType.entity anc).set
A technical lemma that SymEntityData.ofActionType.ancsUDF
produces a well-formed UDF.
theorem
Cedar.Thm.ofActionType_is_wf
{uid : Spec.EntityUID}
{Γ : Validation.TypeEnv}
{entry : Validation.ActionSchemaEntry}
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? Γ.acts uid = some entry)
:
SymCC.SymEntityData.WellFormed (SymCC.SymEnv.ofEnv Γ).entities uid.ty
(SymCC.SymEntityData.ofActionType uid.ty
(List.map (fun (x : Spec.EntityUID × Validation.ActionSchemaEntry) => x.fst.ty) (Data.Map.toList Γ.acts)).eraseDups
Γ.acts)
theorem
Cedar.Thm.entity_uid_wf_implies_sym_entities_is_valid_entity_uid
{Γ : Validation.TypeEnv}
{uid : Spec.EntityUID}
(hwf : Γ.WellFormed)
(huid : Validation.EntityUID.WellFormed Γ uid)
:
theorem
Cedar.Thm.env_valid_uid_implies_sym_env_valid_uid
{Γ : Validation.TypeEnv}
{env : Spec.Env}
{uid : Spec.EntityUID}
(hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ)
(hcont_uid : Data.Map.contains env.entities uid = true)
:
@[irreducible]
theorem
Cedar.Thm.ofEnv_entities_valid_refs_for_wt_expr
{Γ : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(hwf : Γ.WellFormed)
(hwt : TypedExpr.WellTyped Γ tx)
:
Spec.Expr.ValidRefs (fun (x : Spec.EntityUID) => (SymCC.SymEnv.ofEnv Γ).entities.isValidEntityUID x = true) tx.toExpr
Given a well-formed environment and a well-typed expression in that environment,
we show that the expression satisfies ValidRefs
@[irreducible]
theorem
Cedar.Thm.ValidRefs_invariant_under_liftBoolTypes
{tx : Validation.TypedExpr}
{f : Spec.EntityUID → Prop}
(hrefs : Spec.Expr.ValidRefs f tx.liftBoolTypes.toExpr)
:
Removing liftBoolTypes does not affect ValidRefs
theorem
Cedar.Thm.wellTypedPolicy_ok_implies_valid_refs
{Γ : Validation.TypeEnv}
{p p' : Spec.Policy}
(hwf : Γ.WellFormed)
(hok : SymCC.wellTypedPolicy p Γ = Except.ok p')
:
Spec.Expr.ValidRefs (fun (x : Spec.EntityUID) => (SymCC.SymEnv.ofEnv Γ).entities.isValidEntityUID x = true) p'.toExpr
theorem
Cedar.Thm.ofEnv_entities_find?_some
{Γ : Validation.TypeEnv}
{ety : Spec.EntityType}
{δ : SymCC.SymEntityData}
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? (SymCC.SymEnv.ofEnv Γ).entities ety = some δ)
:
((∃ (entry : Validation.StandardSchemaEntry), Data.Map.find? Γ.ets ety = some (Validation.EntitySchemaEntry.standard entry) ∧ δ = SymCC.SymEntityData.ofStandardEntityType ety entry) ∨ ∃ (entry : Data.Set String), Data.Map.find? Γ.ets ety = some (Validation.EntitySchemaEntry.enum entry) ∧ δ = SymCC.SymEntityData.ofEnumEntityType ety entry) ∨ ∃ (uid : Spec.EntityUID), ∃ (entry : Validation.ActionSchemaEntry), uid.ty = ety ∧ Data.Map.find? Γ.acts uid = some entry ∧ δ = SymCC.SymEntityData.ofActionType uid.ty
(List.map (fun (x : Spec.EntityUID × Validation.ActionSchemaEntry) => x.fst.ty)
(Data.Map.toList Γ.acts)).eraseDups
Γ.acts
theorem
Cedar.Thm.ancsUDF_app
{Γ : Validation.TypeEnv}
{uid : Spec.EntityUID}
{entry : Validation.ActionSchemaEntry}
(ancTy : Spec.EntityType)
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? Γ.acts uid = some entry)
:
SymCC.Factory.app (SymCC.SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts ancTy) (SymCC.Term.entity uid) = SymCC.SymEntityData.ofActionType.ancsTerm ancTy entry.ancestors.toList
Simplifies SymEntityData.ofActionType.ancsUDF
theorem
Cedar.Thm.in_ancsUDF_implies_in_ancestors
{Γ : Validation.TypeEnv}
{uid uid' : Spec.EntityUID}
{ancTy : Spec.EntityType}
(hwf : Γ.WellFormed)
(hmem :
uid' ∈ (SymCC.Factory.app (SymCC.SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts ancTy)
(SymCC.Term.entity uid)).entityUIDs)
:
theorem
Cedar.Thm.in_ancestors_implies_in_ancsUDF
{Γ : Validation.TypeEnv}
{uid uid' : Spec.EntityUID}
{entry : Validation.ActionSchemaEntry}
(hwf : Γ.WellFormed)
(hfind : Data.Map.find? Γ.acts uid = some entry)
(hmem : uid' ∈ entry.ancestors)
:
uid' ∈ (SymCC.Factory.app (SymCC.SymEntityData.ofActionType.ancsUDF uid.ty Γ.acts uid'.ty)
(SymCC.Term.entity uid)).entityUIDs
Main well-formedness theorem for SymEnv.ofEnv,
which says that if the input environment Γ is well-formed,
then SymEnv.ofEnv Γ is well-formed.
A stronger version of ofEnv_is_wf that
shows that SymEnv.ofEnv Γ is strongly well-formed.
theorem
Cedar.Thm.ofEnv_wf_for_expr
{Γ : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(hwf : Γ.WellFormed)
(hwt : TypedExpr.WellTyped Γ tx)
:
If an expression is well-typed in a concrete, well-formed TypeEnv,
then it must also be well-formed in the compiled symbolic environment.
theorem
Cedar.Thm.ofEnv_swf_for_expr
{Γ : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(hwf : Γ.WellFormed)
(hwt : TypedExpr.WellTyped Γ tx)
:
Similar to ofEnv_wf_for_expr but for StronglyWellFormedFor.
theorem
Cedar.Thm.ofEnv_swf_for_policy
{Γ : Validation.TypeEnv}
{p p' : Spec.Policy}
(hwf : Γ.WellFormed)
(hwt : SymCC.wellTypedPolicy p Γ = Except.ok p')
:
Similar to ofEnv_swf_for_expr but for StronglyWellFormedForPolicy.
theorem
Cedar.Thm.ofEnv_swf_for_policies
{Γ : Validation.TypeEnv}
{ps ps' : Spec.Policies}
(hwf : Γ.WellFormed)
(hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps')
:
Similar to ofEnv_swf_for_expr but for StronglyWellFormedForPolicies.