		Search-engine friendly clone of the ACL2 documentation.

Bip39

Bip39-english-words-bound-p

Check if all the strings in a list have a length less than or equal to 8, which is the maximum length in the English wordlist.

Signature
(bip39-english-words-bound-p strings) → yes/no
Arguments: strings — Guard (string-listp strings).
Returns: yes/no — Type (booleanp yes/no).

The maximum length of the words in the English wordlist is 8. This function is used to prove upper bounds on the length of the menmonic, based on the lengths of the words in the English wordlist and on the maximum number of words in a mnemonic. See bip39-entropy-to-mnemonic.

Definitions and Theorems

Function: bip39-english-words-bound-p

(defun bip39-english-words-bound-p (strings)
  (declare (xargs :guard (string-listp strings)))
  (or (endp strings)
      (and (<= (length (car strings)) 8)
           (bip39-english-words-bound-p (cdr strings)))))

Theorem: booleanp-of-bip39-english-words-bound-p

(defthm booleanp-of-bip39-english-words-bound-p
  (b* ((yes/no (bip39-english-words-bound-p strings)))
    (booleanp yes/no))
  :rule-classes :rewrite)