Polynomial-Time Completeness of $\text{OT}_1^4$ for Semi-Honest Multi-Party Computation

This module formalizes a proper-coalition variant of Goldreich's semi-honest multi-party completeness theorem for 1-out-of-4 bit oblivious transfer $\text{OT}_1^4$ (Section 7.5.2.4, Theorem 7.5.12, print p. 707; generalizing Section 7.3.4, Theorem 7.3.11, print p. 648), with uniform efficiency certificates for the joint word-level runner and coalition simulators. Given any polynomial-time computable family of $m$-party randomized functionalities specified by a word-level evaluator F : α × List Bool → List Bool with polynomial-time unary input width n : α → ℕ, output width k : α → ℕ, and shared-coin width coins : α → ℕ:

1. Uniform Circuit Compilation: Cslib.Complexity.CircuitValue.exists_uniformCircuitFamily compiles F into a polynomial-time constructible family of Boolean circuits C : (a : α) → Circuit Boolean.signature (m * n a + coins a) (m * k a) whose evaluation agrees with wordRandomizedFunctionality m coins n k F a.
2. Word-Level Protocol Execution & Bridge Lemma: Protocol.runEncoded executes any ot14Spec-hybrid protocol in Cslib.Probability.WordOracleComp Unit (List Bool) by translating each typed ot14Spec query to a 6-bit word query and reading the 1-bit reply prefix. Protocol.eval_runEncoded_eq_evalWith_map proves that running Π.runEncoded against ot14WordHandler yields the exact distribution of (Π.evalWith ot14World x).map (encodeViewsAndOutputs encView encOut).
3. Uniform Efficiency Certificates: Over Sigma-packaged family inputs FamilyRunInput and FamilySimInput, isOraclePPTOn_gmwOT14RandomizedProtocol certifies that the centralized joint word-encoded execution Protocol.runEncoded of gmwOT14RandomizedProtocol across all m parties is Cslib.Probability.IsOraclePPTOn (note that this certifies the joint word-level runner rather than separate per-party local PPT strategies), and isPPTOn_gmwOT14RandomizedSim certifies that for every static coalition I : Finset (Fin m), the encoded view simulator gmwOT14RandomizedSim is Cslib.Probability.IsPPTOn. Because gmwCircuitProtocol (Construction 7.5.10, p. 706) includes one sharedMulSpec m share-refresh call per output coordinate (r, j) : Fin m × Fin k a in Step 3 in addition to one call per .and/.or gate in Step 2, composing with multiPartyMulProtocol m (Construction 7.5.8, p. 704) and twoPartyMulProtocol (Construction 7.3.7, pp. 643–644) expands each sharedMulSpec m call into $m(m-1)/2$ pairwise ot14Spec calls (adding $m \cdot k(a) \cdot m(m-1)/2$ calls in Step 3, polynomial in $m, n(a), k(a), (C\,a).\text{size}$).
4. End-to-End Completeness (exists_perfectSemiHonestPrivate_ot14_of_polyTime): Formalizes a proper-coalition variant of Goldreich's Theorem 7.5.12, combining uniform circuit compilation, proper-coalition perfect semi-honest privacy in ot14World (PerfectSemiHonestPrivateProper), and uniform IsOraclePPTOn / IsPPTOn efficiency. The proper-coalition quantifier I ≠ Finset.univ is narrower than Goldreich's Definition 7.5.1 and Theorem 7.5.12 (which quantify over all I ⊆ [m], p. 696; Goldreich's text on pp. 697 and 703 treats I = [m] as trivial without restricting that remark to deterministic functionalities or to the view-only Eq. 7.39). Under the joint view-and-output equation Eq. 7.40 for randomized functionalities, I = Finset.univ is not vacuous: the canonical independent-coin-share simulator randomizedWrapperSim is refuted at I = Finset.univ by not_perfectSemiHonestPrivate_coinEchoRandomizedWrapper_univ in ComplexityTests/Crypto/MPC.lean, and any full-coalition simulator receiving only (x, y) would have to sample coin shares whose XOR r satisfies g(r, x) = y.

Main definitions

• Cslib.Crypto.Protocols.MPC.encodeCoinsAndInputs, Cslib.Crypto.Protocols.MPC.wordRandomizedFunctionality: word-encoded m-party randomized functionality family induced by F : α × List Bool → List Bool.
• Cslib.Crypto.Protocols.MPC.encodeOT14Query, Cslib.Crypto.Protocols.MPC.ot14WordHandler, Cslib.Crypto.Protocols.MPC.decodeOT14Reply: 6-bit query encoding and stateful word-oracle handler for ot14World (Section 7.3.2, Eq. 7.20, p. 640).
• Cslib.Crypto.Protocols.MPC.Steps.runEncoded, Cslib.Crypto.Protocols.MPC.Protocol.runEncoded, Cslib.Crypto.Protocols.MPC.encodeViewsAndOutputs: generic word-level protocol runner in WordOracleComp Unit (List Bool).
• Cslib.Crypto.Protocols.MPC.FamilyRunInput, Cslib.Crypto.Protocols.MPC.FamilySimInput, Cslib.Crypto.Protocols.MPC.encFamilyRunInput, Cslib.Crypto.Protocols.MPC.encFamilySimInput: Sigma-packaged family input records and injective bit-list encodings.
• Cslib.Crypto.Protocols.MPC.encGMWPartyView, Cslib.Crypto.Protocols.MPC.encodeCoalitionView: word-level view encoders for gmwOT14RandomizedProtocol and gmwOT14RandomizedSim.

Main results

• Cslib.Crypto.Protocols.MPC.Steps.runWith_runEncoded_eq_evalWith, Cslib.Crypto.Protocols.MPC.Protocol.eval_runEncoded_eq_evalWith_map: bridge lemmas relating Steps.runEncoded / Protocol.runEncoded under ot14WordHandler to evalWith ot14World.
• Cslib.Crypto.Protocols.MPC.isOraclePPTOn_gmwOT14RandomizedProtocol: uniform IsOraclePPTOn certificate for the joint word-level runner Protocol.runEncoded applied to gmwOT14RandomizedProtocol.
• Cslib.Crypto.Protocols.MPC.isPPTOn_gmwOT14RandomizedSim: uniform IsPPTOn certificate for gmwOT14RandomizedSim.
• Cslib.Crypto.Protocols.MPC.exists_perfectSemiHonestPrivate_ot14_of_polyTime: proper-coalition variant of Theorem 7.5.12 (Section 7.5.2.4, print p. 707; generalizing Theorem 7.3.11, Section 7.3.4, print p. 648), establishing polynomial-time completeness of $\text{OT}_1^4$ for $m$-party semi-honest computation against every proper coalition I ≠ Finset.univ.

References

• O. Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Section 7.3.2 (Eq. 7.20, p. 640), Section 7.3.3 (Construction 7.3.7, pp. 643–644), Section 7.3.4 (Theorem 7.3.11, p. 648), Section 7.5.1.2 (Definition 7.5.1, Eqs. 7.39–7.40, p. 696; p. 697), Section 7.5.2.1 (p. 703), Section 7.5.2.2 (Construction 7.5.8, p. 704), Section 7.5.2.3 (Construction 7.5.10, p. 706), and Section 7.5.2.4 (Theorem 7.5.12, p. 707).

Part 1: Word-Level Functionality, ot14Spec Word Handler, and Protocol.runEncoded

def Cslib.Crypto.Protocols.MPC.encodeCoinsAndInputs (m coins n : ℕ) (r : BitString coins) (x : Fin m → BitString n) : List Bool

Encode x : Fin m → BitString n and shared coin tape r : BitString coins as the m * n + coins-bit list List.ofFn (Fin.append (BitString.blocksEquiv.symm x) r).

noncomputable def Cslib.Crypto.Protocols.MPC.wordRandomizedFunctionality {α : Type} (m : ℕ) (coins n k : α → ℕ) (F : α × List Bool → List Bool) (a : α) : Functionality m (fun (x : Fin m) => BitString (n a)) fun (x : Fin m) => BitString (k a)

Randomized m-party functionality family induced by a word-level function F : α × List Bool → List Bool with coins a random bits, n a-bit party inputs, and k a-bit party outputs.

def Cslib.Crypto.Protocols.MPC.encodeOT14Query (q : (s : Fin 2) → ot14Spec.Query () s) : List Bool

Serialize a typed ot14Spec query q : (s : Fin 2) → ot14Spec.Query () s as a 6-bit word: the sender's four table bits q 0 0, q 0 1, q 0 2, q 0 3 followed by the receiver's two selector bits (fin4ToBoolPair (q 1)).1, (fin4ToBoolPair (q 1)).2.

noncomputable def Cslib.Crypto.Protocols.MPC.ot14WordHandler : Unit × List Bool → StateT Unit PMF (List Bool)

Stateful word-oracle handler realizing ot14World on 6-bit requests produced by encodeOT14Query: returns the selected sender bit [req.getD idx false] while leaving the Unit state unchanged.

def Cslib.Crypto.Protocols.MPC.decodeOT14Reply (rep : List Bool) (s : Fin 2) : ot14Spec.Answer () s

Decode a 1-bit word-oracle reply rep : List Bool into an ot14Spec answer tuple: returns () to slot 0 and rep.headD false to slot 1.

def Cslib.Crypto.Protocols.MPC.Steps.runEncoded {m : ℕ} {State Out : Fin m → Type} {sc : Schedule m ot14Spec} (steps : Steps State Out sc) (st : (i : Fin m) → State i) : Probability.WordOracleComp Unit ((i : Fin m) → sc.Received i)

Execute steps : Steps State Out sc over ot14Spec in WordOracleComp Unit, translating each .oracle round into a 1-bit ProbOracleComp.query call with payload encodeOT14Query.

def Cslib.Crypto.Protocols.MPC.encodeViewsAndOutputs {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (encView : (i : Fin m) → PartyView In Coins sc i → List Bool) (encOut : (i : Fin m) → Out i → List Bool) (vo : ((i : Fin m) → PartyView In Coins sc i) × ((i : Fin m) → Out i)) : List Bool

Encode a complete (views, outputs) execution outcome into a single bit string List Bool by pairing the framed list of all m encoded party views with the framed list of all m encoded party outputs.

def Cslib.Crypto.Protocols.MPC.Protocol.runEncoded {m : ℕ} {sc : Schedule m ot14Spec} {In Coins Out : Fin m → Type} (encView : (i : Fin m) → PartyView In Coins sc i → List Bool) (encOut : (i : Fin m) → Out i → List Bool) (proto : Protocol m ot14Spec sc In Coins Out) (x : (i : Fin m) → In i) : Probability.WordOracleComp Unit (List Bool)

Generic word-level execution of proto.run x in WordOracleComp Unit (List Bool), translating each ot14Spec query to a word-oracle call and encoding the resulting (views, outputs) pair via (encView, encOut).

theorem Cslib.Crypto.Protocols.MPC.Steps.runWith_runEncoded_eq_evalWith {m : ℕ} {State Out : Fin m → Type} {sc : Schedule m ot14Spec} (steps : Steps State Out sc) (st : (i : Fin m) → State i) : ProbOracleComp.runWith ot14WordHandler (steps.runEncoded st) () = PMF.map (fun (x : (i : Fin m) → sc.Received i) => (x, ())) (steps.evalWith ot14World st)

Step-level bridge lemma: interpreting steps.runEncoded st against ot14WordHandler produces the exact distribution of steps.evalWith ot14World st paired with ().

theorem Cslib.Crypto.Protocols.MPC.Protocol.eval_runEncoded_eq_evalWith_map {m : ℕ} {sc : Schedule m ot14Spec} {In Coins Out : Fin m → Type} (encView : (i : Fin m) → PartyView In Coins sc i → List Bool) (encOut : (i : Fin m) → Out i → List Bool) (proto : Protocol m ot14Spec sc In Coins Out) (x : (i : Fin m) → In i) : PMF.map Prod.fst (ProbOracleComp.runWith ot14WordHandler (runEncoded encView encOut proto x) ()) = PMF.map (encodeViewsAndOutputs encView encOut) (proto.evalWith ot14World x)

Bridge lemma: interpreting proto.runEncoded against the word-encoded ot14World handler produces the exact law of proto.evalWith ot14World x mapped through encodeViewsAndOutputs.

Part 2: Sigma-Packaged Family Input Encodings and encGMWPartyView

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.FamilyRunInput (α : Type) (m : ℕ) (n : α → ℕ) : Type

Sigma-packaged input record for executing a protocol family at instance a : α.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.FamilySimInput (α : Type) (m : ℕ) (n k : α → ℕ) (I : Finset (Fin m)) : Type

Sigma-packaged input record for running the coalition simulator at instance a : α.

def Cslib.Crypto.Protocols.MPC.encFamilyRunInput {α : Type} (enc : α ↪ List Bool) (m : ℕ) (n : α → ℕ) : FamilyRunInput α m n ↪ List Bool

Injective bit-list encoding of FamilyRunInput α m n: pairs enc a with the packed m * n a party input bits List.ofFn (BitString.blocksEquiv.symm x).

def Cslib.Crypto.Protocols.MPC.encFamilySimInput {α : Type} (enc : α ↪ List Bool) (m : ℕ) (n k : α → ℕ) (I : Finset (Fin m)) : FamilySimInput α m n k I ↪ List Bool

Injective bit-list encoding of FamilySimInput α m n k I: pairs enc a with the zero-extended packed coalition input bits extendCoalitionBits I xI and output bits extendCoalitionBits I yI.

def Cslib.Crypto.Protocols.MPC.encGMWPartyView (m coins n k : ℕ) (C : Circuits.Circuit Circuits.Boolean.signature (m * n + coins) (m * k)) (i : Fin m) (v : PartyView (fun (x : Fin m) => BitString n) (fun (j : Fin m) => BitString coins × Schedule.ComposedCoins (fun (x : Unit) (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) (Schedule.ComposedCoins (fun (x : Unit) (x_1 : Fin ((sharedMulSpec m).arity x)) => Unit) (fun (x : Fin m) => Fin (n + coins) → Fin (m - 1) → Bool) (gmwCircuitSchedule m (n + coins) k (C.comp (xorPreludeCircuit m n coins)))) (Schedule.compose (fun (x : (sharedMulSpec m).Op) => multiPartyMulSchedule m) (gmwCircuitSchedule m (n + coins) k (C.comp (xorPreludeCircuit m n coins)))) j) (Schedule.compose (fun (x : (sharedMulSpec 2).Op) => twoPartyMulSchedule) (Schedule.compose (fun (x : (sharedMulSpec m).Op) => multiPartyMulSchedule m) (gmwCircuitSchedule m (n + coins) k (C.comp (xorPreludeCircuit m n coins))))) i) : List Bool

Serialize party i's complete PartyView in gmwOT14RandomizedProtocol m coins n k C to a List Bool encoding:

• v.input : BitString n
• v.coins.1 : BitString coins (randomized-wrapper coin share)
• v.coins.2.1.1 : Fin (n + coins) → Fin (m - 1) → Bool (Step 1 input-sharing coins)
• encOTSubCoins _ i v.coins.2.2 (Step 2 & Step 3 $\text{OT}_1^4$ sender coins)
• Step 1 received input shares (encPairsMsgReceived)
• Step 2 & Step 3 received $\text{OT}_1^4$ receiver answers (encOTOracleAnswers)
• Step 3 received output-reconstruction shares (encOutCoordsMsgReceived).

def Cslib.Crypto.Protocols.MPC.encodeCoalitionView {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins : Fin m → Type} (encView : (i : Fin m) → PartyView In Coins sc i → List Bool) (I : Finset (Fin m)) (vI : (i : ↥I) → PartyView In Coins sc ↑i) : List Bool

Encode a coalition view tuple vI : (i : I) → PartyView In Coins sc i.1 into List Bool by listing encView i (vI ⟨i, hi⟩) for i ∈ I and [] for i ∉ I.

Part 3: Uniform Polynomial-Time Compilation of xorPreludeCircuit

Part 4: Bounded-Growth Monadic List Folds and Word-Level Efficiency

Section 4B: Word-Level Real and Simulated Runners and Their PPT Certificates

Section 4C: Equivalence of Word-Level Runners with Protocol.runEncoded and

gmwOT14RandomizedSim

Sub-part 4C.2: One sharedMulSpec m Round & Step 1 Input Sharing

Sub-part 4C.2: Step 1 (inputShareSteps) Equivalence

Sub-part 4C.3: Step 2 (progSteps) Equivalence

Sub-part 4C.4: Step 3 (outputSteps) Equivalence

Sub-part 4C.5: End-to-End Runner & Simulator Equivalence

Part 5: Uniform Polynomial-Time Certificates and End-to-End Theorem 7.5.12

theorem Cslib.Crypto.Protocols.MPC.isOraclePPTOn_gmwOT14RandomizedProtocol {α : Type} {enc : α ↪ List Bool} (m : ℕ) [NeZero m] {coins n k : α → ℕ} {C : (a : α) → Circuits.Circuit Circuits.Boolean.signature (m * n a + coins a) (m * k a)} (hcoins : Turing.MultiTapeTM.ComputableInPolyTime coins enc Turing.MultiTapeTM.encUnary) (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hC : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => (C a).code) enc Circuits.Boolean.encCode) : Probability.IsOraclePPTOn (encFamilyRunInput enc m n) Turing.MultiTapeTM.encBits fun (inp : FamilyRunInput α m n) => Protocol.runEncoded (encGMWPartyView m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst)) (fun (x : Fin m) (y : Fin (k inp.fst) → Bool) => List.ofFn y) (gmwOT14RandomizedProtocol m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst)) inp.snd

