• 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
          • Merge-64-u8s
          • Merge-32-u8s
          • Merge-32-u16s
          • Merge-16-bits
          • Merge-16-u8s
          • Merge-16-u32s
          • Merge-16-u16s
          • Merge-8-bits
          • Merge-8-u2s
          • Merge-8-u4s
          • Merge-8-u64s
          • Merge-8-u32s
          • Merge-8-u16s
          • Merge-8-u8s
          • Merge-4-bits
          • Merge-4-u8s
          • Merge-4-u4s
          • Merge-4-u16s
          • Merge-4-u2s
          • Merge-4-u64s
          • Merge-4-u32s
          • Merge-4-u128s
          • Merge-2-bits
          • Merge-2-u8s
          • Merge-2-u64s
          • Merge-2-u32s
          • Merge-2-u256s
          • Merge-2-u16s
          • Merge-2-u128s
          • Merge-2-u4s
          • Merge-2-u2s
          • Merge-unsigneds
          • Merge-unsigneds-aux
          • Indexed-subst-templates
        • 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/merge

Merge-16-u32s

Concatenate 16 32-bit numbers together to form an 512-bit result.

Signature

(merge-16-u32s a15 a14 a13 a12 
               a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) 
 
  → 
result

Returns

result — Type (natp result).

Definitions and Theorems

Function: merge-16-u32s

(defun
 merge-16-u32s
 (a15 a14 a13 a12
      a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
 (declare (type (unsigned-byte 32)
                a15 a14 a13 a12
                a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))
 (declare (xargs :guard t))
 (let
  ((__function__ 'merge-16-u32s))
  (declare (ignorable __function__))
  (mbe
   :logic (logapp* 32 (nfix a0)
                   (nfix a1)
                   (nfix a2)
                   (nfix a3)
                   (nfix a4)
                   (nfix a5)
                   (nfix a6)
                   (nfix a7)
                   (nfix a8)
                   (nfix a9)
                   (nfix a10)
                   (nfix a11)
                   (nfix a12)
                   (nfix a13)
                   (nfix a14)
                   (nfix a15)
                   0)
   :exec
   (merge-2-u256s (the (unsigned-byte 256)
                       (merge-8-u32s a15 a14 a13 a12 a11 a10 a9 a8))
                  (the (unsigned-byte 256)
                       (merge-8-u32s a7 a6 a5 a4 a3 a2 a1 a0))))))

Theorem: natp-of-merge-16-u32s

(defthm
 acl2::natp-of-merge-16-u32s
 (b*
    ((result (merge-16-u32s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
    (natp result))
 :rule-classes :type-prescription)

Theorem: unsigned-byte-p-512-of-merge-16-u32s

(defthm unsigned-byte-p-512-of-merge-16-u32s
        (unsigned-byte-p
             512
             (merge-16-u32s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))

Theorem: merge-16-u32s-is-merge-unsigneds

(defthm merge-16-u32s-is-merge-unsigneds
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-unsigneds 32
                                (list (nfix a15)
                                      (nfix a14)
                                      (nfix a13)
                                      (nfix a12)
                                      (nfix a11)
                                      (nfix a10)
                                      (nfix a9)
                                      (nfix a8)
                                      (nfix a7)
                                      (nfix a6)
                                      (nfix a5)
                                      (nfix a4)
                                      (nfix a3)
                                      (nfix a2)
                                      (nfix a1)
                                      (nfix a0)))))

Basic nat-equiv congruences.

Theorem: nat-equiv-implies-equal-merge-16-u32s-16

(defthm
   nat-equiv-implies-equal-merge-16-u32s-16
   (implies
        (nat-equiv a0 a0-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6 a5 a4 a3 a2 a1 a0-equiv)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-15

(defthm
   nat-equiv-implies-equal-merge-16-u32s-15
   (implies
        (nat-equiv a1 a1-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6 a5 a4 a3 a2 a1-equiv a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-14

(defthm
   nat-equiv-implies-equal-merge-16-u32s-14
   (implies
        (nat-equiv a2 a2-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6 a5 a4 a3 a2-equiv a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-13

(defthm
   nat-equiv-implies-equal-merge-16-u32s-13
   (implies
        (nat-equiv a3 a3-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6 a5 a4 a3-equiv a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-12

(defthm
   nat-equiv-implies-equal-merge-16-u32s-12
   (implies
        (nat-equiv a4 a4-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6 a5 a4-equiv a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-11

(defthm
   nat-equiv-implies-equal-merge-16-u32s-11
   (implies
        (nat-equiv a5 a5-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6 a5-equiv a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-10

(defthm
   nat-equiv-implies-equal-merge-16-u32s-10
   (implies
        (nat-equiv a6 a6-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7 a6-equiv a5 a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-9

(defthm
   nat-equiv-implies-equal-merge-16-u32s-9
   (implies
        (nat-equiv a7 a7-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8 a7-equiv a6 a5 a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-8

(defthm
   nat-equiv-implies-equal-merge-16-u32s-8
   (implies
        (nat-equiv a8 a8-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9 a8-equiv a7 a6 a5 a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-7

(defthm
   nat-equiv-implies-equal-merge-16-u32s-7
   (implies
        (nat-equiv a9 a9-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10
                              a9-equiv a8 a7 a6 a5 a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-6

(defthm
   nat-equiv-implies-equal-merge-16-u32s-6
   (implies
        (nat-equiv a10 a10-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11 a10-equiv
                              a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-5

(defthm
   nat-equiv-implies-equal-merge-16-u32s-5
   (implies
        (nat-equiv a11 a11-equiv)
        (equal (merge-16-u32s a15 a14 a13 a12
                              a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-16-u32s a15 a14 a13 a12 a11-equiv
                              a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
   :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-4

(defthm
 nat-equiv-implies-equal-merge-16-u32s-4
 (implies
      (nat-equiv a12 a12-equiv)
      (equal (merge-16-u32s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-u32s a15 a14 a13 a12-equiv
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-3

(defthm
 nat-equiv-implies-equal-merge-16-u32s-3
 (implies
      (nat-equiv a13 a13-equiv)
      (equal (merge-16-u32s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-u32s a15 a14 a13-equiv a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-2

(defthm
 nat-equiv-implies-equal-merge-16-u32s-2
 (implies
      (nat-equiv a14 a14-equiv)
      (equal (merge-16-u32s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-u32s a15 a14-equiv a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u32s-1

(defthm
 nat-equiv-implies-equal-merge-16-u32s-1
 (implies
      (nat-equiv a15 a15-equiv)
      (equal (merge-16-u32s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-u32s a15-equiv a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))