|
|
|---|
|
|
|
|---|
Check if the address keys under a given chain key in a tree comply with the BIP 44 wallet structure, for a given address index limit.
The chain key is identified by a coin index, 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.
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.
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-necc (implies (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit) (implies (ubyte32p address-index) (b* ((path (list (+ *bip44-purpose* (expt 2 31)) coin-index 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-bip44-compliant-addresses-for-limit-p (b* ((yes/no (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-of-bip32-key-tree-fix-tree (equal (bip44-compliant-addresses-for-limit-p (bip32-key-tree-fix tree) coin-index account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit)))
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-bip32-key-tree-equiv-congruence-on-tree (implies (bip32-key-tree-equiv tree tree-equiv) (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree-equiv coin-index account-index chain-index address-index-limit))) :rule-classes :congruence)
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-of-ubyte32-fix-coin-index (equal (bip44-compliant-addresses-for-limit-p tree (ubyte32-fix coin-index) account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit)))
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-ubyte32-equiv-congruence-on-coin-index (implies (acl2::ubyte32-equiv coin-index coin-index-equiv) (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index-equiv account-index chain-index address-index-limit))) :rule-classes :congruence)
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-of-nfix-address-index-limit (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index (nfix address-index-limit)) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit)))
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-nat-equiv-congruence-on-address-index-limit (implies (nat-equiv address-index-limit address-index-limit-equiv) (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit-equiv))) :rule-classes :congruence)
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-of-ubyte32-fix-account-index (equal (bip44-compliant-addresses-for-limit-p tree coin-index (ubyte32-fix account-index) chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit)))
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-ubyte32-equiv-congruence-on-account-index (implies (acl2::ubyte32-equiv account-index account-index-equiv) (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index-equiv chain-index address-index-limit))) :rule-classes :congruence)
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-of-ubyte32-fix-chain-index (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index (ubyte32-fix chain-index) address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit)))
Theorem:
(defthm bip44-compliant-addresses-for-limit-p-ubyte32-equiv-congruence-on-chain-index (implies (acl2::ubyte32-equiv chain-index chain-index-equiv) (equal (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index address-index-limit) (bip44-compliant-addresses-for-limit-p tree coin-index account-index chain-index-equiv address-index-limit))) :rule-classes :congruence)