← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/coi/super-ihs/signed-byte-p-overflow.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/coi/super-ihs/signed-byte-p-overflow.lisp
1
 
(in-package "ACL2")
2
 
 
3
 
(local
4
 
 (encapsulate
5
 
     ()
6
 
     
7
 
(encapsulate
8
 
    (
9
 
     ((local-ifloor * *) => *)
10
 
     ((local-imod * *) => *)
11
 
     ((local-expt2 *) => *)
12
 
     ((local-logcar *) => *)
13
 
     ((local-loghead * *) => *)
14
 
     ((local-logtail * *) => *)
15
 
     ((local-logapp * * *) => *)
16
 
     )
17
 
 
18
 
  (local
19
 
   (encapsulate
20
 
       ()
21
 
 
22
 
     (defun local-ifloor (i j)
23
 
       (floor (ifix i) (ifix j)))
24
 
     
25
 
     (defun local-imod (i j)
26
 
       (mod (ifix i) (ifix j)))
27
 
     
28
 
     (defun local-expt2 (n)
29
 
       (expt 2 (nfix n)))
30
 
     
31
 
     (defun local-logcar (i)
32
 
       (local-imod i 2))
33
 
     
34
 
     (defun local-loghead (size i)
35
 
       (local-imod i (local-expt2 size)))
36
 
     
37
 
     (defun local-logtail (pos i)
38
 
       (local-ifloor i (local-expt2 pos)))
39
 
 
40
 
     (defun local-logapp (size i j) 
41
 
       (let ((j (ifix j)))
42
 
         (+ (local-loghead size i) (* j (local-expt2 size)))))
43
 
 
44
 
     ))
45
 
 
46
 
  (defthm local-ifloor-defn
47
 
    (equal (local-ifloor i j)
48
 
           (floor (ifix i) (ifix j))))
49
 
  
50
 
  (defthm local-imod-defn 
51
 
    (equal (local-imod i j)
52
 
           (mod (ifix i) (ifix j))))
53
 
  
54
 
  (defthm local-expt2-defn 
55
 
    (equal (local-expt2 n)
56
 
           (expt 2 (nfix n))))
57
 
  
58
 
  (defthm local-logcar-defn
59
 
    (equal (local-logcar i)
60
 
           (local-imod i 2)))
61
 
  
62
 
  (defthm local-loghead-defn
63
 
    (equal (local-loghead size i)
64
 
           (local-imod i (local-expt2 size))))
65
 
  
66
 
  (defthm local-logtail-defn
67
 
    (equal (local-logtail size i)
68
 
           (local-ifloor i (local-expt2 size))))
69
 
  
70
 
  (defthm local-logapp-defn
71
 
    (equal (local-logapp size i j) 
72
 
           (let ((j (ifix j)))
73
 
             (+ (local-loghead size i) (* j (local-expt2 size))))))
74
 
  
75
 
  )
76
 
 
77
 
(encapsulate
78
 
    ()
79
 
 
80
 
    (local (include-book "arithmetic-3/bind-free/top" :dir :system))
81
 
     
82
 
    (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
83
 
     
84
 
; Matt K.: There was formerly a set-default-hints at the end of an embedded
85
 
; encapsulate, which had no effect since set-default-hints was local to that
86
 
; encapsulate.
87
 
 
88
 
  (defthm local-special-32-bit-overflow-reduction
89
 
    (implies
90
 
     (and
91
 
      (syntaxp (quotep c))
92
 
      (equal (local-loghead 16 c) 0)
93
 
      (integerp c)
94
 
      (integerp x))
95
 
     (equal (signed-byte-p 32 (+ c x))
96
 
            (signed-byte-p 16 (+ (local-logtail 16 c) (local-logtail 16 x))))))
97
 
  
98
 
     )
99
 
 
100
 
 
101
 
))
102
 
 
103
 
(include-book "ihs/ihs-lemmas" :dir :system)
104
 
 
105
 
(defthm special-32-bit-overflow-reduction
106
 
  (implies
107
 
   (and
108
 
    (syntaxp (quotep c))
109
 
    (equal (loghead 16 c) 0)
110
 
    (integerp c)
111
 
    (integerp x))
112
 
   (equal (signed-byte-p 32 (+ c x))
113
 
          (signed-byte-p 16 (+ (logtail 16 c) (logtail 16 x)))))
114
 
  :hints (("Goal" :in-theory `(logapp loghead logtail logcar expt2 imod ifloor)
115
 
           :use (:functional-instance
116
 
                 local-special-32-bit-overflow-reduction
117
 
                 (local-ifloor  ifloor)
118
 
                 (local-imod    imod)
119
 
                 (local-expt2   expt2)
120
 
                 (local-logcar  logcar)
121
 
                 (local-loghead loghead)
122
 
                 (local-logtail logtail)
123
 
                 (local-logapp  logapp)))))
124
 
 
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
 
31
(in-package "ACL2")
 
32
 
 
33
(local
 
34
 (encapsulate
 
35
     ()
 
36
 
 
37
(encapsulate
 
38
    (
 
39
     ((local-ifloor * *) => *)
 
40
     ((local-imod * *) => *)
 
41
     ((local-expt2 *) => *)
 
42
     ((local-logcar *) => *)
 
43
     ((local-loghead * *) => *)
 
44
     ((local-logtail * *) => *)
 
45
     ((local-logapp * * *) => *)
 
46
     )
 
47
 
 
48
  (local
 
49
   (encapsulate
 
50
       ()
 
51
 
 
52
     (defun local-ifloor (i j)
 
53
       (floor (ifix i) (ifix j)))
 
54
 
 
55
     (defun local-imod (i j)
 
56
       (mod (ifix i) (ifix j)))
 
57
 
 
58
     (defun local-expt2 (n)
 
59
       (expt 2 (nfix n)))
 
60
 
 
61
     (defun local-logcar (i)
 
62
       (local-imod i 2))
 
63
 
 
64
     (defun local-loghead (size i)
 
65
       (local-imod i (local-expt2 size)))
 
66
 
 
67
     (defun local-logtail (pos i)
 
68
       (local-ifloor i (local-expt2 pos)))
 
69
 
 
70
     (defun local-logapp (size i j)
 
71
       (let ((j (ifix j)))
 
72
         (+ (local-loghead size i) (* j (local-expt2 size)))))
 
73
 
 
74
     ))
 
75
 
 
76
  (defthm local-ifloor-defn
 
77
    (equal (local-ifloor i j)
 
78
           (floor (ifix i) (ifix j))))
 
79
 
 
80
  (defthm local-imod-defn
 
81
    (equal (local-imod i j)
 
82
           (mod (ifix i) (ifix j))))
 
83
 
 
84
  (defthm local-expt2-defn
 
85
    (equal (local-expt2 n)
 
86
           (expt 2 (nfix n))))
 
87
 
 
88
  (defthm local-logcar-defn
 
89
    (equal (local-logcar i)
 
90
           (local-imod i 2)))
 
91
 
 
92
  (defthm local-loghead-defn
 
93
    (equal (local-loghead size i)
 
94
           (local-imod i (local-expt2 size))))
 
95
 
 
96
  (defthm local-logtail-defn
 
97
    (equal (local-logtail size i)
 
98
           (local-ifloor i (local-expt2 size))))
 
99
 
 
100
  (defthm local-logapp-defn
 
101
    (equal (local-logapp size i j)
 
102
           (let ((j (ifix j)))
 
103
             (+ (local-loghead size i) (* j (local-expt2 size))))))
 
104
 
 
105
  )
 
106
 
 
107
(encapsulate
 
108
    ()
 
109
 
 
110
    (local (include-book "arithmetic-3/bind-free/top" :dir :system))
 
111
 
 
112
    (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
 
113
 
 
114
; Matt K.: There was formerly a set-default-hints at the end of an embedded
 
115
; encapsulate, which had no effect since set-default-hints was local to that
 
116
; encapsulate.
 
117
 
 
118
  (defthm local-special-32-bit-overflow-reduction
 
119
    (implies
 
120
     (and
 
121
      (syntaxp (quotep c))
 
122
      (equal (local-loghead 16 c) 0)
 
123
      (integerp c)
 
124
      (integerp x))
 
125
     (equal (signed-byte-p 32 (+ c x))
 
126
            (signed-byte-p 16 (+ (local-logtail 16 c) (local-logtail 16 x))))))
 
127
 
 
128
     )
 
129
 
 
130
 
 
131
))
 
132
 
 
133
(include-book "ihs/ihs-lemmas" :dir :system)
 
134
 
 
135
(defthm special-32-bit-overflow-reduction
 
136
  (implies
 
137
   (and
 
138
    (syntaxp (quotep c))
 
139
    (equal (loghead 16 c) 0)
 
140
    (integerp c)
 
141
    (integerp x))
 
142
   (equal (signed-byte-p 32 (+ c x))
 
143
          (signed-byte-p 16 (+ (logtail 16 c) (logtail 16 x)))))
 
144
  :hints (("Goal" :in-theory `(logapp loghead logtail logcar expt2 imod ifloor)
 
145
           :use (:functional-instance
 
146
                 local-special-32-bit-overflow-reduction
 
147
                 (local-ifloor  ifloor)
 
148
                 (local-imod    imod)
 
149
                 (local-expt2   expt2)
 
150
                 (local-logcar  logcar)
 
151
                 (local-loghead loghead)
 
152
                 (local-logtail logtail)
 
153
                 (local-logapp  logapp)))))
 
154