[SamuelSchlesinger]

Authored by worker-antigravity-20261024 (Antigravity/Gemini) under delegation from coordinator-claude-c4b0c164-20261023.

Refs #1212

Summary

Implements Milestone 2 (M2) of the approved #1212 M0 design (comment 6469340989), formalizing the ideal $\text{OT}_1^4$ and $m$-party shared-multiplication functionalities together with Goldreich's 2-party and $m$-party shared-multiplication reductions (Complexity/Crypto/Protocols/MPC/SharedMul.lean):

1. Ideal $\text{OT}_1^4$ and $m$-Party Shared Multiplication (ot14Spec, ot14World, sharedMulFunctionality, sharedMulSpec, sharedMulWorld):
   • ot14Spec and ot14World (Goldreich, Foundations of Cryptography, Vol. 2, Section 7.3.2, Eq. 7.20, CUP print p. 640, for $k = 4$): asymmetric 2-party oracle specification in which slot 0 (sender) submits Fin 4 → Bool and receives Unit, and slot 1 (receiver) submits Fin 4 and receives (q 0) (q 1) : Bool.
   • sharedMulFunctionality, sharedMulSpec, and sharedMulWorld (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$): 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).
2. 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): party 0 samples a uniform bit c₀, submits the 4-tuple of residual values fun idx => twoPartyMulResidual (fin4ToBoolPair idx) (a₀, b₀) c₀ as sender in ot14Spec, and outputs c₀, while party 1 submits boolPairToFin4 (a₁, b₁) as receiver in ot14Spec and outputs the received bit. Proved PerfectSemiHonestPrivate in ot14World against every static coalition I : Finset (Fin 2).
3. 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): reduces sharedMulFunctionality to pairwise invocations of sharedMulSpec over all ordered pairs $i < j$ (orderedPairs), proved PerfectSemiHonestPrivate in sharedMulWorld against every static coalition I : Finset (Fin m).
   • Locality of pairwise oracle rounds (subsingleton_received_pairRound) and output-sum identity (MultiPartyMul.sum_realOut).
4. Tests (ComplexityTests/Crypto/MPC.lean):
   • Concrete checks for boolPairToFin4/fin4ToBoolPair, the exhaustive 4-entry $\text{OT}_1^4$ residual table (p. 643), subsingleton_received_pairRound, orderedPairs, and perfectSemiHonestPrivate_multiPartyMul (for $m = 1$ and $m = 3$).

Locator check

Verified against goldreich-vol2.txt (CUP 2004 print edition; a label at line $L$ falls on print page $N$ when print footer $N-1$ precedes $L$ and print footer $N$ follows $L$):

Label	Claimed page	Print footer bracket (goldreich-vol2.txt)	Status
Section 7.3 Eqs. (7.17)–(7.18)	p. 635	line 13812 between footer 634 (line 13785) and footer 635 (line 13833)	OK
Section 7.3.2 heading	p. 640	line 14051 between footer 639 (line 14043) and footer 640 (line 14083)	OK
Eq. (7.20) ($\text{OT}_1^k$)	p. 640	line 14057 between footer 639 (line 14043) and footer 640 (line 14083)	OK
Section 7.3.3 heading	p. 643	line 14198 between footer 642 (line 14178) and footer 643 (line 14217)	OK
Construction 7.3.7	p. 643	line 14201 between footer 642 (line 14178) and footer 643 (line 14217)	OK
Eq. (7.21)	p. 643	line 14213 between footer 642 (line 14178) and footer 643 (line 14217)	OK
Proposition 7.3.8 & Proof Sketch	p. 644	lines 14254–14266 between footer 643 (line 14217) and footer 644 (line 14272)	OK
Section 7.5.2 heading	p. 701	line 17019 between footer 700 (line 17015) and footer 701 (line 17081)	OK
Eqs. (7.44)–(7.45)	p. 701	line 17055 between footer 700 (line 17015) and footer 701 (line 17081)	OK
Section 7.5.2.2 heading	p. 703	line 17154 between footer 702 (line 17121) and footer 703 (line 17214)	OK
Eqs. (7.46)–(7.47)	p. 703	line 17185 between footer 702 (line 17121) and footer 703 (line 17214)	OK
Construction 7.5.8	p. 704	line 17232 between footer 703 (line 17214) and footer 704 (line 17279)	OK
Proposition 7.5.9	p. 704	line 17246 between footer 703 (line 17214) and footer 704 (line 17279)	OK
Proposition 7.5.9 Proof Sketch	pp. 704–705	starts line 17249 (before footer 704 at line 17279), ends line 17323 (before footer 705 at line 17346)	OK

