		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-derivation

Bip32-ckd-pub

Public child key derivation from public parent key.

Signature
(bip32-ckd-pub parent i) → (mv error? child)
Arguments: parent — Guard (bip32-ext-pub-key-p parent).; i — Guard (ubyte32p i).
Returns: error? — Type (booleanp error?).; child — Type (bip32-ext-pub-key-p child).

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

The first result is t if the index is 2^{31} or more or if the key cannot be computed, as specified in [BIP32]; in these cases, the second result is irrelevant (and we just return the parent key). Otherwise, the first result is nil, meaning no error.

We could have restricted the argument i to be below 2^{31}, but [BIP32] handles the error explicitly in the definition of the function, so we do the same here.

Definitions and Theorems

Function: bip32-ckd-pub

(defun bip32-ckd-pub (parent i)
  (declare (xargs :guard (and (bip32-ext-pub-key-p parent)
                              (ubyte32p i))))
  (b*
    (((bip32-ext-pub-key parent) parent)
     (irrelevant-child (bip32-ext-pub-key-fix parent))
     (i (mbe :logic (ubyte32-fix i) :exec i))
     ((when (>= i (expt 2 31)))
      (mv t irrelevant-child))
     (data (append (secp256k1-point-to-bytes parent.key t)
                   (nat=>bebytes 4 i)))
     (big-i (hmac-sha-512 parent.chain-code 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 (>= parsed-big-i-l n))
      (mv t irrelevant-child))
     (child.key
          (secp256k1-add (secp256k1-mul parsed-big-i-l
                                        (secp256k1-point-generator))
                         parent.key))
     ((when (secp256k1-point-infinityp child.key))
      (mv t irrelevant-child))
     (child.chain-code big-i-r))
    (mv nil
        (bip32-ext-pub-key child.key child.chain-code))))

Theorem: booleanp-of-bip32-ckd-pub.error?

(defthm booleanp-of-bip32-ckd-pub.error?
  (b* (((mv ?error? ?child)
        (bip32-ckd-pub parent i)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bip32-ext-pub-key-p-of-bip32-ckd-pub.child

(defthm bip32-ext-pub-key-p-of-bip32-ckd-pub.child
  (b* (((mv ?error? ?child)
        (bip32-ckd-pub parent i)))
    (bip32-ext-pub-key-p child))
  :rule-classes :rewrite)

Theorem: bip32-ckd-pub-of-bip32-ext-pub-key-fix-parent

(defthm bip32-ckd-pub-of-bip32-ext-pub-key-fix-parent
  (equal (bip32-ckd-pub (bip32-ext-pub-key-fix parent)
                        i)
         (bip32-ckd-pub parent i)))

Theorem: bip32-ckd-pub-bip32-ext-pub-key-equiv-congruence-on-parent

(defthm bip32-ckd-pub-bip32-ext-pub-key-equiv-congruence-on-parent
  (implies (bip32-ext-pub-key-equiv parent parent-equiv)
           (equal (bip32-ckd-pub parent i)
                  (bip32-ckd-pub parent-equiv i)))
  :rule-classes :congruence)

Theorem: bip32-ckd-pub-of-ubyte32-fix-i

(defthm bip32-ckd-pub-of-ubyte32-fix-i
  (equal (bip32-ckd-pub parent (ubyte32-fix i))
         (bip32-ckd-pub parent i)))

Theorem: bip32-ckd-pub-ubyte32-equiv-congruence-on-i

(defthm bip32-ckd-pub-ubyte32-equiv-congruence-on-i
  (implies (acl2::ubyte32-equiv i i-equiv)
           (equal (bip32-ckd-pub parent i)
                  (bip32-ckd-pub parent i-equiv)))
  :rule-classes :congruence)