		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Interp-flags

An 6-bit unsigned bitstruct type.

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 6-bit integer.

Fields

intro-bvars — boolean
intro-synvars — boolean
simplify-logic — boolean
trace-rewrites — boolean
make-ites — boolean
branch-on-ifs — boolean

Definitions and Theorems

Function: interp-flags-p

(defun interp-flags-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'interp-flags-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 6 x)
         :exec (and (natp x) (< x 64)))))

Theorem: interp-flags-p-when-unsigned-byte-p

(defthm interp-flags-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 6 x)
           (interp-flags-p x)))

Theorem: unsigned-byte-p-when-interp-flags-p

(defthm unsigned-byte-p-when-interp-flags-p
  (implies (interp-flags-p x)
           (unsigned-byte-p 6 x)))

Theorem: interp-flags-p-compound-recognizer

(defthm interp-flags-p-compound-recognizer
  (implies (interp-flags-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: interp-flags-fix

(defun interp-flags-fix (x)
  (declare (xargs :guard (interp-flags-p x)))
  (let ((__function__ 'interp-flags-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 6 x) :exec x)))

Theorem: interp-flags-p-of-interp-flags-fix

(defthm interp-flags-p-of-interp-flags-fix
  (b* ((fty::fixed (interp-flags-fix x)))
    (interp-flags-p fty::fixed))
  :rule-classes :rewrite)

Theorem: interp-flags-fix-when-interp-flags-p

(defthm interp-flags-fix-when-interp-flags-p
  (implies (interp-flags-p x)
           (equal (interp-flags-fix x) x)))

Function: interp-flags-equiv$inline

(defun interp-flags-equiv$inline (x y)
  (declare (xargs :guard (and (interp-flags-p x)
                              (interp-flags-p y))))
  (equal (interp-flags-fix x)
         (interp-flags-fix y)))

Theorem: interp-flags-equiv-is-an-equivalence

(defthm interp-flags-equiv-is-an-equivalence
  (and (booleanp (interp-flags-equiv x y))
       (interp-flags-equiv x x)
       (implies (interp-flags-equiv x y)
                (interp-flags-equiv y x))
       (implies (and (interp-flags-equiv x y)
                     (interp-flags-equiv y z))
                (interp-flags-equiv x z)))
  :rule-classes (:equivalence))

Theorem: interp-flags-equiv-implies-equal-interp-flags-fix-1

(defthm interp-flags-equiv-implies-equal-interp-flags-fix-1
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags-fix x)
                  (interp-flags-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: interp-flags-fix-under-interp-flags-equiv

(defthm interp-flags-fix-under-interp-flags-equiv
  (interp-flags-equiv (interp-flags-fix x)
                      x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: interp-flags-fix-of-interp-flags-fix-x

(defthm interp-flags-fix-of-interp-flags-fix-x
  (equal (interp-flags-fix (interp-flags-fix x))
         (interp-flags-fix x)))

Theorem: interp-flags-fix-interp-flags-equiv-congruence-on-x

(defthm interp-flags-fix-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags-fix x)
                  (interp-flags-fix x-equiv)))
  :rule-classes :congruence)

Function: interp-flags

(defun interp-flags
       (intro-bvars intro-synvars simplify-logic
                    trace-rewrites make-ites branch-on-ifs)
 (declare (xargs :guard (and (booleanp intro-bvars)
                             (booleanp intro-synvars)
                             (booleanp simplify-logic)
                             (booleanp trace-rewrites)
                             (booleanp make-ites)
                             (booleanp branch-on-ifs))))
 (let ((__function__ 'interp-flags))
  (declare (ignorable __function__))
  (b* ((intro-bvars (bool->bit intro-bvars))
       (intro-synvars (bool->bit intro-synvars))
       (simplify-logic (bool->bit simplify-logic))
       (trace-rewrites (bool->bit trace-rewrites))
       (make-ites (bool->bit make-ites))
       (branch-on-ifs (bool->bit branch-on-ifs)))
   (logapp
      1 intro-bvars
      (logapp
           1 intro-synvars
           (logapp 1 simplify-logic
                   (logapp 1 trace-rewrites
                           (logapp 1 make-ites branch-on-ifs))))))))

Theorem: interp-flags-p-of-interp-flags

(defthm interp-flags-p-of-interp-flags
  (b* ((interp-flags (interp-flags intro-bvars intro-synvars
                                   simplify-logic trace-rewrites
                                   make-ites branch-on-ifs)))
    (interp-flags-p interp-flags))
  :rule-classes :rewrite)

Theorem: interp-flags-of-bool-fix-intro-bvars

(defthm interp-flags-of-bool-fix-intro-bvars
  (equal (interp-flags (bool-fix intro-bvars)
                       intro-synvars simplify-logic
                       trace-rewrites make-ites branch-on-ifs)
         (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites branch-on-ifs)))

Theorem: interp-flags-iff-congruence-on-intro-bvars

(defthm interp-flags-iff-congruence-on-intro-bvars
  (implies
       (iff intro-bvars intro-bvars-equiv)
       (equal (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs)
              (interp-flags intro-bvars-equiv intro-synvars
                            simplify-logic trace-rewrites
                            make-ites branch-on-ifs)))
  :rule-classes :congruence)

Theorem: interp-flags-of-bool-fix-intro-synvars

(defthm interp-flags-of-bool-fix-intro-synvars
  (equal (interp-flags intro-bvars (bool-fix intro-synvars)
                       simplify-logic
                       trace-rewrites make-ites branch-on-ifs)
         (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites branch-on-ifs)))

Theorem: interp-flags-iff-congruence-on-intro-synvars

(defthm interp-flags-iff-congruence-on-intro-synvars
  (implies
       (iff intro-synvars intro-synvars-equiv)
       (equal (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs)
              (interp-flags intro-bvars intro-synvars-equiv
                            simplify-logic trace-rewrites
                            make-ites branch-on-ifs)))
  :rule-classes :congruence)

Theorem: interp-flags-of-bool-fix-simplify-logic

(defthm interp-flags-of-bool-fix-simplify-logic
  (equal (interp-flags intro-bvars
                       intro-synvars (bool-fix simplify-logic)
                       trace-rewrites make-ites branch-on-ifs)
         (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites branch-on-ifs)))

Theorem: interp-flags-iff-congruence-on-simplify-logic

(defthm interp-flags-iff-congruence-on-simplify-logic
  (implies
       (iff simplify-logic simplify-logic-equiv)
       (equal (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs)
              (interp-flags intro-bvars intro-synvars
                            simplify-logic-equiv trace-rewrites
                            make-ites branch-on-ifs)))
  :rule-classes :congruence)

Theorem: interp-flags-of-bool-fix-trace-rewrites

(defthm interp-flags-of-bool-fix-trace-rewrites
  (equal (interp-flags intro-bvars intro-synvars
                       simplify-logic (bool-fix trace-rewrites)
                       make-ites branch-on-ifs)
         (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites branch-on-ifs)))

Theorem: interp-flags-iff-congruence-on-trace-rewrites

(defthm interp-flags-iff-congruence-on-trace-rewrites
  (implies
       (iff trace-rewrites trace-rewrites-equiv)
       (equal (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs)
              (interp-flags intro-bvars intro-synvars
                            simplify-logic trace-rewrites-equiv
                            make-ites branch-on-ifs)))
  :rule-classes :congruence)

Theorem: interp-flags-of-bool-fix-make-ites

(defthm interp-flags-of-bool-fix-make-ites
  (equal (interp-flags intro-bvars intro-synvars simplify-logic
                       trace-rewrites (bool-fix make-ites)
                       branch-on-ifs)
         (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites branch-on-ifs)))

Theorem: interp-flags-iff-congruence-on-make-ites

(defthm interp-flags-iff-congruence-on-make-ites
  (implies
       (iff make-ites make-ites-equiv)
       (equal (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs)
              (interp-flags intro-bvars intro-synvars
                            simplify-logic trace-rewrites
                            make-ites-equiv branch-on-ifs)))
  :rule-classes :congruence)

Theorem: interp-flags-of-bool-fix-branch-on-ifs

(defthm interp-flags-of-bool-fix-branch-on-ifs
  (equal (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites (bool-fix branch-on-ifs))
         (interp-flags intro-bvars intro-synvars
                       simplify-logic trace-rewrites
                       make-ites branch-on-ifs)))

Theorem: interp-flags-iff-congruence-on-branch-on-ifs

(defthm interp-flags-iff-congruence-on-branch-on-ifs
  (implies
       (iff branch-on-ifs branch-on-ifs-equiv)
       (equal (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs)
              (interp-flags intro-bvars intro-synvars
                            simplify-logic trace-rewrites
                            make-ites branch-on-ifs-equiv)))
  :rule-classes :congruence)

Function: interp-flags-equiv-under-mask

(defun interp-flags-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (interp-flags-p x)
                              (interp-flags-p x1)
                              (integerp mask))))
  (let ((__function__ 'interp-flags-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (interp-flags-fix x)
                               (interp-flags-fix x1)
                               mask)))

Theorem: interp-flags-equiv-under-mask-of-interp-flags-fix-x

(defthm interp-flags-equiv-under-mask-of-interp-flags-fix-x
  (equal (interp-flags-equiv-under-mask (interp-flags-fix x)
                                        x1 mask)
         (interp-flags-equiv-under-mask x x1 mask)))

Theorem: interp-flags-equiv-under-mask-interp-flags-equiv-congruence-on-x

(defthm
   interp-flags-equiv-under-mask-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags-equiv-under-mask x x1 mask)
                  (interp-flags-equiv-under-mask x-equiv x1 mask)))
  :rule-classes :congruence)

Theorem: interp-flags-equiv-under-mask-of-interp-flags-fix-x1

(defthm interp-flags-equiv-under-mask-of-interp-flags-fix-x1
  (equal (interp-flags-equiv-under-mask x (interp-flags-fix x1)
                                        mask)
         (interp-flags-equiv-under-mask x x1 mask)))

Theorem: interp-flags-equiv-under-mask-interp-flags-equiv-congruence-on-x1

(defthm
  interp-flags-equiv-under-mask-interp-flags-equiv-congruence-on-x1
  (implies (interp-flags-equiv x1 x1-equiv)
           (equal (interp-flags-equiv-under-mask x x1 mask)
                  (interp-flags-equiv-under-mask x x1-equiv mask)))
  :rule-classes :congruence)

Theorem: interp-flags-equiv-under-mask-of-ifix-mask

(defthm interp-flags-equiv-under-mask-of-ifix-mask
  (equal (interp-flags-equiv-under-mask x x1 (ifix mask))
         (interp-flags-equiv-under-mask x x1 mask)))

Theorem: interp-flags-equiv-under-mask-int-equiv-congruence-on-mask

(defthm interp-flags-equiv-under-mask-int-equiv-congruence-on-mask
  (implies (acl2::int-equiv mask mask-equiv)
           (equal (interp-flags-equiv-under-mask x x1 mask)
                  (interp-flags-equiv-under-mask x x1 mask-equiv)))
  :rule-classes :congruence)

Function: interp-flags->intro-bvars

(defun interp-flags->intro-bvars (x)
  (declare (xargs :guard (interp-flags-p x)))
  (mbe :logic
       (let ((x (interp-flags-fix x)))
         (bit->bool (acl2::part-select x :low 0 :width 1)))
       :exec (bit->bool (the (unsigned-byte 1)
                             (logand (the (unsigned-byte 1) 1)
                                     (the (unsigned-byte 6) x))))))

Theorem: booleanp-of-interp-flags->intro-bvars

(defthm booleanp-of-interp-flags->intro-bvars
  (b* ((intro-bvars (interp-flags->intro-bvars x)))
    (booleanp intro-bvars))
  :rule-classes :rewrite)

Theorem: interp-flags->intro-bvars-of-interp-flags-fix-x

(defthm interp-flags->intro-bvars-of-interp-flags-fix-x
  (equal (interp-flags->intro-bvars (interp-flags-fix x))
         (interp-flags->intro-bvars x)))

Theorem: interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x

(defthm interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags->intro-bvars x)
                  (interp-flags->intro-bvars x-equiv)))
  :rule-classes :congruence)

Theorem: interp-flags->intro-bvars-of-interp-flags

(defthm interp-flags->intro-bvars-of-interp-flags
  (equal (interp-flags->intro-bvars
              (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs))
         (bool-fix intro-bvars)))

Theorem: interp-flags->intro-bvars-of-write-with-mask

(defthm interp-flags->intro-bvars-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x interp-flags-equiv-under-mask)
                (interp-flags-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 1) 0))
           (equal (interp-flags->intro-bvars x)
                  (interp-flags->intro-bvars y))))

