Three-copy masked-3SAT commitment protocol for GMW zero-knowledge

This module defines the two-round interactive protocol used to prove Goldreich, Micali, and Wigderson's theorem [GMW91] that every language in NP has a computational zero-knowledge interactive proof system from one-way functions (via Naor's bit commitment scheme [Nao91] and ThreeSAT_npHard).

Rather than GMW's original 3-coloring protocol, we formalize a direct 3-copy masked-3SAT truth-table commitment protocol: in each of 3 parallel copies, the prover samples a random mask m for the variables of the 3CNF formula φ and commits (via naorCommit) to copyLen φ bits consisting of m, the XOR-masked assignment v = w ⊕ m, and the 8-bit truth table of each clause under inputs t ⊕ m. A 3-bit challenge ch selects for each copy whether to open m and the full clause truth tables (ch[j] = false) or v and the active truth-table entries (ch[j] = true).

Main definitions

• Cslib.Crypto.GMW.realBits, Cslib.Crypto.GMW.simBits, Cslib.Crypto.GMW.allOpenFlags: committed bit layouts and selective-opening masks across the three protocol copies.
• Cslib.Crypto.GMW.proverReply1, Cslib.Crypto.GMW.proverReply2, Cslib.Crypto.GMW.verifyTranscript: prover round functions and verifier transcript predicate.
• Cslib.Crypto.GMW.runTwoRound: two-round deterministic oracle handler in ProbComp.
• Cslib.Crypto.GMW.gmwProver, Cslib.Crypto.GMW.gmwInteract: honest prover strategy and its ProbComp realization.
• Cslib.Crypto.GMW.gmwVerifier: honest two-round GMW verifier.

Main results

• Cslib.Crypto.GMW.naorMaskBits_realBits: selectively opening the honest committed bits under any challenge ch and valid witness w yields simBits.
• Cslib.Crypto.GMW.run_gmwProver_fst, Cslib.Crypto.GMW.eval_gmwInteract: running a verifier against gmwProver coincides with gmwInteract.

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.

Masked 3SAT truth-table gadgets

def Cslib.Crypto.GMW.gmwBit0Of8 (t : ℕ) : Bool

Bit 0 of a 3-bit truth-table row index t < 8.

def Cslib.Crypto.GMW.gmwBit1Of8 (t : ℕ) : Bool

Bit 1 of a 3-bit truth-table row index t < 8.

def Cslib.Crypto.GMW.gmwBit2Of8 (t : ℕ) : Bool

Bit 2 of a 3-bit truth-table row index t < 8.

def Cslib.Crypto.GMW.gmwActiveIdx (b₀ b₁ b₂ : Bool) : ℕ

Pack three literal-variable bits into an active truth-table row index in 0..7.

theorem Cslib.Crypto.GMW.gmwActiveIdx_lt_eight (b₀ b₁ b₂ : Bool) : gmwActiveIdx b₀ b₁ b₂ < 8

@[simp]

theorem Cslib.Crypto.GMW.gmwBit0Of8_gmwActiveIdx (b₀ b₁ b₂ : Bool) : gmwBit0Of8 (gmwActiveIdx b₀ b₁ b₂) = b₀

@[simp]

theorem Cslib.Crypto.GMW.gmwBit1Of8_gmwActiveIdx (b₀ b₁ b₂ : Bool) : gmwBit1Of8 (gmwActiveIdx b₀ b₁ b₂) = b₁

@[simp]

theorem Cslib.Crypto.GMW.gmwBit2Of8_gmwActiveIdx (b₀ b₁ b₂ : Bool) : gmwBit2Of8 (gmwActiveIdx b₀ b₁ b₂) = b₂

def Cslib.Crypto.GMW.clauseEvalBits (c : Logic.PL.Clause ℕ) (b₀ b₁ b₂ : Bool) : Bool

Evaluate a clause of length at most 3 given the truth values of its first three literals' variables.

theorem Cslib.Crypto.GMW.clauseEvalBits_eq_eval {c : Logic.PL.Clause ℕ} (hc : List.length c ≤ 3) (σ : ℕ → Bool) : clauseEvalBits c (σ (List.getD c 0 (0, false)).1) (σ (List.getD c 1 (0, false)).1) (σ (List.getD c 2 (0, false)).1) = Logic.PL.Clause.eval σ c

