Multi-Party Boolean Circuit Evaluation in the Shared-Multiplication Hybrid Model

This module formalizes the $m$-party Boolean circuit-evaluation protocol and its perfect semi-honest privacy reduction, adapted from Goldreich's Foundations of Cryptography, Volume 2: Basic Applications, Section 7.5.2.3 (Construction 7.5.10 and Proposition 7.5.11, print pp. 705–707; generalizing the 2-party protocol of Section 7.3.4, Construction 7.3.9 and Proposition 7.3.10, print pp. 645–648):

1. Deterministic $m$-Party Circuit Functionality (circuitFunctionality): packs m party inputs x : (i : Fin m) → BitString n into BitString (m * n) via Cslib.BitString.blocksEquiv.symm, evaluates a De Morgan circuit C : Cslib.Circuits.Circuit Boolean.signature (m * n) (m * k) under Boolean.interpretation, and unpacks the m * k output bits into (i : Fin m) → BitString k via Cslib.BitString.block.
2. GMW Circuit-Evaluation Protocol (gmwCircuitSchedule, gmwCircuitProtocol): in the sharedMulSpec m-hybrid model (Section 7.5.2, Eqs. 7.44–7.45, print p. 701):
   • Step 1 (Input sharing): each party s : Fin m samples private coins c s : Fin n → Fin (m - 1) → Bool, forms m additive shares of its input x s : BitString n via ProbComp.completeShares (placing the completing share at party m - 1, i.e., ⊤ : Fin m, rather than at sender s), and sends party r's share over a pairwise private .message s r (BitString n) round across allPairs m (including (s, s) self-messages).
   • Step 2 (Gate-by-gate circuit emulation): evaluates C.program gate by gate, preserving the invariant that the sum of all m parties' shares of every wire equals the true wire value in C.program.trace Boolean.interpretation (BitString.blocksEquiv.symm x). Whereas Construction 7.5.10 is stated for arithmetic circuits over $\mathrm{GF}(2)$ with addition and multiplication gates, Cslib.Circuits.Circuit Boolean.signature uses the De Morgan basis (const, not, and, or): constant and negation gates are evaluated locally (with party 0 holding the constant offset via constShare), while conjunction (.and) and disjunction (.or, via $a \lor b = a + b + a \cdot b$ over $\mathrm{GF}(2)$) invoke sharedMulSpec m.
   • Step 3 (Output share refresh and reconstruction — adaptation of Construction 7.5.10 Step 3): in Goldreich's Construction 7.5.10 Step 3 (print p. 706), parties exchange their output-wire shares directly via .message rounds under the circuit convention (print p. 705) that the output wires are the last, distinct gate wires of the circuit. Because Cslib.Circuits.Circuit.outputs : Fin (m * k) → Wire (m * n) C.size allows arbitrary wire references (including input wires, negated wires, or wires reused across multiple outputs), singleCoordSteps / outputSteps first refreshes the shares of each output coordinate (r, j) : Fin m × Fin k via one sharedMulSpec m call (multiplying by constShare true) before sending all m refreshed shares to recipient party r via .message s r Bool rounds (including s = r) so party r reconstructs circuitFunctionality m n k C x r.
3. Perfect Semi-Honest Privacy (gmwCircuitSim, perfectSemiHonestPrivate_gmwCircuit): proves Proposition 7.5.11 (print pp. 706–707), adapted to include the Step 3 share refresh so that gmwCircuitProtocol m n k C perfectly and privately computes Functionality.ofDeterministic (circuitFunctionality m n k C) in sharedMulWorld m against every static coalition I : Finset (Fin m) for every circuit C without syntactic restrictions on C.outputs.

Main definitions

