This file proves that typechecking of .binaryApp .mem expressions is sound.
theorem
Cedar.Thm.type_of_mem_inversion
{x₁ x₂ : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.binaryApp Spec.BinaryOp.mem x₁ x₂) c env = Except.ok (ty, c'))
:
c' = ∅ ∧ ∃ (ety₁ : Spec.EntityType), ∃ (ety₂ : Spec.EntityType), (∃ (c₁ : Validation.Capabilities), (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.entity ety₁, c₁)) ∧ ∃ (c₂ : Validation.Capabilities), (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.entity ety₂, c₂) ∧ ty.typeOf = Validation.CedarType.bool (Validation.typeOfInₑ ety₁ ety₂ x₁ x₂ env) ∨ (Validation.typeOf x₂ c env).typeOf = Except.ok ((Validation.CedarType.entity ety₂).set, c₂) ∧ ty.typeOf = Validation.CedarType.bool (Validation.typeOfInₛ ety₁ ety₂ x₁ x₂ env)
theorem
Cedar.Thm.entityUID?_some_implies_entity_lit
{x : Spec.Expr}
{euid : Spec.EntityUID}
(h₁ : Validation.entityUID? x = some euid)
:
theorem
Cedar.Thm.actionUID?_some_implies_action_lit
{x : Spec.Expr}
{euid : Spec.EntityUID}
{acts : Validation.ActionSchema}
(h₁ : Validation.actionUID? x acts = some euid)
:
theorem
Cedar.Thm.entityUIDs?_some_implies_entity_lits
{x : Spec.Expr}
{euids : List Spec.EntityUID}
(h₁ : Validation.entityUIDs? x = some euids)
:
theorem
Cedar.Thm.acts_maybeDescendentOf_false_implies_not_ancestor_type
{euid : Spec.EntityUID}
{ety : Spec.EntityType}
{data : Spec.EntityData}
{entry : Validation.ActionSchemaEntry}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(hdesc : env.acts.maybeDescendentOf euid.ty ety = false)
(hent_found : Data.Map.find? entities euid = some data)
(hacts_entry : Data.Map.find? env.acts euid = some entry)
(euid' : Spec.EntityUID)
:
theorem
Cedar.Thm.entity_type_in_false_implies_inₑ_false
{euid₁ euid₂ : Spec.EntityUID}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : env.descendentOf euid₁.ty euid₂.ty = false)
:
theorem
Cedar.Thm.action_type_in_eq_action_inₑ
(euid₁ euid₂ : Spec.EntityUID)
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : env.acts.contains euid₁ = true)
:
theorem
Cedar.Thm.type_of_mem_is_soundₑ
{x₁ x₂ : Spec.Expr}
{c₁ c₁' c₂' : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ety₁ ety₂ : Spec.EntityType}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : (Validation.typeOf x₁ c₁ env).typeOf = Except.ok (Validation.CedarType.entity ety₁, c₁'))
(h₄ : (Validation.typeOf x₂ c₁ env).typeOf = Except.ok (Validation.CedarType.entity ety₂, c₂'))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
:
∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.binaryApp Spec.BinaryOp.mem x₁ x₂) request entities v ∧ InstanceOfType env v (Validation.CedarType.bool (Validation.typeOfInₑ ety₁ ety₂ x₁ x₂ env))
theorem
Cedar.Thm.entity_set_type_implies_set_of_entities
{env : Validation.TypeEnv}
{vs : List Spec.Value}
{ety : Spec.EntityType}
(h₁ : InstanceOfType env (Spec.Value.set (Data.Set.mk vs)) (Validation.CedarType.entity ety).set)
:
theorem
Cedar.Thm.entity_type_in_false_implies_inₛ_false
{euid : Spec.EntityUID}
{euids : List Spec.EntityUID}
{ety : Spec.EntityType}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : env.descendentOf euid.ty ety = false)
(h₃ : ∀ (euid : Spec.EntityUID), euid ∈ euids → euid.ty = ety)
:
theorem
Cedar.Thm.mapM'_eval_lits_eq_prims
{ps : List Spec.Prim}
{vs : List Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : List.mapM' (fun (x : Spec.Expr) => Spec.evaluate x request entities) (List.map Spec.Expr.lit ps) = Except.ok vs)
:
theorem
Cedar.Thm.mapM'_asEntityUID_eq_entities
{vs : List Spec.Value}
{euids : List Spec.EntityUID}
(h₁ : List.mapM' Spec.Value.asEntityUID vs = Except.ok euids)
:
theorem
Cedar.Thm.evaluate_entity_set_eqv
{vs : List Spec.Value}
{euids euids' : List Spec.EntityUID}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ :
Spec.evaluate (Spec.Expr.set (List.map (Spec.Expr.lit ∘ Spec.Prim.entityUID) euids')) request entities = Except.ok (Spec.Value.set (Data.Set.mk vs)))
(h₂ : List.mapM Spec.Value.asEntityUID vs = Except.ok euids)
:
theorem
Cedar.Thm.action_type_in_eq_action_inₛ
{auid : Spec.EntityUID}
{euids euids' : List Spec.EntityUID}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : env.acts.contains auid = true)
(h₃ : euids ≡ euids')
:
Data.Set.any (fun (x : Spec.EntityUID) => Spec.inₑ auid x entities) (Data.Set.make euids) = true ↔ ∃ (euid : Spec.EntityUID), euid ∈ euids' ∧ env.acts.descendentOf auid euid = true
theorem
Cedar.Thm.type_of_mem_is_soundₛ
{x₁ x₂ : Spec.Expr}
{c₁ c₁' c₂' : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ety₁ ety₂ : Spec.EntityType}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : (Validation.typeOf x₁ c₁ env).typeOf = Except.ok (Validation.CedarType.entity ety₁, c₁'))
(h₄ : (Validation.typeOf x₂ c₁ env).typeOf = Except.ok ((Validation.CedarType.entity ety₂).set, c₂'))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
:
∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.binaryApp Spec.BinaryOp.mem x₁ x₂) request entities v ∧ InstanceOfType env v (Validation.CedarType.bool (Validation.typeOfInₛ ety₁ ety₂ x₁ x₂ env))
theorem
Cedar.Thm.type_of_mem_is_sound
{x₁ x₂ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (Spec.Expr.binaryApp Spec.BinaryOp.mem x₁ x₂) c₁ env = Except.ok (ty, c₂))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
:
GuardedCapabilitiesInvariant (Spec.Expr.binaryApp Spec.BinaryOp.mem x₁ x₂) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.binaryApp Spec.BinaryOp.mem x₁ x₂) request entities v ∧ InstanceOfType env v ty.typeOf