Possible sizes of the entropy in bits.
These are the possible values of
This is an ordinary std::defenum.
Function:
(defun bip39-entropy-size-p (x) (declare (xargs :guard t)) (or (eql x '128) (eql x '160) (eql x '192) (eql x '224) (eql x '256)))
Theorem: type-when-bip39-entropy-size-p
(defthm type-when-bip39-entropy-size-p (implies (bip39-entropy-size-p x) (if (integerp x) (< '1 x) 'nil)) :rule-classes :compound-recognizer)