theorem
Cedar.Thm.has_tag_false_of_entity_type_tagless
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{uid : Spec.EntityUID}
{tag : Spec.Tag}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(htagless : env.ets.tags? uid.ty = some none)
:
If the schema does not declare that an entity can have tags, then it does not have any tags.
theorem
Cedar.Thm.eq_false_of_distinct_entity_types
{env : Validation.TypeEnv}
{v₁ v₂ : Spec.Value}
{ety₁ ety₂ : Spec.EntityType}
(hinst₁ : InstanceOfType env v₁ (Validation.CedarType.entity ety₁))
(hinst₂ : InstanceOfType env v₂ (Validation.CedarType.entity ety₂))
(hne : ety₁ ≠ ety₂)
:
Two values of distinct entity types cannot be equal.
theorem
Cedar.Thm.mem_false_of_cannot_be_inₑ
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{v₁ v₂ : Spec.Value}
{ety₁ ety₂ : Spec.EntityType}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(hinst₁ : InstanceOfType env v₁ (Validation.CedarType.entity ety₁))
(hinst₂ : InstanceOfType env v₂ (Validation.CedarType.entity ety₂))
(hdesc : env.descendentOf ety₁ ety₂ = false)
:
An entity of type ety₁ cannot be in an entity of type ety₂ when the schema does not declare ety₂ an ancestor type of ety₁.
theorem
Cedar.Thm.mem_false_of_cannot_be_inₛ
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{v₁ v₂ : Spec.Value}
{ety₁ ety₂ : Spec.EntityType}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(hinst₁ : InstanceOfType env v₁ (Validation.CedarType.entity ety₁))
(hinst₂ : InstanceOfType env v₂ (Validation.CedarType.entity ety₂).set)
(hdesc : env.descendentOf ety₁ ety₂ = false)
:
The set-valued counterpart of mem_false_of_cannot_be_inₑ.
theorem
Cedar.Thm.tpe_inₑ_agrees
{es : Spec.Entities}
{pes : TPE.PartialEntities}
{uid₁ uid₂ : Spec.EntityUID}
{b : Bool}
(href : EntitiesRefine es pes)
(hdec : TPE.inₑ uid₁ uid₂ pes = some b)
:
Whenever TPE.inₑ decides in for two concrete UIDs, concrete evaluation agrees.
theorem
Cedar.Thm.try_decide_residual₂_sound
{env : Validation.TypeEnv}
{op₂ : Spec.BinaryOp}
{r₁ r₂ : Spec.Residual}
{req : Spec.Request}
{es : Spec.Entities}
{v : Spec.Value}
(hwf : InstanceOfWellFormedEnvironment req es env)
(hwt₁ : Residual.WellTyped env r₁)
(hwt₂ : Residual.WellTyped env r₂)
(hdec : TPE.tryDecideResidual₂ env op₂ r₁ r₂ = some v)
:
If tryDecideResidual₂ decides a binary operation from the operands' types,
then concrete evaluation agrees.
theorem
Cedar.Thm.partial_evaluate_is_sound_binary_app
{op₂ : Spec.BinaryOp}
{ty : Validation.CedarType}
{x₁ x₂ : Spec.Residual}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{env : Validation.TypeEnv}
(h₂ : InstanceOfWellFormedEnvironment req es env)
(h₄ : RequestAndEntitiesRefine req es preq pes)
(hwt₁ : Residual.WellTyped env x₁)
(hwt₂ : Residual.WellTyped env x₂)
(howt : Spec.BinaryResidualWellTyped env op₂ x₁ x₂ ty)
(hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate env x₁ preq pes).evaluate req es))
(hᵢ₂ : Except.toOption (x₂.evaluate req es) = Except.toOption ((TPE.evaluate env x₂ preq pes).evaluate req es))
:
Except.toOption ((Spec.Residual.binaryApp op₂ x₁ x₂ ty).evaluate req es) = Except.toOption ((TPE.evaluate env (Spec.Residual.binaryApp op₂ x₁ x₂ ty) preq pes).evaluate req es)