def Cslib.Crypto.GMW.varBit (φ : Logic.PL.CNF ℕ) (vec : List Bool) (v : ℕ) : Bool

Look up the bit for variable v in vec at its first occurrence in φ.vars, returning false when v ∉ φ.vars.

@[simp]

theorem Cslib.Crypto.GMW.varBit_listXor (φ : Logic.PL.CNF ℕ) (w m : List Bool) (v : ℕ) : varBit φ (BitString.listXor φ.vars.length [w, m]) v = (varBit φ w v ^^ varBit φ m v)

@[simp]

theorem Cslib.Crypto.GMW.varBit_listRow (φ : Logic.PL.CNF ℕ) (vec : List Bool) (v : ℕ) : varBit φ (BitString.listRow φ.vars.length 0 vec) v = varBit φ vec v

def Cslib.Crypto.GMW.clauseTableRow (φ : Logic.PL.CNF ℕ) (m : List Bool) (c : Logic.PL.Clause ℕ) : List Bool

The 8-bit masked truth table of clause c under variable mask m.

def Cslib.Crypto.GMW.clauseActiveRow (φ : Logic.PL.CNF ℕ) (v : List Bool) (c : Logic.PL.Clause ℕ) : List Bool

The 8-bit indicator of the active row of clause c under masked assignment v.

@[simp]

theorem Cslib.Crypto.GMW.length_clauseTableRow (φ : Logic.PL.CNF ℕ) (m : List Bool) (c : Logic.PL.Clause ℕ) : (clauseTableRow φ m c).length = 8

@[simp]

theorem Cslib.Crypto.GMW.length_clauseActiveRow (φ : Logic.PL.CNF ℕ) (v : List Bool) (c : Logic.PL.Clause ℕ) : (clauseActiveRow φ v c).length = 8

@[simp]

theorem Cslib.Crypto.GMW.clauseTableRow_listRow (φ : Logic.PL.CNF ℕ) (m : List Bool) (c : Logic.PL.Clause ℕ) : clauseTableRow φ (BitString.listRow φ.vars.length 0 m) c = clauseTableRow φ m c

@[simp]

theorem Cslib.Crypto.GMW.clauseActiveRow_listRow (φ : Logic.PL.CNF ℕ) (v : List Bool) (c : Logic.PL.Clause ℕ) : clauseActiveRow φ (BitString.listRow φ.vars.length 0 v) c = clauseActiveRow φ v c

theorem Cslib.Crypto.GMW.getD_clauseTableRow (φ : Logic.PL.CNF ℕ) (m : List Bool) (c : Logic.PL.Clause ℕ) {t : ℕ} (ht : t < 8) : (clauseTableRow φ m c).getD t false = clauseEvalBits c (gmwBit0Of8 t ^^ varBit φ m (List.getD c 0 (0, false)).1) (gmwBit1Of8 t ^^ varBit φ m (List.getD c 1 (0, false)).1) (gmwBit2Of8 t ^^ varBit φ m (List.getD c 2 (0, false)).1)

theorem Cslib.Crypto.GMW.getD_clauseActiveRow (φ : Logic.PL.CNF ℕ) (v : List Bool) (c : Logic.PL.Clause ℕ) {t : ℕ} (ht : t < 8) : (clauseActiveRow φ v c).getD t false = decide (t = gmwActiveIdx (varBit φ v (List.getD c 0 (0, false)).1) (varBit φ v (List.getD c 1 (0, false)).1) (varBit φ v (List.getD c 2 (0, false)).1))

def Cslib.Crypto.GMW.tableBits (φ : Logic.PL.CNF ℕ) (m : List Bool) : List Bool

The 8 * φ.length-bit concatenation of all clause truth tables of φ under mask m.

def Cslib.Crypto.GMW.activeTableFlags (φ : Logic.PL.CNF ℕ) (v : List Bool) : List Bool

The 8 * φ.length-bit concatenation of all active-row indicators of φ under v.

@[simp]

theorem Cslib.Crypto.GMW.length_tableBits (φ : Logic.PL.CNF ℕ) (m : List Bool) : (tableBits φ m).length = 8 * List.length φ

