Zulip Chat Archive

Stream: new members

Topic: Schnorr Group


view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 03:40):

Hi everyone, I am trying to prove a simple theorem about Schnorr group ( https://en.wikipedia.org/wiki/Schnorr_group ), but getting some typeclass synthesis error for hypothesis Hh1 Hh2 Hg.

import data.zmod.basic data.nat.prime
  data.zmod.quadratic_reciprocity

namespace ElGamal

/-
A Schnorr group is a large prime-order subgroup of โ„คโˆ—๐‘,
the multiplicative group of integers modulo ๐‘.
To generate such a group, we find ๐‘=๐‘ž๐‘Ÿ+1 such that ๐‘ and ๐‘ž
are prime. Then, we choose any โ„Ž
in the range 1<โ„Ž<๐‘ such that โ„Ž^r โ‰  1 (mod๐‘)
The value ๐‘”=โ„Ž^๐‘Ÿ(mod๐‘) is a generator of a subgroup โ„คโˆ—๐‘ of order ๐‘ž.
By Fermat's little theorem
g^q = h^(rq) = h^(p-1) = 1 (mod p)
-/

variables
  (p : โ„•) (q : โ„•) (r : โ„•+)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hhโ‚ : 1 < h < p)
  (Hhโ‚‚ : h^r โ‰  1)
  (g : zmodp p Hp) /- generator of a subgroup of โ„คโ‹†p of order q -/
  (Hg : g = h^r)

include p q r Hp Hq Hdiv h Hhโ‚ Hhโ‚‚ Hg
theorem generate_proof : g ^ q = 1 :=
begin
  /-
   rewrite Hg,
   associativity would turn the goal
   (h ^ r) ^ q = 1  into h ^ (r * q).
   r * q = p - 1.
   Use Fermat little theorem from
   fermat little to prove it -/

end







end ElGamal

view this post on Zulip Alex J. Best (Mar 22 2020 at 04:59):

The typeclass is has_lt (zmodp p Hp) so lean is telling you it doesn't know what < means for zmodp which makes sense, there is no nice notion of lton integers modulo a prime .

view this post on Zulip Alex J. Best (Mar 22 2020 at 05:00):

The sentiment you are trying to express with Hh1 is really just that the residue class h is not 0.

view this post on Zulip Alex J. Best (Mar 22 2020 at 05:01):

The second one is has_pow (zmodp p Hp) โ„•+which is telling you that lean can't take a positive natural power of an element of this type, you could argue that this is an oversight. But the easiest fix is to take h^r.val instead.

view this post on Zulip Alex J. Best (Mar 22 2020 at 05:04):

You could also take r of type nat instead. That might be less work in the long run.

view this post on Zulip Alex J. Best (Mar 22 2020 at 05:06):

Spoilers below:

import data.zmod.basic data.nat.prime
  data.zmod.quadratic_reciprocity

namespace ElGamal

/-
A Schnorr group is a large prime-order subgroup of โ„คโˆ—๐‘,
the multiplicative group of integers modulo ๐‘.
To generate such a group, we find ๐‘=๐‘ž๐‘Ÿ+1 such that ๐‘ and ๐‘ž
are prime. Then, we choose any โ„Ž
in the range 1<โ„Ž<๐‘ such that โ„Ž^r โ‰  1 (mod๐‘)
The value ๐‘”=โ„Ž^๐‘Ÿ(mod๐‘) is a generator of a subgroup โ„คโˆ—๐‘ of order ๐‘ž.
By Fermat's little theorem
g^q = h^(rq) = h^(p-1) = 1 (mod p)
-/

variables
  (p : โ„•) (q : โ„•) (r : โ„•)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hhโ‚ : h โ‰  0)
  (Hhโ‚‚ : h^r โ‰  1)
  (g : zmodp p Hp) /- generator of a subgroup of โ„คโ‹†p of order q -/
  (Hg : g = h^r)

