diff --git a/Complexity/Crypto/Protocols/MPC/Basic.lean b/Complexity/Crypto/Protocols/MPC/Basic.lean
index d03008c40..653449845 100644
--- a/Complexity/Crypto/Protocols/MPC/Basic.lean
+++ b/Complexity/Crypto/Protocols/MPC/Basic.lean
@@ -18,6 +18,12 @@ protocols over pairwise private authenticated point-to-point channels with `k`-a
 calls (`MultiOracleSpec`), together with Goldreich's joint view-and-output definition of perfect
 semi-honest privacy against static coalitions (`PerfectSemiHonestPrivate`).
 
+`PerfectSemiHonestPrivate` departs from Goldreich's Definitions 7.2.1 and 7.5.1 in two ways.
+Privacy is exact equality of distributions, not computational indistinguishability. The coalition
+simulators are arbitrary `ProbComp` values with no efficiency requirement, whereas Goldreich asks
+for a probabilistic polynomial-time simulator. Efficient simulators for the $\text{OT}_1^4$
+completeness theorem are certified separately, in `Complexity.Crypto.Protocols.MPC.PolyTime`.
+
 Each party's view (`PartyView`) is derived from the protocol execution: it records only that
 party's own input `x i`, its own private coins `r i` drawn from `proto.sampleCoins i`, the messages
 addressed to `i`, and the oracle answer parts for slots assigned to `i`. In `Round.Received`,
@@ -519,7 +525,8 @@ def Functionality.ofDeterministic {m : ℕ} {In Out : Fin m → Type}
 
 /-- A simulator for a static coalition `I : Finset (Fin m)` receives the coalition's inputs
 `(i : I) → In i` and the coalition's outputs `(i : I) → Out i`, and samples simulated views
-`(i : I) → PartyView In Coins sc i`. -/
+`(i : I) → PartyView In Coins sc i`. It is an arbitrary `ProbComp`: unlike Goldreich's
+simulators, it need not run in probabilistic polynomial time. -/
 abbrev CoalitionSimulator {m : ℕ} {spec : MultiOracleSpec} (sc : Schedule m spec)
     (In Coins Out : Fin m → Type) (I : Finset (Fin m)) :=
   ((i : I) → In i) → ((i : I) → Out i) → ProbComp ((i : I) → PartyView In Coins sc i)
@@ -536,7 +543,9 @@ def idealJoint {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec}
   return (v, y)
 
 /-- Perfect semi-honest privacy for all static coalitions `I : Finset (Fin m)`
-(Goldreich Def. 7.5.1, Eq. 7.40, p. 696; cf. Def. 7.2.1, Eqs. 7.9–7.10, p. 620). -/
+(Goldreich Def. 7.5.1, Eq. 7.40, p. 696; cf. Def. 7.2.1, Eqs. 7.9–7.10, p. 620), with exact
+equality in place of computational indistinguishability. The simulators `S` are unrestricted:
+Goldreich requires a probabilistic polynomial-time simulator, and this definition does not. -/
 def PerfectSemiHonestPrivate {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec}
     {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out)
     (W : MultiOracleWorld spec) (f : Functionality m In Out)
@@ -544,7 +553,8 @@ def PerfectSemiHonestPrivate {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m
   ∀ (I : Finset (Fin m)) (x : (i : Fin m) → In i),
     ProbComp.eval (idealJoint f I (S I) x) = proto.realJoint W I x
 
-/-- Perfect semi-honest privacy against all proper static coalitions `I ≠ Finset.univ`. -/
+/-- Perfect semi-honest privacy against all proper static coalitions `I ≠ Finset.univ`, with the
+same exact equality and unrestricted simulators as `PerfectSemiHonestPrivate`. -/
 def PerfectSemiHonestPrivateProper {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec}
     {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out)
     (W : MultiOracleWorld spec) (f : Functionality m In Out)
diff --git a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean
index fc90008e9..204a62be5 100644
--- a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean
+++ b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean
@@ -60,6 +60,11 @@ print pp. 645–648):
    every static coalition `I : Finset (Fin m)` for every circuit `C` without syntactic restrictions
    on `C.outputs`.
 