• Cslib.Crypto.Protocols.MPC.circuitFunctionality: deterministic $m$-party functionality computed by a Boolean circuit C.
• Cslib.Crypto.Protocols.MPC.gmwCircuitSchedule, Cslib.Crypto.Protocols.MPC.gmwCircuitProtocol: Construction 7.5.10 (print p. 706), adapted to De Morgan gates and arbitrary Circuit.outputs via Step 3 share refresh.
• Cslib.Crypto.Protocols.MPC.gmwCircuitSim: coalition simulator for gmwCircuitProtocol.

Main results

• Cslib.Crypto.Protocols.MPC.snd_eq_circuitFunctionality_of_mem_support_evalWith: perfect output correctness of gmwCircuitProtocol m n k C in sharedMulWorld m.
• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_gmwCircuit: Proposition 7.5.11 (print pp. 706–707), perfect semi-honest privacy of gmwCircuitProtocol m n k C in sharedMulWorld m against every static coalition I : Finset (Fin m).

References

• O. Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Section 7.3.4 (Construction 7.3.9, Proposition 7.3.10, pp. 645–649), Section 7.5.1.2 (Definition 7.5.1, Eqs. 7.39–7.40, p. 696), Section 7.5.2 (Eqs. 7.44–7.45, p. 701), and Section 7.5.2.3 (Construction 7.5.10, Proposition 7.5.11, pp. 705–707).

Deterministic multi-party circuit functionality

def Cslib.Crypto.Protocols.MPC.circuitFunctionality (m n k : ℕ) (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) (x : Fin m → BitString n) (i : Fin m) : BitString k

Deterministic m-party Boolean circuit functionality (Goldreich Section 7.5.2.3, p. 705; cf. Section 7.3.4, pp. 645–646): packs the m party inputs x : (i : Fin m) → BitString n into BitString (m * n) via BitString.blocksEquiv.symm, evaluates C under Boolean.interpretation, and unpacks the m * k output bits into (i : Fin m) → BitString k via BitString.block.

Step 1: Input sharing via all-to-all point-to-point messages

def Cslib.Crypto.Protocols.MPC.GMWCircuit.allPairs (m : ℕ) : List (Fin m × Fin m)

All ordered sender-receiver pairs (s, r) : Fin m × Fin m (including (s, s) self-pairs).

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.msgRound {m : ℕ} {spec : MultiOracleSpec} (Msg : Type) (p : Fin m × Fin m) : Round m spec

Point-to-point message round from p.1 to p.2 carrying Msg.

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.msgSchedule {m : ℕ} {spec : MultiOracleSpec} (Msg : Type) (L : List (Fin m × Fin m)) : Schedule m spec

Schedule of point-to-point message rounds along L : List (Fin m × Fin m).

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.allToAllSchedule (m : ℕ) {spec : MultiOracleSpec} (Msg : Type) : Schedule m spec

Schedule of all-to-all point-to-point messages of type Msg.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.extractMsg {m : ℕ} {spec : MultiOracleSpec} {Msg : Type} [Zero Msg] (p : Fin m × Fin m) (i : Fin m) (recv : (msgRound Msg p).Received i) : Fin m → Msg

Extract party i's inbox update from message round p = (s, r).

def Cslib.Crypto.Protocols.MPC.GMWCircuit.msgStepsWith {m : ℕ} {spec : MultiOracleSpec} {Msg : Type} [AddCommMonoid Msg] {Out : Fin m → Type} (finish : (i : Fin m) → (Fin m → Msg) → Out i) (L : List (Fin m × Fin m)) : Steps (fun (x : Fin m) => (Fin m → Msg) × (Fin m → Msg)) Out (msgSchedule Msg L)

Execute point-to-point message rounds along L, accumulating received messages into st.2 and applying finish at .done.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.allToAllStepsWith (m : ℕ) {spec : MultiOracleSpec} {Msg : Type} [AddCommMonoid Msg] {Out : Fin m → Type} (finish : (i : Fin m) → (Fin m → Msg) → Out i) : Steps (fun (x : Fin m) => Fin m → Msg) Out (allToAllSchedule m Msg)

