Public child key derivation from private parent key, for non-hardedned child keys only.
(bip32-ckd-priv-pub-nh parent i) → (mv error? child)
There is no explicitly named function for this in [BIP32],
but this corresponds to the expression
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.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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)