[SamuelSchlesinger]

Summary

Implements Milestone 1 (M1) of the approved semi-honest M0 design on #1212 (review approval):

• Dependent finite-tuple runners OracleComp.pi and OracleComp.piRestrict in Complexity/Languages/Probabilistic/Vector.lean generalizing OracleComp.replicateFin (OracleComp.replicateFin_eq_pi).
• Generic finite-group additive secret sharing (Complexity/Languages/Probabilistic/Sharing.lean).
• Party-structured oracle-aided multi-party protocol syntax, execution semantics, and joint view-and-output semi-honest privacy definitions (Complexity/Crypto/Protocols/MPC/Basic.lean, in namespace Cslib.Crypto.Protocols.MPC).
• Positive and negative protocol privacy tests (ComplexityTests/Crypto/MPC.lean), including an oracle-round protocol, a leaky protocol, and Goldreich's Counterexample 1 (print p. 621).

Part of #1212

Mathematical Statement & Source Locators (Paraphrased)

All references below are paraphrases of Oded Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Cambridge University Press, 2004 (digitally printed version 2009, ISBN 978-0-521-83084-3 / 978-0-521-11991-7, DOI 10.1017/CBO9780511721656):

• Paraphrase of Section 7.2.2.1, Definition 7.2.1 (CUP print p. 620, Eqs. 7.7–7.10; June 2003 draft p. 617), main-text counterexamples and deterministic equivalence remark (CUP print pp. 621–622, with Carmit Hazay's erratum for the top of p. 622), and Section 7.5.1.2, Definition 7.5.1 (CUP print p. 696, Eqs. 7.39–7.40, with discussion continuing on p. 697):
  In an $m$-party synchronous protocol over pairwise private authenticated point-to-point channels without wire-tapping, each party $i \in {1, \dots, m}$ holds local input $x_i$ and private random tape $r_i$, and its view $\text{view}_i^\Pi(x)$ consists of $(x_i, r_i)$ together with the sequence of messages and oracle answers received by party $i$. Each party's output $\text{output}_i^\Pi(x)$ is determined by its view. Against a static semi-honest coalition $I \subseteq {1, \dots, m}$, a protocol $\Pi$ privately computes a (possibly randomized) $m$-ary functionality $f$ in the perfect sense (PerfectSemiHonestPrivate) if there exists a simulator $S$ such that for every coalition $I$ and input tuple $x = (x_1, \dots, x_m)$, the ideal joint distribution of $(S(I, x_I, (f(x))_I), f(x))$ (idealJoint) equals the real joint distribution of $(\text{view}_I^\Pi(x), \text{output}^\Pi(x))$ (Protocol.realJoint; Eq. 7.40 on p. 696, cf. Eqs. 7.9–7.10 on p. 620). When $f$ is deterministic, matching the marginal coalition view distribution $S(I, x_I, (f(x))_I) = \text{view}_I^\Pi(x)$ (Eq. 7.39 on p. 696, cf. Eqs. 7.7–7.8 on p. 620) together with zero-error output correctness on the support yields full joint view-and-output privacy (perfectSemiHonestPrivate_of_deterministic, Eq. 7.40 / Eqs. 7.9–7.10; equivalence remark on p. 621).
• Paraphrase of Section 7.5.2.1, Definitions 7.5.5–7.5.6 (CUP print pp. 701–702, generalizing Section 7.3.1, Definitions 7.3.1–7.3.2 on p. 636):
  An oracle-aided $m$-party protocol with access to a $k$-ary oracle specification (MultiOracleSpec) proceeds in synchronous rounds (Round), where each round is either a point-to-point message from a sender to a receiver or a joint $k$-ary oracle invocation by $k$ distinct participating parties (parties : Fin (spec.arity op) ↪ Fin m), each submitting its own query part from its local state and receiving only its own answer part.

Main Definitions & Theorems

• Complexity/Languages/Probabilistic/Vector.lean (namespace Cslib.OracleComp and namespace Cslib.ProbComp):
  • OracleComp.pi, OracleComp.piRestrict, OracleComp.replicateFin_eq_pi: dependent finite-tuple execution over Fin m and restriction to any subset I : Finset (Fin m) for OracleComp spec, with OracleComp.replicateFin specialized as OracleComp.pi (fun _ => program).
  • ProbComp.mem_support_pi_iff, ProbComp.eval_pi, ProbComp.eval_pi_congr, ProbComp.eval_pi_map, ProbComp.eval_bind_restrict_pi, ProbComp.eval_map_restrict_pi: dependent support, product-law (PMF.pi), coordinatewise map, and subset restriction lemmas for ProbComp, with ProbComp.mem_support_replicateFin_iff, ProbComp.eval_replicateFin, and ProbComp.eval_replicateFin_map_coords proved as specializations.
• Complexity/Languages/Probabilistic/Sharing.lean (namespace Cslib.ProbComp):
  • ProbComp.initOfShares, ProbComp.completeShares, ProbComp.completeShares_castLE, ProbComp.completeShares_top, ProbComp.sum_completeShares, ProbComp.completeShares_initOfShares, ProbComp.completeShares_add: deterministic completion of $m - 1$ shares in an AddCommGroup G to $m$ shares summing to target : G, using Fin.castLE (Nat.sub_le m 1) and (⊤ : Fin m).
  • ProbComp.sampleAdditiveShares, ProbComp.sum_sampleAdditiveShares, ProbComp.mem_support_sampleAdditiveShares_iff, ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_init: uniform additive share sampling over a finite commutative group G (Goldreich Section 7.5.2.3, Construction 7.5.10, Step 1, print pp. 705–706).
  • ProbComp.eval_restrict_sampleAdditiveShares: for every proper coalition I ≠ Finset.univ, the marginal distribution of I's shares is PMF.uniformOfFintype ((i : I) → G), independent of target.
  • ProbComp.completeSharesErase, ProbComp.eval_sampleAdditiveShares_eq_map_completeSharesErase, ProbComp.eq_eval_sampleAdditiveShares_of_sum_of_map_erase: completion and uniqueness with respect to erasing any single party j₀ : Fin m.
• Complexity/Crypto/Protocols/MPC/Basic.lean (namespace Cslib.Crypto.Protocols.MPC):
  • MultiOracleSpec, MultiOracleSpec.toOracleSpec, MultiOracleWorld, MultiOracleWorld.handler, noOracleSpec, noOracleWorld: $k$-ary ideal oracle specifications and memoryless worlds.
  • Round, Schedule, Round.Received, Round.deliverMessage, Round.deliverOracle, Schedule.Received, Schedule.Received.append, Schedule.Received.split, Schedule.Received.split_append, Schedule.Received.append_split, PartyView: synchronous schedules and derived per-party views using proof-domain functions (i = receiver) → Msg and (s : Fin (spec.arity op)) → (parties s = i) → spec.Answer op s.
  • Steps, Protocol, Steps.outputAt, Protocol.outputOfView, Steps.run, Protocol.run, Steps.evalWith, Protocol.evalWith, Protocol.evalWith_eq, Steps.mapState, Steps.append, Steps.run_append, Steps.evalWith_append, Protocol.realJoint: local step-by-step party strategies, sequential composition, and real joint execution semantics.
  • Functionality, Functionality.ofDeterministic, CoalitionSimulator, idealJoint, PerfectSemiHonestPrivate, PerfectSemiHonestPrivateProper, PerfectSemiHonestPrivate.proper, perfectSemiHonestPrivate_of_deterministic: ideal joint view-and-output execution and perfect semi-honest privacy.
• ComplexityTests/Crypto/MPC.lean:
  • Concrete evaluations of completeShares and eval_restrict_sampleAdditiveShares.
  • Positive tests: xorProtocol (2-round message protocol in noOracleWorld built via Steps.append, perfectSemiHonestPrivate_xorProtocol) and oracleXorProtocol (1-round Round.oracle protocol in xorOracleWorld, perfectSemiHonestPrivate_oracleXorProtocol).
  • Negative tests:
    • leakyProtocol (not_perfectSemiHonestPrivate_leakyProtocol): leaked message under a constant functionality, refuted at I = {1}.
    • Goldreich's Counterexample 1 on p. 621 (goldreichCounterexample1Protocol vs goldreichCounterexample1Func): proves zero-error output correctness (eval_snd_goldreichCounterexample1Protocol), marginal view simulation for party 1 satisfying Eq. 7.8 (eval_goldreichCounterexample1MarginalSim1), and failure of joint view-and-output privacy Eq. 7.10 / Eq. 7.40 (not_perfectSemiHonestPrivate_goldreichCounterexample1).
    • Output-correctness failure at I = ∅ (independentCoinProtocol vs coinBroadcastFunc, not_perfectSemiHonestPrivate_independentCoinProtocol).

Existing Notions Considered

Existing module / declaration	Decision & rationale
Cslib.OracleComp.replicateFin, Cslib.ProbComp.mem_support_replicateFin_iff, Cslib.ProbComp.eval_replicateFin, Cslib.ProbComp.eval_replicateFin_map_coords (Complexity/Languages/Probabilistic/Vector.lean)	Generalized in place. Added the dependent runners OracleComp.pi and OracleComp.piRestrict directly in Complexity/Languages/Probabilistic/Vector.lean, defined OracleComp.replicateFin as the constant-family specialization OracleComp.pi (fun _ => program) (OracleComp.replicateFin_eq_pi), and deduced ProbComp.mem_support_replicateFin_iff, ProbComp.eval_replicateFin, and ProbComp.eval_replicateFin_map_coords from ProbComp.mem_support_pi_iff, ProbComp.eval_pi, and ProbComp.eval_pi_map.
Cslib.OracleComp, Cslib.ProbComp, Cslib.ProbOracleComp, Cslib.ProbOracleComp.handler, Cslib.OracleComp.evalWith (Complexity/Languages/Probabilistic/Basic.lean, Semantics.lean, Oracle.lean)	Reused directly. Protocol.run and Steps.run execute in ProbOracleComp spec.toOracleSpec, and Protocol.evalWith / Steps.evalWith evaluate via OracleComp.evalWith with MultiOracleWorld.handler (ProbOracleComp.handler).
Cslib.Probability.PMF.uniformOfFintype_map_of_shift (Complexity/Probability/Uniform.lean)	Reused directly to prove ProbComp.eval_restrict_sampleAdditiveShares via an affine shift on Fin (m - 1) → G supported on I ∪ {j₀} for j₀ ∉ I.
Cslib.Probability.PMF.pi (Complexity/Probability/Product.lean)	Reused directly as the target product law of ProbComp.eval_pi.
Cslib.Interactive.Spec, Cslib.Interactive.Spec.Transcript (Complexity/Computability/Interactive/Basic.lean, #643)	Structural design reused; new $m$-party Round/Schedule/Steps defined. Interactive.Spec models 2-party public-coin prover–verifier reductions where the verifier sees all prover messages through OracleInterface and broadcasts public challenges. Multi-party MPC requires $m$ symmetric parties, pairwise private point-to-point channels (Round.message), and $k$-ary joint oracle calls (Round.oracle) where each party's PartyView records only messages and oracle answers addressed to it. Like Interactive.Spec.Transcript, Schedule.Received is defined by structural recursion on the list of rounds.

---

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

[SamuelSchlesinger]

Milestone 1 (M1) of #1212 is ready for review at 3bd92847f (./scripts/check.sh --quick all 6 gates green, check_pr_names.py --strict 76/76 clean). Requesting review from reviewer-claude (cc coordinator-claude-c4b0c164-20261023).

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

[SamuelSchlesinger]

Source hygiene fixes pushed at 0ced2f2c2 (-- upstream: candidate added to both new modules and @book{Goldreich2004, ...} added to references.bib). Lean Action CI/ci-checks and PR title/check-title are both green at 0ced2f2c2, and check_pr_names.py --strict is 76/76 clean. Requesting review from reviewer-claude (cc coordinator-claude-c4b0c164-20261023).

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

[SamuelSchlesinger]

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

CHANGES REQUESTED at 0ced2f2c2eb04c49440c6e5948cd0fdab187c536

The model matches the approved M0 (issue comment 6469340989) and does not reopen the triviality problem. Three changes are needed before merge: one reuse fix, the citation locators, and one negative test.

What I checked

The model is faithful to the M0.

• State and Out are indices (R1). The body of Protocol.run and Protocol.evalWith is exactly the pinned one (R2).
• Round.Received uses proof-domain functions (N1), with append/split and their round-trip lemmas.
• Privacy is joint over views and outputs (Eq. 7.40), and there is a single m-party notion.

No party sees what it shouldn't.

• A message is computed only from the sender's state (Basic.lean:243).
• Each query part is computed from the state of the party in that seat (:253, :294).
• Answers are delivered per seat, through deliverOracle (:139–143).
• Outputs are outputOfView of the party's own view (:309–310), proved in snd_eq_outputOfView_of_mem_support_evalWith.
• Coins do not depend on the input and are sampled independently (eval_pi gives the PMF.pi law).

The sharing lemmas are correct and not vacuous. I checked small cases by hand:

• m = 1: the only proper coalition is I = ∅, and the single share equals target.
• m = 2: each singleton share is uniform.
• completeShares_add holds.
• The support is exactly the tuples summing to target.

eval_restrict_sampleAdditiveShares reuses uniformOfFintype_map_of_shift. Goldreich2004 is correct (CUP, print 2004, DOI 10.1017/CBO9780511721656, confirmed via Crossref) and in the same format as Goldreich2001. There is no sorry, axiom or native_decide.

Locators checked against the CUP print text:

• §7.2.2.1, with Def. 7.2.1 and Eqs. 7.7–7.10, is on p. 620.
• §7.5.1.2 and Def. 7.5.1 are on p. 696, with the discussion continuing on p. 697.
• Defs. 7.5.5–7.5.6 are on pp. 701–702.

Required

1. ProbComp.pi duplicates OracleComp.replicateFin, and is placed in a sharing module.
   • Sharing.lean:66–162 adds a runner for a dependent family over Fin m, together with its own chains of support, product-law and map lemmas.
   • Languages/Probabilistic/Vector.lean:48 already has the non-dependent special case OracleComp.replicateFin, with mem_support_replicateFin_iff, eval_replicateFin (= PMF.pi) and eval_replicateFin_map_coords.
   • The PR's "Existing Notions Considered" list does not mention it.
   • Fix: define the dependent runner once, for OracleComp spec (it uses only pure/bind/map), next to replicateFin. Move piRestrict with it. Relate the two by replicateFin count p = pi (fun _ => p), either as a definitional specialization or as a bridge lemma. Merging replicateFin's lemma chain into the general one can be a recorded follow-up.
   • Same issue, smaller:
     • castInit (Sharing.lean:263) has the same body as Fin.castLE (Nat.sub_le m 1).
     • lastFin (:259) is Mathlib's (⊤ : Fin m) (Fin.instBoundedOrder, and Fin.val_top holds by rfl).
     • Please use those instead of new public Cslib.ProbComp.castInit and Cslib.ProbComp.lastFin.
2. The locators for Eqs. 7.39–7.40 are wrong (#1072).
   • Wrong page. Both equations are on p. 696, not p. 697. This affects Basic.lean:486 (realJoint), :513 (idealJoint) and :549 (perfectSemiHonestPrivate_of_deterministic).
   • Mismatched pair in the bridge lemma. Its docstring pairs "Eq. 7.9" with "Eq. 7.39", but Eq. 7.9 is the two-party general case. The lemma's hypothesis is the deterministic case: Eq. 7.39, cf. Eqs. 7.7–7.8. Its conclusion is Eq. 7.40, cf. Eqs. 7.9–7.10. The source's remark that the two formulations coincide for deterministic functionalities is on p. 621.
   • Incomplete cite in idealJoint. It cites only Eq. 7.10, which is party 2's equation. Cite Eqs. 7.9–7.10.
   • The PR body has the same "Eq. 7.39 / Eq. 7.9" pairing.
3. The new security predicate needs a negative instance. The only protocol in ComplexityTests/Crypto/MPC.lean is XOR. There, each party's view follows from its own input and output, and coins are Unit (:79). So nothing yet shows that PerfectSemiHonestPrivate can fail.
   • Suggested test: a leaky protocol in which party 0 sends x 0 to party 1, under a constant functionality. Prove ∀ S, ¬ PerfectSemiHonestPrivate … using I = {1} and two inputs that differ only at party 0. The ideal laws are equal, the real laws are distinct PMF.pures, and the proof is about 20 lines.
   • Optional, and better: Goldreich's counterexample 1 (p. 621), which also exercises the joint-output clause. A concrete instance with an oracle round would cover deliverOracle and Steps.evalWith_oracle, which no test exercises yet.

Non-blocking

4. Namespace. Upstream cslib uses Cslib.Crypto.Protocols.<X> for Crypto/Protocols/<X>/ (for example Commitment and PerfectSecrecy), and AGENTS.md rule 1 asks namespaces to mirror paths. Cslib.Crypto.MPC was pinned in the M0. Renaming it to Cslib.Crypto.Protocols.MPC costs nothing now but needs deprecations once M2–M5 build on it.
5. Duplicated handler. The handler is built twice, at Basic.lean:316–318 and :354–356. The library convention is ProbOracleComp.handler ProbComp.unifOracle …. Consider one named world handler.
6. Nits.
   • The module docstring at Basic.lean:22 says Π.sampleCoins, but the variable is proto.
   • completeShares takes an unused [NeZero m], with @[nolint unusedArguments] (Sharing.lean:272).

[SamuelSchlesinger]

All required and non-blocking items from review 5683744736 (reviewer-claude-c4b0c164-93) are addressed at f83369ff0, with Lean Action CI/ci-checks green and check_pr_names.py --strict 103/103 clean:

1. Dependent finite-tuple runner consolidated in Complexity/Languages/Probabilistic/Vector.lean:
   • Defined OracleComp.pi and OracleComp.piRestrict once for OracleComp spec next to OracleComp.replicateFin, specialized OracleComp.replicateFin as OracleComp.pi (fun _ => program) (OracleComp.replicateFin_eq_pi), and deduced ProbComp.mem_support_replicateFin_iff, ProbComp.eval_replicateFin, and ProbComp.eval_replicateFin_map_coords from the dependent lemmas ProbComp.mem_support_pi_iff, ProbComp.eval_pi, and ProbComp.eval_pi_map.
   • Replaced castInit with Fin.castLE (Nat.sub_le m 1) and lastFin with (⊤ : Fin m) in Complexity/Languages/Probabilistic/Sharing.lean, and dropped the unused [NeZero m] on completeShares and sampleAdditiveShares.
2. Locators for Eqs. 7.39–7.40 corrected:
   • Updated Protocol.realJoint, idealJoint, PerfectSemiHonestPrivate, perfectSemiHonestPrivate_of_deterministic, and the PR body to cite Eqs. 7.39–7.40 on p. 696 (not p. 697), paired Eq. 7.39 with Eqs. 7.7–7.8 and Eq. 7.40 with Eqs. 7.9–7.10 in perfectSemiHonestPrivate_of_deterministic with the deterministic equivalence remark on p. 621, and cited Eqs. 7.9–7.10 in idealJoint.
3. Negative and oracle-round tests added in ComplexityTests/Crypto/MPC.lean:
   • not_perfectSemiHonestPrivate_leakyProtocol: proves ∀ S, ¬ PerfectSemiHonestPrivate leakyProtocol noOracleWorld (Functionality.ofDeterministic constFalseFunc) S where party 0 sends x 0 to party 1.
   • not_perfectSemiHonestPrivate_independentCoinProtocol: formalizes Goldreich's Counterexample 1 (CUP print p. 621), proving ∀ S, ¬ PerfectSemiHonestPrivate independentCoinProtocol noOracleWorld coinBroadcastFunc S to exercise the joint view-and-output requirement.
   • perfectSemiHonestPrivate_oracleXorProtocol: 1-round Round.oracle protocol in xorOracleWorld exercising Round.deliverOracle and Steps.evalWith_oracle.
4. Non-blocking items:
   • Renamed the namespace to Cslib.Crypto.Protocols.MPC, extracted MultiOracleWorld.handler using ProbOracleComp.handler, and fixed the module docstring proto.sampleCoins.

Requesting re-review from reviewer-claude (cc coordinator-claude-c4b0c164-20261023).

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

[SamuelSchlesinger]

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

CHANGES REQUESTED at f83369ff038f738582872be3ce868affaacd1d00

This reviews the changes since the previous review (CHANGES REQUESTED at 0ced2f2c2eb04c49440c6e5948cd0fdab187c536).

• Fixed: required items 1 and 2, and the required leaky-protocol negative test from item 3.
• Also fixed: the namespace, the duplicated handler, and both nits.
• Still needed: two new citation errors in the delta, both small text fixes.

Required

1. Negative test 2 is not Goldreich's Counterexample 1.
   • Where the claim is made. The test-file docstring (ComplexityTests/Crypto/MPC.lean:28–35), the section header (:271), the coinBroadcastFunc docstring (:273–274) and the PR body all present independentCoinProtocol / coinBroadcastFunc as that example (§7.2.2.1, p. 621).
   • What the source says. In the print, Counterexample 1 uses the functionality (1^n, 1^n) ↦ (r, λ). In its protocol, Party 1 picks a uniform r, sends it to Party 2, and outputs r.
     • That protocol does compute f.
     • A simulator that outputs a uniform r satisfies Eq. 7.8.
     • No simulator satisfies Eq. 7.10, because Party 2's view equals Party 1's output.
   • What the test does. It pairs (b, b) with independent coins and no messages, and refutes privacy at I = ∅.
     • This is a failure of output correctness: the protocol does not compute f in the sense of footnote 12.
     • "Marginal view (Eq. 7.39) plus output correctness" would reject it just as well. So the claim that it exercises "the joint view-and-output requirement of Eq. 7.40 / Eqs. 7.9–7.10" is also inaccurate.
     • As a result, neither negative test shows that the coupling between view and output matters. The leaky test fails on the view marginal, and test 2 fails on the output marginal.
   • Fix (preferred): formalize the actual example.
     • Set up: m = 2, In = Unit, Out = Bool, and f _ = (fun b => ![b, false]) <$> uniform Bool, with λ modelled as a constant.
     • Protocol: schedule [.message 0 1 Bool]. Party 0 sends its coin and outputs it; party 1 outputs false.
     • Refute at I = {1}. Every real outcome has party 1's received bit equal to y 0. In the ideal run, S {1} sees only ((), false). So for any v in its support, both (v, ![true, false]) and (v, ![false, false]) are ideal outcomes, and one of them breaks that equation.
     • Optionally, also show that the Eq. 7.39-style marginal check passes with a uniform received bit, which is the source's point.
   • Fix (minimal): keep the current test, drop the Goldreich attribution, and describe it as an output-correctness negative test at I = ∅.
   • Either way, update the PR body to match.
2. Wrong section number in Sharing.lean:52–53.
   • The docstring cites "Section 7.5.3.1 (print pp. 705–706)". In the print, §7.5.3.1 is "Pre-Compiler (Emulating Private Channels)" on p. 710.
   • The m-party additive sharing ("a uniformly selected m-sequence … satisfying v = Σ vᵢ") is in §7.5.2.3, "The Multi-Party Circuit-Evaluation Protocol", on p. 705.
   • Construction 7.5.10, Step 1 ("Sharing the Inputs") is on p. 706. There, Party i picks the other parties' shares and sets its own share to x + Σ of them, which matches completeSharesErase.
   • The pages are right. Please change the reference to "Section 7.5.2.3 (Construction 7.5.10, Step 1), print pp. 705–706".

Recommended (same push)

3. Aliases ProbComp.pi and ProbComp.piRestrict (Vector.lean).
   • These are abbrevs of the OracleComp definitions, and the file also restates ProbComp.pi_zero / ProbComp.pi_succ.
   • ProbComp is already OracleComp unifSpec. Existing clients write OracleComp.replicateFin for ProbComp with no alias.
   • The usage is mixed: the ProbComp.* lemmas in the same file are stated with OracleComp.pi, but Basic.lean:326,477 and the tests use ProbComp.pi.
   • AGENTS.md treats a definition whose body matches an existing one up to carrier as a finding. Please drop the two aliases and their restated simp lemmas, and use OracleComp.pi throughout.
4. Nits.
   • replicateFin_succ and OracleComp.pi_succ are now @[simp], while replicate_succ on main is not. As a result, plain simp now unfolds replicateFin (n+1) _. Current clients use simp only, so nothing breaks, but you may want to match replicate_succ.
   • In Sharing.lean, open scoped BigOperators is unnecessary.

Fixed and verified

• Parallel definition (item 1).
  • There is now a single OracleComp.pi / OracleComp.piRestrict, in Vector.lean next to replicateFin.
  • replicateFin count p is defined as pi (fun _ => p), and replicateFin_eq_pi holds by rfl.
  • mem_support_replicateFin_iff, eval_replicateFin and eval_replicateFin_map_coords are now one-line specializations of the pi lemmas, so the follow-up merge is already done.
  • No runner, support, product or map lemmas remain in Sharing.lean.
  • castInit / lastFin are replaced by Fin.castLE (Nat.sub_le m 1) / ⊤, and the unused [NeZero m] is gone.
• No existing client breaks.
  • No public statement in Vector.lean changed meaning; only proofs and the body of replicateFin changed.
  • The new body is the same computation up to map = bind pure, and map_ofFn_replicateFin still pins agreement with replicate.
  • Vector.lean is unchanged on main since the merge base.
  • The clients on main (CountMin Program.lean; GSW Sampling, LWE, Randomness and Serialized) use only lemmas whose statements are unchanged, and none of them unfolds replicateFin.
  • No file changed on main since the merge base mentions these names, so the green CI at this head covers them.
• Locators (item 2).
  • Eqs. 7.39 and 7.40 are both on p. 696. The page offset is constant against the print text and agrees with Eqs. 7.7–7.10 on p. 620.
  • These now cite the right places: realJoint, idealJoint (Eqs. 7.9–7.10) and PerfectSemiHonestPrivate.
  • The bridge lemma is also correct. Its hypothesis is Eq. 7.39, cf. Eqs. 7.7–7.8. Its conclusion is Eq. 7.40, cf. Eqs. 7.9–7.10. The deterministic-equivalence remark is on p. 621.
  • The PR body's locators for these are now correct as well.
• Negative test 1 is genuine.
  • not_perfectSemiHonestPrivate_leakyProtocol uses I = {1} and two inputs that differ only at party 0.
  • The ideal laws are equal, because the restricted input and the constant output are equal.
  • Mapped to party 1's received bit, the real laws are pure false and pure true.
  • So the failure comes from the leaked message, not from a type artifact.
  • Test 2's proof is also sound (ideal support has y 0 = y 1, while the real support contains ![false, true]). Only its attribution and description are wrong.
• Oracle round. perfectSemiHonestPrivate_oracleXorProtocol runs a real Round.oracle round through Steps.evalWith_oracle and Round.received_oracle_ext. The view check compares the delivered answer part with yI i.
• Rename (non-blocking item 4).
  • The move to Cslib.Crypto.Protocols.MPC is complete: the namespace, the declaration names in the docstring, the test's open, and the Complexity.lean import.
  • No Cslib.Crypto.MPC remains.
  • MultiOracleWorld.handler, built with ProbOracleComp.handler, replaces both inline handlers.
  • The proto.sampleCoins docstring is fixed.

[SamuelSchlesinger]

All items from review 5684235311 (reviewer-claude-c4b0c164-94) are addressed at 85ad8e977, with Lean Action CI/ci-checks green and check_pr_names.py --strict 106/106 clean:

1. Formalized Goldreich's Counterexample 1 (§7.2.2.1, CUP print p. 621) in ComplexityTests/Crypto/MPC.lean:
   • goldreichCounterexample1Func: models (1^n, 1^n) ↦ (r, λ) as ((), ()) ↦ ![b, false] for uniform b : Bool.
   • goldreichCounterexample1Protocol: 1-round protocol over [.message 0 1 Bool] where party 0 samples uniform r, sends r to party 1, and outputs r, while party 1 outputs false.
   • eval_snd_goldreichCounterexample1Protocol: proves that goldreichCounterexample1Protocol computes goldreichCounterexample1Func with zero error.
   • eval_goldreichCounterexample1MarginalSim1: proves that goldreichCounterexample1MarginalSim1 (sampling a uniform received bit) matches party 1's marginal view distribution at I = {1} (satisfying Eq. 7.8 on p. 620).
   • not_perfectSemiHonestPrivate_goldreichCounterexample1: proves ∀ S, ¬ PerfectSemiHonestPrivate goldreichCounterexample1Protocol noOracleWorld goldreichCounterexample1Func S by refuting Eq. 7.10 / Eq. 7.40 at I = {1}.
   • Kept not_perfectSemiHonestPrivate_independentCoinProtocol as an output-correctness negative test at I = ∅ with no Goldreich attribution.
2. Corrected the section number in Complexity/Languages/Probabilistic/Sharing.lean:
   • Updated the reference to Section 7.5.2.3 (Construction 7.5.10, Step 1), print pp. 705–706.
3. Recommended items & nits:
   • Dropped the ProbComp.pi and ProbComp.piRestrict aliases and the restated ProbComp.pi_zero / ProbComp.pi_succ lemmas in Complexity/Languages/Probabilistic/Vector.lean, using OracleComp.pi throughout.
   • Removed @[simp] from OracleComp.pi_succ and OracleComp.replicateFin_succ (matching OracleComp.replicate_succ), and removed open scoped BigOperators from Sharing.lean.

Requesting re-review from reviewer-claude (cc coordinator-claude-c4b0c164-20261023).

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

[SamuelSchlesinger]

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

APPROVED at 85ad8e977608148b25fae321e9ee0bdcd4f128a4

Delta f83369f..85ad8e9 only; read-only inspection, CI green at this head.

1. Counterexample 1 (print p. 621): the print text reads "(1^n,1^n) -> (r, lambda), r uniform; Party 1 selects r, sends it to Party 2, and outputs r. A simulator S2(1^n) outputting uniform r satisfies Eq. (7.8) but not Eq. (7.10)." The PR now formalizes exactly this, with Party 1 = index 0 and Party 2 = index 1, at coalition I = {1}.
   • (a) eval_snd_goldreichCounterexample1Protocol proves output correctness: the protocol's output distribution equals eval (goldreichCounterexample1Func x).
   • (b) eval_goldreichCounterexample1MarginalSim1 proves the marginal view at {1} is simulated by a uniform received bit (Eq. 7.8).
   • (c) not_perfectSemiHonestPrivate_goldreichCounterexample1 fails for the genuine reason. Every real joint support point has party 1's received bit equal to res.2 0. The ideal joint contains (v, ![b,false]) for both b, with the same simulator output v, because the simulator sees only ((), false). Rewriting through hPriv then forces received = false and received = true for the same v. This is not vacuous: the simulator-support nonemptiness and the ideal-support membership are both proved.
   • Docstrings and the test-file header now match the source: Section 7.2.2.1, p. 621, Eqs. 7.8 and 7.10 on p. 620, Eq. 7.40 on p. 696. The old coin-broadcast test is correctly relabeled as an output-correctness failure at I = empty set, no longer misattributed to Goldreich.
2. Sharing.lean: it now cites "Section 7.5.2.3 (Construction 7.5.10, Step 1), print pp. 705-706". In the print, Section 7.5.2.3 starts before the "705" footer and Construction 7.5.10 with Step 1 follows it, so the range is accurate. The unused open scoped BigOperators was also dropped.
3. Aliases: ProbComp.pi, ProbComp.piRestrict and the duplicate pi_zero/pi_succ are removed, and a grep of the PR head finds no remaining ProbComp.pi* references. All uses are OracleComp.pi*. pi_succ and replicateFin_succ lost @[simp], and the tests that need them now pass them explicitly, which is fine.
4. No new problems found in this delta.