Stream: new members

Topic: Getting the witnesses from a Sigma type

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
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 (Dec 06 2020 at 06:38):

cases H1 should mostly work

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


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

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?

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

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)

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.

Mario Carneiro (Dec 06 2020 at 07:39):

that sounds likely

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

Mukesh Tiwari (Dec 06 2020 at 07:46):

(deleted)

Last updated: May 06 2021 at 20:13 UTC