@[simp]

theorem Cslib.Crypto.GMW.length_activeTableFlags (φ : Logic.PL.CNF ℕ) (v : List Bool) : (activeTableFlags φ v).length = 8 * List.length φ

@[simp]

theorem Cslib.Crypto.GMW.tableBits_listRow (φ : Logic.PL.CNF ℕ) (m : List Bool) : tableBits φ (BitString.listRow φ.vars.length 0 m) = tableBits φ m

@[simp]

theorem Cslib.Crypto.GMW.activeTableFlags_listRow (φ : Logic.PL.CNF ℕ) (v : List Bool) : activeTableFlags φ (BitString.listRow φ.vars.length 0 v) = activeTableFlags φ v

Single-copy and three-copy bit layouts

def Cslib.Crypto.GMW.copyLen (φ : Logic.PL.CNF ℕ) : ℕ

Number of committed bits in one copy of the masked 3SAT gadget: φ.vars.length mask bits, φ.vars.length masked assignment bits, and 8 * φ.length table bits.

def Cslib.Crypto.GMW.totalLen (φ : Logic.PL.CNF ℕ) : ℕ

Number of committed bits across all three parallel copies.

def Cslib.Crypto.GMW.mPart (φ : Logic.PL.CNF ℕ) (copy : List Bool) : List Bool

Extract the m segment (first φ.vars.length bits) of a copy.

def Cslib.Crypto.GMW.vPart (φ : Logic.PL.CNF ℕ) (copy : List Bool) : List Bool

Extract the v segment (second φ.vars.length bits) of a copy.

def Cslib.Crypto.GMW.tablePart (φ : Logic.PL.CNF ℕ) (copy : List Bool) : List Bool

Extract the truth-table segment (8 * φ.length bits) of a copy.

def Cslib.Crypto.GMW.realCopyBits (φ : Logic.PL.CNF ℕ) (w m : List Bool) : List Bool

Honest committed bits for one copy given witness w and mask m.

def Cslib.Crypto.GMW.simCopyBits (φ : Logic.PL.CNF ℕ) (b : Bool) (rand : List Bool) : List Bool

Simulated (and selectively opened) bits for one copy given challenge bit b and random word rand of length φ.vars.length.

def Cslib.Crypto.GMW.copyOpenFlags (φ : Logic.PL.CNF ℕ) (b : Bool) (copy : List Bool) : List Bool

Selective-opening flags for one copy under challenge bit b.

@[simp]

theorem Cslib.Crypto.GMW.length_realCopyBits (φ : Logic.PL.CNF ℕ) (w m : List Bool) : (realCopyBits φ w m).length = copyLen φ

@[simp]

theorem Cslib.Crypto.GMW.length_simCopyBits (φ : Logic.PL.CNF ℕ) (b : Bool) (rand : List Bool) : (simCopyBits φ b rand).length = copyLen φ

@[simp]

theorem Cslib.Crypto.GMW.length_copyOpenFlags (φ : Logic.PL.CNF ℕ) (b : Bool) (copy : List Bool) : (copyOpenFlags φ b copy).length = copyLen φ

@[simp]

theorem Cslib.Crypto.GMW.vPart_realCopyBits (φ : Logic.PL.CNF ℕ) (w m : List Bool) : vPart φ (realCopyBits φ w m) = BitString.listXor φ.vars.length [w, m]

@[simp]

theorem Cslib.Crypto.GMW.mPart_simCopyBits_false (φ : Logic.PL.CNF ℕ) (rand : List Bool) : mPart φ (simCopyBits φ false rand) = BitString.listRow φ.vars.length 0 rand

@[simp]

theorem Cslib.Crypto.GMW.vPart_simCopyBits_true (φ : Logic.PL.CNF ℕ) (rand : List Bool) : vPart φ (simCopyBits φ true rand) = BitString.listRow φ.vars.length 0 rand

@[simp]

theorem Cslib.Crypto.GMW.tablePart_simCopyBits_false (φ : Logic.PL.CNF ℕ) (rand : List Bool) : tablePart φ (simCopyBits φ false rand) = tableBits φ rand

@[simp]

