CD:
d:/NOTES/NOTE_TJK/

; 
;   Internal Note #285
;   Computational Logic, Inc.
;   August 31, 1993


;              SEVERAL APPROACHES TO THE CORRECTNESS OF
;              A SIMPLE IMPERATIVE PROGRAM WITH A LOOP

;                           Matt Kaufmann
                                   
#|
This work was supported in part at Computational Logic, Inc., by the
Defense Advanced Research Projects Agency, ARPA Order 7406. The views
and conclusions contained in this document are those of the author(s)
and should not be interpreted as representing the official policies,
either expressed or implied, of Computational Logic, Inc., the Defense
Advanced Research Projects Agency or the U.S.  Government.
|#

; The various Lisp comment notations in this file allow it to be run
; in the RCL system, as explained below.  I should add that the
; original write date on this note was April 16, 1993, but I am just
; now making it into an internal note.  I've since has interesting
; correspondence with Mark Saaltink that may result in some further
; insights in the direction of this work, but I'll leave those to a
; future paper.

#|

Here is a short note on four approaches to proving correctness of a
simple program that employs a (terminating) loop:  an integer
logarithm (base 2) program.  This note is organized as follows.  We
introduce our presentation by discussing the program that we are
analyzing, relating this program to certain Nqthm functions, and by
summarizing our four approaches to proving correctness.  Next, we
present the ``preliminaries,'' including the introduction of the
program in question and the corresponding Nqthm functions.  The
remainder of the note is dedicated to the presentation of our four
solutions to the correctness problem.  This file executes successfully
in the RCL system [2], [3] (taking about 3 minutes on a Sparc 2).
However, the exposition here is intended to be self-contained for
those having some familiarity with Nqthm.  In those places where we
seem to rely on RCL, the reader can probably convince himself that one
could generate the appropriate proof obligations by hand instead.

Acknowledgements.  First of all, I thank Yuan Yu for taking me through
his solution of this problem, in the case of MC68020 machine code.
Also, I thank Bill Pase of ORA Canada for helping me through a
solution to this problem using the EVES system [1].  Actually, I
performed that solution with John Ramsdell of Mitre Corp., who by the
way got us back on track when he and I started to stall, by suggesting
the loop invariant used below.  Finally, I thank Mark Bickford and
Doug Hoover of ORA (Ithaca) for taking me through a similar solution
to this problem in Ada using the Penelope system [7].

The EVES solution, by the way, is a solution that employs a
verification condition generator (VCG) and hence is closely related to
Approach 2 below.  The Penelope solution is very similar to the EVES
solution, though I gather that the underlying method of generating the
proof obligations may be different from that used in EVES.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Introduction                                                     ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Consider the following non-applicative Lisp program for computing the
logarithm base 2.

(defun log2 (n)
  (if (not (and (integerp n)
                (< 0 n)))
      (return-from log2 0))
  (let ((temp n)
        (ans 0))
    (loop
     (if (< temp 2)
         (return-from log2 ans))
     (setq temp (floor temp 2))
     (setq ans (+ ans 1)))))

Here we use the RCL system, which is a system for non-applicative Lisp
verification that I completed about three and a half years ago (see
[2], [3]).  However, the presentation here is intended to be
self-contained.  RCL is built on top of top of Nqthm [4].  What RCL
does is to automatically generate a ``corresponding'' Nqthm function,
as well as a recursively defined subfunction that corresponds to this
program's loop.  The DEFUN-RCL form appearing among the forms below is
the one that generates these ``corresponding'' Nqthm functions.

First, here is the auxiliary ``loop'' function that the system
generates.  I claim that it's really just one one would expect (or at
least hope for) as a rather direct model of the loop.

(DEFN *CL-LOG2-TAGBODY-0
      (ANS TEMP)
      (IF (LESSP TEMP 2)
          ANS
          (*CL-LOG2-TAGBODY-0 (IPLUS ANS 1)
                              (IQUOTIENT TEMP 2))))