Function: interp-flags->intro-synvars

(defun interp-flags->intro-synvars (x)
 (declare (xargs :guard (interp-flags-p x)))
 (mbe
     :logic
     (let ((x (interp-flags-fix x)))
       (bit->bool (acl2::part-select x :low 1 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 5)
                            (ash (the (unsigned-byte 6) x) -1)))))))

Theorem: booleanp-of-interp-flags->intro-synvars

(defthm booleanp-of-interp-flags->intro-synvars
  (b* ((intro-synvars (interp-flags->intro-synvars x)))
    (booleanp intro-synvars))
  :rule-classes :rewrite)

Theorem: interp-flags->intro-synvars-of-interp-flags-fix-x

(defthm interp-flags->intro-synvars-of-interp-flags-fix-x
  (equal (interp-flags->intro-synvars (interp-flags-fix x))
         (interp-flags->intro-synvars x)))

Theorem: interp-flags->intro-synvars-interp-flags-equiv-congruence-on-x

(defthm
     interp-flags->intro-synvars-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags->intro-synvars x)
                  (interp-flags->intro-synvars x-equiv)))
  :rule-classes :congruence)

Theorem: interp-flags->intro-synvars-of-interp-flags

(defthm interp-flags->intro-synvars-of-interp-flags
  (equal (interp-flags->intro-synvars
              (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs))
         (bool-fix intro-synvars)))

