Ensure that the wallet state file does not already exist.
(check-stat-file-absent state) → (mv error? state)
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''.
(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)))
(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)