Given compiled policies cpss and some asserts, 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 cpss in env violates the property verified
by asserts.
The asserts are expected to be well-formed with respect to the εnv which
cpss where compiled for, according to Cedar.SymCC.Term.WellFormed.
(Caller guarantees that all of the cpss were compiled for the same εnv.)
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, where ps are the
(post-typecheck) policies that were compiled to cpss, 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.
- Cedar.SymCC.satAssertsOpt? [] asserts = throw (IO.userError (toString "satAssertsOpt? called with empty list of policies"))