		Search-engine friendly clone of the ACL2 documentation.

Field-square

Field-square-correctness

Correctness of the circuit.

The equivalence between predicate and specification is proved automatically, using the correctness theorem for the field-mul.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-square-pred-to-spec

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

Theorem: field-square-circuit-to-spec

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