		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Check-stat-file-present

Ensure that the wallet state file exists.

Signature
(check-stat-file-present state) → (mv error? state)
Returns: error? — Type (maybe-command-error-p error?).

Except for the initialization commands, the other wallet commands need to first read the wallet state from the file. Those commands call this function for that purpose.

This function returns nil as first result if the file exists (i.e. no error); otherwise, it returns an error indicating the absence of the file. A different error is returned if the ACL2 function to test whether the file exists fails (that is, the file's existence cannot be tested); this should be a rare event.

If the file exists, we also check that it is a regular file.

Definitions and Theorems

Function: check-stat-file-present

(defun check-stat-file-present (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))
       ((unless file-existsp)
        (mv (command-error-state-file-absent)
            state))
       ((mv err kind state)
        (file-kind *stat-filepath*
                   :follow-symlinks t))
       ((when (or err (not (eq kind :regular-file))))
        (mv (command-error-state-file-not-regular)
            state)))
    (mv nil state)))

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

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