#check Hhโ‚
include p q r Hp Hq Hdiv h Hhโ‚ Hhโ‚‚ Hg
theorem generate_proof : g ^ q = 1 :=
begin
   rewrite Hg,
   rw โ† pow_mul,
   rw mul_comm,
   have : p - 1 = q * r := nat.pred_eq_of_eq_succ Hdiv,
   rw โ† this,
   exact zmodp.fermat_little Hp Hhโ‚,
end







end ElGamal

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 07:05):

Thanks for the answer @Alex J. Best . Now, I am wondering about the error.
If I comment the proof 'generator_proof', then the error goes way.

variables
  (p : โ„•) (q : โ„•) (r : โ„•)
  (Hr : 2 โ‰ค r)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hhโ‚ : h โ‰  0)
  (Hhโ‚‚ : h^r โ‰  1)
  (g : zmodp p Hp) /- generator of a subgroup of โ„คโ‹†p of order q -/
  (Hg : g = h^r)


include Hg
theorem generator_proof : g ^ q = 1 :=
begin
  rw [Hg, <- pow_mul, mul_comm],
  have Ht : p - 1 = q * r := nat.pred_eq_of_eq_succ Hdiv,
  rw <- Ht, exact zmodp.fermat_little Hp Hhโ‚
end

variables
  (prikey : zmodp q Hq) /- private key -/
  (pubkey : zmodp p Hp) /- public key -/
  (Hrel : pubkey = g^prikey.val)

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * h^r.val)

kernel failed to type check declaration 'elgamal_enc' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ฮ  (p q : โ„•) (Hp : nat.prime p) (Hq : nat.prime q) (h g : zmodp p Hp),
    g = h ^ r โ†’ โ„• โ†’ zmodp p Hp โ†’ zmodp q Hq โ†’ zmodp p Hp ร— zmodp p Hp
elaborated value:
  ฮป (p q : โ„•) (Hp : nat.prime p) (Hq : nat.prime q) (h g : zmodp p Hp) (Hg : g = h ^ r) (r : โ„•) (m : zmodp p Hp)
  (r : zmodp q Hq), (g ^ r.val, g ^ m.val * h ^ r.val)
nested exception message:
failed to add declaration to environment, it contains local constants

view this post on Zulip Alex J. Best (Mar 22 2020 at 07:14):

This goes away for me if I wrap the previous declaration and preceding include in section ... end it seems lean doesn't like including these extra hypotheses.

view this post on Zulip Alex J. Best (Mar 22 2020 at 07:14):

import data.zmod.basic data.nat.prime
  data.zmod.quadratic_reciprocity

variables
  (p : โ„•) (q : โ„•) (r : โ„•)
  (Hr : 2 โ‰ค r)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hhโ‚ : h โ‰  0)
  (Hhโ‚‚ : h^r โ‰  1)
  (g : zmodp p Hp) /- generator of a subgroup of โ„คโ‹†p of order q -/
  (Hg : g = h^r)

section
include Hg Hdiv Hhโ‚
theorem generator_proof : g ^ q = 1 :=
begin
  rw [Hg, <- pow_mul, mul_comm],
  have Ht : p - 1 = q * r := nat.pred_eq_of_eq_succ Hdiv,
  rw <- Ht, exact zmodp.fermat_little Hp Hhโ‚
end
end

variables
  (prikey : zmodp q Hq) /- private key -/
  (pubkey : zmodp p Hp) /- public key -/
  (Hrel : pubkey = g^prikey.val)

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * h^r.val)
#check elgamal_enc

works

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 07:27):

Alex J. Best said:

This goes away for me if I wrap the previous declaration and preceding include in section ... end it seems lean doesn't like including these extra hypotheses.

I tried to move all the variable declared after the proof 'generator_proof' before it, but the error is still the same.
Anyway, your solution is working, so it's fine.

view this post on Zulip Alex J. Best (Mar 22 2020 at 07:54):

Right the issue is the include line which adds the unneeded hypotheses (for elgamal_enc) Hg Hdiv Hhโ‚ to all following declarations.

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 07:58):

Why does this find is not returning any lemma? I want to prove Ht1.

