From 25ec6c84bcc30c36c1f9b1dde8cf54911435fcf3 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 31 Oct 2026 10:06:57 +0000
Subject: [PATCH 1/3] refactor(Crypto): replace projection chains across
 Signature, Commitment, and Hash modules (#1764)

---
 .../Computational/CollisionResistant.lean     |  5 +-
 .../Computational/Commitment/Basic.lean       | 14 +++--
 .../Commitment/PublicOperations.lean          |  5 +-
 .../Computational/IndexedSignature.lean       | 14 +++--
 .../IndexedSignature/Counter.lean             | 10 ++--
 .../IndexedSignature/Seeded.lean              | 34 ++++++++-----
 .../Crypto/Computational/MerkleDamgard.lean   |  7 +--
 .../Crypto/Computational/MerkleSignature.lean | 10 ++--
 .../MerkleSignature/Security.lean             | 17 +++++--
 .../Computational/OneWayToSignature.lean      |  8 +--
 .../Computational/PedersenCommitment.lean     | 21 +++++---
 .../PedersenCommitment/ProbComp.lean          |  3 +-
 .../PedersenCommitment/PublicOperations.lean  | 13 +++--
 .../Crypto/Computational/Signature.lean       | 15 +++---
 .../Crypto/Computational/TreeSignature.lean   | 51 ++++++++++++-------
 .../Protocols/Signature/RandomOracle.lean     |  8 +--
 16 files changed, 152 insertions(+), 83 deletions(-)

diff --git a/Complexity/Crypto/Computational/CollisionResistant.lean b/Complexity/Crypto/Computational/CollisionResistant.lean
index 4ab684caeb..a079a5389b 100644
--- a/Complexity/Crypto/Computational/CollisionResistant.lean
+++ b/Complexity/Crypto/Computational/CollisionResistant.lean
@@ -359,7 +359,7 @@ theorem computableInPolyTime_isCollision
       (encPair encUnary encBits) encBool) :
     ComputableInPolyTime
       (fun p : ℕ × List Bool × List Bool × List Bool =>
-        isCollision H valid p.1 p.2.1 p.2.2.1 p.2.2.2)
+        isCollision H valid p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
       (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool := by
   have hv₁ : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool × List Bool =>
       valid p.1 p.2.2.1) (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool :=
@@ -493,7 +493,8 @@ theorem CollisionResistantOn.of_extract
     (hCR : CollisionResistantOn H₂ valid₂)
     (extract : ℕ → List Bool → List Bool → List Bool → List Bool × List Bool)
     (hextract : ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × List Bool => extract p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (fun p : ℕ × List Bool × List Bool × List Bool =>
+        extract p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
       (encPair encUnary (encPair encBits (encPair encBits encBits)))
       (encPair encBits encBits))
     (himp : ∀ᶠ n in Filter.atTop, ∀ k, k.length = n → ∀ m₁ m₂,
diff --git a/Complexity/Crypto/Computational/Commitment/Basic.lean b/Complexity/Crypto/Computational/Commitment/Basic.lean
index e7abb15ec2..107799cdfa 100644
--- a/Complexity/Crypto/Computational/Commitment/Basic.lean
+++ b/Complexity/Crypto/Computational/Commitment/Basic.lean
@@ -108,9 +108,10 @@ noncomputable def CommitmentScheme.hidingForKey {Key : Type}
     (S : CommitmentScheme Key) (k : Key)
     (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : Game := do
   let choice ← ProbComp.eval (adversary.choose n (S.encodeKey k))
+  let msgs := choice.1
   let msg := open Classical in
-    if bit ∧ S.ValidMessage k choice.1.1 ∧ S.ValidMessage k choice.1.2 then choice.1.2
-    else choice.1.1
+    if bit ∧ S.ValidMessage k msgs.1 ∧ S.ValidMessage k msgs.2 then msgs.2
+    else msgs.1
   let co ← S.commitDist k msg
   ProbComp.eval (adversary.guess n choice.2 co.1)
 
@@ -185,9 +186,12 @@ theorem CommitmentScheme.StatisticalHiding.computationalHiding {Key : Type}
 openings `(m₀, o₀)` and `(m₁, o₁)` are accepted by `S.verify k` for the commitment string `c`. -/
 def CommitmentScheme.isBindingCollision {Key : Type} (S : CommitmentScheme Key) (k : Key)
     (out : List Bool × (List Bool × List Bool) × (List Bool × List Bool)) : Bool :=
-  decide (out.2.1.1 ≠ out.2.2.1) &&
-    S.verify k out.2.1.1 out.1 out.2.1.2 &&
-    S.verify k out.2.2.1 out.1 out.2.2.2
+  let openings := out.2
+  let open₀ := openings.1
+  let open₁ := openings.2
+  decide (open₀.1 ≠ open₁.1) &&
+    S.verify k open₀.1 out.1 open₀.2 &&
+    S.verify k open₁.1 out.1 open₁.2
 
 /-- The commitment binding experiment ([BonehShoup2023], Section 8.12, p. 344, and
 Definition 8.8): draw `k ← keyDist n`, give `S.encodeKey k` to `adversary`, and accept when the
diff --git a/Complexity/Crypto/Computational/Commitment/PublicOperations.lean b/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
index 82322e34e8..01875e6722 100644
--- a/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
+++ b/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
@@ -57,11 +57,12 @@ structure PublicOperations {Key : Type} (S : CommitmentScheme Key) where
   map_commit : ∀ k m, (randomness k).map (commit k m) = S.commitDist k m
   /-- Deterministic evaluation is polynomial-time in the public key, message and randomness word. -/
   commit_polyTime : ComputableInPolyTime
-    (fun p : Key × List Bool × List Bool => commit p.1 p.2.1 p.2.2)
+    (fun p : Key × List Bool × List Bool => commit p.1 (Prod.fst p.2) (Prod.snd p.2))
     (encPair S.encodeKey (encPair encBits encBits)) (encPair encBits encBits)
   /-- Verification is polynomial-time in the public key, message, commitment and opening words. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : Key × List Bool × List Bool × List Bool => S.verify p.1 p.2.1 p.2.2.1 p.2.2.2)
+    (fun p : Key × List Bool × List Bool × List Bool =>
+      S.verify p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
     (encPair S.encodeKey (encPair encBits (encPair encBits encBits))) encBool
 
 namespace PublicOperations
diff --git a/Complexity/Crypto/Computational/IndexedSignature.lean b/Complexity/Crypto/Computational/IndexedSignature.lean
index 6e079b1753..cb656f876a 100644
--- a/Complexity/Crypto/Computational/IndexedSignature.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature.lean
@@ -101,10 +101,11 @@ structure IndexedSignatureScheme where
   keyGen_ppt : IsPPTOn encUnary (encPair encBits encBits) keyGen
   /-- Signing is uniformly strict PPT in the secret key, the unary index and the message. -/
   sign_ppt : IsPPTOn (encPair encBits (encPair encUnary encBits)) encBits
-    (fun p => sign p.1 p.2.1 p.2.2)
+    (fun p => sign p.1 (Prod.fst p.2) (Prod.snd p.2))
   /-- Verification is computable in plain polynomial time on `(pk, u, msg, sig)`. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : List Bool × ℕ × List Bool × List Bool => verify p.1 p.2.1 p.2.2.1 p.2.2.2)
+    (fun p : List Bool × ℕ × List Bool × List Bool =>
+      verify p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
     (encPair encBits (encPair encUnary (encPair encBits encBits))) encBool
   /-- Every signature produced at an index below the capacity, under a supported key pair, is
   accepted. -/
@@ -142,8 +143,10 @@ def indexedEufCmaGame (S : IndexedSignatureScheme) (adversary : IndexedForger) (
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.indexedSigningOracle n keys.2)) (adversary n keys.1)).run []
-  return !out.2.contains (out.1.1, out.1.2.1) &&
-    S.verify keys.1 out.1.1 out.1.2.1 out.1.2.2
+  let u_msig := out.1
+  let msig := u_msig.2
+  return !out.2.contains (u_msig.1, msig.1) &&
+    S.verify keys.1 u_msig.1 msig.1 msig.2
 
 /-- Running an oracle-PPT indexed forger against `indexedSigningOracle` is uniformly strict PPT in
 the unary security parameter, the public key and the secret key. -/
@@ -155,7 +158,8 @@ theorem isPPTOn_run_indexedSigningOracle (S : IndexedSignatureScheme) {adversary
       (fun caller : ℕ × (List Bool × List Bool) =>
         (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
-            (S.indexedSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run
+            (S.indexedSigningOracle caller.1 (Prod.snd caller.2)))
+          (adversary caller.1 (Prod.fst caller.2))).run
           []) := by
   obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le
   have hcap := S.capacity_polyTime
diff --git a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
index 9088156c1f..8bd2f49063 100644
--- a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
@@ -111,7 +111,9 @@ def counterEufCmaGame (adversary : Forger) (n : ℕ) : ProbComp Bool := do
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.counterSigningOracle n keys.2)) (adversary n keys.1)).run (0, [])
-  return !out.2.2.contains out.1.1 && S.counterVerify keys.1 out.1.1 out.1.2
+  let msig := out.1
+  let state := out.2
+  return !state.2.contains msig.1 && S.counterVerify keys.1 msig.1 msig.2
 
 variable {S}
 
@@ -150,7 +152,8 @@ theorem isPPTOn_run_counterSigningOracle {adversary : Forger}
       (fun caller : ℕ × (List Bool × List Bool) =>
         (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
-            (S.counterSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run
+            (S.counterSigningOracle caller.1 (Prod.snd caller.2)))
+          (adversary caller.1 (Prod.fst caller.2))).run
           (0, [])) := by
   obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le
   have hcap := S.capacity_polyTime
@@ -280,7 +283,8 @@ def counterForger (bound : ℕ → ℕ → ℕ) (adversary : Forger) : IndexedFo
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k)))
       (S.counterHandler n bound)) (adversary n pk)).run 0
-  return ((requestDecoder.decode out.1.2).1, out.1.1, (requestDecoder.decode out.1.2).2)
+  let msig := out.1
+  return ((requestDecoder.decode msig.2).1, msig.1, (requestDecoder.decode msig.2).2)
 
 /-! ### Exact simulation -/
 
