This file proves that typechecking of .lit and .var expressions is sound.
theorem
Cedar.Thm.type_of_lit_is_sound
{l : Spec.Prim}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₃ : Validation.typeOf (Spec.Expr.lit l) c₁ env = Except.ok (ty, c₂))
:
GuardedCapabilitiesInvariant (Spec.Expr.lit l) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.lit l) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_var_is_sound
{var : Spec.Var}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{e' : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (Spec.Expr.var var) c₁ env = Except.ok (e', c₂))
:
GuardedCapabilitiesInvariant (Spec.Expr.var var) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.var var) request entities v ∧ InstanceOfType env v e'.typeOf