		Search-engine friendly clone of the ACL2 documentation.

Gatesimp

Gatesimp->hashp

Access the |AIGNET|::|HASHP| field of a gatesimp bit structure.

Signature
(gatesimp->hashp x) → hashp
Arguments: x — Guard (gatesimp-p x).
Returns: hashp — Type (booleanp hashp).

Definitions and Theorems

Function: gatesimp->hashp

(defun gatesimp->hashp (x)
  (declare (xargs :guard (gatesimp-p x)))
  (mbe :logic
       (let ((x (gatesimp-fix x)))
         (bit->bool (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-gatesimp->hashp

(defthm booleanp-of-gatesimp->hashp
  (b* ((hashp (gatesimp->hashp x)))
    (booleanp hashp))
  :rule-classes :rewrite)

Theorem: gatesimp->hashp-of-gatesimp-fix-x

(defthm gatesimp->hashp-of-gatesimp-fix-x
  (equal (gatesimp->hashp (gatesimp-fix x))
         (gatesimp->hashp x)))

Theorem: gatesimp->hashp-gatesimp-equiv-congruence-on-x

(defthm gatesimp->hashp-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (gatesimp->hashp x)
                  (gatesimp->hashp x-equiv)))
  :rule-classes :congruence)

Theorem: gatesimp->hashp-of-gatesimp

(defthm gatesimp->hashp-of-gatesimp
  (equal (gatesimp->hashp (gatesimp hashp level xor-mode))
         (acl2::bool-fix hashp)))

Theorem: gatesimp->hashp-of-write-with-mask

(defthm gatesimp->hashp-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x gatesimp-equiv-under-mask)
   (gatesimp-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 1) 0))
  (equal (gatesimp->hashp x)
         (gatesimp->hashp acl2::y))))