		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-trees

Bip32-path-in-tree-p

Check if a path designates a key in a key tree.

Signature
(bip32-path-in-tree-p path tree) → yes/no
Arguments: path — Guard (ubyte32-listp path).; tree — Guard (bip32-key-treep tree).
Returns: yes/no — Type (booleanp yes/no).

The empty path always designates a key: the one at the root.

If a path designates a key, every prefix of it (taken with take) also designates an (ancestor) key.

If a path designates a key, that key can be successfully derived from the root.

If a path designates a key, the total depth of that key (including the root's depth) does not exceed 255.

Definitions and Theorems

Function: bip32-path-in-tree-p

(defun bip32-path-in-tree-p (path tree)
       (declare (xargs :guard (and (ubyte32-listp path)
                                   (bip32-key-treep tree))))
       (b* ((path (mbe :logic (ubyte32-list-fix path)
                       :exec path)))
           (in path
               (bip32-key-tree->index-tree tree))))

Theorem: booleanp-of-bip32-path-in-tree-p

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

Theorem: bip32-path-in-tree-p-of-nil

(defthm bip32-path-in-tree-p-of-nil
        (implies (bip32-key-treep tree)
                 (bip32-path-in-tree-p nil tree)))

Theorem: bip32-path-in-tree-p-of-take

(defthm bip32-path-in-tree-p-of-take
        (implies (and (bip32-key-treep tree)
                      (bip32-path-in-tree-p path tree)
                      (<= (nfix n) (len path)))
                 (bip32-path-in-tree-p (take n path)
                                       tree)))

Theorem: valid-key-when-bip32-path-in-tree-p

(defthm
   valid-key-when-bip32-path-in-tree-p
   (implies (and (bip32-key-treep tree)
                 (bip32-path-in-tree-p path tree))
            (not (mv-nth 0
                         (bip32-ckd* (bip32-key-tree->root-key tree)
                                     path)))))

Theorem: valid-depth-when-bip32-path-in-tree-p

(defthm valid-depth-when-bip32-path-in-tree-p
        (implies (and (bip32-key-treep tree)
                      (bip32-path-in-tree-p path tree))
                 (bytep (+ (bip32-key-tree->root-depth tree)
                           (len path)))))

Theorem: bip32-path-in-tree-p-of-ubyte32-list-fix-path

(defthm bip32-path-in-tree-p-of-ubyte32-list-fix-path
        (equal (bip32-path-in-tree-p (ubyte32-list-fix path)
                                     tree)
               (bip32-path-in-tree-p path tree)))

Theorem: bip32-path-in-tree-p-ubyte32-list-equiv-congruence-on-path

(defthm bip32-path-in-tree-p-ubyte32-list-equiv-congruence-on-path
        (implies (acl2::ubyte32-list-equiv path path-equiv)
                 (equal (bip32-path-in-tree-p path tree)
                        (bip32-path-in-tree-p path-equiv tree)))
        :rule-classes :congruence)

Theorem: bip32-path-in-tree-p-of-bip32-key-tree-fix-tree

(defthm bip32-path-in-tree-p-of-bip32-key-tree-fix-tree
        (equal (bip32-path-in-tree-p path (bip32-key-tree-fix tree))
               (bip32-path-in-tree-p path tree)))

Theorem: bip32-path-in-tree-p-bip32-key-tree-equiv-congruence-on-tree

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