refactor(Crypto): replace projection chains across protocol modules (#1764)

Complexity/Crypto/Computational/Commitment.lean

@@ -228,7 +228,7 @@ structure CommitmentReceiver.IsPPT (receiver : CommitmentReceiver) : Prop where
   /-- The second stage is strict PPT on `(n, state, c)`. -/
   guess :
     IsPPTOn (encPair encUnary (encPair encBits encBits)) encBool
-      (fun p => receiver.guess p.1 p.2.1 p.2.2)
+      (fun ⟨n, state, c⟩ => receiver.guess n state c)
 
 /-- The two-stage commitment-hiding experiment against a stateful receiver `receiver` with
 auxiliary input `aux` and hidden bit selector `bit : Bool` at security parameter `n`.
@@ -239,19 +239,20 @@ noncomputable def commitmentHidingGame (commit : List Bool → Bool → List Boo
     (receiver : CommitmentReceiver) (aux : List Bool) (bit : Bool) (n : ℕ) : ProbComp Bool := do
   let choice ← receiver.choose n aux
   let seed ← BitString.sampleList n
-  receiver.guess n choice.2
-    (commit choice.1.1 (if bit then choice.1.2.2 else choice.1.2.1) seed)
+  let ((r, b₀, b₁), state) := choice
+  receiver.guess n state
+    (commit r (if bit then b₁ else b₀) seed)
 
 /-- The commitment-hiding experiment runs in strict PPT on `(n, aux, bit)` whenever `commit` is
 computable in plain polynomial time and `receiver` is strict PPT. -/
 theorem isPPTOn_commitmentHidingGame {commit : List Bool → Bool → List Bool → List Bool}
     {receiver : CommitmentReceiver}
     (hcommit : ComputableInPolyTime
-      (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+      (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits)
     (hR : receiver.IsPPT) :
     IsPPTOn (encPair encUnary (encPair encBits encBool)) encBool
-      (fun p => commitmentHidingGame commit receiver p.2.1 p.2.2 p.1) := by
+      (fun ⟨n, aux, bit⟩ => commitmentHidingGame commit receiver aux bit n) := by
   have hcommit_tidy := hcommit.tidy
   have hchoose := hR.choose
   have hguess := hR.guess
@@ -263,7 +264,7 @@ indexed family on `(n, aux)`. -/
 theorem isPPT_commitmentHidingGame {commit : List Bool → Bool → List Bool → List Bool}
     {receiver : CommitmentReceiver}
     (hcommit : ComputableInPolyTime
-      (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+      (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits)
     (hR : receiver.IsPPT) (bit : Bool) :
     IsPPT encBool (fun n aux => commitmentHidingGame commit receiver aux bit n) := by
@@ -278,7 +279,7 @@ in the unary security parameter `n`. -/
 theorem isPPTOn_commitmentHidingGame_aux {commit : List Bool → Bool → List Bool → List Bool}
     {receiver : CommitmentReceiver} {aux : ℕ → List Bool}
     (hcommit : ComputableInPolyTime
-      (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+      (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits)
     (hR : receiver.IsPPT)
     (haux : ComputableInPolyTime aux encUnary encBits) (bit : Bool) :
@@ -372,8 +373,9 @@ noncomputable def naorReceiverDistinguisher (receiver : CommitmentReceiver)
     (aux : ℕ → List Bool) (bit : Bool) : Distinguisher :=
   fun n pad => do
     let choice ← receiver.choose n (aux n)
-    receiver.guess n choice.2
-      (naorCommit id choice.1.1 (if bit then choice.1.2.2 else choice.1.2.1) pad)
+    let ((r, b₀, b₁), state) := choice
+    receiver.guess n state
+      (naorCommit id r (if bit then b₁ else b₀) pad)
 
 /-- `naorReceiverDistinguisher receiver aux bit` is a strict PPT distinguisher whenever `receiver`
 is strict PPT and `aux` is computable in plain polynomial time. -/
@@ -1148,13 +1150,12 @@ structure BitCommitmentScheme where
   polyTime_commitLength : ComputableInPolyTime commitLength encUnary encUnary
   /-- `commit` is computable in plain polynomial time. -/
   polyTime_commit :
-    ComputableInPolyTime (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+    ComputableInPolyTime (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits
   /-- `verify` is computable in plain polynomial time. -/
   polyTime_verify :
     ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × Bool × List Bool =>
-        verify p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2)
+      (fun ⟨n, r, c, b, seed⟩ => verify n r c b seed)
       (encPair encUnary (encPair encBits (encPair encBits (encPair encBool encBits)))) encBool
   /-- Honest commitments have length `commitLength n` when `seed.length = n`. -/
   length_commit : ∀ (n : ℕ) (r : List Bool) (b : Bool) (seed : List Bool),

Complexity/Crypto/Computational/DiffieHellman.lean

@@ -160,8 +160,9 @@ def CDH (setup : ℕ → PMF F.Desc) : Prop :=
 to obtain a candidate exponent `a` and multiplying `encode (β • g)` by `a`. -/
 def dlToCDHAdversary (adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool))
     (n : ℕ) (input : F.Desc × List Bool × List Bool) : ProbComp (List Bool) := do
-  let guess ← adversary n (input.1, input.2.1)
-  return F.smul (input.1, ofBits guess, input.2.2)
+  let (d, u, v) := input
+  let guess ← adversary n (d, u)
+  return F.smul (d, ofBits guess, v)
 
 /-- Whenever the discrete-logarithm adversary recovers `α`, `dlToCDHAdversary` outputs the valid
 Diffie–Hellman shared element `encode ((α * β) • g)`. -/
@@ -248,8 +249,9 @@ equals the challenge third element. -/
 def cdhToDDHDistinguisher
     (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool))
     (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool := do
-  let guess ← adversary n (input.1, input.2.1, input.2.2.1)
-  return decide (guess = input.2.2.2)
+  let (d, u, v, w) := input
+  let guess ← adversary n (d, u, v)
+  return decide (guess = w)
 
 /-- In the real DDH game, `cdhToDDHDistinguisher` simulates the CDH game exactly. -/
 @[simp] theorem ddhRealGame_cdhToDDHDistinguisher (setup : ℕ → PMF F.Desc)
@@ -529,13 +531,7 @@ natural-number exponents `r, s₁, s₂ : ℕ`, evaluate the encoded tuple corre
 def encodeDDHRerandomize
     (input : F.Desc × (List Bool × List Bool × List Bool) × ℕ × ℕ × ℕ) :
     List Bool × List Bool × List Bool :=
-  let d := input.1
-  let u := input.2.1.1
-  let v := input.2.1.2.1
-  let w := input.2.1.2.2
-  let r := input.2.2.1
-  let s₁ := input.2.2.2.1
-  let s₂ := input.2.2.2.2
+  let (d, (u, v, w), r, s₁, s₂) := input
   let g := F.encode d (F.generator d)
   (F.add (d, F.smul (d, r, u), F.smul (d, s₁, g)),
     F.add (d, v, F.smul (d, s₂, g)),
@@ -548,18 +544,18 @@ def encodeDDHRerandomize
 /-- `encodeDDHRerandomize` evaluates `ddhRerandomize` on encoded group elements. -/
 @[simp] theorem encodeDDHRerandomize_encode (d : F.Desc) (u v w : F.Carrier d) (r s₁ s₂ : ℕ) :
     F.encodeDDHRerandomize (d, (F.encode d u, F.encode d v, F.encode d w), r, s₁, s₂) =
-      let t := F.ddhRerandomize d u v w
+      let (u', v', w') := F.ddhRerandomize d u v w
         (r : ZMod (F.order d)) (s₁ : ZMod (F.order d)) (s₂ : ZMod (F.order d))
-      (F.encode d t.1, F.encode d t.2.1, F.encode d t.2.2) := by
+      (F.encode d u', F.encode d v', F.encode d w') := by
   simp only [encodeDDHRerandomize, ddhRerandomize, F.smul_encode, F.add_encode, Nat.cast_mul]
 
 /-- Evaluating `encodeDDHRerandomize` at `.val` of exponents in `ZMod (F.order d)` agrees with
 `ddhRerandomize`. -/
 theorem encodeDDHRerandomize_val (d : F.Desc) (u v w : F.Carrier d)
     (r s₁ s₂ : ZMod (F.order d)) :
     F.encodeDDHRerandomize (d, (F.encode d u, F.encode d v, F.encode d w), r.val, s₁.val, s₂.val) =
-      let t := F.ddhRerandomize d u v w r s₁ s₂
-      (F.encode d t.1, F.encode d t.2.1, F.encode d t.2.2) := by
+      let (u', v', w') := F.ddhRerandomize d u v w r s₁ s₂
+      (F.encode d u', F.encode d v', F.encode d w') := by
   simp only [encodeDDHRerandomize_encode, ZMod.natCast_zmod_val]
 
 /-- Word-level DDH tuple re-randomization is computable in polynomial time. -/
@@ -765,9 +761,10 @@ noncomputable def ddhRerandomizeGame (setup : ℕ → PMF F.Desc)
   let r ← PMF.uniformOfFintype (ZMod (F.order d))
   let s₁ ← PMF.uniformOfFintype (ZMod (F.order d))
   let s₂ ← PMF.uniformOfFintype (ZMod (F.order d))
+  let (u, v, w) := tuple d
   ProbComp.eval (distinguisher n
     (d, F.encodeDDHRerandomize
-      (d, (F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2),
+      (d, (F.encode d u, F.encode d v, F.encode d w),
         r.val, s₁.val, s₂.val)))
 
 /-- Re-randomizing any family of real DDH tuples `(α d • g, β d • g, (α d * β d) • g)` with
@@ -855,15 +852,15 @@ theorem DDH.ddhRerandomizeGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF
   exact (F.advantage_ddhRerandomizeGame_eq setup α β α' β' γ' distinguisher n hn).le
 
 /-- The worst-case DDH experiment on a fixed tuple family `tuple` (original): draw `d ← setup n`
-and give the encoded tuple `(d, encode (tuple d).1, encode (tuple d).2.1, encode (tuple d).2.2)`
-directly to `distinguisher`. -/
+and give the encoded tuple `(d, encode u, encode v, encode w)` directly to `distinguisher`. -/
 noncomputable def ddhWorstCaseGame (setup : ℕ → PMF F.Desc)
     (tuple : ∀ d : F.Desc, F.Carrier d × F.Carrier d × F.Carrier d)
     (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool)
     (n : ℕ) : Game := do
   let d ← setup n
+  let (u, v, w) := tuple d
   ProbComp.eval (distinguisher n
-    (d, F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2))
+    (d, F.encode d u, F.encode d v, F.encode d w))
 
 private noncomputable def ddhRerandomizeStep
     (tuple : ∀ d : F.Desc, F.Carrier d × F.Carrier d × F.Carrier d)
@@ -1110,8 +1107,9 @@ theorem computableInPolyTime_ddhIdealRefTuple :
     (tuple : ∀ d : F.Desc, F.Carrier d × F.Carrier d × F.Carrier d)
     (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) :
     F.ddhWorstCaseGame (fun _ => PMF.pure d) tuple distinguisher n =
+      let (u, v, w) := tuple d
       ProbComp.eval (distinguisher n
-        (d, F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2)) := by
+        (d, F.encode d u, F.encode d v, F.encode d w)) := by
   simp [ddhWorstCaseGame]
 
 /-- **Single-trial real DDH proximity**: on any fixed group `d` and any real DDH triple