		Search-engine friendly clone of the ACL2 documentation.

Bip44

Bip44-compliant-accounts-for-limit-p

Check if the account keys in a tree comply with the BIP 44 wallet structure, for a given account index limit.

This is similar to bip44-compliant-addresses-for-limit-p.

[BIP44] says that hardened keys are used for accounts. Thus, we require all non-hardened account keys to be absent and we apply the limit to hardened account keys by adding 2^{31} to the limit.

For each account index below the limit, we require not only the account key to be present, but also the chain keys to be compliant to the BIP 44 wallet structure; again, we are defining compliance incrementally.

We allow a gap in the account keys only if the account key is invalid, or any chain key under it is invalid. See the discussion about this in bip44-compliant-chains-p.

Definitions and Theorems

Theorem: bip44-compliant-accounts-for-limit-p-necc

(defthm bip44-compliant-accounts-for-limit-p-necc
 (implies
  (bip44-compliant-accounts-for-limit-p
       tree coin-index account-index-limit)
  (implies
   (ubyte32p account-index)
   (b* ((root-key (bip32-key-tree->root-key tree))
        (path (list (+ *bip44-purpose* (expt 2 31))
                    coin-index account-index)))
    (cond
     ((< account-index (expt 2 31))
      (not (bip32-path-in-tree-p path tree)))
     ((< account-index
         (+ (nfix account-index-limit)
            (expt 2 31)))
      (or
       (and
           (bip32-path-in-tree-p path tree)
           (bip44-compliant-chains-p tree coin-index account-index))
       (mv-nth 0 (bip32-ckd* root-key path))
       (mv-nth 0 (bip32-ckd* root-key (rcons 0 path)))
       (mv-nth 0
               (bip32-ckd* root-key (rcons 1 path)))))
     (t (not (bip32-path-in-tree-p path tree))))))))

Theorem: booleanp-of-bip44-compliant-accounts-for-limit-p

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

Theorem: bip44-compliant-accounts-for-limit-p-of-bip32-key-tree-fix-tree

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

Theorem: bip44-compliant-accounts-for-limit-p-bip32-key-tree-equiv-congruence-on-tree

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

Theorem: bip44-compliant-accounts-for-limit-p-of-ubyte32-fix-coin-index

(defthm
     bip44-compliant-accounts-for-limit-p-of-ubyte32-fix-coin-index
  (equal (bip44-compliant-accounts-for-limit-p
              tree (ubyte32-fix coin-index)
              account-index-limit)
         (bip44-compliant-accounts-for-limit-p
              tree coin-index account-index-limit)))

Theorem: bip44-compliant-accounts-for-limit-p-ubyte32-equiv-congruence-on-coin-index

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

Theorem: bip44-compliant-accounts-for-limit-p-of-nfix-account-index-limit

(defthm
   bip44-compliant-accounts-for-limit-p-of-nfix-account-index-limit
  (equal (bip44-compliant-accounts-for-limit-p
              tree
              coin-index (nfix account-index-limit))
         (bip44-compliant-accounts-for-limit-p
              tree coin-index account-index-limit)))

Theorem: bip44-compliant-accounts-for-limit-p-nat-equiv-congruence-on-account-index-limit

(defthm
 bip44-compliant-accounts-for-limit-p-nat-equiv-congruence-on-account-index-limit
 (implies (nat-equiv account-index-limit
                     account-index-limit-equiv)
          (equal (bip44-compliant-accounts-for-limit-p
                      tree coin-index account-index-limit)
                 (bip44-compliant-accounts-for-limit-p
                      tree
                      coin-index account-index-limit-equiv)))
 :rule-classes :congruence)