All-to-all message exchange: party s sends toSend s r to party r, and party i applies finish i to the vector fun s => toSend s i of received messages.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.receivedMsgOfInbox {m : ℕ} {spec : MultiOracleSpec} {Msg : Type} (p : Fin m × Fin m) (i : Fin m) (inbox_i : Fin m → Msg) : (msgRound Msg p).Received i

Received record for party i in round p = (s, r) constructed from party i's inbox inbox_i : Fin m → Msg.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.receivedScheduleOfInbox {m : ℕ} {spec : MultiOracleSpec} {Msg : Type} (i : Fin m) (inbox_i : Fin m → Msg) (L : List (Fin m × Fin m)) : (msgSchedule Msg L).Received i

Received transcript for party i along msgSchedule Msg L constructed from inbox_i.

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.deliverMessage_eq_receivedMsgOfInbox {m : ℕ} {spec : MultiOracleSpec} {Msg : Type} (toSend : Fin m → Fin m → Msg) (p : Fin m × Fin m) (i : Fin m) : Round.deliverMessage (toSend p.1 p.2) i = receivedMsgOfInbox p i fun (s : Fin m) => toSend s i

def Cslib.Crypto.Protocols.MPC.GMWCircuit.shareInputBits (m n : ℕ) (x_s : BitString n) (c_s : Fin n → Fin (m - 1) → Bool) : Fin m → BitString n

Party s's m additive shares of its input x_s : BitString n formed from its private coins c_s : Fin n → Fin (m - 1) → Bool via ProbComp.completeShares (Construction 7.5.10, Step 1, p. 706, with the completing share placed at ⊤ : Fin m).

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.shareInputBits_apply (m n : ℕ) (x_s : BitString n) (c_s : Fin n → Fin (m - 1) → Bool) (r : Fin m) (j : Fin n) : shareInputBits m n x_s c_s r j = ProbComp.completeShares m (x_s j) (c_s j) r

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.inputShareSchedule (m n : ℕ) : Schedule m (sharedMulSpec m)

Schedule for Step 1 (Input Sharing): all-to-all point-to-point exchange of BitString n.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.inputShareSteps (m n : ℕ) : Steps (fun (x : Fin m) => BitString n × (Fin n → Fin (m - 1) → Bool)) (fun (x : Fin m) => Fin (m * n) → Bool) (inputShareSchedule m n)

Step 1 (Input Sharing) of Construction 7.5.10 (p. 706): each party s computes shareInputBits m n (x s) (c s) and sends share r to party r; each party i packs the received shares via BitString.blocksEquiv.symm into its initial input-wire valuation Fin (m * n) → Bool.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.deliverInputShares {m n : ℕ} (x : Fin m → BitString n) (c : Fin m → Fin n → Fin (m - 1) → Bool) (i : Fin m) : (inputShareSchedule m n).Received i

Deterministic Step 1 received transcript when party s has input x s and coins c s.

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.outputAt_inputShareSteps {m n : ℕ} (x : Fin m → BitString n) (c : Fin m → Fin n → Fin (m - 1) → Bool) (i : Fin m) : (inputShareSteps m n).outputAt i (x i, c i) (deliverInputShares x c i) = BitString.blocksEquiv.symm fun (s : Fin m) => shareInputBits m n (x s) (c s) i

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.sum_outputAt_inputShareSteps {m n : ℕ} [NeZero m] (x : Fin m → BitString n) (c : Fin m → Fin n → Fin (m - 1) → Bool) (idx : Fin (m * n)) : ∑ i : Fin m, (inputShareSteps m n).outputAt i (x i, c i) (deliverInputShares x c i) idx = BitString.blocksEquiv.symm x idx

Step 2: Gate-by-gate circuit evaluation

