logops-definitions

(in-package "ACL2")

(deflabel begin-logops-definitions)

(defsection bitp-basics
  :parents (bitp)
  (defthm bitp-mod-2
    (implies (integerp i) (bitp (mod i 2)))
    :rule-classes ((:rewrite) (:generalize :corollary (implies (integerp i)
          (or (equal (mod i 2) 0) (equal (mod i 2) 1)))))
    :hints (("Goal" :in-theory (enable linearize-mod)))))

(defsection unsigned-byte-p-basics
  :parents (unsigned-byte-p)
  (defthm unsigned-byte-p-forward
    (implies (unsigned-byte-p bits i)
      (and (integerp i) (>= i 0) (< i (expt 2 bits))))
    :rule-classes :forward-chaining)
  (defthmd unsigned-byte-p-unsigned-byte-p
    (implies (and (unsigned-byte-p size i)
        (integerp size1)
        (>= size1 size))
      (unsigned-byte-p size1 i))
    :hints (("Goal" :in-theory (disable expt-is-weakly-increasing-for-base>1)
       :use ((:instance expt-is-weakly-increasing-for-base>1
          (r 2)
          (i size)
          (j size1)))))))

(defxdoc unsigned-byte-p-discussion
  :parents (unsigned-byte-p)
  :short "Discussion on how to use unsigned-byte-p"
  :long "<p>@(csee unsigned-byte-p) (and @(see signed-byte-p) for that matter) are
  tricky enough that there is no one-size-fits-all solution that everyone
  should use to reason about them.  Depending on your problem you might try any
  of these strategies:</p>

  <ol>

  <li><i>Arithmetic</i> -- Leave unsigned-byte-p's regular definition enabled
  and try to reason about the resulting inequalities.  This sometimes works and
  may be a good approach if you have goals involving "non bit-vector
  functions" like +, *, /, etc.  I usually don't use this approach but I
  haven't done a lot of proofs about true arithmetic functions.</li>

  <li><i>Induction</i> -- Disable unsigned-byte-p's regular definition but
  instead enable an alternate definition, e.g., the
  centaur/bitops/ihsext-basics book has unsigned-byte-p**, which is a recursive
  version that works well for induction.  This definition is in the
  ihsext-recursive-redefs ruleset and also works well with other ** definitions
  like logand**.  This is often a good strategy when proving lemmas about
  unsigned-byte-p but is probably mainly useful when reasoning about new
  recursive functions.</li>

  <li><i>Vector</i> -- Leave @(see unsigned-byte-p) disabled except to prove
  lemmas, and expect to reason about (unsigned-byte-p n x) via lemmas.  I think
  I usually prefer this strategy as it feels more reliable/less magical than
  reasoning about arithmetic inequalities.  Some useful books:

    <ol>

      <li>bitops/ihsext-basics proves the nice/obvious lemmas about
      signed/unsigned-byte-p on many bit-vector functions like logior,
      logand, etc.</li>

      <li>bitops/signed-byte-p has lemmas about signed/unsigned-byte-p for
      some arithmetic functions (+, -, *) and also extended lemmas about
      bit-vector stuff.  It's often very handy for the kinds of guard
      obligations that arise from things like (the (unsigned-byte 32)
      x).</li>

    </ol></li>
  </ol>

  <p>We have occasionally written wrapper functions like @('u32p'), but, I
  think that perhaps the only reason we did this was for macros like @(see
  def-typed-record), where we needed a unary predicate to introduce a fancier
  data structure.  Once we had the typed records in place, we just enabled
  these wrappers and did all our reasoning about @(see unsigned-byte-p).
  (I don't think you'd want to reason about a each various u32p, u64p, etc.,
  individually.)</p>

  <p>In the context of FTY, I don't think you need wrappers, but if for some
  reason you do want to use them then that is probably basically fine.  Note
  here that you have some choice for your fixing function.  You can fix to 0 as
  you've done in your examples, but you might instead prefer to fix to
  @('(loghead n x)').  Why?  When you use loghead, it preserves the lower @('N')
  bits, and this may interact much more nicely with rules about true bit-vector
  functions.  This approach is also good for GL, where loghead is supported in
  an especially good way.</p>

  <p>That said, it should be possible to get by without wrappers; see for
  instance the definition of sizednum in centaur/fty/deftypes-tests.lisp, or
  the definition of vl-constint in centaur/vl/expr.lisp, both of which use a
  loghead-based approach to do the fixing.  (The vl-constint example has
  a :require that is an inequality instead of an unsigned-byte-p term, but I
  don't think there's any particular reason to do it this way instead of the
  other.)</p>

  <p>In general there is good reason to expect it to sometimes be hard to work
  with unsigned-byte-p.  For instance, consider a theorem like the following,
  from @('centaur/bitops/signed-byte-p.lisp'):</p>

  @({
   (defthm lousy-unsigned-byte-p-of-*-mixed
     ;; Probably won't ever unify with anything.
     (implies (and (unsigned-byte-p n1 a)
                   (unsigned-byte-p n2 b))
              (unsigned-byte-p (+ n1 n2) (* a b)))
     :hints(("Goal" :use ((:instance upper-bound)))))
  })

  <p>This would be a good rule to try on goals like @('(unsigned-byte-p 10 (* a
  b))'), but without some insight into @('a') and @('b') it's hard to know how
  to successfully instantiate @('N1/N2').  So you end up resorting to @(':use')
  hints, or special-case variants of this theorem (e.g., another theorem that
  says 7 bits * 3 bits --&gt; 10 bits), or you do something more sophisticated
  with bind-free or similar.</p>

  <p>If you find yourself going down this road, you might see in particular Dave
  Greve's "Parameterized Congruences" paper from the 2006 workshop, which is
  implemented in the coi/nary/nary.lisp book.  You could also look at Sol
  Swords' book to do something similar, see @(see contextual-rewriting).</p>")

