theorem
Cedar.Thm.try_decide_residual₂_is_bool
{env : Validation.TypeEnv}
{op₂ : Spec.BinaryOp}
{r₁ r₂ : Spec.Residual}
{v : Spec.Value}
(hdec : TPE.tryDecideResidual₂ env op₂ r₁ r₂ = some v)
:
The reductions only ever decide a boolean.
theorem
Cedar.Thm.tags_if_partial_tags
{env : Validation.TypeEnv}
{req : Spec.Request}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
{uid : Spec.EntityUID}
{tags : Data.Map Spec.Tag Spec.Value}
(h_wf : InstanceOfWellFormedEnvironment req es env)
(h_eref : EntitiesRefine es pes)
(h_tags : pes.tags uid = some tags)
:
theorem
Cedar.Thm.entity_tag_well_typed
{env : Validation.TypeEnv}
{req : Spec.Request}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
{uid : Spec.EntityUID}
{ety : Spec.EntityType}
{tags : Data.Map Spec.Tag Spec.Value}
{v : Spec.Value}
{ty : Validation.CedarType}
:
InstanceOfWellFormedEnvironment req es env →
EntitiesRefine es pes →
InstanceOfEntityType uid ety env →
pes.tags uid = some tags →
v ∈ tags.values → env.ets.tags? ety = some (some ty) → InstanceOfType env v ty.liftBoolTypes
theorem
Cedar.Thm.partial_eval_well_typed_app₂_values_hasTag
{env : Validation.TypeEnv}
{expr1 : Spec.Residual}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{expr2 : Spec.Residual}
{id₁ : Spec.EntityUID}
{id₂ : String}
{ty : Validation.CedarType}
{id1 : Spec.EntityUID}
{id2 : String}
{req : Spec.Request}
{es : Spec.Entities}
:
Residual.WellTyped env (TPE.evaluate env expr1 preq pes) →
Residual.WellTyped env (TPE.evaluate env expr2 preq pes) →
(TPE.evaluate env expr1 preq pes).asValue = some (Spec.Value.prim (Spec.Prim.entityUID id₁)) →
(TPE.evaluate env expr2 preq pes).asValue = some (Spec.Value.prim (Spec.Prim.string id₂)) →
PEWellTyped env (Spec.Residual.binaryApp Spec.BinaryOp.hasTag expr1 expr2 ty)
(TPE.someOrSelf ((TPE.hasTag id1 id2 pes).bind fun (a : Bool) => some (Spec.Value.prim (Spec.Prim.bool a))) ty
(Spec.Residual.binaryApp Spec.BinaryOp.hasTag (TPE.evaluate env expr1 preq pes)
(TPE.evaluate env expr2 preq pes) ty))
req preq es pes
theorem
Cedar.Thm.partial_eval_well_typed_app₂_values_getTag
{env : Validation.TypeEnv}
{expr1 : Spec.Residual}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{expr2 : Spec.Residual}
{id₁ : Spec.EntityUID}
{id₂ : String}
{ty : Validation.CedarType}
{req : Spec.Request}
{es : Spec.Entities}
:
Residual.WellTyped env (TPE.evaluate env expr1 preq pes) →
Residual.WellTyped env (TPE.evaluate env expr2 preq pes) →
(TPE.evaluate env expr1 preq pes).asValue = some (Spec.Value.prim (Spec.Prim.entityUID id₁)) →
(TPE.evaluate env expr2 preq pes).asValue = some (Spec.Value.prim (Spec.Prim.string id₂)) →
PEWellTyped env (Spec.Residual.binaryApp Spec.BinaryOp.getTag expr1 expr2 ty) (TPE.getTag id₁ id₂ pes ty) req
preq es pes
theorem
Cedar.Thm.partial_eval_well_typed_app₂_values_mem
{env : Validation.TypeEnv}
{expr1 : Spec.Residual}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{expr2 : Spec.Residual}
{v₁ v₂ : Spec.Value}
{ty : Validation.CedarType}
{req : Spec.Request}
{es : Spec.Entities}
:
Residual.WellTyped env (TPE.evaluate env expr1 preq pes) →
Residual.WellTyped env (TPE.evaluate env expr2 preq pes) →
(TPE.evaluate env expr1 preq pes).asValue = some v₁ →
(TPE.evaluate env expr2 preq pes).asValue = some v₂ →
PEWellTyped env (Spec.Residual.binaryApp Spec.BinaryOp.mem expr1 expr2 ty)
(Spec.Residual.binaryApp Spec.BinaryOp.mem (TPE.evaluate env expr1 preq pes) (TPE.evaluate env expr2 preq pes)
ty)
req preq es pes
theorem
Cedar.Thm.partial_eval_well_typed_app₂_values
{env : Validation.TypeEnv}
{expr1 : Spec.Residual}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{expr2 : Spec.Residual}
{v₁ v₂ : Spec.Value}
{op : Spec.BinaryOp}
{ty : Validation.CedarType}
{req : Spec.Request}
{es : Spec.Entities}
:
Residual.WellTyped env (TPE.evaluate env expr1 preq pes) →
Residual.WellTyped env (TPE.evaluate env expr2 preq pes) →
(TPE.evaluate env expr1 preq pes).asValue = some v₁ →
(TPE.evaluate env expr2 preq pes).asValue = some v₂ →
PEWellTyped env (Spec.Residual.binaryApp op expr1 expr2 ty)
(TPE.apply₂ env op (TPE.evaluate env expr1 preq pes) (TPE.evaluate env expr2 preq pes) pes ty) req preq es pes
theorem
Cedar.Thm.partial_eval_well_typed_app₂_nonvalues
{env : Validation.TypeEnv}
{expr1 : Spec.Residual}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{expr2 : Spec.Residual}
{op : Spec.BinaryOp}
{ty : Validation.CedarType}
{req : Spec.Request}
{es : Spec.Entities}
:
Residual.WellTyped env (TPE.evaluate env expr1 preq pes) →
Residual.WellTyped env (TPE.evaluate env expr2 preq pes) →
(TPE.evaluate env expr1 preq pes).asValue = none ∨ (TPE.evaluate env expr2 preq pes).asValue = none →
PEWellTyped env (Spec.Residual.binaryApp op expr1 expr2 ty)
(TPE.apply₂ env op (TPE.evaluate env expr1 preq pes) (TPE.evaluate env expr2 preq pes) pes ty) req preq es pes
theorem
Cedar.Thm.partial_eval_well_typed_app₂
{env : Validation.TypeEnv}
{expr1 : Spec.Residual}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{expr2 : Spec.Residual}
{op : Spec.BinaryOp}
{ty : Validation.CedarType}
{req : Spec.Request}
{es : Spec.Entities}
:
Residual.WellTyped env (TPE.evaluate env expr1 preq pes) →
Residual.WellTyped env (TPE.evaluate env expr2 preq pes) →
PEWellTyped env (Spec.Residual.binaryApp op expr1 expr2 ty)
(TPE.apply₂ env op (TPE.evaluate env expr1 preq pes) (TPE.evaluate env expr2 preq pes) pes ty) req preq es pes