def Cslib.Crypto.Protocols.MPC.GMWCircuit.extendWire {inputCount g : ℕ} (lastBit : Bool) (w : Circuits.Wire inputCount g → Bool) : Circuits.Wire inputCount (g + 1) → Bool

Extend a wire valuation w : Wire inputCount g → Bool with value lastBit on the new gate Wire.gate (Fin.last g).

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.extendWire_last {inputCount g : ℕ} (lastBit : Bool) (w : Circuits.Wire inputCount g → Bool) : extendWire lastBit w (Circuits.Wire.gate (Fin.last g)) = lastBit

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.extendWire_castSucc {inputCount g : ℕ} (lastBit : Bool) (w : Circuits.Wire inputCount g → Bool) (wire : Circuits.Wire inputCount g) : extendWire lastBit w wire.castSucc = w wire

def Cslib.Crypto.Protocols.MPC.GMWCircuit.constShare {m : ℕ} [NeZero m] (b : Bool) (i : Fin m) : Bool

Canonical additive share of a public Boolean constant b : Bool: party 0 holds b and all other parties hold false.

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.lineSchedule (m : ℕ) {inputCount g : ℕ} (line : Circuits.Line Circuits.Boolean.signature inputCount g) : Schedule m (sharedMulSpec m)

Schedule for evaluating a single gate line : Line Boolean.signature inputCount g. Constant and negation gates require no communication ([]); conjunction and disjunction gates invoke sharedMulSpec m once.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.lineSteps (m : ℕ) [NeZero m] {inputCount g : ℕ} (line : Circuits.Line Circuits.Boolean.signature inputCount g) : Steps (fun (x : Fin m) => Circuits.Wire inputCount g → Bool) (fun (x : Fin m) => Circuits.Wire inputCount (g + 1) → Bool) (lineSchedule m line)

Step-by-step protocol for evaluating a single gate line : Line Boolean.signature inputCount g, extending each party's wire valuation from Wire inputCount g → Bool to Wire inputCount (g + 1) → Bool.

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.progSchedule (m : ℕ) {inputCount g : ℕ} (prog : Circuits.Program Circuits.Boolean.signature inputCount g) : Schedule m (sharedMulSpec m)

Schedule for evaluating a straight-line program prog : Program Boolean.signature inputCount g.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.progSteps (m : ℕ) [NeZero m] {inputCount g : ℕ} (prog : Circuits.Program Circuits.Boolean.signature inputCount g) : Steps (fun (x : Fin m) => Fin inputCount → Bool) (fun (x : Fin m) => Circuits.Wire inputCount g → Bool) (progSchedule m prog)

Step-by-step evaluation of prog : Program Boolean.signature inputCount g (Construction 7.5.10, Step 2, p. 706, adapted to the De Morgan basis Boolean.signature).

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.deliverMulOracle {m : ℕ} (ans : Fin m → Bool) (i : Fin m) : Schedule.Received [Round.oracle () (Function.Embedding.refl (Fin m))] i

Deliver a single sharedMulSpec m oracle answer tuple ans as a 1-round Schedule.Received transcript.

noncomputable def Cslib.Crypto.Protocols.MPC.GMWCircuit.lineDist (m : ℕ) {inputCount g : ℕ} (x_flat : Fin inputCount → Bool) (p : Circuits.Program Circuits.Boolean.signature inputCount g) (line : Circuits.Line Circuits.Boolean.signature inputCount g) : ProbComp ((i : Fin m) → (lineSchedule m line).Received i)

Exact received-transcript sampler for a single gate line when the true wire values of p are p.trace Boolean.interpretation x_flat.

noncomputable def Cslib.Crypto.Protocols.MPC.GMWCircuit.progDist (m : ℕ) {inputCount g : ℕ} (x_flat : Fin inputCount → Bool) (prog : Circuits.Program Circuits.Boolean.signature inputCount g) : ProbComp ((i : Fin m) → (progSchedule m prog).Received i)

