Ideal $\text{OT}_1^4$, 2-Party Shared Multiplication, and Pairwise $m$-Party Reduction

This module formalizes the shared-multiplication functionalities and oracle-aided privacy reductions from Goldreich's Foundations of Cryptography, Volume 2: Basic Applications:

1. 1-out-of-4 Oblivious Transfer (ot14Spec, ot14World): the asymmetric 2-party ideal oracle specification and world (Section 7.3.2, Eq. 7.20, print p. 640, for $k = 4$) in which slot 0 (sender) submits a 4-tuple of bits Fin 4 → Bool and receives Unit, while slot 1 (receiver) submits an index Fin 4 and receives the selected bit.
2. $m$-Party Shared Multiplication (sharedMulFunctionality, sharedMulSpec, sharedMulWorld): the randomized $m$-party functionality mapping $((a_1, b_1), \dots, (a_m, b_m))$ to uniform additive shares $(c_1, \dots, c_m) \in \{0, 1\}^m$ summing to $(\sum_i a_i) \cdot (\sum_i b_i)$ over $\mathrm{GF}(2)$ (BooleanRing Bool) (Section 7.3, Eqs. 7.17–7.18, print p. 635 for $m = 2$; Section 7.5.2, Eqs. 7.44–7.45, print p. 701 for general $m$).
3. 2-Party Shared Multiplication in the $\text{OT}_1^4$-Hybrid Model (twoPartyMulProtocol, twoPartyMulSim, perfectSemiHonestPrivate_twoPartyMul): Construction 7.3.7 and Proposition 7.3.8 (Section 7.3.3, Eq. 7.21, print pp. 643–644), proved perfectly semi-honest private against every static coalition I : Finset (Fin 2).
4. Pairwise $m$-Party Shared Multiplication Reduction (multiPartyMulProtocol, multiPartyMulSim, perfectSemiHonestPrivate_multiPartyMul): Construction 7.5.8 and Proposition 7.5.9 (Section 7.5.2.2, Eqs. 7.46–7.47, print pp. 703–705), reducing $m$-party shared multiplication to pairwise invocations of the 2-party shared-multiplication oracle sharedMulSpec 2 over all ordered pairs $i < j$, proved perfectly semi-honest private against every static coalition I : Finset (Fin m).

Main definitions

• Cslib.Crypto.Protocols.MPC.ot14Spec, Cslib.Crypto.Protocols.MPC.ot14World: 2-party $\text{OT}_1^4$ oracle specification and ideal world.
• Cslib.Crypto.Protocols.MPC.sharedMulFunctionality, Cslib.Crypto.Protocols.MPC.sharedMulSpec, Cslib.Crypto.Protocols.MPC.sharedMulWorld: $m$-party shared-multiplication functionality, oracle specification, and ideal world.
• Cslib.Crypto.Protocols.MPC.twoPartyMulSchedule, Cslib.Crypto.Protocols.MPC.twoPartyMulProtocol, Cslib.Crypto.Protocols.MPC.twoPartyMulSim: Construction 7.3.7 and its coalition simulator.
• Cslib.Crypto.Protocols.MPC.multiPartyMulSchedule, Cslib.Crypto.Protocols.MPC.multiPartyMulProtocol, Cslib.Crypto.Protocols.MPC.multiPartyMulSim: Construction 7.5.8 and its coalition simulator.

Main results

• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_twoPartyMul: Proposition 7.3.8 (print p. 644), perfect semi-honest privacy of twoPartyMulProtocol in ot14World against every static coalition I : Finset (Fin 2).
• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_multiPartyMul: Proposition 7.5.9 (print pp. 704–705), perfect semi-honest privacy of multiPartyMulProtocol m in sharedMulWorld 2 against every static coalition I : Finset (Fin m).

References

• O. Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Section 7.3 (Eqs. 7.17–7.18, p. 635), Section 7.3.2 (Eq. 7.20, p. 640), Section 7.3.3 (Construction 7.3.7, Eq. 7.21, Proposition 7.3.8, pp. 643–644), Section 7.5.2 (Eqs. 7.44–7.45, p. 701), and Section 7.5.2.2 (Eqs. 7.46–7.47, Construction 7.5.8, Proposition 7.5.9, pp. 703–705).

