		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-serialization

Bip32-key-fingerprint

Fingerprint of an extended key.

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

The section `Key identifiers' of [BIP32] says that the first 32 bits (i.e. 4 bytes) of a key identifier are the key fingerprint.

Definitions and Theorems

Function: bip32-key-fingerprint

(defun bip32-key-fingerprint (key)
  (declare (xargs :guard (bip32-ext-key-p key)))
  (take 4 (bip32-key-identifier key)))

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

(defthm byte-listp-of-bip32-key-fingerprint
  (b* ((fp (bip32-key-fingerprint key)))
    (byte-listp fp))
  :rule-classes :rewrite)

Theorem: len-of-bip32-key-fingerprint

(defthm len-of-bip32-key-fingerprint
  (b* ((fp (bip32-key-fingerprint key)))
    (equal (len fp) 4))
  :rule-classes :rewrite)

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

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

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

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