Concatenate 4 64-bit numbers together to form an 256-bit result.
(merge-4-u64s a3 a2 a1 a0) → result
Function:
(defun merge-4-u64s (a3 a2 a1 a0) (declare (type (unsigned-byte 64) a3 a2 a1 a0)) (declare (xargs :guard t)) (let ((__function__ 'merge-4-u64s)) (declare (ignorable __function__)) (mbe :logic (logapp* 64 (nfix a0) (nfix a1) (nfix a2) (nfix a3) 0) :exec (merge-2-u128s (the (unsigned-byte 128) (merge-2-u64s a3 a2)) (the (unsigned-byte 128) (merge-2-u64s a1 a0))))))
Theorem:
(defthm acl2::natp-of-merge-4-u64s (b* ((result (merge-4-u64s a3 a2 a1 a0))) (natp result)) :rule-classes :type-prescription)
Theorem:
(defthm unsigned-byte-p-256-of-merge-4-u64s (unsigned-byte-p 256 (merge-4-u64s a3 a2 a1 a0)) :rule-classes ((:rewrite :corollary (implies (>= (nfix n) 256) (unsigned-byte-p n (merge-4-u64s a3 a2 a1 a0))) :hints (("Goal" :in-theory (disable unsigned-byte-p))))))
Theorem:
(defthm merge-4-u64s-is-merge-unsigneds (equal (merge-4-u64s a3 a2 a1 a0) (merge-unsigneds 64 (list (nfix a3) (nfix a2) (nfix a1) (nfix a0)))))
Theorem:
(defthm nat-equiv-implies-equal-merge-4-u64s-4 (implies (nat-equiv a0 a0-equiv) (equal (merge-4-u64s a3 a2 a1 a0) (merge-4-u64s a3 a2 a1 a0-equiv))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-4-u64s-3 (implies (nat-equiv a1 a1-equiv) (equal (merge-4-u64s a3 a2 a1 a0) (merge-4-u64s a3 a2 a1-equiv a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-4-u64s-2 (implies (nat-equiv a2 a2-equiv) (equal (merge-4-u64s a3 a2 a1 a0) (merge-4-u64s a3 a2-equiv a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-4-u64s-1 (implies (nat-equiv a3 a3-equiv) (equal (merge-4-u64s a3 a2 a1 a0) (merge-4-u64s a3-equiv a2 a1 a0))) :rule-classes (:congruence))