		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-types

Secp256k1-point-infinityp

Check if a secp256k1 point is the point at infinity \mathcal{O} of the curve.

Signature
(secp256k1-point-infinityp point) → yes/no
Arguments: point — Guard (secp256k1-pointp point).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: secp256k1-point-infinityp

(defun secp256k1-point-infinityp (point)
  (declare (xargs :guard (secp256k1-pointp point)))
  (and (equal (secp256k1-point->x point) 0)
       (equal (secp256k1-point->y point) 0)))

Theorem: booleanp-of-secp256k1-point-infinityp

(defthm booleanp-of-secp256k1-point-infinityp
  (b* ((yes/no (secp256k1-point-infinityp point)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: secp256k1-point-infinityp-of-secp256k1-point-fix-point

(defthm secp256k1-point-infinityp-of-secp256k1-point-fix-point
  (equal (secp256k1-point-infinityp (secp256k1-point-fix point))
         (secp256k1-point-infinityp point)))

Theorem: secp256k1-point-infinityp-secp256k1-point-equiv-congruence-on-point

(defthm
 secp256k1-point-infinityp-secp256k1-point-equiv-congruence-on-point
 (implies (secp256k1-point-equiv point point-equiv)
          (equal (secp256k1-point-infinityp point)
                 (secp256k1-point-infinityp point-equiv)))
 :rule-classes :congruence)