• 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-extend-tree
            • Bip32-valid-depths-p
            • Bip32-key-tree
            • Bip32-path-set-closedp
            • Bip32-valid-keys-p
            • Bip32-index-tree
            • Bip32-path-in-tree-p
            • Bip32-ckd*
            • Bip32-get-pub-key-at-path
            • Bip32-get-priv-key-at-path
            • Bip32-ckd-priv*
            • Bip32-ckd-pub*
            • Bip32-path
            • Bip32-key-tree-priv-p
            • Bip32-path-set
          • Bip32-key-serialization
          • 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-trees

Bip32-extend-tree

Extend a key tree with a key.

Signature

(bip32-extend-tree tree parent-path child-index) 
  → 
(mv error? new-tree)

Arguments

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

parent-path — Guard (ubyte32-listp parent-path).

child-index — Guard (ubyte32p child-index).

Returns

error? — Type (booleanp error?).

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

The new key is identified by (i) the path of its parent and (ii) the child index of the new key. The parent must be already in the tree, while the new child key must not: this is expressed by the guard of this function. The total depth of the new key should not exceed 255: this is also expressed by the guard.

Given our model of key trees, we just add the path of the new key to the underlying index tree. But we need to check whether the child key derivation fails: if it does, we return the input key tree unchanged, along with t as the first result. The first result is nil if key derivation succeeds.

If the key tree consists of private keys, the new key is private. If the key tree consists of public keys, the new key is public. We uniformly use the bip32-ckd function.

Definitions and Theorems

Function: bip32-extend-tree

(defun bip32-extend-tree (tree parent-path child-index)
 (declare (xargs :guard (and (bip32-key-treep tree)
                             (ubyte32-listp parent-path)
                             (ubyte32p child-index))))
 (declare
  (xargs
     :guard
     (and (bip32-path-in-tree-p parent-path tree)
          (not (bip32-path-in-tree-p (rcons child-index parent-path)
                                     tree))
          (< (+ (bip32-key-tree->root-depth tree)
                (len parent-path))
             255))))
 (b* ((tree (mbe :logic (bip32-key-tree-fix tree)
                 :exec tree))
      (parent-path (mbe :logic (ubyte32-list-fix parent-path)
                        :exec parent-path))
      (child-index (mbe :logic (ubyte32-fix child-index)
                        :exec child-index))
      ((bip32-key-tree tree) tree)
      ((unless (mbt (bip32-path-in-tree-p parent-path tree)))
       (mv t tree))
      (new-path (rcons child-index parent-path))
      ((unless (mbt (not (bip32-path-in-tree-p new-path tree))))
       (mv t tree))
      ((unless (mbt (< (+ tree.root-depth (len parent-path))
                       255)))
       (mv t tree))
      ((mv error? &)
       (bip32-ckd* tree.root-key new-path))
      ((when error?) (mv error? tree))
      (new-index-tree (insert new-path tree.index-tree))
      (new-tree (change-bip32-key-tree tree
                                       :index-tree new-index-tree)))
   (mv nil new-tree)))

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

