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:
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,
(mod res (expt 2 32)) == 0, j is a nonnegative integer whose value is less than 32, andres 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:
So we concentrate on the function mod. Mod is defined in terms of
floor.
(thm
(implies (and (integerp i)
(<= 0 i)
(integerp j)
(<= 0 j)
(< j i)
(integerp z))
(evenp (floor (* z (expt 2 i)) (expt 2 j)))))
(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).
This theorem goes through.
(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)))))
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:
(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))). (equal (mod res (expt 2 i)) 0) from
(equal res (* (expt 2 i) (floor res (expt 2 i)))). 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:
This goes through now.
(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)))
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.
As expected, the proof goes through.
(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 shown above, we can now prove our original conjecture:
The proof goes through.
(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)))))
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)))))