Zulip Chat Archive

Stream: new members

Topic: Getting the witnesses from a Sigma type


view this post on Zulip Mukesh Tiwari (Dec 06 2020 at 06:28):

How can I get t = ↑g ^ w.val, c = ↑(hash [g, h, ↑t]), and s = w + c * x from H₁ (see proof_of_completeness proof)?

1 goal
pq: 
g: zmod p
hash: list (zmod p)  zmod p
wx: zmod q
h: zmod p
H₀: h = g ^ x.val
tcs: zmod q
H₂: zkp_transcript p q g hash w x h H₀ (response t c s)
H₁: t, c, s, H₂⟩⟩⟩ = let t : zmod q := g ^ w.val, c : zmod q := (hash [g, h, t]), s : zmod q := w + c * x in t, c, s, response_step t c s _ (challenge_step t c _ (commitment_step t _))⟩⟩⟩
 g ^ s.val = t * h ^ c.val

Complete source code:

import data.zmod.basic data.nat.prime
 number_theory.quadratic_reciprocity
 tactic.find tactic.omega


namespace nzkp

variables
  (p q k : ) (g h : zmod p)
  (Hk : 2  k) (Hp : fact (nat.prime p)) (Hq : fact (nat.prime q))
  (Hdiv : p = q * k + 1)  (H₁ : h  0) (H₂ : h^k  1)
  (H₃ : g = h^k)


variables
  hash : list (zmod p) -> zmod p

inductive communication : Type*
| commitment : Π  (t : zmod q), communication
| challenge : Π (t c : zmod q), communication
| response : Π (t c s : zmod q), communication
open communication


/- Add more data to hash function https://tools.ietf.org/html/rfc8235 -/
inductive zkp_transcript (w x : zmod q) (h : zmod p) (Hf : h = g^x.val) : communication p -> Type*
| commitment_step (t : zmod q)  : t = g^w.val -> zkp_transcript (commitment t)
| challenge_step (t c : zmod q) : c = hash [g, h, t] -> zkp_transcript (commitment t) ->  zkp_transcript (challenge t c)
| response_step (t c s : zmod q) : s = w + c * x -> zkp_transcript (challenge t c) -> zkp_transcript (response t c s)
open zkp_transcript


/-
We can construct a sigma protocol (discrete logarithm).
we can always construct a valid certificate. Moreover, we will prove this
formally that this function always constructs a valid certificate which checks out
-/
def construct_nzkp_certificate (w x : zmod q) (h : zmod p) (H : h = g^x.val) :
    Σ (t c s : zmod q), zkp_transcript p q g hash w x h H (response t c s)  :=
      let
          t : zmod q := g^w.val,
          c : zmod q := hash [g, h, t],
          s : zmod q := w + c * x
      in  t, c, s, response_step t c s rfl (challenge_step t c rfl (commitment_step t rfl)) 

/- a given certificate is a valid one -/
def accept_nzkp_certificate  (w x : zmod q) (h : zmod p) (H : h = g^x.val)
  (t c s : zmod q) (Hnzkp : zkp_transcript p q g hash w x h H (response t c s)) :=
  g^s.val = t * h^c.val

/- invalid transcript -/
def reject_nzkp_certificate  (w x : zmod q) (h : zmod p) (H : h = g^x.val)
  (t c s : zmod q) (Hnzkp : zkp_transcript p q g hash w x h H (response t c s)) :=
  g^s.val  t * h^c.val


/-
Proof that the construct_nzkp_certificate function always constructs
a valid certificate. Each valid certificate always checks out.
Completeness
-/
theorem proof_of_completeness :  (w x : zmod q) (h : zmod p) (H₀ : h = g^x.val) cert
  (H₁ : cert = construct_nzkp_certificate p q g hash w x h H₀),
  accept_nzkp_certificate p q g hash w x h H₀ cert.1 cert.2.1 cert.2.2.1 cert.2.2.2 = true :=
 λ w x h H₀ t, c, s, H₂ H₁,
 begin
   unfold accept_nzkp_certificate, simp,
   clear _fun_match _x,
   unfold construct_nzkp_certificate at H₁,
  /- I am struck here -/


 end





end nzkp

view this post on Zulip Mario Carneiro (Dec 06 2020 at 06:38):

cases H1 should mostly work

view this post on Zulip Mukesh Tiwari (Dec 06 2020 at 06:52):

@Mario Carneiro Thanks, and now I have a straight forward goal, but library_search is not suggesting anything. How to get rid of this one? (In general, how should a newcomer search for a lemma in mathlib library?)

g ^ (comm_ring.add w ((hash [g, g ^ x.val, (g ^ w.val)]) * x)).val = (g ^ w.val) * (g ^ x.val) ^ (hash [g, g ^ x.val, (g ^ w.val)]).cast.val

view this post on Zulip Mario Carneiro (Dec 06 2020 at 06:55):

alternatively, you can use injection H1 a few times to avoid substituting everything in and making a mess of the goal

view this post on Zulip Mario Carneiro (Dec 06 2020 at 06:55):

I wouldn't expect library search to find anything for that - would you expect that exact theorem to be in the library?

view this post on Zulip Mario Carneiro (Dec 06 2020 at 06:57):

instead, try to think of the reason you think this goal is straightforward, and write down the general theorem statement that you think will be in the library. Then library_search will be able to prove it

view this post on Zulip Mario Carneiro (Dec 06 2020 at 07:08):

Here's a slightly more refined unfolding of the assumption:

begin
  unfold accept_nzkp_certificate, simp,
  clear _fun_match _x,
  unfold construct_nzkp_certificate at H₁,
  obtain rfl, rfl : t = g ^ w.val  s = w + c * x, {cases H₁, split; refl},
  clear H₁,
  subst H₀,
  rw [ pow_mul],
  -- ⊢ g ^ (w + c * x).val = ↑(↑g ^ w.val) * g ^ (x.val * c.val)
end

However the next steps aren't so easy. There are two things in the way of the obvious proof: the zmod.val function is not a homomorphism, which is blocking simplifying things like (w + c * x).val = w.val + c.val * x.val, and there is a coercion around the power ↑(↑g ^ w.val) which is the zmod q -> zmod p coercion, which has really bad properties unless p divides q (and I haven't read the rest of the file carefully but I would assume these are primes so that wouldn't be the case)

view this post on Zulip Mukesh Tiwari (Dec 06 2020 at 07:38):

@Mario Carneiro Yep, p and q are prime (p = k * q + 1 where k >= 2). I feel if I turn zmod p and zmod q into finite field, it would much simpler to prove this, and later, I can instantiate with these concrete instances.

view this post on Zulip Mario Carneiro (Dec 06 2020 at 07:39):

that sounds likely

view this post on Zulip Mario Carneiro (Dec 06 2020 at 07:40):

all this casting zmod to nat does real damage to the number theoretic properties; it would be easier if you use only "approved" operations from field theory

view this post on Zulip Mukesh Tiwari (Dec 06 2020 at 07:46):

(deleted)


Last updated: May 06 2021 at 20:13 UTC