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