; Use of Tail-Recursion to Propagate Inductive Assertions
; J Strother Moore
; February 26, 2003

; cd /u/moore/m5/tolquhon
; (include-book "utilities")
; (ld "vcg-examples.lisp" :ld-pre-eval-print t)

; Certification:
; (include-book "utilities")
; (certify-book "vcg-examples" 1)

; ---------------------------------------------------------------------------
; Preliminaries

; This first part is just ``prelude''.  It has nothing to do with the
; specific programs we will verify.

(in-package "M5")

(include-book "defpun")

(defmacro defpun (g args &rest tail)
  `(acl2::defpun ,g ,args ,@tail))

;(ACL2::SET-MATCH-FREE-ERROR NIL)

(defthm update-nth-opener
  (and (equal (update-nth 0 x a) (cons x (cdr a)))
       (implies (not (zp n))
                (equal (update-nth n x a)
                       (cons (car a) (update-nth (- n 1) x (cdr a)))))))

; ---------------------------------------------------------------------------
; Some Preliminaries for Our First Program

(defthm int-evenp-inv-a
  (implies (intp i)
           (iff (evenp (int-fix (- i 2)))
                (evenp i)))
  :hints
  (("Goal" :in-theory (e/d (intp int-fix)
                           (floor)))))

(defthm int-evenp-inv-b
  (implies (intp i)
           (iff (evenp (- i 2))
                (evenp i)))
  :hints
  (("Goal" :in-theory (e/d (intp int-fix)
                           (floor)))))

(in-theory (disable evenp))

(defthm int-lemma2a
  (implies (and (intp x)
                (<= 0 x))
           (equal (int-fix (+ -2 x))
                  (+ -2 x)))
  :hints (("Goal" :in-theory (e/d (intp) nil))))

(defthm int-lemma2b
  (implies (and (intp x)
                (<= 0 x))
           (intp (+ -2 x)))
  :hints (("Goal" :in-theory (e/d (intp) nil))))

; ---------------------------------------------------------------------------
; Our First Program

; Below is an m5 program that decrements its first local, n, by 2 and
; iterates until the result is 0.  On each iteration it adds 1 to a
; local variable, a, which is initialized to 0.  The program ends with
; a HALT instruction, which puts the machine in an infinite loop, i.e.,
; executing HALT doesn't change the pc and the machine "stops."  Later
; we deal with the more realistic situation of a RETURN to some caller.
; We will prove that if the program below reaches the HALT instruction,
; the initial value, n0, of n was even and the result on the stack is
; n0/2.  This program does not terminate when n0 is odd.

; To make the program slightly simpler to deal with, I only consider
; the case where n0 is a non-negative int.  (Java programmers will note
; that the program actually halts for even negative ints, because of
; wrap-around.)

(defconst *flat-prog*
  '((iconst_0)      ; 0                                           
    (istore_1)      ; 1               a := 0;                     
    (iload_0)       ; 2  top of loop:                             
    (ifeq 14)       ; 3               if n=0, goto 17;            
    (iload_1)       ; 6                                           
    (iconst_1)      ; 7                                           
    (iadd)          ; 8                                           
    (istore_1)      ; 9               a := a+1;                   
    (iload_0)       ;10                                            
    (iconst_2)      ;11                                           
    (isub)          ;12                                           
    (istore_0)      ;13               n := n-2;                   
    (goto -12)      ;14               goto top of loop            
    (iload_1)       ;17                                           
    (halt)))        ;18

; Here is the ``semantics'' of the loop, in the case in interest.

(defun halfa (n a)
  (declare (xargs :measure (nfix n)))
  (if (zp n)
      a
    (halfa (- n 2) (int-fix (+ a 1)))))

; ---------------------------------------------------------------------------
; The Assertions at the Three Cut Points

; We will use a classic ``inductive assertion'' method.  The following
; function takes a state, s, and the ``initial'' value of n, n0, and
; states the assertions we wish to attach to pcs 0, 2, and 18.  These
; are the so-called ``cut points'' of my choice: the entry to the
; program, the top of the loop, and exit from the program.  

; The particular assertions are not my main interest in this paper.
; You can read them if you want.  The real nugget in this paper is not
; the assertions but the fact that I use tail recursion by step to
; propagate assertions from the cut points to all the pcs.

; That said, let me note that the assertions are complicated because
; they have to handle the fact that halfa tracks the program only as
; long as n stays non-negative.  Things would be simpler if I assumed
; that n0 was even.  But I like illustrating the capability of
; establishing conditions that hold for n0 in the event of
; termination.

(defun flat-pre-condition (n0 n)
  (and (equal n n0)
       (intp n0)
       (<= 0 n0)))

(defun flat-loop-invariant (n0 n a)
  (and (intp n0)
       (<= 0 n0)
       (intp n)
       (if (and (<= 0 n)
                (evenp n))
           (equal (halfa n a)
                  (halfa n0 0))
         (not (evenp n)))
       (iff (evenp n0) (evenp n))))

(defun flat-post-condition (n0 value)
  (and (evenp n0)
       (equal value (halfa n0 0))))

(defun flat-assertion (n0 th s)
  (let ((n (nth 0 (locals (top-frame th s))))
        (a (nth 1 (locals (top-frame th s)))))
    (and (equal (program (top-frame th s)) *flat-prog*)
         (case (pc (top-frame th s))
           (0 (flat-pre-condition n0 n))
           (2 (flat-loop-invariant n0 n a))
           (18 (let ((value (top (stack (top-frame th s)))))
                 (flat-post-condition n0 value)))
           (otherwise nil)))))

; Observe that the output condition is that n0 is even and that the
; top of the stack contains the semantic expression (halfa n0 0).
; We will later convert this to n0/2.

; ---------------------------------------------------------------------------
; The Invariant -- The Only New Idea in this Note 

; Here is the new idea.  I define the invariant for the program by
; using defpun.  The assertions are attached at the three cut points
; and all other statements inherit the invariant of the next
; statement.

(defpun flat-inv (n0 th s)
  (if (or (equal (pc (top-frame th s)) 0)
          (equal (pc (top-frame th s)) 2)
          (equal (pc (top-frame th s)) 18))
      (flat-assertion n0 th s)
    (flat-inv n0 th (step th s))))

; In one sense, the next lemma is just a technical lemma to force
; flat-inv to keep opening if it hasn't reached a cut point yet.  But
; in another sense, this lemma highlights the nice feature of this
; approach.  Suppose that in our function flat-assertion we had failed
; to supply a cut point for some loop.  Then we'll get a stack
; overflow from the repeated indefinite application of this rewrite
; rule.  But we do not have to prove we've cut every loop, because the
; flat-inv function is tail recursive and so was admitted by defpun.

; In the past when I've used the classic inductive invariant approach
; and used recursion in flat-inv to avoid an assertion at every pc, I
; had to invent some kind of measure (``distance to the next cut
; point'') to prove that I had cut every loop.  That annoyed me
; because in the classic inductive invariant approach that burden is
; merely pragmatic -- you had to cut every loop or you couldn't
; generate verification conditions.  But you didn't have to prove you
; had cut every loop.  In my past attempts to mimic this, I had to
; prove more stuff!

(defthm flat-inv-opener
  (implies (and (equal pc (pc (top-frame th s)))
                (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 2))
                (not (equal pc 18)))
           (equal (flat-inv n0 th s)
                  (flat-inv n0 th (step th s)))))

; ---------------------------------------------------------------------------
; The Verification Conditions

(defthm VC1
  (implies (flat-pre-condition n0 n) (flat-loop-invariant n0 n 0)))


(defthm VC2
  (implies (and (flat-loop-invariant n0 n a)
                (not (equal n 0)))
           (flat-loop-invariant n0 (int-fix (- n 2)) (int-fix (+ 1 a)))))

(defthm VC3
  (implies (and (flat-loop-invariant N0 n a)
                (EQUAL n 0))
           (flat-post-condition N0 a)))

(in-theory (disable flat-pre-condition
                    flat-loop-invariant
                    flat-post-condition))

; ---------------------------------------------------------------------------
; Using the VCs in the Operational Semantics

; So here is the key theorem of the inductive invariant approach, showing
; that inv is an invariant.

(defthm flat-inv-step
  (implies (flat-inv n0 th s)
           (flat-inv n0 th (step th s))))

; We can immediately conclude that flat-inv is an invariant under run,
; as long as the only thread we step is th.

(defun mono-threadedp (th sched)
  (if (endp sched)
      t
    (and (equal th (car sched))
         (mono-threadedp th (cdr sched)))))

(defthm flat-inv-run
  (implies (and (mono-threadedp th sched)
                (flat-inv n0 th s))
           (flat-inv n0 th (run sched s)))
  :rule-classes nil
  :hints (("Goal" :in-theory (e/d (run)(flat-inv-def)))))

; And so we're done.  If we plug in an initial state satisfying the
; invariant we get a final state satisfying it.  If the final state is
; supposed to have pc 18, then we can read out what the invariant
; tells us about that cut point.

(defthm flat-main
  (let ((s1 (run sched s0)))
    (implies (and (intp n0)
                  (<= 0 n0)
                  (equal (pc (top-frame th s0)) 0)
                  (equal (locals (top-frame th s0)) (list n0 any))
                  (equal (program (top-frame th s0)) *flat-prog*)
                  (mono-threadedp th sched)
                  (equal (pc (top-frame th s1)) 18))
             (and (evenp n0)
                  (equal (top (stack (top-frame th s1)))
                         (halfa n0 0)))))

  :hints (("Goal" :use
           (:instance flat-inv-run
                      (n0 n0)
                      (s s0)
                      (th th)
                      (sched sched))
           :in-theory (enable flat-pre-condition flat-post-condition)))
  :rule-classes nil)

; ---------------------------------------------------------------------------
; Getting Rid of the Semantic Function

; Now, following our standard paradigm, we get rid of halfa and
; introduce n/2 instead.  There is nothing new here, but I have to
; fight intp and int-fix.

(defthm int-back
  (implies (and (intp (+ a x))
                (integerp a)
                (<= 0 a)
                (integerp x)
                (<= 0 x)
                (integerp y)
                (<= 0 y)
                (<= y x))
           (intp (+ y a)))
  :hints (("Goal" :in-theory (enable intp))))

(defthm halfa-is-half
  (implies (and (intp n)
                (<= 0 n)
                (evenp n)
                (integerp a)
                (<= 0 a)
                (intp (+ (/ n 2) a)))
           (equal (halfa n a)
                  (+ (/ n 2) a)))
  :hints (("Goal" :in-theory (enable evenp))))

(defthm intp-half-n
  (implies (and (intp n)
                (<= 0 n)
                (evenp n))
           (intp (* 1/2 n)))
  :hints (("Goal" :in-theory (enable evenp intp))))

; ---------------------------------------------------------------------------
; The (Partial) Correctness Theorem for Half

; The following theorem summarizes what we now know.  Start with a a
; state running *flat-prog* from pc 0 with initial n=n0 and run it
; under an arbitrary mono-threaded schedule to get to s1.  Suppose n0
; is a non-negative int and the pc of s1 is 18.

; Then we conclude that n0 is even and that the top of the stack is
; n0/2.

(defthm flat-is-partially-correct
  (let ((s1 (run sched s0)))
    (implies (and (intp n0)
                  (<= 0 n0)
                  (equal (pc (top-frame th s0)) 0)
                  (equal (locals (top-frame th s0)) (list n0 any))
                  (equal (program (top-frame th s0)) *flat-prog*)
                  (mono-threadedp th sched)
                  (equal (pc (top-frame th s1)) 18))
             (and (evenp n0)
                  (equal (top (stack (top-frame th s1)))
                         (/ n0 2)))))  
  :rule-classes nil
  :hints (("Goal"
           :use ((:instance flat-main)))))

; Note that at no point in this exercise have we counted instructions
; or defined a clock or schedule generator.

; ---------------------------------------------------------------------------
; Dealing with Return

(defconst *half-prog*
  '((iconst_0)      ; 0                                           
    (istore_1)      ; 1               a := 0;                     
    (iload_0)       ; 2  top of loop:                             
    (ifeq 14)       ; 3               if n=0, goto 17;            
    (iload_1)       ; 6                                           
    (iconst_1)      ; 7                                           
    (iadd)          ; 8                                           
    (istore_1)      ; 9               a := a+1;                   
    (iload_0)       ;10                                            
    (iconst_2)      ;11                                           
    (isub)          ;12                                           
    (istore_0)      ;13               n := n-2;                   
    (goto -12)      ;14               goto top of loop            
    (iload_1)       ;17                                           
    (ireturn)))     ;18               return a;

(defun sdepth (stk)
  (declare (xargs :hints (("Goal" :in-theory (enable pop)))))
  (if (endp stk)
      0
    (+ 1 (sdepth (pop stk)))))

(defun half-assertion (n0 d0 th s)
  (cond
   ((< (sdepth (call-stack th s)) d0)
    (let ((value (top (stack (top-frame th s)))))
      (flat-post-condition n0 value)))
   (t
    (let ((n (nth 0 (locals (top-frame th s))))
          (a (nth 1 (locals (top-frame th s)))))
      (and (equal (sdepth (call-stack th s)) d0)
           (equal (program (top-frame th s)) *half-prog*)
           (equal (sync-flg (top-frame th s)) 'UNLOCKED)
           (case (pc (top-frame th s))
             (0 (flat-pre-condition n0 n))
             (2 (flat-loop-invariant n0 n a))
             (18 (let ((value (top (stack (top-frame th s)))))
                   (flat-post-condition n0 value)))
             (otherwise nil)))))))

(defpun half-inv (n0 d0 th s)
  (if (or (< (sdepth (call-stack th s)) d0)
          (equal (pc (top-frame th s)) 0)
          (equal (pc (top-frame th s)) 2)
          (equal (pc (top-frame th s)) 18))
      (half-assertion n0 d0 th s)
    (half-inv n0 d0 th (step th s))))

(defthm half-inv-opener
  (implies (and (equal pc (pc (top-frame th s)))
                (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 2))
                (not (equal pc 18)))
           (equal (half-inv n0 d0 th s)
                  (if (< (sdepth (call-stack th s)) d0)
                      (half-assertion n0 d0 th s)
                    (half-inv n0 d0 th (step th s))))))

(defthm half-inv-step
  (implies (and (integerp d0)
                (< 1 d0)
                (<= d0 (sdepth (call-stack th s)))
                (half-inv n0 d0 th s))
           (half-inv n0 d0 th (step th s)))
  :hints (("Goal" :in-theory (disable halfa-is-half))))

(defun run-to-return (sched th d0 s)
  (cond ((endp sched) s)
        ((<= d0 (sdepth (call-stack th s)))
         (run-to-return (cdr sched) th d0 (step (car sched) s)))
        (t s)))

(defthm half-inv-run-to-return
  (implies (and (mono-threadedp th sched)
                (integerp d0)
                (< 1 d0)
                (half-inv n0 d0 th s))
           (half-inv n0 d0 th (run-to-return sched th d0 s)))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable half-inv-def))))

; And so we're done.  If we plug in an initial state satisfying the
; invariant we get a final state satisfying it.  If the final state is
; supposed to have pc 18, then we can read out what the invariant
; tells us about that cut point.

(defthm half-main
  (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
    (implies (and (intp n0)
                  (<= 0 n0)
                  (equal (pc (top-frame th s0)) 0)
                  (equal (locals (top-frame th s0)) (list n0 any))
                  (equal (program (top-frame th s0)) *half-prog*)
                  (equal (sync-flg (top-frame th s0)) 'unlocked)
                  (< 1 (sdepth (call-stack th s0)))
                  (mono-threadedp th sched)
                  (< (sdepth (call-stack th s1))
                     (sdepth (call-stack th s0))))
             (and (evenp n0)
                  (equal (top (stack (top-frame th s1)))
                         (halfa n0 0)))))
  :hints (("Goal" :use
           (:instance half-inv-run-to-return
                      (n0 n0)
                      (d0 (sdepth (call-stack th s0)))
                      (s s0)
                      (th th)
                      (sched sched))
           :in-theory (enable flat-pre-condition
                              flat-post-condition)))
  :rule-classes nil)

(defthm half-partially-correct
  (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
    (implies (and (intp n0)
                  (<= 0 n0)
                  (equal (pc (top-frame th s0)) 0)
                  (equal (locals (top-frame th s0)) (list n0 any))
                  (equal (program (top-frame th s0)) *half-prog*)
                  (equal (sync-flg (top-frame th s0)) 'unlocked)
                  (< 1 (sdepth (call-stack th s0)))
                  (mono-threadedp th sched)
                  (< (sdepth (call-stack th s1))
                     (sdepth (call-stack th s0))))
             (and (evenp n0)
                  (equal (top (stack (top-frame th s1)))
                         (/ n0 2)))))
  :hints (("Goal" :use half-main))
  :rule-classes nil)

; ---------------------------------------------------------------------------
; Doing a Sum Program

; To re-illustrate the same methodology, without worrying about
; demonstrating that we can conclude things about the input if we're
; told we terminate, here is a program that sums the ints from n0 down
; to 0.

(defconst *sum-prog*   
                    ; We name local[0] n and local[1] a.
  '((iconst_0)      ; 0                                           
    (istore_1)      ; 1               a := 0;                     
    (iload_0)       ; 2  top of loop:                             
    (ifeq 14)       ; 3               if n=0, goto 17;            
    (iload_0)       ; 6                                           
    (iload_1)       ; 7                                           
    (iadd)          ; 8                                           
    (istore_1)      ; 9               a := n+a;                   
    (iload_0)       ;10                                            
    (iconst_m1)     ;11                                           
    (iadd)          ;12                                           
    (istore_0)      ;13               n := n-1;                   
    (goto -12)      ;14               goto top of loop            
    (iload_1)       ;17                                           
    (ireturn)))     ;18               return a;
    
(defun suma (n a)
  (if (zp n)
      a
    (suma (- n 1) (int-fix (+ n a)))))

(defun sum-pre-condition (n0 n)
  (and (equal n n0)
       (intp n0)
       (<= 0 n0)))  

(defun sum-loop-invariant (n0 n a)
  (and (intp n0)
       (intp n)
       (<= 0 n)
       (<= n n0)
       (equal (suma n a)
              (suma n0 0))))

(defun sum-post-condition (n0 value)
  (equal value (suma n0 0)))

(defun sum-assertion (n0 d0 th s)
  (cond ((< (sdepth (call-stack th s)) d0)
         (let ((value (top (stack (top-frame th s)))))
           (sum-post-condition n0 value)))
        (t
         (let ((n (nth 0 (locals (top-frame th s))))
               (a (nth 1 (locals (top-frame th s)))))
           (and (equal (sdepth (call-stack th s)) d0)
                (equal (program (top-frame th s)) *sum-prog*)
                (equal (sync-flg (top-frame th s)) 'UNLOCKED)
                (case (pc (top-frame th s))
                  (0 (sum-pre-condition n0 n))
                  (2 (sum-loop-invariant n0 n a))
                  (18 (let ((value (top (stack (top-frame th s)))))
                        (sum-post-condition n0 value)))
                  (otherwise nil)))))))

(defpun sum-inv (n0 d0 th s)
  (if (or (< (sdepth (call-stack th s)) d0)
          (equal (pc (top-frame th s)) 0)
          (equal (pc (top-frame th s)) 2)
          (equal (pc (top-frame th s)) 18))
      (sum-assertion n0 d0 th s)
    (sum-inv n0 d0 th (step th s))))

(defthm sum-inv-opener
  (implies (and (equal pc (pc (top-frame th s)))
                (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 2))
                (not (equal pc 18)))
           (equal (sum-inv n0 d0 th s)
                  (if (< (sdepth (call-stack th s)) d0)
                      (sum-assertion n0 d0 th s)
                    (sum-inv n0 d0 th (step th s))))))

(defthm sum-VC1
  (implies (sum-pre-condition n0 n) (sum-loop-invariant n0 n 0)))

(defthm sum-VC2
  (implies (and (sum-loop-invariant n0 n a)
                (not (equal n 0)))
           (sum-loop-invariant n0 (int-fix (- n 1)) (int-fix (+ n a)))))

(defthm sum-VC3
  (implies (and (sum-loop-invariant N0 n a)
                (EQUAL n 0))
           (sum-post-condition N0 a)))

(in-theory (disable sum-pre-condition
                    sum-loop-invariant
                    sum-post-condition))

(defthm sum-inv-step
  (implies (and (integerp d0)
                (< 1 d0)
                (<= d0 (sdepth (call-stack th s)))
                (sum-inv  n0 d0 th s))
           (sum-inv n0 d0 th (step th s))))

(defthm sum-inv-run-to-return
  (implies (and (mono-threadedp th sched)
                (integerp d0)
                (< 1 d0)
                (sum-inv n0 d0 th s))
           (sum-inv n0 d0 th (run-to-return sched th d0 s)))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable sum-inv-def))))

(defthm sum-main
  (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
    (implies (and (intp n0)
                  (<= 0 n0)
                  (equal (pc (top-frame th s0)) 0)
                  (equal (locals (top-frame th s0)) (list n0 any))
                  (equal (program (top-frame th s0)) *sum-prog*)
                  (equal (sync-flg (top-frame th s0)) 'unlocked)
                  (< 1 (sdepth (call-stack th s0)))
                  (mono-threadedp th sched)
                  (< (sdepth (call-stack th s1))
                     (sdepth (call-stack th s0))))
             (equal (top (stack (top-frame th s1)))
                    (suma n0 0))))
  :hints (("Goal" :use
           (:instance sum-inv-run-to-return
                      (n0 n0)
                      (d0 (sdepth (call-stack th s0)))
                      (s s0)
                      (th th)
                      (sched sched))
           :in-theory (enable sum-pre-condition
                              sum-post-condition)))
  :rule-classes nil)

; We don't bother to eliminate suma, though we could if we hacked around
; with intp long enough!

; ---------------------------------------------------------------------------
; A Recursive Method

; Now let's do recursive factorial.   We'll bring in the clocked work 
; we have already done, just to have the *demo-state* etc.

(include-book "demo")

(defun ! (n)
  (if (zp n)
      1
    (* n (! (- n 1)))))

; Here is the (redundant) definition of the program.

(defconst *fact-def*
  '("fact" (INT) NIL
    (ILOAD_0)                         ;;;  0
    (IFLE 12)                         ;;;  1
    (ILOAD_0)                         ;;;  4
    (ILOAD_0)                         ;;;  5
    (ICONST_1)                        ;;;  6
    (ISUB)                            ;;;  7
    (INVOKESTATIC "Demo" "fact" 1)    ;;;  8
    (IMUL)                            ;;; 11
    (IRETURN)                         ;;; 12
    (ICONST_1)                        ;;; 13
    (IRETURN)))                       ;;; 14

; The following function recognizes the call stack (cs) of a call of
; the "fact" method on n0.  The function is not applied to the
; top-most frame, because the constraints on the frame are so
; pc-sensitive and the top-most frame may have "any" pc.  So the
; function actually recognizes the rest of the "fact" call stack.
; Here is a picture of the entire call stack.

; -------------------   top-most frame
; pc:       any
; locals:   (n)          5  <- suppose n=5
; stack:    any
; program:  fact prog
; -------------------   caller-frame 
; pc:       11
; locals:   (n+1)        6     this is caller-frame 3
; stack:    (n+1)
; program:  fact prog
; -------------------   caller-frame
; pc:       11
; locals:   (n+2)        7     this is caller-frame 2
; stack:    (n+2)
; program:  fact prog
; -------------------   caller-frame
; ...
; -------------------   caller-frame
; pc:       11
; locals:   (n0)         8  <- suppose n0 = 8 ; this is caller frame 1
; stack:    (n0)
; program:  fact prog
; -------------------   the frame below called fact on n0
; ...                   this is caller frame 0

; Note that there are n0-n fact caller frames.  We number them from
; n0-n down to 1.  Caller frame 0 is actually the ``external'' entry
; into fact on n0.  We don't know (or care) whether fact or some other
; program is running there.  Let k be the number of the caller frame.
; Then note that the value of n in that frame is n0-k+1.

(defun fact-caller-framesp (cs n0 k)
  (declare (xargs :measure (acl2-count k)))
  (cond ((zp k) t)
        ((and (equal (pc (top cs)) 11)
              (equal (program (top cs)) (cdddr *fact-def*))
              (equal (sync-flg (top cs)) 'UNLOCKED)
              (intp (nth 0 (locals (top cs))))
              (equal (+ n0 (- k)) (- (nth 0 (locals (top cs))) 1))
              (equal (nth 0 (locals (top cs)))
                     (top (stack (top cs)))))
         (fact-caller-framesp (pop cs) n0 (- k 1)))
        (t nil)))

(defun fact-assertion (n0 d0 th s)
  (cond
   ((< (sdepth (call-stack th s)) d0)
    (equal (top (stack (top-frame th s)))
           (int-fix (! n0))))
   (t
    (let ((n (nth 0 (locals (top-frame th s)))))
      (and (equal (program (top-frame th s)) (cdddr *fact-def*))
           (equal (lookup-method "fact" "Demo" (class-table s))
                  *fact-def*)
           (equal (sync-flg (top-frame th s)) 'UNLOCKED)
           (intp n0)
           (intp n)
           (<= 0 n)
           (<= n n0)
           (equal (sdepth (call-stack th s)) (+ d0 (- n0 n)))
           (fact-caller-framesp (pop (call-stack th s)) n0 (- n0 n))
           (case (pc (top-frame th s))
             (0 t)
             ((12 14) (equal (top (stack (top-frame th s)))
                             (int-fix (! n))))
             (otherwise nil)))))))

(defpun fact-inv (n0 d0 th s)
  (if (or (< (sdepth (call-stack th s)) d0)
          (equal (pc (top-frame th s)) 0)
          (equal (pc (top-frame th s)) 12)
          (equal (pc (top-frame th s)) 14))
      (fact-assertion n0 d0 th s)
    (fact-inv n0 d0 th (step th s))))

(defthm fact-inv-opener
  (implies (and (equal pc (pc (top-frame th s)))
                (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 12))
                (not (equal pc 14)))
           (equal (fact-inv n0 d0 th s)
                  (if (< (sdepth (call-stack th s)) d0)
                      (fact-assertion n0 d0 th s)
                    (fact-inv n0 d0 th (step th s))))))

; These next three lemmas are technical.  The first two force
; substitutions.  The last opens the stack predicate when we're
; returning and need to know what we're being told about the caller.

(DEFTHM KB-HACK1
  (IMPLIES
   (AND
    (FACT-CALLER-FRAMESP
     (POP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))
     N0
     (+ -1 N0 (- NNN)))
    (EQUAL
     NNN
     (+ -1
        (CAR (LOCALS (TOP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))))))
   (FACT-CALLER-FRAMESP
    (POP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))
    N0
    (+
     N0
     (-
      (CAR (LOCALS (TOP (POP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))))))))

(defthm kb-hack2
  (implies
   (and (integerp n)
        (EQUAL
         tos
         (INT-FIX
          (! (CAR (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))))))))

   (EQUAL
    (INT-FIX (* tos n))
    (INT-FIX
     (* (! (CAR (LOCALS (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S)))))))
        n)))))

(defthm fact-caller-framesp-opener-1
  (implies (and (syntaxp
                 (equal cs
                        '(POP (CAR (CDR (ASSOC-EQUAL TH (THREAD-TABLE S)))))))
                (EQUAL (PC (TOP (CADR (ASSOC-EQUAL TH (THREAD-TABLE S))))) pc0)
                (syntaxp (or (equal pc0 ''12) (equal pc0 ''14))))
           (equal (fact-caller-framesp cs n0 k)
                  (COND ((ZP K) T)
                        ((AND (EQUAL (PC (TOP CS)) 11)
                              (EQUAL (PROGRAM (TOP CS))
                                     (CDDDR *FACT-DEF*))
                              (EQUAL (SYNC-FLG (TOP CS)) 'UNLOCKED)
                              (INTP (NTH 0 (LOCALS (TOP CS))))
                              (EQUAL (+ N0 (- K))
                                     (- (NTH 0 (LOCALS (TOP CS))) 1))
                              (EQUAL (NTH 0 (LOCALS (TOP CS)))
                                     (TOP (STACK (TOP CS)))))
                         (FACT-CALLER-FRAMESP (POP CS)
                                              N0 (- K 1)))
                        (T NIL)))))

(defthm fact-inv-step
  (implies (and (integerp d0)
                (< 1 d0)
                (<= d0 (sdepth (call-stack th s)))
                (fact-inv n0 d0 th s))
           (fact-inv n0 d0 th (step th s))))

(defthm fact-inv-run-to-return
  (implies (and (mono-threadedp th sched)
                (integerp d0)
                (< 1 d0)
                (fact-inv n0 d0 th s))
           (fact-inv n0 d0 th (run-to-return sched th d0 s)))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable fact-inv-def))))

; Here is the main theorem.  It opens by letting s1 be a run-to-return
; of s0.  That particular call runs s0 with an abitrarily long
; schedule, sched.  Note that run-to-return does not always return a
; state that has returned to a shorter call-stack depth -- if the
; schedule is exhausted before that happens, the final state may still
; be as deep or deeper than the initial state.  In any case, s0 is the
; initial state and s1 is the final state.

; Now let's read the hypotheses of the implication.  There are five
; blocks of hypotheses.  The first says that n0 is a positive intp.
; The second says that the top-frame of thread th of s0 is a call of
; our "fact" method on n0.  The third says that the depth of the
; call-stack of thread th is greater than 1.  That means there is a
; frame under the call of "fact".  We will call that frame the
; ``caller's frame.''  Of course, if s1 has a shorter call-stack than
; s0, then the caller's frame will be its top-frame, since
; run-to-return stops as soon as we've returned to that depth.  The
; fourth says the schedule consists of nothing but th steps.  Note
; that otherwise we say nothing about the schedule -- it may be
; arbitrarily long.  The fifth block says that the depth of the call
; stack of s1 is less than that of s0, so we know the initial state
; did run long enough to return and hence, the caller's frame is the
; top-frame of s1.

; Then the conclusion is that (int-fix (! n0)) is on top of
; the stack of the caller's frame.

(defthm fact-main
  (let ((s1 (run-to-return sched th (sdepth (call-stack th s0)) s0)))
    (implies (and (intp n0)
                  (<= 0 n0)

                  (equal (pc (top-frame th s0)) 0)
                  (equal (locals (top-frame th s0)) (list n0))
                  (equal (program (top-frame th s0))
                         (cdddr *fact-def*))
                  (equal (sync-flg (top-frame th s0)) 'unlocked)
                  (equal (lookup-method "fact" "Demo" (class-table s0))
                         *fact-def*)

                  (< 1 (sdepth (call-stack th s0)))
                  
                  (mono-threadedp th sched)
                  
                  (< (sdepth (call-stack th s1))
                     (sdepth (call-stack th s0))))
             (equal (top (stack (top-frame th s1)))
                    (int-fix (! n0)))))

  :hints (("Goal" 
           :use
           (:instance fact-inv-run-to-return
                      (n0 n0)
                      (d0 (sdepth (call-stack th s0)))
                      (s s0)
                      (th th)
                      (sched sched))))
  :rule-classes nil)

; ---------------------------------------------------------------------------
; The Basic Relation Between Run-to-Return and Run

(defun sched-to-return (sched th d0 s)
  (cond ((endp sched) sched)
        ((<= d0 (sdepth (call-stack th s)))
         (sched-to-return (cdr sched) th d0 (step (car sched) s)))
        (t sched)))

(defthm run-to-return-v-run
  (equal (run sched s)
         (run (sched-to-return sched th d0 s)
              (run-to-return sched th d0 s)))
  :rule-classes nil)

; I need to develop the compositional rules.