#find (_ ^ _ โ‰  0)

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * pubkey^r.val)

def elgamal_dec (c : zmodp p Hp ร—  zmodp p Hp) :=
  c.2 * (c.1^prikey.val)โปยน

include Hrel
lemma elgama_enc_dec_identity :
โˆ€ m r, elgamal_dec p q Hp Hq prikey
      (elgamal_enc p q Hp Hq g pubkey m r) = g^m.val :=
begin
  unfold elgamal_enc elgamal_dec,
  intros, simp, rw [Hrel, <- pow_mul, <- pow_mul],
  have Htโ‚ : g ^ (prikey.val * r.val) โ‰  0 :=
    sorry,
  have Htโ‚‚ : r.val * prikey.val = prikey.val * r.val :=
       mul_comm r.val prikey.val,
  rw [Htโ‚‚, mul_assoc, mul_inv_cancel Htโ‚], ring
end

view this post on Zulip Alex J. Best (Mar 22 2020 at 09:19):

What is elgamal_dec? You might find the tactic library_search more useful than find

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 09:34):

Updated the code.

view this post on Zulip Alex J. Best (Mar 22 2020 at 09:47):

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * pubkey^r.val)

def elgamal_dec (c : zmodp p Hp ร—  zmodp p Hp) :=
  c.2 * (c.1^prikey.val)โปยน

include Hrel Hg Hhโ‚
lemma elgama_enc_dec_identity :
โˆ€ m t, elgamal_dec p q Hp Hq prikey
      (elgamal_enc p q Hp Hq g pubkey m t) = g^m.val :=
begin
  unfold elgamal_enc elgamal_dec,
  intros, simp, rw [Hrel, <- pow_mul, <- pow_mul],
  have : g โ‰  0 := begin rw Hg, exact pow_ne_zero r Hhโ‚, end,
  have Htโ‚ : g ^ (prikey.val * t.val) โ‰  0 := pow_ne_zero (prikey.val * t.val) this,
  have Htโ‚‚ : t.val * prikey.val = prikey.val * t.val :=
       mul_comm t.val prikey.val,
  rw [Htโ‚‚, mul_assoc, mul_inv_cancel Htโ‚], ring
end

view this post on Zulip Alex J. Best (Mar 22 2020 at 09:47):

You need g nonzero

view this post on Zulip Alex J. Best (Mar 22 2020 at 09:48):

For which you need h nonzero

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 11:13):

Thanks Alex. I am looking for a vector library, and I see two vector library in mathlib, vector2 and vector3.

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 11:14):

https://github.com/leanprover-community/mathlib/blob/78ffbae077c50ed8ee060b3ac544f6f1d4359f39/src/number_theory/dioph.lean#L109

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 11:16):

https://github.com/leanprover-community/mathlib/blob/c718a22925872db4cb5f64c36ed6e6a07bdf647c/src/data/vector2.lean

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 11:16):

Which one would suggest to use ?

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 11:25):

Use vector

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 11:36):

Thanks Kevin.

view this post on Zulip Mukesh Tiwari (Mar 22 2020 at 11:40):

By the way Coq has a nice extraction facility, and you can extract any Coq program into Haskell, OCaml, or Scheme. I am wondering if there is something like this in Lean?

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 12:58):

In lean 4 you should be able to extract to...umm...C? I don't have a clue about this stuff

view this post on Zulip Scott Morrison (Mar 22 2020 at 22:55):

We really should give #find some additional love.

view this post on Zulip Mukesh Tiwari (Mar 23 2020 at 00:55):

@Scott Morrison That would make the life easier for new comers used to Coq's search pattern. I found linear_search quite nice because it just gives me some lemma from the remote corners of the mathlib library.

view this post on Zulip Mukesh Tiwari (Mar 23 2020 at 07:35):

I am looking for a lemma to prove that

ms : list (zmodp p Hp),
_x : list.length ms = n,
rs : list (zmodp q Hq),
_x : list.length rs = n
โŠข list.length (list.zip_with f  ms rs) = n

