Check if the chain keys under a given account key in a tree comply with the BIP 32 wallet structure.
This is similar to bip32-compliant-addresses-p and bip32-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 an internal 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 internal 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 [BIP32], but it seems reasonable.
Furthermore, in this predicate we require the address keys under each chain to be compliant with the BIP 32 structure. We are defining key tree compliance incrementally here.
Theorem:
(defthm bip32-compliant-chains-p-necc (implies (bip32-compliant-chains-p tree account-index) (implies (ubyte32p chain-index) (b* ((path (list account-index chain-index))) (case chain-index (0 (and (bip32-path-in-tree-p path tree) (bip32-compliant-addresses-p tree account-index chain-index))) (1 (and (bip32-path-in-tree-p path tree) (bip32-compliant-addresses-p tree account-index chain-index))) (t (not (bip32-path-in-tree-p path tree))))))))
Theorem:
(defthm booleanp-of-bip32-compliant-chains-p (b* ((yes/no (bip32-compliant-chains-p tree account-index))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip32-compliant-chains-p-of-bip32-key-tree-fix-tree (equal (bip32-compliant-chains-p (bip32-key-tree-fix tree) account-index) (bip32-compliant-chains-p tree account-index)))
Theorem:
(defthm bip32-compliant-chains-p-bip32-key-tree-equiv-congruence-on-tree (implies (bip32-key-tree-equiv tree tree-equiv) (equal (bip32-compliant-chains-p tree account-index) (bip32-compliant-chains-p tree-equiv account-index))) :rule-classes :congruence)
Theorem:
(defthm bip32-compliant-chains-p-of-ubyte32-fix-account-index (equal (bip32-compliant-chains-p tree (ubyte32-fix account-index)) (bip32-compliant-chains-p tree account-index)))
Theorem:
(defthm bip32-compliant-chains-p-ubyte32-equiv-congruence-on-account-index (implies (acl2::ubyte32-equiv account-index account-index-equiv) (equal (bip32-compliant-chains-p tree account-index) (bip32-compliant-chains-p tree account-index-equiv))) :rule-classes :congruence)