This file contains useful definitions and lemmas about the Typechecker functions.

def Cedar.Thm.EvaluatesTo (e : Spec.Expr) (request : Spec.Request) (entities : Spec.Entities) (v : Spec.Value) : Prop

The type soundness property says that if the typechecker assigns a type to an expression, then it must be the case that the expression EvaluatesTo a value of that type. The EvaluatesTo predicate covers the (obvious) case where evaluation has no errors, but it also allows for errors of type entityDoesNotExist, extensionError, and arithBoundsError.

The typechecker cannot protect against these errors because they depend on runtime information (i.e., the entities passed into the authorization request, extension function applications on authorization-time data, and arithmetic overflow errors). All other errors (attrDoesNotExist and typeError) can be prevented statically.

Note: Currently, extensionErrors can also be ruled out at validation time because the only extension functions that can error are constructors, and all constructors are required to be applied to string literals, meaning that they can be fully evaluated during validation. This is not guaranteed to be the case in the future.

Note: We plan to implement a range analysis that will be able to rule out arithBoundsErrors.

Equations

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

def Cedar.Thm.CapabilitiesInvariant (c : Validation.Capabilities) (request : Spec.Request) (entities : Spec.Entities) : Prop

On input to the typechecking function, for any (e, .attr k) in the Capabilities, e is a record- or entity-typed expression that has attribute k. Similarly, for any (e, .tag k) in the Capabilities, e is an entity-typed expression that has tag k.

Equations

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

def Cedar.Thm.GuardedCapabilitiesInvariant (e : Spec.Expr) (c : Validation.Capabilities) (request : Spec.Request) (entities : Spec.Entities) : Prop

The Capabilities output by the typechecking function will satisfy CapabilitiesInvariant provided that the input expression evaluates to true.

Equations

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

def Cedar.Thm.TypeOfIsSound (x₁ : Spec.Expr) : Prop

Equations

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

theorem Cedar.Thm.empty_capabilities_invariant (request : Spec.Request) (entities : Spec.Entities) : CapabilitiesInvariant ∅ request entities

theorem Cedar.Thm.empty_guarded_capabilities_invariant {e : Spec.Expr} {request : Spec.Request} {entities : Spec.Entities} : GuardedCapabilitiesInvariant e ∅ request entities

theorem Cedar.Thm.capability_implies_record_attribute {x₁ : Spec.Expr} {a : Spec.Attr} {c₁ : Validation.Capabilities} {request : Spec.Request} {entities : Spec.Entities} {r : Data.Map Spec.Attr Spec.Value} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : Spec.evaluate x₁ request entities = Except.ok (Spec.Value.record r)) (h₃ : (x₁, Validation.Key.attr a) ∈ c₁) : ∃ (vₐ : Spec.Value), r.find? a = some vₐ

theorem Cedar.Thm.capability_implies_entity_attribute {x₁ : Spec.Expr} {a : Spec.Attr} {c₁ : Validation.Capabilities} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} {d : Spec.EntityData} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : Spec.evaluate x₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.entityUID uid))) (h₃ : Data.Map.find? entities uid = some d) (h₄ : (x₁, Validation.Key.attr a) ∈ c₁) : ∃ (vₐ : Spec.Value), d.attrs.find? a = some vₐ

theorem Cedar.Thm.capability_union_invariant {c₁ c₂ : Validation.Capabilities} {request : Spec.Request} {entities : Spec.Entities} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : CapabilitiesInvariant c₂ request entities) : CapabilitiesInvariant (c₁ ∪ c₂) request entities

theorem Cedar.Thm.capability_intersection_invariant {c₁ c₂ : Validation.Capabilities} {request : Spec.Request} {entities : Spec.Entities} (h₁ : CapabilitiesInvariant c₁ request entities ∨ CapabilitiesInvariant c₂ request entities) : CapabilitiesInvariant (c₁ ∩ c₂) request entities

def Cedar.Thm.tacticSplit_type_of_ : Lean.ParserDescr

A utility which takes a hypothesis with the form (typeOf x c env).typeOf = Except.ok (ty, c') and splitting it into three new hypotheses typeOf x c env = Except.ok v✝, v✝.fst.typeOf = ty, and v✝.snd = c'.

Equations

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

theorem Cedar.Thm.type_of_is_inhabited {e : Spec.Expr} {c₁ c₂ : Validation.Capabilities} {env : Validation.TypeEnv} {tx : Validation.TypedExpr} (hwf : env.WellFormed) (hty : Validation.typeOf e c₁ env = Except.ok (tx, c₂)) : ∃ (v : Spec.Value), InstanceOfType env v tx.typeOf

A variant of type_is_inhabited assuming instead that the type is the result of typeOf.