		Search-engine friendly clone of the ACL2 documentation.

Basic-tutorial

1. An Example GL Proof

The usual way to load GL is to start with

(include-book "centaur/gl/gl" :dir :system)

Let's use GL to prove a theorem. The following C code, from Sean Anderson Bit Twiddling Hacks page, is a fast way to count how many bits are set in a 32-bit integer.

v = v - ((v >> 1) & 0x55555555);
v = (v & 0x33333333) + ((v >> 2) & 0x33333333);
c = ((v + (v >> 4) & 0xF0F0F0F) * 0x1010101) >> 24;

We can model this in ACL2 as follows. It turns out that using arbitrary-precision addition and subtraction does not affect the result, but we must take care to use a 32-bit multiply to match the C code.

(defun 32* (x y)
  (logand (* x y) (1- (expt 2 32))))

(defun fast-logcount-32 (v)
  (let* ((v (- v (logand (ash v -1) #x55555555)))
         (v (+ (logand v #x33333333)
               (logand (ash v -2) #x33333333))))
    (ash (32* (logand (+ v (ash v -4)) #xF0F0F0F)
              #x1010101)
         -24)))

We can then use GL to prove fast-logcount-32 computes the same result as ACL2's built-in logcount function for all unsigned 32-bit inputs.

(def-gl-thm fast-logcount-32-correct
  :hyp   (unsigned-byte-p 32 x)
  :concl (equal (fast-logcount-32 x)
                (logcount x))
  :g-bindings `((x ,(g-int 0 1 33))))

The :g-bindings form is the only help GL needs from the user. It tells GL how to construct a symbolic object that can represent every value for x that satisfies the hypothesis (we'll cover this shortly). No arithmetic books or lemmas are required—we actually don't even know why this algorithm works. The proof completes in 0.09 seconds and results in the following ACL2 theorem.

(defthm fast-logcount-32-correct
  (implies (unsigned-byte-p 32 x)
           (equal (fast-logcount-32 x)
                  (logcount x)))
  :hints ((gl-hint ...)))

GL can generate counterexamples to non-theorems. At first, we didn't realize we needed to use a 32-bit multiply in fast-logcount-32, and we just used an arbitrary-precision multiply instead. The function still worked for test cases like 0, 1 #b111, and #b10111, but when we tried to prove its correctness, GL showed us three counterexamples: #x80000000, #xFFFFFFFF, and #x9448C263. By default, GL generates a first counterexample by setting bits to 0 wherever possible, a second by setting bits to 1, and a third with random bit settings.