diff --git a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
index 9db059d144..dd1d2f64b9 100644
--- a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
@@ -69,10 +69,11 @@ structure Seeded (S : IndexedSignatureScheme) where
   eval_keyGen : ∀ n length, keyGenBudget n ≤ length →
     ProbComp.eval (S.keyGen n) = (BitString.uniformList length).map (keyGenWith n)
   signWith_polyTime : ComputableInPolyTime
-    (fun p : (List Bool × ℕ × List Bool) × List Bool => signWith p.1.1 p.1.2.1 p.1.2.2 p.2)
+    (fun p : (List Bool × ℕ × List Bool) × List Bool =>
+      signWith (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) (Prod.snd (Prod.snd p.1)) p.2)
     (encPair (encPair encBits (encPair encUnary encBits)) encBits) encBits
   signBudget_polyTime : ComputableInPolyTime
-    (fun p : List Bool × ℕ × List Bool => signBudget p.1 p.2.1 p.2.2)
+    (fun p : List Bool × ℕ × List Bool => signBudget p.1 (Prod.fst p.2) (Prod.snd p.2))
     (encPair encBits (encPair encUnary encBits)) encUnary
   signWith_mem_support : ∀ sk u msg coins,
     signWith sk u msg coins ∈ (ProbComp.eval (S.sign sk u msg)).support
@@ -112,9 +113,12 @@ theorem exists_signWith (S : IndexedSignatureScheme) :
       ComputableInPolyTime (fun p : (List Bool × ℕ × List Bool) × List Bool => signWith p.1 p.2)
         (encPair (encPair encBits (encPair encUnary encBits)) encBits) encBits ∧
       ComputableInPolyTime budget (encPair encBits (encPair encUnary encBits)) encUnary ∧
-      (∀ a coins, signWith a coins ∈ (ProbComp.eval (S.sign a.1 a.2.1 a.2.2)).support) ∧
+      (∀ a coins,
+        let um := a.2
+        signWith a coins ∈ (ProbComp.eval (S.sign a.1 um.1 um.2)).support) ∧
       ∀ a length, budget a ≤ length →
-        ProbComp.eval (S.sign a.1 a.2.1 a.2.2) =
+        let um := a.2
+        ProbComp.eval (S.sign a.1 um.1 um.2) =
           (BitString.uniformList length).map (signWith a) := by
   obtain ⟨c, d, evaluate, hpoly, hsupport, hlaw⟩ :=
     IsPPTOn.exists_total_seeded_evaluator S.sign_ppt
@@ -124,21 +128,27 @@ theorem exists_signWith (S : IndexedSignatureScheme) :
 /-- The seeded algorithms of any indexed scheme, read off its strict-PPT certificates. -/
 noncomputable def seeded (S : IndexedSignatureScheme) : S.Seeded :=
   let hk := S.exists_keyGenWith
+  let hk_spec := hk.choose_spec.choose_spec
+  let hk_rest := hk_spec.2
+  let hk_laws := hk_rest.2
   let hs := S.exists_signWith
+  let hs_spec := hs.choose_spec.choose_spec
+  let hs_rest := hs_spec.2
+  let hs_laws := hs_rest.2
   { keyGenWith := hk.choose
     keyGenBudget := hk.choose_spec.choose
     signWith := fun sk u msg coins => hs.choose (sk, u, msg) coins
     signBudget := fun sk u msg => hs.choose_spec.choose (sk, u, msg)
-    keyGenWith_polyTime := hk.choose_spec.choose_spec.1
-    keyGenBudget_polyTime := hk.choose_spec.choose_spec.2.1
-    keyGenWith_mem_support := hk.choose_spec.choose_spec.2.2.1
-    eval_keyGen := hk.choose_spec.choose_spec.2.2.2
-    signWith_polyTime := hs.choose_spec.choose_spec.1
-    signBudget_polyTime := hs.choose_spec.choose_spec.2.1
+    keyGenWith_polyTime := hk_spec.1
+    keyGenBudget_polyTime := hk_rest.1
+    keyGenWith_mem_support := hk_laws.1
+    eval_keyGen := hk_laws.2
+    signWith_polyTime := hs_spec.1
+    signBudget_polyTime := hs_rest.1
     signWith_mem_support := fun sk u msg coins =>
-      hs.choose_spec.choose_spec.2.2.1 (sk, u, msg) coins
+      hs_laws.1 (sk, u, msg) coins
     eval_sign := fun sk u msg length h =>
-      hs.choose_spec.choose_spec.2.2.2 (sk, u, msg) length h }
+      hs_laws.2 (sk, u, msg) length h }
 
 end IndexedSignatureScheme
 
diff --git a/Complexity/Crypto/Computational/MerkleDamgard.lean b/Complexity/Crypto/Computational/MerkleDamgard.lean
index dcfca8f90d..96683c5b95 100644
--- a/Complexity/Crypto/Computational/MerkleDamgard.lean
+++ b/Complexity/Crypto/Computational/MerkleDamgard.lean
@@ -296,7 +296,7 @@ theorem computableInPolyTime_chainTrace
     (hlen : ∀ k x, x.length = 2 * k.length → (h k x).length = k.length) :
     ComputableInPolyTime
       (fun p : List Bool × List Bool × List (List Bool) =>
-        chainTrace h p.1 p.2.1 p.2.2)
+        chainTrace h p.1 (Prod.fst p.2) (Prod.snd p.2))
       (encPair encBits (encPair encBits (encList encBits)))
       (encPair encBits (encList encBits)) :=
   .of_tidy (computableTidilyInPolyTime_chainTrace hh.tidy hlen
@@ -348,7 +348,8 @@ theorem computableInPolyTime_extractChainCollision
     (hlen : ∀ k x, x.length = 2 * k.length → (h k x).length = k.length) :
     ComputableInPolyTime
       (fun p : List Bool × List Bool × List (List Bool) × List (List Bool) =>
-        extractChainCollision h p.1 p.2.1 p.2.2.1 p.2.2.2)
+        extractChainCollision h p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2))
+          (Prod.snd (Prod.snd p.2)))
       (encPair encBits (encPair encBits (encPair (encList encBits) (encList encBits))))
       (encPair encBits encBits) :=
   .of_tidy (computableTidilyInPolyTime_extractChainCollision hh.tidy hlen
@@ -732,7 +733,7 @@ theorem computableInPolyTime_extractMerkleDamgardCollision
     (hlen : ∀ k x, x.length = 2 * k.length → (h k x).length = k.length) :
     ComputableInPolyTime
       (fun p : List Bool × List Bool × List Bool =>
-        extractMerkleDamgardCollision h p.1 p.2.1 p.2.2)
+        extractMerkleDamgardCollision h p.1 (Prod.fst p.2) (Prod.snd p.2))
       (encPair encBits (encPair encBits encBits))
       (encPair encBits encBits) := by
   apply ComputableInPolyTime.of_tidy
diff --git a/Complexity/Crypto/Computational/MerkleSignature.lean b/Complexity/Crypto/Computational/MerkleSignature.lean
index 77a0155992..0ee501651a 100644
--- a/Complexity/Crypto/Computational/MerkleSignature.lean
+++ b/Complexity/Crypto/Computational/MerkleSignature.lean
@@ -131,8 +131,9 @@ signature verifies on `H k msg`. -/
 def verify (pk : List Bool) (u : ℕ) (msg sig : List Bool) : Bool :=
   let k := unframe pk
   let forged := signatureDecoder.decode sig
-  merkleVerify H k (depth k.length) (dropFrame pk) u forged.1 forged.2.2 &&
-    S.verify forged.1 (H k msg) forged.2.1
+  let otsPath := forged.2
+  merkleVerify H k (depth k.length) (dropFrame pk) u forged.1 otsPath.2 &&
+    S.verify forged.1 (H k msg) otsPath.1
 
 /-! ### Completeness -/
 
@@ -248,7 +249,7 @@ include hH hlen in
 /-- Merkle signing is uniformly strict PPT. -/
 theorem isPPTOn_sign :
     IsPPTOn (encPair encBits (encPair encUnary encBits)) encBits
-      (fun p => sign S H p.1 p.2.1 p.2.2) := by
+      (fun p => sign S H p.1 (Prod.fst p.2) (Prod.snd p.2)) := by
   let E := encPair encBits (encPair encUnary encBits)
   have hdec : ComputableTidilyInPolyTime (fun p : List Bool × ℕ × List Bool =>
       secretKeyDecoder.decode p.1) E (encPair encBits (encList (encPair encBits encBits))) :=
@@ -289,7 +290,8 @@ include hH hlen hcap in
 /-- Merkle verification is computable in polynomial time. -/
 theorem computableInPolyTime_verify :
     ComputableInPolyTime
-      (fun p : List Bool × ℕ × List Bool × List Bool => verify S H depth p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (fun p : List Bool × ℕ × List Bool × List Bool =>
+        verify S H depth p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
       (encPair encBits (encPair encUnary (encPair encBits encBits))) encBool := by
   apply ComputableInPolyTime.of_tidy
   let E := encPair encBits (encPair encUnary (encPair encBits encBits))
diff --git a/Complexity/Crypto/Computational/MerkleSignature/Security.lean b/Complexity/Crypto/Computational/MerkleSignature/Security.lean
index 3e4dae0a3b..57f1fa5a54 100644
--- a/Complexity/Crypto/Computational/MerkleSignature/Security.lean
+++ b/Complexity/Crypto/Computational/MerkleSignature/Security.lean
@@ -103,13 +103,16 @@ keys `keys`: a collision in the tree if the forged verification key is not the o
 and otherwise the forged message with a message signed at leaf `u` with the same digest. -/
 def collisionOf (k : List Bool) (keys : List (List Bool × List Bool))
     (out : (ℕ × List Bool × List Bool) × List (ℕ × List Bool)) : List Bool × List Bool :=
-  let u := out.1.1
-  let forged := signatureDecoder.decode out.1.2.2
+  let u_msig := out.1
+  let u := u_msig.1
+  let msig := u_msig.2
+  let forged := signatureDecoder.decode msig.2
+  let otsPath := forged.2
   let vks := keys.map Prod.fst
   if forged.1 == vks.getD u [] then
-    (out.1.2.1, (out.2.find? fun e => e.1 == u && H k e.2 == H k out.1.2.1).elim [] Prod.snd)
+    (msig.1, (out.2.find? fun e => e.1 == u && H k e.2 == H k msig.1).elim [] Prod.snd)
   else
-    extractMerkleCollision H k forged.1 (vks.getD u []) u forged.2.2 (merklePath H k vks u)
+    extractMerkleCollision H k forged.1 (vks.getD u []) u otsPath.2 (merklePath H k vks u)
 
 /-- The collision finder: given the hash key `k`, generate the one-time keys, answer the forger's
 signing queries honestly, and return `collisionOf` its forgery. -/
@@ -166,7 +169,11 @@ noncomputable def oneTimeForgerAt (bound : ℕ → ℕ) (adversary : IndexedForg
     (ProbOracleComp.handler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j)))
       (plantedHandler S H depth n setup.1 setup.2 i (bound n)))
     (adversary n (publicKey H setup.1 setup.2))).run []