Ideal $\text{OT}_1^4$ and $m$-party shared multiplication

@[reducible]

def Cslib.Crypto.Protocols.MPC.ot14Spec : MultiOracleSpec

2-party 1-out-of-4 Oblivious Transfer oracle specification (Goldreich Section 7.3.2, Eq. 7.20, p. 640, for $k = 4$): slot 0 (sender) submits a 4-tuple of bits Fin 4 → Bool and receives Unit; slot 1 (receiver) submits an index Fin 4 and receives the selected bit Bool.

def Cslib.Crypto.Protocols.MPC.ot14Answer (q : (s : Fin 2) → ot14Spec.Query () s) (s : Fin 2) : ot14Spec.Answer () s

Answer tuple for ot14Spec on query q: returns () to slot 0 and (q 0) (q 1) to slot 1.

def Cslib.Crypto.Protocols.MPC.ot14World : MultiOracleWorld ot14Spec

Ideal memoryless world for ot14Spec (Goldreich Section 7.3.2, Eq. 7.20, p. 640): returns () to the sender (slot 0) and (q 0) (q 1) to the receiver (slot 1).

noncomputable def Cslib.Crypto.Protocols.MPC.sharedMulFunctionality (m : ℕ) : Functionality m (fun (x : Fin m) => Bool × Bool) fun (x : Fin m) => Bool

Randomized m-party shared-multiplication functionality over $\mathrm{GF}(2)$ (Goldreich Section 7.3, Eqs. 7.17–7.18, p. 635 for $m = 2$; Section 7.5.2, Eqs. 7.44–7.45, p. 701 for general $m$): samples uniform additive shares summing to $(\sum_{i=1}^m a_i) \cdot (\sum_{i=1}^m b_i)$.

@[reducible]

def Cslib.Crypto.Protocols.MPC.sharedMulSpec (m : ℕ) : MultiOracleSpec

m-ary oracle specification for shared multiplication (sharedMulFunctionality m).

noncomputable def Cslib.Crypto.Protocols.MPC.sharedMulWorld (m : ℕ) : MultiOracleWorld (sharedMulSpec m)

Ideal memoryless world for sharedMulSpec m backed by sharedMulFunctionality m.

Construction 7.3.7 and Proposition 7.3.8: 2-party shared multiplication

def Cslib.Crypto.Protocols.MPC.boolPairToFin4 (p : Bool × Bool) : Fin 4

