• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
        • Defbytelist
        • Defbyte-standard-instances
        • Defbyte-ihs-theorems
        • Defbyte-implementation
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
      • Fty-extensions
      • Defsubtype
      • Defset
      • Deftypes
      • Specific-types
      • 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

• Fty-extensions
• Fty
• Unsigned-byte-p
• Signed-byte-p

Defbyte

Introduce a fixtype of unsigned or signed bytes of a specified size.

Introduction

Currently fixtypes can only be associated to unary predicates, but unsigned-byte-p and signed-byte-p are binary predicates.

This macro introduces unary recognizers, and associated fixtypes, of unsigned or signed bytes of specified sizes. It also generates various theorems, including some that relate the unary recognizers to the binary predicates.

Besides their use in fixtypes, the unary recognizers introduced by this macro support tau system reasoning.

General Form

(defbyte type
         :size ...
         :signed ...
         :pred ...
         :fix ...
         :equiv ...
         :parents ...
         :short ...
         :long ...
  )

Inputs

:type

A symbol that specifies the name of the fixtype.

:size

A term that specifies the size of the bytes in bits. This must be one of the following: (1) an explicit positive integer value; (2) a named constant whose value is a positive integer; (3) a call of a nullary function (defined or constrained) that is guard-verified and provably denotes a positive integer.

This input must be supplied; there is no default.

:signed

A boolean that specifies whether the bytes are unsigned (nil, the default) or signed (t).

:pred

A symbol that specifies the name of the fixtype's recognizer. If this is nil (the default), the name of the recognizer is type followed by -p.

:fix

A symbol that specifies the name of the fixtype's fixer. If this is nil (the default), the name of the fixer is type followed by -fix.

:equiv

A symbol that specifies the name of the fixtype's equivalence. If this is nil (the default), the name of the equivalence is type followed by -equiv.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the fixtype.

Generated Events

pred

The recognizer for the fixtype, guard-verified.

As a special case, if a function with this name already exists, it is not (re-)generated. This is mainly to accomodate the existing recognizers ACL2::bytep and ACL2::nibblep, but it is a more general mechanism.

booleanp-of-pred

A rewrite rule saying that pred is boolean-valued.

If pred already exists (see above), it is assumed that a theorem like this already exists as well: thus, this theorem is not (re-)generated.

pred-forward-binpred

A forward chaining rule from pred to the corresponding binary predicate unsigned-byte-p or signed-byte-p.

binpred-rewrite-pred

A rule that rewrites the binary predicate unsigned-byte-p or signed-byte-p to pred. This rule is disabled by default, but may be useful in some proofs. Since this is the converse of the definition of the unary recognizer, a theory invariant is also generated preventing the enabling of both this rule and the definition of the unary recognizer.

pred-compound-recognizer

A compound recognizer rule from pred to natp (if the :signed input is nil or integerp (if the :signed input is t.

fix

The fixer for the fixtype, guard-verified.

It fixes values outside of pred to 0.

pred-of-fix

A rewrite rule saying that fix always returns a value that satisfies pred.

fix-when-pred

A rewrite rule saying that fix disappears when its argument satisfies pred.

type
equiv

The fixtype, via a call of deffixtype that also introduces the equivalence equiv.

type-size-is-posp

When the size input is a unary function call, we also generate a rewrite and type prescription rule saying that the unary function call satisfies posp.

The above items are generated with XDOC documentation. If pred already exists (see above), it is assumed that an XDOC topic with the same name exists as well: thus, a subtopic of it is generated, named pred-additional-theorems and containing the theorems associated to pred.

Subtopics

Defbytelist

Introduce a fixtype of true lists of unsigned or signed bytes of a specified size.

Defbyte-standard-instances

Standard fixtypes of unsigned and signed bytes of various sizes, with some accompanying theorems.

Defbyte-ihs-theorems

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

Defbyte-implementation

Implementation of defbyte.