		Search-engine friendly clone of the ACL2 documentation.

Bip39

Bip39-entropy-to-word-indexes

Turn an entropy value into a list of word indexes.

Signature
(bip39-entropy-to-word-indexes entropy) → indexes
Arguments: entropy — Guard (bip39-entropyp entropy).
Returns: indexes — Type (ubyte11-listp indexes).

First, we create a checksum of the entropy by taking the first CS bits of the SHA-256 hash of the entropy. Then we append the checksum after the entropy. The resulting sequence of bits is divided into 11-bit chunks, which become the indexes of the words of the mnemonic.

The numer of word indexes (i.e. the length of the result) is the value MS in the table in [BIP39]. This is calculated from ENT, via CS and ENT+CS, as shown in the table in [BIP39]. The theorem below replicates these calculations. The theorem is disabled by default, because the right-hand side expression, despite not involving this function, is relatively complex.

We also prove a validation theorem (disabled by default for the same reason as the other one) showing all the possible values of MS based on the possible values of ENT.

The maximum numer of word indexes is 24.

Definitions and Theorems

Function: bip39-entropy-to-word-indexes

(defun bip39-entropy-to-word-indexes (entropy)
  (declare (xargs :guard (bip39-entropyp entropy)))
  (b* ((entropy (bip39-entropy-fix entropy))
       (entropy-bytes (bits=>bebytes entropy))
       (hash-bytes (sha-256-bytes entropy-bytes))
       (hash (bebytes=>bits hash-bytes))
       (checksum (take (/ (len entropy) 32) hash))
       (all-bits (append entropy checksum)))
    (bits=>beubyte11s all-bits)))

Theorem: ubyte11-listp-of-bip39-entropy-to-word-indexes

(defthm ubyte11-listp-of-bip39-entropy-to-word-indexes
  (b* ((indexes (bip39-entropy-to-word-indexes entropy)))
    (ubyte11-listp indexes))
  :rule-classes :rewrite)

Theorem: len-of-bip39-entropy-to-word-indexes

(defthm len-of-bip39-entropy-to-word-indexes
  (equal (len (bip39-entropy-to-word-indexes entropy))
         (b* ((ent (len (bip39-entropy-fix entropy)))
              (cs (/ ent 32))
              (ent+cs (+ ent cs))
              (ms (/ ent+cs 11)))
           ms)))

Theorem: values-of-len-of-bip39-entropy-to-word-indexes

(defthm values-of-len-of-bip39-entropy-to-word-indexes
  (equal (len (bip39-entropy-to-word-indexes entropy))
         (case (len (bip39-entropy-fix entropy))
           (128 12)
           (160 15)
           (192 18)
           (224 21)
           (256 24))))

Theorem: bip39-entropy-to-word-indexes-upper-bound

(defthm bip39-entropy-to-word-indexes-upper-bound
  (<= (len (bip39-entropy-to-word-indexes entropy))
      24)
  :rule-classes :linear)

Theorem: bip39-entropy-to-word-indexes-of-bip39-entropy-fix-entropy

(defthm bip39-entropy-to-word-indexes-of-bip39-entropy-fix-entropy
  (equal (bip39-entropy-to-word-indexes (bip39-entropy-fix entropy))
         (bip39-entropy-to-word-indexes entropy)))

Theorem: bip39-entropy-to-word-indexes-bip39-entropy-equiv-congruence-on-entropy

(defthm
 bip39-entropy-to-word-indexes-bip39-entropy-equiv-congruence-on-entropy
 (implies (bip39-entropy-equiv entropy entropy-equiv)
          (equal (bip39-entropy-to-word-indexes entropy)
                 (bip39-entropy-to-word-indexes entropy-equiv)))
 :rule-classes :congruence)