Uniform oracle-PPT certificate for the centralized joint word-level runner Protocol.runEncoded applied to the m-party $\text{OT}_1^4$-hybrid GMW protocol family gmwOT14RandomizedProtocol (certifying the joint word-level execution across all m parties over encFamilyRunInput enc m n rather than separate per-party local PPT strategies).

theorem Cslib.Crypto.Protocols.MPC.isPPTOn_gmwOT14RandomizedSim {α : Type} {enc : α ↪ List Bool} (m : ℕ) [NeZero m] {coins n k : α → ℕ} {C : (a : α) → Circuits.Circuit Circuits.Boolean.signature (m * n a + coins a) (m * k a)} (hcoins : Turing.MultiTapeTM.ComputableInPolyTime coins enc Turing.MultiTapeTM.encUnary) (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hC : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => (C a).code) enc Circuits.Boolean.encCode) (I : Finset (Fin m)) : Probability.IsPPTOn (encFamilySimInput enc m n k I) Turing.MultiTapeTM.encBits fun (inp : FamilySimInput α m n k I) => encodeCoalitionView (encGMWPartyView m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst)) I <$> gmwOT14RandomizedSim m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst) I inp.snd.1 inp.snd.2

Uniform PPT certificate for the m-party $\text{OT}_1^4$-hybrid GMW coalition simulator family gmwOT14RandomizedSim for any static coalition I : Finset (Fin m).