theorem Cslib.Crypto.GMW.tablePart_simCopyBits_true (φ : Logic.PL.CNF ℕ) (rand : List Bool) : tablePart φ (simCopyBits φ true rand) = activeTableFlags φ rand

@[simp]

theorem Cslib.Crypto.GMW.naorMaskBits_simCopyBits (φ : Logic.PL.CNF ℕ) (b : Bool) (rand : List Bool) : naorMaskBits (copyOpenFlags φ b (simCopyBits φ b rand)) (simCopyBits φ b rand) = simCopyBits φ b rand

def Cslib.Crypto.GMW.verifyCopyBits (φ : Logic.PL.CNF ℕ) (b : Bool) (copy : List Bool) : Bool

Check the opened bits of one copy against challenge bit b.

@[simp]

theorem Cslib.Crypto.GMW.verifyCopyBits_simCopyBits (φ : Logic.PL.CNF ℕ) (b : Bool) (rand : List Bool) : verifyCopyBits φ b (simCopyBits φ b rand) = true

Three-copy protocol messages and verification

def Cslib.Crypto.GMW.gmwCopy0 (φ : Logic.PL.CNF ℕ) (bits : List Bool) : List Bool

Extract copy 0 (copyLen φ bits) from a 3-copy GMW bit vector.

def Cslib.Crypto.GMW.gmwCopy1 (φ : Logic.PL.CNF ℕ) (bits : List Bool) : List Bool

Extract copy 1 (copyLen φ bits) from a 3-copy GMW bit vector.

def Cslib.Crypto.GMW.gmwCopy2 (φ : Logic.PL.CNF ℕ) (bits : List Bool) : List Bool

Extract copy 2 (copyLen φ bits) from a 3-copy GMW bit vector.

def Cslib.Crypto.GMW.realBits (φ : Logic.PL.CNF ℕ) (w m₀ m₁ m₂ : List Bool) : List Bool

Honest committed bits across all three copies.

def Cslib.Crypto.GMW.simBits (φ : Logic.PL.CNF ℕ) (ch r₀ r₁ r₂ : List Bool) : List Bool

Simulated (and selectively opened) bits across all three copies.

def Cslib.Crypto.GMW.allOpenFlags (φ : Logic.PL.CNF ℕ) (ch bits : List Bool) : List Bool

Selective-opening flags across all three copies under challenge word ch.

@[simp]

theorem Cslib.Crypto.GMW.length_realBits (φ : Logic.PL.CNF ℕ) (w m₀ m₁ m₂ : List Bool) : (realBits φ w m₀ m₁ m₂).length = totalLen φ

@[simp]

theorem Cslib.Crypto.GMW.length_simBits (φ : Logic.PL.CNF ℕ) (ch r₀ r₁ r₂ : List Bool) : (simBits φ ch r₀ r₁ r₂).length = totalLen φ

@[simp]

theorem Cslib.Crypto.GMW.length_allOpenFlags (φ : Logic.PL.CNF ℕ) (ch bits : List Bool) : (allOpenFlags φ ch bits).length = totalLen φ

@[simp]

theorem Cslib.Crypto.GMW.gmwCopy0_realBits (φ : Logic.PL.CNF ℕ) (w m₀ m₁ m₂ : List Bool) : gmwCopy0 φ (realBits φ w m₀ m₁ m₂) = realCopyBits φ w m₀

@[simp]

theorem Cslib.Crypto.GMW.gmwCopy1_realBits (φ : Logic.PL.CNF ℕ) (w m₀ m₁ m₂ : List Bool) : gmwCopy1 φ (realBits φ w m₀ m₁ m₂) = realCopyBits φ w m₁

@[simp]

theorem Cslib.Crypto.GMW.gmwCopy2_realBits (φ : Logic.PL.CNF ℕ) (w m₀ m₁ m₂ : List Bool) : gmwCopy2 φ (realBits φ w m₀ m₁ m₂) = realCopyBits φ w m₂

@[simp]

theorem Cslib.Crypto.GMW.gmwCopy0_simBits (φ : Logic.PL.CNF ℕ) (ch r₀ r₁ r₂ : List Bool) : gmwCopy0 φ (simBits φ ch r₀ r₁ r₂) = simCopyBits φ (ch.getD 0 false) r₀

