• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Apply$
        • Defpkg
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Loop$-primer
        • Fast-alists
        • Defmacro
        • Defconst
        • Guard
        • Evaluation
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Developers-guide
        • Numbers
          • Natp
          • Unsigned-byte-p
            • Defbyte
            • Unsigned-byte-p-discussion
              • Unsigned-byte-listp
              • Bitops/signed-byte-p
              • Unsigned-byte-fix
              • Bytep
              • Nibblep
              • Ihs/unsigned-byte-p-lemmas
              • Unsigned-byte-p*
              • Unsigned-byte-p-basics
            • Posp
            • +
            • Bitp
            • Zero-test-idioms
            • Nat-listp
            • Integerp
            • <
            • *
            • Zp
            • -
            • Signed-byte-p
            • Logbitp
            • Expt
            • Ash
            • Rationalp
            • Sharp-f-reader
            • Logand
            • =
            • <=
            • Floor
            • Random$
            • Nfix
            • Truncate
            • Complex
            • Numbers-introduction
            • Code-char
            • Integer-length
            • Zip
            • Logior
            • Sharp-u-reader
            • Char-code
            • Unary--
            • Integer-listp
            • Boole$
            • /
            • Mod
            • Logxor
            • Lognot
            • Integer-range-p
            • Ifix
            • ACL2-numberp
            • Ceiling
            • Mod-expt
            • Round
            • Logeqv
            • Explode-nonnegative-integer
            • Max
            • Evenp
            • Nonnegative-integer-quotient
            • Zerop
            • Abs
            • Fix
            • Allocate-fixnum-range
            • Rem
            • 1+
            • Pos-listp
            • Signum
            • Real/rationalp
            • Rational-listp
            • Rfix
            • >=
            • >
            • Logcount
            • ACL2-number-listp
            • /=
            • Unary-/
            • Complex/complex-rationalp
            • Logtest
            • Logandc1
            • Logorc1
            • Logandc2
            • 1-
            • Numerator
            • Logorc2
            • Denominator
            • The-number
            • Realfix
            • Complex-rationalp
            • Min
            • Lognor
            • Zpf
            • Oddp
            • Minusp
            • Lognand
            • Imagpart
            • Conjugate
            • Int=
            • Realpart
            • Plusp
          • Irrelevant-formals
          • Efficiency
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Redefining-programs
          • Lists
          • Invariant-risk
          • Errors
          • Defabbrev
          • Conses
          • Alists
          • Set-register-invariant-risk
          • Strings
          • Program-wrapper
          • Get-internal-time
          • Basics
          • Packages
          • Defmacro-untouchable
          • Primitive
          • <<
          • Revert-world
          • Set-duplicate-keys-action
          • Unmemoize
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Defopen
          • Sleep
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Unsigned-byte-p

    Unsigned-byte-p-discussion

    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:

    1. 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.
    2. 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.
    3. 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:
      1. bitops/ihsext-basics proves the nice/obvious lemmas about signed/unsigned-byte-p on many bit-vector functions like logior, logand, etc.
      2. 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 u32p, but, I think that perhaps the only reason we did this was for macros like def-typed-record, where we needed a unary predicate to introduce a fancier data structure. Once we had the typed records in place, we just enabled these wrappers and did all our reasoning about unsigned-byte-p. (I don't think you'd want to reason about a each various u32p, u64p, etc., individually.)

    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 (loghead n x). Why? When you use loghead, it preserves the lower N bits, and this may interact much more nicely with rules about true bit-vector functions. This approach is also good for GL, where loghead is supported in an especially good way.

    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 centaur/bitops/signed-byte-p.lisp:

    (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 (unsigned-byte-p 10 (* a b)), but without some insight into a and b it's hard to know how to successfully instantiate N1/N2. So you end up resorting to :use hints, or special-case variants of this theorem (e.g., another theorem that says 7 bits * 3 bits --> 10 bits), or you do something more sophisticated with bind-free or similar.

    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.