This file defines the algorithm for emitting well-formedness assumptions about Cedar hierarchies. A valid Cedar hierarchy graph is the irreflexive transitive closure of a DAG. (Note that the in operator is reflexive, but this is enforced separately by the semantics, and it's not needed in the hierarchy.)

The generated assumptions are expressed as Terms that enforce the acyclicty and transitivity constraints on the symbolic store, for a given Cedar expression.

The grounding relies on the fact that a Cedar expression can reference only a finite number of entities (so the domain of the quantification is finite), and we can compute an overapproximation of that set by statically analyzing the expression. We call this set the footprint of the expression x, and it consists of all subexpressions of x that could have an Entity type. The grounding procedure computes the footprint, and grounds the acyclicity and transitivity constraints on the set of entity terms in the footprint.

@[irreducible]

def Cedar.SymCC.footprint (x : Spec.Expr) (εnv : SymEnv) : Data.Set Term

Returns the terms corresponding to subexpressions of x of the following form:

• A variable term with an entity type
• An entity reference literal
• An attribute access expression with an entity type
• A binary (getTag) expression with an entity type

These are the only basic expressions in Cedar that may evaluate to an entity. All other expressions that evaluate to an entity are build up from the above basic expresions.

All returned terms are of type TermType.option .entity.

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.footprint (Cedar.Spec.Expr.lit p) εnv = Cedar.SymCC.footprint.ofEntity (Cedar.Spec.Expr.lit p) εnv
• Cedar.SymCC.footprint (Cedar.Spec.Expr.var v) εnv = Cedar.SymCC.footprint.ofEntity (Cedar.Spec.Expr.var v) εnv
• Cedar.SymCC.footprint (x₁.ite x₂ x₃) εnv = Cedar.SymCC.footprint.ofBranch εnv x₁ (Cedar.SymCC.footprint x₁ εnv) (Cedar.SymCC.footprint x₂ εnv) (Cedar.SymCC.footprint x₃ εnv)
• Cedar.SymCC.footprint (x₁.and x₂) εnv = Cedar.SymCC.footprint.ofBranch εnv x₁ (Cedar.SymCC.footprint x₁ εnv) (Cedar.SymCC.footprint x₂ εnv) Cedar.Data.Set.empty
• Cedar.SymCC.footprint (x₁.or x₂) εnv = Cedar.SymCC.footprint.ofBranch εnv x₁ (Cedar.SymCC.footprint x₁ εnv) Cedar.Data.Set.empty (Cedar.SymCC.footprint x₂ εnv)
• Cedar.SymCC.footprint (x₁.getAttr attr) εnv = Cedar.SymCC.footprint.ofEntity (x₁.getAttr attr) εnv ∪ Cedar.SymCC.footprint x₁ εnv
• Cedar.SymCC.footprint (x₁.hasAttr attr) εnv = Cedar.SymCC.footprint x₁ εnv
• Cedar.SymCC.footprint (Cedar.Spec.Expr.unaryApp op x₁) εnv = Cedar.SymCC.footprint x₁ εnv
• Cedar.SymCC.footprint (Cedar.Spec.Expr.call xfn xs) εnv = xs.mapUnion₁ fun (x : { x : Cedar.Spec.Expr // x ∈ xs }) => match x with | ⟨xᵢ, property⟩ => Cedar.SymCC.footprint xᵢ εnv
• Cedar.SymCC.footprint (Cedar.Spec.Expr.set xs) εnv = xs.mapUnion₁ fun (x : { x : Cedar.Spec.Expr // x ∈ xs }) => match x with | ⟨xᵢ, property⟩ => Cedar.SymCC.footprint xᵢ εnv

def Cedar.SymCC.footprint.ofEntity (x : Spec.Expr) (εnv : SymEnv) : Data.Set Term

Equations

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

def Cedar.SymCC.footprint.ofBranch (εnv : SymEnv) (x₁ : Spec.Expr) (ft₁ ft₂ ft₃ : Data.Set Term) : Data.Set Term

Equations

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

def Cedar.SymCC.footprints (xs : List Spec.Expr) (εnv : SymEnv) : Data.Set Term

Returns the set of Terms corresponding to the footprints of xs.

Equations

• Cedar.SymCC.footprints xs εnv = List.mapUnion (fun (x : Cedar.Spec.Expr) => Cedar.SymCC.footprint x εnv) xs

def Cedar.SymCC.acyclicity (t : Term) (εs : SymEntities) : Term

Returns the acyclicity constraint for the given term.

Equations

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

def Cedar.SymCC.transitivity (t₁ t₂ : Term) (εs : SymEntities) : Term

Returns the transitivity constraint for the given term.

Equations

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

def Cedar.SymCC.transitivity.isAncestor (t₁ t₂ t₂' t₁' : Term) (f₁₂ : UnaryFunction) : Term

Equations

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

def Cedar.SymCC.transitivity.areAncestorsOfType (εs : SymEntities) (t₂' : Term) (f₂₃ : UnaryFunction) (ety₃ : Spec.EntityType) (t₁' : Term) (ety₁ : Spec.EntityType) : Term

Equations

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

def Cedar.SymCC.transitivity.areAncestors (εs : SymEntities) (t₂' : Term) (anc₂ : Data.Map Spec.EntityType UnaryFunction) (t₁' : Term) (ety₁ : Spec.EntityType) : Term

Equations

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

def Cedar.SymCC.enforce (xs : List Spec.Expr) (εnv : SymEnv) : Data.Set Term

Returns the ground acyclicity and transitivity assumptions for xs and env.

Equations

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