Theorem: interp-flags->intro-synvars-of-write-with-mask

(defthm interp-flags->intro-synvars-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x interp-flags-equiv-under-mask)
                (interp-flags-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 2) 0))
           (equal (interp-flags->intro-synvars x)
                  (interp-flags->intro-synvars y))))

Function: interp-flags->simplify-logic

(defun interp-flags->simplify-logic (x)
 (declare (xargs :guard (interp-flags-p x)))
 (mbe
     :logic
     (let ((x (interp-flags-fix x)))
       (bit->bool (acl2::part-select x :low 2 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 4)
                            (ash (the (unsigned-byte 6) x) -2)))))))

Theorem: booleanp-of-interp-flags->simplify-logic

(defthm booleanp-of-interp-flags->simplify-logic
  (b* ((simplify-logic (interp-flags->simplify-logic x)))
    (booleanp simplify-logic))
  :rule-classes :rewrite)

Theorem: interp-flags->simplify-logic-of-interp-flags-fix-x

(defthm interp-flags->simplify-logic-of-interp-flags-fix-x
  (equal (interp-flags->simplify-logic (interp-flags-fix x))
         (interp-flags->simplify-logic x)))

Theorem: interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x

(defthm
    interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags->simplify-logic x)
                  (interp-flags->simplify-logic x-equiv)))
  :rule-classes :congruence)

Theorem: interp-flags->simplify-logic-of-interp-flags

(defthm interp-flags->simplify-logic-of-interp-flags
  (equal (interp-flags->simplify-logic
              (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs))
         (bool-fix simplify-logic)))