I could find anything using find or library_search

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:47):

I agree that list.zip_with doesn't seem to have been given much love in mathlib! It's defined in core, and for some of these things data.list.basic just makes an API, but apparently not here. I think it might be a hole in the library, although I would imagine it's not hard to prove by induction on n?

view this post on Zulip Mukesh Tiwari (Mar 23 2020 at 11:21):

@Kevin Buzzard If, say, my goal is to prove equality x = x, then I can use tactic or write the exact terms. I am wondering how can I see the terms build using the tactics ?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 12:49):

#print

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 12:49):

(deleted)

view this post on Zulip Mukesh Tiwari (Mar 23 2020 at 21:37):

#print is just printing the type signature. For this code

def vector_ciphertext_mult {n : โ„•} :
  vector (zmodp p Hp ร— zmodp p Hp) n -> vector (zmodp p Hp ร— zmodp p Hp) n ->
  vector (zmodp p Hp ร— zmodp p Hp) n
  | โŸจcsโ‚ , Hcโ‚โŸฉ  โŸจcsโ‚‚, Hcโ‚‚โŸฉ :=
    โŸจlist.zip_with (ciphertext_mult p Hp) csโ‚  csโ‚‚,
    begin
      have Ht : list.length csโ‚ = list.length csโ‚‚ :=
      begin rw [Hcโ‚, Hcโ‚‚] end,
      rw <- Hcโ‚, apply zip_with_len_l, exact Ht,
    end โŸฉ

The output of #print vector_ciphertext_mult

def ElGamal.vector_ciphertext_mult : ฮ  (p : โ„•) (Hp : nat.prime p) {n : โ„•},
  vector (zmodp p Hp ร— zmodp p Hp) n โ†’ vector (zmodp p Hp ร— zmodp p Hp) n โ†’ vector (zmodp p Hp ร— zmodp p Hp) n :=
ฮป (p : โ„•) (Hp : nat.prime p) {n : โ„•}, vector_ciphertext_mult._main p Hp

But I want to see the CIC terms build by tactics.

view this post on Zulip Bryan Gin-ge Chen (Mar 23 2020 at 21:40):

The proof term is there, it's everything after the :=.

view this post on Zulip Mukesh Tiwari (Mar 23 2020 at 22:06):

@Bryan Gin-ge Chen Seems like something I misunderstood about Lean, so let me give a similar analogy from Coq. In Coq, when you write tactic to solve some goal, under the hood it is constructing a Gallina (CIC) term (which you could have written manually, but no one does this because it is very cumbersome). Now at any point of the time, if you want to see the CIC (Gallina) terms, then you simply write 'Show Proof', and it will print all the Gallina (CIC) terms constructed so far.

In my 'vector_ciphertext_mult' program, there are two things: a list (which I believe is in CIC) and a proof (but written in tactic mode). I want to see how the proof terms appears in CIC (or core language) because I don't think tactics are part of core language in Lean.

view this post on Zulip Bryan Gin-ge Chen (Mar 23 2020 at 23:00):

Sorry, I guess I was a bit unclear, I meant the part after := in the output of #print vector_ciphertext_mult, namely: ฮป (p : โ„•) (Hp : nat.prime p) {n : โ„•}, vector_ciphertext_mult._main p Hp.

That is a term, not a tactic. I don't know if you would consider that in the "core" language of Lean since you can also export something even lower level. I've never played around with that though.

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 23:13):

I think you just have to keep digging. Can you see that your definition is essentially vector_ciphertext_mult._main? Why don't you #print that, and then keep printing stuff?

Hey -- do you know about set_option pp.all true? Try that before a #print statement, it gives you much more information.

view this post on Zulip Mukesh Tiwari (Mar 24 2020 at 01:25):

Sorry for the confusion. Some how I missed the ._main part in the vector_ciphertext_mult._main p Hp . Thanks again @Kevin Buzzard @Bryan Gin-ge Chen .


Last updated: May 13 2021 at 23:16 UTC