		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Stat-all-valid-key-paths-p

Check if all the key paths in the wallet are valid.

Signature
(stat-all-valid-key-paths-p stat) → yes/no
Arguments: stat — Guard (statp stat).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: stat-all-valid-key-paths-p

(defun stat-all-valid-key-paths-p (stat)
       (declare (xargs :guard (statp stat)))
       (all-valid-key-paths-p
            (bip32-key-tree->index-tree (stat->keys stat))
            (stat->addresses stat)))

Theorem: booleanp-of-stat-all-valid-key-paths-p

(defthm booleanp-of-stat-all-valid-key-paths-p
        (b* ((yes/no (stat-all-valid-key-paths-p stat)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Theorem: not-bip32-path-in-tree-p-of-next-key-path

(defthm
   not-bip32-path-in-tree-p-of-next-key-path
   (implies (and (stat-addresses-bounded-p stat)
                 (stat-all-valid-key-paths-p stat))
            (not (bip32-path-in-tree-p (rcons (stat->addresses stat)
                                              *key-path-prefix*)
                                       (stat->keys stat)))))