Theorem: interp-flags->simplify-logic-of-write-with-mask

(defthm interp-flags->simplify-logic-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x interp-flags-equiv-under-mask)
                (interp-flags-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4) 0))
           (equal (interp-flags->simplify-logic x)
                  (interp-flags->simplify-logic y))))

Function: interp-flags->trace-rewrites

(defun interp-flags->trace-rewrites (x)
 (declare (xargs :guard (interp-flags-p x)))
 (mbe
     :logic
     (let ((x (interp-flags-fix x)))
       (bit->bool (acl2::part-select x :low 3 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 3)
                            (ash (the (unsigned-byte 6) x) -3)))))))

Theorem: booleanp-of-interp-flags->trace-rewrites

(defthm booleanp-of-interp-flags->trace-rewrites
  (b* ((trace-rewrites (interp-flags->trace-rewrites x)))
    (booleanp trace-rewrites))
  :rule-classes :rewrite)

Theorem: interp-flags->trace-rewrites-of-interp-flags-fix-x

(defthm interp-flags->trace-rewrites-of-interp-flags-fix-x
  (equal (interp-flags->trace-rewrites (interp-flags-fix x))
         (interp-flags->trace-rewrites x)))

Theorem: interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x

(defthm
    interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags->trace-rewrites x)
                  (interp-flags->trace-rewrites x-equiv)))
  :rule-classes :congruence)

Theorem: interp-flags->trace-rewrites-of-interp-flags

(defthm interp-flags->trace-rewrites-of-interp-flags
  (equal (interp-flags->trace-rewrites
              (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs))
         (bool-fix trace-rewrites)))

Theorem: interp-flags->trace-rewrites-of-write-with-mask

(defthm interp-flags->trace-rewrites-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x interp-flags-equiv-under-mask)
                (interp-flags-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 8) 0))
           (equal (interp-flags->trace-rewrites x)
                  (interp-flags->trace-rewrites y))))

Function: interp-flags->make-ites

(defun interp-flags->make-ites (x)
 (declare (xargs :guard (interp-flags-p x)))
 (mbe
     :logic
     (let ((x (interp-flags-fix x)))
       (bit->bool (acl2::part-select x :low 4 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 2)
                            (ash (the (unsigned-byte 6) x) -4)))))))

Theorem: booleanp-of-interp-flags->make-ites

(defthm booleanp-of-interp-flags->make-ites
  (b* ((make-ites (interp-flags->make-ites x)))
    (booleanp make-ites))
  :rule-classes :rewrite)

Theorem: interp-flags->make-ites-of-interp-flags-fix-x

(defthm interp-flags->make-ites-of-interp-flags-fix-x
  (equal (interp-flags->make-ites (interp-flags-fix x))
         (interp-flags->make-ites x)))

Theorem: interp-flags->make-ites-interp-flags-equiv-congruence-on-x

(defthm interp-flags->make-ites-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags->make-ites x)
                  (interp-flags->make-ites x-equiv)))
  :rule-classes :congruence)

Theorem: interp-flags->make-ites-of-interp-flags

(defthm interp-flags->make-ites-of-interp-flags
  (equal (interp-flags->make-ites
              (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs))
         (bool-fix make-ites)))

Theorem: interp-flags->make-ites-of-write-with-mask

(defthm interp-flags->make-ites-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x interp-flags-equiv-under-mask)
                (interp-flags-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 16)
                       0))
           (equal (interp-flags->make-ites x)
                  (interp-flags->make-ites y))))

Function: interp-flags->branch-on-ifs

(defun interp-flags->branch-on-ifs (x)
 (declare (xargs :guard (interp-flags-p x)))
 (mbe
     :logic
     (let ((x (interp-flags-fix x)))
       (bit->bool (acl2::part-select x :low 5 :width 1)))
     :exec
     (bit->bool
          (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 1)
                            (ash (the (unsigned-byte 6) x) -5)))))))

Theorem: booleanp-of-interp-flags->branch-on-ifs

(defthm booleanp-of-interp-flags->branch-on-ifs
  (b* ((branch-on-ifs (interp-flags->branch-on-ifs x)))
    (booleanp branch-on-ifs))
  :rule-classes :rewrite)

Theorem: interp-flags->branch-on-ifs-of-interp-flags-fix-x

(defthm interp-flags->branch-on-ifs-of-interp-flags-fix-x
  (equal (interp-flags->branch-on-ifs (interp-flags-fix x))
         (interp-flags->branch-on-ifs x)))

Theorem: interp-flags->branch-on-ifs-interp-flags-equiv-congruence-on-x

(defthm
     interp-flags->branch-on-ifs-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags->branch-on-ifs x)
                  (interp-flags->branch-on-ifs x-equiv)))
  :rule-classes :congruence)

Theorem: interp-flags->branch-on-ifs-of-interp-flags

(defthm interp-flags->branch-on-ifs-of-interp-flags
  (equal (interp-flags->branch-on-ifs
              (interp-flags intro-bvars intro-synvars simplify-logic
                            trace-rewrites make-ites branch-on-ifs))
         (bool-fix branch-on-ifs)))

Theorem: interp-flags->branch-on-ifs-of-write-with-mask

