def Cedar.Thm.EvaluatesToBool (expr : Spec.Expr) (request : Spec.Request) (entities : Spec.Entities) : Prop

For a single expression, evaluates to a boolean value (or appropriate error)

Equations

• Cedar.Thm.EvaluatesToBool expr request entities = ∃ (b : Bool), Cedar.Thm.EvaluatesTo expr request entities (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b))

def Cedar.Thm.AllEvaluateToBool (policies : Spec.Policies) (request : Spec.Request) (entities : Spec.Entities) : Prop

Every policy as an expression evaluates to a boolean value or appropriate error

Equations

• Cedar.Thm.AllEvaluateToBool policies request entities = ∀ (policy : Cedar.Spec.Policy), policy ∈ policies → Cedar.Thm.EvaluatesToBool policy.toExpr request entities

def Cedar.Thm.InstanceOfWellFormedSchema (schema : Validation.Schema) (request : Spec.Request) (entities : Spec.Entities) : Prop

Equations

• Cedar.Thm.InstanceOfWellFormedSchema schema request entities = ∃ (env : Cedar.Validation.TypeEnv), env ∈ schema.environments ∧ Cedar.Thm.InstanceOfWellFormedEnvironment request entities env

theorem Cedar.Thm.action_matches_env {env : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} : InstanceOfWellFormedEnvironment request entities env → request.action = env.reqty.action

theorem Cedar.Thm.typecheck_policy_produces_wt {policy : Spec.Policy} {Γ : Validation.TypeEnv} {tx : Validation.TypedExpr} : Validation.typecheckPolicy policy Γ = Except.ok tx → TypedExpr.WellTyped Γ tx.liftBoolTypes

theorem Cedar.Thm.typecheck_policy_is_sound {policy : Spec.Policy} {env : Validation.TypeEnv} {tx : Validation.TypedExpr} {request : Spec.Request} {entities : Spec.Entities} : InstanceOfWellFormedEnvironment request entities env → Validation.typecheckPolicy policy env = Except.ok tx → ∃ (b : Bool), EvaluatesTo policy.toExpr request entities (Spec.Value.prim (Spec.Prim.bool b))

theorem Cedar.Thm.typecheck_policy_with_environments_is_sound (policy : Spec.Policy) (schema : Validation.Schema) (request : Spec.Request) (entities : Spec.Entities) : (∃ (env : Validation.TypeEnv), env ∈ schema.environments ∧ InstanceOfWellFormedEnvironment request entities env) → Validation.typecheckPolicyWithEnvironments Validation.typecheckPolicy policy schema = Except.ok () → ∃ (b : Bool), EvaluatesTo policy.toExpr request entities (Spec.Value.prim (Spec.Prim.bool b))