		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-point-orderp

Check if a point on a Montgomery curve has a certain order.

Signature
(montgomery-point-orderp point order curve) → yes/no
Arguments: point — Guard (pointp point).; order — Guard (natp order).; curve — Guard (montgomery-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 the neutral element for every 0 < 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: montgomery-point-order-leastp-necc

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

Theorem: booleanp-of-montgomery-point-order-leastp

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

Theorem: montgomery-point-order-leastp-of-point-fix-point

(defthm montgomery-point-order-leastp-of-point-fix-point
  (equal (montgomery-point-order-leastp (point-fix point)
                                        order curve)
         (montgomery-point-order-leastp point order curve)))

Theorem: montgomery-point-order-leastp-point-equiv-congruence-on-point

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

Theorem: montgomery-point-order-leastp-of-nfix-order

(defthm montgomery-point-order-leastp-of-nfix-order
  (equal (montgomery-point-order-leastp point (nfix order)
                                        curve)
         (montgomery-point-order-leastp point order curve)))

Theorem: montgomery-point-order-leastp-nat-equiv-congruence-on-order

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

Theorem: montgomery-point-order-leastp-of-montgomery-curve-fix-curve

(defthm montgomery-point-order-leastp-of-montgomery-curve-fix-curve
 (equal
  (montgomery-point-order-leastp point
                                 order (montgomery-curve-fix curve))
  (montgomery-point-order-leastp point order curve)))

Theorem: montgomery-point-order-leastp-montgomery-curve-equiv-congruence-on-curve

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

Function: montgomery-point-orderp

(defun montgomery-point-orderp (point order curve)
  (declare (xargs :guard (and (pointp point)
                              (natp order)
                              (montgomery-curvep curve))))
  (declare (xargs :guard (point-on-montgomery-p point curve)))
  (let ((acl2::__function__ 'montgomery-point-orderp))
    (declare (ignorable acl2::__function__))
    (b* ((order (nfix order))
         (order*point (montgomery-mul order point curve)))
      (and (> order 0)
           (equal order*point (montgomery-zero))
           (montgomery-point-order-leastp point order curve)))))

Theorem: booleanp-of-montgomery-point-orderp

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

Theorem: montgomery-point-orderp-of-point-fix-point

(defthm montgomery-point-orderp-of-point-fix-point
  (equal (montgomery-point-orderp (point-fix point)
                                  order curve)
         (montgomery-point-orderp point order curve)))

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

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

Theorem: montgomery-point-orderp-of-nfix-order

(defthm montgomery-point-orderp-of-nfix-order
  (equal (montgomery-point-orderp point (nfix order)
                                  curve)
         (montgomery-point-orderp point order curve)))

Theorem: montgomery-point-orderp-nat-equiv-congruence-on-order

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

Theorem: montgomery-point-orderp-of-montgomery-curve-fix-curve

(defthm montgomery-point-orderp-of-montgomery-curve-fix-curve
 (equal (montgomery-point-orderp point
                                 order (montgomery-curve-fix curve))
        (montgomery-point-orderp point order curve)))

Theorem: montgomery-point-orderp-montgomery-curve-equiv-congruence-on-curve

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