Problems with elliptic curves

Stream: general

[Steffen Reith]

Dear all,

I have been learning how to use Lean4 for some time, currently without any particular objective. That's why I'm looking (with childlike joy) at individual areas of Mathlib that interest me at the moment.
Since I'm working on cryptography for embedded systems and hardware, elliptic curves are an obvious choice. That's why I'm currently trying to check simple properties of NIST curves (see e.g., [1] Hankerson, Menezes, Vanstone, Guide to Elliptic Curve Cryptography). Here is a first attempt:

import Mathlib

open WeierstrassCurve Affine Point

-- Prime is taken from example 3.5 of [1]
def p := 29

abbrev 𝔽29 := ZMod 29
abbrev C29 := Affine 𝔽29

#check C29
-- Parameters for a tiny example curve (see example 3.5 of [1])
def a := 4
def b := 20
def n := 37
def basepoint : 𝔽29 × 𝔽29 := (1, 5)

instance : Fact (Nat.Prime p) := ⟨(by decide)⟩
instance : Fact (Nat.Prime n) := ⟨(by decide)⟩

noncomputable instance curve : C29 := ⟨0, 0, 0, a, b⟩

-- curve is in short Weierstrass form
lemma short_curve : IsShortNF curve := by
  rw [isShortNF_iff, curve]
  decide

-- basepoint is located on curve
theorem valid_base : Equation curve basepoint.1 basepoint.2 := by
  rw[equation_iff', curve, a, b]
  rfl

-- and is not singular
theorem nonsingular_base : Nonsingular curve basepoint.1
                                             basepoint.2 := by
  rw [nonsingular_iff', curve, equation_iff]
  constructor
  · rfl
  · right
    decide

-- Now lets check the order of the basepoint
def basePoint' := Point.some nonsingular_base

-- Create a monoid of points on the curve
instance : Add (Point curve) where
  add := sorry  -- It's unclear to me (Point.add doesn't work, but why?)
noncomputable instance : AddMonoid (Point curve) where
  add_assoc := sorry
  zero_add := sorry
  add_zero := sorry
  nsmul := sorry
  nsmul_zero := sorry
  nsmul_succ := sorry

theorem valid_base_order : addOrderOf basePoint' = n := by
  apply addOrderOf_eq_prime
  rw [zero_def]
  · unfold n
    -- In principle something like "norm_num" should work?
    sorry
  · sorry

Can someone please give me a hint? I think I'm doing something fundamentally wrong with the types for the Add and AddMonoid instances.

Many thanks, Steffen

[Kenny Lau]

@Steffen Reith use #backticks to format code

[Kenny Lau]

you should use the provided instances rather than defining your own addition

[Steffen Reith]

Dear Kenny,

thank you for the fast response! Fixed the format of the code (sorry!). Which instances do you mean? If I remove the Add and AddMonoid then addOrderOf doesn't work at all (it seems that the addition of points isn't known to Lean, so i suspect that I miss some tricks with type-classes). Unfortunately, I haven't found any other examples where I can spy a little (or I'm just being too stupid ;-)

Thanks,
Steffen

[Junyan Xu]

instance : Fact (Nat.Prime 29) := ⟨by norm_num⟩
#synth AddCommGroup (Point curve)

[Junyan Xu]

or you could write

abbrev p := 29
abbrev n := 37

[Steffen Reith]

Dear Junyan,

thank you for your remarks! Now I can get rid of the Add /AddMonoid stuff

import Mathlib

open WeierstrassCurve Affine Point

-- Prime is taken from example 3.5 of [1]
abbrev p := 29

abbrev 𝔽29 := ZMod 29
abbrev C29 := Affine 𝔽29

-- Parameters for a tiny example curve (see example 3.5 of [1])
def a := 4
def b := 20
def n := 37
def basepoint : 𝔽29 × 𝔽29 := (1, 5)

instance : Fact (Nat.Prime p) := ⟨(by decide)⟩
instance : Fact (Nat.Prime n) := ⟨(by decide)⟩

noncomputable instance curve : C29 := ⟨0, 0, 0, a, b⟩

-- curve is in short Weierstrass form
lemma short_curve : IsShortNF curve := by
  rw [isShortNF_iff, curve]
  decide

