		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-attachment

Executable attachments for the elliptic curve secp256k1 interface.

We define an executable definition of private-to-public key conversion, and attach it to the constrained function.

We define a wrapper of the curve group multiplication definition and attach the wrapper to the constrained function. The wrapper converts between the fixtype of points and the representation of points used by the definition of the curve group operations; it also ensures that the starting point is on the curve, as required by the guards of the defined curve group operation. Note that secp256k1+ is never expected to return (0, 0), because the point at infinity is represented as :infinity and the point (0, 0) is not on the curve; to satisfy the guard of pointp-to-secp256k1-point, we check that at run time, raising an error if the test should ever fail (which we never expect to).

We define a wrapper of the curve group addition definition and attach the wrapper to the constrained function. The wrapper converts between the fixtype of points and the representation of points used by the definition of the curve group operations; it also ensures that the starting points are on the curve, as required by the guards of the defined curve group operation. Note that secp256k1+ is never expected to return (0, 0), because the point at infinity is represented as :infinity and the point (0, 0) is not on the curve; to satisfy the guard of pointp-to-secp256k1-point, we check that at run time, raising an error if the test should ever fail (which we never expect to). If we multiply the secp256k1 generator point by a private key, we obtain a valid public key, i.e. not the point at infinity. At this time we do not have that theorem proved and available, so for now we insert a run-time check that is never expected to fail.

For executable formal specifications, see the library for the Short Weierstrass elliptic curve secp256k1.

Definitions and Theorems

Function: secp256k1-priv-to-pub-exec

(defun secp256k1-priv-to-pub-exec (priv)
  (declare (xargs :guard (secp256k1-priv-key-p priv)))
  (b* ((priv (mbe :logic (secp256k1-priv-key-fix priv)
                  :exec priv))
       (pub (secp256k1-mul priv (secp256k1-point-generator))))
    pub))

Theorem: secp256k1-pub-key-p-of-secp256k1-priv-to-pub-exec

(defthm secp256k1-pub-key-p-of-secp256k1-priv-to-pub-exec
  (b* ((pub (secp256k1-priv-to-pub-exec priv)))
    (secp256k1-pub-key-p pub))
  :rule-classes :rewrite)

Theorem: secp256k1-priv-to-pub-exec-of-secp256k1-priv-key-fix-priv

(defthm secp256k1-priv-to-pub-exec-of-secp256k1-priv-key-fix-priv
  (equal (secp256k1-priv-to-pub-exec (secp256k1-priv-key-fix priv))
         (secp256k1-priv-to-pub-exec priv)))

Theorem: secp256k1-priv-to-pub-exec-secp256k1-priv-key-equiv-congruence-on-priv

(defthm
 secp256k1-priv-to-pub-exec-secp256k1-priv-key-equiv-congruence-on-priv
 (implies (secp256k1-priv-key-equiv priv priv-equiv)
          (equal (secp256k1-priv-to-pub-exec priv)
                 (secp256k1-priv-to-pub-exec priv-equiv)))
 :rule-classes :congruence)

Function: secp256k1-add-wrapper

