Pointwise reduction and zero-knowledge simulation for the 3-copy GMW protocol

gmwViewReduction is one uniform PRG-challenge test whose ordinary input contains the unary security parameter, instance, witness, auxiliary word and challenge. For every valid tuple, gmwView_advantage_le bounds the real/simulated view advantage by (7 / 8) ^ (n + 1) plus dyadicSize (n + 1) * dyadicSize (totalLen (f a)) times this test's PRG advantage at seed parameter n + 7. No security or efficient-generation assumption is used in that finite bound. The final view test receives the instance and auxiliary word in both games. The simulator gmwSimulator remains witness-free.

isPPTOn_gmwViewReduction charges the complete encoded input, both hybrid selections, all surrounding samples and the malicious verifier's adaptive computation and retained private state. The existing uniform-family theorem gmwView_indistinguishable_gmwSimulator follows from this finite bound and certificate under uniform PRG security, for deterministic polynomial-time instance/witness/auxiliary families.

gmwView_negligible_of_advice_prg instead permits arbitrary families with three separate polynomial encoding-length bounds, under an explicit stronger PRG premise against uniform full-input tests supplied those families as advice. This module does not derive that premise from uniform one-wayness or HILL. Unbounded auxiliary input with a clock independent of its length, witness-level Levin reductions, and sequential soundness amplification remain separate.

The proof uses four distribution transformations:

1. Guess a uniform 3-bit challenge in each of n + 1 independent attempts. The probability of no success is (7 / 8) ^ (n + 1) (advantage_repeatAttempt_le).
2. Factor the commitment seeds into active seeds and pseudorandom unopened pads without changing the attempt distribution (eval_game0Pads_eq_eval_game0).
3. Apply sequenceTest_advantage once to attempts and once to unopened pads. The resulting product of dyadic-range losses is exact (gmwViewReduction_advantage), including zero pads.
4. Uniform unopened pads eliminate the witness from each attempt (eval_game1_eq_eval_gmwSimAttempt), giving the existing witness-free simulator.

Main definitions

• Cslib.Crypto.GMW.gmwRealWithPads: a guessed-challenge attempt with supplied unopened pads.
• Cslib.Crypto.GMW.gmwRealPRGPads, Cslib.Crypto.GMW.gmwRealUniformPads: its two pad sources.
• Cslib.Crypto.GMW.gmwViewReduction: the single-challenge pointwise reduction.
• Cslib.Crypto.GMW.AdvicePRG: explicit advice-supplied PRG premise at seed size n + 7 for arbitrary polynomially bounded instance, witness, and auxiliary-input families.

Main results

• Cslib.Crypto.GMW.gmwView_advantage_le: unconditional finite view-advantage reduction.
• Cslib.Crypto.GMW.isPPTOn_gmwViewReduction: strict full-input polynomial-time certificate.
• Cslib.Crypto.GMW.gmwView_negligible_of_advice_prg: the stronger advice-PRG consequence.
• Cslib.Crypto.GMW.gmwView_indistinguishable_gmwSimulator: the existing uniform-family result.

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.

Step 1: Replacing the verifier's challenge in runTwoRound by a random guess

Step 2: Introducing unopened pads via naorSelectPads