@[simp]

theorem Cslib.Crypto.GMW.gmwCopy1_simBits (φ : Logic.PL.CNF ℕ) (ch r₀ r₁ r₂ : List Bool) : gmwCopy1 φ (simBits φ ch r₀ r₁ r₂) = simCopyBits φ (ch.getD 1 false) r₁

@[simp]

theorem Cslib.Crypto.GMW.gmwCopy2_simBits (φ : Logic.PL.CNF ℕ) (ch r₀ r₁ r₂ : List Bool) : gmwCopy2 φ (simBits φ ch r₀ r₁ r₂) = simCopyBits φ (ch.getD 2 false) r₂

theorem Cslib.Crypto.GMW.naorMaskBits_realBits {φ : Logic.PL.CNF ℕ} {w m₀ m₁ m₂ : List Bool} (ch : List Bool) (hw : Complexity.ThreeSAT.verifier (φ, w) = true) : naorMaskBits (allOpenFlags φ ch (realBits φ w m₀ m₁ m₂)) (realBits φ w m₀ m₁ m₂) = simBits φ ch (if ch.getD 0 false = true then BitString.listXor φ.vars.length [w, m₀] else m₀) (if ch.getD 1 false = true then BitString.listXor φ.vars.length [w, m₁] else m₁) (if ch.getD 2 false = true then BitString.listXor φ.vars.length [w, m₂] else m₂)

theorem Cslib.Crypto.GMW.allOpenFlags_realBits (φ : Logic.PL.CNF ℕ) (ch w m₀ m₁ m₂ : List Bool) : allOpenFlags φ ch (realBits φ w m₀ m₁ m₂) = allOpenFlags φ ch (simBits φ ch (if ch.getD 0 false = true then BitString.listXor φ.vars.length [w, m₀] else m₀) (if ch.getD 1 false = true then BitString.listXor φ.vars.length [w, m₁] else m₁) (if ch.getD 2 false = true then BitString.listXor φ.vars.length [w, m₂] else m₂))

@[simp]

theorem Cslib.Crypto.GMW.naorMaskBits_simBits (φ : Logic.PL.CNF ℕ) (ch r₀ r₁ r₂ : List Bool) : naorMaskBits (allOpenFlags φ ch (simBits φ ch r₀ r₁ r₂)) (simBits φ ch r₀ r₁ r₂) = simBits φ ch r₀ r₁ r₂

def Cslib.Crypto.GMW.proverReply1 (generator : List Bool → List Bool) (m : ℕ) (r openFlags bits : List Bool) (seeds pads : List (List Bool)) : List Bool

Prover's first-round message: flat list of totalLen φ Naor commitments.

def Cslib.Crypto.GMW.proverReply2 (s : ℕ) (φ : Logic.PL.CNF ℕ) (ch bits : List Bool) (seeds : List (List Bool)) : List Bool

Prover's second-round message: masked bits followed by flat selected seeds.

