		Search-engine friendly clone of the ACL2 documentation.

Optimization

Case-splitting

BDD performance can sometimes be improved by breaking a problem into subcases. The standard example is floating-point addition, which benefits from separating the problem into cases based on the difference between the two inputs' exponents. (See for instance work by Chen and Bryant and Aagard, Jones, and Seger.)

For each exponent difference, the two mantissas are aligned differently before being added together, so a different BDD order is necessary to interleave their bits at the right offset. Without case splitting, a single BDD ordering has to be used for the whole problem; no matter what ordering we choose, the mantissas will be poorly interleaved for some exponent differences, causing severe performance problems. Separating the cases allows the appropriate order to be used for each difference.

GL provides a def-gl-param-thm command that supports this technique. This command splits the goal formula into several subgoals and attempts to prove each of them using the def-gl-thm approach, so for each subgoal there is a symbolic execution step and coverage proof. To show the subgoals suffice to prove the goal formula, it also does another def-gl-thm-style proof that establishes that any inputs satisfying the hypothesis are covered by some case.

A First Example

Here is how we might split the proof for fast-logcount-32 into five subgoals. One goal handles the case where the most significant bit is 1. The other four goals assume the most significant bit is 0, and separately handle the cases where the lower two bits are 0, 1, 2, or 3. Each case has a different symbolic binding for x, giving the BDD variable order. Of course, splitting into cases and varying the BDD ordering is unnecessary for this theorem, but it illustrates how the def-gl-param-thm command works.

(def-gl-param-thm fast-logcount-32-correct-alt
  :hyp (unsigned-byte-p 32 x)
  :concl (equal (fast-logcount-32 x)
                (logcount x))
  :param-bindings
  `((((msb 1) (low nil)) ((x ,(g-int 32 -1 33))))
    (((msb 0) (low 0))   ((x ,(g-int  0  1 33))))
    (((msb 0) (low 1))   ((x ,(g-int  5  1 33))))
    (((msb 0) (low 2))   ((x ,(g-int  0  2 33))))
    (((msb 0) (low 3))   ((x ,(g-int  3  1 33)))))
  :param-hyp (and (equal msb (ash x -31))
                  (or (equal msb 1)
                      (equal (logand x 3) low)))
  :cov-bindings `((x ,(g-int 0 1 33))))

We specify the five subgoals to consider using two new variables, msb and low. Here, msb will determine the most significant bit of x; low will determine the two least significant bits of x, but only when msb is 0.

The :param-bindings argument describes the five subgoals by assigning different values to msb and low. It also gives the g-bindings to use in each case. We use different bindings for x for each subgoal to show how it is done.

The :param-hyp argument describes the relationship between msb, low, and x that will be assumed in each subgoal. In the symbolic execution performed for each subgoal, the :param-hyp is used to reduce the space of objects represented by the symbolic binding for x. For example, in the subgoal where msb = 1, this process will assign t to x[31]. The :param-hyp will also be assumed to hold for the coverage proof for each case.

How do we know the case-split is complete? One final proof is needed to show that whenever the hypothesis holds for some x, then at least one of the settings of msb and low satisfies the :param-hyp for this x. That is:

(implies (unsigned-byte-p 32 x)
         (or (let ((msb 1) (low nil))
               (and (equal msb (ash x -31))
                    (or (equal msb 1)
                        (equal (logand x 3) low))))
             (let ((msb 0) (low 0)) ...)
             (let ((msb 0) (low 1)) ...)
             (let ((msb 0) (low 2)) ...)
             (let ((msb 0) (low 3)) ...)))

This proof is also done in the def-gl-thm style, so we need we need one last set of symbolic bindings, which is provided by the :cov-bindings argument.

Another Example

Suppose we want to prove the commutativity of * for two finite natural numbers, a and n, but that GL isn't able to prove this property unless we case-split on the eight possible values for n. We can do so with the following call of def-gl-param-thm

(def-gl-param-thm finite-commute-of-*
  :hyp (and (natp a)
            (< a (expt 2 16))
            (natp n)
            (< n 8))
  :concl (equal (* n a)
                (* a n))
  :param-bindings `((((lsb 0) (mid-sb 0) (high-sb 0))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 0) (mid-sb 0) (high-sb 1))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 0) (mid-sb 1) (high-sb 0))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 0) (mid-sb 1) (high-sb 1))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 1) (mid-sb 0) (high-sb 0))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 1) (mid-sb 0) (high-sb 1))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 1) (mid-sb 1) (high-sb 0))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3)))
                    (((lsb 1) (mid-sb 1) (high-sb 1))
                     ,(gl::auto-bindings (:nat a 16)
                                         (:nat n 3))))
  :param-hyp (equal n
                    (logapp 1 lsb
                            (logapp 1 mid-sb
                                    high-sb)))

  :cov-bindings (gl::auto-bindings (:nat a 16)
                                   (:nat n 3)))

The :hyp and :concl are the same as in a def-gl-thm. The :gl-bindings becomes :cov-bindings. And we must add the :param-bindings and :param-hyp.

As in the previous example, the :param-hyp specifies the relationship between the variables in the theorem that we want to case-split and the values given in :param-bindings. In this example, we essentially encode a truth table into :param-bindings using the least significant bit (lsb), middle significant bit (mid-sb), and most significant bit (high-sb). We then indicate that these three significant-bit variables appended together represent the variable n in our theorem.

The syntax for specifying the variable ordering for each case-split is a bit strange. Currently, for each :param-bindings entry, one must specify the symbolic objects (BDD ordering, number of bits required, etc.) for each case-split. Thus, in this example, you see the bindings specified many times. We could write a macro (perhaps using pairlis$) so we didn't have to type so much, but for clarity of instruction, we leave the expansion in this example.