This file defines the top-level soundness property for the type checker.

def Cedar.Thm.typecheck (policy : Spec.Policy) (env : Validation.TypeEnv) : Except Validation.TypeError Validation.CedarType

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.typecheck_is_sound (policy : Spec.Policy) (env : Validation.TypeEnv) (t : Validation.CedarType) (request : Spec.Request) (entities : Spec.Entities) : InstanceOfWellFormedEnvironment request entities env → typecheck policy env = Except.ok t → ∃ (b : Bool), EvaluatesTo policy.toExpr request entities (Spec.Value.prim (Spec.Prim.bool b))

If typechecking succeeds, then for any request consistent with the schema, either (1) evaluation produces a boolean or (2) it returns an error of type entityDoesNotExist, extensionError, or arithBoundsError. Both options are encoded in the EvaluatesTo predicate. The type checker cannot protect against these errors because it has no knowledge of the entities/context that will be provided at authorization time, and it does not reason about the semantics of arithmetic operators.