basic-definitions

(in-package "ACL2")

(defxdoc logops
  :parents (ihs)
  :short "Definitions and lemmas about logical operations on integers."
  :long "<p>The books @(see logops-definitions) and @(see logops-lemmas)
contain a theory of the logical operations on numbers defined by CLTL (Section
12.7), and a portable implementation of the CLTL byte manipulation
functions (Section 12.8).  These books also extend the CLTL logical operations
and byte manipulation theory with a few new definitions, lemmas supporting
those definitions, and useful macros.</p>

<p>These books were developed as a basis for the formal specification and
verification of hardware, where integers are used to represent binary signals
and busses.  These books should be general enough, however, to be used as a
basis for reasoning about packed data structures, bit-encoded sets, and other
applications of logical operations on integers.</p>")

(defxdoc logops-definitions
  :parents (ihs)
  :short "A book a definitions of logical operations on numbers."
  :long "<p>This book, along with @(see logops-lemmas), includes a theory of
the Common Lisp logical operations on numbers, a portable implementation of the
Common Lisp byte operations, extensions to those theories, and some useful
macros.</p>

<p>This book contains only definitions, lemmas necessary to admit those
definitions, and selected type lemmas.  By "type lemmas" we mean any lemmas
about the logical operations that we have found necessary to verify the guards
of functions that use these operations.  We have separated these "type
lemmas" from the large body of other lemmas in @(see logops-lemmas) to allow a
user to use this book to define guard-verified functions without having to also
include the extensive theory in @('logops-lemmas').</p>

<p>The standard Common Lisp logical operations on numbers are defined on the
signed integers, and return signed integers as appropriate.  This allows a high
level, signed interpretation of hardware operations if that is appropriate for
the specification at hand.  We also provide unsigned versions of several of the
standard logical operations for use in specifications where fixed-length
unsigned integers are used to model hardware registers and busses.  This view
of hardware is used, for example, in Yuan Yu's Nqthm specification of the
Motorola MC68020.</p>")

(define zbp
  :parents (logops-definitions bitp)
  :short "Zero bit recognizer.  @('(zbp x)') tests for zero bits.  Any object
other than @('1') is considered to be a zero bit."
  ((x bitp))
  :returns bool
  :enabled t
  :inline t
  (mbe :logic (equal (bfix x) 0)
    :exec (/= (the (unsigned-byte 1) x) 1)))

(define ifloor
  :short "@('(ifloor i j)') is the same as @(see floor), except that it coerces
  its arguments to integers."
  ((i integerp) (j (and (integerp j) (not (= 0 j)))))
  :returns (int integerp
    :rule-classes :type-prescription :name ifloor-type)
  :inline t
  :enabled t
  (mbe :logic (floor (ifix i) (ifix j)) :exec (floor i j)))

(define imod
  :short "@('(imod i j)') is the same as @(see mod), except that it coerces its
  arguments to integers."
  ((i integerp) (j (and (integerp j) (not (= 0 j)))))
  :returns (int integerp
    :rule-classes :type-prescription :name imod-type)
  :inline t
  :enabled t
  (mbe :logic (mod (ifix i) (ifix j)) :exec (mod i j)))

(define expt2
  :short "@('(expt2 n)') is the same as @('(expt 2 n)'), except that it coerces
  its argument to a natural."
  ((n natp))
  :returns (nat natp :rule-classes :type-prescription :name expt2-type)
  :enabled t
  :inline t
  (mbe :logic (expt 2 (nfix n))
    :exec (the unsigned-byte (ash 1 (the unsigned-byte n)))))

(define binary-minus-for-gl
  ((x acl2-numberp) (y acl2-numberp))
  :parents (binary--)
  :short "Hack for implementing @(see binary--).  Don't use this."
  :long "<p>You should never need to use this, call @(see binary--) instead.</p>

<p>This is the logical definition for @(see binary--).  It has a custom GL
symbolic counterpart.  The only reason to make this a separate function,
instead of directly putting a symbolic counterpart on @('binary--') itself, is
to avoid infinite inlining problems when we define custom symbolic counterparts
for inlined functions on Lisps like SBCL.</p>"
  :enabled t
  (- x y))

(define binary--
  :parents (logops-definitions)
  :short "@('(binary-- x y)') is the same as @('(- x y)'), but may symbolically
simulate more efficiently in @(see gl)."
  ((x acl2-numberp) (y acl2-numberp))
  :enabled t
  :inline t
  :long "<p>This is an alias for @('(- x y)').  It should always be left
enabled and you should never prove any theorems about it.</p>

<p>In ACL2, @(see -) is a macro and @('(- x y)') expands to @('(+ x (unary--
y))').  This form is often not particularly good for symbolic simulation with
@(see gl): GL first has to negate @('y') and then carry out the addition.</p>

<p>In contrast, @('binary--') has a custom symbolic counterpart that avoids
this intermediate negation.  This may result in fewer BDD computations or AIG
nodes.  In the context of @(see hardware-verification), it may also help your
spec functions to better match the real implementation of subtraction circuits
in the hardware being analyzed.</p>"
  (mbe :logic (binary-minus-for-gl x y) :exec (- x y)))

(define logcar
  :short "Least significant bit of a number."
  ((i integerp))
  :returns (bit bitp
    :rule-classes ((:type-prescription) (:generalize :corollary (or (equal (logcar i) 0) (equal (logcar i) 1))))
    :name logcar-type)
  :long "<p>@('(logcar i)') is the @(see car) of an integer conceptualized as a
bit-vector, where the least significant bit is at the head of the list.</p>

<p>In languages like C, this might be written as @('i & 1').</p>"
  :enabled t
  :inline t
  (mbe :logic (imod i 2)
    :exec (the (unsigned-byte 1) (logand (the integer i) 1))))

(define logcdr
  :short "All but the least significant bit of a number."
  ((i integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name logcdr-type)
  :long "<p>@('(logcdr i)') is the @(see cdr) of an integer conceptualized as a
bit-vector, where the least significant bit is at the head of the list.</p>

<p>In languages like C, this might be written as @('i >> 1').</p>"
  :enabled t
  :inline t
  (mbe :logic (ifloor i 2)
    :exec (the integer (ash (the integer i) -1))))

(define logcons
  :short "@('(logcons b i)') is the @(see cons) operation for integers,
conceptualized as bit-vectors, where the least significant bit is at the head
of the list."
  ((b bitp "LSB of the result.") (i integerp "All but the LSB of the result."))
  :returns (int integerp
    :rule-classes :type-prescription :name logcons-type)
  :long "<p>In languages like C, this might be written as @('(i << 1) + b').</p>

<p>See also @(see logcar) and @(see logcdr).</p>"
  :inline t
  :enabled t
  (mbe :logic (let ((b (bfix b)) (i (ifix i)))
      (+ b (* 2 i)))
    :exec (the integer
      (+ (the (unsigned-byte 1) b) (the integer (ash i 1))))))

(define logbit
  :parents (logops-definitions logbitp)
  :short "@('(logbit pos i)') returns the bit of @('i') at bit-position @('pos')
as a @(see bitp), 0 or 1."
  ((pos natp) (i integerp))
  :returns (bit bitp
    :rule-classes :type-prescription :name logbit-type)
  :long "<p>This is just like the Common Lisp function @('(logbitp pos i)'),
except that we return 1 or 0 (instead of t or nil).</p>

<p>In languages like C, this might be written as @('(i >> pos) & 1').</p>"
  :enabled t
  :inline t
  :no-function t
  (if (logbitp pos i)
    1
    0)
  ///)

(define logmask
  :short "@('(logmask size)') creates a low-order, @('size')-bit mask."
  ((size natp))
  :returns (nat natp
    :rule-classes :type-prescription :name logmask-type)
  :long "<p>In languages like C, this might be written as @('(1 << size) - 1').</p>"
  :enabled t
  :inline t
  (mbe :logic (- (expt2 size) 1)
    :exec (the unsigned-byte (1- (the unsigned-byte (ash 1 size))))))

(define logmaskp
  :short "@('(logmaskp i)') recognizes positive bit-masks, i.e., numbers of the
form @($2^n - 1$)."
  (i)
  :returns bool
  :enabled t
  :long "<p>Note that this function explicitly checks @('(integerp i)'), which
means it doesn't satisfy an @(see int-equiv) congruence.  See also @(see
bitmaskp), which fixes its argument and may execute slightly faster.</p>"
  (mbe :logic (and (integerp i)
      (>= i 0)
      (equal i (- (expt2 (integer-length i)) 1)))
    :exec (and (integerp i)
      (eql i
        (the unsigned-byte
          (- (the unsigned-byte (ash 1 (integer-length i))) 1))))))

(define bitmaskp
  :short "@('(bitmaskp i)') recognizes positive masks, i.e., numbers of the form
@($2^n - 1$).  It is like @(see logmaskp) but properly treats non-integers as 0."
  ((i integerp))
  :returns bool
  :inline t
  (mbe :logic (logmaskp (mbe :logic (ifix i) :exec i))
    :exec (eql i
      (the unsigned-byte
        (- (the unsigned-byte (ash 1 (integer-length i))) 1)))))

(define loghead
  :short "@('(loghead size i)') returns the @('size') low-order bits of @('i')."
  ((size (and (integerp size) (<= 0 size)) :type unsigned-byte) (i integerp))
  :returns (nat natp
    :rule-classes :type-prescription :name loghead-type)
  :long "<p>In languages like C, this might be written as @('i & ((1 << size) -
1)').</p>

<p>By convention we define @('(loghead 0 i)') as 0.  This definition is a
bit arbitrary but generally leads to nice lemmas.</p>"
  :inline t
  :enabled t
  :split-types t
  :guard-hints (("Goal" :in-theory (enable mod-of-expt-2-is-logand)))
  (mbe :logic (imod i (expt2 size))
    :exec (the unsigned-byte
      (logand i
        (the unsigned-byte (1- (the unsigned-byte (ash 1 size))))))))

(define logtail
  :short "@('(logtail pos i)') returns the high-order part of @('i'), starting
  at bit position @('pos')."
  ((pos (and (integerp pos) (<= 0 pos)) :type unsigned-byte) (i integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name logtail-type)
  :long "<p>In languages like C, this might be written as @('i >> pos').</p>"
  :split-types t
  :inline t
  :enabled t
  (mbe :logic (ifloor i (expt2 pos))
    :exec (ash i (- (the unsigned-byte pos)))))

(define logapp
  :short "@('(logapp size i j)') is a binary append of i to j, where i
  effectively becomes the 'low' bits and j becomes the 'high' bits."
  ((size (and (integerp size) (<= 0 size)) :type unsigned-byte) (i integerp)
    (j integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name logapp-type)
  :split-types t
  :long "<p>@('logapp') is a specification for merging integers.  Note that
@('i') is truncated to @('size') bits before merging with @('j'), and that @('j')
is shifted to the left by @('size') bits before the merge.</p>"
  :enabled t
  (mbe :logic (let ((j (ifix j)))
      (+ (loghead size i) (* j (expt2 size))))
    :exec (+ (loghead size i) (ash j size))))

(defsection logappn
  :short "N-ary version of @(tsee logapp)."
  :long "<p>When passed an even number of arguments,</p>
   <code>
   (logappn size1 int1 ... sizeN intN)
   </code>
   <p>expands to a nest of @(tsee logapp)s ending with 0:</p>
   <code>
   (logapp size1 int1 ... (logapp sizeN intN 0)...)
   </code>
   <p>where the last @(tsee logapp) could be optimized
      as a @(tsee loghead) without 0,
      but the current form keeps the macro simple and uniform.</p>
   <p>When passed an odd number of arguments,</p>
   <code>
   (logappn size1 int1 ... sizeN intN last)
   </code>
   <p>expands to a nest of @(tsee logapp)s ending with @('last'):</p>
   <code>
   (logapp size1 int1 ... (logapp sizeN intN last)...)
   </code>
   <p>This macro supports the readable appending of bit chunks
      when passed an even number of arguments, e.g.</p>
   <code>
   (logappn 32 base
            8 padding
            24 offset)
   </code>
   <p>The ability to pass an odd number of arguments
      is in spirit with @(tsee logapp),
      whose @('j') argument does not have an associated size.</p>"
  (defun logappn-fn
    (args)
    (cond ((endp args) 0)
      ((endp (cdr args)) (car args))
      (t `(logapp ,(CAR ARGS) ,(CADR ARGS) ,(LOGAPPN-FN (CDDR ARGS))))))
  (defmacro logappn (&rest args) (logappn-fn args)))

(define logrpl
  :short "Logical replace.  @('(logrpl size i j)') replaces the @('size')
  low-order bits of @('j') with the @('size') low-order bits of @('i')."
  ((size (and (integerp size) (<= 0 size))) (i integerp)
    (j integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name logrpl-type)
  :long "<p>@('logrpl') is a specification for the result of storing short
values into long words, i.e., the short value simply replaces the head of the
long word.</p>

<p>This function is equivalent to @('(WRB i (BSP size 0) j)').</p>"
  :enabled t
  (logapp size i (logtail size j)))

(define logext
  :short "@('(logext size i)') sign-extends @('i') to a @('size')-bit signed
integer."
  ((size (and (integerp size) (< 0 size)) :type unsigned-byte) (i integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name logext-type)
  :split-types t
  :long "<p>@('logext') interprets the least significant @('size') bits of
@('i') as a signed, 2's complement integer.</p>

<p>Basic examples:</p>

@({
    (logext 4 7)  --> 7        Bottom four bits are 0111
                               Sign bit is 0
                               Sign extension creates {0000......0}111
                               2's complement interpretation: 7.

    (logext 3 7)  --> -1       Bottom 3 bits are 111
                               Sign bit is 1
                               Sign extension creates {1111.....1}111
                               2's complement interpretation: -1.

    (logext 4 8)  --> -8       Bottom 4 bits are 1000
                               Sign bit is 1
                               Sign extension creates {1111.....1}1000
                               2's complement interpretation: -8.
})

<p>This function returns a (possibly negative) integer.  For consistency with
@(see SIGNED-BYTE-P), @('size') must be strictly greater than 0.  In contrast,
the related function @(see logextu) carries out a sign-extension but only
returns the low @('size') bits, i.e., it always returns a natural number.</p>

<p>We specify @('logext') in terms of the @('size') of the result instead of as
a bit position because we normally specify integer subranges by the number of
significant (including sign) bits.</p>

<p>See also @(see bitops::bitops/fast-logext) for a logically identical
function that is optimized for better performance.</p>"
  :enabled t
  (let* ((size-1 (- size 1)))
    (declare (type unsigned-byte size-1))
    (logapp size-1
      i
      (if (logbitp size-1 i)
        -1
        0))))

(define logrev1
  :parents (logrev)
  :short "Helper function for @(see logrev)."
  ((size (and (integerp size) (<= 0 size))) (i integerp)
    (j integerp))
  :returns (nat)
  :split-types t
  (declare (type unsigned-byte size)
    (type integer i j))
  :enabled t
  (if (zp size)
    (mbe :logic (ifix j) :exec j)
    (logrev1 (the unsigned-byte (- size 1))
      (logcdr i)
      (logcons (logcar i) j))))

(define logrev
  :short "Logical reverse.  @('(logrev size i)') bit-reverses the @('size')
  low-order bits of @('i'), discarding the high-order bits."
  ((size (and (integerp size) (<= 0 size))) (i integerp))
  :returns (nat natp
    :rule-classes :type-prescription :name logrev-type)
  :long "<p>Normally we don't think of bit-reversing as a logical operation,
even though its hardware implementation is trivial: simply reverse the wires
leading from the source to the destination.</p>

<p>@('logrev') is included as a logical operation to support the specification
of DSPs, which may provide bit-reversing in their address generators to improve
the performance of the FFT.</p>

<p>@('logrev') entails a recursive definition of bit-reversing via the helper
function @(see logrev1).</p>

<p>See also @(see bitops::bitops/fast-logrev) for some optimized definitions of
@(see logrev).</p>"
  :inline t
  :enabled t
  (logrev1 size i 0))

(define logsat
  :short "Signed saturation.  @('(logsat size i)') coerces @('i') to a
  @('size')-bit signed integer by saturation."
  ((size (and (integerp size) (< 0 size)) :type unsigned-byte) (i integerp))
  :returns (int integerp
    :rule-classes :type-prescription :name logsat-type)
  :long "<p>If @('i') can be represented as a @('size')-bit signed integer,
then @('i') is returned unchanged.  Otherwise, @('(logsat size i)') returns
the @('size')-bit signed integer closest to @('i').  For positive i, this
will be @($2^{size-1} - 1$).  For negative @('i'), this will be
@($-(2^{size-1}$).</p>

<p>This function returns a (possibly negative) integer.  For consistency with
@(see signed-byte-p), size must be strictly greater than 0.  In contrast, the
related @(see bitops::bitops/saturate) functions always return @('size')-bit
natural numbers.</p>"
  :split-types t
  :enabled t
  (let* ((i (mbe :logic (ifix i) :exec i)) (val (expt2 (the unsigned-byte (1- size))))
      (maxval (the unsigned-byte (1- (the unsigned-byte val))))
      (minval (- val)))
    (declare (type unsigned-byte val maxval)
      (type integer i minval))
    (if (>= i maxval)
      maxval
      (if (<= i minval)
        minval
        i))))

(define logextu
  :short "Logical sign extension, unsigned version.  @('(logextu final-size
 ext-size i)') "sign-extends" i with @('(logext ext-size i)'), then truncates
 the result to @('final-size') bits, creating an unsigned integer."
  ((final-size (and (integerp final-size) (<= 0 final-size))) (ext-size (and (integerp ext-size) (< 0 ext-size)))
    (i integerp))
  :returns (nat natp
    :rule-classes :type-prescription :name logextu-type)
  :enabled t
  :inline t
  (loghead final-size (logext ext-size i)))

(define lognotu
  :short "Logical negation, unsigned version.  @('(lognotu size i)') is an
 unsigned logical @('not').  It just truncates @('(lognot i)') to @('size')
 bits."
  ((size (and (integerp size) (<= 0 size))) (i integerp))
  :returns (nat natp
    :rule-classes :type-prescription :name lognotu-type)
  :enabled t
  :inline t
  (loghead size (lognot i)))

(define logsquash
  ((n natp) (i integerp))
  :short "Squashes to 0 the lowest @('n') bits of @('i')."
  :inline t
  :returns (val integerp :rule-classes :type-prescription)
  (logand i (ash -1 (nfix n))))

(define ashu
  :short "Arithmetic shift, unsigned version."
  ((size (and (integerp size) (< 0 size))) (i integerp)
    (cnt integerp))
  :returns (nat natp :rule-classes :type-prescription :name ashu-type)
  :long "<p>@('ashu') is a fixed-width version of @(see ash).  The integer
@('i') is first coerced to a @('size')-bit signed integer by sign-extension,
then shifted with @('ash'), and finally truncated back to a @('size')-bit
unsigned integer.</p>

<p>See also @(see lshu) for a logical (instead of arithmetic) shift.</p>"
  :enabled t
  (loghead size (ash (logext size i) cnt)))

(define lshu
  :short "Logical shift, unsigned version."
  ((size (and (integerp size) (<= 0 size))) (i integerp)
    (cnt integerp))
  :returns (nat natp :rule-classes :type-prescription :name lshu-type)
  :long "<p>@('lshu') is a fixed-width logical shift.  It shifts @('i')
by @('cnt') bits by first coercing @('i') to an unsigned integer of @('size')
bits, performing the shift, and coercing the result to an @('size')-bit
unsigned integer.</p>

<p>For @('cnt >= 0'), @('(lshu size i cnt) = (ashu size i cnt)').</p>

<p>This is a model of a size-bit logical shift register.</p>"
  :enabled t
  (loghead size (ash (loghead size i) cnt)))

(define logite
  :short "Bitwise if-then-else among integers."
  ((test :type integer) (then :type integer)
    (else :type integer))
  :returns (logite integerp
    :rule-classes :type-prescription :name logite-type)
  (logior (logand test then) (logand (lognot test) else)))

(defxdoc logops-bit-functions
  :parents (logops-definitions bitp)
  :short "Versions of the standard logical operations that operate on single bits."
  :long "<p>We provide versions of the non-trivial standard logical operations
that operate on single bits.</p>

<p>One reason that it is useful to introduce these operations separately from
the standard operations is the fact that @(see lognot) applied to a @(see bitp)
object never returns a @(see bitp).</p>

<p>All arguments to these functions must be @(see bitp), and we prove that
each returns a @(see bitp) integer, i.e., 0 or 1.  We define each function
explicitly in terms of 0 and 1 to simplify reasoning.</p>")

(define b-not
  ((i bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Negation for @(see bitp)s."
  :inline t
  :enabled t
  (mbe :logic (if (zbp i)
      1
      0)
    :exec (the (unsigned-byte 1) (- 1 (the (unsigned-byte 1) i)))))

(define b-and
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Conjunction for @(see bitp)s."
  :inline t
  :enabled t
  (mbe :logic (if (zbp i)
      0
      (if (zbp j)
        0
        1))
    :exec (the (unsigned-byte 1)
      (logand (the (unsigned-byte 1) i) (the (unsigned-byte 1) j)))))

(define b-ior
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Inclusive or for @(see bitp)s."
  :inline t
  :enabled t
  (mbe :logic (if (zbp i)
      (if (zbp j)
        0
        1)
      1)
    :exec (the (unsigned-byte 1)
      (logior (the (unsigned-byte 1) i) (the (unsigned-byte 1) j)))))

(define b-xor
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Exclusive or for @(see bitp)s."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      (if (zbp j)
        0
        1)
      (if (zbp j)
        1
        0))
    :exec (the (unsigned-byte 1)
      (logxor (the (unsigned-byte 1) i) (the (unsigned-byte 1) j)))))

(define b-eqv
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Equivalence (a.k.a. if and only if, xnor) for @(see bitp)s."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      (if (zbp j)
        1
        0)
      (if (zbp j)
        0
        1))
    :exec (the (unsigned-byte 1)
      (logxor (the (unsigned-byte 1)
          (logxor (the (unsigned-byte 1) i) (the (unsigned-byte 1) j)))
        1))))

(define b-nand
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Negated and for @(see bitp)s."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      1
      (if (zbp j)
        1
        0))
    :exec (the (unsigned-byte 1)
      (logxor (the (unsigned-byte 1)
          (logand (the (unsigned-byte 1) i) (the (unsigned-byte 1) j)))
        1))))

(define b-nor
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Negated or for @(see bitp)s."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      (if (zbp j)
        1
        0)
      0)
    :exec (the (unsigned-byte 1)
      (logxor (the (unsigned-byte 1)
          (logior (the (unsigned-byte 1) i) (the (unsigned-byte 1) j)))
        1))))

(define b-andc1
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "And of @(see bitp)s, complementing the first."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      (if (zbp j)
        0
        1)
      0)
    :exec (the (unsigned-byte 1)
      (logandc1 (the (unsigned-byte 1) i)
        (the (unsigned-byte 1) j)))))

(define b-andc2
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "And of @(see bitp)s, complementing the second."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      0
      (if (zbp j)
        1
        0))
    :exec (the (unsigned-byte 1)
      (logandc2 (the (unsigned-byte 1) i)
        (the (unsigned-byte 1) j)))))

(define b-orc1
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Inclusive or of @(see bitp)s, complementing the first."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      1
      (if (zbp j)
        0
        1))
    :exec (the (unsigned-byte 1)
      (logior (the (unsigned-byte 1) (logxor 1 (the (unsigned-byte 1) i)))
        (the (unsigned-byte 1) j)))))

(define b-orc2
  ((i bitp) (j bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "Inclusive or of @(see bitp)s, complementing the second."
  :enabled t
  :inline t
  (mbe :logic (if (zbp i)
      (if (zbp j)
        1
        0)
      1)
    :exec (the (unsigned-byte 1)
      (logior (the (unsigned-byte 1) i)
        (the (unsigned-byte 1) (logxor 1 (the (unsigned-byte 1) j)))))))

(define b-ite
  ((test bitp) (then bitp) (else bitp))
  :returns (bit bitp :rule-classes :type-prescription)
  :short "If-then-else for @(see bitp)s."
  :inline t
  :enabled t
  (if (zbp test)
    (bfix else)
    (bfix then)))