This file defines entity slicing at a level

@[irreducible]

def Cedar.Spec.Value.sliceEUIDs : Value → Data.Set EntityUID

Equations

• (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)).sliceEUIDs = Cedar.Data.Set.singleton uid
• (Cedar.Spec.Value.record (Cedar.Data.Map.mk avs)).sliceEUIDs = avs.mapUnion₃ fun (e : { x : Cedar.Spec.Attr × Cedar.Spec.Value // sizeOf x.snd < 1 + (1 + sizeOf avs) }) => e.val.snd.sliceEUIDs
• (Cedar.Spec.Value.prim p).sliceEUIDs = ∅
• (Cedar.Spec.Value.set s).sliceEUIDs = ∅
• (Cedar.Spec.Value.ext x_1).sliceEUIDs = ∅

def Cedar.Spec.EntityData.sliceEUIDs (ed : EntityData) : Data.Set EntityUID

Equations

• ed.sliceEUIDs = List.mapUnion Cedar.Spec.Value.sliceEUIDs ed.attrs.values ∪ List.mapUnion Cedar.Spec.Value.sliceEUIDs ed.tags.values

def Cedar.Spec.Request.sliceEUIDs (r : Request) : Data.Set EntityUID

Equations

• r.sliceEUIDs = Cedar.Data.Set.make [r.principal, r.action, r.resource] ∪ (Cedar.Spec.Value.record r.context).sliceEUIDs

def Cedar.Spec.Entities.sliceAtLevel (es : Entities) (r : Request) (level : Nat) : Entities

Equations

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

def Cedar.Spec.Entities.sliceAtLevel.sliceAtLevel (es : Entities) (work : Data.Set EntityUID) : Nat → Data.Set EntityUID

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.Entities.sliceAtLevel.sliceAtLevel es work 0 = ∅