Extracting strongly well-formed counterexamples to verification queries

This file defines the function extract?, which turns interpretations into concrete, strongly well-formed counterexamples to verification queries.

The function takes as input a list of expressions xs, an interpretation I, and a symbolic environment εnv. Given these inputs, it returns an environment env ∈ εnv such that env is strongly well-formed, and each term in footprint xs εnv has the same interpretation under both I and every I' for which f env ∼ εnv.interpret I'.

If I is the result of solving a verify* query (see Cedar.SymCC.Verifier), then εnv.extract? xs I is a valid strongly well-formed counterexample to that query. More generally, εnv.extract? xs I extracts such a counterexample for any verification query that is expressed as a boolean combination of (boolean) terms obtained by compiling xs with respect to εnv.

See Cedar.Thm.SymCC.Verification for how this is used to prove that verification queries based on Cedar's compiler and hierarchy enforcer are correct.

def Cedar.SymCC.UnaryFunction.uuf? : UnaryFunction → Option UUF

Equations

• (Cedar.SymCC.UnaryFunction.uuf f).uuf? = some f
• x✝.uuf? = none

def Cedar.SymCC.SymEntityData.uufAncestors (δ : SymEntityData) : Data.Set UUF

Equations

• δ.uufAncestors = Cedar.Data.Set.make (List.filterMap (Cedar.SymCC.UnaryFunction.uuf? ∘ Prod.snd) δ.ancestors.toList)

def Cedar.SymCC.SymEntities.uufAncestors (εs : SymEntities) : Data.Set UUF

Equations

• εs.uufAncestors = List.mapUnion (Cedar.SymCC.SymEntityData.uufAncestors ∘ Prod.snd) (Cedar.Data.Map.toList εs)

def Cedar.SymCC.UUF.repairAncestors (fts : Data.Set Spec.EntityUID) (I : Interpretation) (f : UUF) : UDF

Equations

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

def Cedar.SymCC.UUF.repairAncestors.entry (udf : UDF) (uid : Spec.EntityUID) : Option (Term × Term)

Equations

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

def Cedar.SymCC.UUF.repairAncestors.table (fts : Data.Set Spec.EntityUID) (udf : UDF) : Data.Map Term Term

Equations

• Cedar.SymCC.UUF.repairAncestors.table fts udf = Cedar.Data.Map.mk (List.filterMap (Cedar.SymCC.UUF.repairAncestors.entry udf) fts.elts)

def Cedar.SymCC.UUF.repairAncestors.default (udf : UDF) : Term

Equations

• Cedar.SymCC.UUF.repairAncestors.default udf = match udf.out with | ty.set => Cedar.SymCC.Term.set Cedar.Data.Set.empty ty | x => udf.default

def Cedar.SymCC.Interpretation.repair (footprint : Data.Set Term) (εnv : SymEnv) (I : Interpretation) : Interpretation

Equations

• Cedar.SymCC.Interpretation.repair footprint εnv I = { vars := I.vars, funs := Cedar.SymCC.Interpretation.repair.funs footprint εnv I, partials := I.partials }

def Cedar.SymCC.Interpretation.repair.footprintUIDs (footprint : Data.Set Term) (I : Interpretation) : Data.Set Spec.EntityUID

Equations

• Cedar.SymCC.Interpretation.repair.footprintUIDs footprint I = List.mapUnion (Cedar.SymCC.Term.entityUIDs ∘ Cedar.SymCC.Term.interpret I) footprint.elts

def Cedar.SymCC.Interpretation.repair.footprintAncestors (footprint : Data.Set Term) (εnv : SymEnv) (I : Interpretation) : Data.Map UUF UDF

Equations

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

def Cedar.SymCC.Interpretation.repair.funs (footprint : Data.Set Term) (εnv : SymEnv) (I : Interpretation) : UUF → UDF

Equations

• Cedar.SymCC.Interpretation.repair.funs footprint εnv I f = match (Cedar.SymCC.Interpretation.repair.footprintAncestors footprint εnv I).find? f with | some udf => udf | x => I.funs f

def Cedar.SymCC.SymEnv.extract? (xs : List Spec.Expr) (I : Interpretation) (εnv : SymEnv) : Option Spec.Env

Equations

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