• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
        • Command-error
        • Sign
        • Init-from-mnemonic
        • Command-error-message
        • Stat
        • Next-key
        • Init-from-entropy
        • Process-command
        • Transaction-message
        • Maybe-command-error
        • Maybe-stat
        • Check-stat-file-present
        • Valid-key-path-p
        • String-to-byte-list
        • Load-stat
        • Mnemonic-message
        • Process-sign
        • Process-init-from-entropy
        • All-valid-key-paths-p
        • String-to-word
        • String-to-nat
        • Process-next-key
        • Wallet
        • Process-init-from-mnemonic
        • Check-stat-file-absent
        • Stat-wfp
        • Save-stat
        • Stat-addresses-bounded-p
        • Stat-all-valid-key-paths-p
        • Stat-priv-keys-p
        • Stat-root-depth-zero-p
        • Stat-path-prefix-in-tree-p
        • Crypto-hdwallet-executable
        • *stat-filepath*
        • *key-path-prefix*
        • *coin-type-index*
        • *purpose-index*
        • *external-chain-index*
        • *command-name-init-from-mnemonic*
        • *command-name-init-from-entropy*
        • *account-index*
        • *command-name-sign*
        • *command-name-next-key*
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Crypto-hdwallet

Mnemonic-message

Build a message that describes a generated mnemonic.

Signature

(mnemonic-message mnemonic) → msg

Arguments

mnemonic — Guard (stringp mnemonic).

Returns

msg — Type (msgp msg).

When initializing a wallet from an entropy value, a mnemonic is generated, which is a non-empty string of words separated by individual spaces. This mnemonic must be shown to the user, as the result of running the command to initialize the wallet (from an entropy value).

This function builds a message that consists of the list of words, one per line, indented by two spaces.

Definitions and Theorems

Function: mnemonic-message-aux

(defun mnemonic-message-aux (words)
  (declare (xargs :guard (string-listp words)))
  (cond ((endp words) "")
        (t (msg "  ~s0~%~@1" (car words)
                (mnemonic-message-aux (cdr words))))))

Theorem: msgp-of-mnemonic-message-aux

(defthm msgp-of-mnemonic-message-aux
  (b* ((msg (mnemonic-message-aux words)))
    (msgp msg))
  :rule-classes :rewrite)

Function: mnemonic-message

(defun mnemonic-message (mnemonic)
  (declare (xargs :guard (stringp mnemonic)))
  (mnemonic-message-aux (strtok mnemonic (list #\Space))))

Theorem: msgp-of-mnemonic-message

(defthm msgp-of-mnemonic-message
  (b* ((msg (mnemonic-message mnemonic)))
    (msgp msg))
  :rule-classes :rewrite)