stirling% xacl2h Using ACL2(h) on /u/moore/work/svn-817-1317/ Welcome to Clozure Common Lisp Version 1.8-dev-r15140M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-right-margin* to 83. ; Aside: *hons-init-hook*: Setting *save-source-locations* to t. ; Aside: *hons-init-hook*: Setting *record-source-file* to t. ACL2 Version 5.0 built January 21, 2013 21:35:09. Copyright (C) 2012 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. WARNING: Do not redistribute. This is NOT an ACL2 release; it is, rather, an svn distribution, $Revision: 816 $. The authors of ACL2 consider svn distributions to be experimental. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-5-0 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 5.0. Level 1. Cbd "/Users/moore/work/x86-y86/devel/". System books directory "/Users/moore/work/svn-817-1317/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(ld "y86-temp.lisp" :ld-pre-eval-print t) ; The above file is not provided in the seminar log because it depends on ; things that are still changing. But it loads some tau bounder rules ; and the initial part of the Y86 machine model. ... ; The formal definitions of what is to be a tau-interval and for an object ; to be in a tau-interval. ACL2 !>(pe 'tau-intervalp) V -125 (DEFUN TAU-INTERVALP (INT) (DECLARE (XARGS :GUARD T)) "Documentation available via :doc" (IF (AND (CONSP INT) (CONSP (CDR INT)) (CONSP (CADR INT)) (CONSP (CDDR INT))) (LET ((DOM (TAU-INTERVAL-DOM INT)) (LO-REL (TAU-INTERVAL-LO-REL INT)) (LO (TAU-INTERVAL-LO INT)) (HI-REL (TAU-INTERVAL-HI-REL INT)) (HI (TAU-INTERVAL-HI INT))) (COND ((EQ DOM 'INTEGERP) (AND (NULL LO-REL) (NULL HI-REL) (IF LO (AND (INTEGERP LO) (IF HI (AND (INTEGERP HI) (<= LO HI)) T)) (IF HI (INTEGERP HI) T)))) (T (AND (MEMBER DOM '(RATIONALP ACL2-NUMBERP NIL)) (BOOLEANP LO-REL) (BOOLEANP HI-REL) (IF LO (AND (RATIONALP LO) (IF HI (AND (RATIONALP HI) (<= LO HI)) T)) (IF HI (RATIONALP HI) T)))))) NIL)) Additional events for the logical name TAU-INTERVALP: PV -6351 (DEFUN TAU-INTERVALP (INT) (DECLARE (XARGS :GUARD T)) "Documentation available via :doc" (IF (AND (CONSP INT) (CONSP (CDR INT)) (CONSP (CADR INT)) (CONSP (CDDR INT))) (LET ((DOM (TAU-INTERVAL-DOM INT)) (LO-REL (TAU-INTERVAL-LO-REL INT)) (LO (TAU-INTERVAL-LO INT)) (HI-REL (TAU-INTERVAL-HI-REL INT)) (HI (TAU-INTERVAL-HI INT))) (COND ((EQ DOM 'INTEGERP) (AND (NULL LO-REL) (NULL HI-REL) (IF LO (AND (INTEGERP LO) (IF HI (AND (INTEGERP HI) (<= LO HI)) T)) (IF HI (INTEGERP HI) T)))) (T (AND (MEMBER DOM '(RATIONALP ACL2-NUMBERP NIL)) (BOOLEANP LO-REL) (BOOLEANP HI-REL) (IF LO (AND (RATIONALP LO) (IF HI (AND (RATIONALP HI) (<= LO HI)) T)) (IF HI (RATIONALP HI) T)))))) NIL)) ACL2 !>(pe 'in-tau-intervalp) V -124 (DEFUN IN-TAU-INTERVALP (X INT) (DECLARE (XARGS :GUARD (TAU-INTERVALP INT))) "Documentation available via :doc" (AND (TAU-INTERVAL-DOMAINP (TAU-INTERVAL-DOM INT) X) ((quote (back to slides)) (BACK TO SLIDES) ; The definitions of the functions involved in computing an interval for ; product. Note especially how long the definition of bounds-of-product1 ; is. ACL2 !>(pe 'tau-bounder-*) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ >L (DEFUN TAU-BOUNDER-* (INT1 INT2) (LET ((DOM (DOMAIN-OF-BINARY-ARITHMETIC-FUNCTION (TAU-INTERVAL-DOM INT1) (TAU-INTERVAL-DOM INT2)))) (MV-LET (LO-REL LO HI-REL HI) (BOUNDS-OF-PRODUCT (TAU-INTERVAL-LO-REL INT1) (TAU-INTERVAL-LO INT1) (TAU-INTERVAL-HI-REL INT1) (TAU-INTERVAL-HI INT1) (TAU-INTERVAL-LO-REL INT2) (TAU-INTERVAL-LO INT2) (TAU-INTERVAL-HI-REL INT2) (TAU-INTERVAL-HI INT2)) (MAKE-TAU-INTERVAL DOM LO-REL LO HI-REL HI)))) ACL2 !>(pe 'bounds-of-product) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ >L (DEFUN BOUNDS-OF-PRODUCT (LO-REL1 LO1 HI-REL1 HI1 LO-REL2 LO2 HI-REL2 HI2) (LET ((HI1 (IF (NULL HI1) T HI1)) (HI2 (IF (NULL HI2) T HI2))) (MV-LET (LO-REL LO HI-REL HI) (BOUNDS-OF-PRODUCT1 LO-REL1 LO1 HI-REL1 HI1 LO-REL2 LO2 HI-REL2 HI2) (MV (IF (NULL LO) NIL LO-REL) LO (IF (EQ HI T) NIL HI-REL) (IF (EQ HI T) NIL HI))))) ACL2 !>(pe 'bounds-of-product1) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ >L (DEFUN BOUNDS-OF-PRODUCT1 (LO-REL1 LO1 HI-REL1 HI1 LO-REL2 LO2 HI-REL2 HI2) (COND ((EQUAL LO1 HI1) (COND ((BOUNDS-OF-PRODUCT-< 0 LO1) (MV LO-REL2 (BOUNDS-OF-PRODUCT-* LO1 LO2) HI-REL2 (BOUNDS-OF-PRODUCT-* LO1 HI2))) ((EQUAL LO1 0) (MV NIL 0 NIL 0)) (T (MV HI-REL2 (BOUNDS-OF-PRODUCT-* LO1 HI2) LO-REL2 (BOUNDS-OF-PRODUCT-* LO1 LO2))))) ((EQUAL LO2 HI2) (COND ((BOUNDS-OF-PRODUCT-< 0 LO2) (MV LO-REL1 (BOUNDS-OF-PRODUCT-* LO1 LO2) HI-REL1 (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((EQUAL LO2 0) (MV NIL 0 NIL 0)) (T (MV HI-REL1 (BOUNDS-OF-PRODUCT-* HI1 LO2) LO-REL1 (BOUNDS-OF-PRODUCT-* LO1 LO2))))) ((AND (BOUNDS-OF-PRODUCT-<= 0 LO1) (BOUNDS-OF-PRODUCT-<= 0 LO2)) (MV (AND (OR LO-REL1 LO-REL2) (OR LO-REL1 (NOT (EQUAL LO1 0))) (OR LO-REL2 (NOT (EQUAL LO2 0)))) (BOUNDS-OF-PRODUCT-* LO1 LO2) (OR HI-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((AND (BOUNDS-OF-PRODUCT-<= HI1 0) (BOUNDS-OF-PRODUCT-<= HI2 0)) (MV (AND (OR HI-REL1 HI-REL2) (OR HI-REL1 (NOT (EQUAL HI1 0))) (OR HI-REL2 (NOT (EQUAL HI2 0)))) (BOUNDS-OF-PRODUCT-* HI1 HI2) (OR LO-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) ((AND (BOUNDS-OF-PRODUCT-<= 0 LO1) (BOUNDS-OF-PRODUCT-<= HI2 0)) (MV (OR HI-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* HI1 LO2) (AND (OR LO-REL1 HI-REL2) (OR LO-REL1 (NOT (EQUAL LO1 0))) (OR HI-REL2 (NOT (EQUAL HI2 0)))) (BOUNDS-OF-PRODUCT-* LO1 HI2))) ((AND (BOUNDS-OF-PRODUCT-<= HI1 0) (BOUNDS-OF-PRODUCT-<= 0 LO2)) (MV (OR LO-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* LO1 HI2) (AND (OR HI-REL1 LO-REL2) (OR HI-REL1 (NOT (EQUAL HI1 0))) (OR LO-REL2 (NOT (EQUAL LO2 0)))) (BOUNDS-OF-PRODUCT-* HI1 LO2))) ((AND (BOUNDS-OF-PRODUCT-< LO1 0) (BOUNDS-OF-PRODUCT-< 0 HI1) (BOUNDS-OF-PRODUCT-<= 0 LO2)) (MV (OR LO-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* LO1 HI2) (OR HI-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((AND (BOUNDS-OF-PRODUCT-< LO1 0) (BOUNDS-OF-PRODUCT-< 0 HI1) (BOUNDS-OF-PRODUCT-<= HI2 0)) (MV (OR HI-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* HI1 LO2) (OR LO-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) ((AND (BOUNDS-OF-PRODUCT-<= 0 LO1) (BOUNDS-OF-PRODUCT-< LO2 0) (BOUNDS-OF-PRODUCT-< 0 HI2)) (MV (OR HI-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* HI1 LO2) (OR HI-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((AND (BOUNDS-OF-PRODUCT-<= HI1 0) (BOUNDS-OF-PRODUCT-< LO2 0) (BOUNDS-OF-PRODUCT-< 0 HI2)) (MV (OR LO-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* LO1 HI2) (OR LO-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) (T (COND ((AND (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* LO1 HI2) (BOUNDS-OF-PRODUCT-* HI1 LO2)) (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* LO1 LO2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) (MV (OR LO-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* LO1 HI2) (OR HI-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((AND (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* LO1 HI2) (BOUNDS-OF-PRODUCT-* HI1 LO2)) (EQUAL (BOUNDS-OF-PRODUCT-* LO1 LO2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) (MV (OR LO-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* LO1 HI2) (AND (OR LO-REL1 LO-REL2) (OR HI-REL1 HI-REL2)) (BOUNDS-OF-PRODUCT-* LO1 LO2))) ((AND (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* LO1 HI2) (BOUNDS-OF-PRODUCT-* HI1 LO2)) (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* HI1 HI2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) (MV (OR LO-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* LO1 HI2) (OR LO-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) ((AND (EQUAL (BOUNDS-OF-PRODUCT-* LO1 HI2) (BOUNDS-OF-PRODUCT-* HI1 LO2)) (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* LO1 LO2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) (MV (AND (OR LO-REL1 HI-REL2) (OR HI-REL1 LO-REL2)) (BOUNDS-OF-PRODUCT-* LO1 HI2) (OR HI-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((AND (EQUAL (BOUNDS-OF-PRODUCT-* LO1 HI2) (BOUNDS-OF-PRODUCT-* HI1 LO2)) (EQUAL (BOUNDS-OF-PRODUCT-* LO1 LO2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) (MV (AND (OR LO-REL1 HI-REL2) (OR HI-REL1 LO-REL2)) (BOUNDS-OF-PRODUCT-* LO1 HI2) (AND (OR LO-REL1 LO-REL2) (OR HI-REL1 HI-REL2)) (BOUNDS-OF-PRODUCT-* LO1 LO2))) ((AND (EQUAL (BOUNDS-OF-PRODUCT-* LO1 HI2) (BOUNDS-OF-PRODUCT-* HI1 LO2)) (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* HI1 HI2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) (MV (AND (OR LO-REL1 HI-REL2) (OR HI-REL1 LO-REL2)) (BOUNDS-OF-PRODUCT-* LO1 HI2) (OR LO-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* LO1 LO2))) ((AND (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* HI1 LO2) (BOUNDS-OF-PRODUCT-* LO1 HI2)) (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* LO1 LO2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) (MV (OR HI-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* HI1 LO2) (OR HI-REL1 HI-REL2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) ((AND (BOUNDS-OF-PRODUCT-< (BOUNDS-OF-PRODUCT-* HI1 LO2) (BOUNDS-OF-PRODUCT-* LO1 HI2)) (EQUAL (BOUNDS-OF-PRODUCT-* LO1 LO2) (BOUNDS-OF-PRODUCT-* HI1 HI2))) (MV (OR HI-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* HI1 LO2) (AND (OR LO-REL1 LO-REL2) (OR HI-REL1 HI-REL2)) (BOUNDS-OF-PRODUCT-* LO1 LO2))) (T (MV (OR HI-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* HI1 LO2) (OR LO-REL1 LO-REL2) (BOUNDS-OF-PRODUCT-* LO1 LO2))))))) ACL2 !>(quote (back to slides)) (BACK TO SLIDES) ; The definition of the bounder for LOGAND, which uses both ``analytical'' and ; ``empirical'' methods. The empirical method just runs all the logands over ; small two finite intervals and computes the min and max. It is controlled by ; a heuristic test, worth-computingp which is in turn sensitive to the size of ; the cross-product of the two intervals. Below I demonstrate that the ; analytical method alone can be wildly inaccurate, I show how long it takes to ; compute the empirical min and max for two intervals of size 1024 each, and ; then I verify the guards on the empirical computation and show a dramatic ; improvement in the time. ACL2 !>(pe 'tau-bounder-logand) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ >L (DEFUN TAU-BOUNDER-LOGAND (INT1 INT2) (LET ((LOX (TAU-INTERVAL-LO INT1)) (HIX (TAU-INTERVAL-HI INT1)) (LOY (TAU-INTERVAL-LO INT2)) (HIY (TAU-INTERVAL-HI INT2))) (COND ((AND LOX HIX LOY HIY (WORTH-COMPUTINGP LOX HIX LOY HIY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL (FIND-MINIMAL-LOGAND LOX HIX LOY HIY) NIL (FIND-MAXIMAL-LOGAND LOX HIX LOY HIY))) ((AND LOX (<= 0 LOX) LOY (<= 0 LOY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL (AND HIX HIY (MIN HIX HIY)))) ((AND HIX (< HIX 0) HIY (< HIY 0)) (MAKE-TAU-INTERVAL 'INTEGERP NIL (AND LOX LOY (- (EXPT 2 (MAX (SHIFTS-TO-ALL-ONES LOX) (SHIFTS-TO-ALL-ONES LOY))))) NIL (MIN HIX HIY))) ((AND HIX (<= HIX 0) LOY (<= 0 LOY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL HIY)) ((AND HIY (<= HIY 0) LOX (<= 0 LOX)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL HIX)) ((AND LOX (<= 0 LOX)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL (AND HIX HIY (MAX HIX HIY)))) ((AND LOY (<= 0 LOY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL (AND HIX HIY (MAX HIX HIY)))) (T (MAKE-TAU-INTERVAL 'INTEGERP NIL (AND LOX LOY (MIN 0 (- (EXPT 2 (MAX (SHIFTS-TO-ALL-ONES LOX) (SHIFTS-TO-ALL-ONES LOY)))))) NIL (AND HIX HIY (MAX HIX HIY))))))) ACL2 !>(value :q) ; By setting the threshhold to 0, I rule out the use of the empirical method. ; Then I return to the loop where the threshhold is set to 1024*1024 and ; recompute this example, showing that the actual interval bounding this logand ; is 8 to 15, rather than the analytical 0 to 1073741839. Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ? (let ((*logand-empirical-threshhold* 0)) (tau-bounder-logand '(INTEGERP (NIL . 2147483656) . (NIL . 2147483663)) '(INTEGERP (NIL . 1073741832) . (NIL . 1073741839)))) (INTEGERP (NIL . 0) NIL . 1073741839) ? (lp) ACL2 Version 5.0. Level 1. Cbd "/Users/moore/work/x86-y86/devel/". System books directory "/Users/moore/work/svn-817-1317/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(tau-bounder-logand '(INTEGERP (NIL . 2147483656) . (NIL . 2147483663)) '(INTEGERP (NIL . 1073741832) . (NIL . 1073741839))) (INTEGERP (NIL . 8) NIL . 15) ACL2 !>(tau-bounder-logand `(INTEGERP (nil . ,(+ (expt 2 31) 8)) . (nil . ,(+ (expt 2 31) 8 7))) `(INTEGERP (nil . ,(+ (expt 2 30) 8)) . (nil . ,(+ (expt 2 30) 8 7)))) (INTEGERP (NIL . 8) NIL . 15) ACL2 !>(pe 'tau-bounder-logand) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ >L (DEFUN TAU-BOUNDER-LOGAND (INT1 INT2) (LET ((LOX (TAU-INTERVAL-LO INT1)) (HIX (TAU-INTERVAL-HI INT1)) (LOY (TAU-INTERVAL-LO INT2)) (HIY (TAU-INTERVAL-HI INT2))) (COND ((AND LOX HIX LOY HIY (WORTH-COMPUTINGP LOX HIX LOY HIY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL (FIND-MINIMAL-LOGAND LOX HIX LOY HIY) NIL (FIND-MAXIMAL-LOGAND LOX HIX LOY HIY))) ((AND LOX (<= 0 LOX) LOY (<= 0 LOY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL (AND HIX HIY (MIN HIX HIY)))) ((AND HIX (< HIX 0) HIY (< HIY 0)) (MAKE-TAU-INTERVAL 'INTEGERP NIL (AND LOX LOY (- (EXPT 2 (MAX (SHIFTS-TO-ALL-ONES LOX) (SHIFTS-TO-ALL-ONES LOY))))) NIL (MIN HIX HIY))) ((AND HIX (<= HIX 0) LOY (<= 0 LOY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL HIY)) ((AND HIY (<= HIY 0) LOX (<= 0 LOX)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL HIX)) ((AND LOX (<= 0 LOX)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL (AND HIX HIY (MAX HIX HIY)))) ((AND LOY (<= 0 LOY)) (MAKE-TAU-INTERVAL 'INTEGERP NIL 0 NIL (AND HIX HIY (MAX HIX HIY)))) (T (MAKE-TAU-INTERVAL 'INTEGERP NIL (AND LOX LOY (MIN 0 (- (EXPT 2 (MAX (SHIFTS-TO-ALL-ONES LOX) (SHIFTS-TO-ALL-ONES LOY)))))) NIL (AND HIX HIY (MAX HIX HIY))))))) ACL2 !>(pe 'worth-computingp) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ >L d (DEFUN WORTH-COMPUTINGP (LOX HIX LOY HIY) (< (* (IF (<= LOX HIX) (+ 1 (- HIX LOX)) 0) (IF (<= LOY HIY) (+ 1 (- HIY LOY)) 0)) *LOGAND-EMPIRICAL-THRESHHOLD*)) ACL2 !>(pe '*logand-empirical-threshhold*) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ > (DEFCONST *LOGAND-EMPIRICAL-THRESHHOLD* (* 1024 1024)) ACL2 !>(time$ (find-minimal-logand 0 1023 0 1023)) ; (EV-REC *RETURN-LAST-ARG3* ...) took ; 0.13 seconds realtime, 0.13 seconds runtime ; (1,344 bytes allocated). 0 ACL2 !>(er-progn (verify-guards find-minimal-logand2) (verify-guards find-minimal-logand1) (verify-guards find-minimal-logand) (verify-guards find-maximal-logand2) (verify-guards find-maximal-logand1) (verify-guards find-maximal-logand)) Computing the guard conjecture for FIND-MINIMAL-LOGAND2.... The guard conjecture for FIND-MINIMAL-LOGAND2 is trivial to prove, given primitive type reasoning and the :type-prescription rule BINARY-LOGAND. FIND-MINIMAL-LOGAND2 is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FIND-MINIMAL-LOGAND2) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION BINARY-LOGAND)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Computing the guard conjecture for FIND-MINIMAL-LOGAND1.... The guard conjecture for FIND-MINIMAL-LOGAND1 is trivial to prove, given primitive type reasoning and the :type-prescription rule FIND-MINIMAL-LOGAND2. FIND-MINIMAL-LOGAND1 is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FIND-MINIMAL-LOGAND1) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FIND-MINIMAL-LOGAND2)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Computing the guard conjecture for FIND-MINIMAL-LOGAND.... The guard conjecture for FIND-MINIMAL-LOGAND is trivial to prove, given the :executable-counterpart of NULL. FIND-MINIMAL-LOGAND is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FIND-MINIMAL-LOGAND) Rules: ((:EXECUTABLE-COUNTERPART NULL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Computing the guard conjecture for FIND-MAXIMAL-LOGAND2.... The guard conjecture for FIND-MAXIMAL-LOGAND2 is trivial to prove, given primitive type reasoning and the :type-prescription rule BINARY-LOGAND. FIND-MAXIMAL-LOGAND2 is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FIND-MAXIMAL-LOGAND2) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION BINARY-LOGAND)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Computing the guard conjecture for FIND-MAXIMAL-LOGAND1.... The guard conjecture for FIND-MAXIMAL-LOGAND1 is trivial to prove, given primitive type reasoning and the :type-prescription rule FIND-MAXIMAL-LOGAND2. FIND-MAXIMAL-LOGAND1 is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FIND-MAXIMAL-LOGAND1) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FIND-MAXIMAL-LOGAND2)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Computing the guard conjecture for FIND-MAXIMAL-LOGAND.... The guard conjecture for FIND-MAXIMAL-LOGAND is trivial to prove, given the :executable-counterpart of NULL. FIND-MAXIMAL-LOGAND is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS FIND-MAXIMAL-LOGAND) Rules: ((:EXECUTABLE-COUNTERPART NULL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FIND-MAXIMAL-LOGAND ACL2 !>(time$ (find-minimal-logand 0 1023 0 1023)) ; (EV-REC *RETURN-LAST-ARG3* ...) took ; 0.01 seconds realtime, 0.01 seconds runtime ; (1,344 bytes allocated). 0 ACL2 !>(quote (back to slides)) (BACK TO SLIDES) ; The correctness theorem for the LOGAND bounder is stored succinctly as shown by ; the getprop below. ACL2 !>(pe 'tau-bounder-logand-correct) d 1 (INCLUDE-BOOK "bounders/ab11") \ [Included books, outermost to innermost: "/Users/moore/work/x86-y86/devel/bounders/ab11.lisp" ] \ > (DEFTHM TAU-BOUNDER-LOGAND-CORRECT (IMPLIES (AND (TAU-INTERVALP INT1) (TAU-INTERVALP INT2) (EQUAL (TAU-INTERVAL-DOM INT1) 'INTEGERP) (EQUAL (TAU-INTERVAL-DOM INT2) 'INTEGERP) (IN-TAU-INTERVALP X INT1) (IN-TAU-INTERVALP Y INT2)) (AND (TAU-INTERVALP (TAU-BOUNDER-LOGAND INT1 INT2)) (IN-TAU-INTERVALP (LOGAND X Y) (TAU-BOUNDER-LOGAND INT1 INT2)) (EQUAL (TAU-INTERVAL-DOM (TAU-BOUNDER-LOGAND INT1 INT2)) 'INTEGERP))) :HINTS (("Goal" :IN-THEORY (DISABLE MIN MAX))) :RULE-CLASSES ((:REWRITE) (:FORWARD-CHAINING :TRIGGER-TERMS ((TAU-BOUNDER-LOGAND INT1 INT2))))) ACL2 !>(getprop 'binary-logand 'tau-bounders-form-1 nil 'current-acl2-world (w state)) (((BINARY-LOGAND (INTEGERP) (INTEGERP)) TAU-BOUNDER-LOGAND 0 1)) ; Now I demonstrate some theorems that can (best) be proved by tau using bounders. ACL2 !>(tau-status :system nil) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 3659 ACL2 !>(thm (implies (and (integerp x) (<= (+ (expt 2 31) 8) x) (<= x (+ (expt 2 31) 8 7)) (integerp y) (<= (+ (expt 2 30) 8) y) (<= y (+ (expt 2 30) 8 7))) (< (logand x y) 20))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (INTEGERP X) (<= 2147483656 X) (<= X 2147483663) (INTEGERP Y) (<= 1073741832 Y) (<= Y 1073741839)) (< (LOGAND X Y) 20)) *1 (Goal') is pushed for proof by induction. ]) No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( THM ...) Rules: ((:DEFINITION NOT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EXPT)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 211 --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal' (IMPLIES (AND (INTEGERP X) (<= 2147483656 X) (<= X 2147483663) (INTEGERP Y) (<= 1073741832 Y) (<= Y 1073741839)) (< (LOGAND X Y) 20)) ACL2 Error in ( THM ...): See :DOC failure. ******** FAILED ******** ACL2 !>(tau-status :system t) Summary Form: ( IN-THEORY (ENABLE ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 3660 ACL2 !>(thm (implies (and (integerp x) (<= (+ (expt 2 31) 8) x) (<= x (+ (expt 2 31) 8 7)) (integerp y) (<= (+ (expt 2 30) 8) y) (<= y (+ (expt 2 30) 8 7))) (< (logand x y) 20))) Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION NOT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART TAU-SYSTEM)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 80 Proof succeeded. ACL2 !>(thm (implies (and (integerp x) (<= (+ (expt 2 31) 8) x) (<= x (+ (expt 2 31) 8 7)) (integerp y) (<= (+ (expt 2 30) 8) y) (<= y (+ (expt 2 30) 8 7)) (not (equal (logand x y) 8)) (not (equal (logand x y) 9)) (not (equal (logand x y) 10)) (not (equal (logand x y) 11)) (not (equal (logand x y) 12)) (not (equal (logand x y) 14)) (not (equal (logand x y) 15))) (equal (logand x y) 13))) Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION NOT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART TAU-SYSTEM)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 192 Proof succeeded. ACL2 !>(tau-status :system nil) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 3659 ; This is the semantics of one particular instruction in the Y86 model and ; at issue is verifying the guards. ACL2 !>(defund y86-rA-to-mem-at-rb+D (x86-32) (declare (xargs :guard t :stobjs (x86-32))) (b* ((pc (eip x86-32)) ;; Memory Probe ((if (< *2^32-7* pc)) (!ms (list :at-location pc :instruction 'rmmovl :memory-probe nil) x86-32)) ;; Decode registers (rA-rB (rm08 (+ pc 1) x86-32)) (rB (n03 rA-rB)) (rA (n03 (ash rA-rB -4))) (b3 (n01 (ash rA-rB -3))) (b7 (n01 (ash rA-rB -7))) ;; Register decoding problem? ((if (or (= b7 1) (= b3 1))) (!ms (list :at-location pc :instruction 'rmmovl :b7 b7 :b3 b3 :ra rA :rb rB) x86-32)) ;; ra -> D(rb) (disp (rm32 (+ pc 2) x86-32)) (addr (n32+ (rgfi rb x86-32) disp)) (rA-val (rgfi rA x86-32)) (x86-32 (wm32 addr rA-val x86-32)) ;; Update PC (x86-32 (!eip (+ pc 6) x86-32))) x86-32)) Since Y86-RA-TO-MEM-AT-RB+D is non-recursive, its admission is trivial. We observe that the type of Y86-RA-TO-MEM-AT-RB+D is described by the theorem (CONSP (Y86-RA-TO-MEM-AT-RB+D X86-32)). We used primitive type reasoning and the :type-prescription rules !EIP and !MS. (Y86-RA-TO-MEM-AT-RB+D X86-32) => X86-32. Computing the guard conjecture for Y86-RA-TO-MEM-AT-RB+D.... The non-trivial part of the guard conjecture for Y86-RA-TO-MEM-AT-RB+D is Goal (IMPLIES (X86-32P X86-32) (LET ((PC (EIP X86-32))) (AND (RATIONALP PC) (OR (< 4294967289 PC) (ACL2-NUMBERP PC)) (OR (< 4294967289 PC) (INTEGERP (+ PC 1))) (OR (< 4294967289 PC) (< (+ PC 1) 4294967296)) (OR (< 4294967289 PC) (<= 0 (+ PC 1))) (OR (< 4294967289 PC) (UNSIGNED-BYTE-P 32 (+ PC 1))) (OR (< 4294967289 PC) (LET ((RA-RB (RM08 (+ PC 1) X86-32))) (AND (INTEGERP RA-RB) (LET ((RB (LOGAND RA-RB 7))) (AND (INTEGERP RA-RB) (INTEGERP (ASH RA-RB -4)) (LET ((RA (LOGAND (ASH RA-RB -4) 7))) (AND (INTEGERP RA-RB) (INTEGERP (ASH RA-RB -3)) (LET ((B3 (LOGAND (ASH RA-RB -3) 1))) (AND (INTEGERP RA-RB) (INTEGERP (ASH RA-RB -7)) (LET ((B7 (LOGAND (ASH RA-RB -7) 1))) (AND (ACL2-NUMBERP B7) (OR (NOT (= B7 1)) (ACL2-NUMBERP B7)) (OR (= B7 1) (ACL2-NUMBERP B3)) (OR (OR (= B7 1) (= B3 1)) (ACL2-NUMBERP PC)) (OR (OR (= B7 1) (= B3 1)) (INTEGERP (+ PC 2))) (OR (OR (= B7 1) (= B3 1)) (< (+ PC 2) 4294967296)) (OR (OR (= B7 1) (= B3 1)) (<= 0 (+ PC 2))) (OR (OR (= B7 1) (= B3 1)) (UNSIGNED-BYTE-P 32 (+ PC 2))) (OR (OR (= B7 1) (= B3 1)) (LET ((DISP (RM32 (+ PC 2) X86-32))) (AND (INTEGERP RB) (< RB (RGF-LENGTH X86-32)) (<= 0 RB) (ACL2-NUMBERP (RGFI RB X86-32)) (ACL2-NUMBERP DISP) (INTEGERP (+ (RGFI RB X86-32) DISP)) (LET ((ADDR (LOGAND (+ (RGFI RB X86-32) DISP) 4294967295))) (AND (INTEGERP RA) (< RA (RGF-LENGTH X86-32)) (<= 0 RA) (LET ((RA-VAL (RGFI RA X86-32))) (AND (INTEGERP ADDR) (<= 0 RA-VAL) (< ADDR 4294967296) (UNSIGNED-BYTE-P 32 ADDR) (<= 0 ADDR) (< RA-VAL 4294967296) (INTEGERP RA-VAL) (LET NIL (AND (ACL2-NUMBERP PC) (UNSIGNED-BYTE-P 32 (+ PC 6))))))))))))))))))))))))). Goal' Subgoal 9 Subgoal 8 Subgoal 7 Subgoal 6 Subgoal 5 Subgoal 5' Subgoal 4 Subgoal 3 Forcing Round 1 is pending (caused first by Subgoal 3). Subgoal 2 Subgoal 2' Subgoal 1 q.e.d. (given five forced hypotheses) Modulo five forced goals, that completes the proof of the input Goal. See :DOC forcing-round. [1]Subgoal 5 was forced in Subgoal 1 by applying (:TYPE-PRESCRIPTION NATP-RM08). [1]Subgoal 4 was forced in Subgoal 2' by applying (:TYPE-PRESCRIPTION INTEGERP-RM32). [1]Subgoal 3 was forced in Subgoal 2' by applying (:TYPE-PRESCRIPTION NATP-RGFI). [1]Subgoal 2 was forced in Subgoal 3 by applying (:TYPE-PRESCRIPTION NATP-RGFI). [1]Subgoal 1 was forced in Subgoal 3 by applying (:TYPE-PRESCRIPTION INTEGERP-RM32). We now undertake Forcing Round 1. [1]Subgoal 5 [1]Subgoal 5' [1]Subgoal 4 [1]Subgoal 4' [1]Subgoal 3 [1]Subgoal 3' Forcing Round 2 is pending (caused first by [1]Subgoal 3'). [1]Subgoal 2 [1]Subgoal 2' [1]Subgoal 1 [1]Subgoal 1' q.e.d. (given one forced hypothesis) Modulo one newly forced goal, that completes Forcing Round 1. See :DOC forcing-round. [2]Goal was forced in [1]Subgoal 3' by applying (:TYPE-PRESCRIPTION NATP-RM08). We now undertake Forcing Round 2. [2]Goal [2]Goal' Q.E.D. That completes the proof of the guard theorem for Y86-RA-TO-MEM-AT-RB+D. Y86-RA-TO-MEM-AT-RB+D is compliant with Common Lisp. Summary Form: ( DEFUN Y86-RA-TO-MEM-AT-RB+D ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:DEFINITION =) (:DEFINITION INTEGER-RANGE-P) (:DEFINITION NOT) (:DEFINITION RGF-LENGTH) (:DEFINITION UNSIGNED-BYTE-P) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ACL2-NUMBERP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART NATP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING X86-32P@-PROPERTIES) (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2) (:LINEAR N03P-LOGAND-N03P-LESS-THAN-8) (:LINEAR N32P-LOGAND-N32P-LESS-THAN-4294967296) (:LINEAR RGFI-LESS-THAN-EXPT-2-32) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE X86-32P-IS-X86-32P@) (:TYPE-PRESCRIPTION !EIP) (:TYPE-PRESCRIPTION !MS) (:TYPE-PRESCRIPTION ASH) (:TYPE-PRESCRIPTION CTRP) (:TYPE-PRESCRIPTION DBGP) (:TYPE-PRESCRIPTION EIPP) (:TYPE-PRESCRIPTION FLGP) (:TYPE-PRESCRIPTION INTEGERP-RM32) (:TYPE-PRESCRIPTION LEN) (:TYPE-PRESCRIPTION LOGAND-GREATER-OR-EQUAL-TO-ZERO) (:TYPE-PRESCRIPTION MEMP) (:TYPE-PRESCRIPTION NATP-EIP) (:TYPE-PRESCRIPTION NATP-RGFI) (:TYPE-PRESCRIPTION NATP-RM08) (:TYPE-PRESCRIPTION RGFP) (:TYPE-PRESCRIPTION RM08) (:TYPE-PRESCRIPTION SEG-ACCESSP) (:TYPE-PRESCRIPTION SEG-BASEP) (:TYPE-PRESCRIPTION SEG-LIMITP) (:TYPE-PRESCRIPTION SEGP) (:TYPE-PRESCRIPTION SSRP) (:TYPE-PRESCRIPTION STRP) (:TYPE-PRESCRIPTION X86-32P@)) Time: 0.12 seconds (prove: 0.10, print: 0.01, other: 0.01) Prover steps counted: 16663 Summary Form: ( PROGN (DEFUN Y86-RA-TO-MEM-AT-RB+D ...) ...) Rules: NIL Time: 0.12 seconds (prove: 0.10, print: 0.01, other: 0.01) Prover steps counted: 16663 (:DEFUND Y86-RA-TO-MEM-AT-RB+D) ACL2 !>(u) 39:x(TAU-STATUS :SYSTEM NIL) ACL2 !>(tau-status :system t) Summary Form: ( IN-THEORY (ENABLE ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 3660 ACL2 !>(defund y86-rA-to-mem-at-rb+D (x86-32) (declare (xargs :guard t :stobjs (x86-32))) (b* ((pc (eip x86-32)) ;; Memory Probe ((if (< *2^32-7* pc)) (!ms (list :at-location pc :instruction 'rmmovl :memory-probe nil) x86-32)) ;; Decode registers (rA-rB (rm08 (+ pc 1) x86-32)) (rB (n03 rA-rB)) (rA (n03 (ash rA-rB -4))) (b3 (n01 (ash rA-rB -3))) (b7 (n01 (ash rA-rB -7))) ;; Register decoding problem? ((if (or (= b7 1) (= b3 1))) (!ms (list :at-location pc :instruction 'rmmovl :b7 b7 :b3 b3 :ra rA :rb rB) x86-32)) ;; ra -> D(rb) (disp (rm32 (+ pc 2) x86-32)) (addr (n32+ (rgfi rb x86-32) disp)) (rA-val (rgfi rA x86-32)) (x86-32 (wm32 addr rA-val x86-32)) ;; Update PC (x86-32 (!eip (+ pc 6) x86-32))) x86-32)) Since Y86-RA-TO-MEM-AT-RB+D is non-recursive, its admission is trivial. We observe that the type of Y86-RA-TO-MEM-AT-RB+D is described by the theorem (CONSP (Y86-RA-TO-MEM-AT-RB+D X86-32)). We used primitive type reasoning and the :type-prescription rules !EIP and !MS. (Y86-RA-TO-MEM-AT-RB+D X86-32) => X86-32. Computing the guard conjecture for Y86-RA-TO-MEM-AT-RB+D.... The non-trivial part of the guard conjecture for Y86-RA-TO-MEM-AT-RB+D is Goal (IMPLIES (X86-32P X86-32) (LET ((PC (EIP X86-32))) (AND (RATIONALP PC) (OR (< 4294967289 PC) (ACL2-NUMBERP PC)) (OR (< 4294967289 PC) (INTEGERP (+ PC 1))) (OR (< 4294967289 PC) (< (+ PC 1) 4294967296)) (OR (< 4294967289 PC) (<= 0 (+ PC 1))) (OR (< 4294967289 PC) (UNSIGNED-BYTE-P 32 (+ PC 1))) (OR (< 4294967289 PC) (LET ((RA-RB (RM08 (+ PC 1) X86-32))) (AND (INTEGERP RA-RB) (LET ((RB (LOGAND RA-RB 7))) (AND (INTEGERP RA-RB) (INTEGERP (ASH RA-RB -4)) (LET ((RA (LOGAND (ASH RA-RB -4) 7))) (AND (INTEGERP RA-RB) (INTEGERP (ASH RA-RB -3)) (LET ((B3 (LOGAND (ASH RA-RB -3) 1))) (AND (INTEGERP RA-RB) (INTEGERP (ASH RA-RB -7)) (LET ((B7 (LOGAND (ASH RA-RB -7) 1))) (AND (ACL2-NUMBERP B7) (OR (NOT (= B7 1)) (ACL2-NUMBERP B7)) (OR (= B7 1) (ACL2-NUMBERP B3)) (OR (OR (= B7 1) (= B3 1)) (ACL2-NUMBERP PC)) (OR (OR (= B7 1) (= B3 1)) (INTEGERP (+ PC 2))) (OR (OR (= B7 1) (= B3 1)) (< (+ PC 2) 4294967296)) (OR (OR (= B7 1) (= B3 1)) (<= 0 (+ PC 2))) (OR (OR (= B7 1) (= B3 1)) (UNSIGNED-BYTE-P 32 (+ PC 2))) (OR (OR (= B7 1) (= B3 1)) (LET ((DISP (RM32 (+ PC 2) X86-32))) (AND (INTEGERP RB) (< RB (RGF-LENGTH X86-32)) (<= 0 RB) (ACL2-NUMBERP (RGFI RB X86-32)) (ACL2-NUMBERP DISP) (INTEGERP (+ (RGFI RB X86-32) DISP)) (LET ((ADDR (LOGAND (+ (RGFI RB X86-32) DISP) 4294967295))) (AND (INTEGERP RA) (< RA (RGF-LENGTH X86-32)) (<= 0 RA) (LET ((RA-VAL (RGFI RA X86-32))) (AND (INTEGERP ADDR) (<= 0 RA-VAL) (< ADDR 4294967296) (UNSIGNED-BYTE-P 32 ADDR) (<= 0 ADDR) (< RA-VAL 4294967296) (INTEGERP RA-VAL) (LET NIL (AND (ACL2-NUMBERP PC) (UNSIGNED-BYTE-P 32 (+ PC 6))))))))))))))))))))))))). Q.E.D. That completes the proof of the guard theorem for Y86-RA-TO-MEM-AT-RB+D. Y86-RA-TO-MEM-AT-RB+D is compliant with Common Lisp. Summary Form: ( DEFUN Y86-RA-TO-MEM-AT-RB+D ...) Rules: ((:DEFINITION =) (:DEFINITION NOT) (:DEFINITION RGF-LENGTH) (:EXECUTABLE-COUNTERPART TAU-SYSTEM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE X86-32P-IS-X86-32P@) (:TYPE-PRESCRIPTION !EIP) (:TYPE-PRESCRIPTION !MS)) Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.01) Prover steps counted: 475 Summary Form: ( PROGN (DEFUN Y86-RA-TO-MEM-AT-RB+D ...) ...) Rules: NIL Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.01) Prover steps counted: 475 (:DEFUND Y86-RA-TO-MEM-AT-RB+D) ACL2 !>