		Search-engine friendly clone of the ACL2 documentation.

Field-square

Field-square-circuit

Construction of the circuit.

Signature
(field-square-circuit) → pdef
Returns: pdef — Type (pfcs::definitionp pdef).

This is a PFCS definition with a single equality constraint of the form described in field-square.

Definitions and Theorems

Function: field-square-circuit

(defun field-square-circuit nil
  (declare (xargs :guard t))
  (let ((__function__ 'field-square-circuit))
    (declare (ignorable __function__))
    (pfcs::parse-def
         "field_square(x, y) := {
    field_mul(x, x, y)
    }")))

Theorem: definitionp-of-field-square-circuit

(defthm definitionp-of-field-square-circuit
  (b* ((pdef (field-square-circuit)))
    (pfcs::definitionp pdef))
  :rule-classes :rewrite)

Theorem: sr1cs-definitionp-of-field-square-circuit

(defthm sr1cs-definitionp-of-field-square-circuit
  (b* ((pdef (field-square-circuit)))
    (pfcs::sr1cs-definitionp pdef))
  :rule-classes :rewrite)