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
(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))))
(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