CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

Project 1, Due 10/6/2002 (before midnight)

Note: Make sure that you allocate enough time to the project. As a rough guideline, I suggest that you complete parts 1 and 2 below by September 25.

1. ACL2 Warm Up. Read chapters 3, 4 (section 4.6 is optional), and 5 of CAR (Computer-Aided Reasoning) and check your understanding by doing the exercises as you go. Hand in your solutions to the exercises below. The exercises must be done with ACL2, that is, test your solutions using the ACL2 system (instructions on how to access ACL2 locally appear here).
   • Define (depth-tip d x) so that it returns all tips of x occuring at depth d. See section 3.6.3 of the book for the definitions of tip and depth.
   • Define (bind x y alist) to return an alist that differs from alist only in that x is bound y. More precisely, if x appears as a key in alist, then the first such occurence should be replaced by (x . y), otherwise (if x is not a key in alist), (x . y) should be added to the end of alist.
   • I will give you a specification for <<=. The specification is partial in that it only tells you what the value of <<= is when comparing rationals and conses, all of whose tips are rationals. Since functions in ACL2 are total, you are free to define a function that behaves as specified on the intended domain and does whatever you want on other objects. A rational x is <<= a rational y iff (if and only if) x <= y. If x is a rational and y is a cons, x is <<= y. If both x and y are conses, then x is <<= y iff:
     1. The length of x is less than the length of y, or
     2. All of the following three conditions hold.
        1. The length of x is the same as the length of y; and
        2. the car of x is <<= the car of y; and
        3. the cdr of x is <<= the cdr of y .
     Define (<<= x y) based on the description above. Define (isort x) so that it sorts a list using <<=.
   • Guard verification (see section 3.8 of the book) is used to show that if the inputs to a function satisfy the guard conjecture, then any function call resulting from a call of the verified function is Common Lisp compliant. This allows for efficient execution of verified functions, as is discussed in the book. When specifying and verifying guards, one often has to prove theorems about the type of the return value of a function when its input satisfies the guard conjecture. It would be helpful to be able to specify the return type next to the guard condition. Define defun-g, a simple macro to do this. Consider the following example:

     	  
     :trans1
     (defun-g set-union (X Y)
       "set union, i.e., X U Y"
       (declare (xargs :guard (true-listp X)))
       ((implies (true-listp Y) (true-listp (set-union X Y))) 
        :rule-classes :type-prescription)
       (if (endp X)
           Y
         (cons (car X)
     	  (set-union (cdr X) Y))))
     
     

     which returns

     
     (PROGN
      (DEFUN SET-UNION (X Y)
        "SET UNION, I.E., X U Y"
        (DECLARE (XARGS :GUARD (TRUE-LISTP X)))
        (IF (ENDP X)
            Y (CONS (CAR X)
     	       (SET-UNION (CDR X) Y))))
     
      (DEFTHM SET-UNION-RETURN-TYPE
        (IMPLIES (TRUE-LISTP Y)
     	    (TRUE-LISTP (SET-UNION X Y)))
        :RULE-CLASSES :TYPE-PRESCRIPTION))
     
     

     So defun-g takes an extra argument that appears after the declaration and generates two events: a defun, as expected, and the extra argument is turned into a defthm whose name is derived from the defun.
     1. Write a function make-sym that given symbols s and suf, returns the symbol s-suf in the package of s; specify and verify the guard of make-sym. (ACL2 should do the verification automatically.)
     2. Use make-sym to write the defun-g macro.

     Hint: Refer to the ACL2 online documentation for functions that manipulate symbols, the definition of true-listp, progn, defthm, etc.

2. Modeling processors in ACL2. We will use ACL2 to model processors. Once you go through the above intro to ACL2, you are ready to read the following paper which describes the general approach.

   Mechanized Formal Reasoning about Programs and Computing Machines, Bob Boyer and J Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996. A pdf version is also available.

   This paper explains a formalization style that has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2. This paper presents the so-called "small machine" model, an extremely simple processor whose state consists of the program counter, a RAM, an execute-only program space, a control stack and a flag. The paper explains how to prove theorems about such models.

   Read up to the end of section 4.4 carefully and briefly skim the rest of the paper.

   An ACL2 file with the relevant definitions can be found here.

   Notice that what we have is a simulator for the small machine and what is interesting about the paper is that it then goes on to describe how one can state, prove, and mechanically verify theorems about the simulator.

   Write a pair of functions fact-program and fact-clock so that for any natural number, n

   	
   (equal (car (mem (sm (fact-state n)
   		     (fact-clock n))))
          (fact n))
   	 
   	

   is a theorem, where fact and fact-state are defined as follows.

   	
   (defun fact (n)
     (if (zp n)
         1
       (* n (fact (1- n)))))
   
   (defun fact-state (n)
     (st :pc   '(fact . 0)
         :stk   nil
         :mem  `(,n)
         :halt nil
         :code (list (times-program) (fact-program))))
   	 
   	

   That is, (sm (fact-state n) (fact-clock n)) is a state with a memory whose first element is n! (n factorial). Times-program and the other functions appearing in the above expression are in the ACL2 file mentioned above. Try your solution with the following values for n: 7, 15, 22. You may have to compile your definitions if you run into stack overflows (type (comp t) at the command prompt). If your solutions are correct, then ACL2 should prove theorems of the following form (automatically).

   	
   (defthm fact-theorem-7
     (equal (car (mem (sm (fact-state 7)
                          (fact-clock 7))))
            (fact 7)))
   	 
   	

   For this part of the project, submit your definitions of the functions fact-program and fact-clock and defthms fact-theorem-7, fact-theorem-15, fact-theorem-22, where fact-theorem-7 is as above and the other defthms are the same, except occurences of 7 are replaced by 15 and 22.

3. A JVM-like processor in ACL2. This part of the project requires that you write two simulators for JVM-like languages. The first simulator describes a JVM-like language at a higher level of abstraction than the second. The simulators will act as specifications for the machine we build on hardware.
   1. First we examine bit vectors in ACL2. This is important because the arithmetic and logical operations of our JVM-like machines are on 32-bit numbers. Read about bit-vectors here.
   2. The first JVM-like machine is called the iJVM. The specification of the iJVM along with instructions on what you have to submit can be found here.
   3. The second JVM-like machine is called the iJVM2. The specification of the iJVM2 along with instructions on what you have to submit can be found here.
   4. Optional: Characterize the relationship between the two simulators. Here are some suggestions:
      • Try to do this precisely using English.
      • What theorem would you prove relating the two?
      • Write a compiler in ACL2 from iJVM to iJVM2. What does it mean for the compiler to be correct?

   Sumbission Instructions

   Create an archive of the files using tar or winzip (if you want to use something else, ask first to make sure we can unarchive it) and send us the archive (as a single attatchement) via email. The email should be sent both to me and to Vernard (vernard@cc).