		Search-engine friendly clone of the ACL2 documentation.

Bip32-wallet-structure

Bip32-compliant-depth-p

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

According to the figure in [BIP32], the key tree stops at depth 3, 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 4.

Definitions and Theorems

Theorem: bip32-compliant-depth-p-necc

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

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

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

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

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

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

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