Documentation

Cedar.TPE.Evaluator

inductive Cedar.TPE.Error :

evaluation (err : Spec.Error) : Error
invalidPolicy (err : Validation.TypeError) : Error
invalidEnvironment : Error
invalidRequestOrEntities : Error

Instances For

@[instance_reducible]

instance Cedar.TPE.instReprError :

Equations

Cedar.TPE.instReprError = { reprPrec := Cedar.TPE.instReprError.repr }

def Cedar.TPE.instReprError.repr :

Error → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

@[instance_reducible]

instance Cedar.TPE.instInhabitedError :

Inhabited Error

Equations

Cedar.TPE.instInhabitedError = { default := Cedar.TPE.instInhabitedError.default }

def Cedar.TPE.instDecidableEqError.decEq (x✝ x✝¹ : Error) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance Cedar.TPE.instDecidableEqError :

DecidableEq Error

Equations

Cedar.TPE.instDecidableEqError = Cedar.TPE.instDecidableEqError.decEq

@[instance_reducible]

instance Cedar.TPE.instCoeErrorError :

Coe Spec.Error Error

Equations

Cedar.TPE.instCoeErrorError = { coe := Cedar.TPE.Error.evaluation }

def Cedar.TPE.someOrError :

Option Spec.Value → Validation.CedarType → Spec.Residual

Equations

Cedar.TPE.someOrError (some v) x✝ = Cedar.Spec.Residual.val v x✝
Cedar.TPE.someOrError none x✝ = Cedar.Spec.Residual.error x✝

Instances For

def Cedar.TPE.someOrSelf :

Option Spec.Value → Validation.CedarType → Spec.Residual → Spec.Residual

Equations

Cedar.TPE.someOrSelf (some v) x✝¹ x✝ = Cedar.Spec.Residual.val v x✝¹
Cedar.TPE.someOrSelf none x✝¹ x✝ = x✝

Instances For

def Cedar.TPE.varₚ (req : PartialRequest) (var : Spec.Var) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.varₚ req Cedar.Spec.Var.resource ty = Cedar.TPE.varₚ.varₒ Cedar.Spec.Var.resource ty do let a ← req.resource.asEntityUID pure (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID a))
Cedar.TPE.varₚ req Cedar.Spec.Var.action ty = Cedar.TPE.varₚ.varₒ Cedar.Spec.Var.action ty (some (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.action)))

Instances For

def Cedar.TPE.varₚ.varₒ (var : Spec.Var) (ty : Validation.CedarType) :

Option Spec.Value → Spec.Residual

Equations

Cedar.TPE.varₚ.varₒ var ty x✝ = Cedar.TPE.someOrSelf x✝ ty (Cedar.Spec.Residual.var var ty)

Instances For

def Cedar.TPE.ite (c t e : Spec.Residual) (ty : Validation.CedarType) :

Equations

Cedar.TPE.ite (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b)) ty_1) t e ty = if b = true then t else e
Cedar.TPE.ite (Cedar.Spec.Residual.error ty_1) t e ty = Cedar.Spec.Residual.error ty
Cedar.TPE.ite c t e ty = c.ite t e ty

Instances For

def Cedar.TPE.and :

Spec.Residual → Spec.Residual → Validation.CedarType → Spec.Residual

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.and (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool true)) ty) x✝¹ x✝ = x✝¹
Cedar.TPE.and (Cedar.Spec.Residual.error ty) x✝¹ x✝ = Cedar.Spec.Residual.error x✝
Cedar.TPE.and x✝¹ (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool true)) ty) x✝ = x✝¹
Cedar.TPE.and x✝² x✝¹ x✝ = x✝².and x✝¹ x✝

Instances For

def Cedar.TPE.or :

Spec.Residual → Spec.Residual → Validation.CedarType → Spec.Residual

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.or (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool false)) ty) x✝¹ x✝ = x✝¹
Cedar.TPE.or (Cedar.Spec.Residual.error ty) x✝¹ x✝ = Cedar.Spec.Residual.error x✝
Cedar.TPE.or x✝¹ (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool false)) ty) x✝ = x✝¹
Cedar.TPE.or x✝² x✝¹ x✝ = x✝².or x✝¹ x✝

Instances For

def Cedar.TPE.tryDecideResidual₁ (op₁ : Spec.UnaryOp) (r : Spec.Residual) :

Option Spec.Value

Equations

Cedar.TPE.tryDecideResidual₁ (Cedar.Spec.UnaryOp.is ety₁) r = if r.errorFree = true then some (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (ety₁ == ety₂))) else none
Cedar.TPE.tryDecideResidual₁ op₁✝ r = if r.errorFree = true then none else none

