		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Valid-key-path-p

Check if a key path is valid for the wallet.

Signature
(valid-key-path-p path addresses) → yes/no
Arguments: path — Guard (ubyte32-listp path).; addresses — Guard (natp addresses).
Returns: yes/no — Type (booleanp yes/no).

All the key paths in the wallet must have the form

m / 44' / 60' / 0' / 0 / address_index

where address_index is less than the addresses state component, or they may be prefixes of that; BIP 32 key trees are always required to be closed under prefixes.

This predicate checks if a path has one of these forms.

Definitions and Theorems

Function: valid-key-path-p

(defun valid-key-path-p (path addresses)
       (declare (xargs :guard (and (ubyte32-listp path)
                                   (natp addresses))))
       (b* (((when (atom path)) t)
            ((unless (= (car path) *purpose-index*))
             nil)
            (path (cdr path))
            ((when (atom path)) t)
            ((unless (= (car path) *coin-type-index*))
             nil)
            (path (cdr path))
            ((when (atom path)) t)
            ((unless (= (car path) *account-index*))
             nil)
            (path (cdr path))
            ((when (atom path)) t)
            ((unless (= (car path) *external-chain-index*))
             nil)
            (path (cdr path))
            ((when (atom path)) t)
            ((unless (< (car path) addresses)) nil)
            (path (cdr path)))
           (atom path)))

Theorem: booleanp-of-valid-key-path-p

(defthm booleanp-of-valid-key-path-p
        (b* ((yes/no (valid-key-path-p path addresses)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Theorem: valid-key-path-p-of-next-key-path-under-1+-addresses

(defthm valid-key-path-p-of-next-key-path-under-1+-addresses
        (valid-key-path-p (rcons addresses *key-path-prefix*)
                          (1+ addresses)))

Theorem: valid-key-path-p-of-1+-addresses

(defthm valid-key-path-p-of-1+-addresses
        (implies (valid-key-path-p path addresses)
                 (valid-key-path-p path (1+ addresses))))