There are really two parts to any GL theorem. First, we need to
symbolically execute the goal formula and ensure it cannot evaluate to
**coverage
obligation**.

For

But suppose we forget that

: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

Usually when the

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

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 mentionb 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