-  return (H setup.1 out.1.2.1, (signatureDecoder.decode out.1.2.2).2.1)
+  let u_msig := out.1
+  let msig := u_msig.2
+  let forged := signatureDecoder.decode msig.2
+  let otsPath := forged.2
+  return (H setup.1 msig.1, otsPath.1)
 
 /-- The one-time forger: plant the challenge at a uniform leaf. -/
 noncomputable def oneTimeForger (bound : ℕ → ℕ) (adversary : IndexedForger) : Forger :=
diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean
index a3cc11acb0..8aba6b53dd 100644
--- a/Complexity/Crypto/Computational/OneWayToSignature.lean
+++ b/Complexity/Crypto/Computational/OneWayToSignature.lean
@@ -356,7 +356,8 @@ theorem isPPTOn_lamportSign :
 theorem computableInPolyTime_lamportVerify {f : List Bool → List Bool}
     (hf : ComputableInPolyTime f encBits encBits) :
     ComputableInPolyTime
-      (fun p : List Bool × List Bool × List Bool => lamportVerify f p.1 p.2.1 p.2.2)
+      (fun p : List Bool × List Bool × List Bool =>
+        lamportVerify f p.1 (Prod.fst p.2) (Prod.snd p.2))
       (encPair encBits (encPair encBits encBits)) encBool := by
   have hf := hf.tidy
   refine .of_tidy ?_
@@ -512,7 +513,7 @@ noncomputable def lamportSimKeys (f : List Bool → List Bool) (n j : ℕ) (y :
 theorem isPPTOn_lamportSimKeys {f : List Bool → List Bool}
     (hf : ComputableInPolyTime f encBits encBits) :
     IsPPTOn (encPair (encPair encUnary encBits) encUnary) (encPair encBits encBits)
-      (fun q : (ℕ × List Bool) × ℕ => lamportSimKeys f q.1.1 q.2 q.1.2) := by
+      (fun q : (ℕ × List Bool) × ℕ => lamportSimKeys f (Prod.fst q.1) q.2 (Prod.snd q.1)) := by
   have hf := hf.tidy
   unfold lamportSimKeys
   have hfront : IsPPTOn (encPair (encPair encUnary encBits) encUnary) (encList encBits)
@@ -583,7 +584,8 @@ noncomputable def lamportInverter (f : List Bool → List Bool)
     let out ← (OracleComp.interpret
       (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
         ((lamportScheme f hf).oneTimeSigningOracle keys.2)) (adversary n keys.1)).run []
-    return (frames out.1.2).getD (j / 2) []
+    let msig := out.1
+    return (frames msig.2).getD (j / 2) []
   else
     return []
 
diff --git a/Complexity/Crypto/Computational/PedersenCommitment.lean b/Complexity/Crypto/Computational/PedersenCommitment.lean
index 0c6367c289..0d75bc32bc 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment.lean
@@ -182,9 +182,11 @@ theorem pedersenCommit_smul_generator_eq_iff (d : F.Desc) (α m₀ r₀ m₁ r
 /-- Pedersen commitment on encoded group elements: given `(d, encode h, m, r)`, compute
 `encode (m • g + r • h)`. -/
 def encodePedersenCommit (input : F.Desc × List Bool × ℕ × ℕ) : List Bool :=
+  let hmr := input.2
+  let mr := hmr.2
   F.add (input.1,
-    F.smul (input.1, input.2.2.1, F.encode input.1 (F.generator input.1)),
-    F.smul (input.1, input.2.2.2, input.2.1))
+    F.smul (input.1, mr.1, F.encode input.1 (F.generator input.1)),
+    F.smul (input.1, mr.2, hmr.1))
 
 /-- `encodePedersenCommit` computes `F.encode d (F.pedersenCommit d h m r)` on encoded group
 elements. -/
@@ -510,9 +512,13 @@ Section 10.6.1, Fact 10.3). -/
 theorem pedersenExtractNat_eq_of_isBindingCollision (d : F.Desc) (α : ZMod (F.order d))
     {out : List Bool × (List Bool × List Bool) × (List Bool × List Bool)}
     (hcoll : F.pedersenScheme.isBindingCollision ⟨d, α • F.generator d⟩ out = true) :
+    let openings := out.2
+    let open₀ := openings.1
+    let open₁ := openings.2
     (pedersenExtractNat (F.order d)
-      (ofBits out.2.1.1) (ofBits out.2.1.2)
-      (ofBits out.2.2.1) (ofBits out.2.2.2) : ZMod (F.order d)) = α := by
+      (ofBits open₀.1) (ofBits open₀.2)
+      (ofBits open₁.1) (ofBits open₁.2) : ZMod (F.order d)) = α := by
+  dsimp only
   simp only [CommitmentScheme.isBindingCollision, pedersenScheme, pedersenVerify,
     Bool.and_eq_true, decide_eq_true_eq] at hcoll
   rcases hcoll with ⟨⟨hne, ⟨hm₀_lt, hm₀_bits⟩, hc₀⟩, ⟨hm₁_lt, hm₁_bits⟩, hc₁⟩
@@ -548,9 +554,12 @@ def pedersenToDLAdversary
       ProbComp (List Bool × (List Bool × List Bool) × (List Bool × List Bool)))
     (n : ℕ) (input : F.Desc × List Bool) : ProbComp (List Bool) := do
   let out ← adversary n (encPair F.encDesc encBits input)
+  let openings := out.2
+  let open₀ := openings.1
+  let open₁ := openings.2
   return (pedersenExtractNat (F.order input.1)
-    (ofBits out.2.1.1) (ofBits out.2.1.2)
-    (ofBits out.2.2.1) (ofBits out.2.2.2)).bits
+    (ofBits open₀.1) (ofBits open₀.2)
+    (ofBits open₁.1) (ofBits open₁.2)).bits
 
 /-- **Exact binding-to-discrete-logarithm reduction** ([BonehShoup2023], Section 10.6.1,
 Theorem 10.4, pp. 414–415; [Pedersen1991], Section 3, Theorem 3.1): for every security parameter
diff --git a/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean b/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
index a5d8b70dc6..73d294ec48 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
@@ -68,7 +68,8 @@ public key encoding, and message word. -/
 theorem isPPTOn_pedersenCommitProb :
     IsPPTOn (encPair encUnary (encPair F.pedersenScheme.encodeKey encBits))
       (encPair encBits encBits)
-      (fun p : ℕ × F.PedersenKey × List Bool => F.pedersenCommitProb p.1 p.2.1 p.2.2) := by
+      (fun p : ℕ × F.PedersenKey × List Bool =>
+        F.pedersenCommitProb p.1 (Prod.fst p.2) (Prod.snd p.2)) := by
   let E := encPair encUnary (encPair F.pedersenScheme.encodeKey encBits)
   have hn := ComputableInPolyTime.fst encUnary (encPair F.pedersenScheme.encodeKey encBits)
   have hrest := ComputableInPolyTime.snd encUnary (encPair F.pedersenScheme.encodeKey encBits)
diff --git a/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean b/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
index a52a22729a..c64c52c210 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
@@ -52,10 +52,13 @@ opening words. The public element is already encoded; no discrete logarithm or s
 value is supplied to this algorithm. -/
 def encodePedersenVerify
     (input : (F.Desc × List Bool) × List Bool × List Bool × List Bool) : Bool :=
-  decide (ofBits input.2.1 < F.order input.1.1) &&
-    decide ((ofBits input.2.1).bits = input.2.1) &&
+  let dh := input.1
+  let mco := input.2
+  let co := mco.2
+  decide (ofBits mco.1 < F.order dh.1) &&
+    decide ((ofBits mco.1).bits = mco.1) &&
     decide (F.encodePedersenCommit
-      (input.1.1, input.1.2, ofBits input.2.1, ofBits input.2.2.2) = input.2.2.1)
+      (dh.1, dh.2, ofBits mco.1, ofBits co.2) = co.1)
 
 /-- The encoded verifier computes exactly the verifier used by `pedersenScheme`. -/
 @[simp]
@@ -109,7 +112,7 @@ noncomputable def pedersenPublicOperations : F.pedersenScheme.PublicOperations w
       (encPair encBits (encPair encBits encBits))
     have hv := F.computableInPolyTime_encodePedersenVerify.comp (hpublic.prod hrest)
     convert hv using 1
-    funext p
-    exact (F.encodePedersenVerify_encode p.1.1 p.1.2 p.2.1 p.2.2.1 p.2.2.2).symm
+    funext ⟨⟨d, h⟩, m, c, o⟩
+    exact (F.encodePedersenVerify_encode d h m c o).symm
 
 end Cslib.Crypto.PrimeOrderGroupFamily
diff --git a/Complexity/Crypto/Computational/Signature.lean b/Complexity/Crypto/Computational/Signature.lean
index 204b91866f..25ff20e4d0 100644
--- a/Complexity/Crypto/Computational/Signature.lean
+++ b/Complexity/Crypto/Computational/Signature.lean
@@ -97,7 +97,7 @@ structure SignatureScheme where
   sign_ppt : IsPPTOn (encPair encBits encBits) encBits (fun p => sign p.1 p.2)
   /-- Verification is computable in plain polynomial time on `(pk, msg, sig)`. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : List Bool × List Bool × List Bool => verify p.1 p.2.1 p.2.2)
