		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-serialization

Bip32-serialized-key-p

Check if a sequence of bytes is a serialized extended key.

This is a declarative, non-executable definition, which essentially characterizes the image of bip32-serialize-key over arguments that satisfy that function's guard.

By definition, the witness function is the right inverse of bip32-serialize-key, over valid serialized keys.

Definitions and Theorems

Theorem: bip32-serialized-key-p-suff

(defthm bip32-serialized-key-p-suff
 (implies
   (and (bip32-ext-key-p key)
        (bytep depth)
        (ubyte32p index)
        (byte-listp parent)
        (equal (len parent) 4)
        (booleanp mainnet?)
        (if (equal depth 0)
            (if (and (equal index 0)
                     (equal parent (list 0 0 0 0)))
                t
              nil)
          t)
        (equal (bip32-serialize-key key depth index parent mainnet?)
               (byte-list-fix bytes)))
   (bip32-serialized-key-p bytes)))

Theorem: booleanp-of-bip32-serialized-key-p

(defthm booleanp-of-bip32-serialized-key-p
  (b* ((yes/no (bip32-serialized-key-p bytes)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: bip32-serialized-key-p-of-byte-list-fix-bytes

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

Theorem: bip32-serialized-key-p-byte-list-equiv-congruence-on-bytes

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

Theorem: bip32-ext-key-p-of-mv-nth-0-of-bip32-serialized-key-witness

(defthm bip32-ext-key-p-of-mv-nth-0-of-bip32-serialized-key-witness
 (implies
   (bip32-serialized-key-p bytes)
   (bip32-ext-key-p (mv-nth 0
                            (bip32-serialized-key-witness bytes)))))

Theorem: bytep-of-mv-nth-1-of-bip32-serialized-key-witness

(defthm bytep-of-mv-nth-1-of-bip32-serialized-key-witness
  (implies (bip32-serialized-key-p bytes)
           (bytep (mv-nth 1
                          (bip32-serialized-key-witness bytes)))))

Theorem: ubyte32p-of-mv-nth-2-of-bip32-serialized-key-witness

(defthm ubyte32p-of-mv-nth-2-of-bip32-serialized-key-witness
 (implies (bip32-serialized-key-p bytes)
          (ubyte32p (mv-nth 2
                            (bip32-serialized-key-witness bytes)))))

Theorem: byte-listp-of-mv-nth-3-of-bip32-serialized-key-witness

(defthm byte-listp-of-mv-nth-3-of-bip32-serialized-key-witness
  (implies
       (bip32-serialized-key-p bytes)
       (byte-listp (mv-nth 3
                           (bip32-serialized-key-witness bytes)))))

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

(defthm len-of-mv-nth-3-of-bip32-serialize-key-witness
  (implies
       (bip32-serialized-key-p bytes)
       (equal (len (mv-nth 3 (bip32-serialized-key-witness bytes)))
              4)))

Theorem: booleanp-of-mv-nth-4-of-bip32-serialized-key-witness

(defthm booleanp-of-mv-nth-4-of-bip32-serialized-key-witness
 (implies (bip32-serialized-key-p bytes)
          (booleanp (mv-nth 4
                            (bip32-serialized-key-witness bytes)))))

Theorem: depth-index-parent-constraint-of-bip32-serialized-key-witness

(defthm
      depth-index-parent-constraint-of-bip32-serialized-key-witness
  (implies
       (and (bip32-serialized-key-p bytes)
            (equal (mv-nth 1 (bip32-serialized-key-witness bytes))
                   0))
       (and (equal (mv-nth 2 (bip32-serialized-key-witness bytes))
                   0)
            (equal (mv-nth 3 (bip32-serialized-key-witness bytes))
                   (list 0 0 0 0)))))

Theorem: bip32-serialize-key-of-bip32-serialized-key-witness

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

Theorem: bip32-serialized-key-p-of-bip32-serialize-key

(defthm bip32-serialized-key-p-of-bip32-serialize-key
  (implies
       (and (bip32-ext-key-p key)
            (bytep depth)
            (ubyte32p index)
            (byte-listp parent)
            (equal (len parent) 4)
            (booleanp mainnet?)
            (implies (equal depth 0)
                     (and (equal index 0)
                          (equal parent (list 0 0 0 0)))))
       (bip32-serialized-key-p
            (bip32-serialize-key key depth index parent mainnet?))))