7. Proving Coverage
There are really two parts to any GL theorem. First, we need to
symbolically execute the goal formula and ensure it cannot evaluate to
nil. But in addition to this, we must ensure that the objects we use to
represent the variables of the theorem cover all the cases that satisfy the
hypothesis. This part of the proof is called the coverage
obligation.
For fast-logcount-32-correct, the coverage obligation is to show that
our binding for x is able to represent every integer from 0 to 2^32 -
1. This is true of Xinit, and the coverage proof goes through
automatically.
But suppose we forget that :g-integers use a signed representation, and
attempt to prove fast-logcount-32-correct using the following (incorrect)
g-bindings.
:g-bindings `((x ,(g-int 0 1 32)))
This looks like a 32-bit integer, but because of the sign bit it does not cover
the intended unsigned range. If we submit the def-gl-thm command
with these bindings, the symbolic execution part of the proof is still successful.
But this execution has only really shown the goal holds for 31-bit unsigned
integers, so def-gl-thm prints the message
ERROR: Coverage proof appears to have failed.
and leaves us with a failed subgoal,
(implies (and (integerp x)
(<= 0 x)
(< x 4294967296))
(< x 2147483648))
This goal is clearly not provable: we are trying to show x must be less
than 2^31 (from our :g-bindings) whenever it is less than
2^32 (from the hypothesis).
Usually when the :g-bindings are correct, the coverage proof will be
automatic, so if you see that a coverage proof has failed, the first thing to
do is check whether your bindings are really sufficient.
On the other hand, proving coverage is undecidable in principle, so
sometimes GL will fail to prove coverage even though the bindings are
appropriate. For these cases, there are some keyword arguments to def-gl-thm that may help coverage proofs succeed.
First, as a practical matter, GL does the symbolic execution part of the
proof before trying to prove coverage. This can get in the way of
debugging coverage proofs when the symbolic execution takes a long time. You
can use :test-side-goals t to have GL skip the symbolic execution and go
straight to the coverage proof. Of course, no defthm is produced when
this option is used.
By default, our coverage proof strategy uses a restricted set of rules and
ignores the current theory. It heuristically expands functions in the
hypothesis and throws away terms that seem irrelevant. When this strategy
fails, it is usually for one of two reasons.
- The heuristics expand too many terms and overwhelm ACL2. GL tries to avoid
this by throwing away irrelevant terms, but sometimes this approach is
insufficient. It may be helpful to disable the expansion of functions that are
not important for proving coverage. The :do-not-expand argument allows
you to list functions that should not be expanded.
- The heuristics throw away a necessary hypothesis, leading to unprovable
goals. GL's coverage proof strategy tries to show that the binding for each
variable is sufficient, one variable at a time. During this process it throws
away hypotheses that do not mention the variable, but in some cases this can be
inappropriate. For instance, suppose the following is a coverage goal for
b:
(implies (and (natp a)
(natp b)
(< a (expt 2 15))
(< b a))
(< b (expt 2 15)))
Here, throwing away the terms that don't mention b will cause the proof to
fail. A good way to avoid this problem is to separate type and size hypotheses
from more complicated assumptions that are not important for proving coverage,
along these lines:
(def-gl-thm my-theorem
:hyp (and (type-assms-1 x)
(type-assms-2 y)
(type-assms-3 z)
(complicated-non-type-assms x y z))
:concl ...
:g-bindings ...
:do-not-expand '(complicated-non-type-assms))
For more control, you can also use the :cov-theory-add argument to
enable additional rules during the coverage proof, e.g., :cov-theory-add
'(type-rule1 type-rule2).
