This file proves that typechecking of .getAttr expressions is sound.
theorem
Cedar.Thm.getAttrInRecord_has_empty_capabilities
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₂ : Validation.Capabilities}
{rty : Validation.RecordType}
{ty ty₁ : Validation.CedarType}
:
theorem
Cedar.Thm.type_of_getAttr_inversion
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (x₁.getAttr a) c₁ env = Except.ok (tx, c₂))
:
c₂ = ∅ ∧ ∃ (tx₁ : Validation.TypedExpr), ∃ (c₁' : Validation.Capabilities), Validation.typeOf x₁ c₁ env = Except.ok (tx₁, c₁') ∧ tx = tx₁.getAttr a tx.typeOf ∧ ((∃ (ety : Spec.EntityType), tx₁.typeOf = Validation.CedarType.entity ety) ∨ ∃ (rty : Data.Map Spec.Attr (Validation.Qualified Validation.CedarType)), tx₁.typeOf = Validation.CedarType.record rty)
theorem
Cedar.Thm.type_of_getAttr_is_sound_for_records
{ty : Validation.TypedExpr}
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₁' : Validation.Capabilities}
{env : Validation.TypeEnv}
{rty : Validation.RecordType}
{request : Spec.Request}
{entities : Spec.Entities}
{v₁ : Spec.Value}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : Validation.typeOf (x₁.getAttr a) c₁ env = Except.ok (ty, ∅))
(h₃ : (Validation.typeOf x₁ c₁ env).typeOf = Except.ok (Validation.CedarType.record rty, c₁'))
(h₄ : Spec.evaluate x₁ request entities = Except.ok v₁)
(h₅ : InstanceOfType env v₁ (Validation.CedarType.record rty))
:
∃ (v : Spec.Value), (Spec.getAttr v₁ a entities = Except.error Spec.Error.entityDoesNotExist ∨ Spec.getAttr v₁ a entities = Except.error Spec.Error.extensionError ∨ Spec.getAttr v₁ a entities = Except.error Spec.Error.arithBoundsError ∨ Spec.getAttr v₁ a entities = Except.ok v) ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_getAttr_is_sound_for_entities
{ty : Validation.TypedExpr}
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₁' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ety : Spec.EntityType}
{request : Spec.Request}
{entities : Spec.Entities}
{v₁ : Spec.Value}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (x₁.getAttr a) c₁ env = Except.ok (ty, ∅))
(h₄ : (Validation.typeOf x₁ c₁ env).typeOf = Except.ok (Validation.CedarType.entity ety, c₁'))
(h₅ : Spec.evaluate x₁ request entities = Except.ok v₁)
(h₆ : InstanceOfType env v₁ (Validation.CedarType.entity ety))
:
∃ (v : Spec.Value), (Spec.getAttr v₁ a entities = Except.error Spec.Error.entityDoesNotExist ∨ Spec.getAttr v₁ a entities = Except.error Spec.Error.extensionError ∨ Spec.getAttr v₁ a entities = Except.error Spec.Error.arithBoundsError ∨ Spec.getAttr v₁ a entities = Except.ok v) ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_getAttr_is_sound
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (x₁.getAttr a) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (x₁.getAttr a) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (x₁.getAttr a) request entities v ∧ InstanceOfType env v ty.typeOf