		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-2-u128s

Concatenate 2 128-bit numbers together to form an 256-bit result.

Signature
(merge-2-u128s a1 a0) → result
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-2-u128s

(defun
 merge-2-u128s (a1 a0)
 (declare (type (unsigned-byte 128) a1 a0))
 (declare (xargs :guard t))
 (let
     ((__function__ 'merge-2-u128s))
     (declare (ignorable __function__))
     (mbe :logic (logapp* 128 (nfix a0) (nfix a1) 0)
          :exec (b* ((ans a0))
                    (the (unsigned-byte 256)
                         (logior (the (unsigned-byte 256)
                                      (ash a1 (* 1 128)))
                                 (the (unsigned-byte 256) ans)))))))

Theorem: natp-of-merge-2-u128s

(defthm acl2::natp-of-merge-2-u128s
        (b* ((result (merge-2-u128s a1 a0)))
            (natp result))
        :rule-classes :type-prescription)

Theorem: unsigned-byte-p-256-of-merge-2-u128s

(defthm unsigned-byte-p-256-of-merge-2-u128s
        (unsigned-byte-p 256 (merge-2-u128s a1 a0)))

Theorem: merge-2-u128s-is-merge-unsigneds

(defthm merge-2-u128s-is-merge-unsigneds
        (equal (merge-2-u128s a1 a0)
               (merge-unsigneds 128 (list (nfix a1) (nfix a0)))))

Basic nat-equiv congruences.

Theorem: nat-equiv-implies-equal-merge-2-u128s-2

(defthm nat-equiv-implies-equal-merge-2-u128s-2
        (implies (nat-equiv a0 a0-equiv)
                 (equal (merge-2-u128s a1 a0)
                        (merge-2-u128s a1 a0-equiv)))
        :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-2-u128s-1

(defthm nat-equiv-implies-equal-merge-2-u128s-1
        (implies (nat-equiv a1 a1-equiv)
                 (equal (merge-2-u128s a1 a0)
                        (merge-2-u128s a1-equiv a0)))
        :rule-classes (:congruence))