Computational zero-knowledge interactive proofs for NP

Goldreich, Micali, and Wigderson [GMW91] proved that if one-way functions exist, then every language in NP has a computational zero-knowledge interactive proof system. This module defines computational zero-knowledge interactive proofs (ZeroKnowledgeProof) together with explicit public API predicates distinguishing restricted polynomial-time-generable zero-knowledge (GenerableZeroKnowledge) from general auxiliary-input zero-knowledge over arbitrary polynomially bounded valid families (AuxiliaryInputZeroKnowledge), and constructs a proof system for ThreeSAT and hence for every language in NP via ThreeSAT_npHard and Naor's bit commitment scheme [Nao91] (Complexity.Crypto.Computational.Commitment).

Protocol design and source credit

While the theorem that every language in NP has a computational zero-knowledge interactive proof system from one-way functions is due to Goldreich, Micali, and Wigderson [GMW91] using Naor's commitment scheme [Nao91], the concrete underlying ThreeSAT protocol formalized in Complexity.Crypto.Computational.GMW is a direct 3-copy masked-3SAT truth-table commitment protocol rather than GMW's original 3-coloring protocol: each of 3 parallel copies commits to a random variable mask, the XOR-masked assignment, and the 8-entry masked truth table of each clause, and a random 3-bit challenge selects for each copy whether to open the mask and full truth tables or the masked assignment and the active truth-table entries.

Restricted versus general auxiliary-input zero-knowledge and witness conventions

• Restricted polynomial-time-generable zero-knowledge (GenerableZeroKnowledge, ZeroKnowledgeProof.zero_knowledge, ZeroKnowledgeProof.generableZeroKnowledge). Matching the library's uniform strict-PPT cryptographic conventions (ComputationallyIndistinguishable), GenerableZeroKnowledge quantifies over uniform strict oracle PPT malicious verifiers Vstar (producing one efficient witness-free simulator S per Vstar before the choice of families) and deterministic polynomial-time-generable families of instances a : ℕ → α, valid witnesses w : ℕ → List Bool (∀ n, isWitness (a n) (w n) = true), and auxiliary inputs z : ℕ → List Bool (ComputableInPolyTime · encUnary _). Fixed-instance zero-knowledge (ZeroKnowledgeProof.zero_knowledge_const) is an immediate corollary for constant families fun _ => a and fun _ => w.
• General auxiliary-input zero-knowledge (AuxiliaryInputZeroKnowledge, ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge). Quantifies over the same uniform strict oracle PPT malicious verifiers Vstar and chooses one efficient witness-free simulator S per Vstar before the choice of families, then ranges over arbitrary polynomially bounded families of instances a : ℕ → α, valid witnesses w : ℕ → List Bool, and auxiliary inputs z : ℕ → List Bool (PolynomiallyBounded), against all full-input uniform strict PPT distinguishers adversary charged for the complete encoded input ((1^n, (a n, z n)), view). Every system satisfying AuxiliaryInputZeroKnowledge satisfies GenerableZeroKnowledge (AuxiliaryInputZeroKnowledge.generableZeroKnowledge). Under the explicit advice-PRG premise GMW.AdvicePRG (from GMW.gmwView_negligible_of_advice_prg), the GMW proof systems satisfy ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge (PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction, PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT); this module does not derive GMW.AdvicePRG from uniform PRG or one-way function assumptions.
• Bundled witness relation (ZeroKnowledgeProof.isWitness). ZeroKnowledgeProof bundles its own polynomial-time witness predicate isWitness : α → List Bool → Bool characterizing A (mem_iff_exists_witness). No witness-length bound is imposed, so isWitness by itself need not be an NP relation; membership in IP (mem_IP) does not need one, and in zero_knowledge the witness family w : ℕ → List Bool is polynomial-time-generable in 1^n. In PseudorandomGenerator.zeroKnowledgeProofOfReduction and PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP, the bundled predicate isWitness a w := ThreeSAT.verifier (f a, w) checks a ThreeSAT witness for the Karp-reduced formula f a rather than a witness for the original NP verifier of A.

