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 = ∅

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

Executable check deciding whether es is closed at a level for request r: every entity reachable from the request roots within level dereferences is present in es. It reuses the reachable-entity set computed by the slicing algorithm (Entities.sliceAtLevel.sliceAtLevel, which collects every entity reachable in level hops, whether or not it is present) and checks that each is actually in the store.

Cedar.Thm.closedAtLevel_iff proves this returns true exactly when the EntitiesClosedAtLevel predicate holds, so a Cedar user can run this to obtain the issue-#642 guarantee: a level-validated policy set evaluated against a store passing this check never errors with entityDoesNotExist.

Equations

• es.closedAtLevel r level = Cedar.Data.Set.all (Cedar.Data.Map.contains es) (Cedar.Spec.Entities.sliceAtLevel.sliceAtLevel es r.sliceEUIDs level)