• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
          • Basic-signed-byte-p-of-binary-minus
          • Basic-unsigned-byte-p-of-*
          • Basic-signed-byte-p-of-*
          • Basic-signed-byte-p-of-unary-minus
          • Basic-signed-byte-p-of-mixed-*
          • Basic-unsigned-byte-p-of-+-with-cin
          • Lousy-signed-byte-p-of-*
          • Lousy-signed-byte-p-of-mixed-*
          • Basic-signed-byte-p-of-+-with-cin
          • Basic-signed-byte-p-of-unary-minus-2
          • Lousy-unsigned-byte-p-of-*-mixed
          • Lousy-unsigned-byte-p-of-*
          • Basic-signed-byte-p-of-+
          • Basic-signed-byte-p-of-truncate-split
          • Basic-unsigned-byte-p-of-+
          • Basic-signed-byte-p-of-truncate
          • Basic-signed-byte-p-of-floor-split
          • Basic-signed-byte-p-of-floor
          • Unsigned-byte-p-of-minus-when-signed-byte-p
          • Signed-byte-p-of-decrement-when-natural-signed-byte-p
          • Unsigned-byte-p-of-abs-when-signed-byte-p
          • Signed-byte-p-when-unsigned-byte-p-smaller
          • Signed-byte-p-when-signed-byte-p-smaller
          • Signed-byte-p-of-loghead
          • Basic-unsigned-byte-p-of-truncate
          • Basic-unsigned-byte-p-of-rem
          • Basic-unsigned-byte-p-of-mod
          • Basic-unsigned-byte-p-of-floor
          • Basic-signed-byte-p-of-rem
          • Basic-signed-byte-p-of-mod
          • Basic-signed-byte-p-of-lognot
          • Basic-signed-byte-p-of-1+lognot
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops
• Signed-byte-p
• Unsigned-byte-p

Bitops/signed-byte-p

Lemmas about signed-byte-p and unsigned-byte-p that are often useful when optimizing definitions with ACL2::type-spec declarations.

Subtopics

Basic-signed-byte-p-of-binary-minus

Subtracting N-bit signeds creates an N+1 bit signed.

Basic-unsigned-byte-p-of-*

Multiplying constant N * N bit unsigneds creates an N+N bit unsigned.

Basic-signed-byte-p-of-*

Multiplying constant N * N bit signeds creates an N+N bit signed.

Basic-signed-byte-p-of-unary-minus

Negative N-bit signed is an N+1 bit signed.

Basic-signed-byte-p-of-mixed-*

Multiplying constant N-bit signed * N-bit unsigned creates an N+N bit signed.

Basic-unsigned-byte-p-of-+-with-cin

Adding N-bit unsigneds with a carry bit creates an N+1 bit unsigned.

Lousy-signed-byte-p-of-*

Multiplying N * N bit signeds creates an N+N bit signed.

Lousy-signed-byte-p-of-mixed-*

Multiplying N-bit signed * N-bit unsigned creates an N+N bit signed.

Basic-signed-byte-p-of-+-with-cin

Adding N+1 bit signeds with a carry bit creates an N+1 bit signed.

Basic-signed-byte-p-of-unary-minus-2

Negative N-bit unsigned is an N+1 bit signed.

Lousy-unsigned-byte-p-of-*-mixed

Multiplying N1 * N2 bit unsigneds creates an N1+N2 bit unsigned.

Lousy-unsigned-byte-p-of-*

Multiplying N * N bit unsigneds creates an N+N bit unsigned.

Basic-signed-byte-p-of-+

Adding N-bit signeds creates an N+1 bit signed.

Basic-signed-byte-p-of-truncate-split

Truncate of an N-bit signed by an integer is usually an N-bit signed. (Strong form, case splitting, disabled by default).

Basic-unsigned-byte-p-of-+

Adding N-bit unsigneds creates an N+1 bit unsigned.

Basic-signed-byte-p-of-truncate

Truncating an N-bit signed by an integer is usually an N-bit signed. (Weak form, enabled by default).

Basic-signed-byte-p-of-floor-split

Floor of an N-bit signed by an integer is usually an N-bit signed. (Strong form, case splitting, disabled by default).

Basic-signed-byte-p-of-floor

Floor of an N-bit signed by an integer is usually an N-bit signed. (Weak form, enabled by default).

Unsigned-byte-p-of-minus-when-signed-byte-p

Negating an N-bit signed creates an N-bit unsigned exactly when it was negative.

Signed-byte-p-of-decrement-when-natural-signed-byte-p

Decrementing a positive N-bit signed creates an N-bit signed.

Unsigned-byte-p-of-abs-when-signed-byte-p

Absolute value of an N-bit signed is an N-bit unsigned.

Signed-byte-p-when-unsigned-byte-p-smaller

An N-bit unsigned is an M-big signed for any M < N.

Signed-byte-p-when-signed-byte-p-smaller

An N-bit signed is an M-bit signed for any M >= N.

Signed-byte-p-of-loghead

An N-bit loghead is an M-bit signed for any M > N.

Basic-unsigned-byte-p-of-truncate

Truncate an N-bit unsigned by a natural creates an N-bit unsigned.

Basic-unsigned-byte-p-of-rem

Remainder of an N-bit unsigned by a natural creates an N-bit unsigned.

Basic-unsigned-byte-p-of-mod

Mod an N-bit unsigned by a natural creates an N-bit unsigned.

Basic-unsigned-byte-p-of-floor

Floor an N-bit unsigned by a natural creates an N-bit unsigned.

Basic-signed-byte-p-of-rem

Rem of N-bit signed by N-bit signed creates an N-bit signed.

Basic-signed-byte-p-of-mod

Mod of N-bit signed by N-bit signed creates an N-bit signed.

Basic-signed-byte-p-of-lognot

Lognot of an N-bit unsigned is an N+1 bit signed.

Basic-signed-byte-p-of-1+lognot

Lognot+1 (two's complement) of an N-bit unsigned is an N+1 bit signed.