noncomputable def Cslib.Crypto.GMW.gmwRealWithPads (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (w : List Bool) (prog : Probability.WordOracleComp Unit (List Bool)) (pads : List (List Bool)) : ProbComp (List Bool)

Run one attempt with pre-sampled unopened pads pads and active flags allOpenFlags φ ch_guess bits.

noncomputable def Cslib.Crypto.GMW.gmwRealPRGPads (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (w : List Bool) (prog : Probability.WordOracleComp Unit (List Bool)) : ProbComp (List Bool)

Single-attempt hybrid with pseudorandom unopened pads.

noncomputable def Cslib.Crypto.GMW.gmwRealUniformPads (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (w : List Bool) (prog : Probability.WordOracleComp Unit (List Bool)) : ProbComp (List Bool)

Single-attempt hybrid with uniform unopened pads.

Eliminating the witness: masking unopened committed bits and eliminating the witness

A pointwise finite reduction

noncomputable def Cslib.Crypto.GMW.gmwViewReduction {α : Type} (generator : List Bool → List Bool) (length : ℕ → ℕ) (f : α → Logic.PL.CNF ℕ) (Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)) (adversary : ℕ → α → List Bool → List Bool → ProbComp Bool) (n : ℕ) (a : α) (w z challenge : List Bool) : ProbComp Bool

A single PRG-challenge test for the complete GMW view. The ordinary input is the security parameter n, instance a, witness w, auxiliary word z, and PRG challenge. Two independently sampled dyadic indices select an attempt and an unopened pad. The remaining attempts and pads are generated by this program, including the verifier's adaptive queries and private randomness.

The simulator remains witness-free; only the reduction is given w. No security or validity assumption is needed to define this program. Its PRG challenge has seed parameter n + 7.

theorem Cslib.Crypto.GMW.gmwView_advantage_le {α : Type} (generator : List Bool → List Bool) (length : ℕ → ℕ) (f : α → Logic.PL.CNF ℕ) (Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)) (adversary : ℕ → α → List Bool → List Bool → ProbComp Bool) (n : ℕ) (a : α) (w z : List Bool) (hw : Complexity.ThreeSAT.verifier (f a, w) = true) : (distinguishingGame (PMF.map Prod.fst ((gmwProver generator (n + 7) (length (n + 7)) (f a) w).run (Vstar n a z) (gmwProver generator (n + 7) (length (n + 7)) (f a) w).init)) (adversary n a z)).advantage (distinguishingGame (gmwSimulator generator length f Vstar n a z).eval (adversary n a z)) ≤ (7 / 8) ^ (n + 1) + ↑(Probability.dyadicSize (n + 1)) * ↑(Probability.dyadicSize (totalLen (f a))) * Game.advantage (generator <$> BitString.sampleList (n + 7) >>= gmwViewReduction generator length f Vstar adversary n a w z).eval (BitString.sampleList (length (n + 7)) >>= gmwViewReduction generator length f Vstar adversary n a w z).eval

Pointwise finite GMW view reduction for every valid instance, witness and auxiliary word. The two dyadic factors are exact hybrid losses; the remaining term bounds failure of all n + 1 challenge guesses. The PRG challenge uses the protocol's shifted seed size n + 7.

This is an unconditional reduction identity and statistical bound, not a PRG-security premise. In particular no efficient generation of a, w or z is assumed. The test receives the same public instance and auxiliary word in both views, and the simulator receives no witness.

theorem Cslib.Crypto.GMW.isPPTOn_gmwViewReduction {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → Logic.PL.CNF ℕ} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} {adversary : ℕ → α → List Bool → List Bool → ProbComp Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f enc Complexity.encCNF) (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) (hadv : 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) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : (ℕ × α × List Bool × List Bool) × List Bool) => gmwViewReduction generator length f Vstar adversary p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2

The reduction has a strict uniform clock polynomial in its entire ordinary input. In particular the encoded witness and auxiliary word are charged, without requiring either to be generated efficiently from n. The certificate includes both hybrid indices, all surrounding samples, and the verifier interaction; the verifier may retain its private coins in its output.

theorem Cslib.Crypto.GMW.gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → Logic.PL.CNF ℕ} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} {adversary : ℕ → α → List Bool → List Bool → ProbComp Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f enc Complexity.encCNF) (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) (hadv : 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) (hPRG : ∀ (test : (ℕ × α × List Bool × List Bool) × List Bool → ProbComp Bool), Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool test → ∀ (a : ℕ → α) (w z : ℕ → List Bool), (PolynomiallyBounded fun (n : ℕ) => (enc (a n)).length) → (PolynomiallyBounded fun (n : ℕ) => (w n).length) → (PolynomiallyBounded fun (n : ℕ) => (z n).length) → Negligible fun (n : ℕ) => Game.advantage (do let challenge ← generator <$> BitString.sampleList (n + 7) test ((n, a n, w n, z n), challenge)).eval (do let challenge ← BitString.sampleList (length (n + 7)) test ((n, a n, w n, z n), challenge)).eval) {a : ℕ → α} {w z : ℕ → List Bool} (ha : PolynomiallyBounded fun (n : ℕ) => (enc (a n)).length) (hw : PolynomiallyBounded fun (n : ℕ) => (w n).length) (hz : PolynomiallyBounded fun (n : ℕ) => (z n).length) (hw_sat : ∀ (n : ℕ), Complexity.ThreeSAT.verifier (f (a n), w n) = true) : Negligible fun (n : ℕ) => (distinguishingGame (PMF.map Prod.fst ((gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).run (Vstar n (a n) (z n)) (gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).init)) (adversary n (a n) (z n))).advantage (distinguishingGame (gmwSimulator generator length f Vstar n (a n) (z n)).eval (adversary n (a n) (z n)))

