|
|
|---|
|
|
|
|---|
Multiplication of a point on the secp256k1 curve by a number.
For now we do not require the point to be on the curve, but just to have coordinates in the field, as formalized by the guard.
The number is a natural number, as formalized by the guard.
We constrain this function to return a point unconditionally.
We also constrain this function to fix its arguments to a natural number and to a point.
Furthermore, we constrain this function to return a public key
(i.e. not the point at infinity)
when the number is a private key and the point is the generator.
This is because, since
Theorem:
(defthm secp256k1-pointp-of-secp256k1-mul (secp256k1-pointp (secp256k1-mul nat point)))
Theorem:
(defthm secp256k1-fixes-input-nat (equal (secp256k1-mul (nfix nat) point) (secp256k1-mul nat point)))
Theorem:
(defthm secp256k1-fixes-input-point (equal (secp256k1-mul nat (secp256k1-point-fix point)) (secp256k1-mul nat point)))
Theorem:
(defthm secp256k1-pub-key-p-of-mul-when-priv-key-p (implies (and (secp256k1-priv-key-p k) (equal point (secp256k1-point-generator))) (secp256k1-pub-key-p (secp256k1-mul k point))))
Theorem:
(defthm nat-equiv-implies-equal-secp256k1-mul-1 (implies (nat-equiv nat nat-equiv) (equal (secp256k1-mul nat point) (secp256k1-mul nat-equiv point))) :rule-classes (:congruence))
Theorem:
(defthm secp256k1-point-equiv-implies-equal-secp256k1-mul-2 (implies (secp256k1-point-equiv point point-equiv) (equal (secp256k1-mul nat point) (secp256k1-mul nat point-equiv))) :rule-classes (:congruence))