#||
======================================================================
Using defattach for execution of constrained functions
Nathan Wetzler
September 8, 2011
======================================================================

Abstract:
Defattach is a relatively new feature in ACL2 that allows the user to
extend the current theory with executability in a consistent manner.
In this talk, we will begin by discussing the use of encapsulate to
introduce constrained functions.  Next, we will introduce defattach
and look at its effect on the current theory.  We will then provide
some examples of defattach and give motivation for its use.  Finally,
we will examine a specific case of using defattach where the
constrained function bodies are the same as the executable function
bodies.



======================================================================
Outline
======================================================================

Encapsulate
  Definition
  Modifications to theory
  Uses
Defattach
  Definition
  Proof
  Modifications to theory
  Uses
Case study:  Constrained = Executable
Case study:  Non-local defun in encapsulate
Case study:  Non-local defun-sk in encapsulate...




======================================================================
Encapsulate
======================================================================

------------------------------------------------------------
Definition
------------------------------------------------------------

The general form of an encapsulate:

(encapsulate
 (sig1
  sig2
  ...)
  
 (local
  (witness-to-sig1))
 (local
  (witness-to-sig2))
 ...

 (defthm exported-theorem-about-sigs
   ...)
 (defthm exported-theorem-about-sigs
   ...)
 )


We introduce constrained functions that are bound to the signatures 
listed in the encapsulate.  These functions satsify the theorems from
inside the encapsulate.  Furthermore, the theorems form a consistent
theory.




------------------------------------------------------------
Modifications to theory (encapsulate)
------------------------------------------------------------

||#

; Let's do some quick housekeeping!

; needed for one of our proofs later
(include-book "arithmetic-5/top" :dir :system)

