		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-derivation

Bip32-ckd-priv

Private child key derivation.

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

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

The first result is t when the key cannot be computed, as specified in [BIP32]; in this case, the second result is irrelevant (and we just return the parent key). Otherwise, the first result is nil, meaning no error.

Definitions and Theorems

Function: bip32-ckd-priv

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

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

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

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

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

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

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

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

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

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

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

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

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