refactor(Crypto): replace projection chains across MPC, GMW, and SigmaProtocol modules (#1764)

Complexity/Crypto/Computational/GMW/PolyTime.lean

@@ -517,7 +517,7 @@ theorem isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input :
     {reply1 reply2 : Caller × List Bool → List Bool}
     {bound : Caller → ℕ}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hprep : ComputableInPolyTime prepare input (encPair encUnary (encPair enc encBits)))
     (hr1 : ComputableInPolyTime reply1 (encPair input encBits) encBits)
     (hr2 : ComputableInPolyTime reply2 (encPair input encBits) encBits)
@@ -578,7 +578,7 @@ theorem isPPTOn_runTwoRound_prover {α Caller : Type} {enc : α ↪ List Bool}
     {openFlags bits ch_guess : Caller → List Bool}
     {seeds pads : Caller → List (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hg : ComputableInPolyTime generator encBits encBits)
     (hn : ComputableInPolyTime n input encUnary)
     (hs : ComputableInPolyTime s input encUnary)
@@ -666,11 +666,11 @@ noncomputable def gmwSimWithPads (generator : List Bool → List Bool) (s m : 
     ProbComp (List Bool) := do
   let ch_guess ← BitString.sampleList 3
   let coins ← gmwSampleSimCoins s φ ch_guess
-  let p ← runTwoRound
+  let (view, _, challenge) ← runTwoRound
     (fun r => proverReply1 generator m r (allOpenFlags φ ch_guess coins.1) coins.1 coins.2 pads)
     (fun _ => proverReply2 s φ ch_guess coins.1 coins.2)
     prog (0, [false, false, false])
-  return if p.2.2 == ch_guess then true :: p.1 else []
+  return if challenge == ch_guess then true :: view else []
 
 /-- One attempt of the GMW zero-knowledge simulator (without any witness). -/
 noncomputable def gmwSimAttempt (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ)
@@ -693,7 +693,7 @@ private theorem isPPTOn_gmwSimWithPads {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableTidilyInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) (encList encBits)) encBits
       (fun p : (ℕ × α × List Bool) × List (List Bool) =>
         gmwSimWithPads generator (p.1.1 + 7) (length (p.1.1 + 7))
@@ -719,7 +719,7 @@ private theorem isPPTOn_gmwSimAttempt {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableTidilyInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
       (fun p : ℕ × α × List Bool =>
         gmwSimAttempt generator (p.1 + 7) (length (p.1 + 7))
@@ -742,10 +742,10 @@ theorem isPPTOn_gmwSimulator {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool =>
-        gmwSimulator generator length f Vstar p.1 p.2.1 p.2.2) := by
+      (fun (n, a, z) =>
+        gmwSimulator generator length f Vstar n a z) := by
   have hg := hg.tidy
   have hf := hf.tidy
   have hattempt := isPPTOn_gmwSimAttempt hg hlen hf hV
@@ -794,7 +794,7 @@ private theorem isPPTOn_runTwoRound_honest {α Caller : Type} {enc : α ↪ List
     {n s m : Caller → ℕ} {a : Caller → α} {z : Caller → List Bool}
     {φ : Caller → CNF ℕ} {coins : Caller → List Bool × List (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hg : ComputableTidilyInPolyTime generator encBits encBits)
     (hn : ComputableTidilyInPolyTime n input encUnary)
     (hs : ComputableTidilyInPolyTime s input encUnary)
@@ -827,11 +827,15 @@ theorem isPPTOn_gmwInteract {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair encUnary (encPair enc (encPair encBits encBits))) encBits
-      (fun p : ℕ × α × List Bool × List Bool =>
-        gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1
-          (Vstar p.1 p.2.1 p.2.2.2)) := by
+      (fun (n, a, w, z) =>
+        gmwInteract generator (n + 7) (length (n + 7)) (f a) w
+          (Vstar n a z)) := by
+  change IsPPTOn (encPair encUnary (encPair enc (encPair encBits encBits))) encBits
+    (fun p : ℕ × α × List Bool × List Bool =>
+      gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1
+        (Vstar p.1 p.2.1 p.2.2.2))
   have hgPlain := hg
   have hfPlain := hf
   have hg := hg.tidy

Complexity/Crypto/Computational/GMW/Simulator.lean

@@ -474,11 +474,11 @@ noncomputable def gmwRealWithPads (generator : List Bool → List Bool) (s m : 
   let bits := realBits φ w m₀ m₁ m₂
   let openFlags := allOpenFlags φ ch_guess bits
   let seeds ← OracleComp.replicate (totalLen φ) (BitString.sampleList s)
-  let p ← runTwoRound
+  let (view, _, challenge) ← runTwoRound
     (fun r => proverReply1 generator m r openFlags bits seeds pads)
     (fun _ => proverReply2 s φ ch_guess bits seeds)
     prog (0, [false, false, false])
-  return if p.2.2 == ch_guess then true :: p.1 else []
+  return if challenge == ch_guess then true :: view else []
 
 /-- Single-attempt hybrid with pseudorandom unopened pads. -/
 noncomputable def gmwRealPRGPads (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ)
@@ -862,7 +862,7 @@ private theorem isPPTOn_gmwRealWithPads {α Param : Type} {enc : α ↪ List Boo
     {φ : Param → CNF ℕ} {pads : Param → List (List Bool)}
     (hg : ComputableTidilyInPolyTime generator encBits encBits)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hn : ComputableTidilyInPolyTime n input encUnary)
     (hs : ComputableTidilyInPolyTime s input encUnary)
     (hm : ComputableTidilyInPolyTime m input encUnary)
@@ -918,14 +918,13 @@ theorem isPPTOn_gmwViewReduction {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool
-      (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2)) :
+      (fun ((n, a, z), view) => adversary n a z view)) :
     IsPPTOn
       (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) encBool
-      (fun p : (ℕ × (α × (List Bool × List Bool))) × List Bool =>
-        gmwViewReduction generator length f Vstar adversary
-          p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2) := by
+      (fun ((n, a, w, z), challenge) =>
+        gmwViewReduction generator length f Vstar adversary n a w z challenge) := by
   have hgPlain := hg
   have hfPlain := hf
   have hg := hg.tidy
@@ -1027,9 +1026,9 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool
-      (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2))
+      (fun ((n, a, z), view) => adversary n a z view))
     (hPRG : ∀ test : (ℕ × (α × (List Bool × List Bool))) × List Bool → ProbComp Bool,
       IsPPTOn
         (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits)
@@ -1060,8 +1059,9 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool}
   have hf := hf.tidy
   have hclock := isPPTOn_gmwViewReduction (.of_tidy hg) hlen (.of_tidy hf) hV hadv
   have hneg := hPRG
-    (fun p => gmwViewReduction generator length f Vstar adversary
-      p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2) hclock a w z ha hw hz
+    (fun ((n, a, w, z), challenge) =>
+      gmwViewReduction generator length f Vstar adversary n a w z challenge)
+    hclock a w z ha hw hz
   have hcount : ComputableTidilyInPolyTime (fun a => totalLen (f a)) enc encUnary :=
     (computableInPolyTime_totalLen (.of_tidy hf)).tidy
   have hsize : PolyBounded id (fun n => (enc (a n)).length) :=
@@ -1111,9 +1111,9 @@ theorem AdvicePRG.gmwView_negligible {α : Type} {enc : α ↪ List Bool}
     (hAdv : AdvicePRG enc generator length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool
-      (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2))
+      (fun ((n, a, z), view) => adversary n a z view))
     {a : ℕ → α} {w z : ℕ → List Bool}
     (ha : PolynomiallyBounded (fun n => (enc (a n)).length))
     (hw : PolynomiallyBounded (fun n => (w n).length))
@@ -1139,7 +1139,7 @@ theorem gmwView_indistinguishable_gmwSimulator {α : Type} {enc : α ↪ List Bo
     {f : α → CNF ℕ} (hf : ComputableInPolyTime f enc encCNF)
     {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     {a : ℕ → α} {w z : ℕ → List Bool}
     (ha : ComputableInPolyTime a encUnary enc)
     (hw_comp : ComputableInPolyTime w encUnary encBits)

Complexity/Crypto/Protocols/Cipher/EvenMansour.lean

@@ -1674,9 +1674,17 @@ theorem run_idealLazyHandler_good_le_realLazyHandler {α : Type}
     (program : OracleComp (EvenMansourSpec G) α) (P : α → Prop) (k : G × G)
     {c_e c_π c : Cache G} (hrel : CacheRel k c_e c_π c) :
     ((OracleComp.interpret idealLazyHandler program).run (c_e, c_π)).toOuterMeasure
-      {res | P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} ≤
+      {(r, c_e', c_π') : α × Cache G × Cache G |
+        P r ∧ isBadEvenMansourKey c_e' c_π' k = false} ≤
     ((OracleComp.interpret (realLazyHandler k) program).run c).toOuterMeasure
       {res | P res.1} := by
+  have hset :
+      {(r, c_e', c_π') : α × Cache G × Cache G |
+        P r ∧ isBadEvenMansourKey c_e' c_π' k = false} =
+      {res | P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} := by
+    ext ⟨_, _, _⟩
+    simp
+  rw [hset]
   induction program generalizing c_e c_π c with
   | pure a =>
     change (PMF.pure (a, (c_e, c_π))).toOuterMeasure
@@ -1912,8 +1920,16 @@ private theorem idealGame_apply_le_realGame_add_of_keyDist (keyDist : PMF (G ×
           MeasureTheory.measure_union_le _ _
       _ ≤ ((OracleComp.interpret (realLazyHandler k) program).run []).toOuterMeasure
             (Prod.fst ⁻¹' {b}) +
-          M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true} :=
-          add_le_add
+          M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true} := by
+          have hset :
+              {res : Bool × (Cache G × Cache G) |
+                res.1 = b ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} =
+              {(r, c_e', c_π') : Bool × Cache G × Cache G |
+                r = b ∧ isBadEvenMansourKey c_e' c_π' k = false} := by
+            ext ⟨_, _, _⟩
+            simp
+          rw [hset]
+          exact add_le_add
             (run_idealLazyHandler_good_le_realLazyHandler program (· = b) k (cacheRel_nil k))
             le_rfl
   have hsum_ideal : ∑' k : G × G, keyDist k * evenMansourIdealGame program b =

Complexity/Crypto/Protocols/MPC/CircuitEval.lean

@@ -148,7 +148,8 @@ and applying `finish` at `.done`. -/
     .message (sender := p.1) (receiver := p.2)
       (fun st => st.1 p.2)
       ((msgStepsWith finish L).mapState fun i st =>
-        (st.1.1, st.1.2 + extractMsg p i st.2))
+        let (toSend, acc) := st.1
+        (toSend, acc + extractMsg p i st.2))
 
 /-- 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. -/
@@ -636,18 +637,19 @@ private theorem eval_progDist_restrict_of_ne_univ {m inputCount g : ℕ} [NeZero
     (recv : (Round.message (spec := spec) s r Bool).Received i) : Bool :=
   if h : i = r then recv h else 0
 
-/-- Gather `Bool` shares at receiver `r` from senders `S`, preserving `st.1` and `st.2.1` and
+/-- Gather `Bool` shares at receiver `r` from senders `S`, preserving `state` and `myShare` and
 applying `finish` at `.done`. -/
 @[expose] def 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 => State i × Bool × Bool) Out (gatherSchedule m (spec := spec) r S)
-  | [] => .done (fun i st => finish i st.1 st.2.2)
+  | [] => .done (fun i (state, _, acc) => finish i state acc)
   | s :: S =>
     .message (sender := s) (receiver := r)
-      (fun st => st.2.1)
+      (fun (_, myShare, _) => myShare)
       ((gatherStepsWith r finish S).mapState fun i st =>
-        (st.1.1, st.1.2.1, st.1.2.2 + extractBitFor s r i st.2))
+        let (state, myShare, acc) := st.1
+        (state, myShare, acc + extractBitFor s r i st.2))
 
 /-- Sum of party `i`'s received bits along `gatherSchedule m r S`. -/
 @[expose] def sumGatherBits {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) :

Complexity/Crypto/Protocols/MPC/Composition.lean

@@ -429,16 +429,18 @@ first state component. -/
     .message (sender := parties s₀) (receiver := parties r₀)
       (fun st_sender => send (st_sender.2 s₀ rfl))
       ((Steps.embed parties Outer next).mapState fun _ st_i =>
-        (st_i.1.1, fun s hs =>
-          (st_i.1.2 s hs,
-            pullRoundReceived parties (.message s₀ r₀ Msg) hs st_i.2)))
+        let ((outer_i, st_k_i), recv_i) := st_i
+        (outer_i, fun s hs =>
+          (st_k_i s hs,
+            pullRoundReceived parties (.message s₀ r₀ Msg) hs recv_i)))
   | .oracle (op := op) (parties := subParties) query next =>
     .oracle (op := op) (parties := subParties.trans parties)
       (fun t st_party => query t (st_party.2 (subParties t) rfl))
       ((Steps.embed parties Outer next).mapState fun _ st_i =>
-        (st_i.1.1, fun s hs =>
-          (st_i.1.2 s hs,
-            pullRoundReceived parties (.oracle op subParties) hs st_i.2)))
+        let ((outer_i, st_k_i), recv_i) := st_i
+        (outer_i, fun s hs =>
+          (st_k_i s hs,
+            pullRoundReceived parties (.oracle op subParties) hs recv_i)))
 
 @[simp] private theorem outputAt_embed {k m : ℕ} {spec : MultiOracleSpec}
     (parties : Fin k ↪ Fin m) (Outer : Fin m → Type)
@@ -515,16 +517,19 @@ execution of `(Sub op).steps` along `parties`. -/
     .message (sender := s₀) (receiver := r₀)
       (fun st_sender => send st_sender.1)
       ((Steps.compose Sub next).mapState fun _ st_i =>
-        ((st_i.1.1, st_i.2), st_i.1.2))
+        let ((state_i, coins_i), recv_i) := st_i
+        ((state_i, recv_i), coins_i))
   | .oracle (op := op) (parties := parties) (sc := rest) query next =>
     (((Steps.embed parties (fun i => State i × Schedule.SubCoins Coins₂ rest i)
         (Sub op).steps).mapState
       (fun i st_i =>
-        ((st_i.1, st_i.2.2),
+        let (state_i, slotCoins_i, restCoins_i) := st_i
+        ((state_i, restCoins_i),
           fun (s : Fin (spec₁.arity op)) (hs : parties s = i) =>
-            (query s (hs.symm ▸ st_i.1), st_i.2.1 s hs)))).append
+            (query s (hs.symm ▸ state_i), slotCoins_i s hs)))).append
       ((Steps.compose Sub next).mapState fun _ st_i =>
-        ((st_i.1.1, st_i.2), st_i.1.2)))
+        let ((state_i, restCoins_i), subOut_i) := st_i
+        ((state_i, subOut_i), restCoins_i)))
 
 /-- Expand a simulated outer execution along `steps : Steps State Out sc₁` by invoking the inner
 simulator `S₂ op (subCoalition parties I)` at every `.oracle op parties` round (Goldreich Theorem

Complexity/Crypto/Protocols/MPC/PolyTime.lean

@@ -357,8 +357,9 @@ packed coalition input bits `extendCoalitionBits I xI` and output bits
 def encFamilySimInput {α : Type} (enc : α ↪ List Bool) (m : ℕ) (n k : α → ℕ)
     (I : Finset (Fin m)) : FamilySimInput α m n k I ↪ List Bool where
   toFun inp :=
+    let ⟨a, xI, yI⟩ := inp
     encPair enc (encPair encBits encBits)
-      (inp.1, (extendCoalitionBits I inp.2.1, extendCoalitionBits I inp.2.2))
+      (a, (extendCoalitionBits I xI, extendCoalitionBits I yI))
   inj' := by
     rintro ⟨a₁, x₁, y₁⟩ ⟨a₂, x₂, y₂⟩ h
     obtain ⟨ha, hxy⟩ := Prod.ext_iff.1 ((encPair enc (encPair encBits encBits)).injective h)
@@ -499,13 +500,15 @@ def encGMWPartyView (m coins n k : ℕ)
   let (_, r_out) :=
     splitOTMulCompose (GMWCircuit.progSchedule m D.program)
       (GMWCircuit.outputSchedule m k) i r_prog_out
+  let (preludeCoins, (circuitCoins, _), otSubCoins) := v.coins
   encPair
     (encPair (encPair encBits encBits) (encPair encBits encBits))
     (encPair encBits (encPair encBits encBits))
-    (((List.ofFn v.input, List.ofFn v.coins.1),
+    (((List.ofFn v.input, List.ofFn preludeCoins),
       (List.ofFn
-        ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm v.coins.2.1.1),
-       encOTSubCoins _ i v.coins.2.2)),
+        ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm
+          circuitCoins),
+       encOTSubCoins _ i otSubCoins)),
      (encPairsMsgReceived i (GMWCircuit.allPairs m) r_in,
       (encOTOracleAnswers _ i v.received,
        encOutCoordsMsgReceived i (GMWCircuit.outCoords m k) r_out)))
