Getting the witnesses from a Sigma type

Stream: new members

[Mukesh Tiwari]

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

[Mario Carneiro]

cases H1 should mostly work

[Mukesh Tiwari]

@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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Mukesh Tiwari]

@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.

[Mario Carneiro]

that sounds likely

[Mario Carneiro]

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

[Mukesh Tiwari]

(deleted)