		Search-engine friendly clone of the ACL2 documentation.

Field-div-checked

Field-div-checked-correctness

Correctness of the circuit.

Soundness is proved by expanding the predicate to the predicates for the called circuits, rewriting those to their specifications, and then expand all the specifications to show that they match. For that, we need to open pfield::div to expose pfield::inv, which is used by the specification for field inversion; but we also need to disable a prime fields library rule that interferes.

Completeness is proved by expanding all the specifications, the correctness theorems for the called circuits, and using the suff theorem to obtain the conclusion. We also need to enable pfield::div; but here there is no need to disable the rule disabled in the soundness theorem (see above).

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: field-div-checked-soundness

(defthm field-div-checked-soundness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime))
           (implies (field-div-checked-pred x y z prime)
                    (field-div-checked-spec x y z prime))))

Theorem: field-div-checked-completeness

(defthm field-div-checked-completeness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime))
           (implies (field-div-checked-spec x y z prime)
                    (field-div-checked-pred x y z prime))))

Theorem: field-div-checked-pred-to-spec

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

Theorem: field-div-checked-circuit-to-spec

(defthm field-div-checked-circuit-to-spec
 (implies
   (and (equal (pfcs::lookup-definition (pfname "field_div_checked")
                                        defs)
               (field-div-checked-circuit))
        (equal (pfcs::lookup-definition (pfname "field_inv_checked")
                                        defs)
               (field-inv-checked-circuit))
        (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_div_checked")
                                 defs (list x y z)
                                 prime)
          (field-div-checked-spec x y z prime))))