• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops

Install-bit

(install-bit n val x) sets x[n] = val, where x is an integer, n is a bit position, and val is a bit.

Signature

(install-bit n val x) → *

Arguments

n — Guard (natp n).

val — Guard (bitp val).

x — Guard (integerp x).

Definitions and Theorems

Function: install-bit

(defun
     install-bit (n val x)
     (declare (xargs :guard (and (natp n) (bitp val) (integerp x))))
     (let ((__function__ 'install-bit))
          (declare (ignorable __function__))
          (mbe :logic (b* ((x (ifix x))
                           (n (nfix n))
                           (val (bfix val))
                           (place (ash 1 n))
                           (mask (lognot place)))
                          (logior (logand x mask) (ash val n)))
               :exec (logior (logand x (lognot (ash 1 n)))
                             (ash val n)))))

Theorem: install-bit**

(defthm install-bit**
        (equal (install-bit n val x)
               (if (zp n)
                   (logcons val (logcdr x))
                   (logcons (logcar x)
                            (install-bit (1- n) val (logcdr x)))))
        :rule-classes
        ((:definition :clique (install-bit)
                      :controller-alist ((install-bit t nil nil)))))

Theorem: natp-install-bit

(defthm natp-install-bit
        (implies (not (and (integerp x) (< x 0)))
                 (natp (install-bit n val x)))
        :rule-classes :type-prescription)

Theorem: nat-equiv-implies-equal-install-bit-1

(defthm nat-equiv-implies-equal-install-bit-1
        (implies (nat-equiv n n-equiv)
                 (equal (install-bit n val x)
                        (install-bit n-equiv val x)))
        :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-install-bit-2

(defthm bit-equiv-implies-equal-install-bit-2
        (implies (bit-equiv val val-equiv)
                 (equal (install-bit n val x)
                        (install-bit n val-equiv x)))
        :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-install-bit-3

(defthm int-equiv-implies-equal-install-bit-3
        (implies (int-equiv x x-equiv)
                 (equal (install-bit n val x)
                        (install-bit n val x-equiv)))
        :rule-classes (:congruence))

Theorem: logbitp-of-install-bit-split

(defthm logbitp-of-install-bit-split
        (equal (logbitp m (install-bit n val x))
               (if (= (nfix m) (nfix n))
                   (equal val 1)
                   (logbitp m x))))

Theorem: logbitp-of-install-bit-same

(defthm logbitp-of-install-bit-same
        (equal (logbitp m (install-bit m val x))
               (equal val 1)))

Theorem: logbitp-of-install-bit-diff

(defthm logbitp-of-install-bit-diff
        (implies (not (equal (nfix m) (nfix n)))
                 (equal (logbitp m (install-bit n val x))
                        (logbitp m x))))

Theorem: install-bit-of-install-bit-same

(defthm install-bit-of-install-bit-same
        (equal (install-bit a v (install-bit a v2 x))
               (install-bit a v x)))

Theorem: install-bit-of-install-bit-diff

(defthm
     install-bit-of-install-bit-diff
     (implies (not (equal (nfix a) (nfix b)))
              (equal (install-bit a v (install-bit b v2 x))
                     (install-bit b v2 (install-bit a v x))))
     :rule-classes ((:rewrite :loop-stopper ((a b install-bit)))))

Theorem: install-bit-when-redundant

(defthm install-bit-when-redundant
        (implies (equal (logbit n x) b)
                 (equal (install-bit n b x) (ifix x))))

Theorem: unsigned-byte-p-of-install-bit

(defthm unsigned-byte-p-of-install-bit
        (implies (and (unsigned-byte-p n x)
                      (< (nfix i) n))
                 (unsigned-byte-p n (install-bit i v x))))