		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-point-orderp

Check if a point on a twisted Edwards curve has a certain order.

Signature
(twisted-edwards-point-orderp point order curve) → yes/no
Arguments: point — Guard (pointp point).; order — Guard (natp order).; curve — Guard (twisted-edwards-curvep curve).
Returns: yes/no — Type (booleanp yes/no).

A point P has order n if and only if n > 0, n P is the neutral element, and m P is not for every m < n.

Every point on the curve has an order, so there should really be a function that returns that. However, defining that function requires some theorems that we do not have yet; thus, for now we define this predicate instead. We plan to define the function that returns the order eventually.

Definitions and Theorems

Theorem: twisted-edwards-point-order-leastp-necc

(defthm twisted-edwards-point-order-leastp-necc
  (implies
       (twisted-edwards-point-order-leastp point order curve)
       (implies (and (natp order1)
                     (< 0 order1)
                     (< order1 (nfix order)))
                (not (equal (twisted-edwards-mul order1 point curve)
                            (twisted-edwards-zero))))))

Theorem: booleanp-of-twisted-edwards-point-order-leastp

(defthm booleanp-of-twisted-edwards-point-order-leastp
 (b* ((bool (twisted-edwards-point-order-leastp point order curve)))
   (booleanp bool))
 :rule-classes :type-prescription)

Theorem: twisted-edwards-point-order-leastp-of-point-fix-point

(defthm twisted-edwards-point-order-leastp-of-point-fix-point
  (equal (twisted-edwards-point-order-leastp (point-fix point)
                                             order curve)
         (twisted-edwards-point-order-leastp point order curve)))

Theorem: twisted-edwards-point-order-leastp-point-equiv-congruence-on-point

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

Theorem: twisted-edwards-point-order-leastp-of-nfix-order

(defthm twisted-edwards-point-order-leastp-of-nfix-order
  (equal (twisted-edwards-point-order-leastp point (nfix order)
                                             curve)
         (twisted-edwards-point-order-leastp point order curve)))

Theorem: twisted-edwards-point-order-leastp-nat-equiv-congruence-on-order

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

Theorem: twisted-edwards-point-order-leastp-of-twisted-edwards-curve-fix-curve

(defthm
 twisted-edwards-point-order-leastp-of-twisted-edwards-curve-fix-curve
 (equal (twisted-edwards-point-order-leastp
             point
             order (twisted-edwards-curve-fix curve))
        (twisted-edwards-point-order-leastp point order curve)))

Theorem: twisted-edwards-point-order-leastp-twisted-edwards-curve-equiv-congruence-on-curve

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

Function: twisted-edwards-point-orderp

(defun twisted-edwards-point-orderp (point order curve)
 (declare (xargs :guard (and (pointp point)
                             (natp order)
                             (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-point-orderp))
   (declare (ignorable acl2::__function__))
   (b* ((order (nfix order)))
     (and (> order 0)
          (equal (twisted-edwards-mul order point curve)
                 (twisted-edwards-zero))
          (twisted-edwards-point-order-leastp point order curve)))))

Theorem: booleanp-of-twisted-edwards-point-orderp

(defthm booleanp-of-twisted-edwards-point-orderp
  (b* ((yes/no (twisted-edwards-point-orderp point order curve)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

(defthm twisted-edwards-point-orderp-of-point-fix-point
  (equal (twisted-edwards-point-orderp (point-fix point)
                                       order curve)
         (twisted-edwards-point-orderp point order curve)))

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

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

Theorem: twisted-edwards-point-orderp-of-nfix-order

(defthm twisted-edwards-point-orderp-of-nfix-order
  (equal (twisted-edwards-point-orderp point (nfix order)
                                       curve)
         (twisted-edwards-point-orderp point order curve)))

Theorem: twisted-edwards-point-orderp-nat-equiv-congruence-on-order

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

Theorem: twisted-edwards-point-orderp-of-twisted-edwards-curve-fix-curve

(defthm
    twisted-edwards-point-orderp-of-twisted-edwards-curve-fix-curve
  (equal (twisted-edwards-point-orderp
              point
              order (twisted-edwards-curve-fix curve))
         (twisted-edwards-point-orderp point order curve)))

Theorem: twisted-edwards-point-orderp-twisted-edwards-curve-equiv-congruence-on-curve

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