Here is the top-level function that the system generates.  The RCL
semantics say that when .RCL-FLG is T, we obtain the value returned by
the Lisp routine on the indicated arguments (here, N); when .RCL-FLG
is F, this function returns the ``error or throw situation,'' which
isn't worth explaining here except to note that this routine always
returns normally (as demonstrated by the event LOG2-RETURNS-NORMALLY
that appears later).

(DEFN *CL-LOG2
      (.RCL-FLG N)
      (IF (EQUAL .RCL-FLG T)
          (IF (INTEGERP N)
              (IF (ILESSP 0 N)
                  (*CL-LOG2-TAGBODY-0 0 N)
                  0)
              0)
          F))

Our goal, then, is to prove that this ``corresponding'' Nqthm
function, when applied to an arbitrary positive integer N, returns a
value LOG with following property.

[MAIN]    2 ** LOG <= N < 2 ** (LOG + 1)

In all four of our approaches that follow, MAIN is the name of a
formalization of this theorem, stated as a PROVE-LEMMA event.  In all
but Approach 2, formalizations of the two inequalities are first
proved separately, under the names LOG2-THM1 and LOG2-THM2.  We defer
discussion of these formalizations until we get to the section
``Formalizing the Problem.''

Now that we have discussed the ``corresponding functions'' that RCL
produces, together with an informal statement of our main goal, let us
turn to a discussion our four approaches.

The recursive function *CL-LOG2-TAGBODY-0 shown above is what one
might write to represent the program's loop, if one were doing a
CLInc-style interpreter proof.  In such proofs, one typically proves a
lemma roughly of the form

(interpret '<code> environment)
 =
(<corresponding_function> environment)

This is essentially what Yuan Yu did (see [5] or [6]) when performing
a proof of correctness of a similar MC68020 program.  He proved (among
other things) that if you read data register 0 after running the
processor for an appropriate number of machine instructions, then the
result is the same as that computed by the ``corresponding'' recursive
function on the original ``input.''  Then, a separate argument
establishes that this recursive function computes a number which
satisfies the specification [MAIN] above.

Our four approaches differ from Yuan's in that he proves an
appropriate correspondence between

   (a) applying an interpreter (operational semantics) to the given
   program, and

   (b) a recursive function.

However, the RCL system generates (b) automatically, as the discussion
above for *CL-LOG2-TAGBODY-0 indicates.  Thus, we have to trust the
RCL system in order to believe the equivalence between (a) and (b).
(In point of fact, we have not even written a formalization of an RCL
interpreter!)  At any rate, our goal here is to show and compare some
different ways of reasoning about the function produced in (b), which
is crucial both for RCL and for an interpreter-based approach.  In a
certain sense there's nothing new here; Nqthm users reason about
recursive functions all the time.  However, we attempt to relate some
of our approaches to the more conventional VCG-based approach.

Our four approaches are as follows.

Approach 1:  Relate the recursive function (b) to a simpler Nqthm
function, and reason about that function instead.  This is also what
Yuan has done in the log example.

Approach 2:  Explicitly formulate an invariant that would typically
be used for traditional VCG based approaches, and essentially reduce
the problem to the proof obligation that a VCG would generate.

Approach 3:  Similar to Approach 2, but without explicitly
introducing the notion of an invariant.

Approach 4:  Reason directly about the recursive function (b).

All but the first Approach are somehow related to the invariant that
we referred to briefly in the acknowledgements above:

        ans >= 0
     &  temp >= 1
     &  n >= (2**ans) * temp
     &  n <  (2**ans) * (temp + 1)

Interestingly, Approaches 2 and 4 are related.  We'll show how
Approach 3 may be viewed as their link.  However, we recall actually
carrying out Approach 4 *before* attempting what we call here
Approaches 2 and 3, and taking a rather unprincipled ``hacking'' stab
at Approach 4.  This ``rationalization'' for Approach 4 in terms of
Approach 2 is therefore quite after the fact!

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Preliminaries                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The RCL system starts with a pretty large Nqthm arithmetic library
;; already loaded, though we also start by enabling a rule proved
;; there, to the effect that (iquotient x y) = (quotient x y) [natural
;; number quotient] for naturals x and y; similarly for iplus and
;; plus.  These two enable events below, together with the silly lemma
;; immediately following them, all have to do with the fact that Nqthm
;; handles natural numbers (which are built in and have a
;; corresponding linear arithmetic decision procedure) much better
;; than integers.  This sort of weirdness should be much less of an
;; issue with Acl2.

(enable iquotient-numberp)
(enable iplus-numberp)

(prove-lemma ilessp-lessp (rewrite)
  (implies (not (zerop x))
           (equal (ilessp y x)
                  (lessp y x)))
  ((enable ilessp)))

(prove-lemma log2-helper (rewrite)
  (implies (not (lessp temp 2))
           (lessp (count (iquotient temp 2))
                  (count temp)))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable iquotient)))

