• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
        • Defbytelist
        • Defbyte-standard-instances
        • Defbyte-ihs-theorems
          • Defbyte-ihs-theorems-implementation
        • Defbyte-implementation
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Specific-types
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defomap
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defbyte

Defbyte-ihs-theorems

Introduce some theorems about a defbyte instance and functions in the IHS library.

Introduction

Since unsigned-byte-p and signed-byte-p have certain formal relations with functions in the IHS library, similar relations can be proved for instances of defbyte.

This macro automates this process, by including the IHS basic definitions and by generating theorems.

The reason for not having defbyte itself generate these theorems is to avoid always including IHS when using defbyte. Having a separate macro promotes greater modularity.

General Form

(defbyte-ihs-theorems type)

Inputs

type

A symbol that names a fixtype previously introduced via defbyte. This specifies the defbyte instance for which the theorems are generated.

Generated Events

bytep-of-loghead/logext-of-size

One of the following:

• If the defbyte instance is unsigned, a rewrite rule saying that (loghead size ...), where size is the byte size, satisfies the recognizer of the bytes.
• If the defbyte instance is signed, a rewrite rule saying that (logext size ...), where size is the byte size, satisfies the recognizer of the bytes.

loghead/logext-of-size-when-bytep

One of the following:

• If the defbyte instance is unsigned, a rewrite rule saying that (loghead size x), where size is the byte size, simplifies to x, when x satisfies the recognizer of the bytes.
• If the defbyte instance is signed, a rewrite rule saying that (logext size x), where size is the byte size, simplifies to x, when x satisfies the recognizer of the bytes.

logtail-of-size-when-bytep

One of the following:

• If the defbyte instance is unsigned, a rewrite rule saying that (logtail size x), where size is the byte size, simplifies to 0, when x satisfies the recognizer of the bytes.
• If the defbyte instance is signed, a rewrite rule saying that (logtail size x), where size is the byte size, simplifies to -1 if x is negative and to 0 otherwise, when x satisfies the recognizer of the bytes.

Subtopics

Defbyte-ihs-theorems-implementation

Implementation of defbyte-ihs-theorems.