• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • 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
      • Riscv
      • 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

Twisted-edwards-mul-fast

Fast scalar multiplication in the twisted Edwards group.

Signature

(twisted-edwards-mul-fast scalar point curve) → point1

Arguments

scalar — Guard (integerp scalar).

point — Guard (pointp point).

curve — Guard (twisted-edwards-curvep curve).

Returns

point1 — Type (pointp point1).

This is the same as twisted-edwards-mul but using only doubling and addition in order to reduce the execution time to \mathcal{O}(log(scalar)).

In the future we will either replace the body of twisted-edwards-mul by this definition and adapt the users such as distributivity-over-scalar-addition, or prove equivalence of the two forms.

Definitions and Theorems

Function: twisted-edwards-mul-fast-nonneg

(defun twisted-edwards-mul-fast-nonneg (scalar point curve)
 (declare (xargs :guard (and (natp scalar)
                             (pointp point)
                             (twisted-edwards-curvep curve))))
 (declare
      (xargs :guard (and (twisted-edwards-curve-completep curve)
                         (point-on-twisted-edwards-p point curve))))
 (let ((acl2::__function__ 'twisted-edwards-mul-fast-nonneg))
  (declare (ignorable acl2::__function__))
  (if (zp scalar)
      (twisted-edwards-zero)
    (if
      (evenp scalar)
      (let ((half-scalar-mul
                 (twisted-edwards-mul-fast-nonneg (/ scalar 2)
                                                  point curve)))
        (twisted-edwards-add half-scalar-mul half-scalar-mul curve))
      (twisted-edwards-add
           point
           (twisted-edwards-mul-fast-nonneg (- scalar 1)
                                            point curve)
           curve)))))

Theorem: pointp-of-twisted-edwards-mul-fast-nonneg

(defthm pointp-of-twisted-edwards-mul-fast-nonneg
 (b* ((point1 (twisted-edwards-mul-fast-nonneg scalar point curve)))
   (pointp point1))
 :rule-classes :rewrite)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-mul-fast-nonneg

(defthm
      point-on-twisted-edwards-p-of-twisted-edwards-mul-fast-nonneg
  (implies (and (twisted-edwards-curve-completep curve)
                (pointp point)
                (point-on-twisted-edwards-p point curve))
           (point-on-twisted-edwards-p
                (twisted-edwards-mul-fast-nonneg scalar point curve)
                curve)))

Theorem: twisted-edwards-mul-fast-nonneg-of-0

(defthm twisted-edwards-mul-fast-nonneg-of-0
  (equal (twisted-edwards-mul-fast-nonneg 0 point curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-fast-nonneg-of-1

(defthm twisted-edwards-mul-fast-nonneg-of-1
  (implies (point-on-twisted-edwards-p point curve)
           (equal (twisted-edwards-mul-fast-nonneg 1 point curve)
                  (point-fix point))))

Theorem: twisted-edwards-mul-fast-nonneg-of-zero

(defthm twisted-edwards-mul-fast-nonneg-of-zero
 (equal
      (twisted-edwards-mul-fast-nonneg scalar (twisted-edwards-zero)
                                       curve)
      (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-fast-nonneg-of-nfix-scalar

(defthm twisted-edwards-mul-fast-nonneg-of-nfix-scalar
  (equal (twisted-edwards-mul-fast-nonneg (nfix scalar)
                                          point curve)
         (twisted-edwards-mul-fast-nonneg scalar point curve)))

Theorem: twisted-edwards-mul-fast-nonneg-nat-equiv-congruence-on-scalar

(defthm
     twisted-edwards-mul-fast-nonneg-nat-equiv-congruence-on-scalar
 (implies
   (nat-equiv scalar scalar-equiv)
   (equal
        (twisted-edwards-mul-fast-nonneg scalar point curve)
        (twisted-edwards-mul-fast-nonneg scalar-equiv point curve)))
 :rule-classes :congruence)

Theorem: twisted-edwards-mul-fast-nonneg-of-point-fix-point

(defthm twisted-edwards-mul-fast-nonneg-of-point-fix-point
  (equal (twisted-edwards-mul-fast-nonneg scalar (point-fix point)
                                          curve)
         (twisted-edwards-mul-fast-nonneg scalar point curve)))

Theorem: twisted-edwards-mul-fast-nonneg-point-equiv-congruence-on-point

(defthm
    twisted-edwards-mul-fast-nonneg-point-equiv-congruence-on-point
 (implies
   (point-equiv point point-equiv)
   (equal
        (twisted-edwards-mul-fast-nonneg scalar point curve)
        (twisted-edwards-mul-fast-nonneg scalar point-equiv curve)))
 :rule-classes :congruence)

Theorem: twisted-edwards-mul-fast-nonneg-of-twisted-edwards-curve-fix-curve

(defthm
 twisted-edwards-mul-fast-nonneg-of-twisted-edwards-curve-fix-curve
 (equal (twisted-edwards-mul-fast-nonneg
             scalar
             point (twisted-edwards-curve-fix curve))
        (twisted-edwards-mul-fast-nonneg scalar point curve)))

Theorem: twisted-edwards-mul-fast-nonneg-twisted-edwards-curve-equiv-congruence-on-curve

(defthm
 twisted-edwards-mul-fast-nonneg-twisted-edwards-curve-equiv-congruence-on-curve
 (implies
   (twisted-edwards-curve-equiv curve curve-equiv)
   (equal
        (twisted-edwards-mul-fast-nonneg scalar point curve)
        (twisted-edwards-mul-fast-nonneg scalar point curve-equiv)))
 :rule-classes :congruence)

Function: twisted-edwards-mul-fast

(defun twisted-edwards-mul-fast (scalar point curve)
 (declare (xargs :guard (and (integerp scalar)
                             (pointp point)
                             (twisted-edwards-curvep curve))))
 (declare
      (xargs :guard (and (twisted-edwards-curve-completep curve)
                         (point-on-twisted-edwards-p point curve))))
 (let ((acl2::__function__ 'twisted-edwards-mul-fast))
   (declare (ignorable acl2::__function__))
   (b* ((scalar (ifix scalar)))
     (if (>= scalar 0)
         (twisted-edwards-mul-fast-nonneg scalar point curve)
       (twisted-edwards-neg
            (twisted-edwards-mul-fast-nonneg (- scalar)
                                             point curve)
            curve)))))

Theorem: pointp-of-twisted-edwards-mul-fast

(defthm pointp-of-twisted-edwards-mul-fast
  (b* ((point1 (twisted-edwards-mul-fast scalar point curve)))
    (pointp point1))
  :rule-classes :rewrite)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-mul-fast

(defthm point-on-twisted-edwards-p-of-twisted-edwards-mul-fast
  (implies
       (and (twisted-edwards-curve-completep curve)
            (pointp point)
            (point-on-twisted-edwards-p point curve))
       (b* ((?point1 (twisted-edwards-mul-fast scalar point curve)))
         (point-on-twisted-edwards-p point1 curve))))

Theorem: twisted-edwards-mul-fast-of-0

(defthm twisted-edwards-mul-fast-of-0
  (equal (twisted-edwards-mul-fast 0 point curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-fast-of-1

(defthm twisted-edwards-mul-fast-of-1
  (implies (point-on-twisted-edwards-p point curve)
           (equal (twisted-edwards-mul-fast 1 point curve)
                  (point-fix point))))

Theorem: twisted-edwards-mul-fast-of-zero

(defthm twisted-edwards-mul-fast-of-zero
  (equal (twisted-edwards-mul-fast scalar (twisted-edwards-zero)
                                   curve)
         (twisted-edwards-zero)))

Theorem: twisted-edwards-mul-fast-of-minus1

(defthm twisted-edwards-mul-fast-of-minus1
  (implies (point-on-twisted-edwards-p point curve)
           (equal (twisted-edwards-mul-fast -1 point curve)
                  (twisted-edwards-neg point curve))))

Theorem: twisted-edwards-neg-of-mul-fast

(defthm twisted-edwards-neg-of-mul-fast
  (implies (and (twisted-edwards-curve-completep curve)
                (pointp point)
                (point-on-twisted-edwards-p point curve))
           (equal (twisted-edwards-neg
                       (twisted-edwards-mul-fast scalar point curve)
                       curve)
                  (twisted-edwards-mul-fast (- (ifix scalar))
                                            point curve))))

Theorem: twisted-edwards-mul-fast-of-ifix-scalar

(defthm twisted-edwards-mul-fast-of-ifix-scalar
  (equal (twisted-edwards-mul-fast (ifix scalar)
                                   point curve)
         (twisted-edwards-mul-fast scalar point curve)))

Theorem: twisted-edwards-mul-fast-int-equiv-congruence-on-scalar

(defthm twisted-edwards-mul-fast-int-equiv-congruence-on-scalar
  (implies
       (acl2::int-equiv scalar scalar-equiv)
       (equal (twisted-edwards-mul-fast scalar point curve)
              (twisted-edwards-mul-fast scalar-equiv point curve)))
  :rule-classes :congruence)

Theorem: twisted-edwards-mul-fast-of-point-fix-point

(defthm twisted-edwards-mul-fast-of-point-fix-point
  (equal (twisted-edwards-mul-fast scalar (point-fix point)
                                   curve)
         (twisted-edwards-mul-fast scalar point curve)))

Theorem: twisted-edwards-mul-fast-point-equiv-congruence-on-point

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

Theorem: twisted-edwards-mul-fast-of-twisted-edwards-curve-fix-curve

(defthm twisted-edwards-mul-fast-of-twisted-edwards-curve-fix-curve
 (equal
  (twisted-edwards-mul-fast scalar
                            point (twisted-edwards-curve-fix curve))
  (twisted-edwards-mul-fast scalar point curve)))

Theorem: twisted-edwards-mul-fast-twisted-edwards-curve-equiv-congruence-on-curve

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