		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)