		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-sub

Subtraction of two points of the twisted Edwards group.

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

This is, as usual in groups, essentially an abbreviation for adding the first point to the negation of the second point.

Definitions and Theorems

Function: twisted-edwards-sub

(defun twisted-edwards-sub (point1 point2 curve)
 (declare (xargs :guard (and (pointp point1)
                             (pointp point2)
                             (twisted-edwards-curvep curve))))
 (declare
     (xargs :guard (and (twisted-edwards-curve-completep curve)
                        (point-on-twisted-edwards-p point1 curve)
                        (point-on-twisted-edwards-p point2 curve))))
 (let ((acl2::__function__ 'twisted-edwards-sub))
   (declare (ignorable acl2::__function__))
   (twisted-edwards-add point1
                        (twisted-edwards-neg point2 curve)
                        curve)))

Theorem: pointp-of-twisted-edwards-sub

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

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

(defthm point-on-twisted-edwards-p-of-twisted-edwards-sub
  (implies (and (twisted-edwards-curve-completep curve)
                (pointp point1)
                (pointp point2)
                (point-on-twisted-edwards-p point1 curve)
                (point-on-twisted-edwards-p point2 curve))
           (point-on-twisted-edwards-p
                (twisted-edwards-sub point1 point2 curve)
                curve)))

Theorem: twisted-edwards-sub-of-point-fix-point1

(defthm twisted-edwards-sub-of-point-fix-point1
  (equal (twisted-edwards-sub (point-fix point1)
                              point2 curve)
         (twisted-edwards-sub point1 point2 curve)))

Theorem: twisted-edwards-sub-point-equiv-congruence-on-point1

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

Theorem: twisted-edwards-sub-of-point-fix-point2

(defthm twisted-edwards-sub-of-point-fix-point2
  (equal (twisted-edwards-sub point1 (point-fix point2)
                              curve)
         (twisted-edwards-sub point1 point2 curve)))

Theorem: twisted-edwards-sub-point-equiv-congruence-on-point2

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

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

(defthm twisted-edwards-sub-of-twisted-edwards-curve-fix-curve
  (equal (twisted-edwards-sub point1 point2
                              (twisted-edwards-curve-fix curve))
         (twisted-edwards-sub point1 point2 curve)))

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

(defthm
 twisted-edwards-sub-twisted-edwards-curve-equiv-congruence-on-curve
 (implies (twisted-edwards-curve-equiv curve curve-equiv)
          (equal (twisted-edwards-sub point1 point2 curve)
                 (twisted-edwards-sub point1 point2 curve-equiv)))
 :rule-classes :congruence)