Instances For

def Cedar.TPE.apply₁ (op₁ : Spec.UnaryOp) (r : Spec.Residual) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.apply₁ op₁ (Cedar.Spec.Residual.error ty_1) ty = Cedar.Spec.Residual.error ty

Instances For

def Cedar.TPE.inₑ (uid₁ uid₂ : Spec.EntityUID) (es : PartialEntities) :

Equations

Cedar.TPE.inₑ uid₁ uid₂ es = if uid₁ = uid₂ then some true else Option.map (fun (x : Cedar.Data.Set Cedar.Spec.EntityUID) => x.contains uid₂) (es.ancestors uid₁)

Instances For

def Cedar.TPE.inₛ (uid : Spec.EntityUID) (vs : Data.Set Spec.Value) (es : PartialEntities) :

Equations

Cedar.TPE.inₛ uid vs es = do let __do_lift ← List.mapM (Except.toOption ∘ Cedar.Spec.Value.asEntityUID) vs.toList __do_lift.ternaryAny fun (x : Cedar.Spec.EntityUID) => Cedar.TPE.inₑ uid x es

Instances For

def Cedar.TPE.hasTag (uid : Spec.EntityUID) (tag : String) (es : PartialEntities) :

Equations

Cedar.TPE.hasTag uid tag es = Option.map (fun (x : Cedar.Data.Map String Cedar.Spec.Value) => x.contains tag) (es.tags uid)

Instances For

def Cedar.TPE.getTag (uid : Spec.EntityUID) (tag : String) (es : PartialEntities) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cedar.TPE.tryDecideResidual₂ (env : Validation.TypeEnv) (op₂ : Spec.BinaryOp) (r₁ r₂ : Spec.Residual) :

Option Spec.Value

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.tryDecideResidual₂ env op₂✝ r₁ r₂ = if (r₁.errorFree && r₂.errorFree) = true then none else none

Instances For

def Cedar.TPE.apply₂ (env : Validation.TypeEnv) (op₂ : Spec.BinaryOp) (r₁ r₂ : Spec.Residual) (es : PartialEntities) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.apply₂ env op₂ (Cedar.Spec.Residual.error ty_1) r₂ es ty = Cedar.Spec.Residual.error ty
Cedar.TPE.apply₂ env op₂ r₁ (Cedar.Spec.Residual.error ty_1) es ty = Cedar.Spec.Residual.error ty

Instances For

def Cedar.TPE.apply₂.self (op₂ : Spec.BinaryOp) (r₁ r₂ : Spec.Residual) (ty : Validation.CedarType) :

Equations

Cedar.TPE.apply₂.self op₂ r₁ r₂ ty = Cedar.Spec.Residual.binaryApp op₂ r₁ r₂ ty

Instances For

def Cedar.TPE.attrsOf (r : Spec.Residual) (lookup : Spec.EntityUID → Option (Data.Map Spec.Attr Spec.Value)) :

Option (Data.Map Spec.Attr Spec.Value)

Equations

Cedar.TPE.attrsOf (Cedar.Spec.Residual.val (Cedar.Spec.Value.record m) ty) lookup = some m
Cedar.TPE.attrsOf (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)) ty) lookup = lookup uid
Cedar.TPE.attrsOf r lookup = none

Instances For

def Cedar.TPE.tryDecideHasResidual (env : Validation.TypeEnv) (r : Spec.Residual) (a : Spec.Attr) :

Option Spec.Value

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cedar.TPE.hasAttr (env : Validation.TypeEnv) (r : Spec.Residual) (a : Spec.Attr) (es : PartialEntities) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.hasAttr env (Cedar.Spec.Residual.error ty_1) a es ty = Cedar.Spec.Residual.error ty

Instances For

def Cedar.TPE.extHasAttr (env : Validation.TypeEnv) (r : Spec.Residual) (a : Spec.Attr) (as : List Spec.Attr) (es : PartialEntities) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.extHasAttr env (Cedar.Spec.Residual.error ty_1) a as es ty = Cedar.Spec.Residual.error ty

Instances For

def Cedar.TPE.extHasAttr.tryDecide (env : Validation.TypeEnv) (r : Spec.Residual) (a : Spec.Attr) (as : List Spec.Attr) (ty : Validation.CedarType) :

Equations

Cedar.TPE.extHasAttr.tryDecide env r a as ty = match Cedar.TPE.tryDecideHasResidual env r a with | some v => Cedar.Spec.Residual.val v ty | none => r.extHasAttr a as ty