(defsection signed-byte-p-basics
  :parents (signed-byte-p)
  (defthm signed-byte-p-forward
    (implies (signed-byte-p bits i)
      (and (integerp i)
        (>= i (- (expt 2 (- bits 1))))
        (< i (expt 2 (- bits 1)))))
    :rule-classes :forward-chaining))

(defsection logbit-guard
  :parents (logops-definitions)
  :short "@(call logbit-guard) is a macro form of the guards for @(see logbit)."
  (defmacro logbit-guard
    (pos i)
    `(and (force (integerp ,POS))
      (force (>= ,POS 0))
      (force (integerp ,I)))))

(defsection logmask-guard
  :parents (logops-definitions)
  :short "@(call logmask-guard) is a macro form of the guards for @(see logmask)."
  (defmacro logmask-guard
    (size)
    `(and (force (integerp ,SIZE)) (force (>= ,SIZE 0)))))

(defsection loghead-guard
  :parents (logops-definitions)
  :short "@(call loghead-guard) is a macro form of the guards for @(see loghead)."
  (defmacro loghead-guard
    (size i)
    `(and (force (integerp ,SIZE))
      (force (>= ,SIZE 0))
      (force (integerp ,I)))))

(defsection logtail-guard
  :parents (logops-definitions)
  :short "@(call logtail-guard) is a macro form of the guards for @(see logtail)."
  (defmacro logtail-guard
    (pos i)
    `(and (force (integerp ,POS))
      (force (>= ,POS 0))
      (force (integerp ,I)))))

(defsection logapp-guard
  :parents (logops-definitions)
  :short "@(call logapp-guard) is a macro form of the guards for @(see logapp)."
  (defmacro logapp-guard
    (size i j)
    `(and (force (integerp ,SIZE))
      (force (>= ,SIZE 0))
      (force (integerp ,I))
      (force (integerp ,J)))))

(defsection logrpl-guard
  :parents (logops-definitions)
  :short "@(call logrpl-guard) is a macro form of the guards for @(see logrpl)."
  (defmacro logrpl-guard
    (size i j)
    `(and (force (integerp ,SIZE))
      (force (>= ,SIZE 0))
      (force (integerp ,I))
      (force (integerp ,J)))))

(defsection logext-guard
  :parents (logops-definitions)
  :short "@(call logext-guard) is a macro form of the guards for @(see logext)."
  (defmacro logext-guard
    (size i)
    `(and (force (integerp ,SIZE))
      (force (> ,SIZE 0))
      (force (integerp ,I)))))

(defsection logrev-guard
  :parents (logops-definitions)
  :short "@(call logrev-guard) is a macro form of the guards for @(see logrev)."
  (defmacro logrev-guard
    (size i)
    `(and (force (integerp ,SIZE))
      (force (>= ,SIZE 0))
      (force (integerp ,I)))))

