		Search-engine friendly clone of the ACL2 documentation.

Bip32-master-key-generation

Bip32-master-key

Generate a master key from a seed.

Signature
(bip32-master-key seed) → (mv error? key)
Arguments: seed — Guard (byte-listp seed).
Returns: error? — Type (booleanp error?).; key — Type (bip32-ext-priv-key-p key).

The exact generation of the seed is not specified in [BIP32], so it is an input to this function.

[BIP32] constrains the length of the seed in bits, namely to be between 128 and 512 bits. In principle, the seed could consist of a number of bits that is not a multiple of 8, but this seems unlikely in practice: that is, the seed will likey consist of a number of whole bytes. The number of whole bytes must be therefore between 16 and 64.

The key for HMAC-SHA-512 is shown as the string "Bitcoin seed" in [BIP32]. It seems reasonable to regard that as the list of bytes consisting of the ASCII codes of the characters in the string, in the order in which they appear in the string.

If the calculated private key is invalid as specified in [BIP32], we return an error flag as the first result; in this case, the second result (the key) is irrelevant). Otherwise, the first result is nil, i.e. no error.

Definitions and Theorems

Function: bip32-master-key

(defun bip32-master-key (seed)
  (declare (xargs :guard (byte-listp seed)))
  (declare (xargs :guard (and (<= 16 (len seed))
                              (<= (len seed) 64))))
  (b* ((hmac-key (string=>nats "Bitcoin seed"))
       (hmac-data seed)
       (big-i (hmac-sha-512 hmac-key hmac-data))
       (big-i-l (take 32 big-i))
       (big-i-r (nthcdr 32 big-i))
       (parsed-big-i-l (bebytes=>nat big-i-l))
       (n (secp256k1-group-prime))
       ((when (or (= parsed-big-i-l 0)
                  (>= parsed-big-i-l n)))
        (b* ((irrelevant-ext-key (bip32-ext-priv-key 1 big-i-r)))
          (mv t irrelevant-ext-key)))
       (ext-key (bip32-ext-priv-key parsed-big-i-l big-i-r)))
    (mv nil ext-key)))

Theorem: booleanp-of-bip32-master-key.error?

(defthm booleanp-of-bip32-master-key.error?
  (b* (((mv ?error? ?key)
        (bip32-master-key seed)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bip32-ext-priv-key-p-of-bip32-master-key.key

(defthm bip32-ext-priv-key-p-of-bip32-master-key.key
  (b* (((mv ?error? ?key)
        (bip32-master-key seed)))
    (bip32-ext-priv-key-p key))
  :rule-classes :rewrite)

Theorem: bip32-master-key-of-byte-list-fix-seed

(defthm bip32-master-key-of-byte-list-fix-seed
  (equal (bip32-master-key (byte-list-fix seed))
         (bip32-master-key seed)))

Theorem: bip32-master-key-byte-list-equiv-congruence-on-seed

(defthm bip32-master-key-byte-list-equiv-congruence-on-seed
  (implies (byte-list-equiv seed seed-equiv)
           (equal (bip32-master-key seed)
                  (bip32-master-key seed-equiv)))
  :rule-classes :congruence)