Check if a key tree includes a subtree for a given purpose.
(bip43-key-tree-has-purpose-p tree purpose) → yes/no
We check if the tree is rooted at the private master key and includes the singleton path with the (hardened) purpose number.
Function:
(defun bip43-key-tree-has-purpose-p (tree purpose) (declare (xargs :guard (and (bip32-key-treep tree) (bip43-purposep purpose)))) (and (bip32-key-tree-priv-p tree) (equal (bip32-key-tree->root-depth tree) 0) (b* ((purpose-hardened (+ (bip43-purpose-fix purpose) (expt 2 31)))) (bip32-path-in-tree-p (list purpose-hardened) tree))))
Theorem:
(defthm booleanp-of-bip43-key-tree-has-purpose-p (b* ((yes/no (bip43-key-tree-has-purpose-p tree purpose))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip43-key-tree-has-purpose-p-of-bip32-key-tree-fix-tree (equal (bip43-key-tree-has-purpose-p (bip32-key-tree-fix tree) purpose) (bip43-key-tree-has-purpose-p tree purpose)))
Theorem:
(defthm bip43-key-tree-has-purpose-p-bip32-key-tree-equiv-congruence-on-tree (implies (bip32-key-tree-equiv tree tree-equiv) (equal (bip43-key-tree-has-purpose-p tree purpose) (bip43-key-tree-has-purpose-p tree-equiv purpose))) :rule-classes :congruence)
Theorem:
(defthm bip43-key-tree-has-purpose-p-of-bip43-purpose-fix-purpose (equal (bip43-key-tree-has-purpose-p tree (bip43-purpose-fix purpose)) (bip43-key-tree-has-purpose-p tree purpose)))
Theorem:
(defthm bip43-key-tree-has-purpose-p-bip43-purpose-equiv-congruence-on-purpose (implies (bip43-purpose-equiv purpose purpose-equiv) (equal (bip43-key-tree-has-purpose-p tree purpose) (bip43-key-tree-has-purpose-p tree purpose-equiv))) :rule-classes :congruence)