(defthm interp-flags->branch-on-ifs-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x interp-flags-equiv-under-mask)
                (interp-flags-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 32)
                       0))
           (equal (interp-flags->branch-on-ifs x)
                  (interp-flags->branch-on-ifs y))))

Theorem: interp-flags-fix-in-terms-of-interp-flags

(defthm interp-flags-fix-in-terms-of-interp-flags
  (equal (interp-flags-fix x)
         (change-interp-flags x)))

Function: !interp-flags->intro-bvars

(defun !interp-flags->intro-bvars (intro-bvars x)
  (declare (xargs :guard (and (booleanp intro-bvars)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((intro-bvars (bool->bit intro-bvars))
            (x (interp-flags-fix x)))
         (acl2::part-install intro-bvars x
                             :width 1
                             :low 0))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 2) -2)))
                          (the (unsigned-byte 1)
                               (bool->bit intro-bvars))))))

Theorem: interp-flags-p-of-!interp-flags->intro-bvars

(defthm interp-flags-p-of-!interp-flags->intro-bvars
  (b* ((new-x (!interp-flags->intro-bvars intro-bvars x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->intro-bvars-of-bool-fix-intro-bvars

(defthm !interp-flags->intro-bvars-of-bool-fix-intro-bvars
  (equal (!interp-flags->intro-bvars (bool-fix intro-bvars)
                                     x)
         (!interp-flags->intro-bvars intro-bvars x)))

Theorem: !interp-flags->intro-bvars-iff-congruence-on-intro-bvars

(defthm !interp-flags->intro-bvars-iff-congruence-on-intro-bvars
  (implies (iff intro-bvars intro-bvars-equiv)
           (equal (!interp-flags->intro-bvars intro-bvars x)
                  (!interp-flags->intro-bvars intro-bvars-equiv x)))
  :rule-classes :congruence)

Theorem: !interp-flags->intro-bvars-of-interp-flags-fix-x

(defthm !interp-flags->intro-bvars-of-interp-flags-fix-x
  (equal
       (!interp-flags->intro-bvars intro-bvars (interp-flags-fix x))
       (!interp-flags->intro-bvars intro-bvars x)))

Theorem: !interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x

(defthm
      !interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (!interp-flags->intro-bvars intro-bvars x)
                  (!interp-flags->intro-bvars intro-bvars x-equiv)))
  :rule-classes :congruence)

Theorem: !interp-flags->intro-bvars-is-interp-flags

(defthm !interp-flags->intro-bvars-is-interp-flags
  (equal (!interp-flags->intro-bvars intro-bvars x)
         (change-interp-flags x
                              :intro-bvars intro-bvars)))

Theorem: interp-flags->intro-bvars-of-!interp-flags->intro-bvars

(defthm interp-flags->intro-bvars-of-!interp-flags->intro-bvars
  (b* ((?new-x (!interp-flags->intro-bvars intro-bvars x)))
    (equal (interp-flags->intro-bvars new-x)
           (bool-fix intro-bvars))))

Theorem: !interp-flags->intro-bvars-equiv-under-mask

(defthm !interp-flags->intro-bvars-equiv-under-mask
  (b* ((?new-x (!interp-flags->intro-bvars intro-bvars x)))
    (interp-flags-equiv-under-mask new-x x -2)))

Function: !interp-flags->intro-synvars

(defun !interp-flags->intro-synvars (intro-synvars x)
  (declare (xargs :guard (and (booleanp intro-synvars)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((intro-synvars (bool->bit intro-synvars))
            (x (interp-flags-fix x)))
         (acl2::part-install intro-synvars x
                             :width 1
                             :low 1))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 3) -3)))
                          (the (unsigned-byte 2)
                               (ash (the (unsigned-byte 1)
                                         (bool->bit intro-synvars))
                                    1))))))

Theorem: interp-flags-p-of-!interp-flags->intro-synvars

