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