(defsection logextu-guard
  :parents (logops-definitions)
  :short "@(call logextu-guard) is a macro form of the guards for @(see logextu)."
  (defmacro logextu-guard
    (final-size ext-size i)
    `(and (force (integerp ,FINAL-SIZE))
      (force (>= ,FINAL-SIZE 0))
      (force (integerp ,EXT-SIZE))
      (force (> ,EXT-SIZE 0))
      (force (integerp ,I)))))

(defsection lognotu-guard
  :parents (logops-definitions)
  :short "@(call lognotu-guard) is a macro form of the guards for @(see lognotu)."
  (defmacro lognotu-guard
    (size i)
    `(and (force (integerp ,SIZE))
      (force (>= ,SIZE 0))
      (force (integerp ,I)))))

(defsection ashu-guard
  :parents (logops-definitions)
  :short "@(call ashu-guard) is a macro form of the guards for @(see ashu)."
  (defmacro ashu-guard
    (size i cnt)
    `(and (force (integerp ,SIZE))
      (force (> ,SIZE 0))
      (force (integerp ,I))
      (force (integerp ,CNT)))))

(defsection lshu-guard
  :parents (logops-definitions)
  :short "@(call lshu-guard) is a macro form of the guards for @(see lshu)."
  (defmacro lshu-guard
    (size i cnt)
    `(and (force (integerp ,SIZE))
      (force (>= ,SIZE 0))
      (force (integerp ,I))
      (force (integerp ,CNT)))))

(defsection logcdr-basics
  :parents (logcdr)
  (defthm logcdr-<-0
    (equal (< (logcdr i) 0) (and (integerp i) (< i 0))))
  (defthm justify-logcdr-induction
    (and (implies (> i 0) (< (logcdr i) i))
      (implies (< i -1) (< i (logcdr i))))
    :hints (("Goal" :in-theory (enable logcdr)))))

(defsection logcons-basics
  :parents (logcons)
  (defthm logcons-<-0
    (equal (< (logcons b i) 0) (and (integerp i) (< i 0)))
    :hints (("Goal" :in-theory (enable bfix)))))

(defsection loghead-basics
  :parents (loghead)
  (defthm unsigned-byte-p-loghead
    (implies (and (>= size1 size)
        (integerp size)
        (>= size 0)
        (integerp size1))
      (unsigned-byte-p size1 (loghead size i)))
    :hints (("Goal" :in-theory (e/d (unsigned-byte-p)
         (expt-is-weakly-increasing-for-base>1))
       :use ((:instance expt-is-weakly-increasing-for-base>1
          (r 2)
          (i size)
          (j size1))))))
  (defthm loghead-upper-bound
    (< (loghead size i) (expt 2 size))
    :rule-classes (:linear :rewrite)))

(defsection logapp-basics
  :parents (logapp)
  (defthm logapp-<-0
    (implies (logapp-guard size i j)
      (equal (< (logapp size i j) 0) (< j 0)))
    :hints (("Goal" :in-theory (e/d (loghead) (x-<-y*z))
       :use ((:instance x-<-y*z
          (x (mod i (expt 2 size)))
          (y (expt 2 size))
          (z (abs j))))))))

(defsection logext-basics
  :parents (logext)
  (defthm logext-bounds
    (implies (< 0 size)
      (and (>= (logext size i) (- (expt 2 (1- size))))
        (< (logext size i) (expt 2 (1- size)))))
    :rule-classes ((:linear :trigger-terms ((logext size i))) (:rewrite))
    :hints (("Goal" :in-theory (e/d (logapp loghead)
         (expt-is-increasing-for-base>1 exponents-add))
       :use ((:instance expt-is-increasing-for-base>1
          (r 2)
          (i (1- size))
          (j size))))))
  (defthm signed-byte-p-logext
    (implies (and (>= size1 size)
        (> size 0)
        (integerp size1)
        (integerp size))
      (signed-byte-p size1 (logext size i)))
    :hints (("Goal" :in-theory (e/d (signed-byte-p logapp loghead)
         (expt-is-weakly-increasing-for-base>1 exponents-add))
       :do-not '(eliminate-destructors)
       :use ((:instance expt-is-weakly-increasing-for-base>1
          (r 2)
          (i (1- size))
          (j (1- size1))))))))

