Documentation

Cedar.TPE.Residual

inductive Cedar.Spec.Residual :

val (v : Value) (ty : Validation.CedarType) : Residual
var (v : Var) (ty : Validation.CedarType) : Residual
ite (cond thenExpr elseExpr : Residual) (ty : Validation.CedarType) : Residual
and (a b : Residual) (ty : Validation.CedarType) : Residual
or (a b : Residual) (ty : Validation.CedarType) : Residual
unaryApp (op : UnaryOp) (expr : Residual) (ty : Validation.CedarType) : Residual
binaryApp (op : BinaryOp) (a b : Residual) (ty : Validation.CedarType) : Residual
getAttr (expr : Residual) (attr : Attr) (ty : Validation.CedarType) : Residual
hasAttr (expr : Residual) (attr : Attr) (ty : Validation.CedarType) : Residual
set (ls : List Residual) (ty : Validation.CedarType) : Residual
record (map : List (Attr × Residual)) (ty : Validation.CedarType) : Residual
call (xfn : ExtFun) (args : List Residual) (ty : Validation.CedarType) : Residual
error (ty : Validation.CedarType) : Residual

Instances For

partial def Cedar.Spec.instReprResidual.repr :

Residual → Nat → Std.Format

instance Cedar.Spec.instReprResidual :

Equations

Cedar.Spec.instReprResidual = { reprPrec := Cedar.Spec.instReprResidual.repr }

def Cedar.Spec.instInhabitedResidual.default :

Equations

Cedar.Spec.instInhabitedResidual.default = Cedar.Spec.Residual.val default default

Instances For

instance Cedar.Spec.instInhabitedResidual :

Inhabited Residual

Equations

Cedar.Spec.instInhabitedResidual = { default := Cedar.Spec.instInhabitedResidual.default }

instance Cedar.Spec.instCoeBoolResidual :

Coe Bool Residual

Equations

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

instance Cedar.Spec.instCoeStringResidual :

Coe String Residual

Equations

Cedar.Spec.instCoeStringResidual = { coe := fun (s : String) => Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)) Cedar.Validation.CedarType.string }

instance Cedar.Spec.instCoeEntityUIDResidual :

Coe EntityUID Residual

Equations

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

def Cedar.Spec.Residual.asValue :

Residual → Option Value

Equations

(Cedar.Spec.Residual.val v ty).asValue = some v
x✝.asValue = none

Instances For

def Cedar.Spec.Value.toResidual (v : Value) (ty : Validation.CedarType) :

Equations

v.toResidual ty = Cedar.Spec.Residual.val v ty

Instances For

def Cedar.Spec.Residual.isError :

Residual → Bool

Equations

(Cedar.Spec.Residual.error ty).isError = true
x✝.isError = false

Instances For

def Cedar.Spec.Residual.typeOf :

Residual → Validation.CedarType

Equations

(Cedar.Spec.Residual.val a a_1).typeOf = a_1
(Cedar.Spec.Residual.var a a_1).typeOf = a_1
(a.ite a_1 a_2 a_3).typeOf = a_3
(a.and a_1 a_2).typeOf = a_2
(a.or a_1 a_2).typeOf = a_2
(Cedar.Spec.Residual.unaryApp a a_1 a_2).typeOf = a_2
(Cedar.Spec.Residual.binaryApp a a_1 a_2 a_3).typeOf = a_3
(a.getAttr a_1 a_2).typeOf = a_2
(a.hasAttr a_1 a_2).typeOf = a_2
(Cedar.Spec.Residual.set a a_1).typeOf = a_1
(Cedar.Spec.Residual.record a a_1).typeOf = a_1
(Cedar.Spec.Residual.call a a_1 a_2).typeOf = a_2
(Cedar.Spec.Residual.error a).typeOf = a

Instances For

def Cedar.Spec.BinaryOp.canError :

BinaryOp → Bool

Equations

Instances For

def Cedar.Spec.UnaryOp.canError :

UnaryOp → Bool

Equations

Cedar.Spec.UnaryOp.neg.canError = true
x✝.canError = false

Instances For

@[irreducible]

def Cedar.Spec.Residual.errorFree :

Residual → Bool

Equations

