		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Init-from-mnemonic

Initialization of the wallet from a mnemonic (and passphrase).

Signature
(init-from-mnemonic mnemonic passphrase) → (mv error? stat?)
Arguments: mnemonic — Guard (stringp mnemonic).; passphrase — Guard (stringp passphrase).
Returns: error? — Type (maybe-command-error-p error?).; stat? — Type (maybe-statp stat?).

This models the command used to initialize the wallet from a mnemonic (and a passphrase). This may be used to port the keys from another wallet, as opposed to creating a new wallet from scratch via init-from-entropy.

This initialization function takes two strings as inputs, the first of which should be a space-separated sequence of BIP 39 mnemonic words; however, we do not check that it is, because, as noted in bip39-mnemonic-to-seed, the seed derivation works for any string. The two input strings are converted to a BIP 32 seed, from which the master key is derived. The master key determines the initial key tree.

We also immediately derive the purpose key 44', the Ethereum mainnet coin type key 60', the default account key 0', and the external chain key 0; see stat. We set the number of address keys to 0 initially, i.e. we do not (attempt to) derive any address key yet.

The derivation of the master key, or of the other keys mentioned above, may fail. This is rare, but not impossible. In this case, initialization fails, as signaled by this function returning an error as the first result (and nil as second result).

If this initialization operation succeeds, the initial state of the wallet satisfies all the constraints formalized by stat-wfp.

Errors are returned if the mnemonic or passphrase strings are unreasonably large. Such large strings are virtually impossible to type, but we need the check to ensure that the guards of the involved cryptographic functions are satisfied.

Definitions and Theorems

Function: init-from-mnemonic

(defun init-from-mnemonic (mnemonic passphrase)
  (declare (xargs :guard (and (stringp mnemonic)
                              (stringp passphrase))))
  (b* (((unless (< (length mnemonic) (expt 2 125)))
        (mv (command-error-malformed-mnemonic mnemonic)
            nil))
       ((unless (< (length passphrase)
                   (- (expt 2 125) (+ 128 4 8))))
        (mv (command-error-malformed-passphrase passphrase)
            nil))
       (seed (bip39-mnemonic-to-seed mnemonic passphrase))
       ((mv error? tree)
        (bip32-master-tree seed))
       ((when error?)
        (mv (command-error-root-key-derivation-fail)
            nil))
       (path nil)
       (next *purpose-index*)
       ((mv error? tree)
        (bip32-extend-tree tree path next))
       ((when error?)
        (mv (command-error-purpose-key-derivation-fail)
            nil))
       (path (rcons next path))
       (next *coin-type-index*)
       ((mv error? tree)
        (bip32-extend-tree tree path next))
       ((when error?)
        (mv (command-error-coin-type-key-derivation-fail)
            nil))
       (path (rcons next path))
       (next *account-index*)
       ((mv error? tree)
        (bip32-extend-tree tree path next))
       ((when error?)
        (mv (command-error-account-key-derivation-fail)
            nil))
       (path (rcons next path))
       (next *external-chain-index*)
       ((mv error? tree)
        (bip32-extend-tree tree path next))
       ((when error?)
        (mv (command-error-external-chain-key-derivation-fail)
            nil)))
    (mv nil (stat tree 0))))

Theorem: maybe-command-error-p-of-init-from-mnemonic.error?

(defthm maybe-command-error-p-of-init-from-mnemonic.error?
  (b* (((mv ?error? ?stat?)
        (init-from-mnemonic mnemonic passphrase)))
    (maybe-command-error-p error?))
  :rule-classes :rewrite)

Theorem: maybe-statp-of-init-from-mnemonic.stat?

(defthm maybe-statp-of-init-from-mnemonic.stat?
  (b* (((mv ?error? ?stat?)
        (init-from-mnemonic mnemonic passphrase)))
    (maybe-statp stat?))
  :rule-classes :rewrite)

Theorem: statp-of-init-from-mnemonic-when-no-error

(defthm statp-of-init-from-mnemonic-when-no-error
  (b* (((mv error? stat?)
        (init-from-mnemonic mnemonic passphrase)))
    (implies (not error?) (statp stat?))))

Theorem: stat-wfp-of-init-from-mnemonic-when-no-error

(defthm stat-wfp-of-init-from-mnemonic-when-no-error
  (b* (((mv error? stat?)
        (init-from-mnemonic mnemonic passphrase)))
    (implies (not error?)
             (stat-wfp stat?))))