(defsection logrev-basics
  :parents (logrev)
  (local (defun crock-induction
      (size size1 i j)
      (cond ((zp size) (+ size1 i j))
        (t (crock-induction (1- size)
            (1+ size1)
            (logcdr i)
            (logcons (logcar i) j))))))
  (local (defthm unsigned-byte-p-logrev1
      (implies (and (unsigned-byte-p size1 j) (integerp size) (>= size 0))
        (unsigned-byte-p (+ size size1) (logrev1 size i j)))
      :rule-classes nil
      :hints (("Goal" :in-theory (e/d (expt logcar logcons unsigned-byte-p) (exponents-add))
         :induct (crock-induction size size1 i j)))))
  (defthm unsigned-byte-p-logrev
    (implies (and (>= size1 size)
        (>= size 0)
        (integerp size)
        (integerp size1))
      (unsigned-byte-p size1 (logrev size i)))
    :hints (("Goal" :use ((:instance unsigned-byte-p-logrev1
          (size size)
          (size1 0)
          (i i)
          (j 0)) (:instance unsigned-byte-p-unsigned-byte-p
           (size size)
           (size1 size1)
           (i (logrev size i))))))))

(defsection logsat-basics
  :parents (logsat)
  (local (in-theory (enable exponents-add-unrestricted)))
  (defthm logsat-bounds
    (implies (< 0 size)
      (and (>= (logsat size i) (- (expt 2 size)))
        (< (logsat size i) (expt 2 size))))
    :rule-classes ((:linear :trigger-terms ((logsat size i))) (:rewrite)))
  (local (in-theory (disable exponents-add-unrestricted)))
  (defthm signed-byte-p-logsat
    (implies (and (>= size1 size)
        (> size 0)
        (integerp size1)
        (integerp size))
      (signed-byte-p size1 (logsat size i)))
    :hints (("Goal" :in-theory (e/d (signed-byte-p)
         (expt-is-weakly-increasing-for-base>1 exponents-add))
       :do-not '(eliminate-destructors)
       :use ((:instance expt-is-weakly-increasing-for-base>1
          (r 2)
          (i (1- size))
          (j (1- size1))))))))

(defsection logextu-basics
  :parents (logextu)
  (defthm unsigned-byte-p-logextu
    (implies (and (>= size1 final-size)
        (>= final-size 0)
        (integerp final-size)
        (integerp size1))
      (unsigned-byte-p size1 (logextu final-size ext-size i)))))

(defsection lognotu-basics
  :parents (lognotu)
  (defthm unsigned-byte-p-lognotu
    (implies (and (>= size1 size)
        (>= size 0)
        (integerp size)
        (integerp size1))
      (unsigned-byte-p size1 (lognotu size i)))))

(defsection ashu-basics
  :parents (ashu)
  (defthm unsigned-byte-p-ashu
    (implies (and (>= size1 size)
        (>= size 0)
        (integerp size)
        (integerp size1))
      (unsigned-byte-p size1 (ashu size i cnt)))))

(defsection lshu-basics
  :parents (lshu)
  (defthm unsigned-byte-p-lshu
    (implies (and (>= size1 size)
        (>= size 0)
        (integerp size)
        (integerp size1))
      (unsigned-byte-p size1 (lshu size i cnt)))))

(defxdoc logops-byte-functions
  :parents (logops-definitions)
  :short "A portable implementation and extension of Common Lisp byte
  functions."
  :long "<p>The proposed Common Lisp standard [<a
href='http://en.wikipedia.org/wiki/X3J13'>X3J13</a> Draft 14.10] defines a
number of functions that operate on subfields of integers.  These subfields are
specified by @('(BYTE size position)'), which "indicates a byte of width size
and whose bits have weights @($2^{position+size-1}$) through @($2^{pos}$), and
whose representation is implementation dependent".  Unfortunately, the
standard does not specify what BYTE returns, only that whatever is returned is
understood by the byte manipulation functions LDB, DPB, etc.</p>

<p>This lack of complete specification makes it impossible for ACL2 to specify
the byte manipulation functions of Common Lisp in a portable way.  For example
AKCL uses @('(cons size position)') as a byte specifier, whereas another
implementation might use a special data structure to represent @('(byte size
position)').  Since any theorem about the ACL2 built-ins is meant to be a
theorem for all Common Lisp implementations, ACL2 cannot define BYTE.</p>