theorem Cslib.Crypto.Protocols.MPC.exists_perfectSemiHonestPrivate_ot14_of_polyTime {α : Type} {enc : α ↪ List Bool} (m : ℕ) [NeZero m] {coins n k : α → ℕ} {F : α × List Bool → List Bool} (hcoins : Turing.MultiTapeTM.ComputableInPolyTime coins enc Turing.MultiTapeTM.encUnary) (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hF : Turing.MultiTapeTM.ComputableInPolyTime F (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : ∃ (C : (a : α) → Circuits.Circuit Circuits.Boolean.signature (m * n a + coins a) (m * k a)), Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => (C a).code) enc Circuits.Boolean.encCode ∧ (∀ (a : α) (xr : Fin (m * n a + coins a) → Bool) (j : Fin (m * k a)), (C a).eval Circuits.Boolean.interpretation xr j = (F (a, List.ofFn xr)).getD (↑j) false) ∧ (∀ (a : α), PerfectSemiHonestPrivateProper (gmwOT14RandomizedProtocol m (coins a) (n a) (k a) (C a)) ot14World (wordRandomizedFunctionality m coins n k F a) (gmwOT14RandomizedSim m (coins a) (n a) (k a) (C a))) ∧ (Probability.IsOraclePPTOn (encFamilyRunInput enc m n) Turing.MultiTapeTM.encBits fun (inp : FamilyRunInput α m n) => Protocol.runEncoded (encGMWPartyView m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst)) (fun (x : Fin m) (y : Fin (k inp.fst) → Bool) => List.ofFn y) (gmwOT14RandomizedProtocol m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst)) inp.snd) ∧ ∀ (I : Finset (Fin m)), I ≠ Finset.univ → Probability.IsPPTOn (encFamilySimInput enc m n k I) Turing.MultiTapeTM.encBits fun (inp : FamilySimInput α m n k I) => encodeCoalitionView (encGMWPartyView m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst)) I <$> gmwOT14RandomizedSim m (coins inp.fst) (n inp.fst) (k inp.fst) (C inp.fst) I inp.snd.1 inp.snd.2

