		Search-engine friendly clone of the ACL2 documentation.

Stat-addresses-bounded-p

Constraint on the number of address keys in the wallet state.

Since all the address keys have non-hardened indices, the largest index is 2^{31}-1, so the maximum value of the addresses state component is 2^{31}.

Function: stat-addresses-bounded-p

(defun stat-addresses-bounded-p (stat)
  (declare (xargs :guard (statp stat)))
  (<= (stat->addresses stat) (expt 2 31)))

Theorem: booleanp-of-stat-addresses-bounded-p

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