def Cslib.Crypto.GMW.verifyCommitments (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (r flags commitReply openedBits openSeedsFlat : List Bool) : Bool

Check that every active position i < totalLen φ opens to the committed word in commitReply.

def Cslib.Crypto.GMW.verifyTranscript (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (r commitReply ch openReply : List Bool) : Bool

Verifier's complete check on the two-round interaction transcript.

theorem Cslib.Crypto.GMW.length_proverReply2_any (s : ℕ) (φ : Logic.PL.CNF ℕ) (ch bits : List Bool) (seeds : List (List Bool)) : (proverReply2 s φ ch bits seeds).length = bits.length * (s + 1)

Two-round deterministic state handler, honest prover, and honest verifier

def Cslib.Crypto.GMW.twoRoundStep (reply1 reply2 : List Bool → List Bool) (q : List Bool) (s : ℕ × List Bool) : List Bool × ℕ × List Bool

Deterministic two-round state transition answering the first query with reply1 q, the second query with reply2 (BitString.listRow 3 0 q) while recording the 3-bit challenge in the state, and subsequent queries with [].

def Cslib.Crypto.GMW.runTwoRound {α : Type} (reply1 reply2 : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (s : ℕ × List Bool) : ProbComp (α × ℕ × List Bool)

Run a WordOracleComp Unit program against twoRoundStep inside ProbComp.

@[simp]

theorem Cslib.Crypto.GMW.runTwoRound_pure {α : Type} (reply1 reply2 : List Bool → List Bool) (a : α) (s : ℕ × List Bool) : runTwoRound reply1 reply2 (pure a) s = pure (a, s)

theorem Cslib.Crypto.GMW.runTwoRound_bind {α β : Type} (reply1 reply2 : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (next : α → Probability.WordOracleComp Unit β) (s : ℕ × List Bool) : runTwoRound reply1 reply2 (prog >>= next) s = do let x ← runTwoRound reply1 reply2 prog s runTwoRound reply1 reply2 (next x.1) x.2

theorem Cslib.Crypto.GMW.runTwoRound_map {α β : Type} (reply1 reply2 : List Bool → List Bool) (f : α → β) (prog : Probability.WordOracleComp Unit α) (s : ℕ × List Bool) : runTwoRound reply1 reply2 (f <$> prog) s = Prod.map f id <$> runTwoRound reply1 reply2 prog s

@[simp]

theorem Cslib.Crypto.GMW.runTwoRound_sample {α : Type} (reply1 reply2 : List Bool → List Bool) (prog : ProbComp α) (s : ℕ × List Bool) : runTwoRound reply1 reply2 (ProbOracleComp.sample prog) s = (fun (x : α) => (x, s)) <$> prog

@[simp]

theorem Cslib.Crypto.GMW.runTwoRound_query (reply1 reply2 : List Bool → List Bool) (q : Unit × List Bool) (s : ℕ × List Bool) : runTwoRound reply1 reply2 (ProbOracleComp.query q) s = pure (twoRoundStep reply1 reply2 q.2 s)

theorem Cslib.Crypto.GMW.eval_runTwoRound {α : Type} (reply1 reply2 : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (s : ℕ × List Bool) : (runTwoRound reply1 reply2 prog s).eval = ProbOracleComp.runWith (fun (q : Unit × List Bool) (state : ℕ × List Bool) => PMF.pure (twoRoundStep reply1 reply2 q.2 state)) prog s

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

Sample the honest prover's random masks and commitment seeds, returning (bits, seeds).

def Cslib.Crypto.GMW.honestReply1 (generator : List Bool → List Bool) (m : ℕ) (φ : Logic.PL.CNF ℕ) (coins : List Bool × List (List Bool)) (r : List Bool) : List Bool

Honest first-round reply function for pre-sampled (bits, seeds).

def Cslib.Crypto.GMW.honestReply2 (s : ℕ) (φ : Logic.PL.CNF ℕ) (coins : List Bool × List (List Bool)) (ch : List Bool) : List Bool

Honest second-round reply function for pre-sampled (bits, seeds).

noncomputable def Cslib.Crypto.GMW.gmwProver (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (w : List Bool) : Complexity.Prover Unit

The honest GMW prover for a 3SAT formula φ and witness w. It samples its masks and commitment seeds on the first query and answers the two rounds via honestReply1 and honestReply2.

theorem Cslib.Crypto.GMW.run_gmwProver_fst {α : Type} (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (w : List Bool) (prog : Probability.WordOracleComp Unit α) : PMF.map Prod.fst ((gmwProver generator s m φ w).run prog (gmwProver generator s m φ w).init) = (do let coins ← sampleHonestCoins s φ w Prod.fst <$> runTwoRound (honestReply1 generator m φ coins) (honestReply2 s φ coins) prog (0, [false, false, false])).eval

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

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

theorem Cslib.Crypto.GMW.eval_gmwInteract (generator : List Bool → List Bool) (s m : ℕ) (φ : Logic.PL.CNF ℕ) (w : List Bool) (prog : Probability.WordOracleComp Unit (List Bool)) : (gmwInteract generator s m φ w prog).eval = PMF.map Prod.fst ((gmwProver generator s m φ w).run prog (gmwProver generator s m φ w).init)

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

The two-round GMW verifier for a problem reduced to ThreeSAT by f, at security parameter n (using Naor commitments with seed length n + 7).