(Cedar.Spec.Residual.val v ty).errorFree = true
(Cedar.Spec.Residual.var v ty).errorFree = true
(Cedar.Spec.Residual.binaryApp op x₁ x₂ ty).errorFree = (!op.canError && x₁.errorFree && x₂.errorFree)
(Cedar.Spec.Residual.unaryApp op x₁ ty).errorFree = (!op.canError && x₁.errorFree)
(x₁.and x₂ ty).errorFree = (x₁.errorFree && x₂.errorFree)
(x₁.or x₂ ty).errorFree = (x₁.errorFree && x₂.errorFree)
(x₁.ite x₂ x₃ ty).errorFree = (x₁.errorFree && x₂.errorFree && x₃.errorFree)
(x₁.hasAttr attr ty).errorFree = x₁.errorFree
(Cedar.Spec.Residual.set xs ty).errorFree = xs.attach.all fun (x : { x : Cedar.Spec.Residual // x ∈ xs }) => have this := ⋯; x.val.errorFree
(Cedar.Spec.Residual.record xs ty).errorFree = xs.attach₂.all fun (ax : { x : Cedar.Spec.Attr × Cedar.Spec.Residual // sizeOf x.snd < 1 + sizeOf xs }) => ax.val.snd.errorFree
x✝.errorFree = false

Instances For

@[irreducible]

def Cedar.Spec.Residual.evaluate (x : Residual) (req : Request) (es : Entities) :

Equations

One or more equations did not get rendered due to their size.
(Cedar.Spec.Residual.val v ty).evaluate req es = Except.ok v
(Cedar.Spec.Residual.var Cedar.Spec.Var.principal ty).evaluate req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.principal))
(Cedar.Spec.Residual.var Cedar.Spec.Var.resource ty).evaluate req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.resource))
(Cedar.Spec.Residual.var Cedar.Spec.Var.action ty).evaluate req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.action))
(Cedar.Spec.Residual.var Cedar.Spec.Var.context ty).evaluate req es = Except.ok (Cedar.Spec.Value.record req.context)
(c.ite x_2 y ty).evaluate req es = do let c ← c.evaluate req es let b ← c.asBool if b = true then x_2.evaluate req es else y.evaluate req es
(Cedar.Spec.Residual.unaryApp op e ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.apply₁ op v
(Cedar.Spec.Residual.binaryApp op x_2 y ty).evaluate req es = do let v₁ ← x_2.evaluate req es let v₂ ← y.evaluate req es Cedar.Spec.apply₂ op v₁ v₂ es
(e.hasAttr a ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.hasAttr v a es
(e.getAttr a ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.getAttr v a es
(Cedar.Spec.Residual.error ty).evaluate req es = Except.error Cedar.Spec.Error.extensionError

Instances For

@[irreducible]

def Cedar.Spec.Residual.allLiteralUIDs (x : Residual) :

Data.Set EntityUID

Equations

One or more equations did not get rendered due to their size.
(Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)) _ty).allLiteralUIDs = Cedar.Data.Set.singleton uid
(Cedar.Spec.Residual.val v ty).allLiteralUIDs = Cedar.Data.Set.empty
(Cedar.Spec.Residual.error _e).allLiteralUIDs = Cedar.Data.Set.empty
(Cedar.Spec.Residual.var v ty).allLiteralUIDs = Cedar.Data.Set.empty
(x₁.ite x₂ x₃ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs ∪ x₃.allLiteralUIDs
(x₁.and x₂ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs
(x₁.or x₂ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs
(Cedar.Spec.Residual.unaryApp op x_2 ty).allLiteralUIDs = x_2.allLiteralUIDs
(Cedar.Spec.Residual.binaryApp op x₁ x₂ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs
(x_2.getAttr attr ty).allLiteralUIDs = x_2.allLiteralUIDs
(x_2.hasAttr attr ty).allLiteralUIDs = x_2.allLiteralUIDs
(Cedar.Spec.Residual.set x_2 ty).allLiteralUIDs = x_2.mapUnion₁ fun (x : { x : Cedar.Spec.Residual // x ∈ x_2 }) => match x with | ⟨v, property⟩ => v.allLiteralUIDs
(Cedar.Spec.Residual.call xfn x_2 ty).allLiteralUIDs = x_2.mapUnion₁ fun (x : { x : Cedar.Spec.Residual // x ∈ x_2 }) => match x with | ⟨v, property⟩ => v.allLiteralUIDs

Instances For

def Cedar.Spec.decResidual (x y : Residual) :

Decidable (x = y)

Equations

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

Instances For

def Cedar.Spec.decProdAttrResidualList (axs ays : List (Attr × Residual)) :

Decidable (axs = ays)

Equations

One or more equations did not get rendered due to their size.
Cedar.Spec.decProdAttrResidualList [] [] = isTrue Cedar.Spec.decResidual._proof_224
Cedar.Spec.decProdAttrResidualList (head :: tail) [] = isFalse ⋯
Cedar.Spec.decProdAttrResidualList [] (head :: tail) = isFalse ⋯

Instances For

def Cedar.Spec.decResidualList (xs ys : List Residual) :

Decidable (xs = ys)

Equations

One or more equations did not get rendered due to their size.
Cedar.Spec.decResidualList [] [] = isTrue Cedar.Spec.decResidual._proof_218
Cedar.Spec.decResidualList (head :: tail) [] = isFalse ⋯
Cedar.Spec.decResidualList [] (head :: tail) = isFalse ⋯

Instances For

instance Cedar.Spec.instDecidableEqResidual :

DecidableEq Residual

Equations

Cedar.Spec.instDecidableEqResidual = Cedar.Spec.decResidual

@[irreducible]

def Cedar.Validation.TypedExpr.toResidual :

TypedExpr → Spec.Residual

Equations

One or more equations did not get rendered due to their size.
(Cedar.Validation.TypedExpr.lit p ty).toResidual = Cedar.Spec.Residual.val (Cedar.Spec.Value.prim p) ty
(Cedar.Validation.TypedExpr.var v ty).toResidual = Cedar.Spec.Residual.var v ty
(x₁.ite x₂ x₃ ty).toResidual = x₁.toResidual.ite x₂.toResidual x₃.toResidual ty
(a.and b ty).toResidual = a.toResidual.and b.toResidual ty
(a.or b ty).toResidual = a.toResidual.or b.toResidual ty
(Cedar.Validation.TypedExpr.unaryApp op expr ty).toResidual = Cedar.Spec.Residual.unaryApp op expr.toResidual ty
(Cedar.Validation.TypedExpr.binaryApp op a b ty).toResidual = Cedar.Spec.Residual.binaryApp op a.toResidual b.toResidual ty
(expr.getAttr attr ty).toResidual = expr.toResidual.getAttr attr ty
(expr.hasAttr attr ty).toResidual = expr.toResidual.hasAttr attr ty

Instances For