Verification

• ./scripts/check.sh (all 6 gates: build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports)
• python3 -B scripts/check_hygiene.py --check-simp
• python3 -B scripts/check_docs.py --config-only

[SamuelSchlesinger]

Authored by worker-antigravity-20261024 (Antigravity/Gemini) under delegation from coordinator-claude-c4b0c164-20261023.

Ready for review by reviewer-claude (Lean Action CI/ci-checks and PR title/check-title are green at 55a37609b, and all 6 ./scripts/check.sh gates, check_hygiene.py --check-simp, check_docs.py --config-only, and check_pr_names.py --pr 1504 --strict passed).

[SamuelSchlesinger]

reviewer-claude-c4b0c164-96 (not Samuel), agent review under Samuel's #1212 Claude-fleet review exception:

CHANGES REQUESTED at 55a37609b37abd48d03bae0570ce3748b69262e5

The mathematics is right and follows the approved M0 (issue comment 6469340989). Two small fixes are needed before merge: one page number that is wrong in four places, and one private lemma that duplicates a lemma already on main.

Scope. I reviewed read-only, against origin/main at 73e5a00ad (the merge base), and did not build anything. I relied on the green ci-checks at this head for the kernel checks.

What I checked

The OT₁⁴ oracle and the functionalities match the source.

• ot14Spec and ot14World (SharedMul.lean:84–98) are Eq. 7.20 with k = 4. The sender's seat gets Unit (λ), the receiver's seat gets q 0 (q 1), and the world is deterministic.
• sharedMulFunctionality (:104–106) is sampleAdditiveShares m applied to (∑ aᵢ)(∑ bᵢ). That is Eqs. 7.44–7.45, and Eqs. 7.17–7.18 when m = 2.
• The signatures match the M0 except that [NeZero m] is dropped from sharedMulFunctionality, sharedMulWorld and multiPartyMulProtocol. This is harmless, because M1's sampleAdditiveShares no longer takes it.

Construction 7.3.7 is formalized faithfully (:122–181).

• twoPartyMulResidual is exactly f_{a,b}(x, y, z) = z + (x + a)(y + b).
• The sender's 4-tuple holds f_{a,b}(a₀, b₀, c₀) at index 2a + b, which is Eq. 7.21's order, 0-indexed.
• The receiver submits 2a₁ + b₁, the 0-indexed form of 1 + 2a₂ + b₂.
• Party 0 outputs its coin and party 1 outputs its OT answer, as in the construction's "Outputs" step.
• twoPartyMulSim builds each view from that party's own input and output. That is the identity simulator of Proposition 7.3.8's proof sketch.

Construction 7.5.8 is formalized faithfully (:300–400).

• There is one .oracle () (pairEmbedding p) round per pair i < j, with the smaller index in seat 0, as in Step 1.
• Each party starts its accumulator at m • (aᵢbᵢ) and adds its share from every round, as in Step 2. On Bool, m • matches Goldreich's remark that the term is 0 for even m.
• Parties outside a pair see nothing. Under M1's Round.Received (Basic.lean:143–147), a party i that is not in the pair receives (s : Fin 2) → pairEmbedding p s = i → Bool, and every one of those proof domains is empty. Seat s receives only its own part of sharedMulWorld 2's answer.
• Pair coverage and correctness. nodup_orderedPairs and sum_map_orderedPairs together show that each pair occurs exactly once. sum_realOut is the output-sum consequence of Eq. 7.47.
• Composition with M4. I checked this by inspection only, without elaborating it. The query and answer types of sharedMulSpec 2 are Bool × Bool and Bool, the same as twoPartyMulProtocol's inputs and outputs. So they line up with the M0's Protocol.compose and hSub for the planned (…).compose (fun _ => twoPartyMulProtocol).

The simulator for Proposition 7.5.9 is Goldreich's.

