def Cedar.SymCC.checkSatAsserts (asserts : Asserts) (εnv : SymEnv) : SolverM (Option Interpretation)

Given some asserts and their corresponding symbolic environment εnv, calls the SMT solver (if necessary) on an SMTLib encoding of asserts and returns none if the result is unsatisfiable. Otherwise returns some I containing a counterexample interpretation I. The asserts are expected to be well-formed with respect to εnv according to Cedar.SymCC.Term.WellFormed. This call resets the solver.

Equations

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

def Cedar.SymCC.satAsserts? (ps : Spec.Policies) (asserts : Asserts) (εnv : SymEnv) : SolverM (Option Spec.Env)

Given policies ps (in their post-typecheck forms), some asserts, and the corresponding symbolic environment εnv, calls the SMT solver (if necessary) on an SMTLib encoding of asserts and returns none if the result is unsatisfiable. Otherwise returns some env containing a counterexample environment such that evaluating ps in env violates the property verified by asserts.

The asserts are expected to be well-formed with respect to εnv according to Cedar.SymCC.Term.WellFormed. They must encode a property of policies pc. Specifically, for each term t ∈ asserts, there must be a set of expressions xs such that each x ∈ xs is a subexpression of p ∈ ps, and the meaning of t is a function of the meaning of xs. This ensures that findings generated by solve are sound and complete.

Equations

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

def Cedar.SymCC.sat? (ps : Spec.Policies) (vc : SymEnv → Result Asserts) (εnv : SymEnv) : SolverM (Option Spec.Env)

Given policies ps, a verification condition generator vc, and a symbolic environment εnv, calls the SMT solver (if necessary) on an SMTLib encoding of vc εnv and returns none if the result is unsatisfiable. Otherwise returns some env containing a counterexample environment such that evaluating ps in env violates the property verified by vc.

The function vc is expected to produce a list of terms type .bool that are well-formed with respect to εnv according to Cedar.SymCC.Term.WellFormed. These terms must encode a property of policies pc. Specifically, for each term t ∈ vc εnv, there must be a set of expressions xs such that each x ∈ xs is a subexpression of p ∈ ps, and the meaning of t is a function of the meaning of xs. This ensures that findings generated by solve are sound and complete.

This call resets the solver.

Equations

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

def Cedar.SymCC.checkUnsatAsserts (asserts : Asserts) (εnv : SymEnv) : SolverM Bool

Given some asserts and their corresponding symbolic environment εnv, calls the SMT solver (if necessary) on an SMTLib encoding of asserts and returns true iff the result is unsatisfiable. The asserts are expected to be well-formed with respect to εnv according to Cedar.SymCC.Term.WellFormed. This call resets the solver.

Equations

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

def Cedar.SymCC.checkUnsat (vc : SymEnv → Result Asserts) (εnv : SymEnv) : SolverM Bool

Given a verification condition generator vc and a symbolic environment εnv, calls the SMT solver (if necessary) on an SMTLib encoding of vc εnv and returns true iff the result is unsatisfiable. The function vc is expected to produce a list of terms type .bool that are well-formed with respect to εnv according to Cedar.SymCC.Term.WellFormed. This call resets the solver.

Equations

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