|
|
|---|
|
|
|
|---|
Turn a command error into a user-oriented message.
(command-error-message command error) → msg
The message consists of two parts:
Function:
(defun command-error-message (command error) (declare (xargs :guard (and (stringp command) (command-error-p error)))) (b* ((heading-core (if (member-equal command (list *command-name-init-from-entropy* *command-name-init-from-mnemonic* *command-name-sign* *command-name-next-key*)) (msg "Error in command '~s0':" command) (msg "Error:"))) (heading (msg "~@0~%~%" heading-core)) (body-core (command-error-case error :malformed-mnemonic (msg "The supplied mnemonic argument is impossibly long: ~ it consists of ~x0 characters." (length error.mnemonic)) :malformed-passphrase (msg "The supplied passphrase argument is impossibly long: ~ it consists of ~x0 characters." (length error.passphrase)) :malformed-entropy (msg "The entropy argument must be a sequence of ~ 32, 40, 48, 56, or 64 hexadecimal digits without spaces ~ (forming a sequence of 16, 20, 24, 28, or 32 bytes). The supplied entropy argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.entropy) :malformed-nonce (msg "The nonce argument must be a sequence of ~ decimal digits without spaces that form a 256-bit number. ~ The supplied nonce argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.nonce) :malformed-gas-price (msg "The gas price argument must be a sequence of ~ decimal digits without spaces that forms a 256-bit number. ~ The supplied gas price argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.gas-price) :malformed-gas-limit (msg "The gas limit argument must be a sequence of ~ decimal digits without spaces that forms a 256-bit number. ~ The supplied gas limit argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.gas-limit) :malformed-to (msg "The recipient argument must be a sequence of ~ 40 hexadecimal digits without spaces ~ (forming a sequence of 20 bytes). The supplied recipient argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.to) :malformed-value (msg "The value argument must be a sequence of ~ decimal digits without spaces that form a 256-bit number. ~ The supplied value argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.value) :malformed-data (msg "The data argument must be a sequence of ~ an even number of hexadecimal digits without spaces ~ (forming a sequence of bytes of half the length). ~ The supplied data argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.data) :malformed-address-key-index (msg "The address key index argument must be a sequence of ~ decimal digits without spaces that form a number. ~ The supplied address key index argument~%~%~ ~s0~s1~%~%~ does not have that form." " " error.address-key-index) :address-key-index-too-large (msg "The address key index argument ~x0 ~ must denote an existing key, ~ i.e. it must be a number between ~ 0 (inclusive) and ~x1 (exclusive), ~ where ~x1 is the number of address key indices used so far." error.address-key-index error.limit) :address-key-index-skipped (msg "The address key index argument ~x0 ~ must denote an existing key, ~ but the derivation of the address key with that index failed ~ and therefore the key with that index was skipped." error.address-key-index) :root-key-derivation-fail (msg "The derivation of the root key from the seed ~ failed, and therefore the wallet cannot be initialized. ~ This is rare, but not impossible. Try initializing the wallet again with different inputs, ~ perhaps just a different passphrase: ~ this will generally produce a different seed.") :purpose-key-derivation-fail (msg "The derivation of the purpose key from the root key ~ failed, and therefore the wallet cannot be initialized. ~ This is rare, but not impossible. Try initializing the wallet again with different inputs, ~ perhaps just a different passphrase: ~ this will generally produce a different seed ~ and therefore a different ~ root key.") :coin-type-key-derivation-fail (msg "The derivation of the coin type key from the purpose key ~ failed, and therefore the wallet cannot be initialized. ~ This is rare, but not impossible. Try initializing the wallet again with different inputs, ~ perhaps just a different passphrase: ~ this will generally produce a different seed ~ and therefore a different ~ root key and purpose key.") :account-key-derivation-fail (msg "The derivation of the account key from the coin type key ~ failed, and therefore the wallet cannot be initialized. ~ This is rare, but not impossible. Try initializing the wallet again with different inputs, ~ perhaps just a different passphrase: ~ this will generally produce a different seed ~ and therefore a different ~ root key, purpose key, and coin type key.") :external-chain-key-derivation-fail (msg "The derivation of the external chain key from the account key ~ failed, and therefore the wallet cannot be initialized. ~ This is rare, but not impossible. Try initializing the wallet again with different inputs, ~ perhaps just a different passphrase: ~ this will generally produce a different seed ~ and therefore a different ~ root key, purpose key, coin type key, and account key.") :address-key-derivation-fail (msg "The derivation of the address key with index ~x0 failed. ~ This is rare, but not impossible. This address key index will be marked as skipped. Run this command again to attempt to derive an address key ~ with the next index." error.address-key-index) :address-key-index-limit (msg "A very large number of address keys ~ has already been generated in this wallet, ~ reaching the maximum address key index ~x0. ~ Therefore, it is not possible to generate another key, ~ because its index would exceed the maximum. ~ Try creating an additional wallet." (1- (expt 2 31))) :pretransaction-rlp-fail (msg "An impossibly large transaction is being created for signing. ~ It is so large that it cannot be RLP-encoded, ~ which is required in order to sign it.") :transaction-sign-fail (msg "The ECDSA signature of the transaction failed. ~ This is rare but not impossible. ~ Since this wallet uses a deterministic ECDSA, ~ attempting to create the same transaction will fail again. ~ Try instead varying slightly ~ some non-critical components of the transaction, ~ such as the gas limit.") :transaction-rlp-fail (msg "An impossibly large signed transaction has been created. ~ It is so large that it cannot be RLP-encoded, ~ which is required in order to send it to the Ethereum network.") :state-file-untestable (msg "A failure occurred while attempting to check ~ whether a file with the wallet state exists. ~ This is out of the wallet's control. ~ Make sure that the directory (and file, if it exists) ~ are accessible to the user who is running the wallet: ~ the path of the file is '~s0'." *stat-filepath*) :state-file-absent (msg "No file with the wallet state was found at the path '~s0'. ~ This command requires that file to exist, ~ i.e. that the wallet has already been initialized." *stat-filepath*) :state-file-present (msg "A file with the wallet state was found at the path '~s0'. ~ This command will overwrite that file. ~ If that is intended, separately remove the file ~ and try this command again." *stat-filepath*) :state-file-not-regular (msg "The path '~s0' to the wallet state exists in the file system, ~ but it does not refer to a regular file. ~ The file system entity at that path may have been modified from outside the wallet. ~ Re-create the file by re-initializing the wallet ~ from the original mnemonic and passphrase." *stat-filepath*) :state-file-malformed (msg "The file at the path '~s0' does not contain ~ a well-formed wallet state. ~ The file may have been modified from outside the wallet. ~ Re-create the file by re-initializing the wallet ~ from the original mnemonic and passphrase." *stat-filepath*) :wrong-number-of-arguments (msg "This command requires ~x0 arguments, but ~x1 arguments were supplied instead." error.required error.given) :wrong-command (msg "The supplied command '~s0' is not among the wallet commands. ~ The wallet commands are '~s1', '~s2', '~s3', and '~s4'." command *command-name-init-from-entropy* *command-name-init-from-mnemonic* *command-name-sign* *command-name-next-key*) :no-command (msg "No command was supplied to the wallet. ~ The wallet commands are '~s0', '~s1', '~s2', and '~s3'." *command-name-init-from-entropy* *command-name-init-from-mnemonic* *command-name-sign* *command-name-next-key*))) (body (msg "~@0~%~%" body-core))) (msg "~@0~@1" heading body)))
Theorem:
(defthm msgp-of-command-error-message (b* ((msg (command-error-message command error))) (msgp msg)) :rule-classes :rewrite)