Turn an entropy value into a mnemonic.
This is the composition of the three functions that map entropy to word indexes, word indexes to words, and words to mnemonic.
Since the maximum numer of words is 24, given the bound on the mnemonic as 9 times the number of words, we show that the the length of the mnemonic has an upper bound equal to the product of 9 and 24.
(defun bip39-entropy-to-mnemonic (entropy) (declare (xargs :guard (bip39-entropyp entropy))) (b* ((indexes (bip39-entropy-to-word-indexes entropy)) (words (bip39-word-indexes-to-words indexes)) (mnemonic (bip39-words-to-mnemonic words))) mnemonic))
(defthm stringp-of-bip39-entropy-to-mnemonic (b* ((mnemonic (bip39-entropy-to-mnemonic entropy))) (stringp mnemonic)) :rule-classes :rewrite)
(defthm bip39-entropy-to-mnemonic-upper-bound (<= (length (bip39-entropy-to-mnemonic entropy)) (* 9 24)) :rule-classes :linear)
(defthm bip39-entropy-to-mnemonic-of-bip39-entropy-fix-entropy (equal (bip39-entropy-to-mnemonic (bip39-entropy-fix entropy)) (bip39-entropy-to-mnemonic entropy)))
(defthm bip39-entropy-to-mnemonic-bip39-entropy-equiv-congruence-on-entropy (implies (bip39-entropy-equiv entropy entropy-equiv) (equal (bip39-entropy-to-mnemonic entropy) (bip39-entropy-to-mnemonic entropy-equiv))) :rule-classes :congruence)