		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-serialization

Bip32-serialize-key

Serialize an extended key.

Signature
(bip32-serialize-key key depth index parent mainnet?) → bytes
Arguments: key — Guard (bip32-ext-key-p key).; depth — Guard (bytep depth).; index — Guard (ubyte32p index).; parent — Guard (and (byte-listp parent) (equal (len parent) 4)).; mainnet? — Guard (booleanp mainnet?).
Returns: bytes — Type (byte-listp bytes).

Besides the key, from which chain code and key data are obtained, this function takes additional arguments necessary for a complete serialization as specified in [BIP32].

If the depth is 0, this is the master key and thus the child number and the parent's fingerprint must be 0 too [BIP32]. This is expressed by the guard.

A boolean argument says whether the key is being serialized for the mainnet (if t) or for the testnet (if nil).

Definitions and Theorems

Function: bip32-serialize-key

(defun bip32-serialize-key (key depth index parent mainnet?)
 (declare (xargs :guard (and (bip32-ext-key-p key)
                             (bytep depth)
                             (ubyte32p index)
                             (and (byte-listp parent)
                                  (equal (len parent) 4))
                             (booleanp mainnet?))))
 (declare
      (xargs :guard (implies (equal depth 0)
                             (and (equal index 0)
                                  (equal parent (list 0 0 0 0))))))
 (b*
  ((depth (mbe :logic (byte-fix depth)
               :exec depth))
   (index (mbe :logic (ubyte32-fix index)
               :exec index))
   (parent (mbe :logic (byte-list-fix parent)
                :exec parent))
   (parent (mbe :logic
                (if (= (len parent) 4)
                    parent
                  (list 0 0 0 0))
                :exec parent))
   ((mv key-data chain-code version)
    (bip32-ext-key-case
      key
      :priv
      (mv (cons 0
                (nat=>bebytes 32 (bip32-ext-priv-key->key key.get)))
          (bip32-ext-priv-key->chain-code key.get)
          (if mainnet? *bip32-version-priv-main*
            *bip32-version-priv-test*))
      :pub
      (mv (secp256k1-point-to-bytes (bip32-ext-pub-key->key key.get)
                                    t)
          (bip32-ext-pub-key->chain-code key.get)
          (if mainnet? *bip32-version-pub-main*
            *bip32-version-pub-test*)))))
  (append (nat=>bebytes 4 version)
          (list depth)
          parent (nat=>bebytes 4 index)
          chain-code key-data)))

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

(defthm byte-listp-of-bip32-serialize-key
 (b* ((bytes (bip32-serialize-key key depth index parent mainnet?)))
   (byte-listp bytes))
 :rule-classes :rewrite)

Theorem: len-of-bip32-serialize-key

(defthm len-of-bip32-serialize-key
 (b* ((bytes (bip32-serialize-key key depth index parent mainnet?)))
   (equal (len bytes) 78))
 :rule-classes :rewrite)

Theorem: bip32-serialize-key-of-bip32-ext-key-fix-key

(defthm bip32-serialize-key-of-bip32-ext-key-fix-key
  (equal (bip32-serialize-key (bip32-ext-key-fix key)
                              depth index parent mainnet?)
         (bip32-serialize-key key depth index parent mainnet?)))

Theorem: bip32-serialize-key-bip32-ext-key-equiv-congruence-on-key

(defthm bip32-serialize-key-bip32-ext-key-equiv-congruence-on-key
 (implies
  (bip32-ext-key-equiv key key-equiv)
  (equal
       (bip32-serialize-key key depth index parent mainnet?)
       (bip32-serialize-key key-equiv depth index parent mainnet?)))
 :rule-classes :congruence)

Theorem: bip32-serialize-key-of-byte-fix-depth

(defthm bip32-serialize-key-of-byte-fix-depth
  (equal (bip32-serialize-key key (byte-fix depth)
                              index parent mainnet?)
         (bip32-serialize-key key depth index parent mainnet?)))

Theorem: bip32-serialize-key-byte-equiv-congruence-on-depth

(defthm bip32-serialize-key-byte-equiv-congruence-on-depth
 (implies
  (acl2::byte-equiv depth depth-equiv)
  (equal
       (bip32-serialize-key key depth index parent mainnet?)
       (bip32-serialize-key key depth-equiv index parent mainnet?)))
 :rule-classes :congruence)

Theorem: bip32-serialize-key-of-ubyte32-fix-index

(defthm bip32-serialize-key-of-ubyte32-fix-index
  (equal (bip32-serialize-key key depth (ubyte32-fix index)
                              parent mainnet?)
         (bip32-serialize-key key depth index parent mainnet?)))

Theorem: bip32-serialize-key-ubyte32-equiv-congruence-on-index

(defthm bip32-serialize-key-ubyte32-equiv-congruence-on-index
 (implies
  (acl2::ubyte32-equiv index index-equiv)
  (equal
       (bip32-serialize-key key depth index parent mainnet?)
       (bip32-serialize-key key depth index-equiv parent mainnet?)))
 :rule-classes :congruence)

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

(defthm bip32-serialize-key-of-bool-fix-mainnet?
 (equal (bip32-serialize-key key depth
                             index parent (acl2::bool-fix mainnet?))
        (bip32-serialize-key key depth index parent mainnet?)))

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

(defthm bip32-serialize-key-iff-congruence-on-mainnet?
 (implies
  (iff mainnet? mainnet?-equiv)
  (equal
       (bip32-serialize-key key depth index parent mainnet?)
       (bip32-serialize-key key depth index parent mainnet?-equiv)))
 :rule-classes :congruence)