#|| ====================================================================== 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. ||#