part-install

(in-package "BITOPS")

(include-book "xdoc/top" :dir :system)

(include-book "std/basic/arith-equivs" :dir :system)

(include-book "ihs/basic-definitions" :dir :system)

(include-book "part-select")

(local (include-book "ihsext-basics"))

(local (include-book "equal-by-logbitp"))

(local (in-theory (disable logmask)))

(defsection bitops/part-install
  :parents (bitops)
  :short "This book provides a way to set a portion of an integer to
some value.")

(defsection part-install
  :parents (bitops/part-install)
  :short "Set a portion of bits of an integer to some value"
  :long "<p>@('part-install') is a macro that is defined in terms of
  the function @('part-install-width-low').  This macro can be used to
  set a portion of bits from an integer to some value.</p>

<p>Usage:</p>
@({
     (part-install val x :low 8 :high  15)   ;; x[15:8] = val
     (part-install val x :low 8 :width  8)   ;; x[15:8] = val

})

@(def part-install-width-low)

@(def part-install)
"
  (local (defthm logmask-and-ash
      (implies (natp n)
        (equal (+ -1 (ash 1 n)) (logmask n)))
      :hints (("Goal" :in-theory (enable logmask ash-1-removal)))))
  (defun-inline part-install-width-low
    (val x width low)
    (declare (xargs :guard (and (integerp x)
          (integerp val)
          (natp width)
          (natp low))
        :guard-hints (("Goal" :in-theory (disable logmask ash-1-removal)))))
    (mbe :logic (let* ((x (ifix x)) (val (ifix val))
          (width (nfix width))
          (low (nfix low))
          (val (loghead width val))
          (mask (logmask width)))
        (logior (logand x (lognot (ash mask low)))
          (ash val low)))
      :exec (let* ((mask (1- (ash 1 width))) (val (logand mask val)))
        (logior (logand x (lognot (ash mask low)))
          (ash val low)))))
  (defthm natp-part-install-width-low
    (implies (<= 0 x)
      (natp (part-install-width-low val
          x
          width
          low)))
    :rule-classes :type-prescription)
  (defcong int-equiv
    equal
    (part-install-width-low val
      x
      width
      low)
    1)
  (defcong int-equiv
    equal
    (part-install-width-low val
      x
      width
      low)
    2)
  (defcong nat-equiv
    equal
    (part-install-width-low val
      x
      width
      low)
    3)
  (defcong nat-equiv
    equal
    (part-install-width-low val
      x
      width
      low)
    4)
  (defmacro part-install
    (val x
      &key
      low
      high
      width)
    (cond ((and high width) (er hard?
          'part-install
          "Can't use :high and :width together."))
      ((and low
         high
         (integerp low)
         (integerp high)) `(part-install-width-low ,BITOPS::VAL
          ,BITOPS::X
          ,(+ 1 BITOPS::HIGH (- BITOPS::LOW))
          ,BITOPS::LOW))
      ((and low high) `(part-install-width-low ,BITOPS::VAL
          ,BITOPS::X
          (+ 1 ,BITOPS::HIGH (- ,BITOPS::LOW))
          ,BITOPS::LOW))
      ((and low width) `(part-install-width-low ,BITOPS::VAL
          ,BITOPS::X
          ,BITOPS::WIDTH
          ,BITOPS::LOW))
      (t (er hard?
          'part-install
          "Need either :low and :width, or :low and :high."))))
  (add-macro-alias part-install
    part-install-width-low$inline)
  (defthm unsigned-byte-p-=-n-of-part-install-width-low
    (implies (and (unsigned-byte-p n x)
        (<= (+ width low) n)
        (natp n)
        (natp low)
        (natp width))
      (unsigned-byte-p n
        (part-install-width-low val
          x
          width
          low)))
    :hints (("Goal" :in-theory (e/d nil (unsigned-byte-p)))))
  (defthm unsigned-byte-p->-n-of-part-install-width-low
    (implies (and (unsigned-byte-p n x)
        (< n (+ width low))
        (natp low)
        (natp width))
      (unsigned-byte-p (+ low width)
        (part-install-width-low val
          x
          width
          low)))
    :hints (("Goal" :in-theory (e/d nil (unsigned-byte-p))))))

(local (include-book "std/system/non-parallel-book" :dir :system))

(local (non-parallel-book))

(defsection part-select-and-part-install
  :parents (bitops/part-install bitops/part-select)
  :short "Interactions between @('part-select') and @('part-install')"
  (defthm logbitp-of-part-select-split
    (equal (logbitp n
        (part-select-width-low x
          width
          low))
      (and (< (nfix n) (nfix width))
        (logbitp (+ (nfix n) (nfix low))
          x)))
    :hints (("Goal" :in-theory (enable part-select-width-low))))
  (defthm logbitp-of-part-install-split
    (equal (logbitp n
        (part-install-width-low val
          x
          width
          low))
      (if (and (< (nfix n)
            (+ (nfix low) (nfix width)))
          (<= (nfix low) (nfix n)))
        (logbitp (- (nfix n) (nfix low))
          val)
        (logbitp n x)))
    :hints (("Goal" :in-theory (enable part-install-width-low))))
  (defthm part-select-and-part-install-same
    (equal (part-select-width-low (part-install-width-low val
          x
          width
          low)
        width
        low)
      (loghead width val))
    :hints ((logbitp-reasoning)))
  (defthm part-select-and-part-install-completely-different-1
    (implies (<= (+ (nfix low-i)
          (nfix width-i))
        (nfix low-s))
      (equal (part-select-width-low (part-install-width-low val
            x
            width-i
            low-i)
          width-s
          low-s)
        (part-select-width-low x
          width-s
          low-s)))
    :hints ((logbitp-reasoning)))
  (defthm part-select-and-part-install-completely-different-2
    (implies (<= (+ (nfix low-s)
          (nfix width-s))
        (nfix low-i))
      (equal (part-select-width-low (part-install-width-low val
            x
            width-i
            low-i)
          width-s
          low-s)
        (part-select-width-low x
          width-s
          low-s)))
    :hints ((logbitp-reasoning)))
  (defthmd part-install-in-terms-of-logapp
    (equal (part-install val
        x
        :width width
        :low low)
      (logapp low
        x
        (logapp width
          val
          (logtail (+ (nfix low) (nfix width))
            x))))
    :hints ((logbitp-reasoning))))