@@ -5959,11 +5962,11 @@ theorem isPPTOn_gmwOT14RandomizedSim {α : Type} {enc : α ↪ List Bool}
     (hC : ComputableInPolyTime (fun a => (C a).code) enc Boolean.encCode)
     (I : Finset (Fin m)) :
     Cslib.Probability.IsPPTOn (encFamilySimInput enc m n k I) encBits
-      (fun inp =>
+      (fun ⟨a, xI, yI⟩ =>
         encodeCoalitionView
-          (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$>
-          gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1)
-            (C inp.1) I inp.2.1 inp.2.2) := by
+          (encGMWPartyView m (coins a) (n a) (k a) (C a)) I <$>
+          gmwOT14RandomizedSim m (coins a) (n a) (k a) (C a)
+            I xI yI) := by
   have hD := computableInPolyTime_code_comp_xorPreludeCircuit m hn hcoins hC
   exact (PolyTimeRunner.isPPTOn_simRunWord m I hcoins.tidy hn.tidy hk.tidy hD.tidy).congr
     (PolyTimeRunner.eval_simRunWord_eq_gmwOT14RandomizedSim m coins n k C I)
@@ -6008,11 +6011,11 @@ theorem exists_perfectSemiHonestPrivate_ot14_of_polyTime {α : Type} {enc : α 
             (fun _ y => List.ofFn y) inp.2) ∧
       (∀ (I : Finset (Fin m)), I ≠ Finset.univ →
         Cslib.Probability.IsPPTOn (encFamilySimInput enc m n k I) encBits
-          (fun inp =>
+          (fun ⟨a, xI, yI⟩ =>
             encodeCoalitionView
-              (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$>
-              gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1)
-                (C inp.1) I inp.2.1 inp.2.2)) := by
+              (encGMWPartyView m (coins a) (n a) (k a) (C a)) I <$>
+              gmwOT14RandomizedSim m (coins a) (n a) (k a) (C a)
+                I xI yI)) := by
   have h_in : ComputableInPolyTime (fun a => m * n a + coins a) enc encUnary := by
     have hmn := ComputableTidilyInPolyTime.comp' ComputableTidilyInPolyTime.unary_mul
       ((ComputableTidilyInPolyTime.const m).prod hn.tidy)