Documentation

Cedar.Spec.Template

This file defines abstract syntax for Cedar policy templates. In general, Cedar operations (e.g., authorization, validation) are defined over policies rather than templates. We generate policies from templates by using link?. During differential testing, templates are only used during parsing

@[reducible, inline]

abbrev Cedar.Spec.SlotID :

Equations

Cedar.Spec.SlotID = String

Instances For

inductive Cedar.Spec.EntityUIDOrSlot :

entityUID (entity : EntityUID) : EntityUIDOrSlot
slot (id : SlotID) : EntityUIDOrSlot

Instances For

def Cedar.Spec.instReprEntityUIDOrSlot.repr :

EntityUIDOrSlot → Nat → Std.Format

Equations

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

Instances For

instance Cedar.Spec.instReprEntityUIDOrSlot :

Repr EntityUIDOrSlot

Equations

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

instance Cedar.Spec.instDecidableEqEntityUIDOrSlot :

DecidableEq EntityUIDOrSlot

Equations

Cedar.Spec.instDecidableEqEntityUIDOrSlot = Cedar.Spec.instDecidableEqEntityUIDOrSlot.decEq

def Cedar.Spec.instDecidableEqEntityUIDOrSlot.decEq (x✝ x✝¹ : EntityUIDOrSlot) :

Decidable (x✝ = x✝¹)

Equations

Cedar.Spec.instDecidableEqEntityUIDOrSlot.decEq (Cedar.Spec.EntityUIDOrSlot.entityUID a) (Cedar.Spec.EntityUIDOrSlot.entityUID b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Cedar.Spec.instDecidableEqEntityUIDOrSlot.decEq (Cedar.Spec.EntityUIDOrSlot.entityUID entity) (Cedar.Spec.EntityUIDOrSlot.slot id) = isFalse ⋯
Cedar.Spec.instDecidableEqEntityUIDOrSlot.decEq (Cedar.Spec.EntityUIDOrSlot.slot id) (Cedar.Spec.EntityUIDOrSlot.entityUID entity) = isFalse ⋯
Cedar.Spec.instDecidableEqEntityUIDOrSlot.decEq (Cedar.Spec.EntityUIDOrSlot.slot a) (Cedar.Spec.EntityUIDOrSlot.slot b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

inductive Cedar.Spec.ScopeTemplate :

any : ScopeTemplate
eq (entityOrSlot : EntityUIDOrSlot) : ScopeTemplate
mem (entityOrSlot : EntityUIDOrSlot) : ScopeTemplate
is (ety : EntityType) : ScopeTemplate
isMem (ety : EntityType) (entityOrSlot : EntityUIDOrSlot) : ScopeTemplate

Instances For

def Cedar.Spec.instReprScopeTemplate.repr :

ScopeTemplate → Nat → Std.Format

Equations

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

Instances For

instance Cedar.Spec.instReprScopeTemplate :

Repr ScopeTemplate

Equations

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

instance Cedar.Spec.instDecidableEqScopeTemplate :

DecidableEq ScopeTemplate

Equations

Cedar.Spec.instDecidableEqScopeTemplate = Cedar.Spec.instDecidableEqScopeTemplate.decEq

def Cedar.Spec.instDecidableEqScopeTemplate.decEq (x✝ x✝¹ : ScopeTemplate) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Cedar.Spec.instDecidableEqScopeTemplate.decEq Cedar.Spec.ScopeTemplate.any Cedar.Spec.ScopeTemplate.any = isTrue ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq Cedar.Spec.ScopeTemplate.any (Cedar.Spec.ScopeTemplate.eq entityOrSlot) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq Cedar.Spec.ScopeTemplate.any (Cedar.Spec.ScopeTemplate.mem entityOrSlot) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq Cedar.Spec.ScopeTemplate.any (Cedar.Spec.ScopeTemplate.is ety) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq Cedar.Spec.ScopeTemplate.any (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.eq entityOrSlot) Cedar.Spec.ScopeTemplate.any = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.eq a) (Cedar.Spec.ScopeTemplate.eq b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.eq entityOrSlot) (Cedar.Spec.ScopeTemplate.mem entityOrSlot_1) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.eq entityOrSlot) (Cedar.Spec.ScopeTemplate.is ety) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.eq entityOrSlot) (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot_1) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.mem entityOrSlot) Cedar.Spec.ScopeTemplate.any = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.mem entityOrSlot) (Cedar.Spec.ScopeTemplate.eq entityOrSlot_1) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.mem a) (Cedar.Spec.ScopeTemplate.mem b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.mem entityOrSlot) (Cedar.Spec.ScopeTemplate.is ety) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.mem entityOrSlot) (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot_1) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.is ety) Cedar.Spec.ScopeTemplate.any = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.is ety) (Cedar.Spec.ScopeTemplate.eq entityOrSlot) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.is ety) (Cedar.Spec.ScopeTemplate.mem entityOrSlot) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.is a) (Cedar.Spec.ScopeTemplate.is b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.is ety) (Cedar.Spec.ScopeTemplate.isMem ety_1 entityOrSlot) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot) Cedar.Spec.ScopeTemplate.any = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot) (Cedar.Spec.ScopeTemplate.eq entityOrSlot_1) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot) (Cedar.Spec.ScopeTemplate.mem entityOrSlot_1) = isFalse ⋯
Cedar.Spec.instDecidableEqScopeTemplate.decEq (Cedar.Spec.ScopeTemplate.isMem ety entityOrSlot) (Cedar.Spec.ScopeTemplate.is ety_1) = isFalse ⋯