; handy macro to print the theory since a marker called "start"
(defmacro print-theory-since-start ()
  `(let ((world (w state)))
     (set-difference-theories (current-theory :here)
                              (theory 'start))))

; make a marker for our base theory
(deftheory start (current-theory :here))




; First, let's see how a function and a theorem affect our current
; theory.


; define a function
(defun f (x y)
  (+ x y))

; and a theorem
(defthm f-commutes
  (implies (and (integerp x)
                (integerp y))
           (equal (f y x)
                  (f x y))))

; and see how it affect the theory
(print-theory-since-start)

; undo back to the start
(ubu! 'start)





; Now let's define a simple encapsulate and see how it affects the
; current theory.


; begin our encapsulate
(encapsulate
 (((f * *) => *)     ; two constrained functions of two arguments
  ((g * *) => *))
 
 (local              ; local witnesses for the contstrained functions
  (defun f (x y)
    (+ x y)))

 (local
  (defun g (x y)
    (- x y)))


 (defthm f-commutes               ; some nice theorems about f and g
   (implies (and (integerp x)     ; or "constraints"
                 (integerp y))
            (equal (f y x)
                   (f x y))))

 (defthm g-does-not-commute
   (implies (and (integerp x)
                 (integerp y)
                 (not (equal x y)))
            (not (equal (g y x)
                        (g x y)))))
 )

(print-theory-since-start)

(ubu! 'start)





#||

------------------------------------------------------------
Uses of encapsulate
------------------------------------------------------------

Generally, encapsulate is used to introduce a theory about functions
that we would rather leave abstract.

There is a special case where an encapsulate has no constrained 
functions.  This form is often used when we wish to "box up" part of a
proof.  For example, we might wish to hide certain theorems from the
rest of a proof by making them local inside an encapsulate (and then 
making the "main theorem" non-local").





======================================================================
Defattach
======================================================================

------------------------------------------------------------
Definition
------------------------------------------------------------

The general form of a defattach:

(defattach (f1 g1)
           (f2 g2)
           ...)


We extend the current theory with a new "evaluation theory" that 
allows constrained functions f1, f2, ... to be executed.




------------------------------------------------------------
Proof
------------------------------------------------------------

There are two major sections to the "defattach proof".

First, we prove, for each attachment, that the guard of the 
constrained function implies the guard of the attached function.  Each
of these proofs are executed separately. ("executed" might not be the
right term)

Second, we prove that the constraints are satisfied by the attached
functions via functional instantiation.  Because this proof is about 
the constraint surrounding the constrained functions, it appears as 
a conjunction of all the events on the encapsulate.  This conjunction 
will immediately break down into several subgoals.


Sometimes we need hints for the defattach proof.  The location of the
hints make sense given the structure of the proof above:

(defattach (f1 g1 :hints hints-for-guard-proof)
           (f2 g2 :hints hints-for-guard-proof)
           :hints hints-for-constraint-proof)




------------------------------------------------------------
Modifications to theory (defattach)
------------------------------------------------------------

||#

; first, we introduce constrained functions f and g as before
(encapsulate
 ; note that this time we've added guards to the constrained functions
 (((f * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y)))
  ((g * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y))))
 
 ; and guards to the witnesses
 (local
  (defun f (x y)
    (+ x y)))

 (local
  (defun g (x y)
    (- x y)))


 (defthm f-commutes
   (implies (and (integerp x)
                 (integerp y))
            (equal (f y x)
                   (f x y))))

 (defthm g-does-not-commute
   (implies (and (integerp x)
                 (integerp y)
                 (not (equal x y)))
            (not (equal (g y x)
                        (g x y)))))
 )


; now, we define our attached functions
(defun f-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (* x y))

(defun g-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (< x y))


; and finally, we make the attachment
(defattach (f f-exec)
           (g g-exec))


(print-theory-since-start)

(ubu! 'start)





#||

------------------------------------------------------------
Uses of defattach
------------------------------------------------------------

Stealing from Matt and the documentation:
(1) Constrained function execution
(2) Sound modification of the ACL2 system
(3) Program refinement

Matt to say a few words about the last two items?




======================================================================
Case study:  Constrained = Executable
======================================================================

||#


(encapsulate
 (((f * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y)))
  ((g * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y))))
 
 (local
  (defun f (x y)
    (declare (xargs :guard (and (integerp x)
                                (integerp y))))
    (+ x y)))
 (local
  (defun g (x y)
    (declare (xargs :guard (and (integerp x)
                                (integerp y))))
    (- x y)))

 (defthm f-commutes
   (implies (and (integerp x)
                 (integerp y))
            (equal (f y x)
                   (f x y))))
 (defthm g-does-not-commute
   (implies (and (integerp x)
                 (integerp y)
                 (not (equal x y)))
            (not (equal (g y x)
                        (g x y)))))
 )


(defun f-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (+ x y))

(defun g-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (- x y))



(defthm f-exec-commutes
  (implies (and (integerp x)
                (integerp y))
           (equal (f-exec y x)
                  (f-exec x y))))
(defthm g-exec-does-not-commute
  (implies (and (integerp x)
                (integerp y)
                (not (equal x y)))
           (not (equal (g-exec y x)
                       (g-exec x y)))))

(defattach (f f-exec)
           (g g-exec)
           :hints (("Goal"
                    :use ((:instance f-exec-commutes)
                          (:instance g-exec-does-not-commute)))))

(ubu! 'start)







; Now let's do that again, but using Matt's suggestion from last 
; week's seminar.  This minimizes the proof effort.

(defun f-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (+ x y))

(defun g-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (- x y))


(defthm f-exec-commutes
  (implies (and (integerp x)
                (integerp y))
           (equal (f-exec y x)
                  (f-exec x y))))
(defthm g-exec-does-not-commute
  (implies (and (integerp x)
                (integerp y)
                (not (equal x y)))
           (not (equal (g-exec y x)
                       (g-exec x y)))))

(defthm defattach-proof
  (and (implies (and (integerp x)
                     (integerp y))
                (equal (f-exec y x)
                       (f-exec x y)))
       (implies (and (integerp x)
                     (integerp y)
                     (not (equal x y)))
                (not (equal (g-exec y x)
                            (g-exec x y)))))
  :hints (("Goal"
           :in-theory (disable f-exec
                               g-exec))
          ("Subgoal 2"
           :by (:instance f-exec-commutes))
          ("Subgoal 1"
           :by (:instance g-exec-does-not-commute))))

; alternatively
;; (defthm defattach-proof
;;   (and (implies (and (integerp x)
;;                      (integerp y))
;;                 (equal (f-exec y x)
;;                        (f-exec x y)))
;;        (implies (and (integerp x)
;;                      (integerp y)
;;                      (not (equal x y)))
;;                 (not (equal (g-exec y x)
;;                             (g-exec x y)))))
;;   :hints (("Goal"
;;            :in-theory (theory 'minimal-theory)
;;            :use (f-exec-commutes g-exec-does-not-commute))))



(encapsulate
 (((f * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y)))
  ((g * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y))))
 
 (local
  (defun f (x y)
    (declare (xargs :guard (and (integerp x)
                                (integerp y))))
    (f-exec x y)))
 (local
  (defun g (x y)
    (declare (xargs :guard (and (integerp x)
                                (integerp y))))
    (g-exec x y)))


 (defthm f-commutes
   (implies (and (integerp x)
                 (integerp y))
            (equal (f y x)
                   (f x y)))
   :hints (("Goal"
            :in-theory (disable f-exec))
           ("Goal'"
            :by (:instance f-exec-commutes))))
 (defthm g-does-not-commute
   (implies (and (integerp x)
                 (integerp y)
                 (not (equal x y)))
            (not (equal (g y x)
                        (g x y))))
   :hints (("Goal"
            :in-theory (disable g-exec))
           ("Goal'"
            :by (:instance g-exec-does-not-commute))))


 ; alternatively
 ;; (defthm f-commutes
 ;;   (implies (and (integerp x)
 ;;                 (integerp y))
 ;;            (equal (f y x)
 ;;                   (f x y)))
 ;;   :hints (("Goal"
 ;;            :in-theory (union-theories '(f)
 ;;                                       (theory 'minimal-theory))
 ;;            :use (f-exec-commutes))))
 ;; (defthm g-does-not-commute
 ;;   (implies (and (integerp x)
 ;;                 (integerp y)
 ;;                 (not (equal x y)))
 ;;            (not (equal (g y x)
 ;;                        (g x y))))
 ;;   :hints (("Goal"
 ;;            :in-theory (union-theories '(g)
 ;;                                       (theory 'minimal-theory))
 ;;            :use (g-exec-does-not-commute))))

 )


(defattach (f f-exec)
           (g g-exec)
           :hints (("Goal"
                    :by (:instance defattach-proof))))

; alternatively
;; (defattach (f f-exec)
;;            (g g-exec)
;;            :hints (("Goal"
;;                     :in-theory (theory 'minimal-theory)
;;                     :use (f-exec-commutes 
;;                           g-exec-does-not-commute))))

(ubu! 'start)







#||

======================================================================
Case study:  Non-local defun in encapsulate
======================================================================

||#

(defun f-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (+ x y))

(defun g-exec (x y)
  (declare (xargs :guard (and (rationalp x)
                              (rationalp y))))
  (- x y))


(encapsulate
 (((f * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y)))
  ((g * *) => * :formals (x y) :guard (and (integerp x)
                                           (integerp y))))
 
 (local
  (defun f (x y)
    (declare (xargs :guard (and (integerp x)
                                (integerp y))))
    (+ x y)))
 (local
  (defun g (x y)
    (declare (xargs :guard (and (integerp x)
                                (integerp y))))
    (- x y)))



 (defun h (x y)
   (f x y))

 ; need this theorem for defattach proof
 (defthm h-exec
   (equal (h x y)
          (f-exec x y)))
 


 (defthm f-commutes
   (implies (and (integerp x)
                 (integerp y))
            (equal (f y x)
                   (f x y))))
 (defthm g-does-not-commute
   (implies (and (integerp x)
                 (integerp y)
                 (not (equal x y)))
            (not (equal (g y x)
                        (g x y)))))

 (defthm h-commutes
   (implies (and (integerp x)
                 (integerp y))
            (equal (h y x)
                   (h x y))))   
 )




(defattach (f f-exec)
           (g g-exec))





#||

======================================================================
Case study:  Non-local defun-sk in encapsulate...
======================================================================

Omitted from talk because of complexity.

||#