This file proves that typechecking of .unaryApp expressions is sound.
theorem
Cedar.Thm.type_of_unary_inversion
{op : Spec.UnaryOp}
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.unaryApp op x₁) c₁ env = Except.ok (tx, c₂))
:
c₂ = ∅ ∧ ∃ (tx₁ : Validation.TypedExpr), ∃ (ty : Validation.CedarType), ∃ (c₁' : Validation.Capabilities), tx = Validation.TypedExpr.unaryApp op tx₁ ty ∧ Validation.typeOf x₁ c₁ env = Except.ok (tx₁, c₁') ∧ match op, h₁ with
| Spec.UnaryOp.not, h₁ =>
∃ (bty : Validation.BoolType), ty = Validation.CedarType.bool bty.not ∧ tx₁.typeOf = Validation.CedarType.bool bty
| Spec.UnaryOp.neg, h₁ => tx₁.typeOf = Validation.CedarType.int ∧ ty = Validation.CedarType.int
| Spec.UnaryOp.isEmpty, h₁ =>
ty = Validation.CedarType.bool Validation.BoolType.anyBool ∧ ∃ (ty₀ : Validation.CedarType), tx₁.typeOf = ty₀.set
| Spec.UnaryOp.like p, h₁ =>
ty = Validation.CedarType.bool Validation.BoolType.anyBool ∧ tx₁.typeOf = Validation.CedarType.string
| Spec.UnaryOp.is ety₀, h₁ =>
∃ (ety₁ : Spec.EntityType), ty = Validation.CedarType.bool (if ety₀ = ety₁ then Validation.BoolType.tt else Validation.BoolType.ff) ∧ tx₁.typeOf = Validation.CedarType.entity ety₁
theorem
Cedar.Thm.type_of_not_inversion
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.unaryApp Spec.UnaryOp.not x₁) c₁ env = Except.ok (ty, c₂))
:
theorem
Cedar.Thm.type_of_not_is_sound
{x₁ : Spec.Expr}
{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 (Spec.Expr.unaryApp Spec.UnaryOp.not x₁) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (Spec.Expr.unaryApp Spec.UnaryOp.not x₁) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.unaryApp Spec.UnaryOp.not x₁) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_neg_inversion
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.unaryApp Spec.UnaryOp.neg x₁) c₁ env = Except.ok (ty, c₂))
:
theorem
Cedar.Thm.type_of_neg_is_sound
{x₁ : Spec.Expr}
{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 (Spec.Expr.unaryApp Spec.UnaryOp.neg x₁) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (Spec.Expr.unaryApp Spec.UnaryOp.neg x₁) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.unaryApp Spec.UnaryOp.neg x₁) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_isEmpty_inversion
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.unaryApp Spec.UnaryOp.isEmpty x₁) c₁ env = Except.ok (ty, c₂))
:
theorem
Cedar.Thm.type_of_isEmpty_is_sound
{x₁ : Spec.Expr}
{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 (Spec.Expr.unaryApp Spec.UnaryOp.isEmpty x₁) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (Spec.Expr.unaryApp Spec.UnaryOp.isEmpty x₁) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.unaryApp Spec.UnaryOp.isEmpty x₁) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_like_inversion
{x₁ : Spec.Expr}
{p : Spec.Pattern}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.unaryApp (Spec.UnaryOp.like p) x₁) c₁ env = Except.ok (ty, c₂))
:
c₂ = ∅ ∧ ty.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool ∧ ∃ (c₁' : Validation.Capabilities), (Validation.typeOf x₁ c₁ env).typeOf = Except.ok (Validation.CedarType.string, c₁')
theorem
Cedar.Thm.type_of_like_is_sound
{x₁ : Spec.Expr}
{p : Spec.Pattern}
{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 (Spec.Expr.unaryApp (Spec.UnaryOp.like p) x₁) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (Spec.Expr.unaryApp (Spec.UnaryOp.like p) x₁) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.unaryApp (Spec.UnaryOp.like p) x₁) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_is_inversion
{x₁ : Spec.Expr}
{ety : Spec.EntityType}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.unaryApp (Spec.UnaryOp.is ety) x₁) c₁ env = Except.ok (ty, c₂))
:
c₂ = ∅ ∧ ∃ (ety' : Spec.EntityType), ∃ (c₁' : Validation.Capabilities), ty.typeOf = Validation.CedarType.bool (if ety = ety' then Validation.BoolType.tt else Validation.BoolType.ff) ∧ (Validation.typeOf x₁ c₁ env).typeOf = Except.ok (Validation.CedarType.entity ety', c₁')
theorem
Cedar.Thm.type_of_is_is_sound
{x₁ : Spec.Expr}
{ety : Spec.EntityType}
{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 (Spec.Expr.unaryApp (Spec.UnaryOp.is ety) x₁) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (Spec.Expr.unaryApp (Spec.UnaryOp.is ety) x₁) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.unaryApp (Spec.UnaryOp.is ety) x₁) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_unaryApp_is_sound
{op₁ : Spec.UnaryOp}
{x₁ : Spec.Expr}
{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 (Spec.Expr.unaryApp op₁ x₁) c₁ env = Except.ok (ty, c₂))
(ih : TypeOfIsSound x₁)
:
GuardedCapabilitiesInvariant (Spec.Expr.unaryApp op₁ x₁) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.unaryApp op₁ x₁) request entities v ∧ InstanceOfType env v ty.typeOf