		Search-engine friendly clone of the ACL2 documentation.

Field-mul

Field-mul-correctness

Correctness of the circuit.

The equivalence between predicate and specification is proved automatically, without even using the prime fields library rules.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-mul-pred-to-spec

(defthm field-mul-pred-to-spec
  (implies (and (primep p)
                (pfield::fep x p)
                (pfield::fep y p)
                (pfield::fep z p))
           (equal (field-mul-pred x y z prime)
                  (field-mul-spec x y z prime))))

Theorem: field-mul-circuit-to-spec

(defthm field-mul-circuit-to-spec
  (implies (and (equal (pfcs::lookup-definition (pfname "field_mul")
                                                defs)
                       (field-mul-circuit))
                (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime))
           (equal (pfcs::definition-satp (pfname "field_mul")
                                         defs (list x y z)
                                         prime)
                  (field-mul-spec x y z prime))))