• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
          • R1cs
          • Interfaces
          • Sha-2
          • Keccak
          • Kdf
          • Mimc
          • Padding
          • Hmac
          • Elliptic-curves
            • Secp256k1-attachment
            • Twisted-edwards
              • Twisted-edwards-mul
              • Twisted-edwards-mul-fast
              • Twisted-edwards-add
              • Twisted-edwards-point-orderp
              • Twisted-edwards-add-associativity
              • Twisted-edwards-mul-distributivity-over-scalar-addition
              • Twisted-edwards-neg-inverse
              • Twisted-edwards-mul-fast-nonneg
              • Twisted-edwards-curve
              • Twisted-edwards-mul-nonneg
              • Birational-montgomery-twisted-edwards
              • Twisted-edwards-compress
              • Twisted-edwards-neg
              • Twisted-edwards-sub
              • Point-on-twisted-edwards-p
                • Twisted-edwards-curve-completep
                • Twisted-edwards-point-order-leastp
                • Twisted-edwards-only-points-with-x-0-or-y-1
                • Twisted-edwards-add-inverse-uniqueness
                • Twisted-edwards-distributivity-of-neg-over-add
                • Twisted-edwards-mul-associativity
                • Twisted-edwards-zero
                • Twisted-edwards-add-closure
                • Twisted-edwards-point-orderp-of-neg
                • Twisted-edwards-mul-of-mod-order
                • Twisted-edwards-zero-identity
                • Twisted-edwards-add-cancel-left
                • Twisted-edwards-mul-of-neg
                • Twisted-edwards-add-commutative
              • Montgomery
              • Short-weierstrass-curves
              • Birational-montgomery-twisted-edwards
              • Has-square-root?-satisfies-pfield-squarep
              • Secp256k1
              • Secp256k1-domain-parameters
              • Secp256k1-types
              • Pfield-squarep
              • Secp256k1-interface
              • Prime-field-extra-rules
              • Points
            • Attachments
            • Elliptic-curve-digital-signature-algorithm
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Twisted-edwards

    Point-on-twisted-edwards-p

    Check if a point is on a twisted Edwards curve.

    Signature
    (point-on-twisted-edwards-p point curve) → yes/no
    Arguments
    point — Guard (pointp point).
    curve — Guard (twisted-edwards-curvep curve).
    Returns
    yes/no — Type (booleanp yes/no).

    A point (x, y) is on the curve if and only if its components satisfy the curve equation. We require its components to be below the prime, i.e. that the point is in the cartesian product of the prime field. The point at infinity is not part of a twisted Edwards curve; only finite points are.

    Definitions and Theorems

    Function: point-on-twisted-edwards-p

    (defun point-on-twisted-edwards-p (point curve)
      (declare (xargs :guard (and (pointp point)
                                  (twisted-edwards-curvep curve))))
      (let ((acl2::__function__ 'point-on-twisted-edwards-p))
        (declare (ignorable acl2::__function__))
        (b* ((p (twisted-edwards-curve->p curve))
             (a (twisted-edwards-curve->a curve))
             (d (twisted-edwards-curve->d curve))
             ((when (eq (point-kind point) :infinite))
              nil)
             (x (point-finite->x point))
             (y (point-finite->y point))
             ((unless (< x p)) nil)
             ((unless (< y p)) nil)
             (x^2 (mul x x p))
             (y^2 (mul y y p))
             (x^2.y^2 (mul x^2 y^2 p))
             (a.x^2 (mul a x^2 p))
             (a.x^2+y^2 (add a.x^2 y^2 p))
             (|1+D.X^2.Y^2| (add 1 (mul d x^2.y^2 p) p)))
          (equal a.x^2+y^2 |1+D.X^2.Y^2|))))

    Theorem: booleanp-of-point-on-twisted-edwards-p

    (defthm booleanp-of-point-on-twisted-edwards-p
      (b* ((yes/no (point-on-twisted-edwards-p point curve)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: point-on-twisted-edwards-is-finite

    (defthm point-on-twisted-edwards-is-finite
      (implies (point-on-twisted-edwards-p point curve)
               (equal (point-kind point) :finite))
      :rule-classes :forward-chaining)

    Theorem: point-on-twisted-edwards-p-of-point-fix-point

    (defthm point-on-twisted-edwards-p-of-point-fix-point
      (equal (point-on-twisted-edwards-p (point-fix point)
                                         curve)
             (point-on-twisted-edwards-p point curve)))

    Theorem: point-on-twisted-edwards-p-point-equiv-congruence-on-point

    (defthm point-on-twisted-edwards-p-point-equiv-congruence-on-point
      (implies (point-equiv point point-equiv)
               (equal (point-on-twisted-edwards-p point curve)
                      (point-on-twisted-edwards-p point-equiv curve)))
      :rule-classes :congruence)

    Theorem: point-on-twisted-edwards-p-of-twisted-edwards-curve-fix-curve

    (defthm
          point-on-twisted-edwards-p-of-twisted-edwards-curve-fix-curve
      (equal (point-on-twisted-edwards-p
                  point (twisted-edwards-curve-fix curve))
             (point-on-twisted-edwards-p point curve)))

    Theorem: point-on-twisted-edwards-p-twisted-edwards-curve-equiv-congruence-on-curve

    (defthm
     point-on-twisted-edwards-p-twisted-edwards-curve-equiv-congruence-on-curve
     (implies (twisted-edwards-curve-equiv curve curve-equiv)
              (equal (point-on-twisted-edwards-p point curve)
                     (point-on-twisted-edwards-p point curve-equiv)))
     :rule-classes :congruence)