+Privacy is `PerfectSemiHonestPrivate` with the explicit simulators below: exact equality of
+distributions, with no certificate that the simulators run in probabilistic polynomial time as
+Goldreich's definitions require. Efficiency is certified only for the composed
+$\text{OT}_1^4$-hybrid protocol, in `Complexity.Crypto.Protocols.MPC.PolyTime`.
+
 ## Main definitions
 
 * `Cslib.Crypto.Protocols.MPC.circuitFunctionality`: deterministic $m$-party functionality computed
diff --git a/Complexity/Crypto/Protocols/MPC/SharedMul.lean b/Complexity/Crypto/Protocols/MPC/SharedMul.lean
index 150d2cf32..4e4e42de4 100644
--- a/Complexity/Crypto/Protocols/MPC/SharedMul.lean
+++ b/Complexity/Crypto/Protocols/MPC/SharedMul.lean
@@ -38,6 +38,11 @@ reductions from Goldreich's *Foundations of Cryptography, Volume 2: Basic Applic
    `sharedMulSpec 2` over all ordered pairs $i < j$, proved perfectly semi-honest private against
    every static coalition `I : Finset (Fin m)`.
 
+Privacy is `PerfectSemiHonestPrivate` with the explicit simulators below: exact equality of
+distributions, with no certificate that the simulators run in probabilistic polynomial time as
+Goldreich's definitions require. Efficiency is certified only for the composed
+$\text{OT}_1^4$-hybrid protocol, in `Complexity.Crypto.Protocols.MPC.PolyTime`.
+
 ## Main definitions
 
 * `Cslib.Crypto.Protocols.MPC.ot14Spec`, `Cslib.Crypto.Protocols.MPC.ot14World`: 2-party
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
index 0c1d224e5..03697ab27 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
@@ -24,7 +24,10 @@ The prover's private state between its two messages is explicit. Its commitment
 sampled together, and its response is a function of the state and the challenge; randomness the
 response needs can be sampled with the commitment and kept in the state. Protocols are plain
 functions and distributions, with no efficiency or finiteness assumption; the properties are
-exact statements about a single protocol.
+exact statements about a single protocol. The same holds for extractors and simulators: Boneh and
+Shoup require them to be efficient algorithms (Definitions 19.4 and 19.5), but `SpecialSoundness`
+and `SpecialHVZK` accept arbitrary functions and distributions, so neither makes an efficiency
+claim.
 
 Each property carries its algorithm explicitly. `SpecialSoundness R extract` says that the
 deterministic `extract` computes a witness from any two accepting conversations that share a
@@ -110,7 +113,8 @@ def Complete (R : X → Y → Prop) : Prop :=
 statement from two accepting conversations with a common commitment and distinct challenges.
 The extracted witness has a type `W` and a relation `R` of its own. Usually these are the
 prover's witness type and relation; lattice-based protocols extract a witness of a relaxed
-relation instead. -/
+relation instead. The book requires an efficient deterministic extractor; `extract` here is an
+arbitrary function. -/
 def SpecialSoundness {W : Type*} (R : W → Y → Prop) (extract : Y → T → C → Z → C → Z → W) :
     Prop :=
   ∀ y t c z c' z', c ≠ c' → P.Accepts y t c z → P.Accepts y t c' z' →
@@ -118,7 +122,8 @@ def SpecialSoundness {W : Type*} (R : W → Y → Prop) (extract : Y → T → C
 
 /-- Special honest-verifier zero knowledge ([BonehShoup2023], Definition 19.5) with the explicit
 simulator `simulate`. The simulator gets a statement and a challenge and returns a commitment
-and a response. -/
+and a response. The book requires an efficient probabilistic simulator; `simulate` here is an
+arbitrary distribution-valued function. -/
 structure SpecialHVZK (R : X → Y → Prop) (simulate : Y → C → PMF (T × Z)) : Prop where
   /-- Simulated conversations are accepting, for every statement and challenge. -/
   accepts : ∀ y c, ∀ tz ∈ (simulate y c).support, P.Accepts y tz.1 c tz.2