		Search-engine friendly clone of the ACL2 documentation.

Bip39

Bip39-entropy-to-mnemonic

Turn an entropy value into a mnemonic.

Signature
(bip39-entropy-to-mnemonic entropy) → mnemonic
Arguments: entropy — Guard (bip39-entropyp entropy).
Returns: mnemonic — Type (stringp 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.

Definitions and Theorems

Function: bip39-entropy-to-mnemonic

(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))

Theorem: stringp-of-bip39-entropy-to-mnemonic

(defthm stringp-of-bip39-entropy-to-mnemonic
  (b* ((mnemonic (bip39-entropy-to-mnemonic entropy)))
    (stringp mnemonic))
  :rule-classes :rewrite)

Theorem: bip39-entropy-to-mnemonic-upper-bound

(defthm bip39-entropy-to-mnemonic-upper-bound
  (<= (length (bip39-entropy-to-mnemonic entropy))
      (* 9 24))
  :rule-classes :linear)

Theorem: bip39-entropy-to-mnemonic-of-bip39-entropy-fix-entropy

(defthm bip39-entropy-to-mnemonic-of-bip39-entropy-fix-entropy
  (equal (bip39-entropy-to-mnemonic (bip39-entropy-fix entropy))
         (bip39-entropy-to-mnemonic entropy)))

Theorem: bip39-entropy-to-mnemonic-bip39-entropy-equiv-congruence-on-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)