<p>Therefore, we have provided a portable implementation of the byte operations
specified by the draft standard.  This behavior of this implementation should
be consistent with every Common Lisp that provides the standard byte
operations.  Our byte specifier @('(bsp size pos)') is analogous to CLTL's
@('(byte size pos)'), where size and pos are nonnegative integers.  Note that
the standard indicates that reading a byte of size 0 returns 0, and writing a
byte of size 0 leaves the destination unchanged.</p>

<p>This table indicates the correspondance between the Common Lisp byte
operations and our portable implementation:</p>

@({
  Common Lisp                               This Implementation
  ------ ----                               ---- --------------

  (BYTE size position)                      (BSP size position)
  (BYTE-SIZE bytespec)                      (BSP-SIZE bsp)
  (BYTE-POSITION bytespec)                  (BSP-POSITION bsp)
  (LDB bytespec integer)                    (RDB bsp integer)
  (DPB newbyte bytespec integer)            (WRB newbyte bsp integer)
  (LDB-TEST bytespec integer)               (RDB-TEST bsp integer)
  (MASK-FIELD bytespec integer)             (RDB-FIELD bsp integer)
  (DEPOSIT-FIELD newbyte bytespec integer)  (WRB-FIELD newbyte bsp integer)
})

<p>For more information, see the documentation for the functions listed above.
If you are concerned about the efficiency of this implementation, see the file
@('ihs/logops-efficiency-hack.lsp') for some notes.</p>")

(defsection bsp
  :parents (logops-byte-functions)
  :short "@(call bsp) returns a byte-specifier."
  :long "<p>This specifier designates a byte whose width is size and whose bits have
weights 2^(pos) through 2^(pos+size-1). Both size and pos must be
nonnegative integers.</p>

<p>BSP is mnemonic for Byte SPecifier or Byte Size and Position, and is
analogous to Common Lisp's @('(byte size position)').</p>

<p>BSP is implemented as a macro for simplicity and convenience.  One should
always use BSP in preference to CONS, however, to ensure compatibility with
future releases.</p>

@(def bsp)"
  (defmacro bsp (size pos) `(cons ,SIZE ,POS)))

(define bspp
  (bsp)
  :parents (logops-byte-functions)
  :short "@(call bspp) recognizes objects produced by @(see bsp)."
  :returns bool
  :enabled t
  (and (consp bsp)
    (integerp (car bsp))
    (>= (car bsp) 0)
    (integerp (cdr bsp))
    (>= (cdr bsp) 0))
  ///
  (defthm bspp-bsp
    (implies (and (integerp size) (>= size 0) (integerp pos) (>= pos 0))
      (bspp (bsp size pos)))
    :hints (("Goal" :in-theory (enable bspp)))))

(define bsp-size
  ((bsp bspp))
  :returns (size (and (integerp size) (>= size 0))
    :rule-classes :type-prescription :hyp (bspp bsp)
    :name bsp-size-type)
  :parents (logops-byte-functions)
  :short "@('(bsp-size (bsp size pos)) = size')"
  :long "<p>This is analogous to Common Lisp's @('(byte-size bytespec)').</p>"
  :enabled t
  (car bsp))

(define bsp-position
  ((bsp bspp))
  :returns (pos (and (integerp pos) (>= pos 0))
    :rule-classes :type-prescription :hyp (bspp bsp)
    :name bsp-position-type)
  :parents (logops-byte-functions)
  :short "@('(bsp-position (bsp size pos)) = pos')"
  :long "<p>This is analogous to Common Lisp's @('(byte-position bytespec)').</p>"
  :enabled t
  (cdr bsp))

(define rdb
  ((bsp bspp) (i integerp))
  :returns (nat (and (integerp nat) (>= nat 0))
    :rule-classes :type-prescription :name rdb-type)
  :parents (logops-byte-functions)
  :short "@(call rdb) returns the byte of @('i') specified by @('bsp')."
  :long "<p>This is analogous to Common Lisp's @('(ldb bytespec integer)').</p>"
  :enabled t
  (loghead (bsp-size bsp) (logtail (bsp-position bsp) i))
  ///
  (defthm unsigned-byte-p-rdb
    (implies (and (>= size (bsp-size bsp))
        (force (>= size 0))
        (force (integerp size))
        (force (bspp bsp)))
      (unsigned-byte-p size (rdb bsp i))))
  (defthm rdb-upper-bound
    (implies (force (bspp bsp))
      (< (rdb bsp i) (expt 2 (bsp-size bsp))))
    :rule-classes (:linear :rewrite))
  (defthm bitp-rdb-bsp-1
    (implies (equal (bsp-size bsp) 1) (bitp (rdb bsp i)))
    :hints (("Goal" :in-theory (enable bitp loghead)))))

(define wrb
  ((i integerp) (bsp bspp) (j integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name wrb-type)
  :parents (logops-byte-functions)
  :short "@(call wrb) writes the @('(bsp-size bsp)') low-order bits of @('i')
into the byte of @('j') specified by @('bsp')."
  :long "<p>This is analogous to Common Lisp's @('(dpb newbyte bytespec
integer)').</p>"
  :enabled t
  (logapp (bsp-position bsp)
    (loghead (bsp-position bsp) j)
    (logapp (bsp-size bsp)
      i
      (logtail (+ (bsp-size bsp) (bsp-position bsp)) j))))

(define rdb-test
  ((bsp bspp) (i integerp))
  :returns bool
  :parents (logops-byte-functions)
  :short "@(call rdb-test) is true iff the field of @('i') specified by
  @('bsp') is nonzero."
  :long "<p>This is analogous to Common Lisp's @('(ldb-test bytespec
  integer)').</p>"
  :enabled t
  (not (eql (rdb bsp i) 0)))

(define rdb-field
  ((bsp bspp) (i integerp))
  :returns nat
  :parents (logops-byte-functions)
  :short "@(call rdb-field) is analogous to Common Lisp's @('(mask-field bytespec integer)')."
  :enabled t
  (logand i (wrb -1 bsp 0)))

(define wrb-field
  ((i integerp) (bsp bspp) (j integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name wrb-field-type)
  :parents (logops-byte-functions)
  :short "@(call wrb-field) is analogous to Common Lisp's @('(deposit-field
  newbyte bytespec integer)')."
  :enabled t
  (wrb (rdb bsp i) bsp j))

(defsection rdb-guard
  :parents (logops-byte-functions)
  :short "@(call rdb-guard) is a macro form of the guards for @(see rdb), @(see
  rdb-test), and @(see rdb-field)."
  :long "@(def rdb-guard)"
  (defmacro rdb-guard
    (bsp i)
    `(and (force (bspp ,BSP)) (force (integerp ,I)))))

