Copyright | (c) Ben Selfridge 2020 |
---|---|
Maintainer | benselfridge@galois.com |
Stability | experimental |
Portability | POSIX |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Spec properties are translated into the language of SMT solvers using
What4
. A backend solver is then used to prove the property is true. The
technique is sound, but incomplete. If a property is proved true by this
technique, then it can be guaranteed to be true. However, if a property is
not proved true, that does not mean it isn't true. Very simple specifications
are unprovable by this technique, including:
a = True : a
The above specification will not be proved true. The reason is that this
technique does not perform any sort of induction. When proving the inner a
expression, the technique merely allocates a fresh constant standing for
"a
, one timestep in the past." Nothing is asserted about the fresh
constant.
An example of a property that is provable by this approach is:
a = True : b b = not a -- Property: a || b
By allocating a fresh constant, b_-1
, standing for "the value of b
one
timestep in the past", the equation for a || b
at some arbitrary point in
the future reduces to b_-1 || not b_-1
, which is always true.
In addition to proving that the stream expression is true at some arbitrary
point in the future, we also prove it for the first k
timesteps, where k
is the maximum buffer length of all streams in the given spec. This amounts
to simply interpreting the spec, although external variables are still
represented as constants with unknown values.
Documentation
Attempt to prove all of the properties in a spec via an SMT solver (which must be installed locally on the host). Return an association list mapping the names of each property to the result returned by the solver.