Ensure that the wallet state file exists.
(check-stat-file-present state) → (mv error? state)
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
If the file exists, we also check that it is a regular file.
(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)))
(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)