		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-point-type-conversions

Secp256k1-point-to-pointp

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

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

Definitions and Theorems

Function: secp256k1-point-to-pointp

(defun secp256k1-point-to-pointp (secp-point)
  (declare (xargs :guard (secp256k1-pointp secp-point)))
  (let ((acl2::__function__ 'secp256k1-point-to-pointp))
    (declare (ignorable acl2::__function__))
    (b* ((x (secp256k1-point->x secp-point))
         (y (secp256k1-point->y secp-point)))
      (if (and (= x 0) (= y 0))
          :infinity
        (cons x y)))))

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

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

Theorem: point-in-pxp-p-of-secp256k1-point-to-pointp

(defthm point-in-pxp-p-of-secp256k1-point-to-pointp
  (point-in-pxp-p (secp256k1-point-to-pointp secp-point)
                  (secp256k1-field-prime)))

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

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

Theorem: secp256k1-point-to-pointp-secp256k1-point-equiv-congruence-on-secp-point

(defthm
 secp256k1-point-to-pointp-secp256k1-point-equiv-congruence-on-secp-point
 (implies (secp256k1-point-equiv secp-point secp-point-equiv)
          (equal (secp256k1-point-to-pointp secp-point)
                 (secp256k1-point-to-pointp secp-point-equiv)))
 :rule-classes :congruence)