+    (fun p : List Bool × List Bool × List Bool => verify p.1 (Prod.fst p.2) (Prod.snd p.2))
     (encPair encBits (encPair encBits encBits)) encBool
   /-- Every signature produced by `sign` on an `n`-bit message under a supported key pair at
   security parameter `n` is accepted by `verify`. -/
@@ -173,8 +173,9 @@ def eufCmaGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) :
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.signingOracle keys.2)) (adversary n keys.1)).run []
-  return (out.1.1.length == n) && !out.2.contains out.1.1 &&
-    S.verify keys.1 out.1.1 out.1.2
+  let msig := out.1
+  return (msig.1.length == n) && !out.2.contains msig.1 &&
+    S.verify keys.1 msig.1 msig.2
 
 attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Run the complete EUF-CMA experiment on its unary security parameter for any oracle-PPT
@@ -275,8 +276,9 @@ def eufOneTimeGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) :
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.oneTimeSigningOracle keys.2)) (adversary n keys.1)).run []
-  return (out.1.1.length == n) && !out.2.contains out.1.1 &&
-    S.verify keys.1 out.1.1 out.1.2
+  let msig := out.1
+  return (msig.1.length == n) && !out.2.contains msig.1 &&
+    S.verify keys.1 msig.1 msig.2
 
 /-- Running an oracle-PPT forger against `oneTimeSigningOracle` is uniformly strict PPT in the
 unary security parameter, public key, and secret key. -/
@@ -288,7 +290,8 @@ theorem isPPTOn_run_oneTimeSigningOracle (S : SignatureScheme) {adversary : Forg
       (fun caller : ℕ × (List Bool × List Bool) =>
         (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
-            (S.oneTimeSigningOracle caller.2.2)) (adversary caller.1 caller.2.1)).run []) := by
+            (S.oneTimeSigningOracle (Prod.snd caller.2)))
+          (adversary caller.1 (Prod.fst caller.2))).run []) := by
   obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le
   have hhandler : IsPPTOn
       (encPair (encPair encUnary (encPair encBits encBits))
diff --git a/Complexity/Crypto/Computational/TreeSignature.lean b/Complexity/Crypto/Computational/TreeSignature.lean
index 712a26cca1..6da24f6d78 100644
--- a/Complexity/Crypto/Computational/TreeSignature.lean
+++ b/Complexity/Crypto/Computational/TreeSignature.lean
@@ -113,8 +113,10 @@ abbrev CertState := List Bool × (List Bool × List Bool) × List (List Bool ×
 to it. -/
 def certifyStep (n : ℕ) (k : List Bool) (state : CertState) (a : Bool) : CertState :=
   let child := nodeKey S T coins n k (state.1 ++ [a])
+  let keyCerts := state.2
+  let nodeKeys := keyCerts.1
   (state.1 ++ [a], child,
-    state.2.2 ++ [(child.1, signAt S T coins k state.1 state.2.1.2 a.toNat child.1)])
+    keyCerts.2 ++ [(child.1, signAt S T coins k state.1 nodeKeys.2 a.toNat child.1)])
 
 /-- Certify the path `bits` from the root. -/
 def certify (n : ℕ) (k bits : List Bool) : CertState :=
@@ -139,7 +141,10 @@ def keyDecoder : Decoder (encPair encUnary encBits) := Decoder.unary.pair Decode
 leaf's last bit. -/
 def signWithLeaf (n : ℕ) (k leaf msg : List Bool) : List Bool :=
   let c := certify S T coins n k leaf.dropLast
-  encodeSignature leaf c.2.2 (signAt S T coins k c.1 c.2.1.2 (leaf.getLastD false).toNat msg)
+  let keyCerts := c.2
+  let nodeKeys := keyCerts.1
+  encodeSignature leaf keyCerts.2
+    (signAt S T coins k c.1 nodeKeys.2 (leaf.getLastD false).toNat msg)
 
 /-! ### The algorithms -/
 
@@ -161,7 +166,8 @@ noncomputable def sign (sk msg : List Bool) : ProbComp (List Bool) := do
 public key, and move to the child. -/
 def verifyStep (state : Bool × List Bool) (e : Bool × (List Bool × List Bool)) :
     Bool × List Bool :=
-  (state.1 && S.verify state.2 e.1.toNat e.2.1 e.2.2, e.2.1)
+  let cert := e.2
+  (state.1 && S.verify state.2 e.1.toNat cert.1 cert.2, cert.1)
 
 /-- Verification: the leaf has length `depth n` with `depth n - 1` certificates, the certificates
 chain from the root along the leaf's prefix, and the last certified key signs `msg` at the leaf's
@@ -169,9 +175,10 @@ last bit. -/
 def verify (pk msg sig : List Bool) : Bool :=
   let p := keyDecoder.decode pk
   let s := signatureDecoder.decode sig
-  let r := (s.1.dropLast.zip s.2.1).foldl (verifyStep S) (true, p.2)
-  (s.1.length == depth p.1) && (s.2.1.length + 1 == depth p.1) && r.1 &&
-    S.verify r.2 (s.1.getLastD false).toNat msg s.2.2
+  let certsLast := s.2
+  let r := (s.1.dropLast.zip certsLast.1).foldl (verifyStep S) (true, p.2)
+  (s.1.length == depth p.1) && (certsLast.1.length + 1 == depth p.1) && r.1 &&
+    S.verify r.2 (s.1.getLastD false).toNat msg certsLast.2
 
 /-! ### Completeness -/
 
@@ -185,10 +192,12 @@ theorem certify_append (n : ℕ) (k bits : List Bool) (a : Bool) :
 /-- The chain reaches the node `bits` with its key, issues one certificate per bit, and its
 certificates verify from the root when both indices are below the capacity. -/
 theorem certify_spec (n : ℕ) (hcap : 2 ≤ S.capacity n) (k bits : List Bool) :
-    (certify S T coins n k bits).1 = bits ∧
-      (certify S T coins n k bits).2.1 = nodeKey S T coins n k bits ∧
-      (certify S T coins n k bits).2.2.length = bits.length ∧
-      (bits.zip (certify S T coins n k bits).2.2).foldl (verifyStep S)
+    let c := certify S T coins n k bits
+    let keyCerts := c.2
+    c.1 = bits ∧
+      keyCerts.1 = nodeKey S T coins n k bits ∧
+      keyCerts.2.length = bits.length ∧
+      (bits.zip keyCerts.2).foldl (verifyStep S)
         (true, (nodeKey S T coins n k []).1) = (true, (nodeKey S T coins n k bits).1) := by
   induction bits using List.reverseRecOn with
   | nil => simp [certify]
@@ -260,13 +269,14 @@ local notation "encCertState" =>
   encPair encBits (encPair (encPair encBits encBits) (encList (encPair encBits encBits)))
 
 variable (hcoins : ComputableInPolyTime
-    (fun p : List Bool × List Bool × ℕ => coins p.1 p.2.1 p.2.2)
+    (fun p : List Bool × List Bool × ℕ => coins p.1 (Prod.fst p.2) (Prod.snd p.2))
     (encPair encBits (encPair encBits encUnary)) encBits)
 
 include hcoins in
 /-- Node keys are computable in polynomial time from the parameter, the secret and the path. -/
 theorem computableInPolyTime_nodeKey :
-    ComputableInPolyTime (fun p : (ℕ × List Bool) × List Bool => nodeKey S T coins p.1.1 p.1.2 p.2)
+    ComputableInPolyTime
+      (fun p : (ℕ × List Bool) × List Bool => nodeKey S T coins (Prod.fst p.1) (Prod.snd p.1) p.2)
       (encPair (encPair encUnary encBits) encBits) (encPair encBits encBits) := by
   have hkg := T.keyGenWith_polyTime
   have hbudget := T.keyGenBudget_polyTime
@@ -278,7 +288,8 @@ include hcoins in
 theorem computableInPolyTime_signAt :
     ComputableInPolyTime
       (fun p : (List Bool × List Bool × List Bool) × ℕ × List Bool =>
-        signAt S T coins p.1.1 p.1.2.1 p.1.2.2 p.2.1 p.2.2)
+        signAt S T coins (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) (Prod.snd (Prod.snd p.1))
+          (Prod.fst p.2) (Prod.snd p.2))
       (encPair (encPair encBits (encPair encBits encBits)) (encPair encUnary encBits)) encBits := by
   have hsg := T.signWith_polyTime
   have hbudget := T.signBudget_polyTime
@@ -290,7 +301,8 @@ include hcoins in
 theorem computableInPolyTime_certifyStep :
     ComputableInPolyTime
       (fun p : ((ℕ × List Bool) × CertState) × Bool =>
-        certifyStep S T coins p.1.1.1 p.1.1.2 p.1.2 p.2)
+        certifyStep S T coins (Prod.fst (Prod.fst p.1)) (Prod.snd (Prod.fst p.1))
+          (Prod.snd p.1) p.2)
       (encPair (encPair (encPair encUnary encBits) encCertState) encBool) encCertState := by
   have hnode := computableInPolyTime_nodeKey (T := T) hcoins
   have hsign := computableInPolyTime_signAt (T := T) hcoins
@@ -312,7 +324,8 @@ include hcoins in
 /-- The chain is computable in polynomial time: every node key and signature on the path is
 polynomially bounded, and the chain has one certificate per bit. -/
 theorem computableInPolyTime_certify :
-    ComputableInPolyTime (fun p : (ℕ × List Bool) × List Bool => certify S T coins p.1.1 p.1.2 p.2)
+    ComputableInPolyTime
+      (fun p : (ℕ × List Bool) × List Bool => certify S T coins (Prod.fst p.1) (Prod.snd p.1) p.2)
       (encPair (encPair encUnary encBits) encBits) encCertState := by
   have hnode := computableInPolyTime_nodeKey (T := T) hcoins
   have hsign := computableInPolyTime_signAt (T := T) hcoins
@@ -406,7 +419,7 @@ include hcoins in
 theorem computableInPolyTime_signWithLeaf :
     ComputableInPolyTime
       (fun p : (ℕ × List Bool) × List Bool × List Bool =>
-        signWithLeaf S T coins p.1.1 p.1.2 p.2.1 p.2.2)
+        signWithLeaf S T coins (Prod.fst p.1) (Prod.snd p.1) (Prod.fst p.2) (Prod.snd p.2))
       (encPair (encPair encUnary encBits) (encPair encBits encBits)) encBits := by
   have hcert := computableInPolyTime_certify (T := T) hcoins
   have hsign := computableInPolyTime_signAt (T := T) hcoins
