• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
          • Bip32
            • Bip32-wallet-structure
            • Bip32-key-trees
            • Bip32-key-serialization
            • Bip32-key-derivation
            • Bip32-executable-attachments
            • Bip32-extended-keys
            • Bip32-master-key-generation
              • Bip32-master-key
              • Bip32-master-tree
            • 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
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Bip32-master-key-generation

    Bip32-master-tree

    Generate a key tree with (just) a master key from a seed.

    Signature
    (bip32-master-tree seed) → (mv error? tree)
    Arguments
    seed — Guard (byte-listp seed).
    Returns
    error? — Type (booleanp error?).
    tree — Type (bip32-key-treep tree).

    This lifts bip32-master-key from a single key to a singleton tree containing the key at the root, as a master key.

    Definitions and Theorems

    Function: bip32-master-tree

    (defun bip32-master-tree (seed)
      (declare (xargs :guard (byte-listp seed)))
      (declare (xargs :guard (and (<= 16 (len seed))
                                  (<= (len seed) 64))))
      (b* (((mv error? key)
            (bip32-master-key seed))
           (tree (bip32-key-tree (bip32-ext-key-priv key)
                                 0 0 (list 0 0 0 0)
                                 '(nil))))
        (mv error? tree)))

    Theorem: booleanp-of-bip32-master-tree.error?

    (defthm booleanp-of-bip32-master-tree.error?
      (b* (((mv ?error? ?tree)
            (bip32-master-tree seed)))
        (booleanp error?))
      :rule-classes :rewrite)

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

    (defthm bip32-key-treep-of-bip32-master-tree.tree
      (b* (((mv ?error? ?tree)
            (bip32-master-tree seed)))
        (bip32-key-treep tree))
      :rule-classes :rewrite)

    Theorem: bip32-key-tree->root-key-of-bip32-master-tree

    (defthm bip32-key-tree->root-key-of-bip32-master-tree
     (equal
          (bip32-key-tree->root-key (mv-nth 1 (bip32-master-tree seed)))
          (bip32-ext-key-priv (mv-nth 1 (bip32-master-key seed)))))

    Theorem: bip32-key-tree->root-depth-of-bip32-master-tree

    (defthm bip32-key-tree->root-depth-of-bip32-master-tree
     (equal
        (bip32-key-tree->root-depth (mv-nth 1 (bip32-master-tree seed)))
        0))

    Theorem: bip32-key-tree->root-index-of-bip32-master-tree

    (defthm bip32-key-tree->root-index-of-bip32-master-tree
     (equal
        (bip32-key-tree->root-index (mv-nth 1 (bip32-master-tree seed)))
        0))

    Theorem: bip32-key-tree->root-parent-of-bip32-master-tree

    (defthm bip32-key-tree->root-parent-of-bip32-master-tree
     (equal
       (bip32-key-tree->root-parent (mv-nth 1 (bip32-master-tree seed)))
       (list 0 0 0 0)))

    Theorem: bip32-key-tree->index-tree-of-bip32-master-tree

    (defthm bip32-key-tree->index-tree-of-bip32-master-tree
     (equal
        (bip32-key-tree->index-tree (mv-nth 1 (bip32-master-tree seed)))
        (list nil)))

    Theorem: bip32-key-tree-priv-p-of-bip32-master-tree

    (defthm bip32-key-tree-priv-p-of-bip32-master-tree
      (bip32-key-tree-priv-p (mv-nth 1 (bip32-master-tree seed))))

    Theorem: bip32-master-tree-of-byte-list-fix-seed

    (defthm bip32-master-tree-of-byte-list-fix-seed
      (equal (bip32-master-tree (byte-list-fix seed))
             (bip32-master-tree seed)))

    Theorem: bip32-master-tree-byte-list-equiv-congruence-on-seed

    (defthm bip32-master-tree-byte-list-equiv-congruence-on-seed
      (implies (byte-list-equiv seed seed-equiv)
               (equal (bip32-master-tree seed)
                      (bip32-master-tree seed-equiv)))
      :rule-classes :congruence)