← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/ihs/basic-definitions.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/ihs/basic-definitions.lisp
29
29
;;;    Modified for ACL2 Version_2.7 by:
30
30
;;;    Matt Kaufmann, kaufmann@cs.utexas.edu
31
31
;;;
 
32
;;;    Modified October 2014 by Jared Davis <jared@centtech.com>
 
33
;;;    Ported documentation to XDOC
 
34
;;;
32
35
;;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
33
36
 
34
37
(in-package "ACL2")
35
 
(include-book "ihs-doc-topic")
 
38
(include-book "std/util/define" :dir :system)
36
39
(local (include-book "math-lemmas"))
37
40
(local (include-book "quotient-remainder-lemmas"))
38
41
 
39
 
(deflabel logops
40
 
  :doc ":doc-section ihs
41
 
 
42
 
   Definitions and lemmas about logical operations on integers.~/~/
43
 
 
44
 
   The books \"logops-definitions\" and \"logops-lemmas\" contain a theory of
45
 
   the logical operations on numbers defined by CLTL (Section 12.7), and a
46
 
   portable implementation of the CLTL byte manipulation functions (Section
47
 
   12.8).  These books also extend the CLTL logical operations and byte
48
 
   manipulation theory with a few new definitions, lemmas supporting
49
 
   those definitions, and useful macros.
50
 
 
51
 
   These books were developed as a basis for the formal specification and
52
 
   verification of hardware, where integers are used to represent binary
53
 
   signals and busses.  These books should be general enough, however, to be
54
 
   used as a basis for reasoning about packed data structures, bit-encoded
55
 
   sets, and other applications of logical operations on integers.~/")
56
 
 
57
 
(deflabel logops-definitions
58
 
  :doc ":doc-section logops
59
 
  A book a definitions of logical operations on numbers.
60
 
  ~/
61
 
 
62
 
  This book, along with \"logops-lemmas\", includes a theory of the Common Lisp
63
 
  logical operations on numbers, a portable implementation of the Common Lisp
64
 
  byte operations, extensions to those theories, and some useful macros.
65
 
  This book contains only definitions, lemmas necessary to admit those
66
 
  definitions, and selected type lemmas.  By `type lemmas' we mean any lemmas
67
 
  about the logical operations that we have found necessary to admit
68
 
  functions that use these operations as GOLD.  We have separated these `type
69
 
  lemmas' from the large body of other lemmas in \"logops-lemmas\" to allow a
70
 
  user to use this book to define GOLD functions without having to also
71
 
  include the extensive theory in \"logops-lemmas\".
72
 
  ~/
73
 
 
74
 
  The standard Common Lisp logical operations on numbers are defined on the
75
 
  signed integers, and return signed integers as appropriate.  This allows a
76
 
  high level, signed interpretation of hardware operations if that is
77
 
  appropriate for the specification at hand.  We also provide unsigned
78
 
  versions of several of the standard logical operations for use in
79
 
  specifications where fixed-length unsigned integers are used to model
80
 
  hardware registers and busses.  This view of hardware is used, for example,
81
 
  in Yuan Yu's Nqthm specification of the Motorola MC68020.~/")
82
 
 
 
42
(defxdoc logops
 
43
  :parents (ihs)
 
44
  :short "Definitions and lemmas about logical operations on integers."
 
45
 
 
46
  :long "<p>The books @(see logops-definitions) and @(see logops-lemmas)
 
47
contain a theory of the logical operations on numbers defined by CLTL (Section
 
48
12.7), and a portable implementation of the CLTL byte manipulation
 
49
functions (Section 12.8).  These books also extend the CLTL logical operations
 
50
and byte manipulation theory with a few new definitions, lemmas supporting
 
51
those definitions, and useful macros.</p>
 
52
 
 
53
<p>These books were developed as a basis for the formal specification and
 
54
verification of hardware, where integers are used to represent binary signals
 
55
and busses.  These books should be general enough, however, to be used as a
 
56
basis for reasoning about packed data structures, bit-encoded sets, and other
 
57
applications of logical operations on integers.</p>")
 
58
 
 
59
(defxdoc logops-definitions
 
60
  :parents (ihs)
 
61
  :short "A book a definitions of logical operations on numbers."
 
62
 
 
63
  :long "<p>This book, along with @(see logops-lemmas), includes a theory of
 
64
the Common Lisp logical operations on numbers, a portable implementation of the
 
65
Common Lisp byte operations, extensions to those theories, and some useful
 
66
macros.</p>
 
67
 
 
68
<p>This book contains only definitions, lemmas necessary to admit those
 
69
definitions, and selected type lemmas.  By \"type lemmas\" we mean any lemmas
 
70
about the logical operations that we have found necessary to verify the guards
 
71
of functions that use these operations.  We have separated these \"type
 
72
lemmas\" from the large body of other lemmas in @(see logops-lemmas) to allow a
 
73
user to use this book to define guard-verified functions without having to also
 
74
include the extensive theory in @('logops-lemmas').</p>
 
75
 
 
76
<p>The standard Common Lisp logical operations on numbers are defined on the
 
77
signed integers, and return signed integers as appropriate.  This allows a high
 
78
level, signed interpretation of hardware operations if that is appropriate for
 
79
the specification at hand.  We also provide unsigned versions of several of the
 
80
standard logical operations for use in specifications where fixed-length
 
81
unsigned integers are used to model hardware registers and busses.  This view
 
82
of hardware is used, for example, in Yuan Yu's Nqthm specification of the
 
83
Motorola MC68020.</p>")
 
84
 
 
85
(local (xdoc::set-default-parents logops-definitions))
83
86
 
84
87
; [Jared] some trivial rules that are useful for the MBE substitutions
85
88
 
115
118
                  (equal (ash i pos)
116
119
                         (* i (expt 2 pos))))))
117
120
 
118
 
 
119
 
 
120
 
 
121
 
;;;****************************************************************************
122
 
;;;
123
 
;;;    Definitions -- Round 1.
124
 
;;;
125
 
;;;  Type predicates and functions.
126
 
;;;
127
 
;;;  BITP b
128
 
;;;  BFIX b
129
 
;;;  LBFIX b
130
 
;;;  ZBP x
131
 
;;;
132
 
;;;****************************************************************************
133
 
 
134
 
(defun-inline bitp (b)
135
 
  ":doc-section logops-definitions
136
 
  A predicate form of the type declaration (TYPE BIT b).
137
 
  ~/~/~/"
138
 
  (declare (xargs :guard t))
 
121
(local (defthm logand-positive
 
122
         (implies (natp mask)
 
123
                  (<= 0 (logand i mask)))
 
124
         :rule-classes ((:linear))))
 
125
 
 
126
(local
 
127
 (encapsulate
 
128
   ()
 
129
   (local (defun my-induct (i size)
 
130
            (if (zp size)
 
131
                (list size i)
 
132
              (my-induct (ash i -1)
 
133
                         (- size 1)))))
 
134
 
 
135
   (defthmd mod-of-expt-2-is-logand
 
136
     (implies (and (integerp size)
 
137
                   (>= size 0)
 
138
                   (integerp i))
 
139
              (equal (mod i (expt 2 size))
 
140
                     (logand i (1- (ash 1 size)))))
 
141
     :hints(("Goal" :induct (my-induct i size))))))
 
142
 
 
143
 
 
144
(define bitp (b)
 
145
  :short "Bit recognizer.  @('(bitp b)') recognizes 0 and 1."
 
146
  :long "<p>This is a predicate form of the @(see type-spec) declaration
 
147
@('(TYPE BIT b)').</p>"
 
148
  :returns bool
 
149
  :inline t
 
150
  :enabled t
 
151
  :no-function t ;; Sigh, switching to :abbreviation breaks various proofs
139
152
  (or (eql b 0)
140
153
      (eql b 1)))
141
154
 
142
 
(defun-inline bfix (b)
143
 
  ":doc-section logops-definitions
144
 
  (BFIX b) coerces any object to a bit (0 or 1) by coercing non-1 objects to 0.
145
 
  ~/~/~/"
146
 
  (declare (xargs :guard t))
147
 
  (if (eql b 1) 1 0))
148
 
 
149
 
(defmacro lbfix (x)
150
 
  ":doc-section logops-definitions
151
 
   (LBFIX b) is logically (BFIX b), but requires (BITP b) as a guard and expands
152
 
   to just b.
153
 
   ~/~/~/"
154
 
  `(mbe :logic (bfix ,x) :exec ,x))
155
 
 
156
 
(defun-inline zbp (x)
157
 
  ":doc-section logops-definitions
158
 
  (ZBP x) tests for `zero bits'.  Any object other than 1 is considered a
159
 
  zero bit.
160
 
  ~/~/~/"
161
 
  (declare (xargs :guard (bitp x)))
 
155
(define bfix (b)
 
156
  :parents (logops-definitions bitp)
 
157
  :short "Bit fix.  @('(bfix b)') is a fixing function for @(see bitp)s.  It
 
158
 coerces any object to a bit (0 or 1) by coercing non-1 objects to 0."
 
159
  :long "<p>See also @(see lbfix).</p>"
 
160
  :inline t
 
161
  :returns bit
 
162
  :enabled t
 
163
  :no-function t ;; Sigh, switching to :abbreviation breaks various proofs
 
164
  (if (eql b 1)
 
165
      1
 
166
    0))
 
167
 
 
168
(defsection lbfix
 
169
  :parents (logops-definitions bitp)
 
170
  :short "Logical bit fix.  @('(lbfix b)') is logically identical to @('(bfix
 
171
b)') but executes as the identity.  It requires @('(bitp b)') as a guard, and
 
172
expands to just @('b')."
 
173
  :long "@(def lbfix)"
 
174
 
 
175
  (defmacro lbfix (x)
 
176
    `(mbe :logic (bfix ,x) :exec ,x)))
 
177
 
 
178
(define zbp
 
179
  :parents (logops-definitions bitp)
 
180
  :short "Zero bit recognizer.  @('(zbp x)') tests for zero bits.  Any object
 
181
other than @('1') is considered to be a zero bit."
 
182
  ((x bitp))
 
183
  :returns bool
 
184
  :enabled t
 
185
  :inline t
162
186
  (mbe :logic (equal (bfix x) 0)
163
187
       :exec (/= (the (unsigned-byte 1) x) 1)))
164
188
 
165
 
(defthm bitp-bfix
166
 
  (bitp (bfix b))
167
 
  :doc ":doc-section bitp
168
 
  Rewrite: (BITP (BFIX b)).
169
 
  ~/~/~/")
170
 
 
171
 
(defthm bfix-bitp
172
 
  (implies (bitp b)
173
 
           (equal (bfix b) b))
174
 
  :hints (("Goal" :in-theory (enable bitp)))
175
 
  :doc ":doc-section bfix
176
 
  Rewrite: (BFIX b) = b, when b is a bit.
177
 
  ~/~/~/")
178
 
 
179
 
 
180
 
 
181
 
 
182
 
;;;****************************************************************************
183
 
;;;
184
 
;;;  Definition -- Round 2.
185
 
;;;
186
 
;;;  Extensions to the CLTL logical operations and byte functions.
187
 
;;;
188
 
;;;  IFLOOR i j
189
 
;;;  IMOD i j
190
 
;;;  EXPT2 n
191
 
;;;
192
 
;;;  LOGCAR i
193
 
;;;  LOGCDR i
194
 
;;;  LOGCONS b i
195
 
;;;  LOGBIT pos i
196
 
;;;  LOGMASK size
197
 
;;;  LOGMASKP i
198
 
;;;  LOGHEAD size i
199
 
;;;  LOGTAIL pos i
200
 
;;;  LOGAPP size i j
201
 
;;;  LOGRPL size i j
202
 
;;;  LOGEXT size i
203
 
;;;  LOGREV size i
204
 
;;;  LOGSAT size i
205
 
;;;
206
 
;;;  LOGEXTU final-size ext-size i
207
 
;;;  LOGNOTU size i
208
 
;;;  ASHU size i cnt
209
 
;;;  LSHU size i cnt
210
 
;;;
211
 
;;;  After the definitions, we define a guard macro for each that has a
212
 
;;;  non-trivial guard, and then define :TYPE-PRESCRIPTIONS for them.  We
213
 
;;;  always define our own :TYPE-PRESCRIPTIONS in insure that we always have
214
 
;;;  the strongest ones possible when this book is loaded.  Note that we
215
 
;;;  consider IFLOOR, IMOD, and EXPT2 to be abbreviations.
216
 
;;;
217
 
;;;****************************************************************************
218
 
 
219
 
(defun-inline ifloor (i j)
220
 
  ":doc-section logops-definitions
221
 
  (IFLOOR i j) is the same as floor, except that it coerces its
222
 
  arguments to integers.
223
 
  ~/~/~/"
224
 
  (declare (xargs :guard (and (integerp i)
225
 
                              (integerp j)
226
 
                              (not (= 0 j)))))
 
189
(defsection bitp-basics
 
190
  :extension bitp
 
191
 
 
192
  (defthm bitp-bfix
 
193
    (bitp (bfix b)))
 
194
 
 
195
  (defthm bfix-bitp
 
196
    (implies (bitp b)
 
197
             (equal (bfix b) b))))
 
198
 
 
199
 
 
200
(define ifloor
 
201
  :short "@('(ifloor i j)') is the same as @(see floor), except that it coerces
 
202
  its arguments to integers."
 
203
  ((i integerp)
 
204
   (j (and (integerp j)
 
205
           (not (= 0 j)))))
 
206
  :returns (int integerp
 
207
                :rule-classes :type-prescription
 
208
                :name ifloor-type)
 
209
  :inline t
 
210
  :enabled t
227
211
  (mbe :logic (floor (ifix i) (ifix j))
228
212
       :exec (floor i j)))
229
213
 
230
 
(defun-inline imod (i j)
231
 
  ":doc-section logops-definitions
232
 
  (IMOD i j) is the same as mod, except that it coerces its
233
 
  arguments to integers.
234
 
  ~/~/~/"
235
 
  (declare (xargs :guard (and (integerp i)
236
 
                              (integerp j)
237
 
                              (not (= 0 j)))))
 
214
(define imod
 
215
  :short "@('(imod i j)') is the same as @(see mod), except that it coerces its
 
216
  arguments to integers."
 
217
  ((i integerp)
 
218
   (j (and (integerp j)
 
219
           (not (= 0 j)))))
 
220
  :returns (int integerp
 
221
                :rule-classes :type-prescription
 
222
                :name imod-type)
 
223
  :inline t
 
224
  :enabled t
238
225
  (mbe :logic (mod (ifix i) (ifix j))
239
226
       :exec (mod i j)))
240
227
 
241
 
(defun-inline expt2 (n)
242
 
  ":doc-section logops-definitions
243
 
  (EXPT2 n) is the same as 2^n, except that it coerces its
244
 
  argument to a natural.
245
 
  ~/~/~/"
246
 
  (declare (xargs :guard (and (integerp n)
247
 
                              (<= 0 n))))
 
228
(define expt2
 
229
  :short "@('(expt2 n)') is the same as @('(expt 2 n)'), except that it coerces
 
230
  its argument to a natural."
 
231
  ((n natp))
 
232
  :returns (nat natp
 
233
                :rule-classes :type-prescription
 
234
                :name expt2-type)
 
235
  :enabled t
 
236
  :inline t
248
237
  (mbe :logic (expt 2 (nfix n))
249
 
       :exec (ash 1 n)))
250
 
 
251
 
(defun-inline logcar (i)
252
 
  ":doc-section logops-definitions
253
 
  (LOGCAR i) is the CAR of an integer conceptualized as a bit-vector (where the
254
 
  least significant bit is at the head of the list).
255
 
  ~/~/~/"
256
 
  (declare (xargs :guard (integerp i)))
 
238
       :exec (the unsigned-byte
 
239
                  (ash 1 (the unsigned-byte n)))))
 
240
 
 
241
 
 
242
(define logcar
 
243
  :short "Least significant bit of a number."
 
244
  ((i integerp))
 
245
  :returns bit
 
246
  :long "<p>@('(logcar i)') is the @(see car) of an integer conceptualized as a
 
247
bit-vector, where the least significant bit is at the head of the list.</p>
 
248
 
 
249
<p>In languages like C, this might be written as @('i & 1').</p>"
 
250
  :enabled t
 
251
  :inline t
257
252
  (mbe :logic (imod i 2)
258
 
       :exec (the (unsigned-byte 1) (logand i 1))))
259
 
 
260
 
(defun-inline logcdr (i)
261
 
  ":doc-section logops-definitions
262
 
  (LOGCDR i) is the CDR of an integer conceptualized as a bit-vector (where the
263
 
  least significant bit is at the head of the list).
264
 
  ~/~/~/"
265
 
  (declare (xargs :guard (integerp i)))
 
253
       :exec (the (unsigned-byte 1) (logand (the integer i) 1)))
 
254
  ///
 
255
  (defthm logcar-type
 
256
    (bitp (logcar i))
 
257
    :rule-classes ((:rewrite)
 
258
                   (:type-prescription :corollary (natp (logcar i)))
 
259
                   (:generalize :corollary
 
260
                    (or (equal (logcar i) 0)
 
261
                        (equal (logcar i) 1))))))
 
262
 
 
263
(define logcdr
 
264
  :short "All but the least significant bit of a number."
 
265
  ((i integerp))
 
266
  :returns (int integerp
 
267
                :rule-classes :type-prescription
 
268
                :name logcdr-type)
 
269
  :long "<p>@('(logcdr i)') is the @(see cdr) of an integer conceptualized as a
 
270
bit-vector, where the least significant bit is at the head of the list.</p>
 
271
 
 
272
<p>In languages like C, this might be written as @('i >> 1').</p>"
 
273
  :enabled t
 
274
  :inline t
266
275
  (mbe :logic (ifloor i 2)
267
 
       :exec (ash i -1)))
268
 
 
269
 
(defun-inline logcons (b i)
270
 
  ":doc-section logops-definitions
271
 
  (LOGCONS b i) is the CONS operation for integers conceptualized as
272
 
  bit-vectors (where i is multiplied by 2 and b becomes the new least
273
 
  significant bit).
274
 
  ~/
275
 
  For clarity and efficiency, b is required to be BITP.~/~/"
276
 
  (declare (xargs :guard (and (bitp b)
277
 
                              (integerp i))))
 
276
       :exec (the integer (ash (the integer i) -1))))
 
277
 
 
278
(define logcons
 
279
  :short "@('(logcons b i)') is the @(see cons) operation for integers,
 
280
conceptualized as bit-vectors, where the least significant bit is at the head
 
281
of the list."
 
282
  ((b bitp     "LSB of the result.")
 
283
   (i integerp "All but the LSB of the result."))
 
284
  :returns (int integerp
 
285
                :rule-classes :type-prescription
 
286
                :name logcons-type)
 
287
  :long "<p>In languages like C, this might be written as @('(i << 1) + b').</p>
 
288
 
 
289
<p>See also @(see logcar) and @(see logcdr).</p>"
 
290
  :inline t
 
291
  :enabled t
278
292
  (mbe :logic (let ((b (bfix b))
279
293
                    (i (ifix i)))
280
294
                (+ b (* 2 i)))
281
 
       :exec (+ b (ash i 1))))
282
 
 
283
 
(defun-inline logbit (pos i)
284
 
  ":doc-section logops-definitions
285
 
  (LOGBIT pos i) returns the bit of i at bit-position pos.
286
 
  ~/
287
 
  This is a binary equivalent to the Common Lisp function (LOGBITP pos i).~/~/"
288
 
  (declare (xargs :guard (and (integerp pos)
289
 
                              (>= pos 0)
290
 
                              (integerp i))))
291
 
  (if (logbitp pos i) 1 0))
292
 
 
293
 
(defun-inline logmask (size)
294
 
  ":doc-section logops-definitions
295
 
  (LOGMASK size) creates a low-order, size-bit mask.
296
 
  ~/~/~/"
297
 
  (declare (xargs :guard (and (integerp size)
298
 
                              (>= size 0))))
 
295
       :exec (the integer
 
296
                  (+ (the (unsigned-byte 1) b)
 
297
                     (the integer (ash i 1))))))
 
298
 
 
299
(define logbit
 
300
  :parents (logops-definitions logbitp)
 
301
  :short "@('(logbit pos i)') returns the bit of @('i') at bit-position @('pos')
 
302
as a @(see bitp), 0 or 1."
 
303
  ((pos natp)
 
304
   (i   integerp))
 
305
  :returns bit
 
306
  :long "<p>This is just like the Common Lisp function @('(logbitp pos i)'),
 
307
except that we return 1 or 0 (instead of t or nil).</p>
 
308
 
 
309
<p>In languages like C, this might be written as @('(i >> pos) & 1').</p>"
 
310
  :enabled t
 
311
  :inline t
 
312
  :no-function t ;; Sigh, switching to :abbreviation breaks various proofs
 
313
  (if (logbitp pos i)
 
314
      1
 
315
    0)
 
316
 
 
317
  ///
 
318
  (defthm logbit-type
 
319
    (bitp (logbit pos i))
 
320
    :rule-classes ((:rewrite)
 
321
                   (:type-prescription :corollary (natp (logbit pos i))))
 
322
    ;; BOZO want a generalize rule like in logcar?
 
323
    ))
 
324
 
 
325
 
 
326
(define logmask
 
327
  :short "@('(logmask size)') creates a low-order, @('size')-bit mask."
 
328
  ((size natp))
 
329
  :returns (nat natp
 
330
                :rule-classes :type-prescription
 
331
                :name logmask-type)
 
332
  :long "<p>In languages like C, this might be written as @('(1 << size) - 1').</p>"
 
333
  :enabled t
 
334
  :inline t
299
335
  (mbe :logic (- (expt2 size) 1)
300
 
       :exec (- (ash 1 size) 1)))
 
336
       :exec (the unsigned-byte (1- (the unsigned-byte (ash 1 size))))))
301
337
 
302
 
(defun logmaskp (i)
303
 
  ":doc-section logops-definitions
304
 
  (LOGMASKP i) recognizes positive masks.
305
 
  ~/~/~/"
306
 
  (declare (xargs :guard t))
 
338
(define logmaskp
 
339
  :short "@('(logmaskp i)') recognizes positive bit-masks, i.e., numbers of the
 
340
form @($2^n - 1$)."
 
341
  (i)
 
342
  :returns bool
 
343
  :enabled t
 
344
  :long "<p>Note that this function explicitly checks @('(integerp i)'), which
 
345
means it doesn't satisfy an @(see int-equiv) congruence.  See also @(see
 
346
bitmaskp), which fixes its argument and may execute slightly faster.</p>"
307
347
  (mbe :logic (and (integerp i)
308
348
                   (>= i 0) ;; silly, this is implied by the equality below
309
349
                   (equal i (- (expt2 (integer-length i)) 1)))
310
350
       :exec (and (integerp i)
311
 
                  (= i (- (ash 1 (integer-length i)) 1)))))
312
 
 
313
 
(defund bitmaskp (i)
314
 
  ;; replacement for logmaskp that respects int-equiv
315
 
  (declare (xargs :guard (integerp i)))
316
 
  (logmaskp (ifix i)))
317
 
 
318
 
(defun-inline loghead (size i)
319
 
  ":doc-section logops-definitions
320
 
  (LOGHEAD size i) returns the size low-order bits of i.
321
 
  ~/~/
322
 
  By convention we define (LOGHEAD 0 i) as 0, but this definition is a bit
323
 
  arbitrary.~/"
324
 
  (declare (xargs :guard (and (integerp size)
325
 
                              (>= size 0)
326
 
                              (integerp i))))
 
351
                  (eql i (the unsigned-byte
 
352
                              (- (the unsigned-byte (ash 1 (integer-length i)))
 
353
                                 1))))))
 
354
 
 
355
(define bitmaskp
 
356
  :short "@('(bitmaskp i)') recognizes positive masks, i.e., numbers of the form
 
357
@($2^n - 1$).  It is like @(see logmaskp) but properly treats non-integers as 0."
 
358
  ((i integerp))
 
359
  :returns bool
 
360
  :inline t
 
361
  (mbe :logic (logmaskp (mbe :logic (ifix i)
 
362
                             :exec i))
 
363
       :exec (eql i (the unsigned-byte
 
364
                         (- (the unsigned-byte (ash 1 (integer-length i)))
 
365
                            1)))))
 
366
 
 
367
(define loghead
 
368
  :short "@('(loghead size i)') returns the @('size') low-order bits of @('i')."
 
369
  ((size (and (integerp size)
 
370
              (<= 0 size))
 
371
         :type unsigned-byte)
 
372
   (i    integerp))
 
373
  :returns (nat natp
 
374
                :rule-classes :type-prescription
 
375
                :name loghead-type)
 
376
  :long "<p>In languages like C, this might be written as @('i & ((1 << size) -
 
377
1)').</p>
 
378
 
 
379
<p>By convention we define @('(loghead 0 i)') as 0.  This definition is a
 
380
bit arbitrary but generally leads to nice lemmas.</p>"
 
381
  :inline t
 
382
  :enabled t
 
383
  :split-types t
 
384
  :guard-hints(("Goal" :in-theory (enable mod-of-expt-2-is-logand)))
327
385
  (mbe :logic (imod i (expt2 size))
328
 
       ;; BOZO it'd be nicer to give this an :exec of (logand i (1- (ash 1
329
 
       ;; size))), but that'll require some additional lemmas...
330
 
       :exec (mod i (ash 1 size))))
 
386
       :exec
 
387
       (the unsigned-byte
 
388
            (logand i (the unsigned-byte
 
389
                           (1- (the unsigned-byte (ash 1 size))))))))
331
390
 
332
 
(defun-inline logtail (pos i)
333
 
  ":doc-section logops-definitions
334
 
  (LOGTAIL pos i) returns the high-order part of i starting at bit position
335
 
  pos.
336
 
  ~/~/~/"
 
391
(define logtail
 
392
  :short "@('(logtail pos i)') returns the high-order part of @('i'), starting
 
393
  at bit position @('pos')."
 
394
  ((pos (and (integerp pos)
 
395
             (<= 0 pos))
 
396
        :type unsigned-byte)
 
397
   (i   integerp))
 
398
  :returns (int integerp
 
399
                :rule-classes :type-prescription
 
400
                :name logtail-type)
 
401
  :long "<p>In languages like C, this might be written as @('i >> pos').</p>"
 
402
  :split-types t
 
403
  :inline t
 
404
  :enabled t
337
405
  (declare (xargs :guard (and (integerp pos)
338
406
                              (>= pos 0)
339
407
                              (integerp i))))
340
408
  (mbe :logic (ifloor i (expt2 pos))
341
409
       :exec (ash i (- (the unsigned-byte pos)))))
342
410
 
343
 
(defun logapp (size i j)
344
 
  ":doc-section logops-definitions
345
 
  (LOGAPP size i j) is a binary append of i to j (where i effectively becomes
346
 
  the 'low' bits and j becomes the 'high' bits).
347
 
  ~/~/
348
 
  LOGAPP is a specification for merging integers.  Note that i is truncated to
349
 
  size bits before merging with j, and that j is also shifted to the left by
350
 
  size bits before the merge.~/"
351
 
  (declare (xargs :guard (and (integerp size)
352
 
                              (>= size 0)
353
 
                              (integerp i)
354
 
                              (integerp j))))
 
411
(define logapp
 
412
  :short "@('(logapp size i j)') is a binary append of i to j, where i
 
413
  effectively becomes the 'low' bits and j becomes the 'high' bits."
 
414
  ((size (and (integerp size)
 
415
              (<= 0 size))
 
416
         :type unsigned-byte)
 
417
   (i    integerp)
 
418
   (j    integerp))
 
419
  :returns (int integerp
 
420
                :rule-classes :type-prescription
 
421
                :name logapp-type)
 
422
  :split-types t
 
423
  :long "<p>@('logapp') is a specification for merging integers.  Note that
 
424
@('i') is truncated to @('size') bits before merging with @('j'), and that @('j')
 
425
is shifted to the left by @('size') bits before the merge.</p>"
 
426
  :enabled t
355
427
  (mbe :logic (let ((j (ifix j)))
356
428
                (+ (loghead size i) (* j (expt2 size))))
357
429
       ;; BOZO could do better than calling loghead with some work
 
430
       ;; Could probably use logior instead of +.
358
431
       :exec (+ (loghead size i) (ash j size))))
359
432
 
360
 
(defun logrpl (size i j)
361
 
  ":doc-section logops-definitions
362
 
  (LOGRPL size i j) replaces the size low-order bits of j with the size
363
 
  low-order bits of i.
364
 
  ~/
365
 
  LOGRPL is a common specification for the result of storing short values into
366
 
  long words, i.e., the short value simply replaces the head of the long
367
 
  word.  This function is equivalent to (WRB i (BSP size 0) j).~/~/"
368
 
  (declare (xargs :guard (and (integerp size)
369
 
                              (>= size 0)
370
 
                              (integerp i)
371
 
                              (integerp j))))
 
433
(define logrpl
 
434
  :short "Logical replace.  @('(logrpl size i j)') replaces the @('size')
 
435
  low-order bits of @('j') with the @('size') low-order bits of @('i')."
 
436
  ((size (and (integerp size)
 
437
              (<= 0 size)))
 
438
   (i    integerp)
 
439
   (j    integerp))
 
440
  :returns (int integerp
 
441
                :rule-classes :type-prescription
 
442
                :name logrpl-type)
 
443
  :long "<p>@('logrpl') is a specification for the result of storing short
 
444
values into long words, i.e., the short value simply replaces the head of the
 
445
long word.</p>
 
446
 
 
447
<p>This function is equivalent to @('(WRB i (BSP size 0) j)').</p>"
 
448
  :enabled t
372
449
  (logapp size i (logtail size j)))
373
450
 
374
 
(defun logext (size i)
375
 
  ":doc-section logops-definitions
376
 
  (LOGEXT size i) \"sign-extends\" i to an integer with size - 1 significant
377
 
  bits.
378
 
  ~/
379
 
  LOGEXT coerces any integer i into a signed integer by `sign extending'
380
 
  the bit at size - 1 to infinity.  We specify LOGEXT in terms of the `size'
381
 
  of the result instead of as a bit position because we normally specify
382
 
  integer subranges by the number of significant (including sign) bits.
383
 
 
384
 
  Note that for consistency with SIGNED-BYTE-P, size must be strictly greater
385
 
  than 0.~/~/"
386
 
  (declare (xargs :guard (and (integerp size)
387
 
                              (> size 0)
388
 
                              (integerp i))))
389
 
  ;; BOZO could do better than this with MBE with some work, see centaur/bitops/sign-extend
390
 
  (logapp (1- size) i (if (logbitp (1- size) i) -1 0)))
391
 
 
392
 
(defun logrev1 (size i j)
393
 
  ":doc-section logops-definitions
394
 
  Helper function for LOGREV.
395
 
  ~/~/~/"
396
 
  (declare (xargs :guard (and (integerp size)
397
 
                              (>= size 0)
398
 
                              (integerp i)
399
 
                              (integerp j))))
 
451
(define logext
 
452
  :short "Logical sign extension, signed version.  @('(logext size i)')
 
453
sign-extends @('i') to an integer with @('size - 1') significant bits."
 
454
  ((size (and (integerp size)
 
455
              (< 0 size))
 
456
         :type unsigned-byte)
 
457
   (i    integerp))
 
458
  :returns (int integerp
 
459
                :rule-classes :type-prescription
 
460
                :name logext-type)
 
461
  :split-types t
 
462
  :long "<p>@('logext') coerces any integer @('i') into a signed integer by
 
463
\"sign extending\" the bit at @('size - 1') to infinity.</p>
 
464
 
 
465
<p>We specify logext in terms of the @('size') of the result instead of as a
 
466
bit position because we normally specify integer subranges by the number of
 
467
significant (including sign) bits.</p>
 
468
 
 
469
<p>This function returns a (possibly negative) integer.  For consistency with
 
470
@(see SIGNED-BYTE-P), @('size') must be strictly greater than 0.  In contrast,
 
471
the related function @(see logextu) carries out a sign-extension but only
 
472
returns the low @('size') bits, i.e., it always returns a natural number.</p>
 
473
 
 
474
<p>See also @(see bitops/fast-logext) for an optimized implementation of @(see
 
475
logext).</p>"
 
476
  :enabled t
 
477
 
 
478
  (let* ((size-1 (- size 1)))
 
479
    (declare (type unsigned-byte size-1))
 
480
    (logapp size-1 i
 
481
            (if (logbitp size-1 i)
 
482
                -1
 
483
              0))))
 
484
 
 
485
(define logrev1
 
486
  :parents (logrev)
 
487
  :short "Helper function for @(see logrev)."
 
488
  ((size (and (integerp size)
 
489
              (<= 0 size)))
 
490
   (i integerp)
 
491
   (j integerp))
 
492
  :returns (nat)
 
493
  :split-types t
 
494
  (declare (type unsigned-byte size)
 
495
           (type integer i j))
 
496
  :enabled t
400
497
  (if (zp size)
401
 
      (ifix j)
402
 
    (logrev1 (- size 1) (logcdr i) (logcons (logcar i) j))))
403
 
 
404
 
(defun logrev (size i)
405
 
  ":doc-section logops-definitions
406
 
  (LOGREV size i) bit-reverses the size low-order bits of i, discarding the
407
 
  high-order bits.
408
 
  ~/~/
409
 
  Normally we don't think of bit-reversing as a logical operation,
410
 
  even though its hardware implementation is trivial: simply reverse the
411
 
  wires leading from the source to the destination.  LOGREV is included as a
412
 
  logical operation to support the specification of DSPs, which may
413
 
  provide bit-reversing in their address generators to improve the
414
 
  performance of the FFT.
415
 
 
416
 
  LOGREV entails a recursive definition of bit-reversing via the helper
417
 
  function LOGREV1.~/"
418
 
  (declare (xargs :guard (and (integerp size)
419
 
                              (>= size 0)
420
 
                              (integerp i))))
 
498
      (mbe :logic (ifix j)
 
499
           :exec j)
 
500
    (logrev1 (the unsigned-byte (- size 1))
 
501
             (logcdr i)
 
502
             (logcons (logcar i) j))))
 
503
 
 
504
(local (defthm logrev1-type
 
505
         (implies (>= j 0)
 
506
                  (natp (logrev1 size i j)))
 
507
         :rule-classes :type-prescription
 
508
         :hints(("Goal" :in-theory (disable imod ifloor)))))
 
509
 
 
510
(define logrev
 
511
  :short "Logical reverse.  @('(logrev size i)') bit-reverses the @('size')
 
512
  low-order bits of @('i'), discarding the high-order bits."
 
513
  ((size (and (integerp size)
 
514
              (<= 0 size)))
 
515
   (i    integerp))
 
516
  :returns (nat natp
 
517
                :rule-classes :type-prescription
 
518
                :name logrev-type)
 
519
  :long "<p>Normally we don't think of bit-reversing as a logical operation,
 
520
even though its hardware implementation is trivial: simply reverse the wires
 
521
leading from the source to the destination.</p>
 
522
 
 
523
<p>@('logrev') is included as a logical operation to support the specification
 
524
of DSPs, which may provide bit-reversing in their address generators to improve
 
525
the performance of the FFT.</p>
 
526
 
 
527
<p>@('logrev') entails a recursive definition of bit-reversing via the helper
 
528
function @(see logrev1).</p>
 
529
 
 
530
<p>See also @(see bitops/fast-logrev) for some optimized definitions of @(see
 
531
logrev).</p>"
 
532
  :inline t
 
533
  :enabled t
421
534
  (logrev1 size i 0))
422
535
 
423
 
(defun logsat (size i)
424
 
  ":doc-section logops-definitions
425
 
  (LOGSAT size i) coerces i to a size-bit signed integer by saturation.
426
 
  ~/~/
427
 
  If i can be represented as a size-bit signed integer, then i is returned.
428
 
  Otherwise, (LOGSAT size i) returns the size-bit signed integer closest to
429
 
  i. For positive i, this will be 2^(size-1) - 1.  For negative i, this will
430
 
  be -(2^(size - 1)).
431
 
 
432
 
  Note that for consistency with SIGNED-BYTE-P, size must be strictly
433
 
  greater than 0.~/"
434
 
 
435
 
  (declare (xargs :guard (and (integerp size)
436
 
                              (< 0 size)
437
 
                              (integerp i))))
438
 
 
439
 
  (let* ((i (ifix i))                   ;?
440
 
         (val (expt2 (1- size)))
441
 
         (maxval (1- val))
 
536
(define logsat
 
537
  :short "Signed saturation.  @('(logsat size i)') coerces @('i') to a
 
538
  @('size')-bit signed integer by saturation."
 
539
  ((size (and (integerp size)
 
540
              (< 0 size))
 
541
         :type unsigned-byte)
 
542
   (i    integerp))
 
543
  :returns (int integerp
 
544
                :rule-classes :type-prescription
 
545
                :name logsat-type)
 
546
 
 
547
  :long "<p>If @('i') can be represented as a @('size')-bit signed integer,
 
548
then @('i') is returned unchanged.  Otherwise, @('(logsat size i)') returns
 
549
the @('size')-bit signed integer closest to @('i').  For positive i, this
 
550
will be @($2^{size-1} - 1$).  For negative @('i'), this will be 
 
551
@($-(2^{size-1}$).</p>
 
552
 
 
553
<p>This function returns a (possibly negative) integer.  For consistency with
 
554
@(see signed-byte-p), size must be strictly greater than 0.  In contrast, the
 
555
related @(see bitops/saturate) functions always return @('size')-bit natural
 
556
numbers.</p>"
 
557
 
 
558
  :split-types t
 
559
  :enabled t
 
560
  (let* ((i      (mbe :logic (ifix i) :exec i))
 
561
         (val    (expt2 (the unsigned-byte (1- size))))
 
562
         (maxval (the unsigned-byte (1- (the unsigned-byte val))))
442
563
         (minval (- val)))
443
 
 
 
564
    (declare (type unsigned-byte val maxval)
 
565
             (type integer i minval))
444
566
    (if (>= i maxval)
445
567
        maxval
446
568
      (if (<= i minval)
447
569
          minval
448
570
        i))))
449
571
 
450
 
(defun logextu (final-size ext-size i)
451
 
  ":doc-section logops-definitions
452
 
  (LOGEXTU final-size ext-size i) \"sign-extends\" i with (LOGEXT ext-size i),
453
 
  then truncates the result to final-size bits, creating an unsigned integer.
454
 
  ~/~/~/"
455
 
  (declare (xargs :guard (and (integerp final-size)
456
 
                              (>= final-size 0)
457
 
                              (integerp ext-size)
458
 
                              (> ext-size 0)
459
 
                              (integerp i))
460
 
                  :guard-hints (("Goal" :in-theory (disable exponents-add)))))
 
572
(define logextu
 
573
  :short "Logical sign extension, unsigned version.  @('(logextu final-size
 
574
 ext-size i)') \"sign-extends\" i with @('(logext ext-size i)'), then truncates
 
575
 the result to @('final-size') bits, creating an unsigned integer."
 
576
  ((final-size (and (integerp final-size)
 
577
                    (<= 0 final-size)))
 
578
   (ext-size   (and (integerp ext-size)
 
579
                    (< 0 ext-size)))
 
580
   (i          integerp))
 
581
  :returns (nat natp
 
582
                :rule-classes :type-prescription
 
583
                :name logextu-type)
 
584
  :enabled t
 
585
  :inline t
461
586
  (loghead final-size (logext ext-size i)))
462
587
 
463
 
(defun lognotu (size i)
464
 
  ":doc-section logops-definitions
465
 
  (LOGNOTU size i) is an unsigned logical NOT, truncating (LOGNOT i) to size
466
 
  bits.
467
 
  ~/~/~/"
468
 
  (declare (xargs :guard (and (integerp size)
469
 
                              (>= size 0)
470
 
                              (integerp i))))
 
588
(define lognotu
 
589
  :short "Logical negation, unsigned version.  @('(lognotu size i)') is an
 
590
 unsigned logical @('not').  It just truncates @('(lognot i)') to @('size')
 
591
 bits."
 
592
  ((size  (and (integerp size)
 
593
               (<= 0 size)))
 
594
   (i     integerp))
 
595
  :returns (nat natp
 
596
                :rule-classes :type-prescription
 
597
                :name lognotu-type)
 
598
  :enabled t
 
599
  :inline t
471
600
  (loghead size (lognot i)))
472
601
 
473
 
(defun ashu (size i cnt)
474
 
  ":doc-section logops-definitions
475
 
  (ASHU size i cnt) is an unsigned version of ASH.
476
 
  ~/
477
 
  ASHU is a fixed-width version of ASH. The integer i is first coerced to a
478
 
  signed integer by sign-extension, then shifted with ASH, and finally
479
 
  truncated back to a size-bit unsigned integer.~/~/"
480
 
  (declare (xargs :guard (and (integerp size)
481
 
                              (> size 0)
482
 
                              (integerp i)
483
 
                              (integerp cnt))
484
 
                  :guard-hints (("Goal" :in-theory (disable exponents-add)))))
 
602
(define ashu
 
603
  :short "Arithmetic shift, unsigned version."
 
604
  ((size (and (integerp size)
 
605
              (< 0 size)))
 
606
   (i    integerp)
 
607
   (cnt  integerp))
 
608
  :returns (nat natp
 
609
                :rule-classes :type-prescription
 
610
                :name ashu-type)
 
611
  :long "<p>@('ashu') is a fixed-width version of @(see ash).  The integer
 
612
@('i') is first coerced to a @('size')-bit signed integer by sign-extension,
 
613
then shifted with @('ash'), and finally truncated back to a @('size')-bit
 
614
unsigned integer.</p>
 
615
 
 
616
<p>See also @(see lshu) for a logical (instead of arithmetic) shift.</p>"
 
617
  :enabled t
485
618
  (loghead size (ash (logext size i) cnt)))
486
619
 
487
 
(defun lshu (size i cnt)
488
 
  ":doc-section logops-definitions
489
 
  (LSHU size i cnt) is an unsigned logical shift.
490
 
  ~/
491
 
  LSHU shifts i by cnt bits by first coercing i to an unsigned integer,
492
 
  performing the shift, and coercing the result to an unsigned integer.
493
 
  For cnt >= 0, (LSHU size i cnt) = (ASHU size i cnt).  This is a model
494
 
  of a size-bit logical shift register.~/~/"
495
 
  (declare (xargs :guard (and (integerp size)
496
 
                              (>= size 0)
497
 
                              (integerp i)
498
 
                              (integerp cnt))))
 
620
(define lshu
 
621
  :short "Logical shift, unsigned version."
 
622
  ((size (and (integerp size)
 
623
              (<= 0 size)))
 
624
   (i   integerp)
 
625
   (cnt integerp))
 
626
  :returns (nat natp
 
627
                :rule-classes :type-prescription
 
628
                :name lshu-type)
 
629
  :long "<p>@('lshu') is a fixed-width logical shift.  It shifts @('i')
 
630
by @('cnt') bits by first coercing @('i') to an unsigned integer of @('size')
 
631
bits, performing the shift, and coercing the result to an @('size')-bit
 
632
unsigned integer.</p>
 
633
 
 
634
<p>For @('cnt >= 0'), @('(lshu size i cnt) = (ashu size i cnt)').</p>
 
635
 
 
636
<p>This is a model of a size-bit logical shift register.</p>"
 
637
  :enabled t
499
638
  (loghead size (ash (loghead size i) cnt)))
500
639
 
501
640
 
502
641
 
503
 
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
504
 
;;;
505
 
;;;    Type Lemmas for the new LOGOPS.  Each function is DISABLEd after we
506
 
;;;    have enough information about it (except for IFLOOR, IMOD, and EXPT2,
507
 
;;;    which are considered abbreviations).  We prove even the most obvious
508
 
;;;    type lemmas because you never know what theory this book will be
509
 
;;;    loaded into, and unless the theory is strong enough you may not get
510
 
;;;    everthing you need.
511
 
;;;
512
 
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
513
 
 
514
 
(defthm ifloor-type
515
 
  (integerp (ifloor i j))
516
 
  :rule-classes :type-prescription
517
 
  :doc ":doc-section ifloor
518
 
  Type-prescription: (INTEGERP (IFLOOR I J)).
519
 
  ~/~/~/")
520
 
 
521
 
(defthm imod-type
522
 
  (integerp (imod i j))
523
 
  :rule-classes :type-prescription
524
 
  :doc ":doc-section imod
525
 
  Type-prescription: (INTEGERP (IMOD I J)).
526
 
  ~/~/~/")
527
 
 
528
 
(defthm expt2-type
529
 
  (natp (expt2 n))
530
 
  :rule-classes :type-prescription
531
 
  :doc ":doc-section expt2
532
 
  Type-prescription: (NATP (EXPT2 N)).
533
 
  ~/~/~/")
534
 
 
535
 
(defthm logcar-type
536
 
  (bitp (logcar i))
537
 
  :rule-classes ((:rewrite)
538
 
                 (:type-prescription :corollary (natp (logcar i)))
539
 
                 (:generalize :corollary
540
 
                              (or (equal (logcar i) 0)
541
 
                                  (equal (logcar i) 1))))
542
 
  :doc ":doc-section logcar
543
 
  Rewrite: (BITP (LOGCAR i)).
544
 
  ~/
545
 
  This rule is also stored as appropriate :TYPE-PRESCRIPTION and
546
 
  :GENERALIZE rules.~/~/")
547
 
 
548
 
(defthm logcdr-type
549
 
  (integerp (logcdr i))
550
 
  :rule-classes :type-prescription
551
 
  :doc ":doc-section logcdr
552
 
  Type-Prescription: (INTEGERP (LOGCDR I)).
553
 
  ~/~/~/")
554
 
 
555
 
(defthm logcons-type
556
 
  (integerp (logcons b i))
557
 
  :rule-classes :type-prescription
558
 
  :doc ":doc-section logcons
559
 
  Type-prescription: (INTEGERP (LOGCONS b i)).
560
 
  ~/~/~/")
561
 
 
562
 
(defthm logbit-type
563
 
  (bitp (logbit pos i))
564
 
  :rule-classes ((:rewrite)
565
 
                 (:type-prescription :corollary (natp (logbit pos i))))
566
 
  ;; BOZO want a generalize rule like in logcar?
567
 
  :doc ":doc-section logbit
568
 
  Rewrite: (BITP (LOGBIT pos i)).
569
 
  ~/
570
 
  This rule is also stored as an appropriate :TYPE-PRESCRIPTION.~/~/")
571
 
 
572
 
(defthm logmask-type
573
 
  (natp (logmask i))
574
 
  :rule-classes :type-prescription
575
 
  :doc ":doc-section logmask
576
 
  Type-Prescription: (NATP (LOGMASK i)).
577
 
  ~/~/~/")
578
 
 
579
 
(defthm loghead-type
580
 
  (natp (loghead size i))
581
 
  :rule-classes :type-prescription
582
 
  :doc ":doc-section loghead
583
 
  Type-prescription: (NATP (LOGHEAD size i)).
584
 
  ~/~/~/")
585
 
 
586
 
(defthm logtail-type
587
 
  (integerp (logtail pos i))
588
 
  :rule-classes :type-prescription
589
 
  :doc ":doc-section logcons
590
 
  Type-prescription: (INTEGERP (LOGTAIL POS I)).
591
 
  ~/~/~/")
592
 
 
593
 
(defthm logapp-type
594
 
  (integerp (logapp size i j))
595
 
  :rule-classes :type-prescription
596
 
  :doc ":doc-section logcons
597
 
  Type-prescription: (INTEGERP (LOGAPP SIZE I J)).
598
 
  ~/~/~/")
599
 
 
600
 
(defthm logrpl-type
601
 
  (integerp (logrpl size i j))
602
 
  :rule-classes :type-prescription
603
 
  :doc ":doc-section logcons
604
 
  Type-prescription: (INTEGERP (LOGRPL SIZE I J)).
605
 
  ~/~/~/")
606
 
 
607
 
(defthm logext-type
608
 
  (integerp (logext size i))
609
 
  :rule-classes :type-prescription
610
 
  :doc ":doc-section logext
611
 
  Type-Prescription: (INTEGERP (LOGEXT size i)).
612
 
  ~/~/~/")
613
 
 
614
 
(local (defthm logrev1-type
615
 
         (implies (>= j 0)
616
 
                  (natp (logrev1 size i j)))
617
 
         :rule-classes :type-prescription
618
 
         :hints(("Goal" :in-theory (disable imod ifloor)))))
619
 
 
620
 
(defthm logrev-type
621
 
  (natp (logrev size i))
622
 
  :rule-classes :type-prescription
623
 
  :doc ":doc-section logrev
624
 
  Type-prescription: (NATP (LOGREV size i)).
625
 
  ~/~/~/")
626
 
 
627
 
(defthm logsat-type
628
 
  (integerp (logsat size i))
629
 
  :rule-classes :type-prescription
630
 
  :doc ":doc-section logsat
631
 
  Type-Prescription: (INTEGERP (LOGSAT size i)).
632
 
  ~/~/~/")
633
 
 
634
 
(defthm logextu-type
635
 
  (natp (logextu final-size ext-size i))
636
 
  :rule-classes :type-prescription
637
 
  :doc ":doc-section logextu
638
 
  Type-prescription: (NATP (LOGEXTU final-size ext-size i)).
639
 
  ~/~/~/")
640
 
 
641
 
(defthm lognotu-type
642
 
  (natp (lognotu size i))
643
 
  :rule-classes :type-prescription
644
 
  :doc ":doc-section lognotu
645
 
  Type-prescription: (NATP (LOGNOTU size i)).
646
 
  ~/~/~/")
647
 
 
648
 
(defthm ashu-type
649
 
  (natp (ashu size i cnt))
650
 
  :rule-classes :type-prescription
651
 
  :doc ":doc-section ashu
652
 
  Type-prescription: (NATP (ASHU size i cnt)).
653
 
  ~/~/~/")
654
 
 
655
 
(defthm lshu-type
656
 
  (natp (lshu size i cnt))
657
 
  :rule-classes :type-prescription
658
 
  :doc ":doc-section lshu
659
 
  Type-prescription: (NATP (LSHU size i cnt)).
660
 
  ~/~/~/")
661
 
 
662
 
 
663
 
 
664
 
;;;****************************************************************************
665
 
;;;
666
 
;;;   Definitions -- Round 3.
667
 
;;;
668
 
;;;  Logical operations on single bits.
669
 
;;;
670
 
;;;  B-NOT i
671
 
;;;  B-AND i j
672
 
;;;  B-IOR i j
673
 
;;;  B-XOR i j
674
 
;;;  B-EQV i j
675
 
;;;  B-NAND i j
676
 
;;;  B-NOR i j
677
 
;;;  B-ANDC1 i j
678
 
;;;  B-ANDC2 i j
679
 
;;;  B-ORC1 i j
680
 
;;;  B-ORC2 i j
681
 
;;;
682
 
;;;****************************************************************************
683
 
 
684
 
(deflabel logops-bit-functions
685
 
 :doc ":doc-section logops-definitions
686
 
 Versions of the standard logical operations that operate on single bits.
687
 
 ~/~/
688
 
 
689
 
 We provide versions of the non-trivial standard logical operations that
690
 
 operate on single bits.  The reason that it is necessary to introduce these
691
 
 operations separate from the standard operations is the fact that LOGNOT
692
 
 applied to a BITP object never returns a BITP.  All arguments to these
693
 
 functions must be BITP, and we prove that each returns a BITP integer.  We
694
 
 define each function explicitly in terms of 0 and 1 to simplify
695
 
 reasoning.~/")
696
 
 
697
 
(defun-inline b-not (i)
698
 
  ":doc-section logops-bit-functions
699
 
  B-NOT ~/~/~/"
700
 
  (declare (xargs :guard (bitp i)))
 
642
(defxdoc logops-bit-functions
 
643
  :parents (logops-definitions bitp)
 
644
  :short "Versions of the standard logical operations that operate on single bits."
 
645
  :long "<p>We provide versions of the non-trivial standard logical operations
 
646
that operate on single bits.</p>
 
647
 
 
648
<p>One reason that it is useful to introduce these operations separately from
 
649
the standard operations is the fact that @(see lognot) applied to a @(see bitp)
 
650
object never returns a @(see bitp).</p>
 
651
 
 
652
<p>All arguments to these functions must be @(see bitp), and we prove that
 
653
each returns a @(see bitp) integer, i.e., 0 or 1.  We define each function
 
654
explicitly in terms of 0 and 1 to simplify reasoning.</p>")
 
655
 
 
656
(local (xdoc::set-default-parents logops-bit-functions))
 
657
 
 
658
(define b-not ((i bitp))
 
659
  :returns bit
 
660
  :short "Negation for @(see bitp)s."
 
661
  :inline t
 
662
  :enabled t
701
663
  (mbe :logic (if (zbp i) 1 0)
702
664
       :exec (the (unsigned-byte 1)
703
665
               (- 1 (the (unsigned-byte 1) i)))))
704
666
 
705
 
(defun-inline b-and (i j)
706
 
  ":doc-section logops-bit-functions
707
 
  B-AND ~/~/~/"
708
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
667
(define b-and ((i bitp) (j bitp))
 
668
  :returns bit
 
669
  :short "Conjunction for @(see bitp)s."
 
670
  :inline t
 
671
  :enabled t
709
672
  (mbe :logic (if (zbp i) 0 (if (zbp j) 0 1))
710
673
       :exec (the (unsigned-byte 1)
711
674
               (logand (the (unsigned-byte 1) i)
712
675
                       (the (unsigned-byte 1) j)))))
713
676
 
714
 
(defun-inline b-ior (i j)
715
 
  ":doc-section logops-bit-functions
716
 
  B-IOR ~/~/~/"
717
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
677
(define b-ior ((i bitp) (j bitp))
 
678
  :returns bit
 
679
  :short "Inclusive or for @(see bitp)s."
 
680
  :inline t
 
681
  :enabled t
718
682
  (mbe :logic (if (zbp i) (if (zbp j) 0 1) 1)
719
683
       :exec (the (unsigned-byte 1)
720
684
               (logior (the (unsigned-byte 1) i)
721
685
                       (the (unsigned-byte 1) j)))))
722
686
 
723
 
(defun-inline b-xor (i j)
724
 
  ":doc-section logops-bit-functions
725
 
  B-XOR ~/~/~/"
726
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
687
(define b-xor ((i bitp) (j bitp))
 
688
  :returns bit
 
689
  :short "Exclusive or for @(see bitp)s."
 
690
  :enabled t
 
691
  :inline t
727
692
  (mbe :logic (if (zbp i) (if (zbp j) 0 1) (if (zbp j) 1 0))
728
693
       :exec (the (unsigned-byte 1)
729
694
               (logxor (the (unsigned-byte 1) i)
730
695
                       (the (unsigned-byte 1) j)))))
731
696
 
732
 
(defun-inline b-eqv (i j)
733
 
  ":doc-section logops-bit-functions
734
 
  B-EQV ~/~/~/"
735
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
697
(define b-eqv ((i bitp) (j bitp))
 
698
  :returns bit
 
699
  :short "Equivalence (a.k.a. if and only if, xnor) for @(see bitp)s."
 
700
  :enabled t
 
701
  :inline t
736
702
  (mbe :logic (if (zbp i) (if (zbp j) 1 0) (if (zbp j) 0 1))
737
703
       ;; Goofy definition, Using logeqv or lognot of logxor would require
738
704
       ;; masking (they produce -1 for, e.g., (logeqv 0 0)).  So I'll just xor
743
709
                                 (the (unsigned-byte 1) j)))
744
710
                       1))))
745
711
 
746
 
(defun-inline b-nand (i j)
747
 
  ":doc-section logops-bit-functions
748
 
  B-NAND ~/~/~/"
749
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
712
(define b-nand ((i bitp) (j bitp))
 
713
  :returns bit
 
714
  :short "Negated and for @(see bitp)s."
 
715
  :enabled t
 
716
  :inline t
750
717
  (mbe :logic (if (zbp i) 1 (if (zbp j) 1 0))
751
718
       ;; Goofy :exec, similar to b-eqv for similar reasons
752
719
       :exec (the (unsigned-byte 1)
755
722
                                 (the (unsigned-byte 1) j)))
756
723
                       1))))
757
724
 
758
 
(defun-inline b-nor (i j)
759
 
  ":doc-section logops-bit-functions
760
 
  B-NOR ~/~/~/"
761
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
725
(define b-nor ((i bitp) (j bitp))
 
726
  :returns bit
 
727
  :short "Negated or for @(see bitp)s."
 
728
  :enabled t
 
729
  :inline t
762
730
  (mbe :logic (if (zbp i) (if (zbp j) 1 0) 0)
763
731
       :exec (the (unsigned-byte 1)
764
732
               (logxor (the (unsigned-byte 1)
766
734
                                 (the (unsigned-byte 1) j)))
767
735
                       1))))
768
736
 
769
 
(defun-inline b-andc1 (i j)
770
 
  ":doc-section logops-bit-functions
771
 
  B-ANDC1 ~/~/~/"
772
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
737
(define b-andc1 ((i bitp) (j bitp))
 
738
  :returns bit
 
739
  :short "And of @(see bitp)s, complementing the first."
 
740
  :enabled t
 
741
  :inline t
773
742
  (mbe :logic (if (zbp i) (if (zbp j) 0 1) 0)
774
743
       :exec (the (unsigned-byte 1)
775
744
               (logandc1 (the (unsigned-byte 1) i)
776
745
                         (the (unsigned-byte 1) j)))))
777
746
 
778
 
(defun-inline b-andc2 (i j)
779
 
  ":doc-section logops-bit-functions
780
 
  B-ANDC2 ~/~/~/"
781
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
747
(define b-andc2 ((i bitp) (j bitp))
 
748
  :returns bit
 
749
  :short "And of @(see bitp)s, complementing the second."
 
750
  :enabled t
 
751
  :inline t
782
752
  (mbe :logic (if (zbp i) 0 (if (zbp j) 1 0))
783
753
       :exec (the (unsigned-byte 1)
784
754
               (logandc2 (the (unsigned-byte 1) i)
785
755
                         (the (unsigned-byte 1) j)))))
786
756
 
787
 
(defun-inline b-orc1 (i j)
788
 
  ":doc-section logops-bit-functions
789
 
  B-ORC1 ~/~/~/"
790
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
757
(define b-orc1 ((i bitp) (j bitp))
 
758
  :returns bit
 
759
  :short "Inclusive or of @(see bitp)s, complementing the first."
 
760
  :enabled t
 
761
  :inline t
791
762
  (mbe :logic (if (zbp i) 1 (if (zbp j) 0 1))
792
763
       :exec (the (unsigned-byte 1)
793
764
               (logior (the (unsigned-byte 1)
794
765
                         (logxor 1 (the (unsigned-byte 1) i)))
795
766
                       (the (unsigned-byte 1) j)))))
796
767
 
797
 
(defun-inline b-orc2 (i j)
798
 
  ":doc-section logops-bit-functions
799
 
  B-ORC2 ~/~/~/"
800
 
  (declare (xargs :guard (and (bitp i) (bitp j))))
 
768
(define b-orc2 ((i bitp) (j bitp))
 
769
  :returns bit
 
770
  :short "Inclusive or of @(see bitp)s, complementing the second."
 
771
  :enabled t
 
772
  :inline t
801
773
  (mbe :logic (if (zbp i) (if (zbp j) 1 0) 1)
802
774
       :exec (the (unsigned-byte 1)
803
775
               (logior (the (unsigned-byte 1) i)
804
776
                       (the (unsigned-byte 1)
805
777
                         (logxor 1 (the (unsigned-byte 1) j)))))))
806
778
 
807
 
(defthm bit-functions-type
808
 
  (and (bitp (b-not i))
809
 
       (bitp (b-and i j))
810
 
       (bitp (b-ior i j))
811
 
       (bitp (b-xor i j))
812
 
       (bitp (b-eqv i j))
813
 
       (bitp (b-nand i j))
814
 
       (bitp (b-nor i j))
815
 
       (bitp (b-andc1 i j))
816
 
       (bitp (b-andc2 i j))
817
 
       (bitp (b-orc1 i j))
818
 
       (bitp (b-orc2 i j)))
819
 
  :rule-classes
820
 
  ((:rewrite)
821
 
   (:type-prescription :corollary (natp (b-not i)))
822
 
   (:type-prescription :corollary (natp (b-and i j)))
823
 
   (:type-prescription :corollary (natp (b-ior i j)))
824
 
   (:type-prescription :corollary (natp (b-xor i j)))
825
 
   (:type-prescription :corollary (natp (b-eqv i j)))
826
 
   (:type-prescription :corollary (natp (b-nand i j)))
827
 
   (:type-prescription :corollary (natp (b-nor i j)))
828
 
   (:type-prescription :corollary (natp (b-andc1 i j)))
829
 
   (:type-prescription :corollary (natp (b-andc2 i j)))
830
 
   (:type-prescription :corollary (natp (b-orc1 i j)))
831
 
   (:type-prescription :corollary (natp (b-orc2 i j))))
832
 
  :doc ":doc-section logops-bit-functions
833
 
  Rewrite: All of the bit functions return BITP integers
834
 
  ~/
835
 
  We also prove an appropriate :TYPE-PRESCRIPTION for each.~/~/")
 
779
(defsection bit-functions-type
 
780
  :short "Basic type rules for the @(see logops-bit-functions)."
 
781
 
 
782
  (defthm bit-functions-type
 
783
    (and (bitp (b-not i))
 
784
         (bitp (b-and i j))
 
785
         (bitp (b-ior i j))
 
786
         (bitp (b-xor i j))
 
787
         (bitp (b-eqv i j))
 
788
         (bitp (b-nand i j))
 
789
         (bitp (b-nor i j))
 
790
         (bitp (b-andc1 i j))
 
791
         (bitp (b-andc2 i j))
 
792
         (bitp (b-orc1 i j))
 
793
         (bitp (b-orc2 i j)))
 
794
    :rule-classes
 
795
    ((:rewrite)
 
796
     (:type-prescription :corollary (natp (b-not i)))
 
797
     (:type-prescription :corollary (natp (b-and i j)))
 
798
     (:type-prescription :corollary (natp (b-ior i j)))
 
799
     (:type-prescription :corollary (natp (b-xor i j)))
 
800
     (:type-prescription :corollary (natp (b-eqv i j)))
 
801
     (:type-prescription :corollary (natp (b-nand i j)))
 
802
     (:type-prescription :corollary (natp (b-nor i j)))
 
803
     (:type-prescription :corollary (natp (b-andc1 i j)))
 
804
     (:type-prescription :corollary (natp (b-andc2 i j)))
 
805
     (:type-prescription :corollary (natp (b-orc1 i j)))
 
806
     (:type-prescription :corollary (natp (b-orc2 i j))))))
836
807
 
837
808