@@ -545,7 +558,8 @@ include hdepth in
 /-- Verification is computable in polynomial time. -/
 theorem computableInPolyTime_verify :
     ComputableInPolyTime
-      (fun p : List Bool × List Bool × List Bool => verify S depth p.1 p.2.1 p.2.2)
+      (fun p : List Bool × List Bool × List Bool =>
+        verify S depth p.1 (Prod.fst p.2) (Prod.snd p.2))
       (encPair encBits (encPair encBits encBits)) encBool := by
   have hverify := S.verify_polyTime
   have hkey := keyDecoder.computableInPolyTime
@@ -576,7 +590,8 @@ variable (S T coins keyLen depth) in
 indexed scheme `S` with at least two indices, seeded by `T`, with node coins from `coins`, secrets
 of length `keyLen n` and trees of depth `depth n ≥ 1`. -/
 noncomputable def scheme
-    (hcoins : ComputableInPolyTime (fun p : List Bool × List Bool × ℕ => coins p.1 p.2.1 p.2.2)
+    (hcoins : ComputableInPolyTime
+      (fun p : List Bool × List Bool × ℕ => coins p.1 (Prod.fst p.2) (Prod.snd p.2))
       (encPair encBits (encPair encBits encUnary)) encBits)
     (hkeyLen : ComputableInPolyTime keyLen encUnary encUnary)
     (hdepth : ComputableInPolyTime depth encUnary encUnary)
diff --git a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean
index a5120ef4c6..dda2623ac9 100644
--- a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean
+++ b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean
@@ -144,9 +144,11 @@ noncomputable def eufCmaGame [DecidableEq M] (scheme : Scheme PK SK M Sig Query
   let keys ← scheme.keyGen
   let s ← forger.coins
   let forged ← (interpret (handler scheme keys.2) (forger.forge keys.1 s)).run ([], [])
-  let verified ← (interpret (oracle Digest) (scheme.verify keys.1 forged.1.1 forged.1.2)).run
-    forged.2.1
-  return (verified.1 && !(forged.2.2.contains forged.1.1))
+  let msig := forged.1
+  let state := forged.2
+  let verified ← (interpret (oracle Digest) (scheme.verify keys.1 msig.1 msig.2)).run
+    state.1
+  return (verified.1 && !(state.2.contains msig.1))
 
 /-- A scheme is correct when every honest signature verifies under the same oracle, from every
 state of the oracle. -/

From f043215a08f0a5f95d0c05fe5520eef0b834927d Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 1 Nov 2026 15:01:43 -0500
Subject: [PATCH 2/3] refactor(Crypto): bind signature and commitment
 components by name; restore certificate spellings (#1764)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Review fixes for #2007:
- Restore the original `p.2.1` spelling of the `@[program_certificate]` conclusions and
  certificate fields (`SignatureScheme.verify_polyTime`, `IndexedSignatureScheme.sign_ppt` and
  `verify_polyTime`, `computableInPolyTime_isCollision`, the three Merkle–Damgård certificates,
  `computableInPolyTime_lamportVerify`, `isPPTOn_lamportSimKeys` and the three
  `isPPTOn_run_*SigningOracle` statements) and of the section variable `hcoins` in
  `TreeSignature`. The `Prod.fst`/`Prod.snd` respelling was the same term; a pattern binder
  would index the certificate under the generated `match_1`, and in a `variable` binder it
  elaborates to `sorry`.
- Bind the other statements and fields by name: `CollisionResistantOn.of_extract`,
  `PublicOperations.commit_polyTime`/`verify_polyTime`, `Seeded.signWith_polyTime`/
  `signBudget_polyTime`, `MerkleSignature.isPPTOn_sign`/`computableInPolyTime_verify`,
  `isPPTOn_pedersenCommitProb` and the `TreeSignature` efficiency theorems.
- Destructure instead of naming tuple tails in `indexedEufCmaGame`, `exists_signWith`,
  `encodePedersenCommit`, `encodePedersenVerify`, `MerkleSignature.verify`, `collisionOf`,
  `oneTimeForgerAt`, and `TreeSignature.certifyStep`/`signWithLeaf`/`verify`/`certify_spec`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
---
 .../Computational/CollisionResistant.lean     |  5 +-
 .../Commitment/PublicOperations.lean          |  5 +-
 .../Computational/IndexedSignature.lean       | 14 ++---
 .../IndexedSignature/Counter.lean             |  3 +-
 .../IndexedSignature/Seeded.lean              | 14 ++---
 .../Crypto/Computational/MerkleDamgard.lean   |  7 +--
 .../Crypto/Computational/MerkleSignature.lean | 12 ++--
 .../MerkleSignature/Security.lean             | 21 +++----
 .../Computational/OneWayToSignature.lean      |  5 +-
 .../Computational/PedersenCommitment.lean     |  7 +--
 .../PedersenCommitment/ProbComp.lean          |  3 +-
 .../PedersenCommitment/PublicOperations.lean  | 10 +--
 .../Crypto/Computational/Signature.lean       |  5 +-
 .../Crypto/Computational/TreeSignature.lean   | 62 ++++++++-----------
 14 files changed, 70 insertions(+), 103 deletions(-)

diff --git a/Complexity/Crypto/Computational/CollisionResistant.lean b/Complexity/Crypto/Computational/CollisionResistant.lean
index a079a5389b..63927d6213 100644
--- a/Complexity/Crypto/Computational/CollisionResistant.lean
+++ b/Complexity/Crypto/Computational/CollisionResistant.lean
@@ -359,7 +359,7 @@ theorem computableInPolyTime_isCollision
       (encPair encUnary encBits) encBool) :
     ComputableInPolyTime
       (fun p : ℕ × List Bool × List Bool × List Bool =>
-        isCollision H valid p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
+        isCollision H valid p.1 p.2.1 p.2.2.1 p.2.2.2)
       (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool := by
   have hv₁ : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool × List Bool =>
       valid p.1 p.2.2.1) (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool :=
@@ -493,8 +493,7 @@ theorem CollisionResistantOn.of_extract
     (hCR : CollisionResistantOn H₂ valid₂)
     (extract : ℕ → List Bool → List Bool → List Bool → List Bool × List Bool)
     (hextract : ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × List Bool =>
-        extract p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
+      (fun ((n, k, m₁, m₂) : ℕ × List Bool × List Bool × List Bool) => extract n k m₁ m₂)
       (encPair encUnary (encPair encBits (encPair encBits encBits)))
       (encPair encBits encBits))
     (himp : ∀ᶠ n in Filter.atTop, ∀ k, k.length = n → ∀ m₁ m₂,
diff --git a/Complexity/Crypto/Computational/Commitment/PublicOperations.lean b/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
index 01875e6722..3a920b4a3c 100644
--- a/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
+++ b/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
@@ -57,12 +57,11 @@ structure PublicOperations {Key : Type} (S : CommitmentScheme Key) where
   map_commit : ∀ k m, (randomness k).map (commit k m) = S.commitDist k m
   /-- Deterministic evaluation is polynomial-time in the public key, message and randomness word. -/
   commit_polyTime : ComputableInPolyTime
-    (fun p : Key × List Bool × List Bool => commit p.1 (Prod.fst p.2) (Prod.snd p.2))
+    (fun ((k, msg, r) : Key × List Bool × List Bool) => commit k msg r)
     (encPair S.encodeKey (encPair encBits encBits)) (encPair encBits encBits)
   /-- Verification is polynomial-time in the public key, message, commitment and opening words. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : Key × List Bool × List Bool × List Bool =>
-      S.verify p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
+    (fun ((k, msg, c, o) : Key × List Bool × List Bool × List Bool) => S.verify k msg c o)
     (encPair S.encodeKey (encPair encBits (encPair encBits encBits))) encBool
 
 namespace PublicOperations
diff --git a/Complexity/Crypto/Computational/IndexedSignature.lean b/Complexity/Crypto/Computational/IndexedSignature.lean
index cb656f876a..2a8b9edf46 100644
--- a/Complexity/Crypto/Computational/IndexedSignature.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature.lean
@@ -101,11 +101,10 @@ structure IndexedSignatureScheme where
   keyGen_ppt : IsPPTOn encUnary (encPair encBits encBits) keyGen
   /-- Signing is uniformly strict PPT in the secret key, the unary index and the message. -/
   sign_ppt : IsPPTOn (encPair encBits (encPair encUnary encBits)) encBits
-    (fun p => sign p.1 (Prod.fst p.2) (Prod.snd p.2))
+    (fun p => sign p.1 p.2.1 p.2.2)
   /-- Verification is computable in plain polynomial time on `(pk, u, msg, sig)`. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : List Bool × ℕ × List Bool × List Bool =>
-      verify p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
+    (fun p : List Bool × ℕ × List Bool × List Bool => verify p.1 p.2.1 p.2.2.1 p.2.2.2)
     (encPair encBits (encPair encUnary (encPair encBits encBits))) encBool
   /-- Every signature produced at an index below the capacity, under a supported key pair, is
   accepted. -/
@@ -143,10 +142,8 @@ def indexedEufCmaGame (S : IndexedSignatureScheme) (adversary : IndexedForger) (
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.indexedSigningOracle n keys.2)) (adversary n keys.1)).run []
-  let u_msig := out.1
-  let msig := u_msig.2
-  return !out.2.contains (u_msig.1, msig.1) &&
-    S.verify keys.1 u_msig.1 msig.1 msig.2
+  let (u, msg, sig) := out.1
+  return !out.2.contains (u, msg) && S.verify keys.1 u msg sig
 
 /-- Running an oracle-PPT indexed forger against `indexedSigningOracle` is uniformly strict PPT in
 the unary security parameter, the public key and the secret key. -/
@@ -158,8 +155,7 @@ theorem isPPTOn_run_indexedSigningOracle (S : IndexedSignatureScheme) {adversary
       (fun caller : ℕ × (List Bool × List Bool) =>
         (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
-            (S.indexedSigningOracle caller.1 (Prod.snd caller.2)))
-          (adversary caller.1 (Prod.fst caller.2))).run
+            (S.indexedSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run
           []) := by
   obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le
   have hcap := S.capacity_polyTime
diff --git a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
index 8bd2f49063..c9d5596195 100644
--- a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
@@ -152,8 +152,7 @@ theorem isPPTOn_run_counterSigningOracle {adversary : Forger}
       (fun caller : ℕ × (List Bool × List Bool) =>
         (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
-            (S.counterSigningOracle caller.1 (Prod.snd caller.2)))
-          (adversary caller.1 (Prod.fst caller.2))).run
+            (S.counterSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run
           (0, [])) := by
   obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le
   have hcap := S.capacity_polyTime
diff --git a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
index dd1d2f64b9..ea7c331daa 100644
--- a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
@@ -69,11 +69,11 @@ structure Seeded (S : IndexedSignatureScheme) where
   eval_keyGen : ∀ n length, keyGenBudget n ≤ length →
     ProbComp.eval (S.keyGen n) = (BitString.uniformList length).map (keyGenWith n)
   signWith_polyTime : ComputableInPolyTime
-    (fun p : (List Bool × ℕ × List Bool) × List Bool =>
-      signWith (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) (Prod.snd (Prod.snd p.1)) p.2)
+    (fun (((sk, u, msg), coins) : (List Bool × ℕ × List Bool) × List Bool) =>
+      signWith sk u msg coins)
     (encPair (encPair encBits (encPair encUnary encBits)) encBits) encBits
   signBudget_polyTime : ComputableInPolyTime
-    (fun p : List Bool × ℕ × List Bool => signBudget p.1 (Prod.fst p.2) (Prod.snd p.2))
+    (fun ((sk, u, msg) : List Bool × ℕ × List Bool) => signBudget sk u msg)
     (encPair encBits (encPair encUnary encBits)) encUnary
   signWith_mem_support : ∀ sk u msg coins,
     signWith sk u msg coins ∈ (ProbComp.eval (S.sign sk u msg)).support
@@ -114,11 +114,11 @@ theorem exists_signWith (S : IndexedSignatureScheme) :
         (encPair (encPair encBits (encPair encUnary encBits)) encBits) encBits ∧
       ComputableInPolyTime budget (encPair encBits (encPair encUnary encBits)) encUnary ∧
       (∀ a coins,
-        let um := a.2
-        signWith a coins ∈ (ProbComp.eval (S.sign a.1 um.1 um.2)).support) ∧
+        let (sk, u, msg) := a
+        signWith a coins ∈ (ProbComp.eval (S.sign sk u msg)).support) ∧
       ∀ a length, budget a ≤ length →
-        let um := a.2
-        ProbComp.eval (S.sign a.1 um.1 um.2) =
+        let (sk, u, msg) := a
+        ProbComp.eval (S.sign sk u msg) =
           (BitString.uniformList length).map (signWith a) := by
   obtain ⟨c, d, evaluate, hpoly, hsupport, hlaw⟩ :=
     IsPPTOn.exists_total_seeded_evaluator S.sign_ppt
diff --git a/Complexity/Crypto/Computational/MerkleDamgard.lean b/Complexity/Crypto/Computational/MerkleDamgard.lean
index 96683c5b95..dcfca8f90d 100644
--- a/Complexity/Crypto/Computational/MerkleDamgard.lean
+++ b/Complexity/Crypto/Computational/MerkleDamgard.lean
@@ -296,7 +296,7 @@ theorem computableInPolyTime_chainTrace
     (hlen : ∀ k x, x.length = 2 * k.length → (h k x).length = k.length) :
     ComputableInPolyTime
       (fun p : List Bool × List Bool × List (List Bool) =>
-        chainTrace h p.1 (Prod.fst p.2) (Prod.snd p.2))
+        chainTrace h p.1 p.2.1 p.2.2)
       (encPair encBits (encPair encBits (encList encBits)))
       (encPair encBits (encList encBits)) :=
   .of_tidy (computableTidilyInPolyTime_chainTrace hh.tidy hlen
@@ -348,8 +348,7 @@ theorem computableInPolyTime_extractChainCollision
     (hlen : ∀ k x, x.length = 2 * k.length → (h k x).length = k.length) :
     ComputableInPolyTime
       (fun p : List Bool × List Bool × List (List Bool) × List (List Bool) =>
-        extractChainCollision h p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2))
-          (Prod.snd (Prod.snd p.2)))
+        extractChainCollision h p.1 p.2.1 p.2.2.1 p.2.2.2)
       (encPair encBits (encPair encBits (encPair (encList encBits) (encList encBits))))
       (encPair encBits encBits) :=
   .of_tidy (computableTidilyInPolyTime_extractChainCollision hh.tidy hlen
@@ -733,7 +732,7 @@ theorem computableInPolyTime_extractMerkleDamgardCollision
     (hlen : ∀ k x, x.length = 2 * k.length → (h k x).length = k.length) :
     ComputableInPolyTime
       (fun p : List Bool × List Bool × List Bool =>
-        extractMerkleDamgardCollision h p.1 (Prod.fst p.2) (Prod.snd p.2))
+        extractMerkleDamgardCollision h p.1 p.2.1 p.2.2)
       (encPair encBits (encPair encBits encBits))
       (encPair encBits encBits) := by
   apply ComputableInPolyTime.of_tidy
