|
|
|---|
|
|
|
|---|
Check if the address keys under a given chain key in a tree comply with the BIP 32 wallet structure, for a given address index limit.
The chain key is identified by an account index and a chain index, passed as arguments to this predicate. This predicate essentially checks if the designated chain key has children at all the indices below a limit (passed as another argument to this predicate), and has no other children.
The adverb 'essentially' above refers to the fact that a child key derivation may fail, and so there may be rare but mathematically possible gaps in the sequence of address keys. The address index limit passed as argument is often the number of address keys under the chain key, except for the rare cases in which there are gaps, or in another case described below.
Note that the guard of this predicate requires the chain key to be valid. Therefore bip32-ckd*, as used in the definition of this predicate, returns an error iff the address key is invalid, i.e. iff there is an unavoidable gap in the sequence of address keys. Formally, we require that each address key path whose address index is below the limit either is in the tree or corresponds to an invalid address key.
If the address index limit is 0, this predicate holds iff the chain key has no children. This corresponds to the valid situation in which, in a compliant wallet, a chain key has been created, but no address keys under it have been created yet.
The guard of this predicate allows the address index limit to be
any natural number, not necessarily representable in 32 bits like indices.
Thus, the unlikely but mathematically possible case in which
all possible address keys have been created under a chain key,
can be accommodated by using
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-necc (implies (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit) (implies (ubyte32p address-index) (b* ((path (list account-index chain-index address-index))) (if (< address-index (nfix address-index-limit)) (or (bip32-path-in-tree-p path tree) (mv-nth 0 (bip32-ckd* (bip32-key-tree->root-key tree) path))) (not (bip32-path-in-tree-p path tree)))))))
Theorem:
(defthm booleanp-of-bip32-compliant-addresses-for-limit-p (b* ((yes/no (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-of-bip32-key-tree-fix-tree (equal (bip32-compliant-addresses-for-limit-p (bip32-key-tree-fix tree) account-index chain-index address-index-limit) (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit)))
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-bip32-key-tree-equiv-congruence-on-tree (implies (bip32-key-tree-equiv tree tree-equiv) (equal (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit) (bip32-compliant-addresses-for-limit-p tree-equiv account-index chain-index address-index-limit))) :rule-classes :congruence)
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-of-ubyte32-fix-account-index (equal (bip32-compliant-addresses-for-limit-p tree (ubyte32-fix account-index) chain-index address-index-limit) (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit)))
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-ubyte32-equiv-congruence-on-account-index (implies (acl2::ubyte32-equiv account-index account-index-equiv) (equal (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit) (bip32-compliant-addresses-for-limit-p tree account-index-equiv chain-index address-index-limit))) :rule-classes :congruence)
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-of-ubyte32-fix-chain-index (equal (bip32-compliant-addresses-for-limit-p tree account-index (ubyte32-fix chain-index) address-index-limit) (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit)))
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-ubyte32-equiv-congruence-on-chain-index (implies (acl2::ubyte32-equiv chain-index chain-index-equiv) (equal (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit) (bip32-compliant-addresses-for-limit-p tree account-index chain-index-equiv address-index-limit))) :rule-classes :congruence)
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-of-nfix-address-index-limit (equal (bip32-compliant-addresses-for-limit-p tree account-index chain-index (nfix address-index-limit)) (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit)))
Theorem:
(defthm bip32-compliant-addresses-for-limit-p-nat-equiv-congruence-on-address-index-limit (implies (nat-equiv address-index-limit address-index-limit-equiv) (equal (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit) (bip32-compliant-addresses-for-limit-p tree account-index chain-index address-index-limit-equiv))) :rule-classes :congruence)