		Search-engine friendly clone of the ACL2 documentation.

Points

Point-in-pxp-p

Check if a point is in the cartesian product of a prime field, or it is the point at infinity.

Signature
(point-in-pxp-p point p) → *
Arguments: point — Guard (pointp point).; p — Guard (natp p).

This predicate checks if a point (as defined in pointp) is either the point at infity, or is in the cartesian product \{0, \ldots, p-1\} \times \{0, \ldots, p-1\}, where p \geq 2. In the context of elliptic curves, p is the prime, and this predicate checks if the point, if finite, is in the ``plane'' of the curve.

The purpose of this predicate is to provide a preliminary constraint for points of curves in specific fields (described by p). Thus, we must include the point at infinity in this predicate, even though it is not actually on the the aforementioned plane.

We do not require the parameter p to be prime here. It suffices, for the purpose of defining this predicate, for p to be an integer that is at least 2.

Definitions and Theorems

Function: point-in-pxp-p

(defun point-in-pxp-p (point p)
  (declare (xargs :guard (and (pointp point) (natp p))))
  (declare (xargs :guard (<= 2 p)))
  (let ((acl2::__function__ 'point-in-pxp-p))
    (declare (ignorable acl2::__function__))
    (or (eq point :infinity)
        (and (< (car point) p)
             (< (cdr point) p)))))

Theorem: point-in-pxp-p-of-infinity

(defthm point-in-pxp-p-of-infinity
  (implies (< 0 p)
           (point-in-pxp-p :infinity p)))