Concretizing symbolic environments

This file defines functions for concretizing a literal symbolic environment (SymEnv) into a corresponding concrete environment (Env). This functionality is needed for extracting counterexamples from models returned by the solver and also for proving that Cedar's reduction to SMT (Cedar.SymCC.compile) is complete.

See Cedar.Thm.SymbolicCompilation for a statement of the completeness theorem.

def Cedar.Spec.Prim.entityUIDs : Prim → Data.Set EntityUID

Equations

• (Cedar.Spec.Prim.entityUID uid).entityUIDs = Cedar.Data.Set.singleton uid
• x✝.entityUIDs = Cedar.Data.Set.empty

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Spec.Value.prim p).entityUIDs = p.entityUIDs
• (Cedar.Spec.Value.set (Cedar.Data.Set.mk vs)).entityUIDs = vs.mapUnion₁ fun (x : { x : Cedar.Spec.Value // x ∈ vs }) => match x with | ⟨v, property⟩ => v.entityUIDs
• (Cedar.Spec.Value.ext x_1).entityUIDs = Cedar.Data.Set.empty

def Cedar.Spec.Value.entityUID? : Value → Option EntityUID

Equations

• (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)).entityUID? = some uid
• x✝.entityUID? = none

def Cedar.Spec.Value.record? : Value → Option (Data.Map Attr Value)

Equations

• (Cedar.Spec.Value.record r).record? = some r
• x✝.record? = none

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

Equations

• r.entityUIDs = Cedar.Data.Set.singleton r.principal ∪ Cedar.Data.Set.singleton r.action ∪ Cedar.Data.Set.singleton r.resource ∪ (Cedar.Spec.Value.record r.context).entityUIDs

def Cedar.Spec.EntityData.entityUIDs (d : EntityData) : Data.Set EntityUID

Equations

• d.entityUIDs = d.ancestors ∪ (Cedar.Spec.Value.record d.attrs).entityUIDs ∪ (Cedar.Spec.Value.record d.tags).entityUIDs

def Cedar.Spec.Entities.entityUIDs (es : Entities) : Data.Set EntityUID

Equations

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

structure Cedar.Spec.Env : Type

• request : Request
• entities : Entities

instance Cedar.Spec.instReprEnv : Repr Env

Equations

• Cedar.Spec.instReprEnv = { reprPrec := Cedar.Spec.instReprEnv.repr }

def Cedar.Spec.instReprEnv.repr : Env → Nat → Std.Format

Equations

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

def Cedar.Spec.instDecidableEqEnv.decEq (x✝ x✝¹ : Env) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqEnv.decEq { request := a, entities := a_1 } { request := b, entities := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Cedar.Spec.instDecidableEqEnv : DecidableEq Env

Equations

• Cedar.Spec.instDecidableEqEnv = Cedar.Spec.instDecidableEqEnv.decEq

def Cedar.Spec.Env.entityUIDs (env : Env) : Data.Set EntityUID

Equations

• env.entityUIDs = env.request.entityUIDs ∪ env.entities.entityUIDs

@[irreducible]

def Cedar.Spec.Expr.entityUIDs : Expr → Data.Set EntityUID

Equations

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

def Cedar.SymCC.BitVec.int64? {n : Nat} (bv : BitVec n) : Option Int64

Equations

• Cedar.SymCC.BitVec.int64? bv = if n = 64 then some (Int64.ofInt bv.toInt) else none

def Cedar.SymCC.TermPrim.value? : TermPrim → Option Spec.Value

Equations

• (Cedar.SymCC.TermPrim.bool b).value? = some (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b))
• (Cedar.SymCC.TermPrim.bitvec bv).value? = do let a ← Cedar.SymCC.BitVec.int64? bv pure (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int a))
• (Cedar.SymCC.TermPrim.string s).value? = some (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s))
• (Cedar.SymCC.TermPrim.entity uid).value? = some (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid))
• (Cedar.SymCC.TermPrim.ext xv).value? = some (Cedar.Spec.Value.ext xv)

