		Search-engine friendly clone of the ACL2 documentation.

Field-assert-eq

Field-assert-eq-correctness

Correctness of the circuit.

Soundness is proved by expanding the existentially quantified field equality assertion predicate to the field 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 field equality and truth assertion predicates and all the specifications, but we we use the suff theorem for the field 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: field-assert-eq-pred-soundness

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

Theorem: field-assert-eq-pred-completeness

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

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

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

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

(defthm field-assert-eq-circuit-to-spec
 (implies
  (and
      (equal (pfcs::lookup-definition (pfname "field_assert_eq")
                                      defs)
             (field-assert-eq-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_assert_true")
                                      defs)
             (boolean-assert-true-circuit))
      (equal (pfcs::lookup-definition (pfname "field_eq")
                                      defs)
             (field-eq-circuit))
      (equal (pfcs::lookup-definition (pfname "field_neq")
                                      defs)
             (field-neq-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_not")
                                      defs)
             (boolean-not-circuit))
      (primep prime)
      (pfield::fep x prime)
      (pfield::fep y prime))
  (equal (pfcs::definition-satp (pfname "field_assert_eq")
                                defs (list x y)
                                prime)
         (field-assert-eq-spec x y prime))))