(defthm interp-flags-p-of-!interp-flags->intro-synvars
  (b* ((new-x (!interp-flags->intro-synvars intro-synvars x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->intro-synvars-of-bool-fix-intro-synvars

(defthm !interp-flags->intro-synvars-of-bool-fix-intro-synvars
  (equal (!interp-flags->intro-synvars (bool-fix intro-synvars)
                                       x)
         (!interp-flags->intro-synvars intro-synvars x)))

Theorem: !interp-flags->intro-synvars-iff-congruence-on-intro-synvars

(defthm !interp-flags->intro-synvars-iff-congruence-on-intro-synvars
  (implies
       (iff intro-synvars intro-synvars-equiv)
       (equal (!interp-flags->intro-synvars intro-synvars x)
              (!interp-flags->intro-synvars intro-synvars-equiv x)))
  :rule-classes :congruence)

Theorem: !interp-flags->intro-synvars-of-interp-flags-fix-x

(defthm !interp-flags->intro-synvars-of-interp-flags-fix-x
 (equal
   (!interp-flags->intro-synvars intro-synvars (interp-flags-fix x))
   (!interp-flags->intro-synvars intro-synvars x)))

Theorem: !interp-flags->intro-synvars-interp-flags-equiv-congruence-on-x

(defthm
    !interp-flags->intro-synvars-interp-flags-equiv-congruence-on-x
  (implies
       (interp-flags-equiv x x-equiv)
       (equal (!interp-flags->intro-synvars intro-synvars x)
              (!interp-flags->intro-synvars intro-synvars x-equiv)))
  :rule-classes :congruence)

Theorem: !interp-flags->intro-synvars-is-interp-flags

(defthm !interp-flags->intro-synvars-is-interp-flags
  (equal (!interp-flags->intro-synvars intro-synvars x)
         (change-interp-flags x
                              :intro-synvars intro-synvars)))

Theorem: interp-flags->intro-synvars-of-!interp-flags->intro-synvars

(defthm interp-flags->intro-synvars-of-!interp-flags->intro-synvars
  (b* ((?new-x (!interp-flags->intro-synvars intro-synvars x)))
    (equal (interp-flags->intro-synvars new-x)
           (bool-fix intro-synvars))))

Theorem: !interp-flags->intro-synvars-equiv-under-mask

(defthm !interp-flags->intro-synvars-equiv-under-mask
  (b* ((?new-x (!interp-flags->intro-synvars intro-synvars x)))
    (interp-flags-equiv-under-mask new-x x -3)))

Function: !interp-flags->simplify-logic

(defun !interp-flags->simplify-logic (simplify-logic x)
  (declare (xargs :guard (and (booleanp simplify-logic)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((simplify-logic (bool->bit simplify-logic))
            (x (interp-flags-fix x)))
         (acl2::part-install simplify-logic x
                             :width 1
                             :low 2))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 4) -5)))
                          (the (unsigned-byte 3)
                               (ash (the (unsigned-byte 1)
                                         (bool->bit simplify-logic))
                                    2))))))

Theorem: interp-flags-p-of-!interp-flags->simplify-logic

(defthm interp-flags-p-of-!interp-flags->simplify-logic
  (b* ((new-x (!interp-flags->simplify-logic simplify-logic x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->simplify-logic-of-bool-fix-simplify-logic

(defthm !interp-flags->simplify-logic-of-bool-fix-simplify-logic
  (equal (!interp-flags->simplify-logic (bool-fix simplify-logic)
                                        x)
         (!interp-flags->simplify-logic simplify-logic x)))

Theorem: !interp-flags->simplify-logic-iff-congruence-on-simplify-logic

(defthm
     !interp-flags->simplify-logic-iff-congruence-on-simplify-logic
 (implies
     (iff simplify-logic simplify-logic-equiv)
     (equal (!interp-flags->simplify-logic simplify-logic x)
            (!interp-flags->simplify-logic simplify-logic-equiv x)))
 :rule-classes :congruence)

Theorem: !interp-flags->simplify-logic-of-interp-flags-fix-x

(defthm !interp-flags->simplify-logic-of-interp-flags-fix-x
  (equal (!interp-flags->simplify-logic
              simplify-logic (interp-flags-fix x))
         (!interp-flags->simplify-logic simplify-logic x)))

Theorem: !interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x

(defthm
   !interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x
 (implies
     (interp-flags-equiv x x-equiv)
     (equal (!interp-flags->simplify-logic simplify-logic x)
            (!interp-flags->simplify-logic simplify-logic x-equiv)))
 :rule-classes :congruence)

Theorem: !interp-flags->simplify-logic-is-interp-flags

(defthm !interp-flags->simplify-logic-is-interp-flags
  (equal (!interp-flags->simplify-logic simplify-logic x)
         (change-interp-flags x
                              :simplify-logic simplify-logic)))

Theorem: interp-flags->simplify-logic-of-!interp-flags->simplify-logic

(defthm
      interp-flags->simplify-logic-of-!interp-flags->simplify-logic
  (b* ((?new-x (!interp-flags->simplify-logic simplify-logic x)))
    (equal (interp-flags->simplify-logic new-x)
           (bool-fix simplify-logic))))

Theorem: !interp-flags->simplify-logic-equiv-under-mask

(defthm !interp-flags->simplify-logic-equiv-under-mask
  (b* ((?new-x (!interp-flags->simplify-logic simplify-logic x)))
    (interp-flags-equiv-under-mask new-x x -5)))

Function: !interp-flags->trace-rewrites

(defun !interp-flags->trace-rewrites (trace-rewrites x)
  (declare (xargs :guard (and (booleanp trace-rewrites)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((trace-rewrites (bool->bit trace-rewrites))
            (x (interp-flags-fix x)))
         (acl2::part-install trace-rewrites x
                             :width 1
                             :low 3))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 5) -9)))
                          (the (unsigned-byte 4)
                               (ash (the (unsigned-byte 1)
                                         (bool->bit trace-rewrites))
                                    3))))))

Theorem: interp-flags-p-of-!interp-flags->trace-rewrites