@[irreducible]

def Cedar.SymCC.Term.value? : Term → Option Spec.Value

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.SymCC.Term.prim p).value? = p.value?
• x✝.value? = none

@[irreducible]

def Cedar.SymCC.Term.value?.attrValue? (a : Spec.Attr) : Term → Option (Spec.Attr × Option Spec.Value)

Equations

• Cedar.SymCC.Term.value?.attrValue? a t.some = do let __do_lift ← t.value? some (a, some __do_lift)
• Cedar.SymCC.Term.value?.attrValue? a (Cedar.SymCC.Term.none a_1) = some (a, none)
• Cedar.SymCC.Term.value?.attrValue? a x✝ = do let __do_lift ← x✝.value? some (a, some __do_lift)

def Cedar.SymCC.Term.recordValue? (t : Term) : Option (Data.Map Spec.Attr Spec.Value)

Equations

• t.recordValue? = t.value? >>= Cedar.Spec.Value.record?

def Cedar.SymCC.TermPrim.entityUIDs : TermPrim → Data.Set Spec.EntityUID

Equations

• (Cedar.SymCC.TermPrim.entity uid).entityUIDs = Cedar.Data.Set.singleton uid
• x✝.entityUIDs = Cedar.Data.Set.empty

@[irreducible]

def Cedar.SymCC.Term.entityUIDs : Term → Data.Set Spec.EntityUID

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.SymCC.Term.var a).entityUIDs = Cedar.Data.Set.empty
• (Cedar.SymCC.Term.none a).entityUIDs = Cedar.Data.Set.empty
• (Cedar.SymCC.Term.prim p).entityUIDs = p.entityUIDs
• t.some.entityUIDs = t.entityUIDs
• (Cedar.SymCC.Term.set ts eltsTy).entityUIDs = ts.elts.mapUnion₁ fun (x : { x : Cedar.SymCC.Term // x ∈ ts.elts }) => match x with | ⟨t, property⟩ => t.entityUIDs
• (Cedar.SymCC.Term.app a ts retTy).entityUIDs = ts.mapUnion₁ fun (x : { x : Cedar.SymCC.Term // x ∈ ts }) => match x with | ⟨t, property⟩ => t.entityUIDs

def Cedar.SymCC.Term.entityUID? : Term → Option Spec.EntityUID

Equations

• (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.entity uid)).entityUID? = some uid
• x✝.entityUID? = none

def Cedar.SymCC.Term.setOfEntityUIDs? : Term → Option (Data.Set Spec.EntityUID)

Equations

• (Cedar.SymCC.Term.set (Cedar.Data.Set.mk ts) eltsTy).setOfEntityUIDs? = do let __do_lift ← List.mapM Cedar.SymCC.Term.entityUID? ts some (Cedar.Data.Set.make __do_lift)
• x✝.setOfEntityUIDs? = none

def Cedar.SymCC.Term.tag? : Term → Option Spec.Tag

Equations

• (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.string tag)).tag? = some tag
• x✝.tag? = none

def Cedar.SymCC.Term.setOfTags? : Term → Option (Data.Set Spec.Tag)

Equations

• (Cedar.SymCC.Term.set (Cedar.Data.Set.mk ts) eltsTy).setOfTags? = do let __do_lift ← List.mapM Cedar.SymCC.Term.tag? ts some (Cedar.Data.Set.make __do_lift)
• x✝.setOfTags? = none

def Cedar.SymCC.SymRequest.entityUIDs (ρ : SymRequest) : Data.Set Spec.EntityUID

Equations

• ρ.entityUIDs = ρ.principal.entityUIDs ∪ ρ.action.entityUIDs ∪ ρ.resource.entityUIDs ∪ ρ.context.entityUIDs

def Cedar.SymCC.UDF.entityUIDs (f : UDF) : Data.Set Spec.EntityUID

Equations

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

def Cedar.SymCC.UnaryFunction.entityUIDs : UnaryFunction → Data.Set Spec.EntityUID

Equations

• (Cedar.SymCC.UnaryFunction.uuf a).entityUIDs = Cedar.Data.Set.empty
• (Cedar.SymCC.UnaryFunction.udf f).entityUIDs = f.entityUIDs

def Cedar.SymCC.SymEntityData.entityUIDs (ety : Spec.EntityType) (δ : SymEntityData) : Data.Set Spec.EntityUID

Equations

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

def Cedar.SymCC.SymEntityData.entityUIDs.mems (ety : Spec.EntityType) (δ : SymEntityData) : Data.Set Spec.EntityUID

Equations

• Cedar.SymCC.SymEntityData.entityUIDs.mems ety δ = match δ.members with | none => Cedar.Data.Set.empty | some eids => Cedar.Data.Set.make (List.map (Cedar.Spec.EntityUID.mk ety) eids.elts)

def Cedar.SymCC.SymEntityData.entityUIDs.attrs (δ : SymEntityData) : Data.Set Spec.EntityUID

Equations

• Cedar.SymCC.SymEntityData.entityUIDs.attrs δ = δ.attrs.entityUIDs

def Cedar.SymCC.SymEntityData.entityUIDs.ancs (δ : SymEntityData) : Data.Set Spec.EntityUID

Equations

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

def Cedar.SymCC.SymEntityData.entityUIDs.tags (δ : SymEntityData) : Data.Set Spec.EntityUID

Equations

• Cedar.SymCC.SymEntityData.entityUIDs.tags δ = match δ.tags with | none => Cedar.Data.Set.empty | some τs => τs.vals.entityUIDs

def Cedar.SymCC.SymEntities.entityUIDs (εs : SymEntities) : Data.Set Spec.EntityUID

Equations

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

def Cedar.SymCC.SymEnv.entityUIDs (εnv : SymEnv) : Data.Set Spec.EntityUID

Equations

• εnv.entityUIDs = εnv.request.entityUIDs ∪ εnv.entities.entityUIDs

def Cedar.SymCC.SymRequest.concretize? (ρ : SymRequest) : Option Spec.Request

Equations

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

def Cedar.SymCC.SymEntityData.concretize? (uid : Spec.EntityUID) (δ : SymEntityData) : Option Spec.EntityData

Equations

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

def Cedar.SymCC.SymEntityData.concretize?.isValidEntityUID (uid : Spec.EntityUID) (δ : SymEntityData) : Bool

Equations

• Cedar.SymCC.SymEntityData.concretize?.isValidEntityUID uid δ = match δ.members with | some eids => eids.contains uid.eid | x => true

def Cedar.SymCC.SymEntityData.concretize?.taggedValueFor (τs : SymTags) (tuid : Term) (tag : Spec.Tag) : Option (Spec.Tag × Spec.Value)

Equations

• Cedar.SymCC.SymEntityData.concretize?.taggedValueFor τs tuid tag = do let __do_lift ← (τs.getTag! tuid (Cedar.SymCC.Term.string tag)).value? some (tag, __do_lift)

def Cedar.SymCC.SymEntityData.concretize?.tags (δ : SymEntityData) (tuid : Term) : Option (Data.Map Spec.Tag Spec.Value)

Equations

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

def Cedar.SymCC.SymEntities.concretize? (uids : Data.Set Spec.EntityUID) (εs : SymEntities) : Option Spec.Entities

Equations

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

def Cedar.SymCC.SymEntities.concretize?.entityData? (εs : SymEntities) (uid : Spec.EntityUID) : Option (Spec.EntityUID × Spec.EntityData)

Equations

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

def Cedar.SymCC.SymEnv.concretize? (x : Spec.Expr) (εnv : SymEnv) : Option Spec.Env

Equations

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