Retrieven the public key designated by a path in a key tree.
(bip32-get-pub-key-at-path tree path) → key
The tree may consist of private or public keys.
Function:
(defun bip32-get-pub-key-at-path (tree path) (declare (xargs :guard (and (bip32-key-treep tree) (ubyte32-listp path)))) (declare (xargs :guard (bip32-path-in-tree-p path tree))) (b* ((root-extkey (bip32-key-tree->root-key tree)) ((mv error? extkey) (bip32-ckd* root-extkey path)) ((unless (mbt (not error?))) (b* ((irrelevant (secp256k1-priv-to-pub 1))) irrelevant))) (bip32-ext-key-case extkey :priv (b* ((extprivkey (bip32-ext-key-priv->get extkey)) (privkey (bip32-ext-priv-key->key extprivkey)) (pubkey (secp256k1-priv-to-pub privkey))) pubkey) :pub (b* ((extpubkey (bip32-ext-key-pub->get extkey)) (pubkey (bip32-ext-pub-key->key extpubkey))) pubkey))))
Theorem:
(defthm secp256k1-pub-key-p-of-bip32-get-pub-key-at-path (b* ((key (bip32-get-pub-key-at-path tree path))) (secp256k1-pub-key-p key)) :rule-classes :rewrite)
Theorem:
(defthm bip32-get-pub-key-at-path-of-bip32-key-tree-fix-tree (equal (bip32-get-pub-key-at-path (bip32-key-tree-fix tree) path) (bip32-get-pub-key-at-path tree path)))
Theorem:
(defthm bip32-get-pub-key-at-path-bip32-key-tree-equiv-congruence-on-tree (implies (bip32-key-tree-equiv tree tree-equiv) (equal (bip32-get-pub-key-at-path tree path) (bip32-get-pub-key-at-path tree-equiv path))) :rule-classes :congruence)
Theorem:
(defthm bip32-get-pub-key-at-path-of-ubyte32-list-fix-path (equal (bip32-get-pub-key-at-path tree (ubyte32-list-fix path)) (bip32-get-pub-key-at-path tree path)))
Theorem:
(defthm bip32-get-pub-key-at-path-ubyte32-list-equiv-congruence-on-path (implies (acl2::ubyte32-list-equiv path path-equiv) (equal (bip32-get-pub-key-at-path tree path) (bip32-get-pub-key-at-path tree path-equiv))) :rule-classes :congruence)