Multi-Party Protocol Composition, Randomized Wrapper, and Completeness of $\text{OT}_1^4$

This module formalizes the $m$-party semi-honest composition theorem, the reduction from randomized functionalities to deterministic functionalities via shared coin-tossing, and the resulting information-theoretic reduction of any randomized $m$-party Boolean circuit functionality to $\text{OT}_1^4$ from Goldreich's Foundations of Cryptography, Volume 2: Basic Applications:

1. $k$-ary Subprotocol Composition (Round.embed, Schedule.compose, Schedule.ComposedCoins, Protocol.compose, composeSim, PerfectSemiHonestPrivate.compose): generalizes the 2-party composition theorem (Section 7.3.1, Definitions 7.3.1–7.3.2 on print p. 636 and Theorem 7.3.3 on print pp. 637–638) to $m$-party protocols making $k$-ary ideal oracle calls (Section 7.5.2.1, Definitions 7.5.5–7.5.6 on print pp. 701–702 and Theorem 7.5.7 on print pp. 702–703). Replacing each .oracle op parties round of an outer protocol P with the embedded execution of a perfectly private $k$-party subprotocol Sub op yields a perfectly private $m$-party protocol P.compose Sub in the lower-level oracle world W₂.
2. Reduction of Randomized Functionalities to Deterministic Ones (randomizedFunctionality, detOfRandomized, Protocol.randomizedWrapper, randomizedWrapperSim, perfectSemiHonestPrivate_randomizedWrapper): formalizes Equation 7.48 (Section 7.5.2.4, print p. 707) and Proposition 7.3.4 (Section 7.3.1, print pp. 639–640) combined with the composition theorem ("Application: Reducing Private Computation of General Functionalities to Deterministic Ones", Section 7.3.1, print pp. 638–639, Equation 7.19). Each party i : Fin m samples a uniform private coin share r_i : BitString coins and runs a deterministic protocol on (x_i, r_i) that evaluates g (∑ i : Fin m, r_i) x. Against every proper static coalition I ≠ Finset.univ, the sum ∑ i : Fin m, r_i is uniform and independent of the coalition's coin shares I.restrict r. perfectSemiHonestPrivate_randomizedWrapper is proved directly rather than via PerfectSemiHonestPrivate.compose because the coin-sharing reduction is only private against proper coalitions I ≠ Finset.univ, whereas PerfectSemiHonestPrivate.compose requires all-I privacy of the outer protocol. Note that restricting to I ≠ Finset.univ is narrower than Goldreich's quantifier over all $I \subseteq [m]$ in Definition 7.5.1 (print p. 696, where $I = [m]$ is called "always trivial" on print pp. 697 and 703): under the joint view-and-output equation (Eq. 7.40) for randomized functionalities, $I = [m]$ is not trivial when coin shares are simulated independently of the output (for $m = 2$, Definition 7.2.1 considers only single-party views, so Proposition 7.3.4 itself is fully covered).
3. XOR Prelude Circuit and $\text{OT}_1^4$-Hybrid GMW Protocol (xorPreludeCircuit, eval_xorPreludeCircuit, gmwOT14Protocol, gmwOT14RandomizedProtocol, perfectSemiHonestPrivateProper_gmwOT14Randomized): constructs a Boolean circuit xorPreludeCircuit m n coins (reusing Cslib.Circuits.Program.appendXor and Cslib.Circuits.Circuit.pi) that unpacks the m party input-coin blocks (x_i, r_i) into Fin.append (BitString.blocksEquiv.symm x) (∑ i : Fin m, r_i), composes gmwCircuitProtocol (M3) with multiPartyMulProtocol and twoPartyMulProtocol (M2) to obtain gmwOT14Protocol and gmwOT14RandomizedProtocol, and establishes Theorem 7.5.12 (Section 7.5.2.4, print p. 707; generalizing Theorem 7.3.11, Section 7.3.4, print p. 648) at the circuit level for all proper coalitions I ≠ Finset.univ. Throughout this module, security is stated as exact PMF distributional equality with unrestricted ProbComp simulators, whereas Goldreich's Definitions 7.2.1 and 7.5.1 use computational indistinguishability and PPT simulators (polynomial-time efficiency is certified in M5). Because gmwCircuitProtocol in M3 includes one sharedMulSpec m share-refresh call per output coordinate (r, j) : Fin m × Fin k (in addition to one sharedMulSpec m call per .and/.or gate in Step 2), composing with multiPartyMulProtocol m and twoPartyMulProtocol expands each such call into $m(m-1)/2$ pairwise invocations of ot14Spec (an extra $m \cdot k \cdot m(m-1)/2$ calls to ot14Spec from Step 3, polynomial in $m, n, k, C.\text{size}$).

Main definitions

