		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-polymod-aux

Signature
(bech32-polymod-aux values chk) → checksum
Arguments: values — Guard (unsigned-byte-listp 8 values).; chk — Guard (unsigned-byte-p 48 chk).
Returns: checksum — Type (unsigned-byte-p 48 checksum).

Definitions and Theorems

Function: bech32-polymod-aux

(defun bech32-polymod-aux (values chk)
  (declare (xargs :guard (and (unsigned-byte-listp 8 values)
                              (unsigned-byte-p 48 chk))))
  (let ((__function__ 'bech32-polymod-aux))
    (declare (ignorable __function__))
    (if (not (mbt (unsigned-byte-p 48 chk)))
        0
      (if (endp values)
          chk
        (b* ((v (first values))
             (b (bvshr 48 chk 25))
             (chk (bvxor 48 (bvshl 48 (bvand 48 chk 33554431) 5)
                         v))
             (chk (bvxor 48 chk
                         (if (oddp (bvshr 48 b 0))
                             (nth 0 *bech32-gen*)
                           0)))
             (chk (bvxor 48 chk
                         (if (oddp (bvshr 48 b 1))
                             (nth 1 *bech32-gen*)
                           0)))
             (chk (bvxor 48 chk
                         (if (oddp (bvshr 48 b 2))
                             (nth 2 *bech32-gen*)
                           0)))
             (chk (bvxor 48 chk
                         (if (oddp (bvshr 48 b 3))
                             (nth 3 *bech32-gen*)
                           0)))
             (chk (bvxor 48 chk
                         (if (oddp (bvshr 48 b 4))
                             (nth 4 *bech32-gen*)
                           0))))
          (bech32-polymod-aux (rest values)
                              chk))))))

Theorem: return-type-of-bech32-polymod-aux

(defthm return-type-of-bech32-polymod-aux
  (b* ((checksum (bech32-polymod-aux values chk)))
    (unsigned-byte-p 48 checksum))
  :rule-classes :rewrite)