This file is adapted from books/models/jvm/m5/demo.script.

First evaluate the following shell commands.  The first will show
you a Java definition of a recursive factorial.  The second will
print the bytecode produced by Sun's javac compiler.

% cat Demo.java
% javap -c Demo
% java Demo 5
% java Demo 17

Point out the bytecode for fact, which starts on the line

 public static int fact(int);

Save that bytecode in a separate buffer, say, "fact".
The third command will run that bytecode on 5 and print 120.
The fourth produces a negative answer (32 bit int overflow).

Now start up ACL2 and execute:

(include-book "models/jvm/m5/jvm-fact-setup" :dir :system)
(in-package "M5")

(defun demo-fact (n)
  (let ((sched (fact-sched 0 n)))
    (list (list 'steps (len sched))
          (list 'ans 
                 (top
                  (stack
                   (top-frame 0
                              (run sched
                                   (make-state
                                    (list
                                     (cons 0
                                           (make-thread
                                            (push
                                             (make-frame
                                              0
                                              nil
                                              (push n nil)
                                              '((INVOKESTATIC "Demo" "fact" 1))
                                              'UNLOCKED
                                              "Demo")
                                             nil)
                                            'SCHEDULED
                                            nil)))
                                    *demo-heap*
                                    *demo-class-table*)))))))))

(lookup-method "fact" "Demo" *demo-class-table*)

will display the M5 bytecode corresponding to the fact method
just shown.  Compare it to the bytecode in buffer "fact" produced
earlier.  Then run

(demo-fact 5)

to execute the bytecode on 5 and get 120.

Now do 

(demo-fact 17)

You get the same answer as when we ran "java Demo 17" before.  It
is negative because of 32 bit int overflow, i.e., you get the
lower order 32 bits of the expected answer in twos-complement.

Compare with:

(int-fix (! 17))

That is the negative number fact is returning: ``the low order 32
bits of the true factorial''.

Now prove it:

(defthm fact-is-correct
  (implies (poised-to-invoke-fact th s n)
           (equal
            (run (fact-sched th n) s)
            (modify th s
             :pc (+ 3 (pc (top-frame th s)))
             :stack (push (int-fix (! n))
                          (pop (stack (top-frame th s)))))))
  :hints (("Goal"
           :induct (induction-hint th s n))))

The summary shows rules used in the proof.

The theorem above says that if you have an M5 state poised to
execute the fact method on n in thread th and if you run it a
certain number to steps on thread th, you just modify s by
incrementing the pc past the invoke instruction (which is 3
bytes) and popping the n off the stack and pushing the low order
32 bits of the true n!.