		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Next-key

Address key generation in the wallet.

Signature
(next-key stat) → (mv error? index address stat)
Arguments: stat — Guard (statp stat).
Returns: error? — Type (maybe-command-error-p error?).; index — Type (natp index).; address — Type (byte-list20p address).; stat — Type (statp stat).

This models the command used to generate the next address key in the wallet.

We attempt to derive the address key whose index is the state component that counts the number of (attempted) address key derivations so far.

This may fail in two rare cases. One is the case in which key derivation fails, as discussed in [BIP32]. The other is the case in which the index of the next address key is 2^{31}: since according to [BIP44] address keys are not hardened, their indices are limited to the set [0,2^{31}). In the first case, this function returns :address-key-derivation-failed as the error flag. In the second case, this function returns :address-key-index-too-large as the error flag. In all the other cases, the error flag is nil, i.e. success. If key derivation fails, the state is updated by increasing the number of (attempted) address keys nonetheless, so that the next instance of this command will not re-try to derive the same key (which would fail again). If instead the command fails due to the index being 2^{31}, no state change happens.

Besides the updated state, we also return the address index of the key just derived, as well as the account address derived from the key.

The guard proofs of this operation need some of the constraints formalized in stat-wfp.

This operation preserves the constraints formalized by stat-wfp.

Definitions and Theorems

Function: next-key

(defun
    next-key (stat)
    (declare (xargs :guard (statp stat)))
    (declare (xargs :guard (stat-wfp stat)))
    (b* ((next-index (stat->addresses stat))
         ((when (= next-index (expt 2 31)))
          (mv (command-error-address-key-index-limit)
              next-index (repeat 20 0)
              (stat-fix stat)))
         (key-tree (stat->keys stat))
         ((mv error? new-key-tree)
          (bip32-extend-tree key-tree *key-path-prefix* next-index))
         ((when error?)
          (mv (command-error-address-key-derivation-fail next-index)
              next-index (repeat 20 0)
              (change-stat stat
                           :addresses (1+ next-index))))
         (address (private-key-to-address
                       (bip32-get-priv-key-at-path
                            new-key-tree
                            (rcons next-index *key-path-prefix*)))))
        (mv nil next-index address
            (change-stat stat
                         :keys new-key-tree
                         :addresses (1+ next-index)))))

Theorem: maybe-command-error-p-of-next-key.error?

(defthm maybe-command-error-p-of-next-key.error?
        (b* (((mv ?error? ?index ?address ?stat)
              (next-key stat)))
            (maybe-command-error-p error?))
        :rule-classes :rewrite)

Theorem: natp-of-next-key.index

(defthm natp-of-next-key.index
        (b* (((mv ?error? ?index ?address ?stat)
              (next-key stat)))
            (natp index))
        :rule-classes :rewrite)

Theorem: byte-list20p-of-next-key.address

(defthm byte-list20p-of-next-key.address
        (b* (((mv ?error? ?index ?address ?stat)
              (next-key stat)))
            (byte-list20p address))
        :rule-classes :rewrite)

Theorem: statp-of-next-key.stat

(defthm statp-of-next-key.stat
        (b* (((mv ?error? ?index ?address ?stat)
              (next-key stat)))
            (statp stat))
        :rule-classes :rewrite)

Theorem: stat-wfp-of-next-key

(defthm stat-wfp-of-next-key
        (implies (and (statp stat) (stat-wfp stat))
                 (stat-wfp (mv-nth 3 (next-key stat)))))