Auxiliary-input consequence under an explicitly stronger PRG premise. The three families may be arbitrary, subject to their separate polynomial encoding-length bounds. hPRG supplies those families as ordinary advice to every full-input PPT challenge test, at seed size n + 7. It is not a consequence established here of uniform PRG security or uniform one-wayness.

Both the verifier and final test have clocks polynomial in their complete encoded inputs. This does not cover unbounded auxiliary words with clocks bounded only in the security parameter and common-input length. Witness-level Levin reductions and sequential amplification are separate from this single-execution masked-3SAT view theorem.

def Cslib.Crypto.GMW.AdvicePRG {α : Type} (enc : α ↪ List Bool) (generator : List Bool → List Bool) (length : ℕ → ℕ) : Prop

Explicit advice-PRG premise at GMW seed size n + 7 for an instance encoding enc: generator has output length length, is computable in polynomial time, and its output at seed length n + 7 is indistinguishable from uniform strings of length length (n + 7) against every full-input uniform strict PPT test supplied with arbitrary polynomially bounded instance, witness, and auxiliary-input families (a, w, z).

This stronger advice-supplied premise is not derived here from uniform PseudorandomGenerator security or uniform OneWay security.

theorem Cslib.Crypto.GMW.AdvicePRG.gmwView_negligible {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → Logic.PL.CNF ℕ} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} {adversary : ℕ → α → List Bool → List Bool → ProbComp Bool} (hAdv : AdvicePRG enc generator length) (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Complexity.encCNF) (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) (hadv : 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) {a : ℕ → α} {w z : ℕ → List Bool} (ha : PolynomiallyBounded fun (n : ℕ) => (enc (a n)).length) (hw : PolynomiallyBounded fun (n : ℕ) => (w n).length) (hz : PolynomiallyBounded fun (n : ℕ) => (z n).length) (hw_sat : ∀ (n : ℕ), Complexity.ThreeSAT.verifier (f (a n), w n) = true) : Negligible fun (n : ℕ) => (distinguishingGame (PMF.map Prod.fst ((gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).run (Vstar n (a n) (z n)) (gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).init)) (adversary n (a n) (z n))).advantage (distinguishingGame (gmwSimulator generator length f Vstar n (a n) (z n)).eval (adversary n (a n) (z n)))

Under AdvicePRG enc generator length, the real GMW interaction view and gmwSimulator have negligible distinguishing advantage against every full-input uniform strict PPT distinguisher across all polynomially bounded valid instance, witness, and auxiliary-input families.

theorem Cslib.Crypto.GMW.gmwView_indistinguishable_gmwSimulator {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) {f : α → Logic.PL.CNF ℕ} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f enc Complexity.encCNF) {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) {a : ℕ → α} {w z : ℕ → List Bool} (ha : Turing.MultiTapeTM.ComputableTidilyInPolyTime a Turing.MultiTapeTM.encUnary enc) (hw_comp : Turing.MultiTapeTM.ComputableTidilyInPolyTime w Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (hz : Turing.MultiTapeTM.ComputableTidilyInPolyTime z Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (hw_sat : ∀ (n : ℕ), Complexity.ThreeSAT.verifier (f (a n), w n) = true) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map Prod.fst ((gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).run (Vstar n (a n) (z n)) (gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).init)) fun (n : ℕ) => (gmwSimulator generator length f Vstar n (a n) (z n)).eval

Zero-knowledge simulation of the 3-copy GMW protocol. For any uniform strict oracle PPT malicious verifier Vstar and any deterministic polynomial-time families of instances a, valid ThreeSAT witnesses w, and auxiliary inputs z, the real interaction view of Vstar with gmwProver is computationally indistinguishable from gmwSimulator.