		Search-engine friendly clone of the ACL2 documentation.

Bip32-wallet-structure

Bip32-compliant-tree-p

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

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

Besides requiring the account keys to comply (which includes the compliance of the chain and address keys), we also require the tree to be rooted at the master private key. That is, we exclude subtrees of the master tree used for partial sharing.

We also require the tree to have depth below 4.

Definitions and Theorems

Function: bip32-compliant-tree-p

(defun bip32-compliant-tree-p (tree)
  (declare (xargs :guard (bip32-key-treep tree)))
  (and (bip32-compliant-accounts-p tree)
       (equal 0 (bip32-key-tree->root-depth tree))
       (bip32-key-tree-priv-p tree)
       (bip32-compliant-depth-p tree)))

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

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

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

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

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

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