		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)))))