		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-interface

Secp256k1-add

Addition of two points on the secp256k1 curve.

For now we do not require the points to be on the curve, but just to be two points with coordinates in the field, as formalized by the guard.

We constrain this function to return a point unconditionally.

We also constrain this function to fix its arguments to points.

Definitions and Theorems

Theorem: secp256k1-pointp-of-secp256k1-add

(defthm secp256k1-pointp-of-secp256k1-add
  (secp256k1-pointp (secp256k1-add point1 point2)))

Theorem: secp256k1-fixes-input-point1

(defthm secp256k1-fixes-input-point1
  (equal (secp256k1-add (secp256k1-point-fix point1)
                        point2)
         (secp256k1-add point1 point2)))

Theorem: secp256k1-fixes-input-point2

(defthm secp256k1-fixes-input-point2
  (equal (secp256k1-add point1 (secp256k1-point-fix point2))
         (secp256k1-add point1 point2)))

Theorem: secp256k1-point-equiv-implies-equal-secp256k1-add-1

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

Theorem: secp256k1-point-equiv-implies-equal-secp256k1-add-2

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