		Search-engine friendly clone of the ACL2 documentation.

Curve-parameterization

Curve-subgroup-neg

Negation in the subgroup.

Signature
(curve-subgroup-neg x curve) → (mv okp -x)
Arguments: x — Guard (curve-subgroupp x curve).; curve — Guard (curvep curve).
Returns: okp — Type (booleanp okp).; -x — Type (curve-subgroupp -x curve).

We use the same two-result approach as for addition; see curve-subgroup-add.

Definitions and Theorems

Function: curve-subgroup-neg

(defun curve-subgroup-neg (x curve)
  (declare (xargs :guard (and (curvep curve)
                              (curve-subgroupp x curve))))
  (let ((__function__ 'curve-subgroup-neg))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic
                 (if (curve-subgroupp x curve)
                     x
                   (curve-zero curve))
                 :exec x))
         (-x (ecurve::edwards-bls12-neg x)))
      (if (curve-subgroupp -x curve)
          (mv t -x)
        (mv nil (curve-zero curve))))))

Theorem: booleanp-of-curve-subgroup-neg.okp

(defthm booleanp-of-curve-subgroup-neg.okp
  (b* (((mv ?okp ?-x)
        (curve-subgroup-neg x curve)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: return-type-of-curve-subgroup-neg.-x

(defthm return-type-of-curve-subgroup-neg.-x
  (b* (((mv ?okp ?-x)
        (curve-subgroup-neg x curve)))
    (curve-subgroupp -x curve))
  :rule-classes :rewrite)

Theorem: pointp-of-curve-subgroup-neg.-x

(defthm pointp-of-curve-subgroup-neg.-x
  (b* (((mv ?okp ?-x)
        (curve-subgroup-neg x curve)))
    (pointp -x))
  :rule-classes :rewrite)

Theorem: curve-subgroup-neg-of-curve-fix-curve

(defthm curve-subgroup-neg-of-curve-fix-curve
  (equal (curve-subgroup-neg x (curve-fix curve))
         (curve-subgroup-neg x curve)))

Theorem: curve-subgroup-neg-curve-equiv-congruence-on-curve

(defthm curve-subgroup-neg-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (curve-subgroup-neg x curve)
                  (curve-subgroup-neg x curve-equiv)))
  :rule-classes :congruence)