		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Stat-wfp

All the constraints on the wallet state.

Signature
(stat-wfp stat) → yes/no
Arguments: stat — Guard (statp stat).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: stat-wfp

(defun stat-wfp (stat)
  (declare (xargs :guard (statp stat)))
  (and (stat-addresses-bounded-p stat)
       (stat-priv-keys-p stat)
       (stat-root-depth-zero-p stat)
       (stat-path-prefix-in-tree-p stat)
       (stat-all-valid-key-paths-p stat)))

Theorem: booleanp-of-stat-wfp

(defthm booleanp-of-stat-wfp
  (b* ((yes/no (stat-wfp stat)))
    (booleanp yes/no))
  :rule-classes :rewrite)