From 3bc58fc0a9f37ed0fd5eb13f4bb70debfbd54ab0 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 31 Oct 2026 07:41:40 +0000
Subject: [PATCH 1/2] refactor(CramerShoup): replace projection chains in
 Scheme, Reductions, and CramerShoup (#1764)

---
 .../Crypto/Computational/CramerShoup.lean     |  27 ++--
 .../Computational/CramerShoup/Reductions.lean | 113 +++++++++-------
 .../Computational/CramerShoup/Scheme.lean     | 124 +++++++++++-------
 3 files changed, 159 insertions(+), 105 deletions(-)

diff --git a/Complexity/Crypto/Computational/CramerShoup.lean b/Complexity/Crypto/Computational/CramerShoup.lean
index a3a76c2fde..fd368bf3b6 100644
--- a/Complexity/Crypto/Computational/CramerShoup.lean
+++ b/Complexity/Crypto/Computational/CramerShoup.lean
@@ -183,20 +183,21 @@ noncomputable def cramerShoupMsgCCA2Game
   let τ₂ ← PMF.uniformOfFintype (ZMod (F.order d))
   let sk := F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂
   let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂
+  let pkRest := pkVal.2; let h₁₂ := pkRest.2
   let pk := F.encodeCramerShoupPublicKeyValues d pkVal
   let choiceOut ← ProbComp.eval ((OracleComp.interpret
     (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
       (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
     (adversary.choose n pk)).run ())
-  let choice := choiceOut.1
-  let m₀ := encodeMsg (d, choice.1.1.1)
-  let m₁ := encodeMsg (d, choice.1.1.2)
-  let ad := encodeAD (d, choice.1.2)
+  let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
+  let m₀ := encodeMsg (d, msgs.1)
+  let m₁ := encodeMsg (d, msgs.2)
+  let ad := encodeAD (d, ch.2)
   if isElem (d, m₀) && isElem (d, m₁) then
     let m := if bit then m₁ else m₀
     let β ← PMF.uniformOfFintype (ZMod (F.order d))
     let ct := F.encodeCramerShoupEncrypt H d
-      (F.encode d pkVal.1, F.encode d pkVal.2.1, F.encode d pkVal.2.2.1, F.encode d pkVal.2.2.2)
+      (F.encode d pkVal.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2)
       m ad β.val
     let guessOut ← ProbComp.eval ((OracleComp.interpret
       (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
@@ -315,10 +316,10 @@ noncomputable def cramerShoupGame1
     (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
       (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
     (adversary.choose n pk)).run ())
-  let choice := choiceOut.1
-  let m₀ := encodeMsg (d, choice.1.1.1)
-  let m₁ := encodeMsg (d, choice.1.1.2)
-  let ad := encodeAD (d, choice.1.2)
+  let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
+  let m₀ := encodeMsg (d, msgs.1)
+  let m₁ := encodeMsg (d, msgs.2)
+  let ad := encodeAD (d, ch.2)
   if isElem (d, m₀) && isElem (d, m₁) then
     let m := if bit then m₁ else m₀
     let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -391,10 +392,10 @@ noncomputable def cramerShoupGame2
     (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
       (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
     (adversary.choose n pk)).run ())
-  let choice := choiceOut.1
-  let m₀ := encodeMsg (d, choice.1.1.1)
-  let m₁ := encodeMsg (d, choice.1.1.2)
-  let ad := encodeAD (d, choice.1.2)
+  let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
+  let m₀ := encodeMsg (d, msgs.1)
+  let m₁ := encodeMsg (d, msgs.2)
+  let ad := encodeAD (d, ch.2)
   if isElem (d, m₀) && isElem (d, m₁) then
     let m := if bit then m₁ else m₀
     let ct := F.encodeCramerShoupChallenge H d sk v w m ad
diff --git a/Complexity/Crypto/Computational/CramerShoup/Reductions.lean b/Complexity/Crypto/Computational/CramerShoup/Reductions.lean
index 9b26853680..9f932dd200 100644
--- a/Complexity/Crypto/Computational/CramerShoup/Reductions.lean
+++ b/Complexity/Crypto/Computational/CramerShoup/Reductions.lean
@@ -239,7 +239,8 @@ theorem advantage_bind_sampleCramerShoupTripleExponents_le (n : ℕ) (d : F.Desc
     (k : ZMod (F.order d) → ZMod (F.order d) → ZMod (F.order d) → Game) :
     Game.advantage
       ((ProbComp.eval (F.sampleCramerShoupTripleExponents n d)).bind fun p =>
-        k (p.1 : ZMod (F.order d)) (p.2.1 : ZMod (F.order d)) (p.2.2 : ZMod (F.order d)))
+        let bc := p.2
+        k (p.1 : ZMod (F.order d)) (bc.1 : ZMod (F.order d)) (bc.2 : ZMod (F.order d)))
       ((PMF.uniformOfFintype (ZMod (F.order d))).bind fun α =>
         (PMF.uniformOfFintype (ZMod (F.order d))).bind fun β =>
           (PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => k α β γ) ≤
@@ -691,19 +692,20 @@ noncomputable def cramerShoupMsgToDDHDistinguisher
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (adversary : ADCCA2AdversaryOf Msg AD) (bit : Bool)
     (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool :=
+  let uvw := input.2; let vw := uvw.2
   F.sampleCramerShoupSK n input.1 >>= fun sk =>
-    let pk := F.encodeCramerShoupPublicKey input.1 input.2.1 sk
+    let pk := F.encodeCramerShoupPublicKey input.1 uvw.1 sk
     ((OracleComp.interpret
       (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
         (F.cramerShoupPhase1Oracle hasAD H isElem input.1 sk))
       (adversary.choose n pk)).run ()) >>= fun choiceOut =>
-      let choice := choiceOut.1
-      let m₀ := encodeMsg (input.1, choice.1.1.1)
-      let m₁ := encodeMsg (input.1, choice.1.1.2)
-      let ad := encodeAD (input.1, choice.1.2)
+      let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
+      let m₀ := encodeMsg (input.1, msgs.1)
+      let m₁ := encodeMsg (input.1, msgs.2)
+      let ad := encodeAD (input.1, ch.2)
       if isElem (input.1, m₀) && isElem (input.1, m₁) then
         let m := if bit then m₁ else m₀
-        let ct := F.encodeCramerShoupChallenge H input.1 sk input.2.2.1 input.2.2.2 m ad
+        let ct := F.encodeCramerShoupChallenge H input.1 sk vw.1 vw.2 m ad
         ((OracleComp.interpret
           (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
             (F.cramerShoupPhase2Oracle hasAD H isElem input.1 sk ct ad))
@@ -830,19 +832,20 @@ noncomputable def cramerShoupMsgToCollisionFinder
   fun n d =>
     F.sampleCramerShoupTripleExponents n d >>= fun abc =>
       F.sampleCramerShoupSK n d >>= fun sk =>
+        let bc := abc.2
         let gen := F.encode d (F.generator d)
         let u := F.smul (d, abc.1, gen)
-        let v := F.smul (d, abc.2.1, gen)
-        let w := F.smul (d, abc.2.2, gen)
+        let v := F.smul (d, bc.1, gen)
+        let w := F.smul (d, bc.2, gen)
         let pk := F.encodeCramerShoupPublicKey d u sk
         ((OracleComp.interpret
           (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
             (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
           (adversary.choose n pk)).run ()) >>= fun choiceOut =>
-          let choice := choiceOut.1
-          let m₀ := encodeMsg (d, choice.1.1.1)
-          let m₁ := encodeMsg (d, choice.1.1.2)
-          let ad := encodeAD (d, choice.1.2)
+          let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
+          let m₀ := encodeMsg (d, msgs.1)
+          let m₁ := encodeMsg (d, msgs.2)
+          let ad := encodeAD (d, ch.2)
           if isElem (d, m₀) && isElem (d, m₁) then
             let m := if bit then m₁ else m₀
             let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -978,22 +981,24 @@ theorem isPPTOn_cramerShoupToCollisionFinder
 /-- `encodeCramerShoupPublicKey` depends on `sk` only through its residues modulo `F.order d`. -/
 theorem encodeCramerShoupPublicKey_eq_skNatOfZMod (d : F.Desc)
     (α : ZMod (F.order d)) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) sk =
       F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d))
-        (F.skNatOfZMod d (sk.1.1 : ZMod (F.order d)) (sk.1.2 : ZMod (F.order d))
-          (sk.2.1.1 : ZMod (F.order d)) (sk.2.1.2 : ZMod (F.order d))
-          (sk.2.2.1 : ZMod (F.order d)) (sk.2.2.2 : ZMod (F.order d))) := by
+        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
+          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
+          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) := by
   simp only [encodeCramerShoupPublicKey_encode, skNatOfZMod, ZMod.natCast_zmod_val]
 
 /-- `encodeCramerShoupChallenge` depends on `sk` only through its residues modulo `F.order d`. -/
 theorem encodeCramerShoupChallenge_eq_skNatOfZMod
     (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (v w : F.Carrier d) (m ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupChallenge H d sk (F.encode d v) (F.encode d w) m ad =
       F.encodeCramerShoupChallenge H d
-        (F.skNatOfZMod d (sk.1.1 : ZMod (F.order d)) (sk.1.2 : ZMod (F.order d))
-          (sk.2.1.1 : ZMod (F.order d)) (sk.2.1.2 : ZMod (F.order d))
-          (sk.2.2.1 : ZMod (F.order d)) (sk.2.2.2 : ZMod (F.order d)))
+        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
+          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
+          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d)))
         (F.encode d v) (F.encode d w) m ad := by
   simp only [encodeCramerShoupChallenge, skNatOfZMod, encodeProjHash_encode,
     encodeProjHash2_encode, ZMod.natCast_zmod_val]
@@ -1003,11 +1008,13 @@ theorem decodeCramerShoup_eq_skNatOfZMod
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.decodeCramerShoup H isElem d sk ct ad =
       F.decodeCramerShoup H isElem d
-        (F.skNatOfZMod d (sk.1.1 : ZMod (F.order d)) (sk.1.2 : ZMod (F.order d))
-          (sk.2.1.1 : ZMod (F.order d)) (sk.2.1.2 : ZMod (F.order d))
-          (sk.2.2.1 : ZMod (F.order d)) (sk.2.2.2 : ZMod (F.order d))) ct ad := by
+        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
+          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
+          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) ct ad := by
+  dsimp only
   unfold decodeCramerShoup
   by_cases hvw :
       isElem (d, (decodeBits4 ct).1) = true ∧ isElem (d, (decodeBits4 ct).2.1) = true
@@ -1026,11 +1033,12 @@ theorem cramerShoupPhase1Oracle_eq_skNatOfZMod
     (hasAD : Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.cramerShoupPhase1Oracle hasAD H isElem d sk =
       F.cramerShoupPhase1Oracle hasAD H isElem d
-        (F.skNatOfZMod d (sk.1.1 : ZMod (F.order d)) (sk.1.2 : ZMod (F.order d))
-          (sk.2.1.1 : ZMod (F.order d)) (sk.2.1.2 : ZMod (F.order d))
-          (sk.2.2.1 : ZMod (F.order d)) (sk.2.2.2 : ZMod (F.order d))) := by
+        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
+          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
+          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) := by
   funext req s
   simp only [cramerShoupPhase1Oracle, cramerShoupPhase1Reply,
     F.decodeCramerShoup_eq_skNatOfZMod H isElem hmem d sk]
@@ -1040,11 +1048,12 @@ theorem cramerShoupPhase2Oracle_eq_skNatOfZMod
     (hasAD : Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.cramerShoupPhase2Oracle hasAD H isElem d sk ct ad =
       F.cramerShoupPhase2Oracle hasAD H isElem d
-        (F.skNatOfZMod d (sk.1.1 : ZMod (F.order d)) (sk.1.2 : ZMod (F.order d))
-          (sk.2.1.1 : ZMod (F.order d)) (sk.2.1.2 : ZMod (F.order d))
-          (sk.2.2.1 : ZMod (F.order d)) (sk.2.2.2 : ZMod (F.order d))) ct ad := by
+        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
+          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
+          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) ct ad := by
   funext req s
   simp only [cramerShoupPhase2Oracle, cramerShoupPhase2Reply,
     F.decodeCramerShoup_eq_skNatOfZMod H isElem hmem d sk]
@@ -1055,11 +1064,12 @@ theorem cramerShoupCollisionPhase2Oracle_eq_skNatOfZMod
     (hasAD : Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.cramerShoupCollisionPhase2Oracle hasAD H isElem d sk ct ad =
       F.cramerShoupCollisionPhase2Oracle hasAD H isElem d
-        (F.skNatOfZMod d (sk.1.1 : ZMod (F.order d)) (sk.1.2 : ZMod (F.order d))
-          (sk.2.1.1 : ZMod (F.order d)) (sk.2.1.2 : ZMod (F.order d))
-          (sk.2.2.1 : ZMod (F.order d)) (sk.2.2.2 : ZMod (F.order d))) ct ad := by
+        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
+          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
+          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) ct ad := by
   funext req s
   simp only [cramerShoupCollisionPhase2Oracle, finderPhase2Oracle, cramerShoupCollisionPhase2Reply,
     F.decodeCramerShoup_eq_skNatOfZMod H isElem hmem d sk]
@@ -1072,11 +1082,13 @@ theorem encodeCramerShoupEncrypt_publicKey_eq_challenge
     (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (α β σ τ σ₁ τ₁ σ₂ τ₂ : ZMod (F.order d)) (m ad : List Bool) :
     let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂
+    let pkRest := pkVal.2; let h₁₂ := pkRest.2
     F.encodeCramerShoupEncrypt H d
-      (F.encode d pkVal.1, F.encode d pkVal.2.1, F.encode d pkVal.2.2.1, F.encode d pkVal.2.2.2)
+      (F.encode d pkVal.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2)
       m ad β.val =
       F.encodeCramerShoupChallenge H d (F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂)
         (F.encode d (β • F.generator d)) (F.encode d ((α * β) • F.generator d)) m ad := by
+  dsimp only
   have hαβ : (α * β) • F.generator d = β • (α • F.generator d) := by rw [smul_smul, mul_comm]
   rw [hαβ]
   simp only [encodeCramerShoupEncrypt, encodeCramerShoupChallenge, cramerShoupPublicKey,
@@ -1174,7 +1186,8 @@ theorem computableInPolyTime_cramerShoupValid
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     ComputableInPolyTime
       (fun p : ℕ × List Bool × List Bool × List Bool =>
-        F.cramerShoupValid isElem d p.1 p.2.1 p.2.2.1 p.2.2.2)
+        let r1 := p.2; let r2 := r1.2
+        F.cramerShoupValid isElem d p.1 r1.1 r2.1 r2.2)
       (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool := by
   let EIn := encPair encUnary (encPair encBits (encPair encBits encBits))
   have hd_in : ComputableTidilyInPolyTime
@@ -1225,7 +1238,9 @@ theorem isPPTOn_cramerShoupADEncryptProb
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     IsPPTOn (encPair encUnary (encPair encBits (encPair encBits encAD))) encBits
-      (fun p => F.cramerShoupADEncryptProb encAD H d p.1 p.2.1 p.2.2.1 p.2.2.2) := by
+      (fun p =>
+        let r1 := p.2; let r2 := r1.2
+        F.cramerShoupADEncryptProb encAD H d p.1 r1.1 r2.1 r2.2) := by
   let E0 := encPair encUnary (encPair encBits (encPair encBits encAD))
   let E1 := encPair E0 encNat
   have hct : ComputableTidilyInPolyTime
@@ -1247,7 +1262,9 @@ theorem isPPTOn_cramerShoupEncryptProb
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits
-      (fun p => F.cramerShoupEncryptProb H d p.1 p.2.1 p.2.2) := by
+      (fun p =>
+        let r1 := p.2
+        F.cramerShoupEncryptProb H d p.1 r1.1 r1.2) := by
   let E0 := encPair encUnary (encPair encBits encBits)
   let E1 := encPair E0 encNat
   have hct : ComputableTidilyInPolyTime
@@ -1271,7 +1288,8 @@ theorem computableInPolyTime_cramerShoupADDecryptOpt
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     ComputableInPolyTime
       (fun p : ℕ × List Bool × List Bool × List Bool =>
-        F.cramerShoupADDecryptOpt H isElem d p.1 p.2.1 p.2.2.1 p.2.2.2)
+        let r1 := p.2; let r2 := r1.2
+        F.cramerShoupADDecryptOpt H isElem d p.1 r1.1 r2.1 r2.2)
       (encPair encUnary (encPair encBits (encPair encBits encBits))) (encOption encBits) := by
   exact .of_tidy (F.computableTidilyInPolyTime_decodeCramerShoup hH.tidy hisElem.tidy
     (hd.tidy.comp (by fun_prop))
@@ -1287,7 +1305,9 @@ theorem computableInPolyTime_cramerShoupDecryptOpt
     (hisElem : ComputableInPolyTime isElem (encPair F.encDesc encBits) encBool)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool => F.cramerShoupDecryptOpt H isElem d p.1 p.2.1 p.2.2)
+      (fun p : ℕ × List Bool × List Bool =>
+        let r1 := p.2
+        F.cramerShoupDecryptOpt H isElem d p.1 r1.1 r1.2)
       (encPair encUnary (encPair encBits encBits)) (encOption encBits) := by
   exact .of_tidy (F.computableTidilyInPolyTime_decodeCramerShoup hH.tidy hisElem.tidy
     (hd.tidy.comp (by fun_prop))
@@ -1345,10 +1365,11 @@ theorem cca2Phase2Oracle_cramerShoupDecryptOpt
 @[simp]
 theorem decodeBits4_dropFrame_encodeCramerShoupPublicKey
     (d : F.Desc) (u : List Bool) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     decodeBits4 (dropFrame (F.encodeCramerShoupPublicKey d u sk)) =
-      (u, F.encodeProjHashAux d sk.1.1 sk.1.2 u,
-        F.encodeProjHashAux d sk.2.1.1 sk.2.1.2 u,
-        F.encodeProjHashAux d sk.2.2.1 sk.2.2.2 u) := by
+      (u, F.encodeProjHashAux d st.1 st.2 u,
+        F.encodeProjHashAux d st₁.1 st₁.2 u,
+        F.encodeProjHashAux d st₂.1 st₂.2 u) := by
   simp [encodeCramerShoupPublicKey, encPair_apply, dropFrame_frame_append]
 
 /-- `encodeCramerShoupEncrypt` on the public-key words generated by `skNatOfZMod` agrees with
@@ -1358,14 +1379,16 @@ theorem encodeCramerShoupEncrypt_skNatOfZMod
     (α σ τ σ₁ τ₁ σ₂ τ₂ : ZMod (F.order d)) (m ad : List Bool) (b : ℕ) :
     let u := F.encode d (α • F.generator d)
     let sk := F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂
+    let pkRest := pkVal.2; let h₁₂ := pkRest.2
     F.encodeCramerShoupEncrypt H d
-      (u, F.encodeProjHashAux d sk.1.1 sk.1.2 u,
-        F.encodeProjHashAux d sk.2.1.1 sk.2.1.2 u,
-        F.encodeProjHashAux d sk.2.2.1 sk.2.2.2 u) m ad b =
+      (u, F.encodeProjHashAux d st.1 st.2 u,
+        F.encodeProjHashAux d st₁.1 st₁.2 u,
+        F.encodeProjHashAux d st₂.1 st₂.2 u) m ad b =
       F.encodeCramerShoupEncrypt H d
-        (F.encode d pkVal.1, F.encode d pkVal.2.1,
-          F.encode d pkVal.2.2.1, F.encode d pkVal.2.2.2)
+        (F.encode d pkVal.1, F.encode d pkRest.1,
+          F.encode d h₁₂.1, F.encode d h₁₂.2)
         m ad (b : ZMod (F.order d)).val := by
   simp only [skNatOfZMod, encodeProjHashAux_encode, ZMod.natCast_zmod_val,
     cramerShoupPublicKey, projHash2Aux, encodeCramerShoupEncrypt, F.smul_encode, F.add_encode]
diff --git a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean
index 4e60a0c43c..d2766f3965 100644
--- a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean
+++ b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean
@@ -318,11 +318,13 @@ noncomputable def cca2ADGameOn {Msg AD Out : Type}
       (cca2ADPhase1Oracle encOut decrypt n keys.2))
     (adversary.choose n keys.1)).run ()
   let choice := choiceOut.1
-  if valid n keys.1 choice.1.1.1 choice.1.1.2 then
-    let ct ← encrypt n keys.1 (if bit then choice.1.1.2 else choice.1.1.1) choice.1.2
+  let ch := choice.1
+  let msgs := ch.1
+  if valid n keys.1 msgs.1 msgs.2 then
+    let ct ← encrypt n keys.1 (if bit then msgs.2 else msgs.1) ch.2
     let guessOut ← (OracleComp.interpret
       (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
-        (cca2ADPhase2Oracle encOut decrypt n keys.2 ct (encAD choice.1.2)))
+        (cca2ADPhase2Oracle encOut decrypt n keys.2 ct (encAD ch.2)))
       (adversary.guess n choice.2 ct)).run ()
     return guessOut.1
   else
@@ -425,7 +427,9 @@ theorem decodeBits4_encBits4 (p : List Bool × List Bool × List Bool × List Bo
 associated-data bit string `ad`. -/
 def extractCramerShoupTuple (ct ad : List Bool) : List Bool :=
   let parts := decodeBits4 ct
-  encBits4 (parts.1, parts.2.1, parts.2.2.1, ad)
+  let rest := parts.2
+  let ez := rest.2
+  encBits4 (parts.1, rest.1, ez.1, ad)
 
 @[simp]
 theorem extractCramerShoupTuple_encBits4 (v w e z' ad : List Bool) :
@@ -513,9 +517,10 @@ def cramerShoupEncrypt (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (pk : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d)
     (m : F.Carrier d) (ad : List Bool) (β : ZMod (F.order d)) :
     F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d :=
-  let v := β • F.generator d; let w := β • pk.1; let e := β • pk.2.1 + m
+  let pkRest := pk.2; let h₁₂ := pkRest.2
+  let v := β • F.generator d; let w := β • pk.1; let e := β • pkRest.1 + m
   let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d v w e ad)
-  (v, w, e, β • (pk.2.2.1 + ρ • pk.2.2.2))
+  (v, w, e, β • (h₁₂.1 + ρ • h₁₂.2))
 
 /-- Under a genuine public key `cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂`, the components of
 `cramerShoupEncrypt` coincide with projective hash evaluation (`Game 0 = Game 1`,
@@ -550,9 +555,11 @@ def cramerShoupDecrypt [∀ d, DecidableEq (F.Carrier d)]
       ((ZMod (F.order d) × ZMod (F.order d)) × (ZMod (F.order d) × ZMod (F.order d))))
     (ct : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) (ad : List Bool) :
     Option (F.Carrier d) :=
-  let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d ct.1 ct.2.1 ct.2.2.1 ad)
-  if projHash2 F d sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2 ρ ct.1 ct.2.1 = ct.2.2.2 then
-    some (ct.2.2.1 - projHash F d sk.1.1 sk.1.2 ct.1 ct.2.1)
+  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
+  let ctRest := ct.2; let ez := ctRest.2
+  let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d ct.1 ctRest.1 ez.1 ad)
+  if projHash2 F d st₁.1 st₁.2 st₂.1 st₂.2 ρ ct.1 ctRest.1 = ez.2 then
+    some (ez.1 - projHash F d st.1 st.2 ct.1 ctRest.1)
   else
     none
 
@@ -624,23 +631,26 @@ theorem encodeProjHash2_encode (d : F.Desc) (s₁ t₁ s₂ t₂ r : ℕ) (v w :
 key word presented to a 1CCA adversary. -/
 def encodeCramerShoupPublicKeyValues (d : F.Desc)
     (pk : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) : List Bool :=
+  let pkRest := pk.2; let h₁₂ := pkRest.2
   encPair F.encDesc encBits4
-    (d, (F.encode d pk.1, F.encode d pk.2.1, F.encode d pk.2.2.1, F.encode d pk.2.2.2))
+    (d, (F.encode d pk.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2))
 
 /-- Word-level Cramer–Shoup public key generation from `d : F.Desc`, an encoded
 `u = encode (α • g)`, and natural-number secret exponents
 `sk = ((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
 def encodeCramerShoupPublicKey (d : F.Desc) (u : List Bool)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) : List Bool :=
-  encPair F.encDesc encBits4 (d, (u, F.encodeProjHashAux d sk.1.1 sk.1.2 u,
-    F.encodeProjHashAux d sk.2.1.1 sk.2.1.2 u, F.encodeProjHashAux d sk.2.2.1 sk.2.2.2 u))
+  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
+  encPair F.encDesc encBits4 (d, (u, F.encodeProjHashAux d st.1 st.2 u,
+    F.encodeProjHashAux d st₁.1 st₁.2 u, F.encodeProjHashAux d st₂.1 st₂.2 u))
 
 @[simp]
 theorem encodeCramerShoupPublicKey_encode (d : F.Desc) (α : ZMod (F.order d))
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) sk =
       F.encodeCramerShoupPublicKeyValues d
-        (F.cramerShoupPublicKey d α sk.1.1 sk.1.2 sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2) := by
+        (F.cramerShoupPublicKey d α st.1 st.2 st₁.1 st₁.2 st₂.1 st₂.2) := by
   simp only [encodeCramerShoupPublicKey, encodeCramerShoupPublicKeyValues,
     encodeProjHashAux_encode, cramerShoupPublicKey, projHash2Aux]
 
@@ -648,23 +658,26 @@ theorem encodeCramerShoupPublicKey_encode (d : F.Desc) (α : ZMod (F.order d))
 string. -/
 def encodeCramerShoupCiphertext (d : F.Desc)
     (ct : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) : List Bool :=
-  encBits4 (F.encode d ct.1, F.encode d ct.2.1, F.encode d ct.2.2.1, F.encode d ct.2.2.2)
+  let ctRest := ct.2; let ez := ctRest.2
+  encBits4 (F.encode d ct.1, F.encode d ctRest.1, F.encode d ez.1, F.encode d ez.2)
 
 /-- Word-level Cramer–Shoup encryption from the public key `(u, h, h₁, h₂)`, encoded message `m`,
 encoded associated data `ad`, and randomness `b : ℕ`. -/
 def encodeCramerShoupEncrypt (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (pk : List Bool × List Bool × List Bool × List Bool) (m ad : List Bool) (b : ℕ) : List Bool :=
+  let pkRest := pk.2; let h₁₂ := pkRest.2
   let v := F.smul (d, b, F.encode d (F.generator d)); let w := F.smul (d, b, pk.1)
-  let e := F.add (d, F.smul (d, b, pk.2.1), m)
+  let e := F.add (d, F.smul (d, b, pkRest.1), m)
   let r := ofBits (H (d, encBits4 (v, w, e, ad)))
-  encBits4 (v, w, e, F.smul (d, b, F.add (d, pk.2.2.1, F.smul (d, r, pk.2.2.2))))
+  encBits4 (v, w, e, F.smul (d, b, F.add (d, h₁₂.1, F.smul (d, r, h₁₂.2))))
 
 @[simp]
 theorem encodeCramerShoupEncrypt_encode (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (pk : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d)
     (m : F.Carrier d) (ad : List Bool) (b : ℕ) :
+    let pkRest := pk.2; let h₁₂ := pkRest.2
     F.encodeCramerShoupEncrypt H d
-      (F.encode d pk.1, F.encode d pk.2.1, F.encode d pk.2.2.1, F.encode d pk.2.2.2)
+      (F.encode d pk.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2)
       (F.encode d m) ad b =
       F.encodeCramerShoupCiphertext d
         (F.cramerShoupEncrypt H d pk m ad (b : ZMod (F.order d))) := by
@@ -676,17 +689,19 @@ theorem encodeCramerShoupEncrypt_encode (H : F.Desc × List Bool → List Bool)
 Game 1, printed p. 490, and Exercise 12.27, printed pp. 521–522). -/
 def encodeCramerShoupChallenge (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (v w m ad : List Bool) : List Bool :=
-  let e := F.add (d, F.encodeProjHash d sk.1.1 sk.1.2 v w, m)
+  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
+  let e := F.add (d, F.encodeProjHash d st.1 st.2 v w, m)
   let r := ofBits (H (d, encBits4 (v, w, e, ad)))
-  encBits4 (v, w, e, F.encodeProjHash2 d sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2 r v w)
+  encBits4 (v, w, e, F.encodeProjHash2 d st₁.1 st₁.2 st₂.1 st₂.2 r v w)
 
 @[simp]
 theorem encodeCramerShoupChallenge_encode (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (v w m : F.Carrier d) (ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupChallenge H d sk (F.encode d v) (F.encode d w) (F.encode d m) ad =
-      let e := projHash F d sk.1.1 sk.1.2 v w + m
+      let e := projHash F d st.1 st.2 v w + m
       let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d v w e ad)
-      let z' := projHash2 F d sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2 ρ v w
+      let z' := projHash2 F d st₁.1 st₁.2 st₂.1 st₂.2 ρ v w
       F.encodeCramerShoupCiphertext d (v, w, e, z') := by
   simp only [encodeCramerShoupChallenge, encodeProjHash_encode, F.add_encode,
     encodeProjHash2_encode, encodeCramerShoupTuple, cramerShoupHashMod,
@@ -701,12 +716,13 @@ all pass, return `some (encode (e - f_{s,t}(v, w)))`, else `none`. -/
 def decodeCramerShoup (H : F.Desc × List Bool → List Bool)
     (isElem : F.Desc × List Bool → Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) : Option (List Bool) :=
-  let parts := decodeBits4 ct
-  let v := parts.1; let w := parts.2.1; let e := parts.2.2.1; let z' := parts.2.2.2
+  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
+  let parts := decodeBits4 ct; let rest := parts.2; let ez := rest.2
+  let v := parts.1; let w := rest.1; let e := ez.1; let z' := ez.2
   let r := ofBits (H (d, encBits4 (v, w, e, ad)))
   if (encBits4 parts == ct) && isElem (d, v) && isElem (d, w) && isElem (d, e) &&
-      (F.encodeProjHash2 d sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2 r v w == z') then
-    some (F.add (d, e, F.encodeGroupNeg d (F.encodeProjHash d sk.1.1 sk.1.2 v w)))
+      (F.encodeProjHash2 d st₁.1 st₁.2 st₂.1 st₂.2 r v w == z') then
+    some (F.add (d, e, F.encodeGroupNeg d (F.encodeProjHash d st.1 st.2 v w)))
   else
     none
 
@@ -717,11 +733,12 @@ theorem decodeCramerShoup_encode [∀ d, DecidableEq (F.Carrier d)]
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ)))
     (ct : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) (ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.decodeCramerShoup H isElem d sk (F.encodeCramerShoupCiphertext d ct) ad =
       (F.cramerShoupDecrypt H d
-        (((sk.1.1 : ZMod (F.order d)), (sk.1.2 : ZMod (F.order d))),
-          (((sk.2.1.1 : ZMod (F.order d)), (sk.2.1.2 : ZMod (F.order d))),
-            ((sk.2.2.1 : ZMod (F.order d)), (sk.2.2.2 : ZMod (F.order d))))) ct ad).map
+        (((st.1 : ZMod (F.order d)), (st.2 : ZMod (F.order d))),
+          (((st₁.1 : ZMod (F.order d)), (st₁.2 : ZMod (F.order d))),
+            ((st₂.1 : ZMod (F.order d)), (st₂.2 : ZMod (F.order d))))) ct ad).map
         (F.encode d) := by
   rcases ct with ⟨v, w, e, z'⟩
   have hv : isElem (d, F.encode d v) = true := (hmem d _).mpr ⟨v, rfl⟩
@@ -743,12 +760,14 @@ theorem decodeCramerShoup_cramerShoupEncrypt
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (α β : ZMod (F.order d))
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (m : F.Carrier d) (ad : List Bool) :
+    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.decodeCramerShoup H isElem d sk
       (F.encodeCramerShoupCiphertext d
         (F.cramerShoupEncrypt H d
-          (F.cramerShoupPublicKey d α sk.1.1 sk.1.2 sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2)
+          (F.cramerShoupPublicKey d α st.1 st.2 st₁.1 st₁.2 st₂.1 st₂.2)
           m ad β)) ad = some (F.encode d m) := by
   classical
+  dsimp only
   rw [F.decodeCramerShoup_encode H isElem hmem, F.cramerShoupDecrypt_cramerShoupEncrypt]; rfl
 
 /-! ### Polynomial-time certificates for word-level operations -/
@@ -829,7 +848,8 @@ private theorem computableTidilyInPolyTime_encodeCramerShoupPublicKey
 theorem computableInPolyTime_encodeCramerShoupPublicKey :
     ComputableInPolyTime
       (fun p : F.Desc × List Bool × ((ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) =>
-        F.encodeCramerShoupPublicKey p.1 p.2.1 p.2.2)
+        let rest := p.2
+        F.encodeCramerShoupPublicKey p.1 rest.1 rest.2)
       (encPair F.encDesc (encPair encBits encCramerShoupSK)) encBits :=
   .of_tidy (F.computableTidilyInPolyTime_encodeCramerShoupPublicKey
     (by fun_prop) (by fun_prop) (by fun_prop))
@@ -865,7 +885,8 @@ theorem computableInPolyTime_encodeCramerShoupChallenge
     ComputableInPolyTime
       (fun p : F.Desc × ((ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) ×
           List Bool × List Bool × List Bool × List Bool =>
-        F.encodeCramerShoupChallenge H p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2.1 p.2.2.2.2.2)
+        let r1 := p.2; let r2 := r1.2; let r3 := r2.2; let r4 := r3.2
+        F.encodeCramerShoupChallenge H p.1 r1.1 r2.1 r3.1 r4.1 r4.2)
       (encPair F.encDesc (encPair encCramerShoupSK
         (encPair encBits (encPair encBits (encPair encBits encBits)))))
       encBits :=
@@ -905,7 +926,8 @@ theorem computableInPolyTime_encodeCramerShoupEncrypt
     ComputableInPolyTime
       (fun p : F.Desc × (List Bool × List Bool × List Bool × List Bool) ×
           List Bool × List Bool × ℕ =>
-        F.encodeCramerShoupEncrypt H p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2)
+        let r1 := p.2; let r2 := r1.2; let r3 := r2.2
+        F.encodeCramerShoupEncrypt H p.1 r1.1 r2.1 r3.1 r3.2)
       (encPair F.encDesc (encPair encBits4 (encPair encBits (encPair encBits encNat)))) encBits :=
   .of_tidy (F.computableTidilyInPolyTime_encodeCramerShoupEncrypt hH.tidy
     (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop))
@@ -955,7 +977,8 @@ theorem computableInPolyTime_decodeCramerShoup
     (hisElem : ComputableInPolyTime isElem (encPair F.encDesc encBits) encBool) :
     ComputableInPolyTime
       (fun p : F.Desc × ((ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) × List Bool × List Bool =>
-        F.decodeCramerShoup H isElem p.1 p.2.1 p.2.2.1 p.2.2.2)
+        let r1 := p.2; let r2 := r1.2
+        F.decodeCramerShoup H isElem p.1 r1.1 r2.1 r2.2)
       (encPair F.encDesc (encPair encCramerShoupSK (encPair encBits encBits)))
       (encOption encBits) :=
   .of_tidy (F.computableTidilyInPolyTime_decodeCramerShoup hH.tidy hisElem.tidy
@@ -1057,8 +1080,9 @@ noncomputable def cramerShoupGame3
   let pk := F.encodeCramerShoupPublicKey d u sk
   runStatelessOracle (F.cramerShoupPhase1Reply hasAD H isElem d sk)
     (adversary.choose n pk) fun choice =>
-    let m₀ := encodeMsg (d, choice.1.1.1); let m₁ := encodeMsg (d, choice.1.1.2)
-    let ad := encodeAD (d, choice.1.2)
+    let ch := choice.1; let msgs := ch.1
+    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
+    let ad := encodeAD (d, ch.2)
     if isElem (d, m₀) && isElem (d, m₁) then
       let m := if bit then m₁ else m₀
       let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1078,7 +1102,8 @@ def decodeCramerShoupDH
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (d : F.Desc) (α δ δ₁ δ₂ : ZMod (F.order d)) (ct ad : List Bool) : Option (List Bool) :=
   let parts := decodeBits4 ct
-  if parts.2.1 == F.smul (d, α.val, parts.1) then
+  let rest := parts.2
+  if rest.1 == F.smul (d, α.val, parts.1) then
     F.decodeCramerShoup H isElem d (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0) ct ad
   else
     none
@@ -1109,12 +1134,13 @@ def isCramerShoupBadDH
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (d : F.Desc) (α : ZMod (F.order d))
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct_q ad_q : List Bool) : Bool :=
-  let parts := decodeBits4 ct_q
-  let v := parts.1; let w := parts.2.1; let e := parts.2.2.1; let z' := parts.2.2.2
+  let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
+  let parts := decodeBits4 ct_q; let rest := parts.2; let ez := rest.2
+  let v := parts.1; let w := rest.1; let e := ez.1; let z' := ez.2
   let r := ofBits (H (d, encBits4 (v, w, e, ad_q)))
   (encBits4 parts == ct_q) && isElem (d, v) && isElem (d, w) && isElem (d, e) &&
     (w != F.smul (d, α.val, v)) &&
-    (F.encodeProjHash2 d sk.2.1.1 sk.2.1.2 sk.2.2.1 sk.2.2.2 r v w == z')
+    (F.encodeProjHash2 d st₁.1 st₁.2 st₂.1 st₂.2 r v w == z')
 
 private theorem encodeCramerShoupPublicKey_fiber_eq (d : F.Desc)
     (α δ τ δ₁ τ₁ δ₂ τ₂ : ZMod (F.order d)) :
@@ -1439,14 +1465,15 @@ def HonestPhase2QueryBound (hasAD : Bool) {Msg AD : Type}
         (F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d))
           (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)))).run ())).support,
     ∀ mElem : F.Carrier d,
+      let choice := choiceOut.1; let ch := choice.1
       let v := F.encode d (β • F.generator d); let w := F.encode d (γ • F.generator d)
       let e := F.encode d (projHash F d (δ - α * τ) τ (β • F.generator d) (γ • F.generator d) +
         mElem)
-      let ad := encodeAD (d, choiceOut.1.1.2)
+      let ad := encodeAD (d, ch.2)
       let ρ := F.cramerShoupHashMod H d (encBits4 (v, w, e, ad))
       let ct := encBits4 (v, w, e,
         F.encode d ((β * (δ₁ + ρ * δ₂) + (γ - α * β) * ξ) • F.generator d))
-      (adversary.guess n choiceOut.1.2 ct).IsQueryBounded Q₂
+      (adversary.guess n choice.2 ct).IsQueryBounded Q₂
 
 /-- **Game 3.5** (intermediate hybrid between Game 3 and Game 4 of [BonehShoup2023],
 Section 12.5.3, printed pp. 491–492): under the fiber change of variables
@@ -1467,8 +1494,9 @@ noncomputable def cramerShoupGame3Half
   let pk := F.encodeCramerShoupPublicKey d u (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)
   runStatelessOracle (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂)
     (adversary.choose n pk) fun choice =>
-    let m₀ := encodeMsg (d, choice.1.1.1); let m₁ := encodeMsg (d, choice.1.1.2)
-    let ad := encodeAD (d, choice.1.2)
+    let ch := choice.1; let msgs := ch.1
+    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
+    let ad := encodeAD (d, ch.2)
     if isElem (d, m₀) && isElem (d, m₁) then
       let m := if bit then m₁ else m₀
       let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1543,8 +1571,9 @@ noncomputable def cramerShoupGame4
   let pk := F.encodeCramerShoupPublicKey d u (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)
   runStatelessOracle (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂)
     (adversary.choose n pk) fun choice =>
-    let m₀ := encodeMsg (d, choice.1.1.1); let m₁ := encodeMsg (d, choice.1.1.2)
-    let ad := encodeAD (d, choice.1.2)
+    let ch := choice.1; let msgs := ch.1
+    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
+    let ad := encodeAD (d, ch.2)
     if isElem (d, m₀) && isElem (d, m₁) then
       let m := if bit then m₁ else m₀
       let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1696,8 +1725,9 @@ noncomputable def cramerShoupGame5
   let pk := F.encodeCramerShoupPublicKey d u (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)
   runStatelessOracle (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂)
     (adversary.choose n pk) fun choice =>
-    let m₀ := encodeMsg (d, choice.1.1.1); let m₁ := encodeMsg (d, choice.1.1.2)
-    let ad := encodeAD (d, choice.1.2)
+    let ch := choice.1; let msgs := ch.1
+    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
+    let ad := encodeAD (d, ch.2)
     if isElem (d, m₀) && isElem (d, m₁) then
       let e := F.encode d (ζ • F.generator d)
       let r := ofBits (H (d, encBits4 (v, w, e, ad)))

From c217ab15088259b68bbc1a8986b468f670a9a70e Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 31 Oct 2026 14:55:40 +0000
Subject: [PATCH 2/2] Address PR #1985 review: add named Cramer-Shoup accessors
 and document automation exceptions

---
 .../Crypto/Computational/CramerShoup.lean     |  37 +-
 .../Computational/CramerShoup/Reductions.lean | 123 +++----
 .../Computational/CramerShoup/Scheme.lean     | 328 +++++++++++++-----
 ComplexityTests/Crypto/CramerShoup.lean       |   1 +
 4 files changed, 312 insertions(+), 177 deletions(-)

diff --git a/Complexity/Crypto/Computational/CramerShoup.lean b/Complexity/Crypto/Computational/CramerShoup.lean
index fd368bf3b6..e5eb92ee5d 100644
--- a/Complexity/Crypto/Computational/CramerShoup.lean
+++ b/Complexity/Crypto/Computational/CramerShoup.lean
@@ -183,21 +183,21 @@ noncomputable def cramerShoupMsgCCA2Game
   let τ₂ ← PMF.uniformOfFintype (ZMod (F.order d))
   let sk := F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂
   let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂
-  let pkRest := pkVal.2; let h₁₂ := pkRest.2
   let pk := F.encodeCramerShoupPublicKeyValues d pkVal
   let choiceOut ← ProbComp.eval ((OracleComp.interpret
     (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
       (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
     (adversary.choose n pk)).run ())
-  let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
-  let m₀ := encodeMsg (d, msgs.1)
-  let m₁ := encodeMsg (d, msgs.2)
-  let ad := encodeAD (d, ch.2)
+  let choice := choiceOut.1
+  let m₀ := encodeMsg (d, csChoiceMsg₀ choice)
+  let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+  let ad := encodeAD (d, csChoiceAD choice)
   if isElem (d, m₀) && isElem (d, m₁) then
     let m := if bit then m₁ else m₀
     let β ← PMF.uniformOfFintype (ZMod (F.order d))
     let ct := F.encodeCramerShoupEncrypt H d
-      (F.encode d pkVal.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2)
+      (F.encode d (csPkU pkVal), F.encode d (csPkH pkVal),
+        F.encode d (csPkH₁ pkVal), F.encode d (csPkH₂ pkVal))
       m ad β.val
     let guessOut ← ProbComp.eval ((OracleComp.interpret
       (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
@@ -316,10 +316,10 @@ noncomputable def cramerShoupGame1
     (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
       (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
     (adversary.choose n pk)).run ())
-  let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
-  let m₀ := encodeMsg (d, msgs.1)
-  let m₁ := encodeMsg (d, msgs.2)
-  let ad := encodeAD (d, ch.2)
+  let choice := choiceOut.1
+  let m₀ := encodeMsg (d, csChoiceMsg₀ choice)
+  let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+  let ad := encodeAD (d, csChoiceAD choice)
   if isElem (d, m₀) && isElem (d, m₁) then
     let m := if bit then m₁ else m₀
     let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -343,6 +343,7 @@ theorem cramerShoupMsgCCA2Game_eq_game1
       F.cramerShoupGame1 hasAD encodeMsg encodeAD setup H isElem adversary bit n := by
   simp only [cramerShoupMsgCCA2Game, cramerShoupGame1, PMF.monad_bind_eq_bind,
     PMF.monad_pure_eq_pure, encodeCramerShoupPublicKey_encode, skNatOfZMod,
+    csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂, csChoiceMsg₀, csChoiceMsg₁, csChoiceAD,
     ZMod.natCast_zmod_val, encodeCramerShoupEncrypt_publicKey_eq_challenge]
   refine congrArg _ (funext fun d => congrArg _ (funext fun α => ?_))
   conv_rhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod (F.order d)))]
@@ -392,10 +393,10 @@ noncomputable def cramerShoupGame2
     (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
       (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
     (adversary.choose n pk)).run ())
-  let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
-  let m₀ := encodeMsg (d, msgs.1)
-  let m₁ := encodeMsg (d, msgs.2)
-  let ad := encodeAD (d, ch.2)
+  let choice := choiceOut.1
+  let m₀ := encodeMsg (d, csChoiceMsg₀ choice)
+  let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+  let ad := encodeAD (d, csChoiceAD choice)
   if isElem (d, m₀) && isElem (d, m₁) then
     let m := if bit then m₁ else m₀
     let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1522,7 +1523,9 @@ theorem advantage_cca2ADGameOn_cramerShoupADGroupCCA2Game_le
         congrArg _ (funext fun τ₁ => congrArg _ (funext fun σ₂ =>
           congrArg _ (funext fun τ₂ => ?_)))))))
     simp only [cramerShoupCCA2InnerSK, cramerShoupCCA2InnerB, ↓reduceIte,
-      encodeCramerShoupPublicKey_encode, skNatOfZMod, ZMod.natCast_zmod_val]
+      encodeCramerShoupPublicKey_encode, skNatOfZMod,
+      csPkU, csPkH, csPkH₁, csPkH₂, csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂,
+      csChoiceMsg₀, csChoiceMsg₁, csChoiceAD, ZMod.natCast_zmod_val]
   rw [hgame0, hgame1]
   exact F.advantage_cramerShoupCCA2InnerSK_le true (fun p => encAD p.2) H isElem (d n)
     adversary bit n
@@ -1666,7 +1669,9 @@ theorem advantage_cca2GameOn_cramerShoupGroupCCA2Game_le
         congrArg _ (funext fun τ₁ => congrArg _ (funext fun σ₂ =>
           congrArg _ (funext fun τ₂ => ?_)))))))
     simp only [cramerShoupCCA2InnerSK, cramerShoupCCA2InnerB, ↓reduceIte,
-      encodeCramerShoupPublicKey_encode, skNatOfZMod, ZMod.natCast_zmod_val]
+      encodeCramerShoupPublicKey_encode, skNatOfZMod,
+      csPkU, csPkH, csPkH₁, csPkH₂, csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂,
+      csChoiceMsg₀, csChoiceMsg₁, ZMod.natCast_zmod_val]
   rw [hgame0, hgame1]
   exact F.advantage_cramerShoupCCA2InnerSK_le false (fun _ => []) H isElem (d n)
     adversary.toADUnit bit n
diff --git a/Complexity/Crypto/Computational/CramerShoup/Reductions.lean b/Complexity/Crypto/Computational/CramerShoup/Reductions.lean
index 9f932dd200..142048abf1 100644
--- a/Complexity/Crypto/Computational/CramerShoup/Reductions.lean
+++ b/Complexity/Crypto/Computational/CramerShoup/Reductions.lean
@@ -692,20 +692,19 @@ noncomputable def cramerShoupMsgToDDHDistinguisher
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (adversary : ADCCA2AdversaryOf Msg AD) (bit : Bool)
     (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool :=
-  let uvw := input.2; let vw := uvw.2
   F.sampleCramerShoupSK n input.1 >>= fun sk =>
-    let pk := F.encodeCramerShoupPublicKey input.1 uvw.1 sk
+    let pk := F.encodeCramerShoupPublicKey input.1 (csDdhU input) sk
     ((OracleComp.interpret
       (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
         (F.cramerShoupPhase1Oracle hasAD H isElem input.1 sk))
       (adversary.choose n pk)).run ()) >>= fun choiceOut =>
-      let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
-      let m₀ := encodeMsg (input.1, msgs.1)
-      let m₁ := encodeMsg (input.1, msgs.2)
-      let ad := encodeAD (input.1, ch.2)
+      let choice := choiceOut.1
+      let m₀ := encodeMsg (input.1, csChoiceMsg₀ choice)
+      let m₁ := encodeMsg (input.1, csChoiceMsg₁ choice)
+      let ad := encodeAD (input.1, csChoiceAD choice)
       if isElem (input.1, m₀) && isElem (input.1, m₁) then
         let m := if bit then m₁ else m₀
-        let ct := F.encodeCramerShoupChallenge H input.1 sk vw.1 vw.2 m ad
+        let ct := F.encodeCramerShoupChallenge H input.1 sk (csDdhV input) (csDdhW input) m ad
         ((OracleComp.interpret
           (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
             (F.cramerShoupPhase2Oracle hasAD H isElem input.1 sk ct ad))
@@ -832,20 +831,19 @@ noncomputable def cramerShoupMsgToCollisionFinder
   fun n d =>
     F.sampleCramerShoupTripleExponents n d >>= fun abc =>
       F.sampleCramerShoupSK n d >>= fun sk =>
-        let bc := abc.2
         let gen := F.encode d (F.generator d)
-        let u := F.smul (d, abc.1, gen)
-        let v := F.smul (d, bc.1, gen)
-        let w := F.smul (d, bc.2, gen)
+        let u := F.smul (d, csExpA abc, gen)
+        let v := F.smul (d, csExpB abc, gen)
+        let w := F.smul (d, csExpC abc, gen)
         let pk := F.encodeCramerShoupPublicKey d u sk
         ((OracleComp.interpret
           (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
             (F.cramerShoupPhase1Oracle hasAD H isElem d sk))
           (adversary.choose n pk)).run ()) >>= fun choiceOut =>
-          let choice := choiceOut.1; let ch := choice.1; let msgs := ch.1
-          let m₀ := encodeMsg (d, msgs.1)
-          let m₁ := encodeMsg (d, msgs.2)
-          let ad := encodeAD (d, ch.2)
+          let choice := choiceOut.1
+          let m₀ := encodeMsg (d, csChoiceMsg₀ choice)
+          let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+          let ad := encodeAD (d, csChoiceAD choice)
           if isElem (d, m₀) && isElem (d, m₁) then
             let m := if bit then m₁ else m₀
             let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -981,47 +979,44 @@ theorem isPPTOn_cramerShoupToCollisionFinder
 /-- `encodeCramerShoupPublicKey` depends on `sk` only through its residues modulo `F.order d`. -/
 theorem encodeCramerShoupPublicKey_eq_skNatOfZMod (d : F.Desc)
     (α : ZMod (F.order d)) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) sk =
       F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d))
-        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
-          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
-          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) := by
-  simp only [encodeCramerShoupPublicKey_encode, skNatOfZMod, ZMod.natCast_zmod_val]
+        (F.skNatOfZMod d ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d))) := by
+  simp only [encodeCramerShoupPublicKey_encode, skNatOfZMod,
+    csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂, ZMod.natCast_zmod_val]
 
 /-- `encodeCramerShoupChallenge` depends on `sk` only through its residues modulo `F.order d`. -/
 theorem encodeCramerShoupChallenge_eq_skNatOfZMod
     (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (v w : F.Carrier d) (m ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupChallenge H d sk (F.encode d v) (F.encode d w) m ad =
       F.encodeCramerShoupChallenge H d
-        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
-          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
-          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d)))
+        (F.skNatOfZMod d ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d)))
         (F.encode d v) (F.encode d w) m ad := by
   simp only [encodeCramerShoupChallenge, skNatOfZMod, encodeProjHash_encode,
-    encodeProjHash2_encode, ZMod.natCast_zmod_val]
+    encodeProjHash2_encode, csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂, ZMod.natCast_zmod_val]
 
 /-- `decodeCramerShoup` depends on `sk` only through its residues modulo `F.order d`. -/
 theorem decodeCramerShoup_eq_skNatOfZMod
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.decodeCramerShoup H isElem d sk ct ad =
       F.decodeCramerShoup H isElem d
-        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
-          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
-          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) ct ad := by
-  dsimp only
+        (F.skNatOfZMod d ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d))) ct ad := by
   unfold decodeCramerShoup
   by_cases hvw :
       isElem (d, (decodeBits4 ct).1) = true ∧ isElem (d, (decodeBits4 ct).2.1) = true
   · obtain ⟨v, hv⟩ := (hmem d _).mp hvw.1
     obtain ⟨w, hw⟩ := (hmem d _).mp hvw.2
     simp only [← hv, ← hw, skNatOfZMod, encodeProjHash2_encode, encodeProjHash_encode,
-      ZMod.natCast_zmod_val]
+      csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂, ZMod.natCast_zmod_val]
   · have hfalse : ((encBits4 (decodeBits4 ct) == ct) && isElem (d, (decodeBits4 ct).1) &&
         isElem (d, (decodeBits4 ct).2.1) && isElem (d, (decodeBits4 ct).2.2.1)) = false := by
       revert hvw
@@ -1033,12 +1028,11 @@ theorem cramerShoupPhase1Oracle_eq_skNatOfZMod
     (hasAD : Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.cramerShoupPhase1Oracle hasAD H isElem d sk =
       F.cramerShoupPhase1Oracle hasAD H isElem d
-        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
-          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
-          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) := by
+        (F.skNatOfZMod d ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d))) := by
   funext req s
   simp only [cramerShoupPhase1Oracle, cramerShoupPhase1Reply,
     F.decodeCramerShoup_eq_skNatOfZMod H isElem hmem d sk]
@@ -1048,12 +1042,11 @@ theorem cramerShoupPhase2Oracle_eq_skNatOfZMod
     (hasAD : Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.cramerShoupPhase2Oracle hasAD H isElem d sk ct ad =
       F.cramerShoupPhase2Oracle hasAD H isElem d
-        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
-          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
-          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) ct ad := by
+        (F.skNatOfZMod d ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d))) ct ad := by
   funext req s
   simp only [cramerShoupPhase2Oracle, cramerShoupPhase2Reply,
     F.decodeCramerShoup_eq_skNatOfZMod H isElem hmem d sk]
@@ -1064,12 +1057,11 @@ theorem cramerShoupCollisionPhase2Oracle_eq_skNatOfZMod
     (hasAD : Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.cramerShoupCollisionPhase2Oracle hasAD H isElem d sk ct ad =
       F.cramerShoupCollisionPhase2Oracle hasAD H isElem d
-        (F.skNatOfZMod d (st.1 : ZMod (F.order d)) (st.2 : ZMod (F.order d))
-          (st₁.1 : ZMod (F.order d)) (st₁.2 : ZMod (F.order d))
-          (st₂.1 : ZMod (F.order d)) (st₂.2 : ZMod (F.order d))) ct ad := by
+        (F.skNatOfZMod d ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d))) ct ad := by
   funext req s
   simp only [cramerShoupCollisionPhase2Oracle, finderPhase2Oracle, cramerShoupCollisionPhase2Reply,
     F.decodeCramerShoup_eq_skNatOfZMod H isElem hmem d sk]
@@ -1082,9 +1074,9 @@ theorem encodeCramerShoupEncrypt_publicKey_eq_challenge
     (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (α β σ τ σ₁ τ₁ σ₂ τ₂ : ZMod (F.order d)) (m ad : List Bool) :
     let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂
-    let pkRest := pkVal.2; let h₁₂ := pkRest.2
     F.encodeCramerShoupEncrypt H d
-      (F.encode d pkVal.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2)
+      (F.encode d (csPkU pkVal), F.encode d (csPkH pkVal),
+        F.encode d (csPkH₁ pkVal), F.encode d (csPkH₂ pkVal))
       m ad β.val =
       F.encodeCramerShoupChallenge H d (F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂)
         (F.encode d (β • F.generator d)) (F.encode d ((α * β) • F.generator d)) m ad := by
@@ -1092,6 +1084,7 @@ theorem encodeCramerShoupEncrypt_publicKey_eq_challenge
   have hαβ : (α * β) • F.generator d = β • (α • F.generator d) := by rw [smul_smul, mul_comm]
   rw [hαβ]
   simp only [encodeCramerShoupEncrypt, encodeCramerShoupChallenge, cramerShoupPublicKey,
+    csPkU, csPkH, csPkH₁, csPkH₂, csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂,
     projHash2Aux, skNatOfZMod, F.smul_encode, F.add_encode, ZMod.natCast_zmod_val,
     encodeProjHash_encode, encodeProjHash2_encode, projHash_smul_generator,
     projHash2_smul_generator]
@@ -1185,9 +1178,7 @@ theorem computableInPolyTime_cramerShoupValid
     (hisElem : ComputableInPolyTime isElem (encPair F.encDesc encBits) encBool)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × List Bool =>
-        let r1 := p.2; let r2 := r1.2
-        F.cramerShoupValid isElem d p.1 r1.1 r2.1 r2.2)
+      (fun ⟨n, pk, m₀, m₁⟩ => F.cramerShoupValid isElem d n pk m₀ m₁)
       (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool := by
   let EIn := encPair encUnary (encPair encBits (encPair encBits encBits))
   have hd_in : ComputableTidilyInPolyTime
@@ -1238,9 +1229,7 @@ theorem isPPTOn_cramerShoupADEncryptProb
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     IsPPTOn (encPair encUnary (encPair encBits (encPair encBits encAD))) encBits
-      (fun p =>
-        let r1 := p.2; let r2 := r1.2
-        F.cramerShoupADEncryptProb encAD H d p.1 r1.1 r2.1 r2.2) := by
+      (fun ⟨n, pk, m, ad⟩ => F.cramerShoupADEncryptProb encAD H d n pk m ad) := by
   let E0 := encPair encUnary (encPair encBits (encPair encBits encAD))
   let E1 := encPair E0 encNat
   have hct : ComputableTidilyInPolyTime
@@ -1262,9 +1251,7 @@ theorem isPPTOn_cramerShoupEncryptProb
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits
-      (fun p =>
-        let r1 := p.2
-        F.cramerShoupEncryptProb H d p.1 r1.1 r1.2) := by
+      (fun ⟨n, pk, m⟩ => F.cramerShoupEncryptProb H d n pk m) := by
   let E0 := encPair encUnary (encPair encBits encBits)
   let E1 := encPair E0 encNat
   have hct : ComputableTidilyInPolyTime
@@ -1287,9 +1274,7 @@ theorem computableInPolyTime_cramerShoupADDecryptOpt
     (hisElem : ComputableInPolyTime isElem (encPair F.encDesc encBits) encBool)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × List Bool =>
-        let r1 := p.2; let r2 := r1.2
-        F.cramerShoupADDecryptOpt H isElem d p.1 r1.1 r2.1 r2.2)
+      (fun ⟨n, skBits, ct, ad⟩ => F.cramerShoupADDecryptOpt H isElem d n skBits ct ad)
       (encPair encUnary (encPair encBits (encPair encBits encBits))) (encOption encBits) := by
   exact .of_tidy (F.computableTidilyInPolyTime_decodeCramerShoup hH.tidy hisElem.tidy
     (hd.tidy.comp (by fun_prop))
@@ -1305,9 +1290,7 @@ theorem computableInPolyTime_cramerShoupDecryptOpt
     (hisElem : ComputableInPolyTime isElem (encPair F.encDesc encBits) encBool)
     (hd : ComputableInPolyTime d encUnary F.encDesc) :
     ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool =>
-        let r1 := p.2
-        F.cramerShoupDecryptOpt H isElem d p.1 r1.1 r1.2)
+      (fun ⟨n, skBits, ct⟩ => F.cramerShoupDecryptOpt H isElem d n skBits ct)
       (encPair encUnary (encPair encBits encBits)) (encOption encBits) := by
   exact .of_tidy (F.computableTidilyInPolyTime_decodeCramerShoup hH.tidy hisElem.tidy
     (hd.tidy.comp (by fun_prop))
@@ -1365,11 +1348,10 @@ theorem cca2Phase2Oracle_cramerShoupDecryptOpt
 @[simp]
 theorem decodeBits4_dropFrame_encodeCramerShoupPublicKey
     (d : F.Desc) (u : List Bool) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     decodeBits4 (dropFrame (F.encodeCramerShoupPublicKey d u sk)) =
-      (u, F.encodeProjHashAux d st.1 st.2 u,
-        F.encodeProjHashAux d st₁.1 st₁.2 u,
-        F.encodeProjHashAux d st₂.1 st₂.2 u) := by
+      (u, F.encodeProjHashAux d (csSkS sk) (csSkT sk) u,
+        F.encodeProjHashAux d (csSkS₁ sk) (csSkT₁ sk) u,
+        F.encodeProjHashAux d (csSkS₂ sk) (csSkT₂ sk) u) := by
   simp [encodeCramerShoupPublicKey, encPair_apply, dropFrame_frame_append]
 
 /-- `encodeCramerShoupEncrypt` on the public-key words generated by `skNatOfZMod` agrees with
@@ -1379,18 +1361,17 @@ theorem encodeCramerShoupEncrypt_skNatOfZMod
     (α σ τ σ₁ τ₁ σ₂ τ₂ : ZMod (F.order d)) (m ad : List Bool) (b : ℕ) :
     let u := F.encode d (α • F.generator d)
     let sk := F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂
-    let pkRest := pkVal.2; let h₁₂ := pkRest.2
     F.encodeCramerShoupEncrypt H d
-      (u, F.encodeProjHashAux d st.1 st.2 u,
-        F.encodeProjHashAux d st₁.1 st₁.2 u,
-        F.encodeProjHashAux d st₂.1 st₂.2 u) m ad b =
+      (u, F.encodeProjHashAux d (csSkS sk) (csSkT sk) u,
+        F.encodeProjHashAux d (csSkS₁ sk) (csSkT₁ sk) u,
+        F.encodeProjHashAux d (csSkS₂ sk) (csSkT₂ sk) u) m ad b =
       F.encodeCramerShoupEncrypt H d
-        (F.encode d pkVal.1, F.encode d pkRest.1,
-          F.encode d h₁₂.1, F.encode d h₁₂.2)
+        (F.encode d (csPkU pkVal), F.encode d (csPkH pkVal),
+          F.encode d (csPkH₁ pkVal), F.encode d (csPkH₂ pkVal))
         m ad (b : ZMod (F.order d)).val := by
   simp only [skNatOfZMod, encodeProjHashAux_encode, ZMod.natCast_zmod_val,
+    csPkU, csPkH, csPkH₁, csPkH₂, csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂,
     cramerShoupPublicKey, projHash2Aux, encodeCramerShoupEncrypt, F.smul_encode, F.add_encode]
 
 
diff --git a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean
index d2766f3965..2948ed2627 100644
--- a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean
+++ b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean
@@ -184,7 +184,166 @@ structure ADCCA2AdversaryOf.IsPPT {Msg AD : Type} (encMsg : Msg ↪ List Bool)
     (encPair (encPair (encPair encMsg encMsg) encAD) encBits) adversary.choose
   /-- Phase 2 guessing is uniform strict oracle PPT on `(n, state, ct)`. -/
   guess : IsOraclePPTOn (Operation := Unit) (encPair encUnary (encPair encBits encBits)) encBool
-    (fun p => adversary.guess p.1 p.2.1 p.2.2)
+    (fun ⟨n, state, ct⟩ => adversary.guess n state ct)
+
+/-- Challenge header `((m₀, m₁), ad)` of an `ADCCA2AdversaryOf` choice `(((m₀, m₁), ad), state)`. -/
+abbrev csChoiceHeader {Msg AD : Type} (choice : ((Msg × Msg) × AD) × List Bool) :
+    (Msg × Msg) × AD :=
+  choice.1
+
+/-- Challenge message pair `(m₀, m₁)` of an `ADCCA2AdversaryOf` choice `(((m₀, m₁), ad), state)`. -/
+abbrev csChoiceMsgs {Msg AD : Type} (choice : ((Msg × Msg) × AD) × List Bool) : Msg × Msg :=
+  (csChoiceHeader choice).1
+
+/-- First challenge message `m₀` of an `ADCCA2AdversaryOf` choice `(((m₀, m₁), ad), state)`. -/
+abbrev csChoiceMsg₀ {Msg AD : Type} (choice : ((Msg × Msg) × AD) × List Bool) : Msg :=
+  (csChoiceMsgs choice).1
+
+/-- Second challenge message `m₁` of an `ADCCA2AdversaryOf` choice `(((m₀, m₁), ad), state)`. -/
+abbrev csChoiceMsg₁ {Msg AD : Type} (choice : ((Msg × Msg) × AD) × List Bool) : Msg :=
+  (csChoiceMsgs choice).2
+
+/-- Associated data `ad` of an `ADCCA2AdversaryOf` choice `(((m₀, m₁), ad), state)`. -/
+abbrev csChoiceAD {Msg AD : Type} (choice : ((Msg × Msg) × AD) × List Bool) : AD :=
+  (csChoiceHeader choice).2
+
+/-- Saved state word `state` of an `ADCCA2AdversaryOf` choice `(((m₀, m₁), ad), state)`. -/
+abbrev csChoiceState {Msg AD : Type} (choice : ((Msg × Msg) × AD) × List Bool) : List Bool :=
+  choice.2
+
+/-- Payload hash secret key pair `(s, t)` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkPayload {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α × α :=
+  sk.1
+
+/-- Verification hash secret key pair `((s₁, t₁), (s₂, t₂))` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkVerif {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : (α × α) × (α × α) :=
+  sk.2
+
+/-- First verification hash secret key pair `(s₁, t₁)` of a Cramer–Shoup secret key. -/
+abbrev csSkVerif₁ {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α × α :=
+  (csSkVerif sk).1
+
+/-- Second verification hash secret key pair `(s₂, t₂)` of a Cramer–Shoup secret key. -/
+abbrev csSkVerif₂ {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α × α :=
+  (csSkVerif sk).2
+
+/-- First payload hash secret exponent `s` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkS {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α :=
+  (csSkPayload sk).1
+
+/-- Second payload hash secret exponent `t` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkT {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α :=
+  (csSkPayload sk).2
+
+/-- First verification hash secret exponent `s₁` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkS₁ {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α :=
+  (csSkVerif₁ sk).1
+
+/-- Second verification hash secret exponent `t₁` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkT₁ {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α :=
+  (csSkVerif₁ sk).2
+
+/-- Third verification hash secret exponent `s₂` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkS₂ {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α :=
+  (csSkVerif₂ sk).1
+
+/-- Fourth verification hash secret exponent `t₂` of a Cramer–Shoup secret key
+`((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
+abbrev csSkT₂ {α : Type} (sk : (α × α) × ((α × α) × (α × α))) : α :=
+  (csSkVerif₂ sk).2
+
+/-- Base component `u` of a 4-tuple Cramer–Shoup public key `(u, h, h₁, h₂)`. -/
+abbrev csPkU {α : Type} (pk : α × α × α × α) : α :=
+  pk.1
+
+/-- Hash-key triple `(h, h₁, h₂)` of a 4-tuple Cramer–Shoup public key `(u, h, h₁, h₂)`. -/
+abbrev csPkHashKeys {α : Type} (pk : α × α × α × α) : α × α × α :=
+  pk.2
+
+/-- Verification hash-key pair `(h₁, h₂)` of a 4-tuple Cramer–Shoup public key `(u, h, h₁, h₂)`. -/
+abbrev csPkVerifKeys {α : Type} (pk : α × α × α × α) : α × α :=
+  (csPkHashKeys pk).2
+
+/-- Payload hash key `h` of a 4-tuple Cramer–Shoup public key `(u, h, h₁, h₂)`. -/
+abbrev csPkH {α : Type} (pk : α × α × α × α) : α :=
+  (csPkHashKeys pk).1
+
+/-- First verification hash key `h₁` of a 4-tuple Cramer–Shoup public key `(u, h, h₁, h₂)`. -/
+abbrev csPkH₁ {α : Type} (pk : α × α × α × α) : α :=
+  (csPkVerifKeys pk).1
+
+/-- Second verification hash key `h₂` of a 4-tuple Cramer–Shoup public key `(u, h, h₁, h₂)`. -/
+abbrev csPkH₂ {α : Type} (pk : α × α × α × α) : α :=
+  (csPkVerifKeys pk).2
+
+/-- First ephemeral element `v` of a 4-tuple Cramer–Shoup ciphertext `(v, w, e, z')`. -/
+abbrev csCtV {α : Type} (ct : α × α × α × α) : α :=
+  ct.1
+
+/-- Trailing triple `(w, e, z')` of a 4-tuple Cramer–Shoup ciphertext `(v, w, e, z')`. -/
+abbrev csCtTail {α : Type} (ct : α × α × α × α) : α × α × α :=
+  ct.2
+
+/-- Payload and tag pair `(e, z')` of a 4-tuple Cramer–Shoup ciphertext `(v, w, e, z')`. -/
+abbrev csCtBody {α : Type} (ct : α × α × α × α) : α × α :=
+  (csCtTail ct).2
+
+/-- Second ephemeral element `w` of a 4-tuple Cramer–Shoup ciphertext `(v, w, e, z')`. -/
+abbrev csCtW {α : Type} (ct : α × α × α × α) : α :=
+  (csCtTail ct).1
+
+/-- Masked message element `e` of a 4-tuple Cramer–Shoup ciphertext `(v, w, e, z')`. -/
+abbrev csCtE {α : Type} (ct : α × α × α × α) : α :=
+  (csCtBody ct).1
+
+/-- Tag element `z'` of a 4-tuple Cramer–Shoup ciphertext `(v, w, e, z')`. -/
+abbrev csCtZ {α : Type} (ct : α × α × α × α) : α :=
+  (csCtBody ct).2
+
+/-- First exponent `a` of a sampled triple `(a, b, c) : ℕ × ℕ × ℕ`. -/
+abbrev csExpA (abc : ℕ × ℕ × ℕ) : ℕ :=
+  abc.1
+
+/-- Trailing exponent pair `(b, c)` of a sampled triple `(a, b, c) : ℕ × ℕ × ℕ`. -/
+abbrev csExpBC (abc : ℕ × ℕ × ℕ) : ℕ × ℕ :=
+  abc.2
+
+/-- Second exponent `b` of a sampled triple `(a, b, c) : ℕ × ℕ × ℕ`. -/
+abbrev csExpB (abc : ℕ × ℕ × ℕ) : ℕ :=
+  (csExpBC abc).1
+
+/-- Third exponent `c` of a sampled triple `(a, b, c) : ℕ × ℕ × ℕ`. -/
+abbrev csExpC (abc : ℕ × ℕ × ℕ) : ℕ :=
+  (csExpBC abc).2
+
+/-- Group-element word triple `(u, v, w)` of a 4-tuple DDH input `(d, u, v, w)`. -/
+abbrev csDdhTuple {Desc : Type} (input : Desc × List Bool × List Bool × List Bool) :
+    List Bool × List Bool × List Bool :=
+  input.2
+
+/-- Challenge word pair `(v, w)` of a 4-tuple DDH input `(d, u, v, w)`. -/
+abbrev csDdhChallenge {Desc : Type} (input : Desc × List Bool × List Bool × List Bool) :
+    List Bool × List Bool :=
+  (csDdhTuple input).2
+
+/-- Public-key word `u` of a 4-tuple DDH input `(d, u, v, w)`. -/
+abbrev csDdhU {Desc : Type} (input : Desc × List Bool × List Bool × List Bool) : List Bool :=
+  (csDdhTuple input).1
+
+/-- First challenge word `v` of a 4-tuple DDH input `(d, u, v, w)`. -/
+abbrev csDdhV {Desc : Type} (input : Desc × List Bool × List Bool × List Bool) : List Bool :=
+  (csDdhChallenge input).1
+
+/-- Second challenge word `w` of a 4-tuple DDH input `(d, u, v, w)`. -/
+abbrev csDdhW {Desc : Type} (input : Desc × List Bool × List Bool × List Bool) : List Bool :=
+  (csDdhChallenge input).2
 
 /-- Per-stage decryption-query bound `(Q₁ n, Q₂ n)` for an `ADCCA2AdversaryOf Msg AD`. -/
 def ADCCA2AdversaryOf.IsQueryBounded {Msg AD : Type} (adversary : ADCCA2AdversaryOf Msg AD)
@@ -318,14 +477,13 @@ noncomputable def cca2ADGameOn {Msg AD Out : Type}
       (cca2ADPhase1Oracle encOut decrypt n keys.2))
     (adversary.choose n keys.1)).run ()
   let choice := choiceOut.1
-  let ch := choice.1
-  let msgs := ch.1
-  if valid n keys.1 msgs.1 msgs.2 then
-    let ct ← encrypt n keys.1 (if bit then msgs.2 else msgs.1) ch.2
+  if valid n keys.1 (csChoiceMsg₀ choice) (csChoiceMsg₁ choice) then
+    let ct ← encrypt n keys.1 (if bit then csChoiceMsg₁ choice else csChoiceMsg₀ choice)
+      (csChoiceAD choice)
     let guessOut ← (OracleComp.interpret
       (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m))
-        (cca2ADPhase2Oracle encOut decrypt n keys.2 ct (encAD ch.2)))
-      (adversary.guess n choice.2 ct)).run ()
+        (cca2ADPhase2Oracle encOut decrypt n keys.2 ct (encAD (csChoiceAD choice))))
+      (adversary.guess n (csChoiceState choice) ct)).run ()
     return guessOut.1
   else
     return false
@@ -427,9 +585,7 @@ theorem decodeBits4_encBits4 (p : List Bool × List Bool × List Bool × List Bo
 associated-data bit string `ad`. -/
 def extractCramerShoupTuple (ct ad : List Bool) : List Bool :=
   let parts := decodeBits4 ct
-  let rest := parts.2
-  let ez := rest.2
-  encBits4 (parts.1, rest.1, ez.1, ad)
+  encBits4 (csCtV parts, csCtW parts, csCtE parts, ad)
 
 @[simp]
 theorem extractCramerShoupTuple_encBits4 (v w e z' ad : List Bool) :
@@ -517,10 +673,9 @@ def cramerShoupEncrypt (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (pk : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d)
     (m : F.Carrier d) (ad : List Bool) (β : ZMod (F.order d)) :
     F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d :=
-  let pkRest := pk.2; let h₁₂ := pkRest.2
-  let v := β • F.generator d; let w := β • pk.1; let e := β • pkRest.1 + m
+  let v := β • F.generator d; let w := β • csPkU pk; let e := β • csPkH pk + m
   let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d v w e ad)
-  (v, w, e, β • (h₁₂.1 + ρ • h₁₂.2))
+  (v, w, e, β • (csPkH₁ pk + ρ • csPkH₂ pk))
 
 /-- Under a genuine public key `cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂`, the components of
 `cramerShoupEncrypt` coincide with projective hash evaluation (`Game 0 = Game 1`,
@@ -555,11 +710,10 @@ def cramerShoupDecrypt [∀ d, DecidableEq (F.Carrier d)]
       ((ZMod (F.order d) × ZMod (F.order d)) × (ZMod (F.order d) × ZMod (F.order d))))
     (ct : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) (ad : List Bool) :
     Option (F.Carrier d) :=
-  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
-  let ctRest := ct.2; let ez := ctRest.2
-  let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d ct.1 ctRest.1 ez.1 ad)
-  if projHash2 F d st₁.1 st₁.2 st₂.1 st₂.2 ρ ct.1 ctRest.1 = ez.2 then
-    some (ez.1 - projHash F d st.1 st.2 ct.1 ctRest.1)
+  let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d (csCtV ct) (csCtW ct) (csCtE ct) ad)
+  if projHash2 F d (csSkS₁ sk) (csSkT₁ sk) (csSkS₂ sk) (csSkT₂ sk) ρ (csCtV ct) (csCtW ct) =
+      csCtZ ct then
+    some (csCtE ct - projHash F d (csSkS sk) (csSkT sk) (csCtV ct) (csCtW ct))
   else
     none
 
@@ -574,7 +728,9 @@ theorem cramerShoupDecrypt_cramerShoupEncrypt [∀ d, DecidableEq (F.Carrier d)]
     F.cramerShoupDecrypt H d ((σ, τ), ((σ₁, τ₁), (σ₂, τ₂)))
       (F.cramerShoupEncrypt H d (F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂) m ad β) ad =
       some m := by
-  rw [F.cramerShoupEncrypt_cramerShoupPublicKey]; simp [cramerShoupDecrypt]
+  rw [F.cramerShoupEncrypt_cramerShoupPublicKey]
+  simp [cramerShoupDecrypt, csCtV, csCtW, csCtE, csCtZ,
+    csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂]
 
 /-! ### Word-level polynomial-time Cramer–Shoup operations -/
 
@@ -631,53 +787,55 @@ theorem encodeProjHash2_encode (d : F.Desc) (s₁ t₁ s₂ t₂ r : ℕ) (v w :
 key word presented to a 1CCA adversary. -/
 def encodeCramerShoupPublicKeyValues (d : F.Desc)
     (pk : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) : List Bool :=
-  let pkRest := pk.2; let h₁₂ := pkRest.2
   encPair F.encDesc encBits4
-    (d, (F.encode d pk.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2))
+    (d, (F.encode d (csPkU pk), F.encode d (csPkH pk),
+      F.encode d (csPkH₁ pk), F.encode d (csPkH₂ pk)))
 
 /-- Word-level Cramer–Shoup public key generation from `d : F.Desc`, an encoded
 `u = encode (α • g)`, and natural-number secret exponents
 `sk = ((s, t), ((s₁, t₁), (s₂, t₂)))`. -/
 def encodeCramerShoupPublicKey (d : F.Desc) (u : List Bool)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) : List Bool :=
-  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
-  encPair F.encDesc encBits4 (d, (u, F.encodeProjHashAux d st.1 st.2 u,
-    F.encodeProjHashAux d st₁.1 st₁.2 u, F.encodeProjHashAux d st₂.1 st₂.2 u))
+  encPair F.encDesc encBits4 (d, (u, F.encodeProjHashAux d (csSkS sk) (csSkT sk) u,
+    F.encodeProjHashAux d (csSkS₁ sk) (csSkT₁ sk) u,
+    F.encodeProjHashAux d (csSkS₂ sk) (csSkT₂ sk) u))
 
 @[simp]
 theorem encodeCramerShoupPublicKey_encode (d : F.Desc) (α : ZMod (F.order d))
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) sk =
       F.encodeCramerShoupPublicKeyValues d
-        (F.cramerShoupPublicKey d α st.1 st.2 st₁.1 st₁.2 st₂.1 st₂.2) := by
+        (F.cramerShoupPublicKey d α
+          ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+          ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+          ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d))) := by
   simp only [encodeCramerShoupPublicKey, encodeCramerShoupPublicKeyValues,
-    encodeProjHashAux_encode, cramerShoupPublicKey, projHash2Aux]
+    encodeProjHashAux_encode, cramerShoupPublicKey, projHash2Aux,
+    csPkU, csPkH, csPkH₁, csPkH₂, csPkHashKeys, csPkVerifKeys]
 
 /-- Encode a 4-tuple ciphertext `(v, w, e, z') : (F.Carrier d)⁴` as a canonically framed bit
 string. -/
 def encodeCramerShoupCiphertext (d : F.Desc)
     (ct : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) : List Bool :=