diff --git a/Complexity/Crypto/Computational/MerkleSignature.lean b/Complexity/Crypto/Computational/MerkleSignature.lean
index 0ee501651a..764d358163 100644
--- a/Complexity/Crypto/Computational/MerkleSignature.lean
+++ b/Complexity/Crypto/Computational/MerkleSignature.lean
@@ -130,10 +130,8 @@ verification key opens leaf `u` of the depth-`depth k.length` tree with root `ro
 signature verifies on `H k msg`. -/
 def verify (pk : List Bool) (u : ℕ) (msg sig : List Bool) : Bool :=
   let k := unframe pk
-  let forged := signatureDecoder.decode sig
-  let otsPath := forged.2
-  merkleVerify H k (depth k.length) (dropFrame pk) u forged.1 otsPath.2 &&
-    S.verify forged.1 (H k msg) otsPath.1
+  let (vk, ots, path) := signatureDecoder.decode sig
+  merkleVerify H k (depth k.length) (dropFrame pk) u vk path && S.verify vk (H k msg) ots
 
 /-! ### Completeness -/
 
@@ -249,7 +247,7 @@ include hH hlen in
 /-- Merkle signing is uniformly strict PPT. -/
 theorem isPPTOn_sign :
     IsPPTOn (encPair encBits (encPair encUnary encBits)) encBits
-      (fun p => sign S H p.1 (Prod.fst p.2) (Prod.snd p.2)) := by
+      (fun (sk, u, msg) => sign S H sk u msg) := by
   let E := encPair encBits (encPair encUnary encBits)
   have hdec : ComputableTidilyInPolyTime (fun p : List Bool × ℕ × List Bool =>
       secretKeyDecoder.decode p.1) E (encPair encBits (encList (encPair encBits encBits))) :=
@@ -290,8 +288,8 @@ include hH hlen hcap in
 /-- Merkle verification is computable in polynomial time. -/
 theorem computableInPolyTime_verify :
     ComputableInPolyTime
-      (fun p : List Bool × ℕ × List Bool × List Bool =>
-        verify S H depth p.1 (Prod.fst p.2) (Prod.fst (Prod.snd p.2)) (Prod.snd (Prod.snd p.2)))
+      (fun ((pk, u, msg, sig) : List Bool × ℕ × List Bool × List Bool) =>
+        verify S H depth pk u msg sig)
       (encPair encBits (encPair encUnary (encPair encBits encBits))) encBool := by
   apply ComputableInPolyTime.of_tidy
   let E := encPair encBits (encPair encUnary (encPair encBits encBits))
diff --git a/Complexity/Crypto/Computational/MerkleSignature/Security.lean b/Complexity/Crypto/Computational/MerkleSignature/Security.lean
index 57f1fa5a54..f55615a256 100644
--- a/Complexity/Crypto/Computational/MerkleSignature/Security.lean
+++ b/Complexity/Crypto/Computational/MerkleSignature/Security.lean
@@ -103,16 +103,13 @@ keys `keys`: a collision in the tree if the forged verification key is not the o
 and otherwise the forged message with a message signed at leaf `u` with the same digest. -/
 def collisionOf (k : List Bool) (keys : List (List Bool × List Bool))
     (out : (ℕ × List Bool × List Bool) × List (ℕ × List Bool)) : List Bool × List Bool :=
-  let u_msig := out.1
-  let u := u_msig.1
-  let msig := u_msig.2
-  let forged := signatureDecoder.decode msig.2
-  let otsPath := forged.2
+  let ((u, msg, sig), signed) := out
+  let (vk, _, path) := signatureDecoder.decode sig
   let vks := keys.map Prod.fst
-  if forged.1 == vks.getD u [] then
-    (msig.1, (out.2.find? fun e => e.1 == u && H k e.2 == H k msig.1).elim [] Prod.snd)
+  if vk == vks.getD u [] then
+    (msg, (signed.find? fun e => e.1 == u && H k e.2 == H k msg).elim [] Prod.snd)
   else
-    extractMerkleCollision H k forged.1 (vks.getD u []) u otsPath.2 (merklePath H k vks u)
+    extractMerkleCollision H k vk (vks.getD u []) u path (merklePath H k vks u)
 
 /-- The collision finder: given the hash key `k`, generate the one-time keys, answer the forger's
 signing queries honestly, and return `collisionOf` its forgery. -/
@@ -169,11 +166,9 @@ noncomputable def oneTimeForgerAt (bound : ℕ → ℕ) (adversary : IndexedForg
     (ProbOracleComp.handler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j)))
       (plantedHandler S H depth n setup.1 setup.2 i (bound n)))
     (adversary n (publicKey H setup.1 setup.2))).run []
-  let u_msig := out.1
-  let msig := u_msig.2
-  let forged := signatureDecoder.decode msig.2
-  let otsPath := forged.2
-  return (H setup.1 msig.1, otsPath.1)
+  let ((_, msg, sig), _) := out
+  let (_, ots, _) := signatureDecoder.decode sig
+  return (H setup.1 msg, ots)
 
 /-- The one-time forger: plant the challenge at a uniform leaf. -/
 noncomputable def oneTimeForger (bound : ℕ → ℕ) (adversary : IndexedForger) : Forger :=
diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean
index 8aba6b53dd..2aa668a10a 100644
--- a/Complexity/Crypto/Computational/OneWayToSignature.lean
+++ b/Complexity/Crypto/Computational/OneWayToSignature.lean
@@ -356,8 +356,7 @@ theorem isPPTOn_lamportSign :
 theorem computableInPolyTime_lamportVerify {f : List Bool → List Bool}
     (hf : ComputableInPolyTime f encBits encBits) :
     ComputableInPolyTime
-      (fun p : List Bool × List Bool × List Bool =>
-        lamportVerify f p.1 (Prod.fst p.2) (Prod.snd p.2))
+      (fun p : List Bool × List Bool × List Bool => lamportVerify f p.1 p.2.1 p.2.2)
       (encPair encBits (encPair encBits encBits)) encBool := by
   have hf := hf.tidy
   refine .of_tidy ?_
@@ -513,7 +512,7 @@ noncomputable def lamportSimKeys (f : List Bool → List Bool) (n j : ℕ) (y :
 theorem isPPTOn_lamportSimKeys {f : List Bool → List Bool}
     (hf : ComputableInPolyTime f encBits encBits) :
     IsPPTOn (encPair (encPair encUnary encBits) encUnary) (encPair encBits encBits)
-      (fun q : (ℕ × List Bool) × ℕ => lamportSimKeys f (Prod.fst q.1) q.2 (Prod.snd q.1)) := by
+      (fun q : (ℕ × List Bool) × ℕ => lamportSimKeys f q.1.1 q.2 q.1.2) := by
   have hf := hf.tidy
   unfold lamportSimKeys
   have hfront : IsPPTOn (encPair (encPair encUnary encBits) encUnary) (encList encBits)
diff --git a/Complexity/Crypto/Computational/PedersenCommitment.lean b/Complexity/Crypto/Computational/PedersenCommitment.lean
index 0d75bc32bc..1f119b7a85 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment.lean
@@ -182,11 +182,8 @@ theorem pedersenCommit_smul_generator_eq_iff (d : F.Desc) (α m₀ r₀ m₁ r
 /-- Pedersen commitment on encoded group elements: given `(d, encode h, m, r)`, compute
 `encode (m • g + r • h)`. -/
 def encodePedersenCommit (input : F.Desc × List Bool × ℕ × ℕ) : List Bool :=
-  let hmr := input.2
-  let mr := hmr.2
-  F.add (input.1,
-    F.smul (input.1, mr.1, F.encode input.1 (F.generator input.1)),
-    F.smul (input.1, mr.2, hmr.1))
+  let (d, h, m, r) := input
+  F.add (d, F.smul (d, m, F.encode d (F.generator d)), F.smul (d, r, h))
 
 /-- `encodePedersenCommit` computes `F.encode d (F.pedersenCommit d h m r)` on encoded group
 elements. -/
diff --git a/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean b/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
index 73d294ec48..7bb991b88c 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
@@ -68,8 +68,7 @@ public key encoding, and message word. -/
 theorem isPPTOn_pedersenCommitProb :
     IsPPTOn (encPair encUnary (encPair F.pedersenScheme.encodeKey encBits))
       (encPair encBits encBits)
-      (fun p : ℕ × F.PedersenKey × List Bool =>
-        F.pedersenCommitProb p.1 (Prod.fst p.2) (Prod.snd p.2)) := by
+      (fun ((n, key, msg) : ℕ × F.PedersenKey × List Bool) => F.pedersenCommitProb n key msg) := by
   let E := encPair encUnary (encPair F.pedersenScheme.encodeKey encBits)
   have hn := ComputableInPolyTime.fst encUnary (encPair F.pedersenScheme.encodeKey encBits)
   have hrest := ComputableInPolyTime.snd encUnary (encPair F.pedersenScheme.encodeKey encBits)
diff --git a/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean b/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
index c64c52c210..741abce388 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
@@ -52,13 +52,9 @@ opening words. The public element is already encoded; no discrete logarithm or s
 value is supplied to this algorithm. -/
 def encodePedersenVerify
     (input : (F.Desc × List Bool) × List Bool × List Bool × List Bool) : Bool :=
-  let dh := input.1
-  let mco := input.2
-  let co := mco.2
-  decide (ofBits mco.1 < F.order dh.1) &&
-    decide ((ofBits mco.1).bits = mco.1) &&
-    decide (F.encodePedersenCommit
-      (dh.1, dh.2, ofBits mco.1, ofBits co.2) = co.1)
+  let ((d, h), m, c, o) := input
+  decide (ofBits m < F.order d) && decide ((ofBits m).bits = m) &&
+    decide (F.encodePedersenCommit (d, h, ofBits m, ofBits o) = c)
 
 /-- The encoded verifier computes exactly the verifier used by `pedersenScheme`. -/
 @[simp]
diff --git a/Complexity/Crypto/Computational/Signature.lean b/Complexity/Crypto/Computational/Signature.lean
index 25ff20e4d0..1f6425216f 100644
--- a/Complexity/Crypto/Computational/Signature.lean
+++ b/Complexity/Crypto/Computational/Signature.lean
@@ -97,7 +97,7 @@ structure SignatureScheme where
   sign_ppt : IsPPTOn (encPair encBits encBits) encBits (fun p => sign p.1 p.2)
   /-- Verification is computable in plain polynomial time on `(pk, msg, sig)`. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : List Bool × List Bool × List Bool => verify p.1 (Prod.fst p.2) (Prod.snd p.2))
+    (fun p : List Bool × List Bool × List Bool => verify p.1 p.2.1 p.2.2)
     (encPair encBits (encPair encBits encBits)) encBool
   /-- Every signature produced by `sign` on an `n`-bit message under a supported key pair at
   security parameter `n` is accepted by `verify`. -/
@@ -290,8 +290,7 @@ theorem isPPTOn_run_oneTimeSigningOracle (S : SignatureScheme) {adversary : Forg
       (fun caller : ℕ × (List Bool × List Bool) =>
         (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
-            (S.oneTimeSigningOracle (Prod.snd caller.2)))
-          (adversary caller.1 (Prod.fst caller.2))).run []) := by
+            (S.oneTimeSigningOracle caller.2.2)) (adversary caller.1 caller.2.1)).run []) := by
   obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le
   have hhandler : IsPPTOn
       (encPair (encPair encUnary (encPair encBits encBits))
diff --git a/Complexity/Crypto/Computational/TreeSignature.lean b/Complexity/Crypto/Computational/TreeSignature.lean
index 6da24f6d78..ab374c80b5 100644
--- a/Complexity/Crypto/Computational/TreeSignature.lean
+++ b/Complexity/Crypto/Computational/TreeSignature.lean
@@ -112,11 +112,9 @@ abbrev CertState := List Bool × (List Bool × List Bool) × List (List Bool ×
 /-- One step of the chain: derive the child at `a`, sign its public key at index `a`, and move
 to it. -/
 def certifyStep (n : ℕ) (k : List Bool) (state : CertState) (a : Bool) : CertState :=
-  let child := nodeKey S T coins n k (state.1 ++ [a])
-  let keyCerts := state.2
-  let nodeKeys := keyCerts.1
-  (state.1 ++ [a], child,
-    keyCerts.2 ++ [(child.1, signAt S T coins k state.1 nodeKeys.2 a.toNat child.1)])
+  let (node, (_, sk), certs) := state
+  let child := nodeKey S T coins n k (node ++ [a])
+  (node ++ [a], child, certs ++ [(child.1, signAt S T coins k node sk a.toNat child.1)])
 
 /-- Certify the path `bits` from the root. -/
 def certify (n : ℕ) (k bits : List Bool) : CertState :=
@@ -140,11 +138,8 @@ def keyDecoder : Decoder (encPair encUnary encBits) := Decoder.unary.pair Decode
 /-- Sign `msg` at the leaf `leaf`: certify the path to the leaf's parent, which signs `msg` at the
 leaf's last bit. -/
 def signWithLeaf (n : ℕ) (k leaf msg : List Bool) : List Bool :=
-  let c := certify S T coins n k leaf.dropLast
-  let keyCerts := c.2
-  let nodeKeys := keyCerts.1
-  encodeSignature leaf keyCerts.2
-    (signAt S T coins k c.1 nodeKeys.2 (leaf.getLastD false).toNat msg)
+  let (node, (_, sk), certs) := certify S T coins n k leaf.dropLast
+  encodeSignature leaf certs (signAt S T coins k node sk (leaf.getLastD false).toNat msg)
 
 /-! ### The algorithms -/
 
@@ -174,11 +169,10 @@ chain from the root along the leaf's prefix, and the last certified key signs `m
 last bit. -/
 def verify (pk msg sig : List Bool) : Bool :=
   let p := keyDecoder.decode pk
