		Search-engine friendly clone of the ACL2 documentation.

Bech32

Hrp-valid-p

Check if a Bech32 human-readable portion is valid.

Signature
(hrp-valid-p s) → y/n
Arguments: s — Guard (stringp s).
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: hrp-valid-p

(defun hrp-valid-p (s)
  (declare (xargs :guard (stringp s)))
  (let ((__function__ 'hrp-valid-p))
    (declare (ignorable __function__))
    (and (hrp-valid-string-length-p s)
         (loop$ for x in (explode s)
                always
                (and (characterp x)
                     (hrp-valid-char-code-p (char-code x)))))))

Theorem: booleanp-of-hrp-valid-p

(defthm booleanp-of-hrp-valid-p
  (b* ((y/n (hrp-valid-p s)))
    (booleanp y/n))
  :rule-classes :rewrite)