Main definitions

• Cslib.Crypto.GenerableZeroKnowledge: uniform computational zero-knowledge over deterministic polynomial-time-generable instance, valid-witness, and auxiliary-input families.
• Cslib.Crypto.AuxiliaryInputZeroKnowledge, Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge: general auxiliary-input computational zero-knowledge over arbitrary polynomially bounded valid families against full-input uniform strict PPT distinguishers.
• Cslib.Crypto.ZeroKnowledgeProof: a computational zero-knowledge interactive proof system for a language A, bundling a uniform strict oracle PPT verifier, an honest prover with a uniform strict PPT interaction realization, perfect completeness, soundness 1 / 3 against unbounded provers, and GenerableZeroKnowledge.
• Cslib.Crypto.PseudorandomGenerator.zeroKnowledgeProofOfReduction, Cslib.Crypto.PseudorandomGenerator.zeroKnowledgeProofThreeSAT: GMW zero-knowledge proof systems for any language Karp-reducible to ThreeSAT and for ThreeSAT itself.

Main results

• Cslib.Crypto.AuxiliaryInputZeroKnowledge.generableZeroKnowledge, Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.generableZeroKnowledge: general auxiliary-input zero-knowledge implies poly-time-generable zero-knowledge.
• Cslib.Crypto.ZeroKnowledgeProof.isInteractiveProof, Cslib.Crypto.ZeroKnowledgeProof.mem_IP: every language with a ZeroKnowledgeProof belongs to IP.
• Cslib.Crypto.ZeroKnowledgeProof.zero_knowledge_const, Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.zero_knowledge_const: fixed-instance computational zero-knowledge.
• Cslib.Crypto.PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP, Cslib.Crypto.OneWay.exists_zeroKnowledgeProof_of_mem_NP: GMW zero-knowledge proof systems for every language in NP from any pseudorandom generator (with stretch 3 * k + 1) or one-way function, establishing GenerableZeroKnowledge.
• Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction, Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT, Cslib.Crypto.PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP: general AuxiliaryInputZeroKnowledge for the GMW proof systems under the explicit advice-PRG premise GMW.AdvicePRG.

References

• O. Goldreich, S. Micali, A. Wigderson, Proofs that Yield Nothing But Their Validity, or All Languages in NP Have Zero-Knowledge Proof Systems
• M. Naor, Bit Commitment Using Pseudorandomness
• O. Goldreich, Foundations of Cryptography: Volume 1, Basic Tools, Chapter 4.
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 9.

Restricted versus general auxiliary-input zero-knowledge predicates

def Cslib.Crypto.GenerableZeroKnowledge {α : Type} (enc : α ↪ List Bool) (prover : ℕ → α → List Bool → Complexity.Prover Unit) (isWitness : α → List Bool → Bool) : Prop

Uniform computational zero-knowledge with polynomial-time-generable families. For every uniform strict oracle PPT malicious verifier Vstar (taking security parameter n, instance a, and auxiliary input z, charged for the complete encoded input (1^n, (a, z))), there exists a single uniform strict PPT witness-free simulator S (chosen before the families and charged for (1^n, (a, z))) whose output ensemble is computationally indistinguishable from the real interaction output across all deterministic polynomial-time-generable families of instances a : ℕ → α, valid witnesses w : ℕ → List Bool (∀ n, isWitness (a n) (w n) = true), and auxiliary inputs z : ℕ → List Bool (ComputableInPolyTime · encUnary _).

def Cslib.Crypto.AuxiliaryInputZeroKnowledge {α : Type} (enc : α ↪ List Bool) (prover : ℕ → α → List Bool → Complexity.Prover Unit) (isWitness : α → List Bool → Bool) : Prop

General auxiliary-input computational zero-knowledge for arbitrary polynomially bounded valid families. For every uniform strict oracle PPT malicious verifier Vstar (charged for its complete encoded input (1^n, (a, z))), there exists a single uniform strict PPT witness-free simulator S (chosen before the families and distinguisher, and charged for (1^n, (a, z))) such that for all arbitrary polynomially bounded families of instances a : ℕ → α, valid witnesses w : ℕ → List Bool (∀ n, isWitness (a n) (w n) = true), and auxiliary inputs z : ℕ → List Bool, and for every uniform strict PPT distinguisher adversary (charged for its complete encoded input ((1^n, (a, z)), view)), the distinguishing advantage between the real interaction view and the simulated view is negligible.

