• 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
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
        • Bip32
        • Bech32
        • Bip39
        • Bip44
          • Bip44-compliant-addresses-for-limit-p
          • Bip44-compliant-chains-p
          • Bip44-compliant-accounts-for-limit-p
          • Bip44-compliant-addresses-p
          • Bip44-compliant-coins-for-set-p
          • Bip44-compliant-tree-p
          • Bip44-compliant-accounts-p
          • Bip44-compliant-coins-p
          • Bip44-compliant-depth-p
          • Bip44-coin-type-set
          • Bip44-coin-types
          • *bip44-purpose*
        • 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

• Bip44

Bip44-compliant-coins-for-set-p

Check if the coin keys under the purpose key in a tree comply with the BIP 44 wallet structure, for a given set of coin types.

This is similar to bip44-compliant-addresses-for-limit-p, but instead of an address limit we have a set of coin types. We require that there is a coin key in the tree exactly for each coin type in the given set. Furthermore, we require, for each such coin key, its children account keys to be compliant with the BIP 44 wallet structure.

Following [BIP44], we require each coin key to be hardened.

Definitions and Theorems

Theorem: bip44-compliant-coins-for-set-p-necc

(defthm bip44-compliant-coins-for-set-p-necc
 (implies
   (bip44-compliant-coins-for-set-p tree coins)
   (implies
        (ubyte32p coin-index)
        (b* ((path (list (+ *bip44-purpose* (expt 2 31))
                         coin-index)))
          (cond ((< coin-index (expt 2 31))
                 (not (bip32-path-in-tree-p path tree)))
                ((in (- coin-index (expt 2 31))
                     (bip44-coin-type-set-fix coins))
                 (and (bip32-path-in-tree-p path tree)
                      (bip44-compliant-accounts-p tree coin-index)))
                (t (not (bip32-path-in-tree-p path tree))))))))

Theorem: booleanp-of-bip44-compliant-coins-for-set-p

(defthm booleanp-of-bip44-compliant-coins-for-set-p
  (b* ((yes/no (bip44-compliant-coins-for-set-p tree coins)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: bip44-compliant-coins-for-set-p-of-bip32-key-tree-fix-tree

(defthm bip44-compliant-coins-for-set-p-of-bip32-key-tree-fix-tree
  (equal (bip44-compliant-coins-for-set-p (bip32-key-tree-fix tree)
                                          coins)
         (bip44-compliant-coins-for-set-p tree coins)))

Theorem: bip44-compliant-coins-for-set-p-bip32-key-tree-equiv-congruence-on-tree

(defthm
 bip44-compliant-coins-for-set-p-bip32-key-tree-equiv-congruence-on-tree
 (implies
      (bip32-key-tree-equiv tree tree-equiv)
      (equal (bip44-compliant-coins-for-set-p tree coins)
             (bip44-compliant-coins-for-set-p tree-equiv coins)))
 :rule-classes :congruence)

Theorem: bip44-compliant-coins-for-set-p-of-bip44-coin-type-set-fix-coins

(defthm
   bip44-compliant-coins-for-set-p-of-bip44-coin-type-set-fix-coins
  (equal (bip44-compliant-coins-for-set-p
              tree (bip44-coin-type-set-fix coins))
         (bip44-compliant-coins-for-set-p tree coins)))

Theorem: bip44-compliant-coins-for-set-p-bip44-coin-type-set-equiv-congruence-on-coins

(defthm
 bip44-compliant-coins-for-set-p-bip44-coin-type-set-equiv-congruence-on-coins
 (implies
      (bip44-coin-type-set-equiv coins coins-equiv)
      (equal (bip44-compliant-coins-for-set-p tree coins)
             (bip44-compliant-coins-for-set-p tree coins-equiv)))
 :rule-classes :congruence)