		Search-engine friendly clone of the ACL2 documentation.

Bip44

Bip44-compliant-depth-p

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

According to [BIP44], the key tree stops at depth 5, i.e. the address keys have no children (and therefore no grandchildren, great-grandchildren, etc.). This is formally expressed by saying that every path in the tree has a length below 6.

Definitions and Theorems

Theorem: bip44-compliant-depth-p-necc

(defthm bip44-compliant-depth-p-necc
  (implies (bip44-compliant-depth-p tree)
           (implies (and (ubyte32-listp path)
                         (bip32-path-in-tree-p path tree))
                    (< (len path) 6))))

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

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

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

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

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

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