(defsection wrb-guard
  :parents (logops-byte-functions)
  :short "@(call wrb-guard) is a macro form of the guards for @(see wrb) and @(see wrb-field)."
  :long "@(def wrb-guard)"
  (defmacro wrb-guard
    (i bsp j)
    `(and (force (integerp ,I))
      (force (bspp ,BSP))
      (force (integerp ,J)))))

(defval *logops-functions*
  :parents (logops-definitions)
  :short "A list of all functions considered to be part of the theory of logical
          operations on numbers."
  '(binary-logior binary-logxor
    binary-logand
    binary-logeqv
    lognand
    lognor
    logandc1
    logandc2
    logorc1
    logorc2
    lognot
    logtest
    logbitp
    ash
    logcount
    integer-length
    bitp
    signed-byte-p
    unsigned-byte-p
    logcar$inline
    logcdr$inline
    logcons$inline
    logbit$inline
    logmask$inline
    logmaskp
    loghead$inline
    logtail$inline
    logapp
    logrpl
    logext
    logrev1
    logrev$inline
    logsat
    lognotu$inline
    logextu$inline
    ashu
    lshu
    bspp
    bsp-size
    bsp-position
    rdb
    wrb
    rdb-test
    rdb-field
    wrb-field
    b-not$inline
    b-and$inline
    b-ior$inline
    b-xor$inline
    b-eqv$inline
    b-nand$inline
    b-nor$inline
    b-andc1$inline
    b-andc2$inline
    b-orc1$inline
    b-orc2$inline))

(defsection logops-functions
  :parents (logops-definitions)
  :short "A theory consisting of all function names of functions considered to
          be logical operations on numbers."
  :long "<p>If you are using the book @('logops-lemmas'), you will need to
  DISABLE this theory in order to use the lemmas contained therein, as most of
  the logical operations on numbers are non-recursive.</p>"
  (deftheory logops-functions *logops-functions*))

(defsection logops-definitions-theory
  :parents (logops-definitions)
  :short "The "minimal" theory for the book "logops-definitions"."
  :long "<p>This theory contains the DEFUN-TYPE/EXEC-THEORY (which see) of all
functions considered to be logical operations on numbers, and all
lemmas (predominately `type lemmas') proved in this book.  All functions in the
list *LOGOPS-FUNCTIONS* are DISABLEd.</p>"
  (deftheory logops-definitions-theory
    (union-theories (set-difference-theories (set-difference-theories (universal-theory :here)
          (universal-theory 'begin-logops-definitions))
        *logops-functions*)
      (defun-type/exec-theory *logops-functions*))))

(defsection defbytetype
  :parents (logops-definitions)
  :short "A macro for defining integer subrange types."
  :long "<p>The "byte types" defined by DEFBYTETYPE correspond to the Common
Lisp concept of a "byte", that is, an integer with a fixed number of bits.
We extend the Common Lisp concept to allow signed bytes.</p>

<p>Example:</p>

@({
    (DEFBYTETYPE WORD 32 :SIGNED)
})

<p>Defines a new integer type of 32-bit signed integers, recognized by
@('(WORD-P i)').</p>

<p>General Form:</p>

@({
   (DEFBYTETYPE name size s/u &key saturating-coercion)
})

<p>The argument name should be a symbol, size should be a constant
expression (suitable for DEFCONST) for a positive integer, s/u is
either :SIGNED or :UNSIGNED, saturating-coercion should be a symbol (default
NIL).</p>

<p>Each data type defined by DEFBYTETYPE produces a number of events:</p>

<ul>

<li>A constant @('*<name>-MAX*'), set to the maximum value of the type.</li>

<li>A constant @('*<name>-MIN*'), set to the minimum value of the type.</li>

<li>A predicate, @('(<pred> x)'), that recognizes either @('(UNSIGNED-BYTE-P
size x)') or @('(SIGNED-BYTE-P size x)'), depending on whether s/u
was :UNSIGNED or :SIGNED respectively. This predicate is DISABLED.  The name of
the predicate will be @('<name>-p').</li>

<li>A coercion function, @('(<name> i)'), that coerces any object @('i') to the
correct type by LOGHEAD and LOGEXT for unsigned and signed integers
respectively.  This function is DISABLED.</li>

<li>A lemma showing that the coercion function actually does the correct
coercion.</li>

<li>A lemma that reduces calls of the coercion function when its argument
satisfies the predicate.</li>

<li>A forward chaining lemma from the predicate to the appropriate type
information.</li>

<li>If :SATURATING-COERCION is specified, the value of this keyword argument
should be a symbol.  A function of this name will be defined to provide a
saturating coercion.  `Saturation' in this context means that values outside of
the legal range for the type are coerced to the type by setting them to the
nearest legal value, which will be either the minimum or maximum value of the
type. This function will be DISABLEd, and a lemma will be generated that proves
that this function returns the correct type.  Note that
the :SATURATING-COERCION option is only valid for :SIGNED types.</li>

<li>A theory named @('<name>')-THEORY that includes the lemmas and the
DEFUN-TYPE/EXEC-THEORY of the functions.</li>

</ul>")

(defloop defword-keyword-field-alist
  (name set-conc-name field-names)
  (for ((field-name in field-names))
    (collect (cons (intern-in-package-of-symbol (string field-name) :keyword)
        (defword-updater-name name set-conc-name field-name)))))

(defsection defword
  :parents (logops-definitions)
  :short "A macro to define packed integer data structures."
  :long "<p>Example:</p>

@({
    (DEFWORD FM9001-INSTRUCTION-WORD
      ((RN-A 4 0) (MODE-A 2 4) (IMMEDIATE 9 0) (A-IMMEDIATE 1 9)
       (RN-B 4 10) (MODE-B 2 14)
       (SET-FLAGS 4 16) (STORE-CC 4 20) (OP-CODE 4 24))
      :CONC-NAME ||
      :SET-CONC-NAME SET-)
})

<p>The above example defines the instruction word layout for the FM9001.  The
macro defines accessing macros (RN-A i), ... ,(OP-CODE i), updating
macros (SET-RN-A val i), ... ,(SET-OP-CODE val i), and a keyword updating
macro @('(UPDATE-FM9001-INSTRUCTION-WORD val &rest args)').</p>

<p>General form:</p>

@({
    (DEFWORD name struct &key conc-name set-conc-name keyword-updater)
})

<p>The DEFWORD macro defines a packed integer data structure, for example an
instruction word for a programmable processor or a status word.  DEFWORD is a
simple macro that defines accessing and updating macros for the fields of the
data structure. The utility of DEFWORD is mainly to simplify the specification
of packed integer data structures, and to improve the readability of code
manipulating these data structures without affecting performance. As long as
the book "logops-lemmas" is loaded all of the important facts about the macro
expansions should be available to the theorem prover.</p>

<p>Arguments</p>

@({
  name:  The name of the data structure, a symbol.

  struct : The field structure of the word. The form of this argument is
  given by the following grammar:

  <tuple>  := (<field> <size> <pos> [ <doc> ])
  <struct> := () | (<tuple> . <struct>)

  where:

  (SYMBOLP <field>)
  (AND (INTEGERP <size>) (> <size> 0))
  (AND (INTEGERP <pos>) (>= <pos> 0))
  (STRINGP <doc>)
})

<p>In other words, a list of tuples, the first element being a symbol, the
second a positive integer, the third a nonnegative integer, and the optional
fourth a string.</p>

<p>Note that there are few other requirements on the @('<struct>') other than
the syntactic ones above.  For example, the FM9001 DEFWORD shows that a word
may have more than one possible structure - the first 9 bits of the FM9001
instruction word are either an immediate value, or they include the RN-A and
MODE-A fields.</p>

<p>conc-name, set-conc-name: These are symbols whose print names will be
concatenated with the field names to produce the name of the accessors and
updaters respectively.  The default is @('<name>')- and @('SET-<name>')-
respectively.  The access and update macro names will be interned in the
package of name.</p>

<p>keyword-updater:  This is a symbol, and specifies the name of the keyword
updating macro (see below).  The default is @('UPDATE-<name>').</p>


<h3>Interpretation</h3>

<p>DEFWORD creates an ACL2 DEFLABEL event named @('<name>').</p>

<p>Each tuple @('(<field> <size> <pos>)') represents a @('<size>')-bit field of
a word at the bit position indicated.  Each field tuple produces an accessor
macro</p>

@({
  (<accessor> word)
})

<p>where @('<accessor>') is computed from the :conc-name (see above).  This
accessor will expand into:</p>

@({
  (RDB (BSP <size> <pos>) word).
})

<p>DEFWORD also generates an updating macro</p>

@({
  (<updater> val word)
})

<p>where @('<updater>') is computed from the :set-conc-name (see above).  This
macro will expand to</p>

@({
     (WRB val (BSP <size> <pos>) word)
})

<p>The keyword updater</p>

@({
  (<keyword-updater> word &rest args)
})

<p>is equivalent to multiple nested calls of the updaters on the initial word.
 For example,</p>

@({
  (UPDATE-FM9001-INSTRUCTION-WORD WORD :RN-A 10 :RN-B 12)
})

<p>is the same as @('(SET-RN-A 10 (SET-RN-B 12 WORD))').</p>")

(defxdoc word/bit-macros
  :parents (logops-definitions)
  :short "Macros for manipulating integer words defined as contiguous bits."
  :long "<p>These macros were defined to support the functions produced by
  translating SPW .eqn files to ACL2 functions.</p>")

(defsection bind-word-to-bits
  :parents (word/bit-macros)
  :short "Bind variables to the contiguous low-order bits of word."
  :long "<p>Example:</p>

@({
  (BIND-WORD-TO-BITS (A B C) I (B-AND A (B-IOR B C)))
})

<p>The above macro call will bind A, B, and C to the 0th, 1st, and 2nd bit of
I, and then evaluate the logical expression under those bindings.  The list of
bit names is always interpreted from low to high order.</p>"
  (defmacro bind-word-to-bits
    (bit-names word &rest forms)
    (declare (xargs :guard (and (symbol-listp bit-names) (no-duplicatesp bit-names))))
    `(let ,(BIND-WORD-TO-BITS-FN BIT-NAMES 0 WORD)
      ,@FORMS)))

(defsection make-word-from-bits
  :parents (word/bit-macros)
  :short "Update the low-order bits of word with the indicated values."
  :long "<p>Example:</p>

@({
    (MAKE-WORD-FROM-BITS A B C)
})

<p>The above macro call will build an unsigned integer from the bits A B, and
C.  The list of bits is always interpreted from low to high order. Note that
the expression generated by this macro will coerce the values to bits before
building the word.</p>"
  (defmacro make-word-from-bits
    (&rest bits)
    (cond ((endp bits) 0)
      (t `(logapp 1 ,(CAR BITS) (make-word-from-bits ,@(CDR BITS)))))))