• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
        • Bip32
          • Bip32-wallet-structure
          • Bip32-key-trees
          • Bip32-key-serialization
            • Bip32-export-key
            • Bip32-deserialize-key
            • Bip32-serialize-key
            • Bip32-serialized-key-p
            • Bip32-import-key
            • Bip32-key-identifier
            • Bip32-serialization-versions
            • Bip32-key-fingerprint
          • Bip32-key-derivation
          • Bip32-executable-attachments
          • Bip32-extended-keys
          • Bip32-master-key-generation
        • Bech32
        • Bip39
        • Bip44
        • Base58
        • Bip43
        • Bytes
        • Base58check
        • Cryptography
        • Bip-350
        • Bip-173
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Bip32-key-serialization

Bip32-import-key

Import a key into a tree.

Signature

(bip32-import-key bytes) → (mv error? tree mainnet?)

Arguments

bytes — Guard (byte-listp bytes).

Returns

error? — Type (booleanp error?).

tree — Type (bip32-key-treep tree).

mainnet? — Type (booleanp mainnet?).

We deserialize the key into its components, which we use to construct a singleton key tree that contains just that key.

The boolean flag that distinguishes mainnet from testnet, returned by serialization, is not used to construct the tree. We return this flag as an additional result.

If deserialization fails, the first result is t, which signals an error. In this case, the second and third results are irrelevant.

Definitions and Theorems

Function: bip32-import-key

(defun bip32-import-key (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (b* (((mv error? key depth index parent mainnet?)
        (bip32-deserialize-key bytes))
       (tree (bip32-key-tree key depth index parent '(nil))))
    (mv error? tree mainnet?)))

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

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

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

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

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

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

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

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

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

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