• 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
      • Abnf
      • 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
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Crypto-hdwallet

Check-stat-file-absent

Ensure that the wallet state file does not already exist.

Signature

(check-stat-file-absent state) → (mv error? state)

Returns

error? — Type (maybe-command-error-p error?).

The initialization commands should not overwrite an existing wallet file. Thus, the initialization commands call this function to ensure that the file does not already exist.

This function is analogous to check-stat-file-present, with the check ``flipped''.

Definitions and Theorems

Function: check-stat-file-absent

(defun check-stat-file-absent (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (b* (((mv errmsg? file-existsp state)
        (path-exists-p *stat-filepath*))
       ((when errmsg?)
        (mv (command-error-state-file-untestable)
            state))
       ((when file-existsp)
        (mv (command-error-state-file-present)
            state)))
    (mv nil state)))

Theorem: maybe-command-error-p-of-check-stat-file-absent.error?

(defthm maybe-command-error-p-of-check-stat-file-absent.error?
  (b* (((mv ?error? acl2::?state)
        (check-stat-file-absent state)))
    (maybe-command-error-p error?))
  :rule-classes :rewrite)