		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-serialization

Bip32-export-key

Export a key from a tree.

Signature
(bip32-export-key tree path mainnet? public?) → exported
Arguments: tree — Guard (bip32-key-treep tree).; path — Guard (ubyte32-listp path).; mainnet? — Guard (booleanp mainnet?).; public? — Guard (booleanp public?).
Returns: exported — Type (byte-listp exported).

The key to export is designated by a path, which must be a valid path in the tree.

A boolean argument specifies whether the key is for the mainnet or for the testnet.

Another boolean argument specified whether the key should be public. If this is nil, then the tree must consist of private keys, as expressed by the guard. If this is t instead, the tree may consist of private or public keys; if it consists of private keys, we use bip32-n to turn the extended private key at the path into the corresponding extended public key, prior to serializing it.

We first derive the key at the path from the root, via bip32-ckd*. Since the key tree satisfies bip32-valid-keys-p and the path is in the tree, this never returns an error, as proved via mbt below.

We calculate the total depth of the key by adding the length of the path to the root's depth. Since the key tree satisfies bip32-valid-depths-p and the path is in the tree, this never exceeds 255 (i.e. always fits in a byte), as proved via mbt below.

The index of the key is the last element of the path if the path is not empty. Otherwise, it is the index of the root.

The parent key's fingerprint is calculated from the parent key if the path is not empty. The path of the parent is obtained by removing the last element from the path of the key: since this is also a path in the tree, the call of bip32-ckd* on the parent's path does not return an error either, as proved via mbt below. Otherwise, if the path is empty, we obtain the parent's fingerprint from the root of the tree.

With all the above pieces of data in hand, we serialize the key, completing the export.

Definitions and Theorems

Function: bip32-export-key

(defun bip32-export-key (tree path mainnet? public?)
 (declare (xargs :guard (and (bip32-key-treep tree)
                             (ubyte32-listp path)
                             (booleanp mainnet?)
                             (booleanp public?))))
 (declare
     (xargs :guard (and (bip32-path-in-tree-p path tree)
                        (or public? (bip32-key-tree-priv-p tree)))))
 (b*
  ((path (mbe :logic (ubyte32-list-fix path)
              :exec path))
   ((bip32-key-tree tree) tree)
   ((mv error? key)
    (bip32-ckd* tree.root-key path))
   ((unless (mbt (not error?))) nil)
   (key
     (if (and public? (bip32-key-tree-priv-p tree))
         (bip32-ext-key-pub (bip32-n (bip32-ext-key-priv->get key)))
       key))
   (depth (+ tree.root-depth (len path)))
   ((unless (mbt (bytep depth))) nil)
   (index (if (consp path)
              (car (last path))
            tree.root-index))
   (parent (if (consp path)
               (b* ((parent-path (butlast path 1))
                    ((mv error? parent-key)
                     (bip32-ckd* tree.root-key parent-path))
                    ((unless (mbt (not error?))) nil))
                 (bip32-key-fingerprint parent-key))
             tree.root-parent)))
  (bip32-serialize-key key depth index parent mainnet?)))

Theorem: byte-listp-of-bip32-export-key

(defthm byte-listp-of-bip32-export-key
  (b* ((exported (bip32-export-key tree path mainnet? public?)))
    (byte-listp exported))
  :rule-classes :rewrite)

Theorem: bip32-export-key-of-bip32-key-tree-fix-tree

(defthm bip32-export-key-of-bip32-key-tree-fix-tree
  (equal (bip32-export-key (bip32-key-tree-fix tree)
                           path mainnet? public?)
         (bip32-export-key tree path mainnet? public?)))

Theorem: bip32-export-key-bip32-key-tree-equiv-congruence-on-tree

(defthm bip32-export-key-bip32-key-tree-equiv-congruence-on-tree
  (implies
       (bip32-key-tree-equiv tree tree-equiv)
       (equal (bip32-export-key tree path mainnet? public?)
              (bip32-export-key tree-equiv path mainnet? public?)))
  :rule-classes :congruence)

Theorem: bip32-export-key-of-ubyte32-list-fix-path

(defthm bip32-export-key-of-ubyte32-list-fix-path
  (equal (bip32-export-key tree (ubyte32-list-fix path)
                           mainnet? public?)
         (bip32-export-key tree path mainnet? public?)))

Theorem: bip32-export-key-ubyte32-list-equiv-congruence-on-path

(defthm bip32-export-key-ubyte32-list-equiv-congruence-on-path
  (implies
       (acl2::ubyte32-list-equiv path path-equiv)
       (equal (bip32-export-key tree path mainnet? public?)
              (bip32-export-key tree path-equiv mainnet? public?)))
  :rule-classes :congruence)

Theorem: bip32-export-key-of-bool-fix-mainnet?

(defthm bip32-export-key-of-bool-fix-mainnet?
  (equal (bip32-export-key tree path (acl2::bool-fix mainnet?)
                           public?)
         (bip32-export-key tree path mainnet? public?)))

Theorem: bip32-export-key-iff-congruence-on-mainnet?

(defthm bip32-export-key-iff-congruence-on-mainnet?
  (implies
       (iff mainnet? mainnet?-equiv)
       (equal (bip32-export-key tree path mainnet? public?)
              (bip32-export-key tree path mainnet?-equiv public?)))
  :rule-classes :congruence)

Theorem: bip32-export-key-of-bool-fix-public?

(defthm bip32-export-key-of-bool-fix-public?
  (equal (bip32-export-key tree
                           path mainnet? (acl2::bool-fix public?))
         (bip32-export-key tree path mainnet? public?)))

Theorem: bip32-export-key-iff-congruence-on-public?

(defthm bip32-export-key-iff-congruence-on-public?
  (implies
       (iff public? public?-equiv)
       (equal (bip32-export-key tree path mainnet? public?)
              (bip32-export-key tree path mainnet? public?-equiv)))
  :rule-classes :congruence)