This file contains useful definitions and lemmas about Cedar types.
Equations
Instances For
def
Cedar.Thm.InstanceOfEntityType
(e : Spec.EntityUID)
(ety : Spec.EntityType)
(env : Validation.TypeEnv)
:
Equations
- Cedar.Thm.InstanceOfEntityType e ety env = (ety = e.ty ∧ Cedar.Validation.EntityUID.WellFormed env e)
Instances For
Equations
- Cedar.Thm.InstanceOfExtType (Cedar.Spec.Ext.decimal d) Cedar.Validation.ExtType.decimal = True
- Cedar.Thm.InstanceOfExtType (Cedar.Spec.Ext.ipaddr ip) Cedar.Validation.ExtType.ipAddr = True
- Cedar.Thm.InstanceOfExtType (Cedar.Spec.Ext.datetime dt) Cedar.Validation.ExtType.datetime = True
- Cedar.Thm.InstanceOfExtType (Cedar.Spec.Ext.duration dur) Cedar.Validation.ExtType.duration = True
- Cedar.Thm.InstanceOfExtType x✝¹ x✝ = False
Instances For
- instance_of_bool {env : Validation.TypeEnv} (b : Bool) (bty : Validation.BoolType) (h₁ : InstanceOfBoolType b bty) : InstanceOfType env (Spec.Value.prim (Spec.Prim.bool b)) (Validation.CedarType.bool bty)
- instance_of_int {env : Validation.TypeEnv} {x✝ : Int64} : InstanceOfType env (Spec.Value.prim (Spec.Prim.int x✝)) Validation.CedarType.int
- instance_of_string {env : Validation.TypeEnv} {x✝ : String} : InstanceOfType env (Spec.Value.prim (Spec.Prim.string x✝)) Validation.CedarType.string
- instance_of_entity {env : Validation.TypeEnv} (e : Spec.EntityUID) (ety : Spec.EntityType) (h₁ : InstanceOfEntityType e ety env) : InstanceOfType env (Spec.Value.prim (Spec.Prim.entityUID e)) (Validation.CedarType.entity ety)
- instance_of_set {env : Validation.TypeEnv} (s : Data.Set Spec.Value) (ty : Validation.CedarType) (h₁ : ∀ (v : Spec.Value), v ∈ s → InstanceOfType env v ty) : InstanceOfType env (Spec.Value.set s) ty.set
- instance_of_record {env : Validation.TypeEnv} (r : Data.Map Spec.Attr Spec.Value) (rty : Validation.RecordType) (h₁ : ∀ (k : Spec.Attr), r.contains k = true → Data.Map.contains rty k = true) (h₂ : ∀ (k : Spec.Attr) (v : Spec.Value) (qty : Validation.QualifiedType), r.find? k = some v → Data.Map.find? rty k = some qty → InstanceOfType env v (Validation.Qualified.getType qty)) (h₃ : ∀ (k : Spec.Attr) (qty : Validation.QualifiedType), Data.Map.find? rty k = some qty → Validation.Qualified.isRequired qty = true → r.contains k = true) : InstanceOfType env (Spec.Value.record r) (Validation.CedarType.record rty)
- instance_of_ext {env : Validation.TypeEnv} (x : Spec.Ext) (xty : Validation.ExtType) (h₁ : InstanceOfExtType x xty) : InstanceOfType env (Spec.Value.ext x) (Validation.CedarType.ext xty)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Cedar.Thm.InstanceOfEntityTags
(data : Spec.EntityData)
(entry : Validation.EntitySchemaEntry)
(env : Validation.TypeEnv)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Cedar.Thm.IsValidEntityEID (Cedar.Validation.EntitySchemaEntry.standard ty) eid = True
- Cedar.Thm.IsValidEntityEID (Cedar.Validation.EntitySchemaEntry.enum eids) eid = (eid ∈ eids)
Instances For
def
Cedar.Thm.InstanceOfEntitySchemaEntry
(uid : Spec.EntityUID)
(data : Spec.EntityData)
(env : Validation.TypeEnv)
:
For every entity (uid, data) in the store,
- The entity's type is defined in the type store.
- The entity's attributes match the attribute types indicated in the type store.
- The entity's ancestors' types are consistent with the ancestor information in the type store.
- The entity's tags' types are consistent with the tags information in the type store.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Cedar.Thm.InstanceOfActionSchemaEntry
(uid : Spec.EntityUID)
(data : Spec.EntityData)
(env : Validation.TypeEnv)
:
Similar to WellFormedEntityData, but a special case for action entities
since they are stored disjoint from ets
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Cedar.Thm.InstanceOfSchemaEntry
(uid : Spec.EntityUID)
(data : Spec.EntityData)
(env : Validation.TypeEnv)
:
Equations
- Cedar.Thm.InstanceOfSchemaEntry uid data env = (Cedar.Thm.InstanceOfEntitySchemaEntry uid data env ∨ Cedar.Thm.InstanceOfActionSchemaEntry uid data env)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Each entry in the store is valid
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Cedar.Thm.InstanceOfWellFormedEnvironment
(request : Spec.Request)
(entities : Spec.Entities)
(env : Validation.TypeEnv)
:
Equations
- Cedar.Thm.InstanceOfWellFormedEnvironment request entities env = (env.WellFormed ∧ Cedar.Thm.InstanceOfRequestType request env ∧ Cedar.Thm.InstanceOfSchema entities env)
Instances For
theorem
Cedar.Thm.instance_of_bool_is_bool
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
{bty : Validation.BoolType}
:
InstanceOfType env v₁ (Validation.CedarType.bool bty) → ∃ (b : Bool), v₁ = Spec.Value.prim (Spec.Prim.bool b)
theorem
Cedar.Thm.instance_of_anyBool_is_bool
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
InstanceOfType env v₁ (Validation.CedarType.bool Validation.BoolType.anyBool) →
∃ (b : Bool), v₁ = Spec.Value.prim (Spec.Prim.bool b)
theorem
Cedar.Thm.instance_of_int_is_int
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
InstanceOfType env v₁ Validation.CedarType.int → ∃ (i : Int64), v₁ = Spec.Value.prim (Spec.Prim.int i)
theorem
Cedar.Thm.instance_of_string_is_string
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
InstanceOfType env v₁ Validation.CedarType.string → ∃ (s : String), v₁ = Spec.Value.prim (Spec.Prim.string s)
theorem
Cedar.Thm.instance_of_entity_type_is_entity
{v₁ : Spec.Value}
{env : Validation.TypeEnv}
{ety : Spec.EntityType}
:
InstanceOfType env v₁ (Validation.CedarType.entity ety) →
∃ (euid : Spec.EntityUID), euid.ty = ety ∧ v₁ = Spec.Value.prim (Spec.Prim.entityUID euid)
theorem
Cedar.Thm.instance_of_decimal_type_is_decimal
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
theorem
Cedar.Thm.instance_of_ipAddr_type_is_ipAddr
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
InstanceOfType env v₁ (Validation.CedarType.ext Validation.ExtType.ipAddr) →
∃ (d : Spec.IPAddr), v₁ = Spec.Value.ext (Spec.Ext.ipaddr d)
theorem
Cedar.Thm.instance_of_datetime_type_is_datetime
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
theorem
Cedar.Thm.instance_of_duration_type_is_duration
{env : Validation.TypeEnv}
{v₁ : Spec.Value}
:
theorem
Cedar.Thm.instance_of_set_type_is_set
{env : Validation.TypeEnv}
{v : Spec.Value}
{ty : Validation.CedarType}
:
InstanceOfType env v ty.set →
∃ (s : Data.Set Spec.Value), v = Spec.Value.set s ∧ ∀ (ev : Spec.Value), ev ∈ s → InstanceOfType env ev ty
theorem
Cedar.Thm.instance_of_record_type_is_record
{env : Validation.TypeEnv}
{v : Spec.Value}
{rty : Validation.RecordType}
:
InstanceOfType env v (Validation.CedarType.record rty) → ∃ (r : Data.Map Spec.Attr Spec.Value), v = Spec.Value.record r
theorem
Cedar.Thm.instance_of_attribute_type
{env : Validation.TypeEnv}
{r : Data.Map Spec.Attr Spec.Value}
{v : Spec.Value}
{rty : Validation.RecordType}
{a : Spec.Attr}
{aty : Validation.CedarType}
{qaty : Validation.QualifiedType}
(h₁ : InstanceOfType env (Spec.Value.record r) (Validation.CedarType.record rty))
(h₂ : Data.Map.find? rty a = some qaty)
(h₃ : Validation.Qualified.getType qaty = aty)
(h₄ : r.find? a = some v)
:
InstanceOfType env v aty
theorem
Cedar.Thm.absent_attribute_is_absent
{env : Validation.TypeEnv}
{r : Data.Map Spec.Attr Spec.Value}
{rty : Validation.RecordType}
{a : Spec.Attr}
(h₁ : InstanceOfType env (Spec.Value.record r) (Validation.CedarType.record rty))
(h₂ : Data.Map.find? rty a = none)
:
theorem
Cedar.Thm.required_attribute_is_present
{env : Validation.TypeEnv}
{r : Data.Map Spec.Attr Spec.Value}
{rty : Validation.RecordType}
{a : Spec.Attr}
{aty : Validation.CedarType}
(h₁ : InstanceOfType env (Spec.Value.record r) (Validation.CedarType.record rty))
(h₂ : Data.Map.find? rty a = some (Validation.Qualified.required aty))
:
theorem
Cedar.Thm.well_typed_entity_attributes
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{uid : Spec.EntityUID}
{d : Spec.EntityData}
{rty : Validation.RecordType}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : Data.Map.find? entities uid = some d)
(h₃ : env.ets.attrs? uid.ty = some rty)
:
InstanceOfType env (Spec.Value.record d.attrs) (Validation.CedarType.record rty)
theorem
Cedar.Thm.instance_of_type_bool_is_bool
{env : Validation.TypeEnv}
(v : Spec.Value)
(ty : Validation.CedarType)
:
InstanceOfType env v ty →
(ty ⊑ Validation.CedarType.bool Validation.BoolType.anyBool) = true →
∃ (b : Bool), v = Spec.Value.prim (Spec.Prim.bool b)
theorem
Cedar.Thm.entity_type_is_inhabited
{env : Validation.TypeEnv}
{ety : Spec.EntityType}
(hwf_env : env.WellFormed)
(hwf : Validation.EntityType.WellFormed env ety)
:
theorem
Cedar.Thm.instance_of_record_cons
{env : Validation.TypeEnv}
{hd : Spec.Attr × Validation.Qualified Validation.CedarType}
{tl : List (Spec.Attr × Validation.Qualified Validation.CedarType)}
{rhd : Spec.Value}
{rtl : List (Spec.Attr × Spec.Value)}
(h₁ : InstanceOfType env rhd hd.snd.getType)
(h₂ : InstanceOfType env (Spec.Value.record (Data.Map.mk rtl)) (Validation.CedarType.record (Data.Map.mk tl)))
:
InstanceOfType env (Spec.Value.record (Data.Map.mk ((hd.fst, rhd) :: rtl)))
(Validation.CedarType.record (Data.Map.mk (hd :: tl)))
theorem
Cedar.Thm.type_is_inhabited_entity
{env : Validation.TypeEnv}
{ety : Spec.EntityType}
:
env.WellFormed →
Validation.CedarType.WellFormed env (Validation.CedarType.entity ety) →
∃ (v : Spec.Value), InstanceOfType env v (Validation.CedarType.entity ety)
theorem
Cedar.Thm.type_is_inhabited_record
{env : Validation.TypeEnv}
{rty : List (Spec.Attr × Validation.Qualified Validation.CedarType)}
(hwf : Validation.CedarType.WellFormed env (Validation.CedarType.record (Data.Map.mk rty)))
(ih_ty :
∀ (aty : Spec.Attr × Validation.Qualified Validation.CedarType),
aty ∈ rty →
Validation.CedarType.WellFormed env aty.snd.getType → ∃ (v : Spec.Value), InstanceOfType env v aty.snd.getType)
:
@[irreducible]
theorem
Cedar.Thm.type_is_inhabited
{env : Validation.TypeEnv}
{ty : Validation.CedarType}
(hwf_env : env.WellFormed)
(hwf : Validation.CedarType.WellFormed env ty)
:
theorem
Cedar.Thm.instance_of_lubBool_left
{env : Validation.TypeEnv}
{v : Spec.Value}
{bty₁ bty₂ : Validation.BoolType}
:
InstanceOfType env v (Validation.CedarType.bool bty₁) →
InstanceOfType env v (Validation.CedarType.bool (Validation.lubBool bty₁ bty₂))
theorem
Cedar.Thm.instance_of_lubBool
{env : Validation.TypeEnv}
{v : Spec.Value}
{bty₁ bty₂ : Validation.BoolType}
:
InstanceOfType env v (Validation.CedarType.bool bty₁) ∨ InstanceOfType env v (Validation.CedarType.bool bty₂) →
InstanceOfType env v (Validation.CedarType.bool (Validation.lubBool bty₁ bty₂))
theorem
Cedar.Thm.sizeOf_attr_type_lt_sizeOf_record_type
{ty : Validation.CedarType}
{a : Spec.Attr}
{qty : Validation.QualifiedType}
{rty : List (Spec.Attr × Validation.Qualified Validation.CedarType)}
(h₁ : Validation.CedarType.record (Data.Map.mk rty) = ty)
(h₂ : (Data.Map.mk rty).find? a = some qty)
:
@[irreducible]
theorem
Cedar.Thm.instance_of_lub_left
{env : Validation.TypeEnv}
{v : Spec.Value}
{ty ty₁ ty₂ : Validation.CedarType}
(h₁ : (ty₁ ⊔ ty₂) = some ty)
(h₂ : InstanceOfType env v ty₁)
:
InstanceOfType env v ty
theorem
Cedar.Thm.instance_of_lub
{env : Validation.TypeEnv}
{v : Spec.Value}
{ty ty₁ ty₂ : Validation.CedarType}
(h₁ : (ty₁ ⊔ ty₂) = some ty)
(h₂ : InstanceOfType env v ty₁ ∨ InstanceOfType env v ty₂)
:
InstanceOfType env v ty
theorem
Cedar.Thm.type_of_lit_inversion
{p : Spec.Prim}
{c₁ c₂ : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
(h₁ : Validation.typeOf (Spec.Expr.lit p) c₁ env = Except.ok (tx, c₂))
:
TODO: move this back to Cedar/Thm/Validation/Typechecker/LitVar.lean after we fix the proof.
theorem
Cedar.Thm.InstanceOfWellFormedEnvironment.wf_env
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h : InstanceOfWellFormedEnvironment request entities env)
:
env.WellFormed
Obtains the fact of well-formed environment from InstanceOfWellFormedEnvironment.
theorem
Cedar.Thm.InstanceOfWellFormedEnvironment.instance_of_schema_entry
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{uid : Spec.EntityUID}
{data : Spec.EntityData}
(h : InstanceOfWellFormedEnvironment request entities env)
(hentry : Data.Map.find? entities uid = some data)
:
InstanceOfSchemaEntry uid data env
theorem
Cedar.Thm.InstanceOfWellFormedEnvironment.instance_of_schema
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h : InstanceOfWellFormedEnvironment request entities env)
:
InstanceOfSchema entities env
theorem
Cedar.Thm.InstanceOfWellFormedEnvironment.wf_action_data
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{uid : Spec.EntityUID}
{entry : Validation.ActionSchemaEntry}
(h : InstanceOfWellFormedEnvironment request entities env)
(hacts : Data.Map.find? env.acts uid = some entry)
: