		Search-engine friendly clone of the ACL2 documentation.

Bip44

Bip44-compliant-tree-p

Check if a key tree complies with the BIP 44 wallet structure.

Signature
(bip44-compliant-tree-p tree) → yes/no
Arguments: tree — Guard (bip32-key-treep tree).
Returns: yes/no — Type (booleanp yes/no).

We require the tree to start with the master private key (depth 0), to include the purpose key, to have compliant subtrees for any supported coins, and to not exceed depth 5.

Definitions and Theorems

Function: bip44-compliant-tree-p

(defun bip44-compliant-tree-p (tree)
  (declare (xargs :guard (bip32-key-treep tree)))
  (and (equal 0 (bip32-key-tree->root-depth tree))
       (bip32-key-tree-priv-p tree)
       (bip43-key-tree-has-purpose-p tree *bip44-purpose*)
       (bip44-compliant-coins-p tree)
       (bip44-compliant-depth-p tree)))

Theorem: booleanp-of-bip44-compliant-tree-p

(defthm booleanp-of-bip44-compliant-tree-p
  (b* ((yes/no (bip44-compliant-tree-p tree)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: bip44-compliant-tree-p-of-bip32-key-tree-fix-tree

(defthm bip44-compliant-tree-p-of-bip32-key-tree-fix-tree
  (equal (bip44-compliant-tree-p (bip32-key-tree-fix tree))
         (bip44-compliant-tree-p tree)))

Theorem: bip44-compliant-tree-p-bip32-key-tree-equiv-congruence-on-tree

(defthm
     bip44-compliant-tree-p-bip32-key-tree-equiv-congruence-on-tree
  (implies (bip32-key-tree-equiv tree tree-equiv)
           (equal (bip44-compliant-tree-p tree)
                  (bip44-compliant-tree-p tree-equiv)))
  :rule-classes :congruence)