Documentation

Cedar.TPE.Evaluator

inductive Cedar.TPE.Error :

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

Instances For

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 Cedar.TPE.instReprError :

Equations

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

def Cedar.TPE.instInhabitedError.default :

Equations

Cedar.TPE.instInhabitedError.default = Cedar.TPE.Error.invalidEnvironment

Instances For

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 Cedar.TPE.instDecidableEqError :

DecidableEq Error

Equations

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

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.apply₁ (op₁ : Spec.UnaryOp) (r : Spec.Residual) (ty : Validation.CedarType) :

Equations

Cedar.TPE.apply₁ op₁ (Cedar.Spec.Residual.error ty_1) ty = Cedar.Spec.Residual.error ty
Cedar.TPE.apply₁ op₁ r ty = match r.asValue with | some v => Cedar.TPE.someOrError (Except.toOption (Cedar.Spec.apply₁ op₁ v)) ty | none => Cedar.Spec.Residual.unaryApp op₁ r 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 List.anyM (fun (x : Cedar.Spec.EntityUID) => Cedar.TPE.inₑ uid x es) __do_lift

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.apply₂ (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.

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.hasAttr (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 (Cedar.Spec.Residual.error ty_1) a es ty = Cedar.Spec.Residual.error ty

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 (x : Spec.Residual) (req : PartialRequest) (es : PartialEntities) :

Equations

One or more equations did not get rendered due to their size.
Cedar.TPE.evaluate (Cedar.Spec.Residual.val l ty) req es = Cedar.Spec.Residual.val l ty
Cedar.TPE.evaluate (Cedar.Spec.Residual.var v ty) req es = Cedar.TPE.varₚ req v ty
Cedar.TPE.evaluate (Cedar.Spec.Residual.error ty) req es = Cedar.Spec.Residual.error ty
Cedar.TPE.evaluate (x₁.ite x₂ x₃ ty) req es = Cedar.TPE.ite (Cedar.TPE.evaluate x₁ req es) (Cedar.TPE.evaluate x₂ req es) (Cedar.TPE.evaluate x₃ req es) ty
Cedar.TPE.evaluate (x₁.and x₂ ty) req es = Cedar.TPE.and (Cedar.TPE.evaluate x₁ req es) (Cedar.TPE.evaluate x₂ req es) ty
Cedar.TPE.evaluate (x₁.or x₂ ty) req es = Cedar.TPE.or (Cedar.TPE.evaluate x₁ req es) (Cedar.TPE.evaluate x₂ req es) ty
Cedar.TPE.evaluate (Cedar.Spec.Residual.unaryApp op₁ x₁ ty) req es = Cedar.TPE.apply₁ op₁ (Cedar.TPE.evaluate x₁ req es) ty
Cedar.TPE.evaluate (Cedar.Spec.Residual.binaryApp op₂ x₁ x₂ ty) req es = Cedar.TPE.apply₂ op₂ (Cedar.TPE.evaluate x₁ req es) (Cedar.TPE.evaluate x₂ req es) es ty
Cedar.TPE.evaluate (x₁.hasAttr a ty) req es = Cedar.TPE.hasAttr (Cedar.TPE.evaluate x₁ req es) a es ty
Cedar.TPE.evaluate (x₁.getAttr a ty) req es = Cedar.TPE.getAttr (Cedar.TPE.evaluate 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