		Search-engine friendly clone of the ACL2 documentation.

Fp-statusbits

!fp-statusbits->top

Update the |ACL2|::|TOP| field of a fp-statusbits bit structure.

Signature
(!fp-statusbits->top top x) → new-x
Arguments: top — Guard (3bits-p top).; x — Guard (fp-statusbits-p x).
Returns: new-x — Type (fp-statusbits-p new-x).

Definitions and Theorems

Function: !fp-statusbits->top$inline

(defun !fp-statusbits->top$inline (top x)
 (declare (xargs :guard (and (3bits-p top)
                             (fp-statusbits-p x))))
 (mbe
     :logic
     (b* ((top (mbe :logic (3bits-fix top) :exec top))
          (x (fp-statusbits-fix x)))
       (part-install top x :width 3 :low 11))
     :exec (the (unsigned-byte 16)
                (logior (the (unsigned-byte 16)
                             (logand (the (unsigned-byte 16) x)
                                     (the (signed-byte 15) -14337)))
                        (the (unsigned-byte 14)
                             (ash (the (unsigned-byte 3) top)
                                  11))))))

Theorem: fp-statusbits-p-of-!fp-statusbits->top

(defthm fp-statusbits-p-of-!fp-statusbits->top
  (b* ((new-x (!fp-statusbits->top$inline top x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->top$inline-of-3bits-fix-top

(defthm !fp-statusbits->top$inline-of-3bits-fix-top
  (equal (!fp-statusbits->top$inline (3bits-fix top)
                                     x)
         (!fp-statusbits->top$inline top x)))

Theorem: !fp-statusbits->top$inline-3bits-equiv-congruence-on-top

(defthm !fp-statusbits->top$inline-3bits-equiv-congruence-on-top
  (implies (3bits-equiv top top-equiv)
           (equal (!fp-statusbits->top$inline top x)
                  (!fp-statusbits->top$inline top-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->top$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->top$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->top$inline top (fp-statusbits-fix x))
         (!fp-statusbits->top$inline top x)))

Theorem: !fp-statusbits->top$inline-fp-statusbits-equiv-congruence-on-x

(defthm
     !fp-statusbits->top$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->top$inline top x)
                  (!fp-statusbits->top$inline top x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->top-is-fp-statusbits

(defthm !fp-statusbits->top-is-fp-statusbits
  (equal (!fp-statusbits->top top x)
         (change-fp-statusbits x :top top)))

Theorem: fp-statusbits->top-of-!fp-statusbits->top

(defthm fp-statusbits->top-of-!fp-statusbits->top
  (b* ((?new-x (!fp-statusbits->top$inline top x)))
    (equal (fp-statusbits->top new-x)
           (3bits-fix top))))

Theorem: !fp-statusbits->top-equiv-under-mask

(defthm !fp-statusbits->top-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->top$inline top x)))
    (fp-statusbits-equiv-under-mask new-x x -14337)))