Polynomial-time and PPT certificates for the 3-copy GMW protocol

This module registers @[fun_prop] polynomial-time and strict-(oracle-)PPT certificates for the 3-copy masked-3SAT GMW protocol gadgets defined in Complexity.Crypto.Computational.GMW.Protocol, proves that runTwoRound preserves strict PPT when driven by polynomial-time round functions and a strict oracle PPT verifier (isPPTOn_runTwoRound), defines the zero-knowledge simulator gmwSimulator (via gmwFirstSuccess, gmwSampleSimCoins, gmwSimWithPads, gmwSimAttempt), and certifies:

• isOraclePPTOn_gmwVerifier: the honest verifier gmwVerifier is uniform strict oracle PPT;
• isPPTOn_gmwInteract: running any uniform strict oracle PPT verifier against the honest prover is uniform strict PPT;
• isPPTOn_gmwSimulator: the GMW zero-knowledge simulator gmwSimulator is uniform strict PPT.

Main definitions

• Cslib.Crypto.GMW.gmwFirstSuccess: extracts the payload of the first successful simulation attempt (true :: out) from a list of attempts.
• Cslib.Crypto.GMW.gmwSampleSimCoins, Cslib.Crypto.GMW.gmwSimWithPads, Cslib.Crypto.GMW.gmwSimAttempt: single-attempt GMW simulator components.
• Cslib.Crypto.GMW.gmwSimulator: the GMW zero-knowledge simulator repeating gmwSimAttempt n + 1 times.

Main results

• Cslib.Crypto.GMW.isOraclePPTOn_gmwVerifier: gmwVerifier is IsOraclePPTOn.
• Cslib.Crypto.GMW.isPPTOn_gmwInteract: gmwInteract is IsPPTOn.
• Cslib.Crypto.GMW.isPPTOn_gmwSimulator: gmwSimulator is IsPPTOn.

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

