		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-trees

Bip32-ckd*

Key designated by a specified path in the tree with the specified root key.

Signature
(bip32-ckd* root path) → (mv error? key)
Arguments: root — Guard (bip32-ext-key-p root).; path — Guard (ubyte32-listp path).
Returns: error? — Type (booleanp error?).; key — Type (bip32-ext-key-p key).

Definitions and Theorems

Function: bip32-ckd*

(defun bip32-ckd* (root path)
  (declare (xargs :guard (and (bip32-ext-key-p root)
                              (ubyte32-listp path))))
  (bip32-ext-key-case root :priv
                      (b* (((mv error? key)
                            (bip32-ckd-priv* root.get path)))
                        (mv error? (bip32-ext-key-priv key)))
                      :pub
                      (b* (((mv error? key)
                            (bip32-ckd-pub* root.get path)))
                        (mv error? (bip32-ext-key-pub key)))))

Theorem: booleanp-of-bip32-ckd*.error?

(defthm booleanp-of-bip32-ckd*.error?
  (b* (((mv ?error? ?key)
        (bip32-ckd* root path)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bip32-ext-key-p-of-bip32-ckd*.key

(defthm bip32-ext-key-p-of-bip32-ckd*.key
  (b* (((mv ?error? ?key)
        (bip32-ckd* root path)))
    (bip32-ext-key-p key))
  :rule-classes :rewrite)

Theorem: bip32-ext-key-kind-of-bip32-ckd*

(defthm bip32-ext-key-kind-of-bip32-ckd*
  (equal (bip32-ext-key-kind (mv-nth 1 (bip32-ckd* root path)))
         (bip32-ext-key-kind root)))

Theorem: bip32-ckd*-of-bip32-ext-key-fix-root

(defthm bip32-ckd*-of-bip32-ext-key-fix-root
  (equal (bip32-ckd* (bip32-ext-key-fix root)
                     path)
         (bip32-ckd* root path)))

Theorem: bip32-ckd*-bip32-ext-key-equiv-congruence-on-root

(defthm bip32-ckd*-bip32-ext-key-equiv-congruence-on-root
  (implies (bip32-ext-key-equiv root root-equiv)
           (equal (bip32-ckd* root path)
                  (bip32-ckd* root-equiv path)))
  :rule-classes :congruence)

Theorem: bip32-ckd*-of-ubyte32-list-fix-path

(defthm bip32-ckd*-of-ubyte32-list-fix-path
  (equal (bip32-ckd* root (ubyte32-list-fix path))
         (bip32-ckd* root path)))

Theorem: bip32-ckd*-ubyte32-list-equiv-congruence-on-path

(defthm bip32-ckd*-ubyte32-list-equiv-congruence-on-path
  (implies (acl2::ubyte32-list-equiv path path-equiv)
           (equal (bip32-ckd* root path)
                  (bip32-ckd* root path-equiv)))
  :rule-classes :congruence)