(defthm interp-flags-p-of-!interp-flags->trace-rewrites
  (b* ((new-x (!interp-flags->trace-rewrites trace-rewrites x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->trace-rewrites-of-bool-fix-trace-rewrites

(defthm !interp-flags->trace-rewrites-of-bool-fix-trace-rewrites
  (equal (!interp-flags->trace-rewrites (bool-fix trace-rewrites)
                                        x)
         (!interp-flags->trace-rewrites trace-rewrites x)))

Theorem: !interp-flags->trace-rewrites-iff-congruence-on-trace-rewrites

(defthm
     !interp-flags->trace-rewrites-iff-congruence-on-trace-rewrites
 (implies
     (iff trace-rewrites trace-rewrites-equiv)
     (equal (!interp-flags->trace-rewrites trace-rewrites x)
            (!interp-flags->trace-rewrites trace-rewrites-equiv x)))
 :rule-classes :congruence)

Theorem: !interp-flags->trace-rewrites-of-interp-flags-fix-x

(defthm !interp-flags->trace-rewrites-of-interp-flags-fix-x
  (equal (!interp-flags->trace-rewrites
              trace-rewrites (interp-flags-fix x))
         (!interp-flags->trace-rewrites trace-rewrites x)))

Theorem: !interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x

(defthm
   !interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x
 (implies
     (interp-flags-equiv x x-equiv)
     (equal (!interp-flags->trace-rewrites trace-rewrites x)
            (!interp-flags->trace-rewrites trace-rewrites x-equiv)))
 :rule-classes :congruence)

Theorem: !interp-flags->trace-rewrites-is-interp-flags

(defthm !interp-flags->trace-rewrites-is-interp-flags
  (equal (!interp-flags->trace-rewrites trace-rewrites x)
         (change-interp-flags x
                              :trace-rewrites trace-rewrites)))

Theorem: interp-flags->trace-rewrites-of-!interp-flags->trace-rewrites

(defthm
      interp-flags->trace-rewrites-of-!interp-flags->trace-rewrites
  (b* ((?new-x (!interp-flags->trace-rewrites trace-rewrites x)))
    (equal (interp-flags->trace-rewrites new-x)
           (bool-fix trace-rewrites))))

Theorem: !interp-flags->trace-rewrites-equiv-under-mask

(defthm !interp-flags->trace-rewrites-equiv-under-mask
  (b* ((?new-x (!interp-flags->trace-rewrites trace-rewrites x)))
    (interp-flags-equiv-under-mask new-x x -9)))

Function: !interp-flags->make-ites

(defun !interp-flags->make-ites (make-ites x)
  (declare (xargs :guard (and (booleanp make-ites)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((make-ites (bool->bit make-ites))
            (x (interp-flags-fix x)))
         (acl2::part-install make-ites x
                             :width 1
                             :low 4))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 6) -17)))
                          (the (unsigned-byte 5)
                               (ash (the (unsigned-byte 1)
                                         (bool->bit make-ites))
                                    4))))))

Theorem: interp-flags-p-of-!interp-flags->make-ites

(defthm interp-flags-p-of-!interp-flags->make-ites
  (b* ((new-x (!interp-flags->make-ites make-ites x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->make-ites-of-bool-fix-make-ites

(defthm !interp-flags->make-ites-of-bool-fix-make-ites
  (equal (!interp-flags->make-ites (bool-fix make-ites)
                                   x)
         (!interp-flags->make-ites make-ites x)))

Theorem: !interp-flags->make-ites-iff-congruence-on-make-ites

(defthm !interp-flags->make-ites-iff-congruence-on-make-ites
  (implies (iff make-ites make-ites-equiv)
           (equal (!interp-flags->make-ites make-ites x)
                  (!interp-flags->make-ites make-ites-equiv x)))
  :rule-classes :congruence)

Theorem: !interp-flags->make-ites-of-interp-flags-fix-x

(defthm !interp-flags->make-ites-of-interp-flags-fix-x
  (equal (!interp-flags->make-ites make-ites (interp-flags-fix x))
         (!interp-flags->make-ites make-ites x)))

Theorem: !interp-flags->make-ites-interp-flags-equiv-congruence-on-x

(defthm !interp-flags->make-ites-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (!interp-flags->make-ites make-ites x)
                  (!interp-flags->make-ites make-ites x-equiv)))
  :rule-classes :congruence)

Theorem: !interp-flags->make-ites-is-interp-flags

(defthm !interp-flags->make-ites-is-interp-flags
  (equal (!interp-flags->make-ites make-ites x)
         (change-interp-flags x
                              :make-ites make-ites)))

Theorem: interp-flags->make-ites-of-!interp-flags->make-ites

(defthm interp-flags->make-ites-of-!interp-flags->make-ites
  (b* ((?new-x (!interp-flags->make-ites make-ites x)))
    (equal (interp-flags->make-ites new-x)
           (bool-fix make-ites))))

Theorem: !interp-flags->make-ites-equiv-under-mask

(defthm !interp-flags->make-ites-equiv-under-mask
  (b* ((?new-x (!interp-flags->make-ites make-ites x)))
    (interp-flags-equiv-under-mask new-x x -17)))

Function: !interp-flags->branch-on-ifs

(defun !interp-flags->branch-on-ifs (branch-on-ifs x)
  (declare (xargs :guard (and (booleanp branch-on-ifs)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((branch-on-ifs (bool->bit branch-on-ifs))
            (x (interp-flags-fix x)))
         (acl2::part-install branch-on-ifs x
                             :width 1
                             :low 5))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 7) -33)))
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 1)
                                         (bool->bit branch-on-ifs))
                                    5))))))

Theorem: interp-flags-p-of-!interp-flags->branch-on-ifs

