POLISHING-PROOFS-TUTORIAL

A Beginner's Guide to Developing and Polishing ACL2 Proofs

This tutorial has been written by Shilpi Goel and Sandip Ray.

This documentation is about "styles" and user-level experience and mainly intended to provide advice to the new user to become successful at approaching a formalization and proof problem in ACL2. In this note we will consider the following two basic questions:

1. What kind of factors should the user look for and consider to successfully guide the theorem prover to a successful proof?
2. Once the proof is completed, how should it be cleaned up in order to facilitate maintenance and extension of the book?
The suggestions and advice provided herein are of course guided by our own styles of approaching an ACL2 proof. Eventually every user develops her unique proof style and there is no "right" or "wrong" approach. One should just use the style that one feels most comfortable with. Thus, the advice in this documentation should be taken as a template for guidance to eventually develop your own style --- not as an immutable ground truth on an ACL2 proof approach. Furthermore, many of the suggestions, at least in the answer to the first question above, are influenced by common ACL2 guidance and also discussed elsewhere in the ACL2 documentation (see, for example, THE-METHOD). Here we show how some of these guidances translate into concrete directives in the interaction with the theorem prover.

To make the ideas concrete, we will take the following conjecture:

Conjecture: "If the lower 32 bits of a number are all zero, then any bit at a position less than 32 will have the value zero."

This is an arithmetic conjecture, and it actually arose in the context of developing correctness proofs for X86 machine code.

Corresponding to (1) and (2) above, we will consider the proof of this conjecture twice. First we will develop the proof, and then we will clean it up.

PART A: Proof Development:

Here is a formal version of the conjecture above.

(defthm lower-32-all-zero-no-<-32-set
(implies (and (equal (logand (1- (expt 2 32)) res) 0)
(natp j)
(natp res)
(< j 32))
(null (logbitp j res))))

In this document, we will not consider the (interesting but orthogonal) question of whether this is the "right" approach to formalize the English statement of the conjecture in ACL2 or not. The focus of this document is to determine how to get ACL2 to prove it, once such a formalization is given.

The conjecture above is an arithmetic conjecture. So the first thing that a user should do is use an arithmetic library. This is specifically relevant for arithmetic, and in particular, reasoning about functions like floor and mod. This is because (1) such functions are difficult to reason about, and (2) ACL2 now has powerful support of libraries of lemmas for reasoning about them.

So we first include the library arithmetic-5 (which, as of this writing, is one of the most elaborate arithmetic libraries in ACL2).

(include-book "arithmetic-5/top" :dir :system)

We then submit the conjecture.

(defthm lower-32-all-zero-no-<-32-set
(implies (and (equal (logand (1- (expt 2 32)) res) 0)
(natp j)
(natp res)
(< j 32))
(null (logbitp j res))))

The proof fails. So we will apply "The Method" to debug this. In particular, the following checkpoint shows up:

(1)
(IMPLIES (AND (EQUAL (MOD RES 4294967296) 0)
(INTEGERP J)
(<= 0 J)
(INTEGERP RES)
(<= 0 RES)
(< J 32))
(INTEGERP (* 1/2 (FLOOR RES (EXPT 2 J)))))

The key to success with ACL2 is the ability to read such checkpoints and determine what to do. So what information can we glean from the above?

First, we notice that 4294967296 is (expt 2 32) . What this checkpoint tells us is that:

Given the following three facts,

1. (mod res (expt 2 32)) == 0,
2. j is a nonnegative integer whose value is less than 32, and
3. res is a nonnegative integer,

ACL2 can not prove that 1/2 of (floor res (expt 2 j)) is an integer. In other words, ACL2 can not prove that (floor res (expt 2 j)) returns an even number under the given conditions.

We ask ourselves - is the above actually true? So, first we figure out what the function floor does. From the ACL2 documentation, we find that (floor x y) divides x by y and truncates the quotient. (Actually, the quotient is truncated towards negative infinity but we can ignore this fact for the purpose of this exercise).