;; The following Lisp definition introduces an auxiliary function
;; *CL-LOG2-TAGBODY-0, which represents the loop, and then a top-level
;; function *CL-LOG2 that ``represents'' this Lisp routine.  See the
;; introductory section for more explanation.

(defun-rcl log2 (n)
  (if (not (and (integerp n)
                (< 0 n)))
      (return-from log2 0))
  (let ((temp n)
        (ans 0))
    (loop
     (if (< temp 2)
         (return-from log2 ans))
     (setq temp (floor temp 2))
     (setq ans (+ ans 1)))))

;; Here is how we say that the LOG2 routine always returns normally.
;; We don't need this result for anything below, but it's a nice thing
;; to know.

(prove-lemma log2-returns-normally ()
  (equal (*cl-log2 f n) f))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Formalizing the Problem
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

Now let us consider four approaches to proving correctness of this
program.  By that I mean that we want to prove that the value returned
by the Lisp (RCL) routine LOG2 on input N, which [as explained above]
is (*CL-LOG2 T N), satisfies the following inequalities.

Theorem.  MAIN
(N > 0)
 ==>
(EXP 2 (*CL-LOG2 T N)) <= N < (EXP 2 (ADD1 (*CL-LOG2 T N)))

In all these cases, the main subfunction of *CL-LOG2 that we have to
reason about is the function generated to represent the loop
computation, which is *CL-LOG2-TAGBODY-0.  So in most cases, we
address our energy to proving one or more key lemmas about
*CL-LOG2-TAGBODY-0, in order to obtain the final result.  However,
we'll see that in Approach 2 we can avoid thinking about this
function.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Approach 1:  Relate the loop function to a simpler Nqthm         ;;
;; function, which we'll call LOG_2.                                ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defn log_2 (n)
  (if (or (zerop n) (equal n 1))
      0
    (add1 (log_2 (quotient n 2)))))

;; The following rewrite rule lets us do the rest of our reasoning
;; about LOG_2 instead of about the more complicated function
;; *CL-LOG2-TAGBODY-0.

(prove-lemma *cl-log2-tagbody-0-is-log_2 (rewrite)
  (implies (and (not (zerop n))
                (numberp ans))
           (equal (*cl-log2-tagbody-0 ans n)
                  (plus ans (log_2 n)))))

;; The following two are analogues of lemmas proved by Yuan Yu.

(prove-lemma log2-thm1 (rewrite)
     (implies (not (zerop n))
              (not (lessp n (exp 2 (log_2 n))))))

(prove-lemma log2-thm2 (rewrite)
     (lessp n (exp 2 (add1 (log_2 n)))))

