		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-neg

Negation of a point of the twisted Edwards curve group.

Signature
(twisted-edwards-neg point curve) → point1
Arguments: point — Guard (pointp point).; curve — Guard (twisted-edwards-curvep curve).
Returns: point1 — Type (pointp point1).

This is the inverse with respect to the group addition operation.

It is obtained by negating the x coordinate. See the paper referenced in twisted-edwards.

Definitions and Theorems

Function: twisted-edwards-neg

(defun twisted-edwards-neg (point curve)
 (declare (xargs :guard (and (pointp point)
                             (twisted-edwards-curvep curve))))
 (declare
      (xargs :guard (and (twisted-edwards-curve-completep curve)
                         (point-on-twisted-edwards-p point curve))))
 (let ((acl2::__function__ 'twisted-edwards-neg))
   (declare (ignorable acl2::__function__))
   (point-finite (neg (point-finite->x point)
                      (twisted-edwards-curve->p curve))
                 (point-finite->y point))))

Theorem: pointp-of-twisted-edwards-neg

(defthm pointp-of-twisted-edwards-neg
  (b* ((point1 (twisted-edwards-neg point curve)))
    (pointp point1))
  :rule-classes :rewrite)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-neg

(defthm point-on-twisted-edwards-p-of-twisted-edwards-neg
  (implies
       (and (twisted-edwards-curve-completep curve)
            (point-on-twisted-edwards-p point curve))
       (point-on-twisted-edwards-p (twisted-edwards-neg point curve)
                                   curve)))

Theorem: twisted-edwards-neg-of-zero

(defthm twisted-edwards-neg-of-zero
  (equal (twisted-edwards-neg (twisted-edwards-zero)
                              curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-neg-of-neg

(defthm twisted-edwards-neg-of-neg
  (implies
       (point-on-twisted-edwards-p point curve)
       (equal (twisted-edwards-neg (twisted-edwards-neg point curve)
                                   curve)
              (point-fix point))))

Theorem: twisted-edwards-neg-is-zero-iff-zero

(defthm twisted-edwards-neg-is-zero-iff-zero
  (implies (and (pointp point)
                (point-on-twisted-edwards-p point curve))
           (equal (equal (twisted-edwards-neg point curve)
                         (twisted-edwards-zero))
                  (equal point (twisted-edwards-zero)))))

Theorem: twisted-edwards-neg-of-point-fix-point

(defthm twisted-edwards-neg-of-point-fix-point
  (equal (twisted-edwards-neg (point-fix point)
                              curve)
         (twisted-edwards-neg point curve)))

Theorem: twisted-edwards-neg-point-equiv-congruence-on-point

(defthm twisted-edwards-neg-point-equiv-congruence-on-point
  (implies (point-equiv point point-equiv)
           (equal (twisted-edwards-neg point curve)
                  (twisted-edwards-neg point-equiv curve)))
  :rule-classes :congruence)

Theorem: twisted-edwards-neg-of-twisted-edwards-curve-fix-curve

(defthm twisted-edwards-neg-of-twisted-edwards-curve-fix-curve
  (equal
       (twisted-edwards-neg point (twisted-edwards-curve-fix curve))
       (twisted-edwards-neg point curve)))

Theorem: twisted-edwards-neg-twisted-edwards-curve-equiv-congruence-on-curve

(defthm
 twisted-edwards-neg-twisted-edwards-curve-equiv-congruence-on-curve
 (implies (twisted-edwards-curve-equiv curve curve-equiv)
          (equal (twisted-edwards-neg point curve)
                 (twisted-edwards-neg point curve-equiv)))
 :rule-classes :congruence)