theorem Cslib.Crypto.AuxiliaryInputZeroKnowledge.generableZeroKnowledge {α : Type} {enc : α ↪ List Bool} {prover : ℕ → α → List Bool → Complexity.Prover Unit} {isWitness : α → List Bool → Bool} (h : AuxiliaryInputZeroKnowledge enc prover isWitness) : GenerableZeroKnowledge enc prover isWitness

General auxiliary-input zero-knowledge implies poly-time-generable zero-knowledge. Every deterministic polynomial-time-generable family has polynomially bounded encoded output length, and every unary-indexed ComputationallyIndistinguishable distinguisher lifts to a full-input distinguisher by ignoring the extra (a, z) component.

theorem Cslib.Crypto.GenerableZeroKnowledge.advantage_negligible {α : Type} {enc : α ↪ List Bool} {prover : ℕ → α → List Bool → Complexity.Prover Unit} {isWitness : α → List Bool → Bool} (h : GenerableZeroKnowledge enc prover isWitness) {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} (hV : Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => Vstar p.1 p.2.1 p.2.2) : ∃ (S : ℕ → α → List Bool → ProbComp (List Bool)), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => S p.1 p.2.1 p.2.2) ∧ ∀ (a : ℕ → α) (w z : ℕ → List Bool), Turing.MultiTapeTM.ComputableInPolyTime a Turing.MultiTapeTM.encUnary enc → Turing.MultiTapeTM.ComputableInPolyTime w Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits → Turing.MultiTapeTM.ComputableInPolyTime z Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits → (∀ (n : ℕ), isWitness (a n) (w n) = true) → ∀ (adversary : ℕ → α → List Bool → List Bool → ProbComp Bool), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : (ℕ × α × List Bool) × List Bool) => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) → Negligible fun (n : ℕ) => (distinguishingGame (PMF.map Prod.fst ((prover n (a n) (w n)).run (Vstar n (a n) (z n)) (prover n (a n) (w n)).init)) (adversary n (a n) (z n))).advantage (distinguishingGame (S n (a n) (z n)).eval (adversary n (a n) (z n)))

Under GenerableZeroKnowledge, any full-input uniform strict PPT distinguisher adversary n (a n) (z n) also has negligible distinguishing advantage on deterministic polynomial-time-generable families a, w, z, since (a n, z n) can be recomputed from 1^n.

Bundled computational zero-knowledge proof systems

structure Cslib.Crypto.ZeroKnowledgeProof {α : Type} (enc : α ↪ List Bool) (A : Set α) : Type 1

A computational zero-knowledge interactive proof system for a language A : Set α (with instance encoding enc : α ↪ List Bool), indexed by a security parameter n : ℕ Goldreich, Micali, and Wigderson.

• verifier n a: the honest verifier's interactive program on security parameter n and instance a, certified uniform strict oracle PPT in (1^n, a) by isOraclePPT_verifier.
• prover n a w: the honest prover strategy on security parameter n, instance a, and witness w, certified efficient by interact, eval_interact, and isPPT_interact.
• isWitness a w: the bundled polynomial-time witness predicate characterizing membership in A (mem_iff_exists_witness). No witness-length bound is imposed, so isWitness by itself need not be an NP relation (in zero_knowledge, w is polynomial-time-generable in 1^n). When constructed via a Karp reduction f : α → CNF ℕ to ThreeSAT (PseudorandomGenerator.zeroKnowledgeProofOfReduction), isWitness a w is ThreeSAT.verifier (f a, w), checking a ThreeSAT witness for f a.
• complete and sound: completeness 1 for valid witnesses and soundness error at most 1 / 3 against all computationally unbounded stateful provers P : Prover Unit.
• zero_knowledge: uniform zero-knowledge with poly-time-generable families (GenerableZeroKnowledge enc prover isWitness). For every uniform strict oracle PPT malicious verifier Vstar (taking security parameter n, instance a, and auxiliary input z), there is a uniform strict PPT simulator S (taking (1^n, a, z) without any witness) whose output ensemble is computationally indistinguishable from the real interaction output across all deterministic polynomial-time-generable families of instances a : ℕ → α, valid witnesses w : ℕ → List Bool, and auxiliary inputs z : ℕ → List Bool (ComputableInPolyTime · encUnary _). The stronger general auxiliary-input property over arbitrary polynomially bounded valid families is stated separately as ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.