Exact received-transcript sampler for prog : Program Boolean.signature inputCount g on flattened input x_flat.

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.evalWith_progSteps {m inputCount g : ℕ} [NeZero m] (x_flat : Fin inputCount → Bool) (prog : Circuits.Program Circuits.Boolean.signature inputCount g) (st : Fin m → Fin inputCount → Bool) (hst : ∀ (idx : Fin inputCount), ∑ i : Fin m, st i idx = x_flat idx) : (progSteps m prog).evalWith (sharedMulWorld m) st = (progDist m x_flat prog).eval ∧ ∀ r_prog ∈ (progDist m x_flat prog).eval.support, ∀ (wire : Circuits.Wire inputCount g), ∑ i : Fin m, (progSteps m prog).outputAt i (st i) (r_prog i) wire = prog.trace Circuits.Boolean.interpretation x_flat wire

Step 3: Output share refresh and reconstruction

def Cslib.Crypto.Protocols.MPC.GMWCircuit.outCoords (m k : ℕ) : List (Fin m × Fin k)

All output coordinates (r, j) : Fin m × Fin k in lexicographic order.

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.gatherSchedule (m : ℕ) {spec : MultiOracleSpec} (r : Fin m) (S : List (Fin m)) : Schedule m spec

Schedule for gathering Bool shares from every sender s ∈ S at receiver r.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.extractBitFor {m : ℕ} {spec : MultiOracleSpec} (s r i : Fin m) (recv : (Round.message s r Bool).Received i) : Bool

Extract party i's received bit in .message s r Bool.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.gatherStepsWith {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} (r : Fin m) (finish : (i : Fin m) → State i → Bool → Out i) (S : List (Fin m)) : Steps (fun (i : Fin m) => State i × Bool × Bool) Out (gatherSchedule m r S)

Gather Bool shares at receiver r from senders S, preserving st.1 and st.2.1 and applying finish at .done.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.sumGatherBits {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) (S : List (Fin m)) (i : Fin m) : (gatherSchedule m r S).Received i → Bool

Sum of party i's received bits along gatherSchedule m r S.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.deliverGather {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) (ans : Fin m → Bool) (S : List (Fin m)) (i : Fin m) : (gatherSchedule m r S).Received i

Deterministic received transcript along gatherSchedule m r S when sender s sends ans s.

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.sumGatherBits_deliverGather {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) (ans : Fin m → Bool) (i : Fin m) : sumGatherBits r (List.finRange m) i (deliverGather r ans (List.finRange m) i) = if i = r then ∑ s : Fin m, ans s else 0

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.coordSchedule (m : ℕ) (r : Fin m) : Schedule m (sharedMulSpec m)

