diff --git a/Complexity/Crypto/Computational/CollisionResistant.lean b/Complexity/Crypto/Computational/CollisionResistant.lean
index 4ab684caeb..63927d6213 100644
--- a/Complexity/Crypto/Computational/CollisionResistant.lean
+++ b/Complexity/Crypto/Computational/CollisionResistant.lean
@@ -493,7 +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 p.2.1 p.2.2.1 p.2.2.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/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..3a920b4a3c 100644
--- a/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
+++ b/Complexity/Crypto/Computational/Commitment/PublicOperations.lean
@@ -57,11 +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 p.2.1 p.2.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 p.2.1 p.2.2.1 p.2.2.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 6e079b1753..2a8b9edf46 100644
--- a/Complexity/Crypto/Computational/IndexedSignature.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature.lean
@@ -142,8 +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 []
-  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, 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. -/
diff --git a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean
index 9088156c1f..c9d5596195 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}
 
@@ -280,7 +282,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..6420d41f77 100644
--- a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
+++ b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean
@@ -112,9 +112,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 (sk, u, msg) := a
+        signWith a coins ∈ (ProbComp.eval (S.sign sk u msg)).support) ∧
       ∀ a length, budget a ≤ length →
-        ProbComp.eval (S.sign a.1 a.2.1 a.2.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
@@ -124,21 +127,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/MerkleSignature.lean b/Complexity/Crypto/Computational/MerkleSignature.lean
index 77a0155992..764d358163 100644
--- a/Complexity/Crypto/Computational/MerkleSignature.lean
+++ b/Complexity/Crypto/Computational/MerkleSignature.lean
@@ -130,9 +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
-  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 (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 -/
 
@@ -248,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 p.2.1 p.2.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))) :=
@@ -289,7 +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 p.2.1 p.2.2.1 p.2.2.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 3e4dae0a3b..f55615a256 100644
--- a/Complexity/Crypto/Computational/MerkleSignature/Security.lean
+++ b/Complexity/Crypto/Computational/MerkleSignature/Security.lean
@@ -103,13 +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 := out.1.1
-  let forged := signatureDecoder.decode out.1.2.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
-    (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)
+  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 forged.2.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. -/
@@ -166,7 +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 []
-  return (H setup.1 out.1.2.1, (signatureDecoder.decode out.1.2.2).2.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 a3cc11acb0..2aa668a10a 100644
--- a/Complexity/Crypto/Computational/OneWayToSignature.lean
+++ b/Complexity/Crypto/Computational/OneWayToSignature.lean
@@ -583,7 +583,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..1f119b7a85 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment.lean
@@ -182,9 +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 :=
-  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))
+  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. -/
@@ -510,9 +509,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 +551,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..7bb991b88c 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean
@@ -68,7 +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 p.2.1 p.2.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 a52a22729a..741abce388 100644
--- a/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
+++ b/Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean
@@ -52,10 +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 :=
-  decide (ofBits input.2.1 < F.order input.1.1) &&
-    decide ((ofBits input.2.1).bits = input.2.1) &&
-    decide (F.encodePedersenCommit
-      (input.1.1, input.1.2, ofBits input.2.1, ofBits input.2.2.2) = input.2.2.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]
@@ -109,7 +108,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..1f6425216f 100644
--- a/Complexity/Crypto/Computational/Signature.lean
+++ b/Complexity/Crypto/Computational/Signature.lean
@@ -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. -/
diff --git a/Complexity/Crypto/Computational/TreeSignature.lean b/Complexity/Crypto/Computational/TreeSignature.lean
index 712a26cca1..ab374c80b5 100644
--- a/Complexity/Crypto/Computational/TreeSignature.lean
+++ b/Complexity/Crypto/Computational/TreeSignature.lean
@@ -112,9 +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])
-  (state.1 ++ [a], child,
-    state.2.2 ++ [(child.1, signAt S T coins k state.1 state.2.1.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 :=
@@ -138,8 +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
-  encodeSignature leaf c.2.2 (signAt S T coins k c.1 c.2.1.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 -/
 
@@ -161,17 +161,18 @@ 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
 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 (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 -/
 
@@ -185,15 +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) :
-    (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 (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], ?_⟩
@@ -215,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 _)
@@ -266,7 +270,8 @@ variable (hcoins : ComputableInPolyTime
 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 (((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
@@ -277,8 +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 p.1.1 p.1.2.1 p.1.2.2 p.2.1 p.2.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
@@ -289,8 +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 p.1.1.1 p.1.1.2 p.1.2 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
@@ -312,7 +317,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 (((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
@@ -405,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 p.1.1 p.1.2 p.2.1 p.2.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
@@ -545,7 +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 p.2.1 p.2.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
@@ -576,7 +582,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 ((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)
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. -/
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 =>