• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
        • Bed-op-eval
        • Bed-op-fix
        • Bed-op-xor
        • Bed-op-true
        • Bed-op-orc2
        • Bed-op-orc1
        • Bed-op-not2
        • Bed-op-not1
        • Bed-op-nor
        • Bed-op-nand
        • Bed-op-ior
        • Bed-op-false
        • Bed-op-eqv
        • Bed-op-arg2
        • Bed-op-arg1
        • Bed-op-andc2
        • Bed-op-andc1
        • Bed-op-and
        • Bed-op-fix$
      • Bed-from-aig
      • Bed-mk1
      • Bed-eval
      • Up
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bed-op-p

Bed-op-eval

Application of a BED operator to two bits.

Signature

(bed-op-eval op x y) → value

Arguments

op — Guard (bed-op-p op).

x — Guard (bitp x).

y — Guard (bitp y).

Returns

value — Type (bitp value).

This is just a truth-table lookup into the operator.

Definitions and Theorems

Function: bed-op-eval$inline

(defun bed-op-eval$inline (op x y)
  (declare (type (unsigned-byte 4) op)
           (type bit x)
           (type bit y))
  (declare (xargs :guard (and (bed-op-p op) (bitp x) (bitp y))))
  (declare (xargs :split-types t))
  (let ((__function__ 'bed-op-eval))
    (declare (ignorable __function__))
    (b* (((the (unsigned-byte 2) xshift)
          (ash (the bit (lbfix x)) 1))
         ((the (unsigned-byte 2) index)
          (logior xshift (the bit (lbfix y))))
         ((the (signed-byte 3) nindex) (- index))
         ((the (unsigned-byte 4) op-shifted)
          (ash (the (unsigned-byte 4)
                    (mbe :logic (bed-op-fix op) :exec op))
               nindex)))
      (the bit (logand 1 op-shifted)))))

Theorem: bitp-of-bed-op-eval

(defthm bitp-of-bed-op-eval
  (b* ((value (bed-op-eval$inline op x y)))
    (bitp value))
  :rule-classes :rewrite)

Theorem: bit-equiv-implies-equal-bed-op-eval-2

(defthm bit-equiv-implies-equal-bed-op-eval-2
  (implies (bit-equiv x x-equiv)
           (equal (bed-op-eval op x y)
                  (bed-op-eval op x-equiv y)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-bed-op-eval-3

(defthm bit-equiv-implies-equal-bed-op-eval-3
  (implies (bit-equiv y y-equiv)
           (equal (bed-op-eval op x y)
                  (bed-op-eval op x y-equiv)))
  :rule-classes (:congruence))

Theorem: bed-op-eval-of-bed-op-fix

(defthm bed-op-eval-of-bed-op-fix
  (equal (bed-op-eval (bed-op-fix op) x y)
         (bed-op-eval op x y)))

Theorem: bed-op-equiv-implies-equal-bed-op-eval-1

(defthm bed-op-equiv-implies-equal-bed-op-eval-1
  (implies (bed-op-equiv op op-equiv)
           (equal (bed-op-eval op x y)
                  (bed-op-eval op-equiv x y)))
  :rule-classes (:congruence))

Theorem: bed-op-eval-when-fix-is-exact

(defthm bed-op-eval-when-fix-is-exact
  (implies (and (equal (bed-op-fix op) x)
                (syntaxp (or (quotep x)
                             (and (consp x) (not (cdr x))))))
           (equal (bed-op-eval op left right)
                  (bed-op-eval x left right))))