This file contains useful definitions and lemmas about the Typechecker functions.
@[irreducible]
theorem
Cedar.Thm.type_of_is_sound
{e : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
:
CapabilitiesInvariant c₁ request entities →
InstanceOfWellFormedEnvironment request entities env →
Validation.typeOf e c₁ env = Except.ok (ty, c₂) →
GuardedCapabilitiesInvariant e c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo e request entities v ∧ InstanceOfType env v ty.typeOf
If an expression is well-typed according to the typechecker, and the input
environment and capabilities satisfy some invariants, then either (1) evaluation
produces a value of the returned type or (2) it returns an error of type
entityDoesNotExist, extensionError, or arithBoundsError. Both options are
encoded in the EvaluatesTo predicate.
theorem
Cedar.Thm.type_of_preserves_evaluation_results
{e : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
:
CapabilitiesInvariant c₁ request entities →
InstanceOfWellFormedEnvironment request entities env →
Validation.typeOf e c₁ env = Except.ok (ty, c₂) →
Spec.evaluate e request entities = Spec.evaluate ty.toExpr request entities
The type checker, if succeeds, should produce a typed expression that evaluates to the same result as the input expression.