		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Init-from-entropy

Initialization of the wallet from an entropy value (and a passphrase).

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

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

The entropy is supplied as a hex string (see string-to-byte-list). After turning the string into a list of bytes and then a list of bits, we turn the resulting entropy into a mnemonic, and then we call init-from-mnemonic to initialize the wallet from the generated mnemonic.

Besides the initial wallet state, we also return the generated mnemonic, so that the user can make a note of it and store it securely. The mnemonic can be later used by the user to re-create the wallet, via init-from-mnemonic.

The first result is an error flag. It is set exactly when the input entropy string is malformed, or the creation of the initial state from the mnemonic fails (see init-from-mnemonic).

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

Definitions and Theorems

Function: init-from-entropy

(defun init-from-entropy (entropy-string passphrase)
  (declare (xargs :guard (and (stringp entropy-string)
                              (stringp passphrase))))
  (b* (((mv error? entropy-bytes)
        (string-to-byte-list entropy-string))
       ((when error?)
        (mv (command-error-malformed-entropy entropy-string)
            "" nil))
       (entropy (bebytes=>bits entropy-bytes))
       ((unless (bip39-entropy-size-p (len entropy)))
        (mv (command-error-malformed-entropy entropy-string)
            "" nil))
       (mnemonic (bip39-entropy-to-mnemonic entropy))
       ((unless (< (length passphrase)
                   (- (expt 2 125) (+ 128 4 8))))
        (mv (command-error-malformed-passphrase passphrase)
            "" nil))
       ((mv error? stat)
        (init-from-mnemonic mnemonic passphrase))
       ((when error?) (mv error? "" nil)))
    (mv nil mnemonic stat)))

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

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

Theorem: stringp-of-init-from-entropy.mnemonic

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

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

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

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

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

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

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