Instances For

def Cedar.TPE.extHasAttr.loop (env : Validation.TypeEnv) (m : Data.Map Spec.Attr Spec.Value) (attrs : List Spec.Attr) (es : PartialEntities) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.extHasAttr.loop env m [] es ty = Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool true)) (Cedar.Validation.CedarType.bool Cedar.Validation.BoolType.anyBool)

Instances For

def Cedar.TPE.getAttr (r : Spec.Residual) (a : Spec.Attr) (es : PartialEntities) (ty : Validation.CedarType) :

Equations

Cedar.TPE.getAttr (Cedar.Spec.Residual.error ty_1) a es ty = Cedar.Spec.Residual.error ty
Cedar.TPE.getAttr r a es ty = match Cedar.TPE.attrsOf r es.attrs with | some m => Cedar.TPE.someOrError (m.find? a) ty | none => r.getAttr a ty

Instances For

def Cedar.TPE.set (rs : List Spec.Residual) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cedar.TPE.record (m : List (Spec.Attr × Spec.Residual)) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.

Instances For

def Cedar.TPE.call (xfn : Spec.ExtFun) (rs : List Spec.Residual) (ty : Validation.CedarType) :

Equations

One or more equations did not get rendered due to their size.

Instances For

@[irreducible]

def Cedar.TPE.evaluate (env : Validation.TypeEnv) (x : Spec.Residual) (req : PartialRequest) (es : PartialEntities) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.evaluate env (Cedar.Spec.Residual.val l ty) req es = Cedar.Spec.Residual.val l ty
Cedar.TPE.evaluate env (Cedar.Spec.Residual.var v ty) req es = Cedar.TPE.varₚ req v ty
Cedar.TPE.evaluate env (Cedar.Spec.Residual.error ty) req es = Cedar.Spec.Residual.error ty
Cedar.TPE.evaluate env (x₁.ite x₂ x₃ ty) req es = Cedar.TPE.ite (Cedar.TPE.evaluate env x₁ req es) (Cedar.TPE.evaluate env x₂ req es) (Cedar.TPE.evaluate env x₃ req es) ty
Cedar.TPE.evaluate env (x₁.and x₂ ty) req es = Cedar.TPE.and (Cedar.TPE.evaluate env x₁ req es) (Cedar.TPE.evaluate env x₂ req es) ty
Cedar.TPE.evaluate env (x₁.or x₂ ty) req es = Cedar.TPE.or (Cedar.TPE.evaluate env x₁ req es) (Cedar.TPE.evaluate env x₂ req es) ty
Cedar.TPE.evaluate env (Cedar.Spec.Residual.unaryApp op₁ x₁ ty) req es = Cedar.TPE.apply₁ op₁ (Cedar.TPE.evaluate env x₁ req es) ty
Cedar.TPE.evaluate env (Cedar.Spec.Residual.binaryApp op₂ x₁ x₂ ty) req es = Cedar.TPE.apply₂ env op₂ (Cedar.TPE.evaluate env x₁ req es) (Cedar.TPE.evaluate env x₂ req es) es ty
Cedar.TPE.evaluate env (x₁.hasAttr a ty) req es = Cedar.TPE.hasAttr env (Cedar.TPE.evaluate env x₁ req es) a es ty
Cedar.TPE.evaluate env (x₁.extHasAttr a as ty) req es = Cedar.TPE.extHasAttr env (Cedar.TPE.evaluate env x₁ req es) a as es ty
Cedar.TPE.evaluate env (x₁.getAttr a ty) req es = Cedar.TPE.getAttr (Cedar.TPE.evaluate env x₁ req es) a es ty

Instances For

def Cedar.TPE.evaluatePolicy (schema : Validation.Schema) (p : Spec.Policy) (req : PartialRequest) (es : PartialEntities) :

Except Error Spec.Residual

Partially evaluating a policy. Note that this function actually evaluates a type-lifted version of TypedExpr produced by the type checker, as opposed to evaluating the expression directly. This design is to simplify proofs otherwise we need to prove theorems that state type-lifting (i.e, TypedExpr.liftBoolTypes) do not change the results of evaluating residuals. The soundness theorem still holds. That is, reauthorizing the residuals produces the same outcome as authorizing the input expressions with consistent requests/entities. It is just that the types in the residuals are all lifted. We essentially trade efficiency for ease of proofs, which I (Shaobo) think is fine because the Lean model is a reference model not used in production.

Equations

One or more equations did not get rendered due to their size.

Instances For