Public child key derivation from private parent key, for both hardened and non-hardened child keys.
(bip32-ckd-priv-pub 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.
Function:
(defun bip32-ckd-priv-pub (parent i) (declare (xargs :guard (and (bip32-ext-priv-key-p parent) (ubyte32p i)))) (b* ((irrelevant-child (bip32-n parent)) ((mv error? child-priv) (bip32-ckd-priv parent i)) ((when error?) (mv t irrelevant-child)) (child-pub (bip32-n child-priv))) (mv nil child-pub)))
Theorem:
(defthm booleanp-of-bip32-ckd-priv-pub.error? (b* (((mv ?error? ?child) (bip32-ckd-priv-pub parent i))) (booleanp error?)) :rule-classes :rewrite)
Theorem:
(defthm bip32-ext-pub-key-p-of-bip32-ckd-priv-pub.child (b* (((mv ?error? ?child) (bip32-ckd-priv-pub parent i))) (bip32-ext-pub-key-p child)) :rule-classes :rewrite)
Theorem:
(defthm bip32-ckd-priv-pub-of-bip32-ext-priv-key-fix-parent (equal (bip32-ckd-priv-pub (bip32-ext-priv-key-fix parent) i) (bip32-ckd-priv-pub parent i)))
Theorem:
(defthm bip32-ckd-priv-pub-bip32-ext-priv-key-equiv-congruence-on-parent (implies (bip32-ext-priv-key-equiv parent parent-equiv) (equal (bip32-ckd-priv-pub parent i) (bip32-ckd-priv-pub parent-equiv i))) :rule-classes :congruence)
Theorem:
(defthm bip32-ckd-priv-pub-of-ubyte32-fix-i (equal (bip32-ckd-priv-pub parent (ubyte32-fix i)) (bip32-ckd-priv-pub parent i)))
Theorem:
(defthm bip32-ckd-priv-pub-ubyte32-equiv-congruence-on-i (implies (acl2::ubyte32-equiv i i-equiv) (equal (bip32-ckd-priv-pub parent i) (bip32-ckd-priv-pub parent i-equiv))) :rule-classes :congruence)