(prove-lemma main ()
  (implies (not (zerop n))
           (and (not (lessp n (exp 2 (*cl-log2 t n))))
                (lessp n (exp 2 (add1 (*cl-log2 t n))))))
  ((enable ilessp integerp)
   (disable log_2 exp-add1 exp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Approach 2: With J Moore's ``small-machine'' example as an       ;;
;; inspiration, now let us try to model the invariance argument in  ;;
;; a more principled way.  That is, we explicitly formulate an      ;;
;; invariant that would typically be used for traditional VCG       ;;
;; (verification condition generator) based approaches, and         ;;
;; essentially reduce the problem to the proof obligation that a    ;;
;; VCG would generate.                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Let's back up to where the previous approach started.

(ubt log_2)

;; The following lemma is very helpful with the proof of
;; INV2-PRESERVED below.  We may as well prove it here.

(prove-lemma lessp-2 (rewrite)
  (equal (lessp x 2)
         (or (zerop x)
             (equal x 1))))

;; Let's say that the invariant is (INV ANS TEMP N).  We define two
;; main subfunctions of the invariant, one for each of the two
;; inequalities displayed as [MAIN] in the introduction above, and
;; prove that each is preserved by one step through the loop.

(defn inv1 (ans temp n)
  (not (lessp n (times (exp 2 ans) temp))))

(prove-lemma inv1-preserved ()
  (implies (and (lessp 1 temp)
                (numberp ans)
                (inv1 ans temp n))
           (inv1 (add1 ans) (quotient temp 2) n)))

(defn inv2 (ans temp n)
  (lessp n (times (exp 2 ans) (add1 temp))))

(prove-lemma inv2-preserved ()
  (implies (and (lessp 1 temp)
                (numberp ans)
                (inv2 ans temp n))
           (inv2 (add1 ans) (quotient temp 2) n)))

;; And now the invariant is defined.

(defn inv (ans temp n)
  (and (numberp ans)
       (not (zerop temp))
       (inv1 ans temp n)
       (inv2 ans temp n)))

;; Consider the lemma INV-HOLDS-AT-END-OF-LOOP, to be proved below.

;;   Lemma.  INV-HOLDS-AT-END-OF-LOOP
;;   (implies (inv ans temp n)
;;            (inv (*cl-log2-tagbody-0 ans temp)
;;                 1
;;                 n))

;; Roughly speaking, it says that the invariant is preserved from the
;; beginning to the end of the loop; more on that below.  Notice that
;; the lemma's consequent, (inv (*cl-log2-tagbody-0 ans temp) 1 n), is
;; unchanged between the inductive hypothesis and inductive
;; conclusion, because in the inductive step case, we have

;;      (*cl-log2-tagbody-0     ans           temp)
;;   =  (*cl-log2-tagbody-0 (add1 ans) (quotient temp 2)).

;; Thus, the inductive step for the lemma INV-HOLDS-AT-END-OF-LOOP
;; (displayed above) has the following form, where:  Q is either of
;; the terms displayed in the equation immediately above; P is the
;; hypothesis that says we are in the inductive step case; Inv is the
;; current invariant (inv ans temp n); and Inv' is the invariant after
;; stepping once through the loop, which is
;; (inv (add1 ans) (quotient temp 2) n).

;; (P & (Inv' ==> Q)) ==> (Inv ==> Q).

;; Clearly then it suffices, for this inductive step, to prove:

;; (P & Inv) ==> Inv'.

;; That is: the inductive step reduces to proving that the invariant
;; is preserved when we go one time through the loop.  THIS IS THE
;; TRADITIONAL MAIN PROOF OBLIGATION FOR VCG-BASED APPROACHES!  Here
;; is that sublemma, which follows immediately from the two lemmas
;; proved just above.

(prove-lemma inv-preserved (rewrite)
  (implies (and (lessp 1 temp)
                (numberp ans)
                (inv ans temp n))
           (inv (add1 ans) (quotient temp 2) n))
  ((disable inv1 inv2)
   (use (inv1-preserved)
        (inv2-preserved))))

;; From this inductive step, it seems to be an excellent idea to keep
;; the definition of INV turned off in the proof of
;; INV-HOLDS-AT-END-OF-LOOP; otherwise the rewrite rule just proved
;; will probably not apply, since INV will have already been expanded
;; away by the time the theorem prover is ready to consider this rule.
;; But with INV to be disabled, we then also need a lemma to help with
;; the base case.

(prove-lemma trivial-inv-consequences (rewrite)
  (implies (inv ans temp n)
           (and (numberp ans)
                (numberp temp)
                (not (equal 0 temp)))))

;; Although the theorem prover evidently succeeds on the following
;; lemma without more than the single disable hint provided, still the
;; reasoning above kind of explains what's going on in terms of
;; traditional loop verification.

;; Let us elaborate a bit. The idea is to say and prove that if the
;; invariant holds when entering the loop, then it holds when leaving
;; the loop.  The consequent of this implication is conveniently
;; stated using the ``corresponding function'' for the loop, i.e.,
;; *CL-LOG2-TAGBODY-0, to describe the value coming out of the loop.

(prove-lemma inv-holds-at-end-of-loop ()
  (implies (inv ans temp n)
           (inv (*cl-log2-tagbody-0 ans temp)
                1
                n))
  ((disable inv)))

;; The main property now follows readily, instantiating ANS to 0 and
;; TEMP to N to represent the values of these locals when the loop is
;; entered.

(prove-lemma main ()
  (implies (not (zerop n))
           (and (not (lessp n (exp 2 (*cl-log2 t n))))
                (lessp n (exp 2 (add1 (*cl-log2 t n))))))
  ((use (inv-holds-at-end-of-loop
         (ans 0)
         (temp n)
         (n n)))
   (enable numberp-is-integerp)))

;; A minor point:  The system needs to know that (NUMBERP X) implies
;; (INTEGERP X) or the proof above fails, which is why we give the
;; hint just above, to enable the rule NUMBERP-IS-INTEGERP.
;; Alternatively we could just enable the definition of INTEGERP
;; there.  With Acl2 I imagine there would be no such
;; ``natural-versus-integer'' issues, or at least far fewer of them.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Approach 3:  Let's try to reason about the tagbody (loop)        ;;
;; function directly this time, but still in the spirit of showing  ;;
;; the preservation of a loop invariant.                            ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The lemma LESSP-2 seems crucial for the proof of LOG-THM2-LEMMA
;; below, so we only back up *to* it instead of *past* it.

(ubt inv1)

;; Here is one of the proof obligations from the invariant.  It's
;; commented out because the prover does not really need this lemma,
;; even though it does use this lemma if we do include it.  In fact,
;; it helps with (and essentially IS) the inductive step of the next
;; lemma.  We leave it in as a comment because it suggests how the
;; present Approach is analogous to Approach 2 above, in that the
;; proof is mainly an argument that the invariant is preserved by one
;; trip through the loop.

;; Actually, in order to get the following lemma to apply to the proof
;; of LOG-THM1, we would seem to need a fairly elaborate hint in
;; LOG-THM1.

;;   (disable times exp
;;            exp-add1 ;says that x**(k+1) = x*(x**k)
;;            ;; but with EXP and EXP-ADD1 disabled, it turns out
;;            ;; that we also need to disable:
;;            commutativity-of-times)

#|
(prove-lemma log-thm1-lemma (rewrite)
  (implies (and (lessp 1 temp)
                (numberp ans)
                (not (lessp n (times (exp 2 ans) temp))))
           (not (lessp n
                       (times (exp 2 (add1 ans)) (quotient temp 2))))))

     ;; Technical point:  the lemma above is stored as a so-called
     ;; linear [arithmetic] rule, because other than NOT, the
     ;; top-level function symbol of the conclusion is LESSP.  It's
     ;; reasonably accurate to say that the prover's inequality
     ;; reasoning routines use this lemma by forward chaining on the
     ;; conclusion when they see the ``triggering'' term in the second
     ;; argument of the conclusion's LESSP term.  However, before the
     ;; prover decides to use this lemma in that way, it must
     ;; establish the hypotheses.  Since the variable N appears in the
     ;; third hypothesis but does not appear in the trigger term, the
     ;; prover treats N literally; it does not do more than a very
     ;; weak attempt to instantiate this variable appropriately.
     ;; Hence, the exact form of this lemma is very important; in
     ;; fact, if the arguments are switched in the TIMES term from the
     ;; third hypothesis, the proof gets bogged down.

|#

;; When ans=0 and temp=n, the following says that n >= 2**(log2 n).

(prove-lemma log-thm1 ()
  (implies (and (not (zerop temp))
                (numberp ans)
                (not (lessp n (times (exp 2 ans) temp))))
           (not (lessp n
                       (exp 2 (*cl-log2-tagbody-0 ans temp)))))
  ;; Unfortunately necessary induction hint....
  ((induct (*cl-log2-tagbody-0 ans temp))))

;; Here is an analogue of the other invariant requirement.  One might
;; expect something like the following.

;;   (implies (and (lessp 1 temp)
;;                 (numberp ans)
;;                 (lessp n (times (exp 2 ans) (add1 temp))))
;;            (lessp n
;;                   (times (exp 2 (add1 ans)) (add1 (quotient temp 2)))))

;; Actually, we don't need a lemma for the inductive step from the
;; other invariant-preserved lemma either, but we'll leave it in a
;; comment for the same reason we left the preceding one in a comment.

#|

;; This time we would need to leave enabled EXP-ADD1 (which says that
;; [x**(k+1) = x*(x**k)] and COMMUTATIVITY-OF-TIMES; that seems
;; important for the proof of LOG-THM2 that follows, in order to bring
;; the factor of 2 out.  So, the following lemma is stated in a form
;; that can not be further rewritten -- in particular, the rewrite
;; rule EXP-ADD1 has already (implicitly) been applied, as have
;; multiplication facts.  Then, the linear arithmetic package can see
;; this lemma's applicability.

(prove-lemma log-thm2-lemma (rewrite)
  (implies (and (lessp 1 temp)
                (numberp ans)
                (lessp n (plus (exp 2 ans)
                               (times temp (exp 2 ans)))))
           (lessp n
                  (plus (exp 2 ans)
                        (exp 2 ans)
                        (times (exp 2 ans) (quotient temp 2))
                        (times (exp 2 ans) (quotient temp 2))))))

|#

;; When ans=0 and temp=n, the following says that
;; 2**(1+ log2 n) >= n+1.  It's stated in terms of (add1 temp) so that
;; the proof by induction can succeed; note that 2*[(temp/2)+1] >=
;; temp+1.

(prove-lemma log-thm2 ()
  (implies (and (not (zerop temp))
                (numberp ans)
                (lessp n (times (exp 2 ans) (add1 temp))))
           (lessp n
                  (exp 2 (add1 (*cl-log2-tagbody-0 ans temp)))))
  ((induct (*cl-log2-tagbody-0 ans temp))))

(prove-lemma main ()
  (implies (not (zerop n))
           (and (not (lessp n (exp 2 (*cl-log2 t n))))
                (lessp n (exp 2 (add1 (*cl-log2 t n))))))
  ((enable integerp)
   (use (log-thm1 (ans 0) (temp n) (n n))
        (log-thm2 (ans 0) (temp n) (n n)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Approach 4:  Reason directly about the ``corresponding           ;;
;; recursive function.''                                                      ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; In this Approach we'll reason directly about the function
;; *CL-LOG2-TAGBODY-0, without any motivation from the notion of loop
;; invariants.  In fact, I believe I put together such a proof
;; directly in this sense; more importantly, it's easy to imagine that
;; one could so so.  However, comments have been added below that
;; explain a relationship between this Approach and the preceding one.
;; The preceding one, in turn, has been explained from the point of
;; view of loop invariants, and hence we have demonstrated some kind
;; of relationship between the present approach and loop invariants
;; after all!

;; First we back up past the start of the preceding Approach.

(ubt log-thm1)

;; The preceding Approach's version of the lemma LOG-THM1 says:

;;     temp >=1
;;   & ans >= 0
;;   & n >= (2**ans) * temp
;;     ==>
;;   n >= (2**(*cl-log2-tagbody-0 ans temp))

;; This time, we do a bit of inequality reasoning to produce a
;; stronger lemma that does not mention n, and hence more directly
;; concerns the term (*CL-LOG2-TAGBODY-0 ANS TEMP) that we are trying
;; to reason about:

;;     temp >=1
;;   & ans >= 0
;;     ==>
;;   (2**ans) * temp >= (2**(*cl-log2-tagbody-0 ans temp))

(prove-lemma log-thm1 (rewrite)
  (implies (and (not (zerop temp))
                (numberp ans))
           (not (lessp (times (exp 2 ans) temp)
                       (exp 2 (*cl-log2-tagbody-0 ans temp))))))

;; The preceding approach's version of the lemma LOG-THM2 said:

;;     temp >= 1
;;   & ans >= 0
;;   & n < (2**ans) * (temp + 1)
;;     ==>
;;   n < 2 ** (2**(1 + (*cl-log2-tagbody-0 ans temp)))

;; This time, we do a bit of inequality reasoning to produce a
;; stronger lemma that does not mention n, and hence more directly
;; concerns the term (*CL-LOG2-TAGBODY-0 ANS TEMP) that we are trying
;; to reason about:

;;     temp >=1
;;   & ans >= 0
;;     ==>
;;   2 ** (1 + (*cl-log2-tagbody-0 ans temp))
;;   >=
;;   (2**ans) * (temp + 1)

(prove-lemma log-thm2 (rewrite)
  (implies (and (not (zerop temp))
                (numberp ans))
           (not (lessp (exp 2 (add1 (*cl-log2-tagbody-0 ans temp)))
                       (times (exp 2 ans) (add1 temp))))))

;; Since the two lemmas above capture the key properties of the loop
;; function, the main result may now be proved automatically.
;; (Technical point:  The two lemmas above are stored linear rules;
;; see comments above for more on this topic.  As in other events
;; above, we disable rules about EXP that could open up terms of the
;; form (EXP 2 (ADD1 x)) and thus prohibit the applicability of these
;; linear rules.)

(prove-lemma main ()
  (implies (not (zerop n))
           (and (not (lessp n (exp 2 (*cl-log2 t n))))
                (lessp n (exp 2 (add1 (*cl-log2 t n))))))
  ((enable integerp)
   (disable exp-add1 exp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; References                                                       ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

[1] D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M.
Saaltink.  EVES System Description.  In Proceedings of CADE-11.
Saratoga Springs, New York, June 1992.

[2] M. Kaufmann, ``A Verification System for a Subset of Common
Lisp,'' Internal Note 110, Computational Logic, Inc., January, 1989.

[3] M. Kaufmann, ``A User's Manual for RCL,'' Internal Note 157,
Computational Logic, Inc., October, 1989.

[4] R. S. Boyer and J S. Moore, ``A Computational Logic Handbook,''
Academic Press, Boston, 1988.

[5] R. S. Boyer and Yuan Yu, Automated Correctness Proofs of Machine
Code Programs for a Commercial Microprocessor, in D. Kapur, editor,
Automated Deduction -- CADE-11, Lecture Notes in Computer Science 607,
Springer-Verlag, pp. 416-430.

[6] Yuan Yu, Automated Proofs of Object Code for a Widely Used
Microprocessor, Ph. D. Dissertation, University of Texas at Austin,
December, 1992.

[7] David Guaspari, Carla Marceau, and Wolfgang Polak, ``Formal
Verification of Ada Programs,'' IEEE Transactions on Software
Engineering, vol. 16, no. 9, Sept. 1990, pp. 1058-1075.

|#