		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-point-type-conversions

Pointp-to-secp256k1-point

Convert the representation of a secp256k1 point from pointp to secp256k1-point.

Signature
(pointp-to-secp256k1-point point) → secp-point
Arguments: point — Guard (pointp point).
Returns: secp-point — Type (secp256k1-pointp secp-point).

The type pointp is larger than secp256k1-point, because it includes all possible points for all possible fields. So, we limit the conversion to points in the field of secp256k1, as expressed by the guard.

Furthermore, we limit the conversion to points that are not (0, 0), because that represents the point of infinity in secp256k1-point, but not in pointp (which uses :infinity. Without this restriction, one of the two the inverse theorem below (the one with the hypotheses) would not be provable.

Definitions and Theorems

Function: pointp-to-secp256k1-point

(defun pointp-to-secp256k1-point (point)
 (declare (xargs :guard (pointp point)))
 (declare
   (xargs :guard (and (point-in-pxp-p point (secp256k1-field-prime))
                      (not (equal point (cons 0 0))))))
 (let ((acl2::__function__ 'pointp-to-secp256k1-point))
   (declare (ignorable acl2::__function__))
   (if (eq point :infinity)
       (secp256k1-point 0 0)
     (secp256k1-point (car point)
                      (cdr point)))))

Theorem: secp256k1-pointp-of-pointp-to-secp256k1-point

(defthm secp256k1-pointp-of-pointp-to-secp256k1-point
  (b* ((secp-point (pointp-to-secp256k1-point point)))
    (secp256k1-pointp secp-point))
  :rule-classes :rewrite)

Theorem: pointp-to-secp256k1-point-of-secp256k1-point-to-pointp

(defthm pointp-to-secp256k1-point-of-secp256k1-point-to-pointp
 (equal
  (pointp-to-secp256k1-point (secp256k1-point-to-pointp secp-point))
  (secp256k1-point-fix secp-point)))

Theorem: secp256k1-point-to-pointp-of-pointp-to-secp256k1-point

(defthm secp256k1-point-to-pointp-of-pointp-to-secp256k1-point
 (implies
  (and (pointp point)
       (point-in-pxp-p point (secp256k1-field-prime))
       (not (equal point (cons 0 0))))
  (equal
       (secp256k1-point-to-pointp (pointp-to-secp256k1-point point))
       point)))