		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-derivation

Bip32-ckd-priv-pub-nh

Public child key derivation from private parent key, for non-hardedned child keys only.

Signature
(bip32-ckd-priv-pub-nh 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-pub-key-p child).

There is no explicitly named function for this in [BIP32], but this corresponds to the expression \mathsf{CKDpub} (\mathsf{N} (\mathsf{k}_\mathsf{par},\mathsf{c}_\mathsf{par}), \mathsf{i}) in [BIP32]. We define an explicit function for that here.

In case of error, we return an irrelevant child key.

Proving the equivalence of this function with bip32-ckd-priv-pub (for non-hardened child keys) requires the use of certain properties of elliptic curve operations that are currently not formalized in the secp256k1 interface. Thus, this proof will be done later.

Definitions and Theorems

Function: bip32-ckd-priv-pub-nh

(defun bip32-ckd-priv-pub-nh (parent i)
  (declare (xargs :guard (and (bip32-ext-priv-key-p parent)
                              (ubyte32p i))))
  (bip32-ckd-pub (bip32-n parent) i))

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

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

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

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

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

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

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

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

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

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

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

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