		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-serialization

Bip32-key-identifier

Identifier of an extended key.

Signature
(bip32-key-identifier key) → id
Arguments: key — Guard (bip32-ext-key-p key).
Returns: id — Type (byte-listp id).

The section `Key identifiers' of [BIP32] says that an extended key is identified by the Hash160 of the serialized elliptic curve public key, ignoring the chain code..

This should apply to both private and public keys. If given a private key, we calculate the corresponding public key.

Definitions and Theorems

Function: bip32-key-identifier

(defun bip32-key-identifier (key)
 (declare (xargs :guard (bip32-ext-key-p key)))
 (b*
  ((pubkey
    (bip32-ext-key-case
     key
     :priv (secp256k1-priv-to-pub (bip32-ext-priv-key->key key.get))
     :pub (bip32-ext-pub-key->key key.get)))
   (serialized (secp256k1-point-to-bytes pubkey t)))
  (hash160 serialized)))

Theorem: byte-listp-of-bip32-key-identifier

(defthm byte-listp-of-bip32-key-identifier
  (b* ((id (bip32-key-identifier key)))
    (byte-listp id))
  :rule-classes :rewrite)

Theorem: len-of-bip32-key-identifier

(defthm len-of-bip32-key-identifier
  (b* ((id (bip32-key-identifier key)))
    (equal (len id) 20))
  :rule-classes :rewrite)

Theorem: bip32-key-identifier-of-bip32-ext-key-fix-key

(defthm bip32-key-identifier-of-bip32-ext-key-fix-key
  (equal (bip32-key-identifier (bip32-ext-key-fix key))
         (bip32-key-identifier key)))

Theorem: bip32-key-identifier-bip32-ext-key-equiv-congruence-on-key

(defthm bip32-key-identifier-bip32-ext-key-equiv-congruence-on-key
  (implies (bip32-ext-key-equiv key key-equiv)
           (equal (bip32-key-identifier key)
                  (bip32-key-identifier key-equiv)))
  :rule-classes :congruence)