• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • 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
            • All-valid-key-paths-p
            • Process-sign
            • Process-init-from-entropy
            • 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*
          • Error-checking
          • Apt
          • Abnf
          • Fty-extensions
          • Isar
          • Kestrel-utilities
          • Prime-field-constraint-systems
          • Soft
          • Bv
          • Imp-language
          • Event-macros
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Java
          • C
          • Syntheto
          • Number-theory
          • Cryptography
          • Lists-light
          • File-io-light
          • Json
          • Built-ins
          • Solidity
          • Axe
          • Std-extensions
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • 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)