		Search-engine friendly clone of the ACL2 documentation.

Bip32-wallet-structure

Bip32-compliant-accounts-for-limit-p

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

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

The figure in [BIP32] shows account keys as non-hardned keys, because there are no \mathsf{H} subscripts in the indices. However, the text in [BIP32] shows the \mathsf{H} subscripts. It seems reasonable for account keys to be hardened, so we require that in this predicate. Specifically, 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 32 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 bip32-compliant-chains-p.

Definitions and Theorems

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

(defthm bip32-compliant-accounts-for-limit-p-necc
 (implies
  (bip32-compliant-accounts-for-limit-p tree account-index-limit)
  (implies
    (ubyte32p account-index)
    (b* ((root-key (bip32-key-tree->root-key tree))
         (path (list 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)
                      (bip32-compliant-chains-p tree 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-bip32-compliant-accounts-for-limit-p

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

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

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

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

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

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

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

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

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