Cedar.Thm.SymCC.WellTyped

This file contains some results about wellTypedPolicies and wellTypedPolicy preserving the validity or results of some definitions (StronglyWellFormedFor*, evaluate, isAuthorized, etc.).

source

theorem Cedar.Thm.wellTypedPolicy_ok_implies_exists_typed_exprs {Γ : Validation.TypeEnv} {p p' : Spec.Policy} (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') :

∃ (tx : Validation.TypedExpr ), ∃ (tx' : Validation.TypedExpr ), ∃ (c : Validation.Capabilities ), TypedExpr.WellTyped Γ tx.liftBoolTypes ∧ TypedExpr.WellTyped Γ tx' ∧ Validation.typeOf (Validation.substituteAction Γ.reqty.action p.toExpr) ∅ Γ = Except.ok (tx, c) ∧ p'.toExpr = tx'.toExpr ∧ tx' = (Validation.TypedExpr.lit (Spec.Prim.bool true) (Validation.CedarType.bool Validation.BoolType.anyBool)).and ((Validation.TypedExpr.lit (Spec.Prim.bool true) (Validation.CedarType.bool Validation.BoolType.anyBool)).and ((Validation.TypedExpr.lit (Spec.Prim.bool true) (Validation.CedarType.bool Validation.BoolType.anyBool)).and tx.liftBoolTypes (Validation.CedarType.bool Validation.BoolType.anyBool)) (Validation.CedarType.bool Validation.BoolType.anyBool)) (Validation.CedarType.bool Validation.BoolType.anyBool) ∧ tx.liftBoolTypes.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool

Reduces wellTypedPolicy being ok to the existence of TypedExprs.

source

theorem Cedar.Thm.wellTypedPolicy_ok_implies_well_typed_expr {Γ : Validation.TypeEnv} {p p' : Spec.Policy} (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') :

∃ (tx : Validation.TypedExpr ), TypedExpr.WellTyped Γ tx ∧ tx.toExpr = p'.toExpr

If a policy p is well-typed via wellTypedPolicy, then there is a well-typed TypedExpr corresponding to p's condition.

source

@[irreducible]

theorem Cedar.Thm.substitute_action_preserves_valid_refs {Γ : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} {expr : Spec.Expr} (hinst : InstanceOfWellFormedEnvironment request entities Γ) :

entities.ValidRefsFor expr ↔ entities.ValidRefsFor (Validation.substituteAction request.action expr)

wellTypedPolicy preserves Entities.ValidRefsFor.

source

theorem Cedar.Thm.wellTypedPolicy_preserves_valid_refs {Γ : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} {p p' : Spec.Policy} (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') (hswf : entities.ValidRefsFor p.toExpr) :

entities.ValidRefsFor p'.toExpr

wellTypedPolicy preserves Entities.ValidRefsFor.

source

theorem Cedar.Thm.wellTypedPolicy_preserves_StronglyWellFormedForPolicy {Γ : Validation.TypeEnv} {env : Spec.Env} {p p' : Spec.Policy} (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') (hswf : env.StronglyWellFormedForPolicy p) :

env.StronglyWellFormedForPolicy p'

source

theorem Cedar.Thm.wellTypedPolicies_preserves_StronglyWellFormedForPolicies {Γ : Validation.TypeEnv} {env : Spec.Env} {ps ps' : Spec.Policies} (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') (hswf : env.StronglyWellFormedForPolicies ps) :

env.StronglyWellFormedForPolicies ps'

source

theorem Cedar.Thm.wellTypedPolicy_preserves_evaluation {Γ : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} {p p' : Spec.Policy} (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') :

Spec.evaluate p.toExpr request entities = Spec.evaluate p'.toExpr request entities

wellTypedPolicy preserves the result of evaluate.

source

theorem Cedar.Thm.wellTypedPolicies_preserves_policy_id_and_effect {Γ : Validation.TypeEnv} {p p' : Spec.Policy} (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') :

p.id = p'.id ∧ p.effect = p'.effect

source

theorem Cedar.Thm.wellTypedPolicies_preserves_satisfiedWithEffect {Γ : Validation.TypeEnv} {entities : Spec.Entities} {request : Spec.Request} {p p' : Spec.Policy} (effect : Spec.Effect) (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') :

Spec.satisfiedWithEffect effect p request entities = Spec.satisfiedWithEffect effect p' request entities

source

theorem Cedar.Thm.wellTypedPolicies_preserves_satisfiedPolicies {Γ : Validation.TypeEnv} {entities : Spec.Entities} {request : Spec.Request} {ps ps' : Spec.Policies} (effect : Spec.Effect) (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') :

Spec.satisfiedPolicies effect ps request entities = Spec.satisfiedPolicies effect ps' request entities

source

theorem Cedar.Thm.wellTypedPolicies_preserves_errored {Γ : Validation.TypeEnv} {entities : Spec.Entities} {request : Spec.Request} {p p' : Spec.Policy} (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') :

Spec.errored p request entities = Spec.errored p' request entities

source

theorem Cedar.Thm.wellTypedPolicies_preserves_errorPolicies {Γ : Validation.TypeEnv} {entities : Spec.Entities} {request : Spec.Request} {ps ps' : Spec.Policies} (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') :

Spec.errorPolicies ps request entities = Spec.errorPolicies ps' request entities

source

theorem Cedar.Thm.wellTypedPolicies_preserves_isAuthorized {Γ : Validation.TypeEnv} {entities : Spec.Entities} {request : Spec.Request} {ps ps' : Spec.Policies} (hinst : InstanceOfWellFormedEnvironment request entities Γ) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') :

Spec.isAuthorized request entities ps = Spec.isAuthorized request entities ps'

wellTypedPolicies preserves the result of isAuthorized.