(defthm interp-flags-p-of-!interp-flags->branch-on-ifs
  (b* ((new-x (!interp-flags->branch-on-ifs branch-on-ifs x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->branch-on-ifs-of-bool-fix-branch-on-ifs

(defthm !interp-flags->branch-on-ifs-of-bool-fix-branch-on-ifs
  (equal (!interp-flags->branch-on-ifs (bool-fix branch-on-ifs)
                                       x)
         (!interp-flags->branch-on-ifs branch-on-ifs x)))

Theorem: !interp-flags->branch-on-ifs-iff-congruence-on-branch-on-ifs

(defthm !interp-flags->branch-on-ifs-iff-congruence-on-branch-on-ifs
  (implies
       (iff branch-on-ifs branch-on-ifs-equiv)
       (equal (!interp-flags->branch-on-ifs branch-on-ifs x)
              (!interp-flags->branch-on-ifs branch-on-ifs-equiv x)))
  :rule-classes :congruence)

Theorem: !interp-flags->branch-on-ifs-of-interp-flags-fix-x

(defthm !interp-flags->branch-on-ifs-of-interp-flags-fix-x
 (equal
   (!interp-flags->branch-on-ifs branch-on-ifs (interp-flags-fix x))
   (!interp-flags->branch-on-ifs branch-on-ifs x)))

Theorem: !interp-flags->branch-on-ifs-interp-flags-equiv-congruence-on-x

(defthm
    !interp-flags->branch-on-ifs-interp-flags-equiv-congruence-on-x
  (implies
       (interp-flags-equiv x x-equiv)
       (equal (!interp-flags->branch-on-ifs branch-on-ifs x)
              (!interp-flags->branch-on-ifs branch-on-ifs x-equiv)))
  :rule-classes :congruence)

Theorem: !interp-flags->branch-on-ifs-is-interp-flags

(defthm !interp-flags->branch-on-ifs-is-interp-flags
  (equal (!interp-flags->branch-on-ifs branch-on-ifs x)
         (change-interp-flags x
                              :branch-on-ifs branch-on-ifs)))

Theorem: interp-flags->branch-on-ifs-of-!interp-flags->branch-on-ifs

(defthm interp-flags->branch-on-ifs-of-!interp-flags->branch-on-ifs
  (b* ((?new-x (!interp-flags->branch-on-ifs branch-on-ifs x)))
    (equal (interp-flags->branch-on-ifs new-x)
           (bool-fix branch-on-ifs))))

Theorem: !interp-flags->branch-on-ifs-equiv-under-mask

(defthm !interp-flags->branch-on-ifs-equiv-under-mask
  (b* ((?new-x (!interp-flags->branch-on-ifs branch-on-ifs x)))
    (interp-flags-equiv-under-mask new-x x 31)))

Function: interp-flags-debug

(defun interp-flags-debug (x)
 (declare (xargs :guard (interp-flags-p x)))
 (let ((__function__ 'interp-flags-debug))
  (declare (ignorable __function__))
  (b* (((interp-flags x)))
   (cons
    (cons 'intro-bvars x.intro-bvars)
    (cons
       (cons 'intro-synvars x.intro-synvars)
       (cons (cons 'simplify-logic x.simplify-logic)
             (cons (cons 'trace-rewrites x.trace-rewrites)
                   (cons (cons 'make-ites x.make-ites)
                         (cons (cons 'branch-on-ifs x.branch-on-ifs)
                               nil)))))))))

Theorem: interp-flags-debug-of-interp-flags-fix-x

(defthm interp-flags-debug-of-interp-flags-fix-x
  (equal (interp-flags-debug (interp-flags-fix x))
         (interp-flags-debug x)))

Theorem: interp-flags-debug-interp-flags-equiv-congruence-on-x

(defthm interp-flags-debug-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (interp-flags-debug x)
                  (interp-flags-debug x-equiv)))
  :rule-classes :congruence)

Subtopics

!interp-flags->trace-rewrites: Update the |FGL|::|TRACE-REWRITES| field of a interp-flags bit structure.
!interp-flags->simplify-logic: Update the |FGL|::|SIMPLIFY-LOGIC| field of a interp-flags bit structure.
!interp-flags->intro-synvars: Update the |FGL|::|INTRO-SYNVARS| field of a interp-flags bit structure.
!interp-flags->branch-on-ifs: Update the |FGL|::|BRANCH-ON-IFS| field of a interp-flags bit structure.
!interp-flags->intro-bvars: Update the |FGL|::|INTRO-BVARS| field of a interp-flags bit structure.
!interp-flags->make-ites: Update the |FGL|::|MAKE-ITES| field of a interp-flags bit structure.
Interp-flags-fix: Fixing function for interp-flags bit structures.
Interp-flags-p: Recognizer for interp-flags bit structures.
Interp-flags->trace-rewrites: Access the |FGL|::|TRACE-REWRITES| field of a interp-flags bit structure.
Interp-flags->simplify-logic: Access the |FGL|::|SIMPLIFY-LOGIC| field of a interp-flags bit structure.
Interp-flags->branch-on-ifs: Access the |FGL|::|BRANCH-ON-IFS| field of a interp-flags bit structure.
Interp-flags->intro-synvars: Access the |FGL|::|INTRO-SYNVARS| field of a interp-flags bit structure.
Interp-flags->intro-bvars: Access the |FGL|::|INTRO-BVARS| field of a interp-flags bit structure.
Interp-flags->make-ites: Access the |FGL|::|MAKE-ITES| field of a interp-flags bit structure.