-  let s := signatureDecoder.decode sig
-  let certsLast := s.2
-  let r := (s.1.dropLast.zip certsLast.1).foldl (verifyStep S) (true, p.2)
-  (s.1.length == depth p.1) && (certsLast.1.length + 1 == depth p.1) && r.1 &&
-    S.verify r.2 (s.1.getLastD false).toNat msg certsLast.2
+  let (leaf, certs, last) := signatureDecoder.decode sig
+  let r := (leaf.dropLast.zip certs).foldl (verifyStep S) (true, p.2)
+  (leaf.length == depth p.1) && (certs.length + 1 == depth p.1) && r.1 &&
+    S.verify r.2 (leaf.getLastD false).toNat msg last
 
 /-! ### Completeness -/
 
@@ -192,17 +186,17 @@ theorem certify_append (n : ℕ) (k bits : List Bool) (a : Bool) :
 /-- The chain reaches the node `bits` with its key, issues one certificate per bit, and its
 certificates verify from the root when both indices are below the capacity. -/
 theorem certify_spec (n : ℕ) (hcap : 2 ≤ S.capacity n) (k bits : List Bool) :
-    let c := certify S T coins n k bits
-    let keyCerts := c.2
-    c.1 = bits ∧
-      keyCerts.1 = nodeKey S T coins n k bits ∧
-      keyCerts.2.length = bits.length ∧
-      (bits.zip keyCerts.2).foldl (verifyStep S)
+    let (node, keys, certs) := certify S T coins n k bits
+    node = bits ∧
+      keys = nodeKey S T coins n k bits ∧
+      certs.length = bits.length ∧
+      (bits.zip certs).foldl (verifyStep S)
         (true, (nodeKey S T coins n k []).1) = (true, (nodeKey S T coins n k bits).1) := by
   induction bits using List.reverseRecOn with
   | nil => simp [certify]
   | append_singleton bits a ih =>
     obtain ⟨hpath, hkey, hlen, hchain⟩ := ih