(defun secp256k1-add-wrapper (secp-point1 secp-point2)
 (declare (xargs :guard (and (secp256k1-pointp secp-point1)
                             (secp256k1-pointp secp-point2))))
 (let ((acl2::__function__ 'secp256k1-add-wrapper))
   (declare (ignorable acl2::__function__))
   (b* ((point1 (secp256k1-point-to-pointp secp-point1))
        (point2 (secp256k1-point-to-pointp secp-point2))
        ((unless (point-on-weierstrass-elliptic-curve-p
                      point1 (secp256k1-field-prime)
                      (secp256k1-a)
                      (secp256k1-b)))
         (secp256k1-point 1 1))
        ((unless (point-on-weierstrass-elliptic-curve-p
                      point2 (secp256k1-field-prime)
                      (secp256k1-a)
                      (secp256k1-b)))
         (secp256k1-point 1 1))
        (result (secp256k1+ point1 point2))
        ((when (equal result (cons 0 0)))
         (acl2::raise "Internal error: SECP256K1+ produced (0, 0).")
         (secp256k1-point 1 1))
        (secp-result (pointp-to-secp256k1-point result)))
     secp-result)))

Theorem: secp256k1-pointp-of-secp256k1-add-wrapper

(defthm secp256k1-pointp-of-secp256k1-add-wrapper
 (b* ((secp-result (secp256k1-add-wrapper secp-point1 secp-point2)))
   (secp256k1-pointp secp-result))
 :rule-classes :rewrite)

Theorem: secp256k1-add-wrapper-of-secp256k1-point-fix-secp-point1

(defthm secp256k1-add-wrapper-of-secp256k1-point-fix-secp-point1
  (equal (secp256k1-add-wrapper (secp256k1-point-fix secp-point1)
                                secp-point2)
         (secp256k1-add-wrapper secp-point1 secp-point2)))

Theorem: secp256k1-add-wrapper-secp256k1-point-equiv-congruence-on-secp-point1

(defthm
 secp256k1-add-wrapper-secp256k1-point-equiv-congruence-on-secp-point1
 (implies
      (secp256k1-point-equiv secp-point1 secp-point1-equiv)
      (equal (secp256k1-add-wrapper secp-point1 secp-point2)
             (secp256k1-add-wrapper secp-point1-equiv secp-point2)))
 :rule-classes :congruence)

Theorem: secp256k1-add-wrapper-of-secp256k1-point-fix-secp-point2

(defthm secp256k1-add-wrapper-of-secp256k1-point-fix-secp-point2
  (equal (secp256k1-add-wrapper secp-point1
                                (secp256k1-point-fix secp-point2))
         (secp256k1-add-wrapper secp-point1 secp-point2)))

Theorem: secp256k1-add-wrapper-secp256k1-point-equiv-congruence-on-secp-point2

(defthm
 secp256k1-add-wrapper-secp256k1-point-equiv-congruence-on-secp-point2
 (implies
      (secp256k1-point-equiv secp-point2 secp-point2-equiv)
      (equal (secp256k1-add-wrapper secp-point1 secp-point2)
             (secp256k1-add-wrapper secp-point1 secp-point2-equiv)))
 :rule-classes :congruence)

Function: secp256k1-mul-wrapper

(defun secp256k1-mul-wrapper (nat secp-point)
 (declare (xargs :guard (and (natp nat)
                             (secp256k1-pointp secp-point))))
 (let ((acl2::__function__ 'secp256k1-mul-wrapper))
  (declare (ignorable acl2::__function__))
  (b*
   ((nat (mbe :logic (nfix nat) :exec nat))
    (point (secp256k1-point-to-pointp secp-point))
    ((unless (point-on-weierstrass-elliptic-curve-p
                  point (secp256k1-field-prime)
                  (secp256k1-a)
                  (secp256k1-b)))
     (secp256k1-point 1 1))
    (result (secp256k1* nat point))
    ((when (equal result (cons 0 0)))
     (acl2::raise "Internal error: SECP256K1* produced (0, 0).")
     (secp256k1-point 1 1))
    (secp-result (pointp-to-secp256k1-point result))
    ((when (and (secp256k1-priv-key-p nat)
                (secp256k1-point-equiv
                     secp-point (secp256k1-point-generator))
                (not (secp256k1-pub-key-p secp-result))))
     (acl2::raise
      "Internal error: ~
                        SECP256K1* on a private key and the generator ~
                        has produced ~x0, which is not a public key."
      secp-result)
     (secp256k1-point 1 1)))
   secp-result)))

Theorem: secp256k1-pointp-of-secp256k1-mul-wrapper

(defthm secp256k1-pointp-of-secp256k1-mul-wrapper
  (b* ((secp-result (secp256k1-mul-wrapper nat secp-point)))
    (secp256k1-pointp secp-result))
  :rule-classes :rewrite)

Theorem: secp256k1-mul-wrapper-yields-pub-from-priv

(defthm secp256k1-mul-wrapper-yields-pub-from-priv
  (implies (and (secp256k1-priv-key-p nat)
                (equal point (secp256k1-point-generator)))
           (secp256k1-pub-key-p (secp256k1-mul-wrapper nat point))))

Theorem: secp256k1-mul-wrapper-of-nfix-nat

(defthm secp256k1-mul-wrapper-of-nfix-nat
  (equal (secp256k1-mul-wrapper (nfix nat)
                                secp-point)
         (secp256k1-mul-wrapper nat secp-point)))

Theorem: secp256k1-mul-wrapper-nat-equiv-congruence-on-nat

(defthm secp256k1-mul-wrapper-nat-equiv-congruence-on-nat
  (implies (nat-equiv nat nat-equiv)
           (equal (secp256k1-mul-wrapper nat secp-point)
                  (secp256k1-mul-wrapper nat-equiv secp-point)))
  :rule-classes :congruence)

Theorem: secp256k1-mul-wrapper-of-secp256k1-point-fix-secp-point

(defthm secp256k1-mul-wrapper-of-secp256k1-point-fix-secp-point
 (equal (secp256k1-mul-wrapper nat (secp256k1-point-fix secp-point))
        (secp256k1-mul-wrapper nat secp-point)))

Theorem: secp256k1-mul-wrapper-secp256k1-point-equiv-congruence-on-secp-point

(defthm
 secp256k1-mul-wrapper-secp256k1-point-equiv-congruence-on-secp-point
 (implies (secp256k1-point-equiv secp-point secp-point-equiv)
          (equal (secp256k1-mul-wrapper nat secp-point)
                 (secp256k1-mul-wrapper nat secp-point-equiv)))
 :rule-classes :congruence)