• Cslib.Crypto.Protocols.MPC.Round.embed, Cslib.Crypto.Protocols.MPC.Schedule.compose, Cslib.Crypto.Protocols.MPC.Schedule.ComposedCoins: schedule and coin-type composition for $k$-ary oracle replacement (Definitions 7.5.5–7.5.6, pp. 701–702).
• Cslib.Crypto.Protocols.MPC.Protocol.compose, Cslib.Crypto.Protocols.MPC.composeSim: protocol and coalition-simulator composition (Theorem 7.5.7, pp. 702–703).
• Cslib.Crypto.Protocols.MPC.Protocol.mapInput, Cslib.Crypto.Protocols.MPC.mapInputSim: precomposing a protocol and coalition simulator with local party input encodings.
• Cslib.Crypto.Protocols.MPC.randomizedFunctionality, Cslib.Crypto.Protocols.MPC.detOfRandomized, Cslib.Crypto.Protocols.MPC.Protocol.randomizedWrapper, Cslib.Crypto.Protocols.MPC.randomizedWrapperSim: randomized-to-deterministic wrapper (Eq. 7.19, p. 638; Proposition 7.3.4, pp. 639–640; Eq. 7.48, p. 707).
• Cslib.Crypto.Protocols.MPC.xorPreludeCircuit: Boolean prelude circuit combining party coin shares by bitwise XOR.
• Cslib.Crypto.Protocols.MPC.gmwOT14Protocol, Cslib.Crypto.Protocols.MPC.gmwOT14Sim, Cslib.Crypto.Protocols.MPC.gmwOT14RandomizedProtocol, Cslib.Crypto.Protocols.MPC.gmwOT14RandomizedSim: $\text{OT}_1^4$-hybrid GMW protocols and coalition simulators.

Main results

• Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate.compose: Theorem 7.5.7 (print pp. 702–703; cf. Theorem 7.3.3, print pp. 637–638), multi-party composition theorem for perfect semi-honest privacy.
• Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate.mapInput: preservation of perfect semi-honest privacy under local party input encodings.
• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_randomizedWrapper: Proposition 7.3.4 (print pp. 639–640) combined with the composition theorem (Section 7.3.1 Application, print pp. 638–639, Eq. 7.19) and Section 7.5.2.4 Eq. 7.48 (print p. 707), proper-coalition privacy of the randomized-functionality wrapper.
• Cslib.Crypto.Protocols.MPC.eval_xorPreludeCircuit, Cslib.Crypto.Protocols.MPC.size_xorPreludeCircuit: correctness and gate count of xorPreludeCircuit.
• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_gmwOT14: full-coalition perfect privacy of deterministic gmwOT14Protocol in ot14World.
• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivateProper_gmwOT14Randomized: Theorem 7.5.12 (print p. 707; cf. Theorem 7.3.11, print p. 648), proper-coalition perfect privacy of gmwOT14RandomizedProtocol in ot14World.

References

• O. Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Section 7.3.1 (Definitions 7.3.1–7.3.2 on p. 636, Theorem 7.3.3 on pp. 637–638, Eq. 7.19 on p. 638, Proposition 7.3.4 on pp. 639–640), Section 7.3.4 (Theorem 7.3.11, p. 648), Section 7.5.2.1 (Definitions 7.5.5–7.5.6 on pp. 701–702, Theorem 7.5.7 on pp. 702–703), and Section 7.5.2.4 (Eq. 7.48, Theorem 7.5.12, p. 707).

Part 1: $k$-ary Subprotocol Composition (Theorem 7.5.7)

@[reducible]

def Cslib.Crypto.Protocols.MPC.Round.embed {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) : Round k spec → Round m spec

Lift a k-party round r : Round k spec to an m-party round along a party embedding parties : Fin k ↪ Fin m (Goldreich Definition 7.5.5, pp. 701–702).

@[reducible]

def Cslib.Crypto.Protocols.MPC.Schedule.compose {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} (sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂) : Schedule m spec₁ → Schedule m spec₂

Replace each .oracle op parties round in sc₁ with the lifted schedule (sc₂ op).map (Round.embed parties), taking sc₂ first and matching sc₁ after the colon (Goldreich Definitions 7.5.5–7.5.6 and Theorem 7.5.7, pp. 701–703).

@[reducible]

def Cslib.Crypto.Protocols.MPC.Schedule.SubCoins {m : ℕ} {spec₁ : MultiOracleSpec} (Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type) : Schedule m spec₁ → Fin m → Type

Per-party subprotocol coins needed along an outer schedule sc₁ : Schedule m spec₁: for each .oracle op parties round, party i holds (s : Fin (spec₁.arity op)) → (parties s = i) → Coins₂ op s (proof-domain indexed so parties outside parties hold a canonical subsingleton).