+    simp only [← certify.eq_1] at hpath hkey hlen hchain
     rw [certify_append]
     simp only [certifyStep, hpath, hkey, true_and]
     refine ⟨by simp [hlen], ?_⟩
@@ -224,6 +218,7 @@ theorem verify_signWithLeaf (n : ℕ) (hcap : 2 ≤ S.capacity n) (hdepth : 1 
       (signWithLeaf S T coins n k leaf msg) = true := by
   obtain ⟨hpath, hkey, hlen, hchain⟩ :=
     certify_spec (T := T) (coins := coins) n hcap k leaf.dropLast
+  simp only [← certify.eq_1] at hpath hkey hlen hchain
   have hu : (leaf.getLastD false).toNat < S.capacity n := by
     cases leaf.getLastD false <;> simp <;> omega
   have hv := S.verify_sign n (nodeKey S T coins n k leaf.dropLast) (T.keyGenWith_mem_support n _)
@@ -269,14 +264,14 @@ local notation "encCertState" =>
   encPair encBits (encPair (encPair encBits encBits) (encList (encPair encBits encBits)))
 
 variable (hcoins : ComputableInPolyTime
-    (fun p : List Bool × List Bool × ℕ => coins p.1 (Prod.fst p.2) (Prod.snd p.2))
+    (fun p : List Bool × List Bool × ℕ => coins p.1 p.2.1 p.2.2)
     (encPair encBits (encPair encBits encUnary)) encBits)
 
 include hcoins in
 /-- Node keys are computable in polynomial time from the parameter, the secret and the path. -/
 theorem computableInPolyTime_nodeKey :
     ComputableInPolyTime
-      (fun p : (ℕ × List Bool) × List Bool => nodeKey S T coins (Prod.fst p.1) (Prod.snd p.1) p.2)
+      (fun (((n, k), path) : (ℕ × List Bool) × List Bool) => nodeKey S T coins n k path)
       (encPair (encPair encUnary encBits) encBits) (encPair encBits encBits) := by
   have hkg := T.keyGenWith_polyTime
   have hbudget := T.keyGenBudget_polyTime
@@ -287,9 +282,8 @@ include hcoins in
 /-- Node signatures are computable in polynomial time. -/
 theorem computableInPolyTime_signAt :
     ComputableInPolyTime
-      (fun p : (List Bool × List Bool × List Bool) × ℕ × List Bool =>
-        signAt S T coins (Prod.fst p.1) (Prod.fst (Prod.snd p.1)) (Prod.snd (Prod.snd p.1))
-          (Prod.fst p.2) (Prod.snd p.2))
+      (fun (((k, path, sk), u, msg) : (List Bool × List Bool × List Bool) × ℕ × List Bool) =>
+        signAt S T coins k path sk u msg)
       (encPair (encPair encBits (encPair encBits encBits)) (encPair encUnary encBits)) encBits := by
   have hsg := T.signWith_polyTime
   have hbudget := T.signBudget_polyTime
@@ -300,9 +294,8 @@ include hcoins in
 /-- One chain step is computable in polynomial time. -/
 theorem computableInPolyTime_certifyStep :
     ComputableInPolyTime
-      (fun p : ((ℕ × List Bool) × CertState) × Bool =>
-        certifyStep S T coins (Prod.fst (Prod.fst p.1)) (Prod.snd (Prod.fst p.1))
-          (Prod.snd p.1) p.2)
+      (fun ((((n, k), state), a) : ((ℕ × List Bool) × CertState) × Bool) =>
+        certifyStep S T coins n k state a)
       (encPair (encPair (encPair encUnary encBits) encCertState) encBool) encCertState := by
   have hnode := computableInPolyTime_nodeKey (T := T) hcoins
   have hsign := computableInPolyTime_signAt (T := T) hcoins
@@ -325,7 +318,7 @@ include hcoins in
 polynomially bounded, and the chain has one certificate per bit. -/
 theorem computableInPolyTime_certify :
     ComputableInPolyTime
-      (fun p : (ℕ × List Bool) × List Bool => certify S T coins (Prod.fst p.1) (Prod.snd p.1) p.2)
+      (fun (((n, k), bits) : (ℕ × List Bool) × List Bool) => certify S T coins n k bits)
       (encPair (encPair encUnary encBits) encBits) encCertState := by
   have hnode := computableInPolyTime_nodeKey (T := T) hcoins
   have hsign := computableInPolyTime_signAt (T := T) hcoins
@@ -418,8 +411,8 @@ include hcoins in
 /-- Signing at a given leaf is computable in polynomial time. -/
 theorem computableInPolyTime_signWithLeaf :
     ComputableInPolyTime
-      (fun p : (ℕ × List Bool) × List Bool × List Bool =>
-        signWithLeaf S T coins (Prod.fst p.1) (Prod.snd p.1) (Prod.fst p.2) (Prod.snd p.2))
+      (fun (((n, k), leaf, msg) : (ℕ × List Bool) × List Bool × List Bool) =>
+        signWithLeaf S T coins n k leaf msg)
       (encPair (encPair encUnary encBits) (encPair encBits encBits)) encBits := by
   have hcert := computableInPolyTime_certify (T := T) hcoins
   have hsign := computableInPolyTime_signAt (T := T) hcoins
@@ -558,8 +551,7 @@ include hdepth in
 /-- Verification is computable in polynomial time. -/
 theorem computableInPolyTime_verify :
     ComputableInPolyTime
-      (fun p : List Bool × List Bool × List Bool =>
-        verify S depth p.1 (Prod.fst p.2) (Prod.snd p.2))
+      (fun ((pk, msg, sig) : List Bool × List Bool × List Bool) => verify S depth pk msg sig)
       (encPair encBits (encPair encBits encBits)) encBool := by
   have hverify := S.verify_polyTime
   have hkey := keyDecoder.computableInPolyTime
@@ -591,7 +583,7 @@ indexed scheme `S` with at least two indices, seeded by `T`, with node coins fro
 of length `keyLen n` and trees of depth `depth n ≥ 1`. -/
 noncomputable def scheme
     (hcoins : ComputableInPolyTime
-      (fun p : List Bool × List Bool × ℕ => coins p.1 (Prod.fst p.2) (Prod.snd p.2))
+      (fun ((k, input, length) : List Bool × List Bool × ℕ) => coins k input length)
       (encPair encBits (encPair encBits encUnary)) encBits)
     (hkeyLen : ComputableInPolyTime keyLen encUnary encUnary)
     (hdepth : ComputableInPolyTime depth encUnary encUnary)

From 7fb513a8eba2f42aeb877901e82ddf12688a6b88 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Mon, 2 Nov 2026 15:19:04 +0000
Subject: [PATCH 3/3] fix(Crypto/IndexedSignature): restore Seeded
 program_certificate field spellings and guard in
 ProgramCertificateDiagnostics (#1764)

---
 Complexity/Crypto/Computational/IndexedSignature/Seeded.lean | 5 ++---
 ComplexityTests/ProgramCertificateDiagnostics.lean           | 5 +++++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
index ea7c331daa..6420d41f77 100644
--- a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
@@ -69,11 +69,10 @@ structure Seeded (S : IndexedSignatureScheme) where
   eval_keyGen : ∀ n length, keyGenBudget n ≤ length →
     ProbComp.eval (S.keyGen n) = (BitString.uniformList length).map (keyGenWith n)
   signWith_polyTime : ComputableInPolyTime
-    (fun (((sk, u, msg), coins) : (List Bool × ℕ × List Bool) × List Bool) =>
-      signWith sk u msg coins)
+    (fun p : (List Bool × ℕ × List Bool) × List Bool => signWith p.1.1 p.1.2.1 p.1.2.2 p.2)
     (encPair (encPair encBits (encPair encUnary encBits)) encBits) encBits
   signBudget_polyTime : ComputableInPolyTime
-    (fun ((sk, u, msg) : List Bool × ℕ × List Bool) => signBudget sk u msg)
+    (fun p : List Bool × ℕ × List Bool => signBudget p.1 p.2.1 p.2.2)
     (encPair encBits (encPair encUnary encBits)) encUnary
   signWith_mem_support : ∀ sk u msg coins,
     signWith sk u msg coins ∈ (ProbComp.eval (S.sign sk u msg)).support
diff --git a/ComplexityTests/ProgramCertificateDiagnostics.lean b/ComplexityTests/ProgramCertificateDiagnostics.lean
index d4f8c4c774..998290b2b9 100644
--- a/ComplexityTests/ProgramCertificateDiagnostics.lean
+++ b/ComplexityTests/ProgramCertificateDiagnostics.lean
@@ -5,6 +5,7 @@ Authors: Samuel Schlesinger
 -/
 
 import Complexity.Crypto.Computational.Signature
+import Complexity.Crypto.Computational.IndexedSignature.Seeded
 import Complexity.Crypto.Computational.MAC
 import ComplexityTests.PolyTimePlainDriver
 
@@ -16,6 +17,10 @@ open Turing.MultiTapeTM Cslib.Crypto
 run_meta do
   for (certificate, program) in
       [(`Cslib.Crypto.SignatureScheme.verify_polyTime, `Cslib.Crypto.SignatureScheme.verify),
+       (`Cslib.Crypto.IndexedSignatureScheme.Seeded.signWith_polyTime,
+        `Cslib.Crypto.IndexedSignatureScheme.Seeded.signWith),
+       (`Cslib.Crypto.IndexedSignatureScheme.Seeded.signBudget_polyTime,
+        `Cslib.Crypto.IndexedSignatureScheme.Seeded.signBudget),
        (`Cslib.Crypto.MACScheme.verify_polyTime, `Cslib.Crypto.MACScheme.verify)] do
     let type := (← Lean.getConstInfo certificate).type
     let key ← Lean.Meta.forallTelescope type fun _ conclusion =>