If (mod res (expt 2 32)) is zero, then res is a multiple of (expt 2 32). So, if res is divided by (expt 2 j) where j is a value less than 32, the quotient will always be even (to be precise, it will be a multiple of 2^(32 - j). Hence, informally, we have reasoned that the above is a theorem and hence, should be provable.

We then formalize the above reasoning as:

(defthm lemma-floor-inference
(implies (and (integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(< j i)
(equal (mod res (expt 2 i)) 0))
(evenp (floor res (expt 2 j)))))

When we submit the above conjecture to ACL2, we get the following checkpoint:

(2)
(IMPLIES (AND (INTEGERP RES)
(<= 0 RES)
(INTEGERP I)
(<= 0 I)
(INTEGERP J)
(< J I)
(EQUAL (MOD RES (EXPT 2 I)) 0))
(INTEGERP (* 1/2 (FLOOR RES (EXPT 2 J)))))

Notice that if i is 32 in the above checkpoint, this is equivalent to the checkpoint (1). Indeed, the sufficiency of the lemma lemma-floor-inference above for proving our original goal is evident from the following:

(skip-proofs
(defthm lemma-floor-inference
(implies (and (integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(< j i)
(equal (mod res (expt 2 i)) 0))
(evenp (floor res (expt 2 j))))))

(defthm lower-32-all-zero-no-<-32-set
(implies (and (equal (logand (1- (expt 2 32)) res) 0)
(natp j)
(natp res)
(< j 32))
(null (logbitp j res)))
:hints
(("Goal"
:use (:instance lemma-floor-inference (i 32)))))

Thus we know that our final theorem will be proven if lemma-floor-inference goes through. So we shift our focus now to proving lemma-floor-inference.

We guess that may be ACL2 can not infer from (equal (mod res (expt 2 i)) 0) that res is a multiple of (expt 2 i) because had it been able to infer that, it would have been able to figure out the conclusion of lemma-floor-inference.

ACL2 can prove the following, which affirms the above fact:

(thm
(implies (and (integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i)
(integerp z))
(evenp (floor (* z (expt 2 i)) (expt 2 j)))))

So we concentrate on the function mod. Mod is defined in terms of floor.

(mod x y) => (- x (* (floor x y) y))

So, informally, if (equal (mod x y) 0) is true, then (equal x (* (floor x y) y)) is also true (and vice versa).

So, informally (equal (mod res (expt 2 i)) 0) means that res is equal to (* (expt 2 i) (floor res (expt 2 i)) (and vice versa).

We replace res by (* (expt 2 i) (floor res (expt 2 i)) in lemma-floor-inference, and remove the hypothesis (equal (mod res (expt 2 i)) 0) since at this point, we are assuming that ACL2 can infer that res is a multiple of (expt 2 i) from (equal (mod res (expt 2 i)) 0).

(defthm floor-even-number-return
(implies
(and (integerp (* (expt 2 i) (floor res (expt 2 i))))
(<= 0 (* (expt 2 i) (floor res (expt 2 i))))
(integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i))
(evenp (floor (* (expt 2 i) (floor res (expt 2 i)))
(expt 2 j)))))
This theorem goes through.

So, we notice that lemma-floor-inference can be proved if only ACL2 can "replace" res with (* (expt 2 i) (floor res (expt 2 i))). The tactic we will follow to prove lemma-floor-inference is:

1. Prove that (evenp (floor res (expt 2 j))) is true given, among other conditions, that res is equal to (* (expt 2 i) (floor res (expt 2 i))).
2. Figure out under what conditions we can derive (equal (mod res (expt 2 i)) 0) from (equal res (* (expt 2 i) (floor res (expt 2 i)))).
3. Add these conditions to the hypotheses of 1 to prove lemma-floor-inference.

For point 1, we try the following:

(defthm floor-even-number-return-equality-hypothesis
(implies (and (integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i)
(equal res
(* (expt 2 i) (floor res (expt 2 i)))))
(integerp (* (floor res (expt 2 j)) 1/2)))
:hints (("Goal"
:do-not '(simplify)
:in-theory (disable floor-mod-elim))))

We include the hints so that ACL2 does not simplify away /eliminate the definition of floor. However, the proof does not go through. Inspecting the failed proof, we notice that the following is where the proof attempt stalls:

Goal'
(IMPLIES (AND (INTEGERP (* (EXPT 2 I) (FLOOR RES (EXPT 2 I))))
(<= 0 (* (EXPT 2 I) (FLOOR RES (EXPT 2 I))))
(INTEGERP I)
(<= 0 I)
(INTEGERP J)
(<= 0 J)
(< J I)
(HIDE (EQUAL RES
(* (EXPT 2 I) (FLOOR RES (EXPT 2 I))))))
(INTEGERP (* (FLOOR (* (EXPT 2 I) (FLOOR RES (EXPT 2 I)))
(EXPT 2 J))
1/2)))

This form is very similar to floor-even-number-return and hence, we put in the following:

(defthm floor-even-number-return-equality-hypothesis
(implies (and (integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i)
(equal res
(* (expt 2 i) (floor res (expt 2 i)))))
(integerp (* (floor res (expt 2 j)) 1/2)))
:hints (("Goal" :do-not '(simplify)
:in-theory (disable floor-mod-elim))
("Goal'" :use floor-even-number-return)))
This goes through now.

For point 2, we notice that we can derive (equal (mod res (expt 2 i)) 0) from (equal res (* (expt 2 i) (floor res (expt 2 i)))) under the following conditions:

(defthm derive-mod-expression-from-equality
(implies (and (integerp res)
(<= 0 res)
(equal res (* (expt 2 i) (floor res (expt 2 i))))
(equal (mod res (expt 2 i)) 0)))

These conditions are already in the hypotheses of floor-even-number-return-equality-hypothesis. Thus floor-even-number-return-equality-hypothesis should suffice to prove lemma-floor-inference.

We now prove lemma-floor-inference.

(defthm lemma-floor-inference
(implies (and (integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(< j i)
(equal (mod res (expt 2 i)) 0))
(evenp (floor res (expt 2 j))))
:hints (("Goal"
:use  floor-even-number-return-equality-hypothesis)))
As expected, the proof goes through.

As shown above, we can now prove our original conjecture:

(defthm lower-32-all-zero-no-<-32-set
(implies (and (equal (logand (1- (expt 2 32)) res) 0)
(natp j)
(natp res)
(< j 32))
(null (logbitp j res)))
:hints
(("Goal"
:use (:instance lemma-floor-inference (i 32)))))
The proof goes through.

PART B: Cleaning Up Proofs:

Here are some very general tips to clean up proofs.

Note: The following are not hard-and-fast rules but are essentially tips to have a cleaner proof.

First, it is typically not a good idea to non-locally include a book like arithmetic-5. This is because later on in the project you might want to use a different arithmetic book, which might be incompatible with arithmetic-5.

Second, it is worthwhile to try to make the lemmas that are auxiliary in the way of proving the main result local. This helps to have a lot more control in the subsequent use of the book --- in particular, this way, you do not need to worry about whether a weird auxiliary rule that you had used as a hack to prove your main theorem could subsequently cause a problem later.

Third, it is a good practice always to disable the rule that you are using as a :use hint.

Fourth, if at all possible, put all the subgoal hints to the top goal (or to the top subgoals after the induction). This is not always going to work, but it is typically ok if the only subgoal hints are :use hints. Putting :use hints at subgoal is absolutely ok when you were developing the proof since you really want to put it at the subgoal in which you found the problem, so that you do not have to think about the extraneous stuff. But when everything works, it is often better to put all the subgoal :use hints together and put it at the top level. One key reason for this is that as ACL2 goes from one version to another, the subgoal numbers where the hint is applicable may change (due to slight change in the simplification heuristic or some such). Putting it at the top level is more robust to such changes.

Fifth, try to remove the :do-not hints. This is because they are not usually needed for proof replay (only for debugging failed proofs when you are developing them) and hence do not need to be around in the cleaned-up version. This makes the script look less messy. There are exceptions to this of course, --- there are situations when a :do-not hint is actually necessary (the typical case is :do-not '(generalize)), but more often than not they are not. The simplest way to remove the hints from the cleaned-up version is to remove the :do-not hint and if the proof does not work just put it back on.

Incorporating the above tips makes the proof script look like this:

(local
(include-book "arithmetic-5/top" :dir :system))

(local
(defthm floor-even-number-return
(implies
(and (integerp (* (expt 2 i) (floor res (expt 2 i))))
(<= 0 (* (expt 2 i) (floor res (expt 2 i))))
(integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i))
(evenp (floor (* (expt 2 i) (floor res (expt 2 i)))
(expt 2 j))))))

(local (in-theory (disable floor-even-number-return)))

(local
(defthm floor-even-number-return-equality-hypothesis
(implies (and (equal res
(* (expt 2 i) (floor res (expt 2 i))))
(integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i))
(integerp (* (floor res (expt 2 j)) 1/2)))
:hints (("Goal"
:use floor-even-number-return))))

(local (in-theory (disable floor-even-number-return-equality-hypothesis)))

(local
(defthm lemma-floor-inference
(implies (and (integerp res)
(<= 0 res)
(integerp i)
(<= 0 i)
(integerp j)
(< j i)
(equal (mod res (expt 2 i)) 0))
(evenp (floor res (expt 2 j))))
:hints (("Goal"
:use  floor-even-number-return-equality-hypothesis))))

(local (in-theory (disable lemma-floor-inference)))

(defthm lower-32-all-zero-no-<-32-set
(implies (and (equal (logand (1- (expt 2 32)) res) 0)
(natp j)
(natp res)
(< j 32))
(null (logbitp j res)))
:hints
(("Goal"
:use (:instance lemma-floor-inference (i 32)))))