• 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
          • Part-install
          • Part-select-and-part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops/part-install
• Bitops/part-select

Part-select-and-part-install

Interactions between part-select and part-install

Definitions and Theorems

Theorem: logbitp-of-part-select-split

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

Theorem: logbitp-of-part-install-split

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

Theorem: part-select-and-part-install-same

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

Theorem: part-select-and-part-install-completely-different-1

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

Theorem: part-select-and-part-install-completely-different-2

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

Theorem: part-install-in-terms-of-logapp

(defthm 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)))))