|
|
|---|
|
|
|
|---|
Turn a list of mnemonic words into a single string, i.e. the mnemonic.
(bip39-words-to-mnemonic words) → mnemonic
If the words come from the English wordlist (as they do), whose maximum word length is 8, then we can calculate an upper bound on the length of the mnemonic that is a function of the number of words. Given that one extra character (the space) is added after each word (except the last one), the upper bound is 9 multiplied by the number of words. Since there is no ending space, a tighter bound is one unit smaller, but that holds only if there is at least one word (if there is no word, the total length is 0). So it's just simpler to use the slightly looser, but simpler, bound.
Function:
(defun bip39-words-to-mnemonic (words) (declare (xargs :guard (string-listp words))) (str::join (str::string-list-fix words) " "))
Theorem:
(defthm stringp-of-bip39-words-to-mnemonic (b* ((mnemonic (bip39-words-to-mnemonic words))) (stringp mnemonic)) :rule-classes :rewrite)
Theorem:
(defthm bip39-words-to-mnemonic-upper-bound (implies (bip39-english-words-bound-p words) (<= (length (bip39-words-to-mnemonic words)) (* 9 (len words)))) :rule-classes :linear)
Theorem:
(defthm bip39-words-to-mnemonic-of-string-list-fix-words (equal (bip39-words-to-mnemonic (str::string-list-fix words)) (bip39-words-to-mnemonic words)))
Theorem:
(defthm bip39-words-to-mnemonic-string-list-equiv-congruence-on-words (implies (str::string-list-equiv words words-equiv) (equal (bip39-words-to-mnemonic words) (bip39-words-to-mnemonic words-equiv))) :rule-classes :congruence)