(defthm booleanp-of-bip32-extend-tree.error?
  (b* (((mv ?error? ?new-tree)
        (bip32-extend-tree tree parent-path child-index)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bip32-key-treep-of-bip32-extend-tree.new-tree

(defthm bip32-key-treep-of-bip32-extend-tree.new-tree
  (b* (((mv ?error? ?new-tree)
        (bip32-extend-tree tree parent-path child-index)))
    (bip32-key-treep new-tree))
  :rule-classes :rewrite)

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

(defthm bip32-key-tree->root-key-of-bip32-extend-tree
 (equal
     (bip32-key-tree->root-key
          (mv-nth 1
                  (bip32-extend-tree tree parent-path child-index)))
     (bip32-key-tree->root-key tree)))

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

(defthm bip32-key-tree->root-depth-of-bip32-extend-tree
 (equal
     (bip32-key-tree->root-depth
          (mv-nth 1
                  (bip32-extend-tree tree parent-path child-index)))
     (bip32-key-tree->root-depth tree)))

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

(defthm bip32-key-tree->root-index-of-bip32-extend-tree
 (equal
     (bip32-key-tree->root-index
          (mv-nth 1
                  (bip32-extend-tree tree parent-path child-index)))
     (bip32-key-tree->root-index tree)))

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

(defthm bip32-key-tree->root-parent-of-bip32-extend-tree
 (equal
     (bip32-key-tree->root-parent
          (mv-nth 1
                  (bip32-extend-tree tree parent-path child-index)))
     (bip32-key-tree->root-parent tree)))

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

(defthm bip32-key-tree->index-tree-of-bip32-extend-tree
  (b* (((mv error? tree1)
        (bip32-extend-tree tree parent-path child-index)))
    (equal (bip32-key-tree->index-tree tree1)
           (if error? (bip32-key-tree->index-tree tree)
             (insert (rcons (ubyte32-fix child-index)
                            (ubyte32-list-fix parent-path))
                     (bip32-key-tree->index-tree tree))))))

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

(defthm bip32-key-tree-priv-p-of-bip32-extend-tree
 (equal
     (bip32-key-tree-priv-p
          (mv-nth 1
                  (bip32-extend-tree tree parent-path child-index)))
     (bip32-key-tree-priv-p tree)))

Theorem: bip32-path-in-tree-p-of-bip32-extend-tree

(defthm bip32-path-in-tree-p-of-bip32-extend-tree
  (b* (((mv error? new-key-tree)
        (bip32-extend-tree key-tree path index)))
    (implies (not error?)
             (bip32-path-in-tree-p (rcons index path)
                                   new-key-tree))))

Theorem: bip32-extend-tree-of-bip32-key-tree-fix-tree

(defthm bip32-extend-tree-of-bip32-key-tree-fix-tree
  (equal (bip32-extend-tree (bip32-key-tree-fix tree)
                            parent-path child-index)
         (bip32-extend-tree tree parent-path child-index)))

Theorem: bip32-extend-tree-bip32-key-tree-equiv-congruence-on-tree

(defthm bip32-extend-tree-bip32-key-tree-equiv-congruence-on-tree
 (implies
     (bip32-key-tree-equiv tree tree-equiv)
     (equal (bip32-extend-tree tree parent-path child-index)
            (bip32-extend-tree tree-equiv parent-path child-index)))
 :rule-classes :congruence)

Theorem: bip32-extend-tree-of-ubyte32-list-fix-parent-path

(defthm bip32-extend-tree-of-ubyte32-list-fix-parent-path
  (equal (bip32-extend-tree tree (ubyte32-list-fix parent-path)
                            child-index)
         (bip32-extend-tree tree parent-path child-index)))

Theorem: bip32-extend-tree-ubyte32-list-equiv-congruence-on-parent-path

(defthm
     bip32-extend-tree-ubyte32-list-equiv-congruence-on-parent-path
 (implies
     (acl2::ubyte32-list-equiv parent-path parent-path-equiv)
     (equal (bip32-extend-tree tree parent-path child-index)
            (bip32-extend-tree tree parent-path-equiv child-index)))
 :rule-classes :congruence)

Theorem: bip32-extend-tree-of-ubyte32-fix-child-index

(defthm bip32-extend-tree-of-ubyte32-fix-child-index
  (equal (bip32-extend-tree tree
                            parent-path (ubyte32-fix child-index))
         (bip32-extend-tree tree parent-path child-index)))

Theorem: bip32-extend-tree-ubyte32-equiv-congruence-on-child-index

(defthm bip32-extend-tree-ubyte32-equiv-congruence-on-child-index
 (implies
     (acl2::ubyte32-equiv child-index child-index-equiv)
     (equal (bip32-extend-tree tree parent-path child-index)
            (bip32-extend-tree tree parent-path child-index-equiv)))
 :rule-classes :congruence)