@[reducible]

def Cslib.Crypto.Protocols.MPC.Schedule.ComposedCoins {m : ℕ} {spec₁ : MultiOracleSpec} (Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type) (Coins₁ : Fin m → Type) (sc₁ : Schedule m spec₁) (i : Fin m) : Type

Combined coin type for party i : Fin m in Π.compose Sub: outer coins Coins₁ i paired with the sequence of subprotocol coins Schedule.SubCoins Coins₂ sc₁ i.

Independent product helper for single-party slot sampling

Induced sub-coalitions, tuple pushforwards, and subprotocol coin sampling

def Cslib.Crypto.Protocols.MPC.Composition.subCoalition {k m : ℕ} (parties : Fin k ↪ Fin m) (I : Finset (Fin m)) : Finset (Fin k)

Induced sub-coalition in Fin k of an outer coalition I : Finset (Fin m) along an embedding parties : Fin k ↪ Fin m (Goldreich Theorem 7.5.7 Proof Sketch, pp. 702–703). Defined via Finset.univ.filter rather than Finset.preimage so that subCoalition and expandSimSteps remain computable.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Composition.mem_subCoalition {k m : ℕ} {parties : Fin k ↪ Fin m} {I : Finset (Fin m)} {s : Fin k} : s ∈ subCoalition parties I ↔ parties s ∈ I

def Cslib.Crypto.Protocols.MPC.Composition.pushTuple {k m : ℕ} (parties : Fin k ↪ Fin m) {F : Fin k → Type} (c_k : (s : Fin k) → F s) (i : Fin m) (s : Fin k) : parties s = i → F s

Push a k-party tuple c_k : (s : Fin k) → F s forward along parties : Fin k ↪ Fin m to the proof-domain indexed m-party family fun i s _ => c_k s.

def Cslib.Crypto.Protocols.MPC.Composition.pushTupleRestrict {k m : ℕ} (parties : Fin k ↪ Fin m) (I : Finset (Fin m)) {F : Fin k → Type} (c_J : (s : ↥(subCoalition parties I)) → F ↑s) (i : ↥I) (s : Fin k) : parties s = ↑i → F s

Push a coalition-restricted J-tuple c_J : (s : subCoalition parties I) → F s.1 forward along parties : Fin k ↪ Fin m to (i : I) → (s : Fin k) → (parties s = i.1) → F s.

noncomputable def Cslib.Crypto.Protocols.MPC.Composition.sampleSlotCoins {k m : ℕ} (parties : Fin k ↪ Fin m) {Coins_k : Fin k → Type} (sample_k : (s : Fin k) → ProbComp (Coins_k s)) (i : Fin m) : ProbComp ((s : Fin k) → parties s = i → Coins_k s)

Sample party i's proof-domain indexed subcoins (s : Fin k) → (parties s = i) → Coins_k s from sample_k : (s : Fin k) → ProbComp (Coins_k s).

theorem Cslib.Crypto.Protocols.MPC.Composition.eval_pi_sampleSlotCoins {k m : ℕ} (parties : Fin k ↪ Fin m) {Coins_k : Fin k → Type} (sample_k : (s : Fin k) → ProbComp (Coins_k s)) : ProbComp.eval (OracleComp.pi (sampleSlotCoins parties sample_k)) = PMF.map (pushTuple parties) (ProbComp.eval (OracleComp.pi sample_k))

Joint distribution of sampleSlotCoins parties sample_k across all m outer parties equals the pushforward of OracleComp.pi sample_k along pushTuple parties.

noncomputable def Cslib.Crypto.Protocols.MPC.Composition.sampleSubCoins {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} {sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂} {Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type} (Sub : (op : spec₁.Op) → Protocol (spec₁.arity op) spec₂ (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op)) (sc₁ : Schedule m spec₁) (i : Fin m) : ProbComp (Schedule.SubCoins Coins₂ sc₁ i)

Sample party i's sequence of subprotocol coins along an outer schedule sc₁.

Embedded round/schedule transcripts and Steps.embed

