		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-neg

Negation of a point of the Montgomery curve group.

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

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

The negation of the point at infinity is the point at infinity. The negation of a finite point is obtained by negating the y coordinate.

Definitions and Theorems

Function: montgomery-neg

(defun montgomery-neg (point curve)
  (declare (xargs :guard (and (pointp point)
                              (montgomery-curvep curve))))
  (declare (xargs :guard (point-on-montgomery-p point curve)))
  (let ((acl2::__function__ 'montgomery-neg))
    (declare (ignorable acl2::__function__))
    (case (point-kind point)
      (:infinite (point-infinite))
      (:finite (b* ((p (montgomery-curve->p curve))
                    (x (point-finite->x point))
                    (y (point-finite->y point)))
                 (point-finite x (neg y p)))))))

Theorem: pointp-of-montgomery-neg

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

Theorem: point-on-montgomery-p-of-montgomery-neg

(defthm point-on-montgomery-p-of-montgomery-neg
  (implies (point-on-montgomery-p point curve)
           (point-on-montgomery-p (montgomery-neg point curve)
                                  curve)))

Theorem: montgomery-neg-of-zero

(defthm montgomery-neg-of-zero
  (equal (montgomery-neg (montgomery-zero) curve)
         (montgomery-zero)))

Theorem: montgomery-neg-of-neg

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

Theorem: montgomery-neg-of-point-fix-point

(defthm montgomery-neg-of-point-fix-point
  (equal (montgomery-neg (point-fix point) curve)
         (montgomery-neg point curve)))

Theorem: montgomery-neg-point-equiv-congruence-on-point

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

Theorem: montgomery-neg-of-montgomery-curve-fix-curve

(defthm montgomery-neg-of-montgomery-curve-fix-curve
  (equal (montgomery-neg point (montgomery-curve-fix curve))
         (montgomery-neg point curve)))

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

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