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