• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • 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
  • Testing-utilities

• 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))))