-- basepoint is located on curve
theorem valid_base : Equation curve basepoint.1 basepoint.2 := by
  rw[equation_iff', curve, a, b]
  rfl

-- and is not singular
theorem nonsingular_base : Nonsingular curve basepoint.1
                                             basepoint.2 := by
  rw [nonsingular_iff', curve, equation_iff]
  constructor
  · rfl
  · right
    decide

-- Now lets check the order of the basepoint
def basePoint' := Point.some nonsingular_base

theorem valid_base_order : addOrderOf basePoint' = n := by
  apply addOrderOf_eq_prime
  · unfold n
    sorry
  · simp

It seems that abbrev p is enough. So p is marked "reducible" and the type-class mechanism works again (right?). You additionally suggested "#synth AddCommGroup (Point curve)". This seems not to work. It is not clear to me what #synth is good for. So Lean seems to be a little stubborn to evaluate the smul (38 * basepoint' = 0), but you gave me a good starting point!

Thanks,
Steffen

[Junyan Xu]

You get an error message "failed to synthesize ..." with #synth AddCommGroup (Point curve) if you don't add the Fact Prime instance. Once you add the instance the synthesis works and you can use the AddCommGroup structure, in particular the addition; that's all I wanted to express.

I think we need to make WeierstrassCurve.Affine.Point.add computable (by adding a DecidableEq assumption), and then rfl probably works. Or maybe we want a norm_num extension instead. Has this been done before? cc @David Ang
It seems you need simp [basePoint'] in the last line to solve the goal that basePoint' isn't zero.

[Kenny Lau]

@Steffen Reith I've cleaned up your code a bit:

import Mathlib

open WeierstrassCurve Affine Point

-- Prime is taken from example 3.5 of [1]
abbrev p := 29

abbrev 𝔽29 := ZMod 29
abbrev C29 := Affine 𝔽29

-- Parameters for a tiny example curve (see example 3.5 of [1])
abbrev a := 4
abbrev b := 20
abbrev n := 37

instance : Fact (Nat.Prime p) := by decide
instance : Fact (Nat.Prime n) := by decide

abbrev curve : C29 := ⟨0, 0, 0, a, b⟩

-- curve is in short Weierstrass form
instance : IsShortNF curve := by
  simp [isShortNF_iff]

def basepoint : curve.Point :=
  .some (x := 1) (y := 5) <| by
    rw [nonsingular_iff, equation_iff]
    decide

theorem valid_base_order : addOrderOf basepoint = n := by
  apply addOrderOf_eq_prime
  · unfold n basepoint
    sorry
  · sorry

[Kenny Lau]

and yeah we probably need to hold Lean's hand to prove that 37P=0

[Junyan Xu]

rfl still doesn't work after I made the AddCommGroup instance computable. I traced this to Nat.xgcdAux (which is used in docs#ZMod.inv) being defined using well-founded recursion. See #lean4 > opaque recursion definitions break mergeSort decidability @ 💬 ; it shouldn't be too hard to rewrite the function.

I wonder whether Lean should mark everything produced by well-founded recursion noncomputable, since it blocks kernel computation. (Is marking WellFounded.fix noncomputable enough? it's already marked noncomputable)

[Aaron Liu]

see also #24514

[Junyan Xu]

I made the AddCommGroup instance computable

#27299

[David Ang]

Thanks! I've been wanting to change having noncomputable to having the decidable assumption, but hadn't had a chance.

[Steffen Reith]

Hi Kenny,

I really like your improvement!

Some questions: We know

WeierstrassCurve.IsShortNF.{u_1} {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

Why did you do an instance IsShortNF? I'm a little be confused about this usage of an proposition. I agree it is elegant.

.some (x := 1) (y := 5) <| by
    rw [nonsingular_iff, equation_iff]
    decide

This is awesome! You use the "by" to get the proof term for nonsingularity and <| to add the third argument h of

WeierstrassCurve.Affine.Point.some.{r} {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) :
W'.Point

Yes, currying is nice. One difference: Im my solution the second "sorry" of the last theorem can be solved by "simp". In your solution this does not work. This sorry can be removed by simp[basepoint]

Best Steffen

[Steffen Reith]

Dear Junyan,

I would like to learn the background of your remark "... produced by well-founded recursion noncomputable ... blocks kernel computation." Any pointers to literature for me?
Thx

[Steffen Reith]

Dear Aaron&Junyan
thanks for the PRs! Do you think Lean will be able to work with "real" parameters? The point-multiplication will become massive.

-- Parameters for curve secp224r1
def secp224r1_p := p224
def secp224r1_a := 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFFFFFFFFFFFFFFFFFFFE
def secp224r1_b := 0xB4050A850C04B3ABF54132565044B0B7D7BFD8BA270B39432355FFB4

instance : Fact (Nat.Prime p224) := ⟨(by exact prime_p224)⟩
abbrev 𝔽p224 := ZMod p224

For the prime p224 (2 ^ 224 - 2 ^ 96 + 1) I have a Python-script, which computes a Pratt-certificate and some Lean-code to prove that p224 is prime.

[Kenny Lau]

@Steffen Reith use #backticks for codes.

instance is used if and only if the resulting type is a class, which in this case it is. You can check by doing:

import Mathlib

#print WeierstrassCurve.IsShortNF -- class WeierstrassCurve.IsShortNF ...

As for solving the last point by simp, you can still do that after unfold basepoint, but I would say using simp isn't the best solution. We should really use decide (after some more code has been implemented)

[Steffen Reith]

simp [basepoint] also works, but I agree decide would be nice. What can I do to help?

[Kenny Lau]

Steffen Reith said:

What can I do to help?

not really anything, sorry, there's already a bunch of PR's being referenced above

[Junyan Xu]

The example works in this branch (in which I merged #24514) with recursion depth 1606. Since Lean kernel trusts GMP library, it probably can handle much larger integers, but "smul by doubling" probably needs to be implemented.

[Steffen Reith]

I added

[[require]]
name = "mathlib"
scope = "leanprover-community"
from = "https://github.com/leanprover-community/mathlib4.git"
branch = "EllipticCurveFiniteField"

to my lakefile.toml and I can see that I get the correct branch of mathlib. But #24514 doesn't seem to be merged in this branch (xgcd is not fueled). I'm probably doing something wrong.

[Junyan Xu]

The branch https://github.com/alreadydone/mathlib4/tree/EllipticCurveFiniteField only exists in my fork, and I'm curious why you were able to get the correct branch from leanprover-community ...

[Steffen Reith]

Now my lakefile looks like

[[require]]
name = "mathlib"
#scope = "leanprover-community"
#from = "https://github.com/leanprover-community/mathlib4.git"
git = "https://github.com/alreadydone/mathlib4"
branch = "EllipticCurveFiniteField"

In

.lake/packages/mathlib

have in .git/config

[remote "origin"]
    url = https://github.com/alreadydone/mathlib4
    fetch = +refs/heads/*:refs/remotes/origin/*

and ```
git branch

• (HEAD detached at 7e1a2b8b1f)
  EllipticCurveFiniteField
  master

[Steffen Reith]

I would like to give a brief summary of the current status:

The patch in the EllipticCurveFiniteField branch of https://github.com/alreadydone/mathlib4 solves the problems for curves with small parameters (taken from D. Hankerson, A. Menezes, S. Vanstone, Guide to Elliptic Curve Cryptography, Springer, 2004, Example 3.5):

import Mathlib

namespace ECCDEMO

open WeierstrassCurve Affine Point

abbrev p := 29

abbrev 𝔽29 := ZMod p
abbrev C29 := Affine 𝔽29

-- Parameters for a tiny example curve
def a := 4
def b := 20
def n := 37
def basepoint : 𝔽29 × 𝔽29 := (1, 5)

instance : Fact (Nat.Prime p) := ⟨(by decide)⟩
instance : Fact (Nat.Prime n) := ⟨(by decide)⟩

instance curve : C29 := ⟨0, 0, 0, a, b⟩

-- curve is in short Weierstrass form
lemma short_curve : IsShortNF curve := by
  rw [isShortNF_iff, curve]
  decide

-- basepoint is located on the curve
theorem valid_base : Equation curve basepoint.1 basepoint.2 := by
  rw[equation_iff', curve, a, b]
  rfl

-- and is not singular
theorem nonsingular_base : Nonsingular curve basepoint.1
                                             basepoint.2 := by
  rw [nonsingular_iff', curve, equation_iff]
  constructor
  · rfl
  · right
    decide

-- Now lets check the order of the basepoint
abbrev basePoint' := Point.some nonsingular_base

set_option maxRecDepth 1606
theorem valid_base_order : addOrderOf basePoint' = n := by
  apply addOrderOf_eq_prime
  · rfl
  · simp

end ECCDEMO

Please pay attention to the recursion depth! You have to add Junyan special mathlib4 to your project. Hence, add

[[require]]
name = "mathlib"
git = "https://github.com/alreadydone/mathlib4"
rev = "638b227b3639da2d6f7280cd8d07958f5aa87dd2"

to your lakefile.toml. Moreover, make sure that you use the right toolchain and set leanprover/lean4:v4.22.0-rc3 in lean-toolchain!

Many thanks to Yunyan Xu for the great help! I will modify the example to include all NIST curves (may take some time) and post the result here again.

Regards,
Steffen

[Junyan Xu]

I'm combining the changes (including multiplication by doubling) into #30185; once it's merged you wouldn't need to rely on my branch.

With multiplication by doubling, set_option maxRecDepth 1606 is no longer needed (178 is already enough, which is below default threshold).

[Steffen Reith]

Sounds great! Thank you for all the work. Your implementation of “add-and-double” is interesting since correctness and implementation are mixed. Is there any kind of literature to learn more about this?

[Junyan Xu]

Are you referring to the definition of binaryRecAux or binaryRec? Their correctness is essentially the lemma binaryRec_eq_of_ne_zero, so I'd say the definition and correctness are separate. To prove that binaryRec computes scalar multiplication or exponentiation by natural numbers, the lemma npowRec_eq_npowBinRec is key, which is again separate from the definition.

[Steffen Reith]

For example this stuff:

suppress_compilation in
instance (priority := mid) pow : (n : ℕ) → (p ^ n).ComputableRepr :=
Nat.strongRec₀ fun n ih ↦ if h0 : n = 0 then
ofEq 1 _ (h0 ▸ pow_zero _).symm else
letI := ih (n / 2) (by omega)
let pow_half := p ^ (n / 2)
n.even_or_odd.by_cases (fun h ↦ ofEq (pow_half * pow_half) _ <| by
rw [← Nat.two_mul_div_two_of_even h, two_mul, pow_add])
fun h ↦ ofEq (p * (pow_half * pow_half)) _ <| by
rw [← Nat.two_mul_div_two_add_one_of_odd h, add_comm, two_mul, pow_add, pow_add, pow_one]

To me it seems to be the classical "repeated double and add", but you mixed in some rewrites that proof the correctness. Right?

[Junyan Xu]

You're probably referring to some old code I sent to you in DM. In that case, yes, in order to construct a term of type (p ^ n).ComputableRepr I have to show Computable.coeffs indeed computes p^n.
But I'm no longer using that code in #30185; I found that mathlib already contained docs#npowBinRec and docs#nsmulBinRec, so I'm now directly using them. I only reimplemented the dependency Nat.binaryRec in order to make it computable (kernel reducible).

[Steffen Reith]

Sorry, I missed that!

@[to_additive
def npowBinRec {M : Type*} [One M] [Mul M] (k : ℕ) : M → M :=
  npowBinRec.go k 1
where
  /-- Auxiliary tail-recursive implementation for `npowBinRec`. -/
  @[to_additive nsmulBinRec.go /-- Auxiliary tail-recursive implementation for `nsmulBinRec`. -/]
  go (k : ℕ) : M → M → M :=
    k.binaryRec (fun y _ ↦ y) fun bn _n fn y x ↦ fn (cond bn (y * x) y) (x * x)

Ok, this code seems to be a typical “repeated square and multiply” for an arbitrary multiplicative monoid, and nsmulBinRec is the additive counterpart. What you did with “Nat.binaryRec” is that you implemented the recursion principle used for them for natural numbers. Right? Hence, my next step is to read the diffs in #30185. This helped me a lot. Thanks!