• verifier : ℕ → α → Probability.WordOracleComp Unit Bool

  The honest verifier, indexed by security parameter n and instance a.

• prover : ℕ → α → List Bool → Complexity.Prover Unit

  The honest prover strategy, taking security parameter n, instance a, and witness w.

• isWitness : α → List Bool → Bool

  The polynomial-time witness check used by the honest prover.

• polyTime_isWitness : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × List Bool) => self.isWitness p.1 p.2) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

  isWitness is computable in plain polynomial time.

• mem_iff_exists_witness (a : α) : a ∈ A ↔ ∃ (w : List Bool), self.isWitness a w = true

  a ∈ A if and only if some witness w satisfies isWitness a w = true.

• isOraclePPT_verifier : Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary enc) Turing.MultiTapeTM.encBool fun (p : ℕ × α) => self.verifier p.1 p.2

  The honest verifier is uniform strict oracle PPT in (1^n, a).

• interact : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool) → ProbComp (List Bool)

  The PPT program realizing the honest prover's interaction with a verifier program.

• eval_interact (n : ℕ) (a : α) (w : List Bool) (prog : Probability.WordOracleComp Unit (List Bool)) : (self.interact n a w prog).eval = PMF.map Prod.fst ((self.prover n a w).run prog (self.prover n a w).init)

  interact has the exact output distribution of prover.run.

• isPPT_interact (Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)) : (Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => Vstar p.1 p.2.1 p.2.2) → Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool × List Bool) => self.interact p.1 p.2.1 p.2.2.1 (Vstar p.1 p.2.1 p.2.2.2)

  Running any uniform strict oracle PPT verifier against the honest prover is uniform strict PPT in (1^n, a, w, z).

• complete (n : ℕ) (a : α) (w : List Bool) : self.isWitness a w = true → Complexity.acceptProb (self.verifier n a) (self.prover n a w) = 1

  Perfect completeness: for every valid witness w of a, the honest prover convinces the honest verifier with probability 1.

• sound (n : ℕ) (a : α) : a ∉ A → ∀ (P : Complexity.Prover Unit), Complexity.acceptProb (self.verifier n a) P ≤ 1 / 3

  Soundness: for every a ∉ A and every computationally unbounded stateful prover P, the verifier accepts with probability at most 1 / 3.

• zero_knowledge : GenerableZeroKnowledge enc self.prover self.isWitness

  Uniform computational zero-knowledge with poly-time-generable auxiliary input against all uniform strict oracle PPT malicious verifiers, quantified over polynomial-time-generable families of instances a, valid witnesses w, and auxiliary inputs z.

theorem Cslib.Crypto.ZeroKnowledgeProof.generableZeroKnowledge {α : Type} {enc : α ↪ List Bool} {A : Set α} (zk : ZeroKnowledgeProof enc A) : GenerableZeroKnowledge enc zk.prover zk.isWitness

Named projection for the restricted polynomial-time-generable zero-knowledge property bundled by ZeroKnowledgeProof.

def Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge {α : Type} {enc : α ↪ List Bool} {A : Set α} (zk : ZeroKnowledgeProof enc A) : Prop

General auxiliary-input computational zero-knowledge for a bundled ZeroKnowledgeProof system, ranging over arbitrary polynomially bounded instance, valid-witness, and auxiliary-input families.

