• 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

Crypto-hdwallet-executable

Executable version of the hierachical deterministic wallet for cryptocurrencies.

The wallet specification is mostly executable. We make it completely executable by including the following in this file, besides the wallet specification itself:

• The needed cryptographic executable attachments.
• The BIP 32 executable attachments.
• The raw Lisp code for some OSLIB utilities. See `Loading the library' on that manual page.