-  let ctRest := ct.2; let ez := ctRest.2
-  encBits4 (F.encode d ct.1, F.encode d ctRest.1, F.encode d ez.1, F.encode d ez.2)
+  encBits4 (F.encode d (csCtV ct), F.encode d (csCtW ct),
+    F.encode d (csCtE ct), F.encode d (csCtZ ct))
 
 /-- Word-level Cramer–Shoup encryption from the public key `(u, h, h₁, h₂)`, encoded message `m`,
 encoded associated data `ad`, and randomness `b : ℕ`. -/
 def encodeCramerShoupEncrypt (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (pk : List Bool × List Bool × List Bool × List Bool) (m ad : List Bool) (b : ℕ) : List Bool :=
-  let pkRest := pk.2; let h₁₂ := pkRest.2
-  let v := F.smul (d, b, F.encode d (F.generator d)); let w := F.smul (d, b, pk.1)
-  let e := F.add (d, F.smul (d, b, pkRest.1), m)
+  let v := F.smul (d, b, F.encode d (F.generator d)); let w := F.smul (d, b, csPkU pk)
+  let e := F.add (d, F.smul (d, b, csPkH pk), m)
   let r := ofBits (H (d, encBits4 (v, w, e, ad)))
-  encBits4 (v, w, e, F.smul (d, b, F.add (d, h₁₂.1, F.smul (d, r, h₁₂.2))))
+  encBits4 (v, w, e, F.smul (d, b, F.add (d, csPkH₁ pk, F.smul (d, r, csPkH₂ pk))))
 
 @[simp]
 theorem encodeCramerShoupEncrypt_encode (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (pk : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d)
     (m : F.Carrier d) (ad : List Bool) (b : ℕ) :
-    let pkRest := pk.2; let h₁₂ := pkRest.2
     F.encodeCramerShoupEncrypt H d
-      (F.encode d pk.1, F.encode d pkRest.1, F.encode d h₁₂.1, F.encode d h₁₂.2)
+      (F.encode d (csPkU pk), F.encode d (csPkH pk),
+        F.encode d (csPkH₁ pk), F.encode d (csPkH₂ pk))
       (F.encode d m) ad b =
       F.encodeCramerShoupCiphertext d
         (F.cramerShoupEncrypt H d pk m ad (b : ZMod (F.order d))) := by
@@ -689,23 +847,25 @@ theorem encodeCramerShoupEncrypt_encode (H : F.Desc × List Bool → List Bool)
 Game 1, printed p. 490, and Exercise 12.27, printed pp. 521–522). -/
 def encodeCramerShoupChallenge (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (v w m ad : List Bool) : List Bool :=
-  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
-  let e := F.add (d, F.encodeProjHash d st.1 st.2 v w, m)
+  let e := F.add (d, F.encodeProjHash d (csSkS sk) (csSkT sk) v w, m)
   let r := ofBits (H (d, encBits4 (v, w, e, ad)))
-  encBits4 (v, w, e, F.encodeProjHash2 d st₁.1 st₁.2 st₂.1 st₂.2 r v w)
+  encBits4 (v, w, e,
+    F.encodeProjHash2 d (csSkS₁ sk) (csSkT₁ sk) (csSkS₂ sk) (csSkT₂ sk) r v w)
 
 @[simp]
 theorem encodeCramerShoupChallenge_encode (H : F.Desc × List Bool → List Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (v w m : F.Carrier d) (ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.encodeCramerShoupChallenge H d sk (F.encode d v) (F.encode d w) (F.encode d m) ad =
-      let e := projHash F d st.1 st.2 v w + m
+      let e := projHash F d
+        ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d)) v w + m
       let ρ := F.cramerShoupHashMod H d (F.encodeCramerShoupTuple d v w e ad)
-      let z' := projHash2 F d st₁.1 st₁.2 st₂.1 st₂.2 ρ v w
+      let z' := projHash2 F d
+        ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+        ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d)) ρ v w
       F.encodeCramerShoupCiphertext d (v, w, e, z') := by
   simp only [encodeCramerShoupChallenge, encodeProjHash_encode, F.add_encode,
     encodeProjHash2_encode, encodeCramerShoupTuple, cramerShoupHashMod,
-    encodeCramerShoupCiphertext]
+    encodeCramerShoupCiphertext, csCtV, csCtW, csCtE, csCtZ]
 
 /-- Word-level Cramer–Shoup decryption ([BonehShoup2023], Section 12.5.3, Remark 12.3, and
 Exercise 12.27, printed pp. 489, 493, 522): given `(d, sk, ct, ad)`, unpack `(v, w, e, z') :=
@@ -716,13 +876,12 @@ all pass, return `some (encode (e - f_{s,t}(v, w)))`, else `none`. -/
 def decodeCramerShoup (H : F.Desc × List Bool → List Bool)
     (isElem : F.Desc × List Bool → Bool) (d : F.Desc)
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct ad : List Bool) : Option (List Bool) :=
-  let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
-  let parts := decodeBits4 ct; let rest := parts.2; let ez := rest.2
-  let v := parts.1; let w := rest.1; let e := ez.1; let z' := ez.2
+  let parts := decodeBits4 ct
+  let v := csCtV parts; let w := csCtW parts; let e := csCtE parts; let z' := csCtZ parts
   let r := ofBits (H (d, encBits4 (v, w, e, ad)))
   if (encBits4 parts == ct) && isElem (d, v) && isElem (d, w) && isElem (d, e) &&
-      (F.encodeProjHash2 d st₁.1 st₁.2 st₂.1 st₂.2 r v w == z') then
-    some (F.add (d, e, F.encodeGroupNeg d (F.encodeProjHash d st.1 st.2 v w)))
+      (F.encodeProjHash2 d (csSkS₁ sk) (csSkT₁ sk) (csSkS₂ sk) (csSkT₂ sk) r v w == z') then
+    some (F.add (d, e, F.encodeGroupNeg d (F.encodeProjHash d (csSkS sk) (csSkT sk) v w)))
   else
     none
 
@@ -733,13 +892,12 @@ theorem decodeCramerShoup_encode [∀ d, DecidableEq (F.Carrier d)]
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ)))
     (ct : F.Carrier d × F.Carrier d × F.Carrier d × F.Carrier d) (ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.decodeCramerShoup H isElem d sk (F.encodeCramerShoupCiphertext d ct) ad =
       (F.cramerShoupDecrypt H d
-        (((st.1 : ZMod (F.order d)), (st.2 : ZMod (F.order d))),
-          (((st₁.1 : ZMod (F.order d)), (st₁.2 : ZMod (F.order d))),
-            ((st₂.1 : ZMod (F.order d)), (st₂.2 : ZMod (F.order d))))) ct ad).map
-        (F.encode d) := by
+        ((((csSkS sk : ℕ) : ZMod (F.order d)), ((csSkT sk : ℕ) : ZMod (F.order d))),
+          ((((csSkS₁ sk : ℕ) : ZMod (F.order d)), ((csSkT₁ sk : ℕ) : ZMod (F.order d))),
+            (((csSkS₂ sk : ℕ) : ZMod (F.order d)), ((csSkT₂ sk : ℕ) : ZMod (F.order d)))))
+        ct ad).map (F.encode d) := by
   rcases ct with ⟨v, w, e, z'⟩
   have hv : isElem (d, F.encode d v) = true := (hmem d _).mpr ⟨v, rfl⟩
   have hw : isElem (d, F.encode d w) = true := (hmem d _).mpr ⟨w, rfl⟩
@@ -747,6 +905,8 @@ theorem decodeCramerShoup_encode [∀ d, DecidableEq (F.Carrier d)]
   have hinj : ∀ a b : F.Carrier d, (F.encode d a == F.encode d b) = decide (a = b) := fun a b => by
     rw [Bool.eq_iff_iff, beq_iff_eq, decide_eq_true_eq]; exact (F.encode_injective d).eq_iff
   simp only [decodeCramerShoup, encodeCramerShoupCiphertext, decodeBits4_encBits4, beq_self_eq_true,
+    csCtV, csCtW, csCtE, csCtZ, csCtTail, csCtBody,
+    csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂, csSkPayload, csSkVerif, csSkVerif₁, csSkVerif₂,
     hv, hw, he, Bool.true_and, encodeProjHash2_encode, hinj, encodeProjHash_encode,
     encodeGroupNeg_encode, F.add_encode, cramerShoupDecrypt, encodeCramerShoupTuple,
     cramerShoupHashMod, sub_eq_add_neg, decide_eq_true_eq]
@@ -760,14 +920,15 @@ theorem decodeCramerShoup_cramerShoupEncrypt
     (hmem : ∀ d x, isElem (d, x) = true ↔ x ∈ Set.range (F.encode d))
     (d : F.Desc) (α β : ZMod (F.order d))
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (m : F.Carrier d) (ad : List Bool) :
-    let st := sk.1; let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
     F.decodeCramerShoup H isElem d sk
       (F.encodeCramerShoupCiphertext d
         (F.cramerShoupEncrypt H d
-          (F.cramerShoupPublicKey d α st.1 st.2 st₁.1 st₁.2 st₂.1 st₂.2)
+          (F.cramerShoupPublicKey d α
+            ((csSkS sk : ℕ) : ZMod (F.order d)) ((csSkT sk : ℕ) : ZMod (F.order d))
+            ((csSkS₁ sk : ℕ) : ZMod (F.order d)) ((csSkT₁ sk : ℕ) : ZMod (F.order d))
+            ((csSkS₂ sk : ℕ) : ZMod (F.order d)) ((csSkT₂ sk : ℕ) : ZMod (F.order d)))
           m ad β)) ad = some (F.encode d m) := by
   classical
-  dsimp only
   rw [F.decodeCramerShoup_encode H isElem hmem, F.cramerShoupDecrypt_cramerShoupEncrypt]; rfl
 
 /-! ### Polynomial-time certificates for word-level operations -/
@@ -847,9 +1008,7 @@ private theorem computableTidilyInPolyTime_encodeCramerShoupPublicKey
 /-- Word-level Cramer–Shoup public key generation is computable in polynomial time. -/
 theorem computableInPolyTime_encodeCramerShoupPublicKey :
     ComputableInPolyTime
-      (fun p : F.Desc × List Bool × ((ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) =>
-        let rest := p.2
-        F.encodeCramerShoupPublicKey p.1 rest.1 rest.2)
+      (fun ⟨d, u, sk⟩ => F.encodeCramerShoupPublicKey d u sk)
       (encPair F.encDesc (encPair encBits encCramerShoupSK)) encBits :=
   .of_tidy (F.computableTidilyInPolyTime_encodeCramerShoupPublicKey
     (by fun_prop) (by fun_prop) (by fun_prop))
@@ -883,10 +1042,7 @@ theorem computableInPolyTime_encodeCramerShoupChallenge
     {H : F.Desc × List Bool → List Bool}
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) :
     ComputableInPolyTime
-      (fun p : F.Desc × ((ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) ×
-          List Bool × List Bool × List Bool × List Bool =>
-        let r1 := p.2; let r2 := r1.2; let r3 := r2.2; let r4 := r3.2
-        F.encodeCramerShoupChallenge H p.1 r1.1 r2.1 r3.1 r4.1 r4.2)
+      (fun ⟨d, sk, v, w, m, ad⟩ => F.encodeCramerShoupChallenge H d sk v w m ad)
       (encPair F.encDesc (encPair encCramerShoupSK
         (encPair encBits (encPair encBits (encPair encBits encBits)))))
       encBits :=
@@ -924,10 +1080,7 @@ theorem computableInPolyTime_encodeCramerShoupEncrypt
     {H : F.Desc × List Bool → List Bool}
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) :
     ComputableInPolyTime
-      (fun p : F.Desc × (List Bool × List Bool × List Bool × List Bool) ×
-          List Bool × List Bool × ℕ =>
-        let r1 := p.2; let r2 := r1.2; let r3 := r2.2
-        F.encodeCramerShoupEncrypt H p.1 r1.1 r2.1 r3.1 r3.2)
+      (fun ⟨d, pk, m, ad, b⟩ => F.encodeCramerShoupEncrypt H d pk m ad b)
       (encPair F.encDesc (encPair encBits4 (encPair encBits (encPair encBits encNat)))) encBits :=
   .of_tidy (F.computableTidilyInPolyTime_encodeCramerShoupEncrypt hH.tidy
     (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop))
@@ -976,9 +1129,7 @@ theorem computableInPolyTime_decodeCramerShoup
     (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits)
     (hisElem : ComputableInPolyTime isElem (encPair F.encDesc encBits) encBool) :
     ComputableInPolyTime
-      (fun p : F.Desc × ((ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) × List Bool × List Bool =>
-        let r1 := p.2; let r2 := r1.2
-        F.decodeCramerShoup H isElem p.1 r1.1 r2.1 r2.2)
+      (fun ⟨d, sk, ct, ad⟩ => F.decodeCramerShoup H isElem d sk ct ad)
       (encPair F.encDesc (encPair encCramerShoupSK (encPair encBits encBits)))
       (encOption encBits) :=
   .of_tidy (F.computableTidilyInPolyTime_decodeCramerShoup hH.tidy hisElem.tidy
@@ -1080,9 +1231,8 @@ noncomputable def cramerShoupGame3
   let pk := F.encodeCramerShoupPublicKey d u sk
   runStatelessOracle (F.cramerShoupPhase1Reply hasAD H isElem d sk)
     (adversary.choose n pk) fun choice =>
-    let ch := choice.1; let msgs := ch.1
-    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
-    let ad := encodeAD (d, ch.2)
+    let m₀ := encodeMsg (d, csChoiceMsg₀ choice); let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+    let ad := encodeAD (d, csChoiceAD choice)
     if isElem (d, m₀) && isElem (d, m₁) then
       let m := if bit then m₁ else m₀
       let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1102,8 +1252,7 @@ def decodeCramerShoupDH
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (d : F.Desc) (α δ δ₁ δ₂ : ZMod (F.order d)) (ct ad : List Bool) : Option (List Bool) :=
   let parts := decodeBits4 ct
-  let rest := parts.2
-  if rest.1 == F.smul (d, α.val, parts.1) then
+  if csCtW parts == F.smul (d, α.val, csCtV parts) then
     F.decodeCramerShoup H isElem d (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0) ct ad
   else
     none
@@ -1134,13 +1283,12 @@ def isCramerShoupBadDH
     (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool)
     (d : F.Desc) (α : ZMod (F.order d))
     (sk : (ℕ × ℕ) × ((ℕ × ℕ) × (ℕ × ℕ))) (ct_q ad_q : List Bool) : Bool :=
-  let sk₂ := sk.2; let st₁ := sk₂.1; let st₂ := sk₂.2
-  let parts := decodeBits4 ct_q; let rest := parts.2; let ez := rest.2
-  let v := parts.1; let w := rest.1; let e := ez.1; let z' := ez.2
+  let parts := decodeBits4 ct_q
+  let v := csCtV parts; let w := csCtW parts; let e := csCtE parts; let z' := csCtZ parts
   let r := ofBits (H (d, encBits4 (v, w, e, ad_q)))
   (encBits4 parts == ct_q) && isElem (d, v) && isElem (d, w) && isElem (d, e) &&
     (w != F.smul (d, α.val, v)) &&
-    (F.encodeProjHash2 d st₁.1 st₁.2 st₂.1 st₂.2 r v w == z')
+    (F.encodeProjHash2 d (csSkS₁ sk) (csSkT₁ sk) (csSkS₂ sk) (csSkT₂ sk) r v w == z')
 
 private theorem encodeCramerShoupPublicKey_fiber_eq (d : F.Desc)
     (α δ τ δ₁ τ₁ δ₂ τ₂ : ZMod (F.order d)) :
@@ -1149,6 +1297,7 @@ private theorem encodeCramerShoupPublicKey_fiber_eq (d : F.Desc)
     F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d))
       (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0) := by
   simp only [encodeCramerShoupPublicKey_encode, cramerShoupPublicKey, skNatOfZMod,
+    csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂,
     ZMod.natCast_zmod_val, projHash2Aux, projHashAux_generator_smul, sub_add_cancel,
     mul_zero, add_zero]
 
@@ -1163,6 +1312,7 @@ private theorem encodeCramerShoupChallenge_fiber_eq
         (δ₂ - α * τ₂) τ₂) v w m ad =
       encBits4 (v, w, e, F.encode d ((β * (δ₁ + ρ * δ₂) + (γ - α * β) * ξ) • F.generator d)) := by
   simp only [encodeCramerShoupChallenge, skNatOfZMod, encodeProjHash2_encode,
+    csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂, csSkPayload, csSkVerif, csSkVerif₁, csSkVerif₂,
     ZMod.natCast_zmod_val, cramerShoupHashMod, projHash2_fiber_challenge_eq]
 
 private theorem decodeCramerShoup_fiber_eq_decodeCramerShoupDH_of_not_bad
@@ -1465,15 +1615,14 @@ def HonestPhase2QueryBound (hasAD : Bool) {Msg AD : Type}
         (F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d))
           (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)))).run ())).support,
     ∀ mElem : F.Carrier d,
-      let choice := choiceOut.1; let ch := choice.1
       let v := F.encode d (β • F.generator d); let w := F.encode d (γ • F.generator d)
       let e := F.encode d (projHash F d (δ - α * τ) τ (β • F.generator d) (γ • F.generator d) +
         mElem)
-      let ad := encodeAD (d, ch.2)
+      let ad := encodeAD (d, csChoiceAD choiceOut.1)
       let ρ := F.cramerShoupHashMod H d (encBits4 (v, w, e, ad))
       let ct := encBits4 (v, w, e,
         F.encode d ((β * (δ₁ + ρ * δ₂) + (γ - α * β) * ξ) • F.generator d))
-      (adversary.guess n choice.2 ct).IsQueryBounded Q₂
+      (adversary.guess n (csChoiceState choiceOut.1) ct).IsQueryBounded Q₂
 
 /-- **Game 3.5** (intermediate hybrid between Game 3 and Game 4 of [BonehShoup2023],
 Section 12.5.3, printed pp. 491–492): under the fiber change of variables
@@ -1494,9 +1643,8 @@ noncomputable def cramerShoupGame3Half
   let pk := F.encodeCramerShoupPublicKey d u (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)
   runStatelessOracle (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂)
     (adversary.choose n pk) fun choice =>
-    let ch := choice.1; let msgs := ch.1
-    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
-    let ad := encodeAD (d, ch.2)
+    let m₀ := encodeMsg (d, csChoiceMsg₀ choice); let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+    let ad := encodeAD (d, csChoiceAD choice)
     if isElem (d, m₀) && isElem (d, m₁) then
       let m := if bit then m₁ else m₀
       let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1571,9 +1719,8 @@ noncomputable def cramerShoupGame4
   let pk := F.encodeCramerShoupPublicKey d u (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)
   runStatelessOracle (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂)
     (adversary.choose n pk) fun choice =>
-    let ch := choice.1; let msgs := ch.1
-    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
-    let ad := encodeAD (d, ch.2)
+    let m₀ := encodeMsg (d, csChoiceMsg₀ choice); let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+    let ad := encodeAD (d, csChoiceAD choice)
     if isElem (d, m₀) && isElem (d, m₁) then
       let m := if bit then m₁ else m₀
       let ct := F.encodeCramerShoupChallenge H d sk v w m ad
@@ -1725,9 +1872,8 @@ noncomputable def cramerShoupGame5
   let pk := F.encodeCramerShoupPublicKey d u (F.skNatOfZMod d δ 0 δ₁ 0 δ₂ 0)
   runStatelessOracle (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂)
     (adversary.choose n pk) fun choice =>
-    let ch := choice.1; let msgs := ch.1
-    let m₀ := encodeMsg (d, msgs.1); let m₁ := encodeMsg (d, msgs.2)
-    let ad := encodeAD (d, ch.2)
+    let m₀ := encodeMsg (d, csChoiceMsg₀ choice); let m₁ := encodeMsg (d, csChoiceMsg₁ choice)
+    let ad := encodeAD (d, csChoiceAD choice)
     if isElem (d, m₀) && isElem (d, m₁) then
       let e := F.encode d (ζ • F.generator d)
       let r := ofBits (H (d, encBits4 (v, w, e, ad)))
@@ -1811,6 +1957,8 @@ theorem advantage_cramerShoupGame4_game5_le
           k (projHash F d (δ - α * τ) τ (β • F.generator d) (γ • F.generator d) + mElem) := by
       funext τ
       simp only [encodeCramerShoupChallenge, skNatOfZMod, v, w, ad, ← hmElem, encodeProjHash_encode,
+        csSkS, csSkT, csSkS₁, csSkT₁, csSkS₂, csSkT₂,
+        csSkPayload, csSkVerif, csSkVerif₁, csSkVerif₂,
         F.add_encode, ZMod.natCast_zmod_val, k]
     rw [h4]; exact uniform_projHash_fiber_add F d hγ δ mElem k
   · simp only [hvalid, Bool.false_eq_true, ↓reduceIte]
diff --git a/ComplexityTests/Crypto/CramerShoup.lean b/ComplexityTests/Crypto/CramerShoup.lean
index 301da83c9a..027ace3b94 100644
--- a/ComplexityTests/Crypto/CramerShoup.lean
+++ b/ComplexityTests/Crypto/CramerShoup.lean
@@ -69,6 +69,7 @@ example [∀ d, DecidableEq (schnorrGroups.Carrier d)] :
     schnorrGroups.cramerShoupDecrypt testHash d23 sk badCt [] = none := by
   simp [PrimeOrderGroupFamily.cramerShoupDecrypt, PrimeOrderGroupFamily.cramerShoupEncrypt,
     PrimeOrderGroupFamily.cramerShoupPublicKey, ProjectiveHash.projHash2Aux,
+    csPkU, csPkH, csPkH₁, csPkH₂, csSkS₁, csSkT₁, csSkS₂, csSkT₂, csCtV, csCtW, csCtE, csCtZ,
     ProjectiveHash.projHash2_smul_generator, schnorrGroups.generator_ne_zero d23]
 
 /-- Framing roundtrips for `encBits3`, `encBits4`, `extractCramerShoupTuple`, and