Polynomial-time certificates for protocol gadgets

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwBit0Of8 {α : Type} {input : α ↪ List Bool} {t : α → ℕ} (ht : Turing.MultiTapeTM.ComputableTidilyInPolyTime t input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwBit0Of8 (t a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwBit1Of8 {α : Type} {input : α ↪ List Bool} {t : α → ℕ} (ht : Turing.MultiTapeTM.ComputableTidilyInPolyTime t input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwBit1Of8 (t a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwBit2Of8 {α : Type} {input : α ↪ List Bool} {t : α → ℕ} (ht : Turing.MultiTapeTM.ComputableTidilyInPolyTime t input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwBit2Of8 (t a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwActiveIdx {α : Type} {input : α ↪ List Bool} {b₀ b₁ b₂ : α → Bool} (hb₀ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₀ input Turing.MultiTapeTM.encBool) (hb₁ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₁ input Turing.MultiTapeTM.encBool) (hb₂ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₂ input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwActiveIdx (b₀ a) (b₁ a) (b₂ a)) input Turing.MultiTapeTM.encUnary

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_clauseEvalBits {α : Type} {input : α ↪ List Bool} {c : α → Logic.PL.Clause ℕ} {b₀ b₁ b₂ : α → Bool} (hc : Turing.MultiTapeTM.ComputableTidilyInPolyTime c input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) (hb₀ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₀ input Turing.MultiTapeTM.encBool) (hb₁ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₁ input Turing.MultiTapeTM.encBool) (hb₂ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₂ input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => clauseEvalBits (c a) (b₀ a) (b₁ a) (b₂ a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_varBit {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {vec : α → List Bool} {v : α → ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hvec : Turing.MultiTapeTM.ComputableTidilyInPolyTime vec input Turing.MultiTapeTM.encBits) (hv : Turing.MultiTapeTM.ComputableTidilyInPolyTime v input Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => varBit (φ a) (vec a) (v a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_clauseTableRow {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {m : α → List Bool} {c : α → Logic.PL.Clause ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encBits) (hc : Turing.MultiTapeTM.ComputableTidilyInPolyTime c input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => clauseTableRow (φ a) (m a) (c a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_clauseActiveRow {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {v : α → List Bool} {c : α → Logic.PL.Clause ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hv : Turing.MultiTapeTM.ComputableTidilyInPolyTime v input Turing.MultiTapeTM.encBits) (hc : Turing.MultiTapeTM.ComputableTidilyInPolyTime c input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => clauseActiveRow (φ a) (v a) (c a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_tableBits {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {m : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => tableBits (φ a) (m a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_activeTableFlags {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {v : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hv : Turing.MultiTapeTM.ComputableTidilyInPolyTime v input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => activeTableFlags (φ a) (v a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_copyLen {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => copyLen (φ a)) input Turing.MultiTapeTM.encUnary

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_totalLen {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => totalLen (φ a)) input Turing.MultiTapeTM.encUnary

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_mPart {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {copy : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hcopy : Turing.MultiTapeTM.ComputableTidilyInPolyTime copy input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => mPart (φ a) (copy a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_vPart {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {copy : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hcopy : Turing.MultiTapeTM.ComputableTidilyInPolyTime copy input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => vPart (φ a) (copy a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_tablePart {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {copy : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hcopy : Turing.MultiTapeTM.ComputableTidilyInPolyTime copy input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => tablePart (φ a) (copy a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_realCopyBits {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {w m : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encBits) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => realCopyBits (φ a) (w a) (m a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_simCopyBits {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {b : α → Bool} {rand : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b input Turing.MultiTapeTM.encBool) (hrand : Turing.MultiTapeTM.ComputableTidilyInPolyTime rand input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => simCopyBits (φ a) (b a) (rand a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_copyOpenFlags {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {b : α → Bool} {copy : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b input Turing.MultiTapeTM.encBool) (hcopy : Turing.MultiTapeTM.ComputableTidilyInPolyTime copy input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => copyOpenFlags (φ a) (b a) (copy a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_verifyCopyBits {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {b : α → Bool} {copy : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b input Turing.MultiTapeTM.encBool) (hcopy : Turing.MultiTapeTM.ComputableTidilyInPolyTime copy input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => verifyCopyBits (φ a) (b a) (copy a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwCopy0 {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {bits : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwCopy0 (φ a) (bits a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwCopy1 {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {bits : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwCopy1 (φ a) (bits a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwCopy2 {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {bits : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwCopy2 (φ a) (bits a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_realBits {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {w m₀ m₁ m₂ : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encBits) (hm₀ : Turing.MultiTapeTM.ComputableTidilyInPolyTime m₀ input Turing.MultiTapeTM.encBits) (hm₁ : Turing.MultiTapeTM.ComputableTidilyInPolyTime m₁ input Turing.MultiTapeTM.encBits) (hm₂ : Turing.MultiTapeTM.ComputableTidilyInPolyTime m₂ input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => realBits (φ a) (w a) (m₀ a) (m₁ a) (m₂ a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_simBits {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {ch r₀ r₁ r₂ : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hch : Turing.MultiTapeTM.ComputableTidilyInPolyTime ch input Turing.MultiTapeTM.encBits) (hr₀ : Turing.MultiTapeTM.ComputableTidilyInPolyTime r₀ input Turing.MultiTapeTM.encBits) (hr₁ : Turing.MultiTapeTM.ComputableTidilyInPolyTime r₁ input Turing.MultiTapeTM.encBits) (hr₂ : Turing.MultiTapeTM.ComputableTidilyInPolyTime r₂ input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => simBits (φ a) (ch a) (r₀ a) (r₁ a) (r₂ a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_allOpenFlags {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {ch bits : α → List Bool} (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hch : Turing.MultiTapeTM.ComputableTidilyInPolyTime ch input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => allOpenFlags (φ a) (ch a) (bits a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_proverReply1 {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {m : α → ℕ} {r openFlags bits : α → List Bool} {seeds pads : α → List (List Bool)} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openFlags input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) (hseeds : Turing.MultiTapeTM.ComputableTidilyInPolyTime seeds input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hpads : Turing.MultiTapeTM.ComputableTidilyInPolyTime pads input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => proverReply1 generator (m a) (r a) (openFlags a) (bits a) (seeds a) (pads a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_proverReply2 {α : Type} {input : α ↪ List Bool} {s : α → ℕ} {φ : α → Logic.PL.CNF ℕ} {ch bits : α → List Bool} {seeds : α → List (List Bool)} (hs : Turing.MultiTapeTM.ComputableTidilyInPolyTime s input Turing.MultiTapeTM.encUnary) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hch : Turing.MultiTapeTM.ComputableTidilyInPolyTime ch input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) (hseeds : Turing.MultiTapeTM.ComputableTidilyInPolyTime seeds input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => proverReply2 (s a) (φ a) (ch a) (bits a) (seeds a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_verifyCommitments {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {s m : α → ℕ} {φ : α → Logic.PL.CNF ℕ} {r flags commitReply openedBits openSeedsFlat : α → List Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hs : Turing.MultiTapeTM.ComputableTidilyInPolyTime s input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hflags : Turing.MultiTapeTM.ComputableTidilyInPolyTime flags input Turing.MultiTapeTM.encBits) (hcommit : Turing.MultiTapeTM.ComputableTidilyInPolyTime commitReply input Turing.MultiTapeTM.encBits) (hopened : Turing.MultiTapeTM.ComputableTidilyInPolyTime openedBits input Turing.MultiTapeTM.encBits) (hseeds : Turing.MultiTapeTM.ComputableTidilyInPolyTime openSeedsFlat input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => verifyCommitments generator (s a) (m a) (φ a) (r a) (flags a) (commitReply a) (openedBits a) (openSeedsFlat a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_verifyTranscript {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {s m : α → ℕ} {φ : α → Logic.PL.CNF ℕ} {r commitReply ch openReply : α → List Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hs : Turing.MultiTapeTM.ComputableTidilyInPolyTime s input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hcommit : Turing.MultiTapeTM.ComputableTidilyInPolyTime commitReply input Turing.MultiTapeTM.encBits) (hch : Turing.MultiTapeTM.ComputableTidilyInPolyTime ch input Turing.MultiTapeTM.encBits) (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openReply input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => verifyTranscript generator (s a) (m a) (φ a) (r a) (commitReply a) (ch a) (openReply a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.GMW.isOraclePPTOn_gmwVerifier {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → Logic.PL.CNF ℕ} (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) : Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary enc) Turing.MultiTapeTM.encBool fun (p : ℕ × α) => gmwVerifier generator length f p.1 p.2

PPT certificates for runTwoRound and honest interaction

theorem Cslib.Crypto.GMW.isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input : Caller ↪ List Bool} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} {prepare : Caller → ℕ × α × List Bool} {reply1 reply2 : Caller × List Bool → List Bool} {bound : Caller → ℕ} (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) (hprep : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits))) (hr1 : Turing.MultiTapeTM.ComputableTidilyInPolyTime reply1 (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hr2 : Turing.MultiTapeTM.ComputableTidilyInPolyTime reply2 (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hle1 : ∀ (c : Caller) (q : List Bool), (reply1 (c, q)).length ≤ bound c) (hle2 : ∀ (c : Caller) (q : List Bool), (reply2 (c, q)).length ≤ bound c) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) fun (c : Caller) => runTwoRound (fun (q : List Bool) => reply1 (c, q)) (fun (q : List Bool) => reply2 (c, q)) (Vstar (prepare c).1 (prepare c).2.1 (prepare c).2.2) (0, [false, false, false])

theorem Cslib.Crypto.GMW.isPPTOn_runTwoRound_prover {α Caller : Type} {enc : α ↪ List Bool} {input : Caller ↪ List Bool} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List Bool)} {generator : List Bool → List Bool} {n s m : Caller → ℕ} {a : Caller → α} {z : Caller → List Bool} {φ : Caller → Logic.PL.CNF ℕ} {openFlags bits ch_guess : Caller → List Bool} {seeds pads : Caller → List (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) (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableTidilyInPolyTime s input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableTidilyInPolyTime a input enc) (hz : Turing.MultiTapeTM.ComputableTidilyInPolyTime z input Turing.MultiTapeTM.encBits) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openFlags input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) (hch : Turing.MultiTapeTM.ComputableTidilyInPolyTime ch_guess input Turing.MultiTapeTM.encBits) (hseeds : Turing.MultiTapeTM.ComputableTidilyInPolyTime seeds input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hpads : Turing.MultiTapeTM.ComputableTidilyInPolyTime pads input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) fun (c : Caller) => runTwoRound (fun (r : List Bool) => proverReply1 generator (m c) r (openFlags c) (bits c) (seeds c) (pads c)) (fun (x : List Bool) => proverReply2 (s c) (φ c) (ch_guess c) (bits c) (seeds c)) (Vstar (n c) (a c) (z c)) (0, [false, false, false])

GMW zero-knowledge simulator and its PPT certificate

def Cslib.Crypto.GMW.gmwFirstSuccess (attempts : List (List Bool)) : List Bool

Extract the payload of the first successful GMW simulation attempt (true :: out), or [] if all attempts failed ([]).

theorem Cslib.Crypto.GMW.computableTidilyInPolyTime_gmwFirstSuccess {α : Type} {input : α ↪ List Bool} {attempts : α → List (List Bool)} (ha : Turing.MultiTapeTM.ComputableTidilyInPolyTime attempts input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => gmwFirstSuccess (attempts a)) input Turing.MultiTapeTM.encBits

noncomputable def Cslib.Crypto.GMW.gmwSampleSimCoins (s : ℕ) (φ : Logic.PL.CNF ℕ) (ch_guess : List Bool) : ProbComp (List Bool × List (List Bool))

Sample the GMW simulator's random strings and commitment seeds for a guessed challenge ch_guess, returning (simBits φ ch_guess r₀ r₁ r₂, seeds).

theorem Cslib.Crypto.GMW.isPPTOn_gmwSampleSimCoins {α : Type} {input : α ↪ List Bool} {s : α → ℕ} {φ : α → Logic.PL.CNF ℕ} {ch_guess : α → List Bool} (hs : Turing.MultiTapeTM.ComputableTidilyInPolyTime s input Turing.MultiTapeTM.encUnary) (hφ : Turing.MultiTapeTM.ComputableTidilyInPolyTime φ input Complexity.encCNF) (hch : Turing.MultiTapeTM.ComputableTidilyInPolyTime ch_guess input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => gmwSampleSimCoins (s a) (φ a) (ch_guess a)

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

Run one simulated GMW attempt with pre-sampled unopened pads pads (without any witness).

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

One attempt of the GMW zero-knowledge simulator (without any witness).

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

The GMW zero-knowledge simulator: repeat gmwSimAttempt n + 1 times and return the first successful output (gmwFirstSuccess).

theorem Cslib.Crypto.GMW.isPPTOn_gmwSimulator {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → Logic.PL.CNF ℕ} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List 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) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × α × List Bool) => gmwSimulator generator length f Vstar p.1 p.2.1 p.2.2

theorem Cslib.Crypto.GMW.isPPTOn_gmwInteract {α : Type} {enc : α ↪ List Bool} {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → Logic.PL.CNF ℕ} {Vstar : ℕ → α → List Bool → Probability.WordOracleComp Unit (List 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) : 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) => gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1 (Vstar p.1 p.2.1 p.2.2.2)