		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-eq

Boolean-assert-eq-correctness

Correctness of the circuit.

Soundness is proved by expanding the existentially quantified boolean equality assertion predicate to the boolean equality and truth assertion predicates, using the correcness theorems of the latter two, and expanding all three specifications.

Completeness is proved also by expanding the boolean equality and truth assertion predicates and all the specifications, but we we use the suff theorem for the boolean equality assertion predicate. The witness for the existential quantification is the result of comparing the two operands for equality.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: boolean-assert-eq-pred-soundness

(defthm boolean-assert-eq-pred-soundness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (bitp x)
                (bitp y))
           (implies (boolean-assert-eq-pred x y prime)
                    (boolean-assert-eq-spec x y prime))))

Theorem: boolean-assert-eq-pred-completeness

(defthm boolean-assert-eq-pred-completeness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (bitp x)
                (bitp y))
           (implies (boolean-assert-eq-spec x y prime)
                    (boolean-assert-eq-pred x y prime))))

Theorem: boolean-assert-eq-pred-to-spec

(defthm boolean-assert-eq-pred-to-spec
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (bitp x)
                (bitp y))
           (equal (boolean-assert-eq-pred x y prime)
                  (boolean-assert-eq-spec x y prime))))

Theorem: boolean-assert-eq-circuit-to-spec

(defthm boolean-assert-eq-circuit-to-spec
 (implies
  (and
      (equal (pfcs::lookup-definition (pfname "boolean_assert_eq")
                                      defs)
             (boolean-assert-eq-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_assert_true")
                                      defs)
             (boolean-assert-true-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_eq")
                                      defs)
             (boolean-eq-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_neq")
                                      defs)
             (boolean-neq-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_not")
                                      defs)
             (boolean-not-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_xor")
                                      defs)
             (boolean-xor-circuit))
      (primep prime)
      (pfield::fep x prime)
      (pfield::fep y prime)
      (bitp x)
      (bitp y))
  (equal (pfcs::definition-satp (pfname "boolean_assert_eq")
                                defs (list x y)
                                prime)
         (boolean-assert-eq-spec x y prime))))