theorem Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.generableZeroKnowledge {α : Type} {enc : α ↪ List Bool} {A : Set α} {zk : ZeroKnowledgeProof enc A} (h : zk.AuxiliaryInputZeroKnowledge) : GenerableZeroKnowledge enc zk.prover zk.isWitness

General auxiliary-input zero-knowledge for zk implies the bundled restricted GenerableZeroKnowledge guarantee.

theorem Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.zero_knowledge_const {α : Type} {enc : α ↪ List Bool} {A : Set α} {zk : ZeroKnowledgeProof enc A} (h : zk.AuxiliaryInputZeroKnowledge) {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} (hV : Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => Vstar p.1 p.2.1 p.2.2) : ∃ (S : ℕ → α → List Bool → ProbComp (List Bool)), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => S p.1 p.2.1 p.2.2) ∧ ∀ (a : α) (w : List Bool) (z : ℕ → List Bool), zk.isWitness a w = true → (PolynomiallyBounded fun (n : ℕ) => (z n).length) → ∀ (adversary : ℕ → α → List Bool → List Bool → ProbComp Bool), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : (ℕ × α × List Bool) × List Bool) => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) → Negligible fun (n : ℕ) => (distinguishingGame (PMF.map Prod.fst ((zk.prover n a w).run (Vstar n a (z n)) (zk.prover n a w).init)) (adversary n a (z n))).advantage (distinguishingGame (S n a (z n)).eval (adversary n a (z n)))

Fixed-instance auxiliary-input zero-knowledge under zk.AuxiliaryInputZeroKnowledge: for any fixed instance a, valid witness w, and arbitrary polynomially bounded auxiliary-input family z : ℕ → List Bool, the real and simulated views have negligible distinguishing advantage against every full-input uniform strict PPT distinguisher.

theorem Cslib.Crypto.ZeroKnowledgeProof.isInteractiveProof {α : Type} {enc : α ↪ List Bool} {A : Set α} (zk : ZeroKnowledgeProof enc A) (n : ℕ) : Complexity.IsInteractiveProof (zk.verifier n) A (2 / 3) (1 / 3)

At every security parameter n, the honest verifier of a zero-knowledge proof system is an interactive proof for A with completeness 2 / 3 and soundness 1 / 3.

theorem Cslib.Crypto.ZeroKnowledgeProof.mem_IP {α : Type} {enc : α ↪ List Bool} {A : Set α} (zk : ZeroKnowledgeProof enc A) : A ∈ Complexity.IP enc

Every language with a zero-knowledge interactive proof system belongs to IP.

theorem Cslib.Crypto.ZeroKnowledgeProof.zero_knowledge_const {α : Type} {enc : α ↪ List Bool} {A : Set α} (zk : ZeroKnowledgeProof enc A) {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} (hV : Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => Vstar p.1 p.2.1 p.2.2) : ∃ (S : ℕ → α → List Bool → ProbComp (List Bool)), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => S p.1 p.2.1 p.2.2) ∧ ∀ (a : α) (w : List Bool) (z : ℕ → List Bool), zk.isWitness a w = true → Turing.MultiTapeTM.ComputableInPolyTime z Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits → ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map Prod.fst ((zk.prover n a w).run (Vstar n a (z n)) (zk.prover n a w).init)) fun (n : ℕ) => (S n a (z n)).eval

Fixed-instance computational zero-knowledge: for every fixed instance a and valid witness w (zk.isWitness a w = true), and every polynomial-time auxiliary input family z : ℕ → List Bool, the real interaction output and simulator output are computationally indistinguishable.

GMW zero-knowledge proof systems

noncomputable def Cslib.Crypto.PseudorandomGenerator.zeroKnowledgeProofOfReduction {α : Type} {enc : α ↪ List Bool} {A : Set α} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) {f : α → Logic.PL.CNF ℕ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Complexity.encCNF) (hred : ∀ (a : α), a ∈ A ↔ f a ∈ Complexity.ThreeSAT) : ZeroKnowledgeProof enc A