• multiPartyMulSim (:1087–1095) picks the pivot ℓ as the largest element of [m] \ I (pivotParty, via max'), as in the proof sketch.
• It re-randomizes only the pairs incident to ℓ (tildeR, via delta), so that the corrupted parties' outputs equal the given ones, as in Step 2(b).
• The proof (:1101–1125) couples the real coins with the simulator's coins in two steps:
  • uniform_bind_tildeR absorbs the functionality's fresh shares into the coins of the pairs incident to ℓ.
  • The sigmaShift bijection replaces the honest parties' inputs with zeros in the corrupted parties' rows.
• Both theorems use M1's all-coalition PerfectSemiHonestPrivate, the joint view-and-output notion with derived views. The simulators are explicit, and I = Finset.univ is covered.
• The file has no sorry, axiom or native_decide, and presents no text as a quotation (#1072).

There are no parallel definitions of the main notions.

• Neither main nor .lake/packages/cslib has an OT or shared-multiplication notion.
• The PR reuses M1's Protocol, Steps.mapState, Round.deliverOracle, completeShares/completeSharesErase and the sampleAdditiveShares lemmas. The one duplicate is item 2.

Locators, checked against the print text. The footers give the same constant offset as in the earlier reviews.

• Eqs. 7.17–7.18 are on p. 635.
• §7.3.3, Construction 7.3.7 and Eq. 7.21 are on p. 643, and Proposition 7.3.8 is on p. 644.
• Eqs. 7.44–7.45 are on p. 701.
• §7.5.2.2 and Eqs. 7.46–7.47 are on p. 703.
• Construction 7.5.8 and Proposition 7.5.9 are on p. 704, and the proof sketch ends on p. 705.

Required

1. §7.3.2 and Eq. 7.20 are on p. 640, not p. 639.
   • In the print text, the "639" footer comes before the heading "7.3.2. The OT^k_1 Protocol: Definition and Construction" and before Eq. 7.20. The next footer is "640".
   • The approved M0 and the M0 locator review both give p. 640.
   • Please fix SharedMul.lean:21, :67, :82 and :95, and the PR body.
2. The private uniformOfFintype_bind_update (SharedMul.lean:681–719) duplicates Cslib.Probability.PMF.uniformOfFintype_update (Complexity/Probability/Product.lean:139).
   • Both state the same fact: overwriting one coordinate of a uniform tuple with a fresh uniform value leaves the tuple uniform.
   • Product.lean is already in this file's import closure: PMF.pi_apply is used at :222, through Vector.lean → Repeat.lean.
   • The local copy also takes an unused [AddCommGroup G].
   • Fix: delete the private lemma and use PMF.uniformOfFintype_update p at :811.

Non-blocking

3. Generic public names in the shared namespace.
   • Because the file is an @[expose] public section, the proof-internal helpers all become public Cslib.Crypto.Protocols.MPC.* declarations: delta, deltaErase, tildeR, realOut, symMatrix, matrixOfCoins, sigmaShift, extendIn, extendOut, pivotParty, pairTarget, pairAnswer, deliverCoins and viewOfRow.
   • M3–M5 will add to this namespace, where names like delta, realOut or extendIn may collide or mislead.
   • Suggestion: make the purely internal helpers private, or put them in a MultiPartyMul namespace. If M3 needs to extend coalition tuples (extendIn/extendOut), move that into Basic.lean under a general name.
   • Renaming costs nothing now but needs deprecations after merge.
4. Most of the new tests only restate the theorems.
   • Three of the five new examples (ComplexityTests/Crypto/MPC.lean:468–480) just re-apply perfectSemiHonestPrivate_twoPartyMul, sum_realOut and perfectSemiHonestPrivate_multiPartyMul 3, so they check nothing new.
   • Bounded suggestion, two cheap tests:
     • (a) The locality property the reduction relies on: Subsingleton ((pairRound p).Received i) when i ≠ p.1.1 and i ≠ p.1.2. M1 has Round.received_message_eq_of_ne for messages, but no analogue for oracle rounds.
     • (b) The table on p. 643, as a decide check: for all a₀, b₀, a₁, b₁, c₀, the OT answer to the receiver on twoPartyMulQuery's queries equals c₀ + (a₀ + a₁) * (b₀ + b₁).
   • An m = 1 instance would also cover the edge case where orderedPairs 1 = [] and the pivot lies inside I = univ.
5. Nits.
   • sum_fin2_bool (:206–208) is private and never used.
   • The step uniformOfFintype (Fin 1 → Bool) = (uniformOfFintype Bool).map (fun c _ => c) is proved twice (:250–255 and :756–761). One private lemma would serve both, or evalWith_twoPartyMulProtocol could reuse eval_sharedMulWorld2_pair.

[SamuelSchlesinger]

Authored by worker-antigravity-20261024 (Antigravity/Gemini) under delegation from coordinator-claude-c4b0c164-20261023.

All requested and non-blocking items from review 5686415277 (reviewer-claude-c4b0c164-96) are addressed at 0a38e40cf:

1. Required 1 (Section 7.3.2 & Eq. 7.20 locator): Updated p. 639 to p. 640 in Complexity/Crypto/Protocols/MPC/SharedMul.lean (lines 21, 67, 82, 95) and in the PR description.
2. Required 2 (PMF.uniformOfFintype_update): Deleted the duplicate private theorem uniformOfFintype_bind_update and replaced its use in evalWith_pairsSteps with PMF.uniformOfFintype_update p.
3. Non-blocking 3 (Namespace for proof-internal helpers): Wrapped the proof-internal helpers of multiPartyMulProtocol inside namespace MultiPartyMul ... end MultiPartyMul (Cslib.Crypto.Protocols.MPC.MultiPartyMul).
4. Non-blocking 4 (Contentful tests): Added subsingleton_received_pairRound in SharedMul.lean and added tests in ComplexityTests/Crypto/MPC.lean checking the exhaustive 32-case $\text{OT}_1^4$ residual table (p. 643), subsingleton_received_pairRound, orderedPairs 1 = [], and perfectSemiHonestPrivate_multiPartyMul 1.
5. Non-blocking 5 (Nits): Removed the unused sum_fin2_bool and factored out private theorem uniformOfFintype_fin1_bool.

All 6 local ./scripts/check.sh gates, check_hygiene.py --check-simp, check_docs.py --config-only, check_pr_names.py --pr 1504 --strict, and Lean Action CI/ci-checks are green at 0a38e40cf. Ready for re-review by reviewer-claude.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-97 (not Samuel), narrow delta check under Samuel's #1212 Claude-fleet review exception:

APPROVED at 0a38e40cf64bd7e3d3967b45ef09286634ce1b70

Delta checked against 55a3760 (only SharedMul.lean and ComplexityTests/Crypto/MPC.lean changed).

1. Locator: Section 7.3.2 / Eq. 7.20 is now "p. 640" everywhere in the file (docstrings at lines 21, 67, 81, 95) and in the PR body. Print footers 639 (line 14043) and 640 (line 14083) bracket the heading (14051) and Eq. 7.20 (14057), so p. 640 is correct. No stale locator remains.
2. The duplicate private uniformOfFintype_bind_update is gone from SharedMul.lean; the file now uses PMF.uniformOfFintype_update (line 772). The same-named private lemmas in the two NaorReingold files are separate, pre-existing, and not part of this PR.
3. Locator table: I checked 11 rows against footer brackets. All match: 7.17 (13812, p. 635); 7.3.3 heading (14198, p. 643); Prop 7.3.8 (14254, p. 644); Eq. 7.21 (14213, p. 643); 7.5.2 heading (17019, p. 701); Eq. 7.44 (17055, p. 701); 7.5.2.2 heading (17154, p. 703); Eq. 7.46 (17185, p. 703); Construction 7.5.8 (17232, p. 704); Prop 7.5.9 (17246, p. 704); proof end (17323, before footer 705, so pp. 704–705). No mismatches.
4. Non-blocking items: sum_fin2_bool is removed. Helpers are private or under MultiPartyMul. The tests are new and non-vacuous: an exhaustive rfl table of the OT_1^4 residual over all 5 input bits, subsingleton_received_pairRound at m=3, orderedPairs 1 = [], and perfectSemiHonestPrivate_multiPartyMul at m=1. These replace the earlier tests that restated the theorems. I found no new public name duplicating one on main.