This file contains residual-specific lemmas of the theorem residual_well_typed_is_sound
theorem
Cedar.Thm.residual_well_typed_is_sound_val
{v v' : Spec.Value}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ty : Validation.CedarType}
(h₁ : InstanceOfType env v' ty)
(h₂ : (Spec.Residual.val v' ty).evaluate request entities = Except.ok v)
:
InstanceOfType env v (Spec.Residual.val v' ty).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_var
{v : Spec.Value}
{var : Spec.Var}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ty : Validation.CedarType}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : Spec.Var.WellTyped env var ty)
(h₃ : (Spec.Residual.var var ty).evaluate request entities = Except.ok v)
:
InstanceOfType env v (Spec.Residual.var var ty).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_and
{v : Spec.Value}
{x₁ x₂ : Spec.Residual}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool)
(h₂ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool)
(hᵢ₁ : ∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf)
(hᵢ₂ : ∀ {v : Spec.Value}, x₂.evaluate request entities = Except.ok v → InstanceOfType env v x₂.typeOf)
(h₃ : (x₁.and x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.and x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_or
{v : Spec.Value}
{x₁ x₂ : Spec.Residual}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool)
(h₂ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool)
(hᵢ₁ : ∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf)
(hᵢ₂ : ∀ {v : Spec.Value}, x₂.evaluate request entities = Except.ok v → InstanceOfType env v x₂.typeOf)
(h₃ : (x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_ite
{v : Spec.Value}
{x₁ x₂ x₃ : Spec.Residual}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool)
(h₂ : x₂.typeOf = x₃.typeOf)
(hᵢ₁ : ∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf)
(hᵢ₂ : ∀ {v : Spec.Value}, x₂.evaluate request entities = Except.ok v → InstanceOfType env v x₂.typeOf)
(hᵢ₃ : ∀ {v : Spec.Value}, x₃.evaluate request entities = Except.ok v → InstanceOfType env v x₃.typeOf)
(h₃ : (x₁.ite x₂ x₃ x₂.typeOf).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.ite x₂ x₃ x₂.typeOf).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_unary_app
{v : Spec.Value}
{op₁ : Spec.UnaryOp}
{x₁ : Spec.Residual}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ty : Validation.CedarType}
(h₁ : Spec.UnaryResidualWellTyped op₁ x₁ ty)
:
(∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf) →
∀ (h₂ : (Spec.Residual.unaryApp op₁ x₁ ty).evaluate request entities = Except.ok v),
InstanceOfType env v (Spec.Residual.unaryApp op₁ x₁ ty).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_binary_app
{v : Spec.Value}
{op₂ : Spec.BinaryOp}
{x₁ x₂ : Spec.Residual}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ty : Validation.CedarType}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₄ : Spec.BinaryResidualWellTyped env op₂ x₁ x₂ ty)
(hᵢ₁ : ∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf)
(hᵢ₂ : ∀ {v : Spec.Value}, x₂.evaluate request entities = Except.ok v → InstanceOfType env v x₂.typeOf)
(h₃ : (Spec.Residual.binaryApp op₂ x₁ x₂ ty).evaluate request entities = Except.ok v)
:
InstanceOfType env v (Spec.Residual.binaryApp op₂ x₁ x₂ ty).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_has_attr_entity
{v : Spec.Value}
{x₁ : Spec.Residual}
{attr : Spec.Attr}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₃ : (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_has_attr_record
{v : Spec.Value}
{x₁ : Spec.Residual}
{attr : Spec.Attr}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(h₃ : (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_get_attr_entity
{v : Spec.Value}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ety : Spec.EntityType}
{rty : Validation.RecordType}
{x₁ : Spec.Residual}
{attr : Spec.Attr}
{ty : Validation.CedarType}
(h₁ : InstanceOfWellFormedEnvironment request entities env)
(h₂ : ∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf)
(h₄ : x₁.typeOf = Validation.CedarType.entity ety)
(h₅ : Option.map Validation.RecordType.liftBoolTypes (env.ets.attrs? ety) = some rty)
(h₆ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty)
(h₇ : (x₁.getAttr attr ty).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.getAttr attr ty).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_get_attr_record
{v : Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
{rty : Validation.RecordType}
{x₁ : Spec.Residual}
{attr : Spec.Attr}
{ty : Validation.CedarType}
{env : Validation.TypeEnv}
(h₂ : ∀ {v : Spec.Value}, x₁.evaluate request entities = Except.ok v → InstanceOfType env v x₁.typeOf)
(h₄ : x₁.typeOf = Validation.CedarType.record rty)
(h₅ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty)
(h₆ : (x₁.getAttr attr ty).evaluate request entities = Except.ok v)
:
InstanceOfType env v (x₁.getAttr attr ty).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_set
{v : Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
{ls : List Spec.Residual}
{ty : Validation.CedarType}
{env : Validation.TypeEnv}
(h₁ :
∀ (x : Spec.Residual),
x ∈ ls → ∀ (v : Spec.Value), x.evaluate request entities = Except.ok v → InstanceOfType env v x.typeOf)
(h₂ : ∀ (x : Spec.Residual), x ∈ ls → x.typeOf = ty)
(h₃ : (Spec.Residual.set ls ty.set).evaluate request entities = Except.ok v)
:
InstanceOfType env v (Spec.Residual.set ls ty.set).typeOf
theorem
Cedar.Thm.residual_attr_value_has_attrType
{request : Spec.Request}
{entities : Spec.Entities}
{m : List (Spec.Attr × Spec.Residual)}
{r : List (Spec.Attr × Spec.Value)}
{env : Validation.TypeEnv}
(h₁ :
∀ (k : Spec.Attr) (v : Spec.Residual),
(k, v) ∈ m → ∀ (v_1 : Spec.Value), v.evaluate request entities = Except.ok v_1 → InstanceOfType env v_1 v.typeOf)
(h₃ :
List.Forall₂
(fun (x : Spec.Attr × Spec.Residual) (y : Spec.Attr × Spec.Value) =>
Prod.mk x.fst <$> x.snd.evaluate request entities = Except.ok y)
m r)
:
List.Forall₂
(fun (x : Spec.Attr × Spec.Value) (y : Spec.Attr × Validation.Qualified Validation.CedarType) =>
x.fst = y.fst ∧ InstanceOfType env x.snd y.snd.getType)
r
(List.map
(fun (x : Spec.Attr × Spec.Residual) =>
match x with
| (a, ty) => (a, Validation.Qualified.required ty.typeOf))
m)
theorem
Cedar.Thm.residual_well_typed_is_sound_record
{v : Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
{m : List (Spec.Attr × Spec.Residual)}
{rty : Validation.RecordType}
{env : Validation.TypeEnv}
(h₁ :
∀ (k : Spec.Attr) (v : Spec.Residual),
(k, v) ∈ m → ∀ (v_1 : Spec.Value), v.evaluate request entities = Except.ok v_1 → InstanceOfType env v_1 v.typeOf)
(h₂ :
rty = Data.Map.make
(List.map
(fun (x : Spec.Attr × Spec.Residual) =>
match x with
| (a, r) => (a, Validation.Qualified.required r.typeOf))
m))
(h₃ : (Spec.Residual.record m (Validation.CedarType.record rty)).evaluate request entities = Except.ok v)
:
InstanceOfType env v (Spec.Residual.record m (Validation.CedarType.record rty)).typeOf
theorem
Cedar.Thm.residual_well_typed_is_sound_call
{v : Spec.Value}
{request : Spec.Request}
{entities : Spec.Entities}
{xfn : Spec.ExtFun}
{args : List Spec.Residual}
{ty : Validation.CedarType}
{env : Validation.TypeEnv}
(h₁ : Spec.ExtResidualWellTyped xfn args ty)
(h₂ : (Spec.Residual.call xfn args ty).evaluate request entities = Except.ok v)
:
InstanceOfType env v (Spec.Residual.call xfn args ty).typeOf