Proper-coalition variant of Theorem 7.5.12 (Goldreich Section 7.5.2.4, p. 707; generalizing Theorem 7.3.11, Section 7.3.4, p. 648): every polynomial-time m-party randomized functionality family F is privately reducible to $\text{OT}_1^4$ in the semi-honest model against every proper static coalition I ≠ Finset.univ, with uniform polynomial-time circuit family C, uniform IsOraclePPTOn joint word-level protocol execution via Protocol.runEncoded (linked to Protocol.evalWith ot14World by Protocol.eval_runEncoded_eq_evalWith_map), and uniform IsPPTOn coalition simulators.

Note that the proper-coalition quantifier I ≠ Finset.univ (PerfectSemiHonestPrivateProper) is narrower than Goldreich's Definition 7.5.1 and Theorem 7.5.12 (which quantify over all I ⊆ [m], p. 696; Goldreich's text on pp. 697 and 703 treats I = [m] as trivial without restricting that remark to deterministic functionalities or to the view-only Eq. 7.39). Under the joint view-and-output equation Eq. 7.40 for randomized functionalities, I = Finset.univ is not vacuous: the canonical independent-coin-share simulator randomizedWrapperSim is refuted at I = Finset.univ by not_perfectSemiHonestPrivate_coinEchoRandomizedWrapper_univ in ComplexityTests/Crypto/MPC.lean, and any full-coalition simulator receiving only (x, y) would have to sample coin shares whose XOR r satisfies g(r, x) = y.