def Cslib.Crypto.Protocols.MPC.Composition.pullRoundReceived {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (r : Round k spec) {s : Fin k} {i : Fin m} (hs : parties s = i) (recv_i : (Round.embed parties r).Received i) : r.Received s

Pull a received record in Round.embed parties r at party i back to slot s : Fin k given hs : parties s = i.

def Cslib.Crypto.Protocols.MPC.Composition.pullScheduleReceived {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (sc : Schedule k spec) {s : Fin k} {i : Fin m} (hs : parties s = i) : Schedule.Received (List.map (Round.embed parties) sc) i → sc.Received s

Pull a received transcript in sc.map (Round.embed parties) at party i back to slot s : Fin k given hs : parties s = i.

def Cslib.Crypto.Protocols.MPC.Composition.pushRoundReceived {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (r : Round k spec) (recv_k : (s : Fin k) → r.Received s) (i : Fin m) : (Round.embed parties r).Received i

Push a k-party received record recv_k : (s : Fin k) → r.Received s forward to all m parties in Round.embed parties r.

def Cslib.Crypto.Protocols.MPC.Composition.pushScheduleReceived {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (sc : Schedule k spec) : ((s : Fin k) → sc.Received s) → (i : Fin m) → Schedule.Received (List.map (Round.embed parties) sc) i

Push a k-party received transcript recv_k : (s : Fin k) → sc.Received s forward to all m parties in sc.map (Round.embed parties).

def Cslib.Crypto.Protocols.MPC.Composition.pushRoundReceivedRestrict {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (I : Finset (Fin m)) (r : Round k spec) (recv_J : (s : ↥(subCoalition parties I)) → r.Received ↑s) (i : ↥I) : (Round.embed parties r).Received ↑i

Push a coalition-restricted received record recv_J : (s : subCoalition parties I) → r.Received s.1 forward to (i : I) → (Round.embed parties r).Received i.1.

def Cslib.Crypto.Protocols.MPC.Composition.pushScheduleReceivedRestrict {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (I : Finset (Fin m)) (sc : Schedule k spec) : ((s : ↥(subCoalition parties I)) → sc.Received ↑s) → (i : ↥I) → Schedule.Received (List.map (Round.embed parties) sc) ↑i

Push a coalition-restricted received transcript recv_J : (s : subCoalition parties I) → sc.Received s.1 forward to (i : I) → Schedule.Received (sc.map (Round.embed parties)) i.1.

def Cslib.Crypto.Protocols.MPC.Composition.Steps.embed {k m : ℕ} {spec : MultiOracleSpec} (parties : Fin k ↪ Fin m) (Outer : Fin m → Type) {State_k Out_k : Fin k → Type} {sc : Schedule k spec} (steps : Steps State_k Out_k sc) : Steps (fun (i : Fin m) => Outer i × ((s : Fin k) → parties s = i → State_k s)) (fun (i : Fin m) => Outer i × ((s : Fin k) → parties s = i → Out_k s)) (List.map (Round.embed parties) sc)

Embed a k-party step computation steps : Steps State_k Out_k sc along parties : Fin k ↪ Fin m, threading an arbitrary m-party outer state Outer : Fin m → Type unchanged through the first state component.

Composing Steps, Protocol, and CoalitionSimulator

def Cslib.Crypto.Protocols.MPC.Composition.Steps.compose {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} {State Out : Fin m → Type} {sc₁ : Schedule m spec₁} {sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂} {Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type} (Sub : (op : spec₁.Op) → Protocol (spec₁.arity op) spec₂ (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op)) (steps : Steps State Out sc₁) : Steps (fun (i : Fin m) => State i × Schedule.SubCoins Coins₂ sc₁ i) Out (Schedule.compose sc₂ sc₁)

Replace each .oracle op parties node in steps : Steps State Out sc₁ with the embedded execution of (Sub op).steps along parties.

def Cslib.Crypto.Protocols.MPC.Composition.expandSimSteps {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} {State Out : Fin m → Type} {sc₁ : Schedule m spec₁} {sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂} {Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type} (S₂ : (op : spec₁.Op) → (J : Finset (Fin (spec₁.arity op))) → CoalitionSimulator (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op) J) (I : Finset (Fin m)) (steps : Steps State Out sc₁) (stI : (i : ↥I) → State ↑i) (recvI : (i : ↥I) → sc₁.Received ↑i) : ProbComp ((i : ↥I) → Schedule.SubCoins Coins₂ sc₁ ↑i × (Schedule.compose sc₂ sc₁).Received ↑i)

Expand a simulated outer execution along steps : Steps State Out sc₁ by invoking the inner simulator S₂ op (subCoalition parties I) at every .oracle op parties round (Goldreich Theorem 7.5.7 Proof Sketch, pp. 702–703).

noncomputable def Cslib.Crypto.Protocols.MPC.Protocol.compose {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} {sc₁ : Schedule m spec₁} {sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂} {In Coins₁ Out : Fin m → Type} {Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type} (P : Protocol m spec₁ sc₁ In Coins₁ Out) (Sub : (op : spec₁.Op) → Protocol (spec₁.arity op) spec₂ (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op)) : Protocol m spec₂ (Schedule.compose sc₂ sc₁) In (Schedule.ComposedCoins Coins₂ Coins₁ sc₁) Out

Compose an m-party protocol P over spec₁ with k-party subprotocols Sub op over spec₂ (Goldreich Section 7.5.2.1, Theorem 7.5.7, pp. 702–703; generalizing Section 7.3.1, Theorem 7.3.3, pp. 637–638).

noncomputable def Cslib.Crypto.Protocols.MPC.composeSim {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} {sc₁ : Schedule m spec₁} {sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂} {In Coins₁ Out : Fin m → Type} {Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type} (P : Protocol m spec₁ sc₁ In Coins₁ Out) (S₁ : (I : Finset (Fin m)) → CoalitionSimulator sc₁ In Coins₁ Out I) (S₂ : (op : spec₁.Op) → (J : Finset (Fin (spec₁.arity op))) → CoalitionSimulator (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op) J) (I : Finset (Fin m)) : CoalitionSimulator (Schedule.compose sc₂ sc₁) In (Schedule.ComposedCoins Coins₂ Coins₁ sc₁) Out I

Composed coalition simulator for P.compose Sub (Goldreich Section 7.5.2.1, Theorem 7.5.7 Proof Sketch, pp. 702–703; cf. Section 7.3.1, Theorem 7.3.3 Proof Sketch, pp. 637–638): runs the outer simulator S₁ I xI yI to obtain simulated outer views v₁ and expands each oracle call in P.steps using the inner simulator S₂ op (subCoalition parties I).

theorem Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate.compose {m : ℕ} {spec₁ spec₂ : MultiOracleSpec} {sc₁ : Schedule m spec₁} {sc₂ : (op : spec₁.Op) → Schedule (spec₁.arity op) spec₂} {In Coins₁ Out : Fin m → Type} {Coins₂ : (op : spec₁.Op) → Fin (spec₁.arity op) → Type} {P : Protocol m spec₁ sc₁ In Coins₁ Out} {W₁ : MultiOracleWorld spec₁} {W₂ : MultiOracleWorld spec₂} {f : Functionality m In Out} {S₁ : (I : Finset (Fin m)) → CoalitionSimulator sc₁ In Coins₁ Out I} {Sub : (op : spec₁.Op) → Protocol (spec₁.arity op) spec₂ (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op)} {S₂ : (op : spec₁.Op) → (J : Finset (Fin (spec₁.arity op))) → CoalitionSimulator (sc₂ op) (spec₁.Query op) (Coins₂ op) (spec₁.Answer op) J} (hP : PerfectSemiHonestPrivate P W₁ f S₁) (hSub : ∀ (op : spec₁.Op), PerfectSemiHonestPrivate (Sub op) W₂ (W₁ op) (S₂ op)) : PerfectSemiHonestPrivate (P.compose Sub) W₂ f (composeSim P S₁ S₂)

Theorem 7.5.7 (Goldreich Section 7.5.2.1, pp. 702–703; cf. Theorem 7.3.3, pp. 637–638): composing a perfectly private m-party outer protocol P with perfectly private k-party subprotocols Sub op yields a perfectly private m-party protocol P.compose Sub in W₂.

Part 2: Randomized-to-Deterministic Wrapper (Proposition 7.3.4 & Eq. 7.48)

noncomputable def Cslib.Crypto.Protocols.MPC.randomizedFunctionality {m : ℕ} {In Out : Fin m → Type} (coins : ℕ) (g : BitString coins → ((i : Fin m) → In i) → (i : Fin m) → Out i) : Functionality m In Out

Randomized m-party functionality defined by sampling a uniform shared coin string r : BitString coins and evaluating g r x (Goldreich Section 7.3.1, pp. 638–639; Section 7.5.2.4, p. 707).

def Cslib.Crypto.Protocols.MPC.detOfRandomized {m : ℕ} {In Out : Fin m → Type} (coins : ℕ) (g : BitString coins → ((i : Fin m) → In i) → (i : Fin m) → Out i) (xr : (i : Fin m) → In i × BitString coins) (i : Fin m) : Out i

Deterministic functionality associated to g via shared coin-tossing (Goldreich Section 7.5.2.4, Eq. 7.48, p. 707; generalizing Section 7.3.1, Eq. 7.19 on p. 638 and Proposition 7.3.4 on p. 639): takes party inputs (x_i, r_i) and evaluates g (∑ i : Fin m, r_i) x, where addition on BitString coins is bitwise XOR.

def Cslib.Crypto.Protocols.MPC.Protocol.mapInput {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In In' Coins Out : Fin m → Type} (enc : (i : Fin m) → In i → In' i) (P : Protocol m spec sc In' Coins Out) : Protocol m spec sc In Coins Out

Precompose an m-party protocol P with local party input encodings enc : (i : Fin m) → In i → In' i.

def Cslib.Crypto.Protocols.MPC.mapInputSim {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In In' Coins Out : Fin m → Type} (enc : (i : Fin m) → In i → In' i) (S : (I : Finset (Fin m)) → CoalitionSimulator sc In' Coins Out I) (I : Finset (Fin m)) : CoalitionSimulator sc In Coins Out I

Coalition simulator for P.mapInput enc.

theorem Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate.mapInput {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In In' Coins Out : Fin m → Type} {enc : (i : Fin m) → In i → In' i} {P : Protocol m spec sc In' Coins Out} {W : MultiOracleWorld spec} {f : Functionality m In' Out} {S : (I : Finset (Fin m)) → CoalitionSimulator sc In' Coins Out I} (hP : PerfectSemiHonestPrivate P W f S) : PerfectSemiHonestPrivate (Protocol.mapInput enc P) W (fun (x : (i : Fin m) → In i) => f fun (i : Fin m) => enc i (x i)) (mapInputSim enc S)

Perfect semi-honest privacy is preserved under local input encodings Protocol.mapInput.

noncomputable def Cslib.Crypto.Protocols.MPC.Protocol.randomizedWrapper {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (coins : ℕ) (P : Protocol m spec sc (fun (i : Fin m) => In i × BitString coins) Coins Out) : Protocol m spec sc In (fun (i : Fin m) => BitString coins × Coins i) Out

Wrap a deterministic-input protocol P expecting (x_i, r_i) into a protocol for input x_i in which each party i independently samples a uniform r_i : BitString coins as part of its private random tape (Goldreich Section 7.3.1, Proposition 7.3.4, p. 639; Section 7.5.2.4, Eq. 7.48, p. 707).

noncomputable def Cslib.Crypto.Protocols.MPC.randomizedWrapperSim {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (coins : ℕ) (S : (I : Finset (Fin m)) → CoalitionSimulator sc (fun (i : Fin m) => In i × BitString coins) Coins Out I) (I : Finset (Fin m)) : CoalitionSimulator sc In (fun (i : Fin m) => BitString coins × Coins i) Out I

Coalition simulator for P.randomizedWrapper coins (Goldreich Section 7.3.1, Proposition 7.3.4 Proof, pp. 639–640; Section 7.5.2.4, p. 707): samples independent uniform coin shares rI i for each coalition party i ∈ I, runs the deterministic simulator S I (fun i => (xI i, rI i)) yI, and combines (rI i, (v i).coins) into the simulated coin tape.

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_randomizedWrapper {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (coins : ℕ) (g : BitString coins → ((i : Fin m) → In i) → (i : Fin m) → Out i) (P : Protocol m spec sc (fun (i : Fin m) => In i × BitString coins) Coins Out) (W : MultiOracleWorld spec) (S : (I : Finset (Fin m)) → CoalitionSimulator sc (fun (i : Fin m) => In i × BitString coins) Coins Out I) (hP : PerfectSemiHonestPrivate P W (Functionality.ofDeterministic (detOfRandomized coins g)) S) : PerfectSemiHonestPrivateProper (Protocol.randomizedWrapper coins P) W (randomizedFunctionality coins g) (randomizedWrapperSim coins S)

Proposition 7.3.4 (Goldreich Section 7.3.1, pp. 639–640) combined with the composition theorem (Section 7.3.1 Application, pp. 638–639, Eq. 7.19) and Section 7.5.2.4 Eq. 7.48 (p. 707): if P is perfectly semi-honest private for detOfRandomized coins g, then P.randomizedWrapper coins is perfectly semi-honest private for randomizedFunctionality coins g against every proper static coalition I ≠ Finset.univ.

This is proved directly rather than via PerfectSemiHonestPrivate.compose, because the coin-sharing reduction is only private against proper coalitions I ≠ Finset.univ, whereas PerfectSemiHonestPrivate.compose requires all-I privacy of the outer protocol. Note that restricting to I ≠ Finset.univ is narrower than Goldreich's quantifier over all I ⊆ [m] in Definition 7.5.1 (p. 696, where I = [m] is called trivial on pp. 697, 703): under the joint view-and-output equation Eq. 7.40 for randomized functionalities, I = Finset.univ is not satisfied by an output-independent coin simulator (for m = 2, Definition 7.2.1 considers only single-party views, so Proposition 7.3.4 itself is fully covered). Moreover, this theorem proves exact PMF equality with an unrestricted ProbComp simulator rather than Goldreich's computational indistinguishability with PPT simulators.

Part 3: XOR Prelude Circuit and $\text{OT}_1^4$-Hybrid GMW Protocol (Theorem 7.5.12)

def Cslib.Crypto.Protocols.MPC.XORPrelude.xorBitAtCircuit (coins : ℕ) (c : Fin coins) : Circuits.Circuit Circuits.Boolean.signature (coins + coins) 1

Single-output 4-gate De Morgan circuit computing a c + b c (a c ^^ b c) at coordinate c : Fin coins of Fin.append a b : BitString (coins + coins), built from Cslib.Circuits.Program.appendXor.

def Cslib.Crypto.Protocols.MPC.XORPrelude.zeroBitStringCircuit (w coins : ℕ) : Circuits.Circuit Circuits.Boolean.signature w coins

Single-gate Boolean circuit outputting 0 : BitString coins via .const false.

def Cslib.Crypto.Protocols.MPC.XORPrelude.xorBitStringsCircuit (coins : ℕ) : Circuits.Circuit Circuits.Boolean.signature (coins + coins) coins

Coordinatewise XOR circuit of size 4 * coins on two coins-bit strings, constructed side by side via Cslib.Circuits.Circuit.pi from xorBitAtCircuit.

def Cslib.Crypto.Protocols.MPC.XORPrelude.sumBlocksCircuit (m coins : ℕ) : Circuits.Circuit Circuits.Boolean.signature (m * coins) coins

Boolean circuit summing m blocks of width coins by coordinatewise XOR.

def Cslib.Crypto.Protocols.MPC.XORPrelude.extractInputsCircuit (m n coins : ℕ) : Circuits.Circuit Circuits.Boolean.signature (m * (n + coins)) (m * n)

Zero-gate wiring circuit extracting the m * n party input bits from m blocks of width n + coins.

def Cslib.Crypto.Protocols.MPC.XORPrelude.extractCoinsCircuit (m n coins : ℕ) : Circuits.Circuit Circuits.Boolean.signature (m * (n + coins)) (m * coins)

Zero-gate wiring circuit extracting the m * coins party coin bits from m blocks of width n + coins.

def Cslib.Crypto.Protocols.MPC.xorPreludeCircuit (m n coins : ℕ) : Circuits.Circuit Circuits.Boolean.signature (m * (n + coins)) (m * n + coins)

XOR-combining prelude circuit (Goldreich Section 7.5.2.4, Eq. 7.48, p. 707): takes m party blocks (x_i, r_i) of width n + coins and outputs the m * n packed party inputs BitString.blocksEquiv.symm x followed by the coins-bit XOR sum ∑ i : Fin m, r i.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.eval_xorPreludeCircuit (m n coins : ℕ) (x : Fin m → BitString n) (r : Fin m → BitString coins) : (xorPreludeCircuit m n coins).eval Circuits.Boolean.interpretation (BitString.blocksEquiv.symm fun (i : Fin m) => Fin.append (x i) (r i)) = Fin.append (BitString.blocksEquiv.symm x) (∑ i : Fin m, r i)

Correctness of xorPreludeCircuit: evaluating xorPreludeCircuit m n coins on the packed input-coin blocks fun i => Fin.append (x i) (r i) yields Fin.append (BitString.blocksEquiv.symm x) (∑ i : Fin m, r i).

@[simp]

theorem Cslib.Crypto.Protocols.MPC.size_xorPreludeCircuit (m n coins : ℕ) : (xorPreludeCircuit m n coins).size = 1 + m * (4 * coins)

Gate count of xorPreludeCircuit m n coins.

noncomputable def Cslib.Crypto.Protocols.MPC.gmwOT14Protocol (m n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) : Protocol m ot14Spec (Schedule.compose (fun (x : (sharedMulSpec 2).Op) => twoPartyMulSchedule) (Schedule.compose (fun (x : (sharedMulSpec m).Op) => multiPartyMulSchedule m) (gmwCircuitSchedule m n k C))) (fun (x : Fin m) => BitString n) (Schedule.ComposedCoins (fun (x : (sharedMulSpec 2).Op) (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) (Schedule.ComposedCoins (fun (x : (sharedMulSpec m).Op) (x_1 : Fin m) => Unit) (fun (x : Fin m) => Fin n → Fin (m - 1) → Bool) (gmwCircuitSchedule m n k C)) (Schedule.compose (fun (x : (sharedMulSpec m).Op) => multiPartyMulSchedule m) (gmwCircuitSchedule m n k C))) fun (x : Fin m) => BitString k

Deterministic m-party $\text{OT}_1^4$-hybrid GMW protocol composed from gmwCircuitProtocol m n k C (Construction 7.5.10, p. 706), multiPartyMulProtocol m (Construction 7.5.8, p. 704), and twoPartyMulProtocol (Construction 7.3.7, p. 643). Because gmwCircuitProtocol m n k C makes one sharedMulSpec m call per .and/.or gate in Step 2 plus m * k sharedMulSpec m share-refresh calls in Step 3 (coordSchedule), composing with multiPartyMulProtocol m (m * (m - 1) / 2 calls to sharedMulSpec 2) and twoPartyMulProtocol (1 call to ot14Spec) expands each sharedMulSpec m call into m * (m - 1) / 2 pairwise calls to ot14Spec.

noncomputable def Cslib.Crypto.Protocols.MPC.gmwOT14Sim (m n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) (I : Finset (Fin m)) : CoalitionSimulator (Schedule.compose (fun (x : (sharedMulSpec 2).Op) => twoPartyMulSchedule) (Schedule.compose (fun (x : (sharedMulSpec m).Op) => multiPartyMulSchedule m) (gmwCircuitSchedule m n k C))) (fun (x : Fin m) => BitString n) (Schedule.ComposedCoins (fun (x : (sharedMulSpec 2).Op) (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) (Schedule.ComposedCoins (fun (x : (sharedMulSpec m).Op) (x_1 : Fin m) => Unit) (fun (x : Fin m) => Fin n → Fin (m - 1) → Bool) (gmwCircuitSchedule m n k C)) (Schedule.compose (fun (x : (sharedMulSpec m).Op) => multiPartyMulSchedule m) (gmwCircuitSchedule m n k C))) (fun (x : Fin m) => BitString k) I

Composed coalition simulator for gmwOT14Protocol m n k C.

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_gmwOT14 (m n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) : PerfectSemiHonestPrivate (gmwOT14Protocol m n k C) ot14World (Functionality.ofDeterministic (circuitFunctionality m n k C)) (gmwOT14Sim m n k C)

Full-coalition perfect semi-honest privacy of the deterministic gmwOT14Protocol m n k C in ot14World (combining Proposition 7.5.11, pp. 706–707; Proposition 7.5.9, pp. 704–705; Proposition 7.3.8, p. 644; and Theorem 7.5.7, pp. 702–703).

noncomputable def Cslib.Crypto.Protocols.MPC.gmwOT14RandomizedProtocol (m coins n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n + coins) (m * k)) : Protocol m ot14Spec (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))))) (fun (x : Fin m) => BitString n) (fun (i : Fin m) => BitString coins × Schedule.ComposedCoins (fun (x : (sharedMulSpec 2).Op) (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) (Schedule.ComposedCoins (fun (x : (sharedMulSpec m).Op) (x_1 : Fin m) => 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)))) i) fun (x : Fin m) => BitString k

Randomized m-party $\text{OT}_1^4$-hybrid GMW protocol (Goldreich Section 7.5.2.4, Eq. 7.48 and Theorem 7.5.12, p. 707; cf. Section 7.3.4, Theorem 7.3.11, p. 648): runs Protocol.randomizedWrapper coins around gmwOT14Protocol m (n + coins) k (C.comp (xorPreludeCircuit m n coins)) precomposed with Protocol.mapInput packing (x_i, r_i) into Fin.append x_i r_i : BitString (n + coins).

noncomputable def Cslib.Crypto.Protocols.MPC.gmwOT14RandomizedSim (m coins n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n + coins) (m * k)) (I : Finset (Fin m)) : CoalitionSimulator (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))))) (fun (x : Fin m) => BitString n) (fun (i : Fin m) => BitString coins × Schedule.ComposedCoins (fun (x : (sharedMulSpec 2).Op) (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) (Schedule.ComposedCoins (fun (x : (sharedMulSpec m).Op) (x_1 : Fin m) => 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)))) i) (fun (x : Fin m) => BitString k) I

Coalition simulator for gmwOT14RandomizedProtocol m coins n k C.

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivateProper_gmwOT14Randomized (m coins n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n + coins) (m * k)) : PerfectSemiHonestPrivateProper (gmwOT14RandomizedProtocol m coins n k C) ot14World (randomizedFunctionality coins fun (r : BitString coins) (x : Fin m → BitString n) (i : Fin m) => BitString.block (C.eval Circuits.Boolean.interpretation (Fin.append (BitString.blocksEquiv.symm x) r)) i) (gmwOT14RandomizedSim m coins n k C)

Theorem 7.5.12 (Goldreich Section 7.5.2.4, p. 707; generalizing Theorem 7.3.11, Section 7.3.4, p. 648): for any randomized m-party Boolean circuit C : Circuit Boolean.signature (m * n + coins) (m * k), gmwOT14RandomizedProtocol m coins n k C perfectly and privately computes the randomized functionality of C in ot14World against every proper static coalition I ≠ Finset.univ.

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, treating I = [m] as trivial on pp. 697, 703), because under the joint view-and-output equation Eq. 7.40 for randomized functionalities, I = Finset.univ is not satisfied when coin shares are simulated independently of the output. Furthermore, this theorem establishes exact PMF distributional equality with an unrestricted ProbComp simulator (gmwOT14RandomizedSim), whereas Goldreich states computational indistinguishability with PPT simulators (uniform polynomial-time efficiency is certified in M5).