		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-serialization

Bip32-deserialize-key

Deserialize an extended key.

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

This is declaratively specified as the inverse of serialization.

The first result is t if the input bytes are not a serialized key; in this case, the other results are irrelevant. Otherwise, the first result is nil (i.e. no error) and the constituents of the the serialized key are returned; these correspond to the inputs of bip32-serialize-key.

We prove that deserialization is the right inverse of serialization. To prove that it is also left inverse, we need to prove the injectivity of serialization first. This will be done soon.

Definitions and Theorems

Function: bip32-deserialize-key

(defun bip32-deserialize-key (bytes)
 (declare (xargs :guard (byte-listp bytes)))
 (b* ((bytes (byte-list-fix bytes)))
  (if (bip32-serialized-key-p bytes)
      (b* (((mv key depth index parent mainnet?)
            (bip32-serialized-key-witness bytes)))
        (mv nil key depth index parent mainnet?))
   (b*
    ((irrelevant-key
         (bip32-ext-key-priv (bip32-ext-priv-key 1 (repeat 32 0)))))
    (mv t irrelevant-key 0 0 (list 0 0 0 0)
        nil)))))

Theorem: booleanp-of-bip32-deserialize-key.error?

(defthm booleanp-of-bip32-deserialize-key.error?
  (b* (((mv ?error?
            ?key ?depth ?index ?parent ?mainnet?)
        (bip32-deserialize-key bytes)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bip32-ext-key-p-of-bip32-deserialize-key.key

(defthm bip32-ext-key-p-of-bip32-deserialize-key.key
  (b* (((mv ?error?
            ?key ?depth ?index ?parent ?mainnet?)
        (bip32-deserialize-key bytes)))
    (bip32-ext-key-p key))
  :rule-classes :rewrite)

Theorem: bytep-of-bip32-deserialize-key.depth

(defthm bytep-of-bip32-deserialize-key.depth
  (b* (((mv ?error?
            ?key ?depth ?index ?parent ?mainnet?)
        (bip32-deserialize-key bytes)))
    (bytep depth))
  :rule-classes :rewrite)

Theorem: ubyte32p-of-bip32-deserialize-key.index

(defthm ubyte32p-of-bip32-deserialize-key.index
  (b* (((mv ?error?
            ?key ?depth ?index ?parent ?mainnet?)
        (bip32-deserialize-key bytes)))
    (ubyte32p index))
  :rule-classes :rewrite)

Theorem: return-type-of-bip32-deserialize-key.parent

(defthm return-type-of-bip32-deserialize-key.parent
  (b* (((mv ?error?
            ?key ?depth ?index ?parent ?mainnet?)
        (bip32-deserialize-key bytes)))
    (and (byte-listp parent)
         (equal (len parent) 4)))
  :rule-classes :rewrite)

Theorem: booleanp-of-bip32-deserialize-key.mainnet?

(defthm booleanp-of-bip32-deserialize-key.mainnet?
  (b* (((mv ?error?
            ?key ?depth ?index ?parent ?mainnet?)
        (bip32-deserialize-key bytes)))
    (booleanp mainnet?))
  :rule-classes :rewrite)

Theorem: not-mv-nth-0-of-bip32-deserialize-key-when-bip32-serialized-key-p

(defthm
  not-mv-nth-0-of-bip32-deserialize-key-when-bip32-serialized-key-p
  (implies (bip32-serialized-key-p bytes)
           (not (mv-nth 0 (bip32-deserialize-key bytes)))))

Theorem: bip32-ext-key-p-of-mv-nth-1-of-bip32-deserialize-key

(defthm bip32-ext-key-p-of-mv-nth-1-of-bip32-deserialize-key
  (bip32-ext-key-p (mv-nth 1 (bip32-deserialize-key bytes))))

Theorem: bytep-of-mv-nth-2-of-bip32-deserialize-key

(defthm bytep-of-mv-nth-2-of-bip32-deserialize-key
  (bytep (mv-nth 2 (bip32-deserialize-key bytes))))

Theorem: ubyte32p-of-mv-nth-3-of-bip32-deserialize-key

(defthm ubyte32p-of-mv-nth-3-of-bip32-deserialize-key
  (ubyte32p (mv-nth 3 (bip32-deserialize-key bytes))))

Theorem: byte-listp-of-mv-nth-4-of-bip32-deserialize-key

(defthm byte-listp-of-mv-nth-4-of-bip32-deserialize-key
  (byte-listp (mv-nth 4 (bip32-deserialize-key bytes))))

Theorem: len-of-mv-nth-4-of-bip32-serialize-key-witness

(defthm len-of-mv-nth-4-of-bip32-serialize-key-witness
  (equal (len (mv-nth 4 (bip32-deserialize-key bytes)))
         4))

Theorem: booleanp-of-mv-nth-5-of-bip32-deserialize-key

(defthm booleanp-of-mv-nth-5-of-bip32-deserialize-key
  (booleanp (mv-nth 5 (bip32-deserialize-key bytes))))

Theorem: depth-index-parent-constraint-of-bip32-deserialize-key

(defthm depth-index-parent-constraint-of-bip32-deserialize-key
  (implies (equal (mv-nth 2 (bip32-deserialize-key bytes))
                  0)
           (and (equal (mv-nth 3 (bip32-deserialize-key bytes))
                       0)
                (equal (mv-nth 4 (bip32-deserialize-key bytes))
                       (list 0 0 0 0)))))

Theorem: bip32-serialize-key-of-bip32-deserialize-key

(defthm bip32-serialize-key-of-bip32-deserialize-key
 (implies
  (bip32-serialized-key-p bytes)
  (b* (((mv error? key depth index parent mainnet?)
        (bip32-deserialize-key bytes)))
   (and (not error?)
        (equal (bip32-serialize-key key depth index parent mainnet?)
               (byte-list-fix bytes))))))

Theorem: bip32-deserialize-key-of-byte-list-fix-bytes

(defthm bip32-deserialize-key-of-byte-list-fix-bytes
  (equal (bip32-deserialize-key (byte-list-fix bytes))
         (bip32-deserialize-key bytes)))

Theorem: bip32-deserialize-key-byte-list-equiv-congruence-on-bytes

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