This file proves that typechecking of .hasAttr expressions is sound.
theorem
Cedar.Thm.hasAttrInRecord_has_empty_or_singleton_capabilities
{b : Bool}
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₂ : Validation.Capabilities}
{rty : Validation.RecordType}
{ty₁ : Validation.CedarType}
:
Validation.hasAttrInRecord rty x₁ a c₁ b = Except.ok (ty₁, c₂) →
c₂ = ∅ ∨ c₂ = Validation.Capabilities.singleton x₁ (Validation.Key.attr a)
theorem
Cedar.Thm.type_of_hasAttr_inversion
{x₁ : Spec.Expr}
{a : Spec.Attr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (x₁.hasAttr a) c₁ env = Except.ok (tx, c₂))
:
(c₂ = ∅ ∨ c₂ = Validation.Capabilities.singleton x₁ (Validation.Key.attr a)) ∧ ∃ (tx₁ : Validation.TypedExpr), ∃ (c₁' : Validation.Capabilities), Validation.typeOf x₁ c₁ env = Except.ok (tx₁, c₁') ∧ tx = tx₁.hasAttr 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_hasAttr_is_sound_for_records
{ty : Validation.TypedExpr}
{c₂ : Validation.Capabilities}
{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₁.hasAttr a) c₁ env = Except.ok (ty, c₂))
(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.hasAttr v₁ a entities = Except.error Spec.Error.entityDoesNotExist ∨ Spec.hasAttr v₁ a entities = Except.error Spec.Error.extensionError ∨ Spec.hasAttr v₁ a entities = Except.error Spec.Error.arithBoundsError ∨ Spec.hasAttr v₁ a entities = Except.ok v) ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_hasAttr_is_sound_for_entities
{ty : Validation.TypedExpr}
{c₂ : Validation.Capabilities}
{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₁.hasAttr a) c₁ env = Except.ok (ty, c₂))
(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.hasAttr v₁ a entities = Except.error Spec.Error.entityDoesNotExist ∨ Spec.hasAttr v₁ a entities = Except.error Spec.Error.extensionError ∨ Spec.hasAttr v₁ a entities = Except.error Spec.Error.arithBoundsError ∨ Spec.hasAttr v₁ a entities = Except.ok v) ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_hasAttr_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₁.hasAttr a) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (x₁.hasAttr a) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (x₁.hasAttr a) request entities v ∧ InstanceOfType env v ty.typeOf