• 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-chains-p

Check if the chain keys under a given account key in a tree comply with the BIP 44 wallet structure.

This is similar to bip44-compliant-addresses-p and bip44-compliant-addresses-for-limit-p, but the limit is always 2 in this case, because there must be exactly two chains for each account: an external chain and a change chain. So we do not need the existential quantification over the limit and we just have a single level of (universal) quantification.

There is also another difference with address keys, namely that we require both chain keys to be present. While an invalid address key is acceptable and is simply skipped, we cannot skip an external or change chain for an account. If either chain key is invalid, then presumably the whole account key should be skipped; this is not explicitly said in [BIP44], but it seems reasonable.

Furthermore, in this predicate we require the address keys under each chain to be compliant with the BIP 44 structure. We are defining key tree compliance incrementally here.

Definitions and Theorems

Theorem: bip44-compliant-chains-p-necc

(defthm bip44-compliant-chains-p-necc
 (implies
   (bip44-compliant-chains-p tree coin-index account-index)
   (implies (ubyte32p chain-index)
            (b* ((path (list (+ *bip44-purpose* (expt 2 31))
                             coin-index account-index chain-index)))
              (case chain-index
                (0 (and (bip32-path-in-tree-p path tree)
                        (bip44-compliant-addresses-p
                             tree
                             coin-index account-index chain-index)))
                (1 (and (bip32-path-in-tree-p path tree)
                        (bip44-compliant-addresses-p
                             tree
                             coin-index account-index chain-index)))
                (t (not (bip32-path-in-tree-p path tree))))))))

Theorem: booleanp-of-bip44-compliant-chains-p

(defthm booleanp-of-bip44-compliant-chains-p
  (b*
    ((yes/no
          (bip44-compliant-chains-p tree coin-index account-index)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: bip44-compliant-chains-p-of-bip32-key-tree-fix-tree

(defthm bip44-compliant-chains-p-of-bip32-key-tree-fix-tree
  (equal (bip44-compliant-chains-p (bip32-key-tree-fix tree)
                                   coin-index account-index)
         (bip44-compliant-chains-p tree coin-index account-index)))

Theorem: bip44-compliant-chains-p-bip32-key-tree-equiv-congruence-on-tree

(defthm
   bip44-compliant-chains-p-bip32-key-tree-equiv-congruence-on-tree
 (implies
  (bip32-key-tree-equiv tree tree-equiv)
  (equal
    (bip44-compliant-chains-p tree coin-index account-index)
    (bip44-compliant-chains-p tree-equiv coin-index account-index)))
 :rule-classes :congruence)

Theorem: bip44-compliant-chains-p-of-ubyte32-fix-coin-index

(defthm bip44-compliant-chains-p-of-ubyte32-fix-coin-index
  (equal (bip44-compliant-chains-p tree (ubyte32-fix coin-index)
                                   account-index)
         (bip44-compliant-chains-p tree coin-index account-index)))

Theorem: bip44-compliant-chains-p-ubyte32-equiv-congruence-on-coin-index

(defthm
    bip44-compliant-chains-p-ubyte32-equiv-congruence-on-coin-index
 (implies
  (acl2::ubyte32-equiv coin-index coin-index-equiv)
  (equal
    (bip44-compliant-chains-p tree coin-index account-index)
    (bip44-compliant-chains-p tree coin-index-equiv account-index)))
 :rule-classes :congruence)

Theorem: bip44-compliant-chains-p-of-ubyte32-fix-account-index

(defthm bip44-compliant-chains-p-of-ubyte32-fix-account-index
 (equal
   (bip44-compliant-chains-p tree
                             coin-index (ubyte32-fix account-index))
   (bip44-compliant-chains-p tree coin-index account-index)))

Theorem: bip44-compliant-chains-p-ubyte32-equiv-congruence-on-account-index

(defthm
 bip44-compliant-chains-p-ubyte32-equiv-congruence-on-account-index
 (implies
  (acl2::ubyte32-equiv account-index account-index-equiv)
  (equal
    (bip44-compliant-chains-p tree coin-index account-index)
    (bip44-compliant-chains-p tree coin-index account-index-equiv)))
 :rule-classes :congruence)