Encode a pair of bits (a, b) : Bool × Bool as 2 * a + b in Fin 4 (0-indexed version of Goldreich Construction 7.3.7's 1 + 2a₂ + b₂ ∈ {1, 2, 3, 4}, p. 643).

def Cslib.Crypto.Protocols.MPC.fin4ToBoolPair (idx : Fin 4) : Bool × Bool

Decode an index in Fin 4 to its pair of bits Bool × Bool.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.fin4ToBoolPair_boolPairToFin4 (p : Bool × Bool) : fin4ToBoolPair (boolPairToFin4 p) = p

def Cslib.Crypto.Protocols.MPC.twoPartyMulResidual (ab xy : Bool × Bool) (z : Bool) : Bool

Residual function $f_{a,b}(x, y, z) = z + (x + a) \cdot (y + b)$ over $\mathrm{GF}(2)$ from Goldreich Construction 7.3.7, Step 2 (p. 643).

@[reducible]

def Cslib.Crypto.Protocols.MPC.twoPartyMulSchedule : Schedule 2 ot14Spec

Schedule for twoPartyMulProtocol: a single joint 2-party invocation of ot14Spec with party 0 as sender and party 1 as receiver.

noncomputable def Cslib.Crypto.Protocols.MPC.twoPartyMulSampleCoins (i : Fin 2) : ProbComp (Fin.cases Bool (fun (x : Fin 1) => Unit) i)

Coin sampler for twoPartyMulProtocol: party 0 samples a uniform bit; party 1 uses ().

def Cslib.Crypto.Protocols.MPC.twoPartyMulCoins (c₀ : Bool) (i : Fin 2) : Fin.cases Bool (fun (x : Fin 1) => Unit) i

Package party 0's coin c₀ : Bool and party 1's coin () : Unit into the 2-party coin tuple.

def Cslib.Crypto.Protocols.MPC.twoPartyMulQuery (s : Fin (ot14Spec.arity ())) (st : (Bool × Bool) × Fin.cases Bool (fun (x : Fin 1) => Unit) ((Function.Embedding.refl (Fin 2)) s)) : ot14Spec.Query () s

Oracle query function for twoPartyMulProtocol (Eq. 7.21, p. 643).

def Cslib.Crypto.Protocols.MPC.twoPartyMulOutput (i : Fin 2) (st : ((Bool × Bool) × Fin.cases Bool (fun (x : Fin 1) => Unit) i) × (Round.oracle () (Function.Embedding.refl (Fin 2))).Received i) : Bool

Output extraction function for twoPartyMulProtocol.

noncomputable def Cslib.Crypto.Protocols.MPC.twoPartyMulProtocol : Protocol 2 ot14Spec twoPartyMulSchedule (fun (x : Fin 2) => Bool × Bool) (fun (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) fun (x : Fin 2) => Bool

Construction 7.3.7 (p. 643): 2-party shared multiplication in the ot14Spec-hybrid model. Party 0 samples a uniform bit c₀, submits the 4-tuple of residual values fun idx => twoPartyMulResidual (fin4ToBoolPair idx) (a₀, b₀) c₀ (Eq. 7.21, p. 643) as sender in ot14Spec, and outputs c₀. Party 1 submits boolPairToFin4 (a₁, b₁) as receiver in ot14Spec and outputs the received bit c₀ + (a₀ + a₁) * (b₀ + b₁).

def Cslib.Crypto.Protocols.MPC.twoPartyMulReceived (i : Fin 2) (yi : Bool) : (Round.oracle () (Function.Embedding.refl (Fin 2))).Received i

Received oracle record for party i in twoPartyMulProtocol when its output is yi.

def Cslib.Crypto.Protocols.MPC.twoPartyMulViewOfInOut (i : Fin 2) (xi : Bool × Bool) (yi : Bool) : PartyView (fun (x : Fin (1 + 1)) => Bool × Bool) (fun (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) twoPartyMulSchedule i

Reconstruct party i's complete PartyView in twoPartyMulProtocol deterministically from its input xi : Bool × Bool and its output yi : Bool (Goldreich Proposition 7.3.8 Proof Sketch, p. 644): for party 0, its coin is yi and its oracle answer is (); for party 1, its coin is () and its oracle answer is yi.

def Cslib.Crypto.Protocols.MPC.twoPartyMulSim (I : Finset (Fin 2)) : CoalitionSimulator twoPartyMulSchedule (fun (x : Fin 2) => Bool × Bool) (fun (i : Fin (1 + 1)) => Fin.cases Bool (fun (x : Fin 1) => Unit) i) (fun (x : Fin 2) => Bool) I

Coalition simulator for twoPartyMulProtocol (Goldreich Proposition 7.3.8, p. 644): each corrupted party i ∈ I deterministically forms its view from its own input xI i and output yI i.

@[instance_reducible]

instance Cslib.Crypto.Protocols.MPC.instFintypeFinCasesBoolUnit (i : Fin 2) : Fintype (Fin.cases Bool (fun (x : Fin 1) => Unit) i)

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_twoPartyMul : PerfectSemiHonestPrivate twoPartyMulProtocol ot14World (sharedMulFunctionality 2) twoPartyMulSim

Proposition 7.3.8 (p. 644): Construction 7.3.7 is perfectly semi-honest private in ot14World against every static coalition I : Finset (Fin 2).

Construction 7.5.8 and Proposition 7.5.9: pairwise $m$-party reduction

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.OrderedPair (m : ℕ) : Type

An ordered pair (i, j) of parties in Fin m with i < j.

def Cslib.Crypto.Protocols.MPC.pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m

Embedding of Fin 2 into Fin m sending 0 ↦ p.1.1 and 1 ↦ p.1.2 for an ordered pair p : OrderedPair m.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.pairEmbedding_zero {m : ℕ} (p : OrderedPair m) : (pairEmbedding p) 0 = (↑p).1

@[simp]

theorem Cslib.Crypto.Protocols.MPC.pairEmbedding_one {m : ℕ} (p : OrderedPair m) : (pairEmbedding p) 1 = (↑p).2

@[reducible]

def Cslib.Crypto.Protocols.MPC.pairRound {m : ℕ} (p : OrderedPair m) : Round m (sharedMulSpec 2)

Joint 2-party shared-multiplication oracle round for p : OrderedPair m.

theorem Cslib.Crypto.Protocols.MPC.subsingleton_received_pairRound {m : ℕ} (p : OrderedPair m) {i : Fin m} (h1 : i ≠ (↑p).1) (h2 : i ≠ (↑p).2) : Subsingleton ((pairRound p).Received i)

A party i that is neither p.1.1 nor p.1.2 receives a subsingleton record in pairRound p.

@[reducible]

def Cslib.Crypto.Protocols.MPC.pairsSchedule {m : ℕ} (L : List (OrderedPair m)) : Schedule m (sharedMulSpec 2)

Schedule of 2-party shared-multiplication oracle rounds for a list of ordered pairs L.

def Cslib.Crypto.Protocols.MPC.orderedPairs (m : ℕ) : List (OrderedPair m)

Canonical list of all ordered pairs i < j in Fin m in lexicographic order.

@[reducible]

def Cslib.Crypto.Protocols.MPC.multiPartyMulSchedule (m : ℕ) : Schedule m (sharedMulSpec 2)

Schedule for multiPartyMulProtocol m: invokes sharedMulSpec 2 once for each ordered pair i < j in orderedPairs m (Goldreich Construction 7.5.8, Step 1, p. 704).

def Cslib.Crypto.Protocols.MPC.extractPairShare {m : ℕ} (p : OrderedPair m) (i : Fin m) (r : (pairRound p).Received i) : Bool

Extract party i's oracle answer share from pairRound p (0 if i is not one of the two participating parties p.1.1 or p.1.2).

def Cslib.Crypto.Protocols.MPC.pairsSteps {m : ℕ} (L : List (OrderedPair m)) : Steps (fun (x : Fin m) => (Bool × Bool) × Bool) (fun (x : Fin m) => Bool) (pairsSchedule L)

Step-by-step execution over a list of ordered pairs L, where each party's local state is ((a_i, b_i), acc_i) : (Bool × Bool) × Bool. In each round p ∈ L, p.1.1 and p.1.2 submit their input pairs (a_i, b_i) to sharedMulSpec 2 and each party adds its received share (extractPairShare p i) to acc_i.

def Cslib.Crypto.Protocols.MPC.multiPartyMulProtocol (m : ℕ) : Protocol m (sharedMulSpec 2) (multiPartyMulSchedule m) (fun (x : Fin m) => Bool × Bool) (fun (x : Fin m) => Unit) fun (x : Fin m) => Bool

Construction 7.5.8 (p. 704): m-party shared multiplication in the 2-ary sharedMulSpec 2-hybrid model, invoking sharedMulSpec 2 once for each pair i < j. Party i initializes its accumulator to $m \cdot a_i b_i$ (m • ((x i).1 * (x i).2)), adds its received share from every pair {i, j}, and outputs the resulting sum $c_i = m a_i b_i + \sum_{j \neq i} c_i^{\{i, j\}}$.

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.sumReceivedShares {m : ℕ} (L : List (OrderedPair m)) (i : Fin m) : (pairsSchedule L).Received i → Bool

Sum of party i's received oracle shares across L : List (OrderedPair m).

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.outputAt_pairsSteps {m : ℕ} (L : List (OrderedPair m)) (i : Fin m) (st_i : (Bool × Bool) × Bool) (recv_i : (pairsSchedule L).Received i) : (pairsSteps L).outputAt i st_i recv_i = st_i.2 + sumReceivedShares L i recv_i

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.outputOfView_multiPartyMulProtocol {m : ℕ} (i : Fin m) (v : PartyView (fun (x : Fin m) => Bool × Bool) (fun (x : Fin m) => Unit) (multiPartyMulSchedule m) i) : (multiPartyMulProtocol m).outputOfView i v = m • (v.input.1 * v.input.2) + sumReceivedShares (orderedPairs m) i v.received

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) : (pairRound p).Received i

Construct party i's received oracle record in pairRound p from party i's row of pairwise shares row_i : Fin m → Bool.

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.receivedScheduleOfRow {m : ℕ} (i : Fin m) (row_i : Fin m → Bool) (L : List (OrderedPair m)) : (pairsSchedule L).Received i

Construct party i's received transcript along pairsSchedule L from party i's row of pairwise shares row_i : Fin m → Bool.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.extractPairShare_receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) : extractPairShare p i (receivedPairOfRow p i row_i) = (if (↑p).1 = i then row_i (↑p).2 else 0) + if (↑p).2 = i then row_i (↑p).1 else 0

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.sumReceivedShares_receivedScheduleOfRow {m : ℕ} (i : Fin m) (row_i : Fin m → Bool) (hdiag : row_i i = 0) : sumReceivedShares (orderedPairs m) i (receivedScheduleOfRow i row_i (orderedPairs m)) = ∑ j : Fin m, row_i j

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.pairTarget {m : ℕ} (x : Fin m → Bool × Bool) (i j : Fin m) : Bool

Target sum $(a_i + a_j) \cdot (b_i + b_j)$ for the pair of parties (i, j).

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.pairTarget_comm {m : ℕ} (x : Fin m → Bool × Bool) (i j : Fin m) : pairTarget x i j = pairTarget x j i

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.pairTarget_self {m : ℕ} (x : Fin m → Bool × Bool) (i : Fin m) : pairTarget x i i = 0

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.matrixOfCoins {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (i j : Fin m) : Bool

Matrix of pairwise shares $C(r, x)_{i, j}$ generated by coin vector r : OrderedPair m → Bool on input x:

• for i < j, party i receives r ⟨(i, j), h⟩;
• for j < i, party i receives r ⟨(j, i), h⟩ + pairTarget x i j;
• for i = j, 0.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.matrixOfCoins_self {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (i : Fin m) : matrixOfCoins x r i i = 0

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.symMatrix {m : ℕ} (d : OrderedPair m → Bool) (i j : Fin m) : Bool

Symmetric zero-diagonal matrix associated with d : OrderedPair m → Bool.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.matrixOfCoins_add {m : ℕ} (x : Fin m → Bool × Bool) (r d : OrderedPair m → Bool) (i j : Fin m) : matrixOfCoins x (r + d) i j = matrixOfCoins x r i j + symMatrix d i j

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.realOut {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (i : Fin m) : Bool

Output of party i in multiPartyMulProtocol m when the pairwise coin vector is r.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.realOut_add {m : ℕ} (x : Fin m → Bool × Bool) (r d : OrderedPair m → Bool) (i : Fin m) : realOut x (r + d) i = realOut x r i + ∑ j : Fin m, symMatrix d i j

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.sum_symMatrix {m : ℕ} (d : OrderedPair m → Bool) : ∑ i : Fin m, ∑ j : Fin m, symMatrix d i j = 0

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.sum_realOut {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) : ∑ i : Fin m, realOut x r i = (∑ i : Fin m, (x i).1) * ∑ i : Fin m, (x i).2

Equations (7.46)–(7.47) (Goldreich Section 7.5.2.2, p. 703): for every coin vector r, the sum of all m parties' outputs in Construction 7.5.8 equals $(\sum_i a_i) \cdot (\sum_i b_i)$.

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.viewOfRow {m : ℕ} (i : Fin m) (xi : Bool × Bool) (row_i : Fin m → Bool) : PartyView (fun (x : Fin m) => Bool × Bool) (fun (x : Fin m) => Unit) (multiPartyMulSchedule m) i

Complete PartyView of party i in multiPartyMulProtocol m constructed from its input xi : Bool × Bool and its row of pairwise shares row_i : Fin m → Bool.

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.pairAnswer {m : ℕ} (x : Fin m → Bool × Bool) (p : OrderedPair m) (b : Bool) : Fin 2 → Bool

2-party oracle answer tuple for pair p on input x and coin b : Bool.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.deliverOracle_pairAnswer_eq_receivedPairOfRow {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (p : OrderedPair m) (i : Fin m) : Round.deliverOracle (pairEmbedding p) (pairAnswer x p (r p)) i = receivedPairOfRow p i (matrixOfCoins x r i)

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.nodup_orderedPairs (m : ℕ) : (orderedPairs m).Nodup

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.deliverCoins {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (L : List (OrderedPair m)) (i : Fin m) : (pairsSchedule L).Received i

Received transcript along pairsSchedule L generated by r : OrderedPair m → Bool.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.deliverCoins_eq_receivedScheduleOfRow {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (L : List (OrderedPair m)) (i : Fin m) : deliverCoins x r L i = receivedScheduleOfRow i (matrixOfCoins x r i) L

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.deliverCoins_update_of_not_mem {m : ℕ} (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) {p₀ : OrderedPair m} {L : List (OrderedPair m)} (hp₀ : p₀ ∉ L) (b : Bool) : deliverCoins x (Function.update r p₀ b) L = deliverCoins x r L

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.evalWith_pairsSteps {m : ℕ} {L : List (OrderedPair m)} (hL : L.Nodup) (st : Fin m → (Bool × Bool) × Bool) : (pairsSteps L).evalWith (sharedMulWorld 2) st = PMF.map (fun (r : OrderedPair m → Bool) => deliverCoins (fun (j : Fin m) => (st j).1) r L) (Probability.PMF.uniformOfFintype (OrderedPair m → Bool))

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.evalWith_multiPartyMulProtocol (m : ℕ) (x : Fin m → Bool × Bool) : (multiPartyMulProtocol m).evalWith (sharedMulWorld 2) x = PMF.map (fun (r : OrderedPair m → Bool) => (fun (i : Fin m) => viewOfRow i (x i) (matrixOfCoins x r i), realOut x r)) (Probability.PMF.uniformOfFintype (OrderedPair m → Bool))

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.delta {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) (p : OrderedPair m) : Bool

Coin adjustment supported on pairs incident to the pivot party ℓ : Fin m.

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.deltaErase {m : ℕ} (ℓ : Fin m) (u : ↥(Finset.univ.erase ℓ) → Bool) (p : OrderedPair m) : Bool

Restriction-based presentation of delta ℓ depending only on Finset.univ.erase ℓ.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.delta_eq_deltaErase_restrict {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) : delta ℓ w = deltaErase ℓ ((Finset.univ.erase ℓ).restrict w)

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.symMatrix_delta_of_ne {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) {i : Fin m} (hi : i ≠ ℓ) (j : Fin m) : symMatrix (delta ℓ w) i j = if j = ℓ then w i else 0

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.realOut_add_delta_of_ne {m : ℕ} (ℓ : Fin m) (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (w : Fin m → Bool) {i : Fin m} (hi : i ≠ ℓ) : realOut x (r + delta ℓ w) i = realOut x r i + w i

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.tildeR {m : ℕ} (ℓ : Fin m) (x : Fin m → Bool × Bool) (y : Fin m → Bool) (r : OrderedPair m → Bool) : OrderedPair m → Bool

Adjust coin vector r at pairs incident to ℓ so the protocol outputs equal y.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.realOut_tildeR_of_ne {m : ℕ} (ℓ : Fin m) (x : Fin m → Bool × Bool) (y : Fin m → Bool) (r : OrderedPair m → Bool) {i : Fin m} (hi : i ≠ ℓ) : realOut x (tildeR ℓ x y r) i = y i

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.realOut_tildeR {m : ℕ} (ℓ : Fin m) (x : Fin m → Bool × Bool) (y : Fin m → Bool) (r : OrderedPair m → Bool) (hy : ∑ i : Fin m, y i = (∑ i : Fin m, (x i).1) * ∑ i : Fin m, (x i).2) : realOut x (tildeR ℓ x y r) = y

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.pivotParty {m : ℕ} [NeZero m] (I : Finset (Fin m)) : Fin m

Choose a pivot party outside I when I ≠ Finset.univ, or ⊤ when I = Finset.univ.

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.pivotParty_not_mem {m : ℕ} [NeZero m] {I : Finset (Fin m)} (hI : I ≠ Finset.univ) : pivotParty I ∉ I

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.extendIn {m : ℕ} (I : Finset (Fin m)) (xI : ↥I → Bool × Bool) (j : Fin m) : Bool × Bool

Extend coalition inputs xI : I → Bool × Bool by (0, 0) outside I.

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.extendOut {m : ℕ} (I : Finset (Fin m)) (yI : ↥I → Bool) (j : Fin m) : Bool

Extend coalition outputs yI : I → Bool by 0 outside I.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.extendIn_of_mem {m : ℕ} (I : Finset (Fin m)) (xI : ↥I → Bool × Bool) {j : Fin m} (hj : j ∈ I) : extendIn I xI j = xI ⟨j, hj⟩

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.extendOut_of_mem {m : ℕ} (I : Finset (Fin m)) (yI : ↥I → Bool) {j : Fin m} (hj : j ∈ I) : extendOut I yI j = yI ⟨j, hj⟩

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.extendIn_univ {m : ℕ} (x : Fin m → Bool × Bool) : extendIn Finset.univ (Finset.univ.restrict x) = x

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.extendOut_univ {m : ℕ} (y : Fin m → Bool) : extendOut Finset.univ (Finset.univ.restrict y) = y

def Cslib.Crypto.Protocols.MPC.MultiPartyMul.sigmaShift {m : ℕ} (I : Finset (Fin m)) (x : Fin m → Bool × Bool) (p : OrderedPair m) : Bool

Coin shift aligning matrixOfCoins x (r + sigmaShift I x) i with matrixOfCoins (extendIn I (I.restrict x)) r i for all i ∈ I.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.sigmaShift_univ {m : ℕ} (x : Fin m → Bool × Bool) : sigmaShift Finset.univ x = 0

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.matrixOfCoins_add_sigmaShift {m : ℕ} (I : Finset (Fin m)) (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) {i : Fin m} (hi : i ∈ I) (j : Fin m) : matrixOfCoins x (r + sigmaShift I x) i j = matrixOfCoins (extendIn I (I.restrict x)) r i j

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.realOut_add_sigmaShift {m : ℕ} (I : Finset (Fin m)) (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) {i : Fin m} (hi : i ∈ I) : realOut x (r + sigmaShift I x) i = realOut (extendIn I (I.restrict x)) r i

theorem Cslib.Crypto.Protocols.MPC.MultiPartyMul.matrixOfCoins_tildeR_add_sigmaShift {m : ℕ} [NeZero m] (I : Finset (Fin m)) (x : Fin m → Bool × Bool) (y : Fin m → Bool) (r : OrderedPair m → Bool) {i : Fin m} (hi : i ∈ I) : matrixOfCoins x (tildeR (pivotParty I) x y (r + sigmaShift I x)) i = matrixOfCoins (extendIn I (I.restrict x)) (tildeR (pivotParty I) (extendIn I (I.restrict x)) (extendOut I (I.restrict y)) r) i

noncomputable def Cslib.Crypto.Protocols.MPC.multiPartyMulSim (m : ℕ) [NeZero m] (I : Finset (Fin m)) : CoalitionSimulator (multiPartyMulSchedule m) (fun (x : Fin m) => Bool × Bool) (fun (x : Fin m) => Unit) (fun (x : Fin m) => Bool) I

Coalition simulator for multiPartyMulProtocol m (Goldreich Proposition 7.5.9, pp. 704–705).

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_multiPartyMul (m : ℕ) [NeZero m] : PerfectSemiHonestPrivate (multiPartyMulProtocol m) (sharedMulWorld 2) (sharedMulFunctionality m) (multiPartyMulSim m)

Proposition 7.5.9 (Goldreich Section 7.5.2.2, p. 704): multiPartyMulProtocol m privately reduces m-party shared multiplication sharedMulFunctionality m to 2-party shared multiplication sharedMulWorld 2 with perfect semi-honest security against all static coalitions I : Finset (Fin m).