Construct the Goldreich–Micali–Wigderson zero-knowledge proof system for any language A with a polynomial-time many-one reduction f : α → CNF ℕ to ThreeSAT, using a pseudorandom generator with stretch at least 3 * k + 1 and the 3-copy masked-3SAT commitment protocol in Cslib.Crypto.GMW. The bundled witness check isWitness a w is ThreeSAT.verifier (f a, w) on the reduced formula f a.

theorem Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction {α : Type} {enc : α ↪ List Bool} {A : Set α} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) {f : α → Logic.PL.CNF ℕ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Complexity.encCNF) (hred : ∀ (a : α), a ∈ A ↔ f a ∈ Complexity.ThreeSAT) (hAdv : GMW.AdvicePRG enc generator length) : (hG.zeroKnowledgeProofOfReduction hstretch hf hred).AuxiliaryInputZeroKnowledge

Under the explicit advice-PRG premise GMW.AdvicePRG enc generator length, the GMW proof system hG.zeroKnowledgeProofOfReduction hstretch hf hred satisfies general auxiliary-input zero-knowledge (ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge) across all arbitrary polynomially bounded valid instance, witness, and auxiliary-input families.

noncomputable def Cslib.Crypto.PseudorandomGenerator.zeroKnowledgeProofThreeSAT {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) : ZeroKnowledgeProof Complexity.encCNF Complexity.ThreeSAT

The Goldreich–Micali–Wigderson computational zero-knowledge proof system for ThreeSAT, built from any pseudorandom generator with stretch at least 3 * k + 1 via the 3-copy masked-3SAT commitment protocol in Cslib.Crypto.GMW.

theorem Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) (hAdv : GMW.AdvicePRG Complexity.encCNF generator length) : (hG.zeroKnowledgeProofThreeSAT hstretch).AuxiliaryInputZeroKnowledge

Under the explicit advice-PRG premise GMW.AdvicePRG encCNF generator length, the GMW proof system hG.zeroKnowledgeProofThreeSAT hstretch satisfies general auxiliary-input zero-knowledge (ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge).

theorem Cslib.Crypto.PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP {α : Type} {enc : α ↪ List Bool} {A : Set α} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) (hA : A ∈ Complexity.NP enc) : Nonempty (ZeroKnowledgeProof enc A)

Goldreich–Micali–Wigderson theorem (from a pseudorandom generator). Given a pseudorandom generator with stretch at least 3 * k + 1 (such as fun k => 3 * k + 1), every language A ∈ NP enc has a computational zero-knowledge interactive proof system Goldreich, Micali, and Wigderson in the uniform polynomial-time-generable sense (GenerableZeroKnowledge).

theorem Cslib.Crypto.PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP {α : Type} {enc : α ↪ List Bool} {A : Set α} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) (hAdv : GMW.AdvicePRG enc generator length) (hA : A ∈ Complexity.NP enc) : ∃ (zk : ZeroKnowledgeProof enc A), zk.AuxiliaryInputZeroKnowledge

Goldreich–Micali–Wigderson theorem under an explicit advice-PRG premise. Given a pseudorandom generator with stretch at least 3 * k + 1 that also satisfies the advice-supplied premise GMW.AdvicePRG enc generator length, every language A ∈ NP enc has a computational zero-knowledge interactive proof system satisfying general auxiliary-input zero-knowledge (ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge) across all polynomially bounded valid families. This theorem takes GMW.AdvicePRG as an explicit hypothesis rather than deriving it from uniform PseudorandomGenerator or OneWay security.

theorem Cslib.Crypto.OneWay.exists_zeroKnowledgeProof_of_mem_NP {α : Type} {enc : α ↪ List Bool} {A : Set α} {f : List Bool → List Bool} (hf : OneWay f) (hA : A ∈ Complexity.NP enc) : Nonempty (ZeroKnowledgeProof enc A)

Goldreich–Micali–Wigderson theorem (from a one-way function). If a one-way function exists, then every language A ∈ NP enc has a computational zero-knowledge interactive proof system Goldreich, Micali, and Wigderson, in the uniform-family sense of GenerableZeroKnowledge (ZeroKnowledgeProof.zero_knowledge): instances, witnesses and auxiliary inputs range over polynomial-time-generable families rather than arbitrary ones.