		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-derivation

Bip32-n

Calculate an extended public key from an extended private key.

Signature
(bip32-n private) → extpubkey
Arguments: private — Guard (bip32-ext-priv-key-p private).
Returns: extpubkey — Type (bip32-ext-pub-key-p extpubkey).

This is the function \mathsf{N} in [BIP32].

Definitions and Theorems

Function: bip32-n

(defun bip32-n (private)
  (declare (xargs :guard (bip32-ext-priv-key-p private)))
  (b* (((bip32-ext-priv-key private) private)
       (public.key (secp256k1-priv-to-pub private.key))
       (public.chain-code private.chain-code))
    (bip32-ext-pub-key public.key public.chain-code)))

Theorem: bip32-ext-pub-key-p-of-bip32-n

(defthm bip32-ext-pub-key-p-of-bip32-n
  (b* ((extpubkey (bip32-n private)))
    (bip32-ext-pub-key-p extpubkey))
  :rule-classes :rewrite)

Theorem: bip32-n-of-bip32-ext-priv-key-fix-private

(defthm bip32-n-of-bip32-ext-priv-key-fix-private
  (equal (bip32-n (bip32-ext-priv-key-fix private))
         (bip32-n private)))

Theorem: bip32-n-bip32-ext-priv-key-equiv-congruence-on-private

(defthm bip32-n-bip32-ext-priv-key-equiv-congruence-on-private
  (implies (bip32-ext-priv-key-equiv private private-equiv)
           (equal (bip32-n private)
                  (bip32-n private-equiv)))
  :rule-classes :congruence)