Schedule for refreshing and reconstructing a single output bit belonging to party r: one sharedMulSpec m oracle call (an adaptation of Goldreich Construction 7.5.10 Step 3, p. 706, that refreshes the output wire's shares for arbitrary Circuit.outputs) followed by m point-to-point .message s r Bool rounds (including s = r).

def Cslib.Crypto.Protocols.MPC.GMWCircuit.singleCoordSteps (m k : ℕ) [NeZero m] (coord : Fin m × Fin k) : Steps (fun (x : Fin m) => (Fin m → BitString k) × BitString k) (fun (x : Fin m) => (Fin m → BitString k) × BitString k) (coordSchedule m coord.1)

Refresh and reconstruct a single output coordinate coord = (r, j) : Fin m × Fin k (adaptation of Goldreich Construction 7.5.10 Step 3, p. 706): invokes sharedMulSpec m on (st.1 r j, constShare true s) to obtain fresh independent additive shares ans before sending ans s from each party s to party r, which adds Pi.single j (∑ s, ans s) to its output accumulator st.2 : BitString k. The extra sharedMulSpec m refresh allows C.outputs to reference arbitrary wires (including input wires, negated wires, or repeated wires).

def Cslib.Crypto.Protocols.MPC.GMWCircuit.deliverCoord {m : ℕ} (r : Fin m) (ans : Fin m → Bool) (i : Fin m) : (coordSchedule m r).Received i

Received transcript for coordSchedule m r when the refresh oracle returns ans.

theorem Cslib.Crypto.Protocols.MPC.GMWCircuit.outputAt_singleCoordSteps {m k : ℕ} [NeZero m] (coord : Fin m × Fin k) (ans : Fin m → Bool) (st_i : (Fin m → BitString k) × BitString k) (i : Fin m) : (singleCoordSteps m k coord).outputAt i st_i (deliverCoord coord.1 ans i) = (st_i.1, st_i.2 + if i = coord.1 then Pi.single coord.2 (∑ s : Fin m, ans s) else 0)

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.outCoordsSchedule (m : ℕ) {k : ℕ} : List (Fin m × Fin k) → Schedule m (sharedMulSpec m)

Schedule for refreshing and reconstructing a list L : List (Fin m × Fin k) of output coordinates.

def Cslib.Crypto.Protocols.MPC.GMWCircuit.outCoordsSteps (m k : ℕ) [NeZero m] (L : List (Fin m × Fin k)) : Steps (fun (x : Fin m) => (Fin m → BitString k) × BitString k) (fun (x : Fin m) => BitString k) (outCoordsSchedule m L)

Step-by-step refresh and reconstruction along L : List (Fin m × Fin k).

noncomputable def Cslib.Crypto.Protocols.MPC.GMWCircuit.outCoordsDist (m k : ℕ) (y : Fin m → BitString k) (L : List (Fin m × Fin k)) : ProbComp ((i : Fin m) → (outCoordsSchedule m L).Received i)

Exact received-transcript sampler for outCoordsSteps m k L on output table y.

@[reducible]

def Cslib.Crypto.Protocols.MPC.GMWCircuit.outputSchedule (m k : ℕ) : Schedule m (sharedMulSpec m)

Schedule for Step 3 (Output Share Refresh and Reconstruction).

def Cslib.Crypto.Protocols.MPC.GMWCircuit.outputSteps (m n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) : Steps (fun (x : Fin m) => Circuits.Wire (m * n) C.size → Bool) (fun (x : Fin m) => BitString k) (outputSchedule m k)

Step 3 of gmwCircuitProtocol (adapting Goldreich Construction 7.5.10 Step 3, p. 706, with a per-coordinate sharedMulSpec m share refresh so C.outputs can reference arbitrary wires): extracts each party's shares of the m * k designated output wires C.outputs and runs outCoordsSteps m k (outCoords m k).

noncomputable def Cslib.Crypto.Protocols.MPC.GMWCircuit.outputDist (m k : ℕ) (y : Fin m → BitString k) : ProbComp ((i : Fin m) → (outputSchedule m k).Received i)

Exact received-transcript sampler for outputSteps m n k C when the circuit output is y.

Coalition restriction and simulation helpers

def Cslib.Crypto.Protocols.MPC.GMWCircuit.extendByZero {m : ℕ} {α : Type} [Zero α] (I : Finset (Fin m)) (vI : ↥I → α) (j : Fin m) : α

Extend a partial tuple vI : (i : I) → α on a coalition I : Finset (Fin m) to all m parties by padding parties outside I with 0.

@[reducible]

def Cslib.Crypto.Protocols.MPC.gmwCircuitSchedule (m n k : ℕ) (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) : Schedule m (sharedMulSpec m)

Complete schedule for gmwCircuitProtocol m n k C (Construction 7.5.10, p. 706, with Step 3 share refresh): Step 1 (inputShareSchedule m n), followed by Step 2 (progSchedule m C.program) and Step 3 (outputSchedule m k).

noncomputable def Cslib.Crypto.Protocols.MPC.gmwCircuitProtocol (m n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) : Protocol m (sharedMulSpec m) (gmwCircuitSchedule m n k C) (fun (x : Fin m) => BitString n) (fun (x : Fin m) => Fin n → Fin (m - 1) → Bool) fun (x : Fin m) => BitString k

Construction 7.5.10 (Goldreich Section 7.5.2.3, p. 706; cf. Construction 7.3.9, pp. 646–647), adapted to De Morgan circuits (Boolean.signature) and arbitrary C.outputs: m-party Boolean circuit evaluation protocol in the sharedMulSpec m-hybrid model. In Step 1, party i samples Fin n → Fin (m - 1) → Bool from sampleCoins i, applies ProbComp.completeShares m (x i j) to form the m shares of bit j, and sends share r via .message rounds. Step 2 evaluates C.program gate by gate, and Step 3 refreshes each output coordinate via one sharedMulSpec m call (multiplying by constShare true) before exchanging the refreshed output shares via .message rounds.

noncomputable def Cslib.Crypto.Protocols.MPC.GMWCircuit.gmwCircuitRealViews (m n k : ℕ) (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) (x : Fin m → BitString n) (y : Fin m → BitString k) : ProbComp ((i : Fin m) → PartyView (fun (x : Fin m) => BitString n) (fun (x : Fin m) => Fin n → Fin (m - 1) → Bool) (gmwCircuitSchedule m n k C) i)

Joint view sampler for gmwCircuitProtocol m n k C given full input tuple x and output tuple y: samples Step 1 coins c, Step 2 gate transcripts r_prog, and Step 3 output transcripts r_out independently.

theorem Cslib.Crypto.Protocols.MPC.snd_eq_circuitFunctionality_of_mem_support_evalWith {m n k : ℕ} [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) (x : Fin m → BitString n) {res : ((i : Fin m) → PartyView (fun (x : Fin m) => BitString n) (fun (x : Fin m) => Fin n → Fin (m - 1) → Bool) (gmwCircuitSchedule m n k C) i) × (Fin m → BitString k)} (hres : res ∈ ((gmwCircuitProtocol m n k C).evalWith (sharedMulWorld m) x).support) : res.2 = circuitFunctionality m n k C x

Output correctness of gmwCircuitProtocol: every outcome in the support of (gmwCircuitProtocol m n k C).evalWith (sharedMulWorld m) x produces output tuple circuitFunctionality m n k C x.

noncomputable def Cslib.Crypto.Protocols.MPC.gmwCircuitSim (m n k : ℕ) (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) (I : Finset (Fin m)) : CoalitionSimulator (gmwCircuitSchedule m n k C) (fun (x : Fin m) => BitString n) (fun (x : Fin m) => Fin n → Fin (m - 1) → Bool) (fun (x : Fin m) => BitString k) I

Simulator for gmwCircuitProtocol m n k C (Proposition 7.5.11, pp. 706–707; cf. Proposition 7.3.10, pp. 647–648): extends the coalition's inputs xI and outputs yI by padding honest parties outside I with 0, runs gmwCircuitRealViews on the extended tuples, and restricts the resulting party views to I.

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_gmwCircuit (m n k : ℕ) [NeZero m] (C : Circuits.Circuit Circuits.Boolean.signature (m * n) (m * k)) : PerfectSemiHonestPrivate (gmwCircuitProtocol m n k C) (sharedMulWorld m) (Functionality.ofDeterministic (circuitFunctionality m n k C)) (gmwCircuitSim m n k C)

Proposition 7.5.11 (Goldreich Section 7.5.2.3, pp. 706–707; cf. Proposition 7.3.10, pp. 647–648), adapted to De Morgan circuits (Boolean.signature) and arbitrary C.outputs via Step 3 share refresh: gmwCircuitProtocol m n k C perfectly and privately computes Functionality.ofDeterministic (circuitFunctionality m n k C) in sharedMulWorld m against every static coalition I : Finset (Fin m).