Reducing exponentiation modulo huge number

Stream: mathlib4

[Quang Dao]

I am trying to prove that this 254-bit number
p := 21888242871839275222246405745257275088548364400416034343698204186575808495617
is a prime. For context, this is the scalar prime field of the BN254 curve used in Ethereum. To do so, I use the existing Lucas primality test, with the extension for checking Pratt certificate here. I use the Pratt certificate found in this file.

With that in mind, one of the steps is to establish that 5 is a primitive root mod p, i.e. 5 ^ (p - 1) = (1 : ZMod p). I can't tell Lean to directly compute 5 ^ (p - 1) mod p since Lean doesn't do the "smart" thing and break the computation into manageable chunks, and reducing mod p at every step.

So I tried to define exponentiation via chunking and tell Lean to work with this definition instead:

import Mathlib.Data.ZMod.Basic

namespace ZMod

def powSplit (a : ZMod n) (k : ℕ) (b : ℕ) (h : b ≥ 2) : ZMod n :=
  if k = 0 then 1
  else a ^ (k % b) * (a.powSplit (k / b) b h) ^ b
termination_by k
decreasing_by
  simp_wf
  rename_i hk
  exact Nat.div_lt_self (Nat.ne_zero_iff_zero_lt.mp hk) h

-- I have a proof of this, not showing to reduce length
theorem pow_eq_powSplit {x : ZMod n} {k : ℕ} (b : ℕ) (h : b ≥ 2) : x ^ k = x.powSplit k b h := sorry

end ZMod

notation "BN254_SCALAR" => 21888242871839275222246405745257275088548364400416034343698204186575808495617

-- This returns immediately, can do split size up to around 1000
#eval ZMod.powSplit (5 : ZMod BN254_SCALAR) (BN254_SCALAR - 1) 10 (by decide)

theorem mod_comp : (5 ^ (BN254_SCALAR - 1) : ZMod BN254_SCALAR) = 1 := by
  rw [ZMod.pow_eq_powSplit 100 (by decide)]
  simp
  repeat (unfold ZMod.powSplit <;> simp <;> norm_num)
  -- At this point, I end up with horrible goals due to Lean not being able to unfold fully

How do I tell Lean to do computation with my powSplit instead of the usual pow in the proof?

[Markus Himmel]

There seem to be some errors in your MWE. There should be a namespace ZMod somewhere and you don't define SCALAR_FIELD_CARD.

[Quang Dao]

Sorry, It should be working now?

[Markus Himmel]

Since you're already using things from the old normnum_powmod branch, have you seen that that branch (see the diff) also includes a modification to the reduce_mod_char tactic that enables it to handle modular exponentiation? On that branch, you can just do

theorem mod_comp : (5 ^ (BN254_SCALAR - 1) : ZMod BN254_SCALAR) = 1 := by reduce_mod_char

[Quang Dao]

Ah awesome, I didn't look through the other branch changes

[Quang Dao]

This is a dumb question, but what is the best way to get the diff from that branch, while staying updated with master? I suppose I could just copy the changes into my local repo

[Jireh Loreaux]

@Kim Morrison it would be so nice if we could get your csimp PR for this merged. Care to try and convince Eric again?

[Matthew Ballard]

On current master, now you can do

import Mathlib.Data.ZMod.Defs

set_option linter.style.longLine false in
abbrev M : Nat := 0xb10b8f96a080e01dde92de5eae5d54ec52c99fbcfb06a3c69a6a9dca52d23b616073e28675a23d189838ef1e2ee652c013ecb4aea906112324975c3cd49b83bfaccbdd7d90c4bd7098488e9c219a73724effd6fae5644738faa31a4ff55bccc0a151af5f0dc8b4bd45bf37df365c1a65e68cfda76d4da708df1fb2bc2e4a4371

set_option linter.style.longLine false in
abbrev g : Nat := 0xa4d1cbd5c3fd34126765a442efb99905f8104dd258ac507fd6406cff14266d31266fea1e5c41564b777e690f5504f213160217b4b01b886a5e91547f9e2749f4d7fbd7d3b9a92ee1909d0d2263f80a76a6a24c087a091f531dbf0a0169b6a28ad662a4d18e73afa32d779d5918d08bc8858f4dcef97c2a24855e6eeb22b3b2e5
abbrev N : Nat := 0xf518aa8781a8df278aba4e7d64b7cb9d49462353

example : (g : ZMod M) ^ N = 1 := by native_decide

but the enhancement to reduce_mod_char would be preferable still

[Matthew Ballard]

I bumped branch#normnum-powmod to build on current master (though not lint)

[Quang Dao]

Do you expect it to be merged into Mathlib soon? Anything I can help with?

[Matthew Ballard]

I think we should check with @Markus Himmel if he thinks it is (or parts of it are) in a reasonable state to start PRing first.

[Matthew Ballard]

Values taken from here for the example

[Eric Wieser]

Can we add a test for the above to prevent a performance regression?

[Markus Himmel]

Matthew Ballard said:

I think we should check with Markus Himmel if he thinks it is (or parts of it are) in a reasonable state to start PRing first.

The primality stuff on the branch is definitely just a prototype and not ready for PRing. The changes to norm_num/reduce_mod_char are mostly inspired by existing code, so they should be much closer to being ready to merge.

I think it would be great to have this in mathlib, but I'm not planning to PR it, so I would be grateful if someone else could take the lead on this. As usual with meta code, I expect the greatest challenge will be to find a reviewer.

[Matthew Ballard]

Eric Wieser said:

Can we add a test for the above to prevent a performance regression?

#17996

[Matthew Ballard]

It might make sense to use pari/gp (or even roll our own in rust) a'la polyrith for certificate generation for ECPP.

But for reduce_mod_char if @Quang Dao wants to PR this part, I will review (in a reasonable time frame) it

[Quang Dao]

I opened PR #18030

[Matthew Ballard]

I've reviewed. Only minor suggestions

[Matthew Ballard]

I added the following as a test

-- The 20th Mersenne prime
abbrev q : Nat := 2 ^ 4423 - 1

-- This takes a little time but the 21st Mersenne prime is too large
set_option exponentiation.threshold 10000 in
example : (3 : ZMod q) ^ (q - 1) = 1 := by reduce_mod_char

Thanks to @Anne Baanen for looking at the ReduceModChar changes. I think this is ready to go and I will merge it later today.