Discussion on how to use unsigned-byte-p

Unsigned-byte-p (and signed-byte-p for that matter) are tricky enough that there is no one-size-fits-all solution that everyone should use to reason about them. Depending on your problem you might try any of these strategies:

*Arithmetic*-- Leave unsigned-byte-p's regular definition enabled and try to reason about the resulting inequalities. This sometimes works and may be a good approach if you have goals involving "non bit-vector functions" like +, *, /, etc. I usually don't use this approach but I haven't done a lot of proofs about true arithmetic functions.*Induction*-- Disable unsigned-byte-p's regular definition but instead enable an alternate definition, e.g., the centaur/bitops/ihsext-basics book has unsigned-byte-p**, which is a recursive version that works well for induction. This definition is in the ihsext-recursive-redefs ruleset and also works well with other ** definitions like logand**. This is often a good strategy when proving lemmas about unsigned-byte-p but is probably mainly useful when reasoning about new recursive functions.*Vector*-- Leave unsigned-byte-p disabled except to prove lemmas, and expect to reason about (unsigned-byte-p n x) via lemmas. I think I usually prefer this strategy as it feels more reliable/less magical than reasoning about arithmetic inequalities. Some useful books:- bitops/ihsext-basics proves the nice/obvious lemmas about signed/unsigned-byte-p on many bit-vector functions like logior, logand, etc.
- bitops/signed-byte-p has lemmas about signed/unsigned-byte-p for some arithmetic functions (+, -, *) and also extended lemmas about bit-vector stuff. It's often very handy for the kinds of guard obligations that arise from things like (the (unsigned-byte 32) x).

We have occasionally written wrapper functions like

In the context of FTY, I don't think you need wrappers, but if for some
reason you do want to use them then that is probably basically fine. Note
here that you have some choice for your fixing function. You can fix to 0 as
you've done in your examples, but you might instead prefer to fix to

That said, it should be possible to get by without wrappers; see for instance the definition of sizednum in centaur/fty/deftypes-tests.lisp, or the definition of vl-constint in centaur/vl/expr.lisp, both of which use a loghead-based approach to do the fixing. (The vl-constint example has a :require that is an inequality instead of an unsigned-byte-p term, but I don't think there's any particular reason to do it this way instead of the other.)

In general there is good reason to expect it to sometimes be hard to work
with unsigned-byte-p. For instance, consider a theorem like the following,
from

(defthm lousy-unsigned-byte-p-of-*-mixed ;; Probably won't ever unify with anything. (implies (and (unsigned-byte-p n1 a) (unsigned-byte-p n2 b)) (unsigned-byte-p (+ n1 n2) (* a b))) :hints(("Goal" :use ((:instance upper-bound)))))

This would be a good rule to try on goals like

If you find yourself going down this road, you might see in particular Dave Greve's "Parameterized Congruences" paper from the 2006 workshop, which is implemented in the coi/nary/nary.lisp book. You could also look at Sol Swords' book to do something similar, see contextual-rewriting.