		Search-engine friendly clone of the ACL2 documentation.

Bip43

Bip43-import-key

BIP 43 key import.

Signature
(bip43-import-key bytes) → (mv error? tree)
Arguments: bytes — Guard (byte-listp bytes).
Returns: error? — Type (booleanp error?).; tree — Type (bip32-key-treep tree).

[BIP43] prescribes that BIP 32 key serialization be always done with the version numbers of the mainnet, i.e. *bip32-version-priv-main* and *bip32-version-pub-main*.

This function calls bip32-import-key and ensures that the serialized key was for the mainnet.

Definitions and Theorems

Function: bip43-import-key

(defun bip43-import-key (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (b* (((mv error? tree mainnet?)
        (bip32-import-key bytes))
       ((when error?) (mv t tree))
       ((unless mainnet?) (mv t tree)))
    (mv nil tree)))

Theorem: booleanp-of-bip43-import-key.error?

(defthm booleanp-of-bip43-import-key.error?
  (b* (((mv ?error? ?tree)
        (bip43-import-key bytes)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bip32-key-treep-of-bip43-import-key.tree

(defthm bip32-key-treep-of-bip43-import-key.tree
  (b* (((mv ?error? ?tree)
        (bip43-import-key bytes)))
    (bip32-key-treep tree))
  :rule-classes :rewrite)

Theorem: bip43-import-key-of-byte-list-fix-bytes

(defthm bip43-import-key-of-byte-list-fix-bytes
  (equal (bip43-import-key (byte-list-fix bytes))
         (bip43-import-key bytes)))

Theorem: bip43-import-key-byte-list-equiv-congruence-on-bytes

(defthm bip43-import-key-byte-list-equiv-congruence-on-bytes
  (implies (byte-list-equiv bytes bytes-equiv)
           (equal (bip43-import-key bytes)
                  (bip43-import-key bytes-equiv)))
  :rule-classes :congruence)