Instances For

inductive Cedar.Spec.PrincipalScopeTemplate :

principalScope (scope : ScopeTemplate) : PrincipalScopeTemplate

Instances For

def Cedar.Spec.instReprPrincipalScopeTemplate.repr :

PrincipalScopeTemplate → Nat → Std.Format

Equations

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

Instances For

instance Cedar.Spec.instReprPrincipalScopeTemplate :

Repr PrincipalScopeTemplate

Equations

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

def Cedar.Spec.instDecidableEqPrincipalScopeTemplate.decEq (x✝ x✝¹ : PrincipalScopeTemplate) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Cedar.Spec.instDecidableEqPrincipalScopeTemplate :

DecidableEq PrincipalScopeTemplate

Equations

Cedar.Spec.instDecidableEqPrincipalScopeTemplate = Cedar.Spec.instDecidableEqPrincipalScopeTemplate.decEq

inductive Cedar.Spec.ResourceScopeTemplate :

resourceScope (scope : ScopeTemplate) : ResourceScopeTemplate

Instances For

def Cedar.Spec.instReprResourceScopeTemplate.repr :

ResourceScopeTemplate → Nat → Std.Format

Equations

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

Instances For

instance Cedar.Spec.instReprResourceScopeTemplate :

Repr ResourceScopeTemplate

Equations

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

instance Cedar.Spec.instDecidableEqResourceScopeTemplate :

DecidableEq ResourceScopeTemplate

Equations

Cedar.Spec.instDecidableEqResourceScopeTemplate = Cedar.Spec.instDecidableEqResourceScopeTemplate.decEq

def Cedar.Spec.instDecidableEqResourceScopeTemplate.decEq (x✝ x✝¹ : ResourceScopeTemplate) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[reducible, inline]

abbrev Cedar.Spec.TemplateID :

Equations

Cedar.Spec.TemplateID = String

Instances For

structure Cedar.Spec.Template :

effect : Effect
principalScope : PrincipalScopeTemplate
actionScope : ActionScope
resourceScope : ResourceScopeTemplate
condition : Conditions

Instances For

instance Cedar.Spec.instReprTemplate :

Equations

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

def Cedar.Spec.instReprTemplate.repr :

Template → Nat → Std.Format

Equations

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

Instances For

def Cedar.Spec.instDecidableEqTemplate.decEq (x✝ x✝¹ : Template) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Cedar.Spec.instDecidableEqTemplate :

DecidableEq Template

Equations

Cedar.Spec.instDecidableEqTemplate = Cedar.Spec.instDecidableEqTemplate.decEq

@[reducible, inline]

abbrev Cedar.Spec.Templates :

Equations

Cedar.Spec.Templates = Cedar.Data.Map Cedar.Spec.TemplateID Cedar.Spec.Template

Instances For

@[reducible, inline]

abbrev Cedar.Spec.SlotEnv :

Equations

Cedar.Spec.SlotEnv = Cedar.Data.Map Cedar.Spec.SlotID Cedar.Spec.EntityUID

Instances For

def Cedar.Spec.SlotEnv.empty :

Equations

Cedar.Spec.SlotEnv.empty = Cedar.Data.Map.empty

Instances For

structure Cedar.Spec.TemplateLinkedPolicy :

id : PolicyID
ID of the link, which for static policies will match the templateId
templateId : TemplateID
ID of the template, which for static policies will match the id
slotEnv : SlotEnv

Instances For

instance Cedar.Spec.instReprTemplateLinkedPolicy :

Repr TemplateLinkedPolicy

Equations

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

def Cedar.Spec.instReprTemplateLinkedPolicy.repr :

TemplateLinkedPolicy → Nat → Std.Format

Equations

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

Instances For

@[reducible, inline]

abbrev Cedar.Spec.TemplateLinkedPolicies :

Equations

Cedar.Spec.TemplateLinkedPolicies = List Cedar.Spec.TemplateLinkedPolicy

Instances For

def Cedar.Spec.Template.link? (template : Template) (id : PolicyID) (slotEnv : SlotEnv) :

Except String Policy

Equations

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

Instances For

def Cedar.Spec.link? (templates : Templates) (links : TemplateLinkedPolicies) :

Except String Policies

Equations

Cedar.Spec.link? templates links = List.mapM (Cedar.Spec.linkPolicy?✝ templates) links

Instances For