refactor(Crypto): replace projection chains across Signature, Commitment, and Hash modules (#1764)

Complexity/Crypto/Computational/CollisionResistant.lean

@@ -493,7 +493,7 @@ theorem CollisionResistantOn.of_extract
     (hCR : CollisionResistantOn H₂ valid₂)
     (extract : ℕ → List Bool → List Bool → List Bool → List Bool × List Bool)
     (hextract : ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × List Bool => extract p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (fun ((n, k, m₁, m₂) : ℕ × List Bool × List Bool × List Bool) => extract n k m₁ m₂)
       (encPair encUnary (encPair encBits (encPair encBits encBits)))
       (encPair encBits encBits))
     (himp : ∀ᶠ n in Filter.atTop, ∀ k, k.length = n → ∀ m₁ m₂,

Complexity/Crypto/Computational/Commitment/Basic.lean

@@ -108,9 +108,10 @@ noncomputable def CommitmentScheme.hidingForKey {Key : Type}
     (S : CommitmentScheme Key) (k : Key)
     (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : Game := do
   let choice ← ProbComp.eval (adversary.choose n (S.encodeKey k))
+  let msgs := choice.1
   let msg := open Classical in
-    if bit ∧ S.ValidMessage k choice.1.1 ∧ S.ValidMessage k choice.1.2 then choice.1.2
-    else choice.1.1
+    if bit ∧ S.ValidMessage k msgs.1 ∧ S.ValidMessage k msgs.2 then msgs.2
+    else msgs.1
   let co ← S.commitDist k msg
   ProbComp.eval (adversary.guess n choice.2 co.1)
 
@@ -185,9 +186,12 @@ theorem CommitmentScheme.StatisticalHiding.computationalHiding {Key : Type}
 openings `(m₀, o₀)` and `(m₁, o₁)` are accepted by `S.verify k` for the commitment string `c`. -/
 def CommitmentScheme.isBindingCollision {Key : Type} (S : CommitmentScheme Key) (k : Key)
     (out : List Bool × (List Bool × List Bool) × (List Bool × List Bool)) : Bool :=
-  decide (out.2.1.1 ≠ out.2.2.1) &&
-    S.verify k out.2.1.1 out.1 out.2.1.2 &&
-    S.verify k out.2.2.1 out.1 out.2.2.2
+  let openings := out.2
+  let open₀ := openings.1
+  let open₁ := openings.2
+  decide (open₀.1 ≠ open₁.1) &&
+    S.verify k open₀.1 out.1 open₀.2 &&
+    S.verify k open₁.1 out.1 open₁.2
 
 /-- The commitment binding experiment ([BonehShoup2023], Section 8.12, p. 344, and
 Definition 8.8): draw `k ← keyDist n`, give `S.encodeKey k` to `adversary`, and accept when the

Complexity/Crypto/Computational/Commitment/PublicOperations.lean

@@ -57,11 +57,11 @@ structure PublicOperations {Key : Type} (S : CommitmentScheme Key) where
   map_commit : ∀ k m, (randomness k).map (commit k m) = S.commitDist k m
   /-- Deterministic evaluation is polynomial-time in the public key, message and randomness word. -/
   commit_polyTime : ComputableInPolyTime
-    (fun p : Key × List Bool × List Bool => commit p.1 p.2.1 p.2.2)
+    (fun ((k, msg, r) : Key × List Bool × List Bool) => commit k msg r)
     (encPair S.encodeKey (encPair encBits encBits)) (encPair encBits encBits)
   /-- Verification is polynomial-time in the public key, message, commitment and opening words. -/
   verify_polyTime : ComputableInPolyTime
-    (fun p : Key × List Bool × List Bool × List Bool => S.verify p.1 p.2.1 p.2.2.1 p.2.2.2)
+    (fun ((k, msg, c, o) : Key × List Bool × List Bool × List Bool) => S.verify k msg c o)
     (encPair S.encodeKey (encPair encBits (encPair encBits encBits))) encBool
 
 namespace PublicOperations

Complexity/Crypto/Computational/IndexedSignature.lean

@@ -142,8 +142,8 @@ def indexedEufCmaGame (S : IndexedSignatureScheme) (adversary : IndexedForger) (
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.indexedSigningOracle n keys.2)) (adversary n keys.1)).run []
-  return !out.2.contains (out.1.1, out.1.2.1) &&
-    S.verify keys.1 out.1.1 out.1.2.1 out.1.2.2
+  let (u, msg, sig) := out.1
+  return !out.2.contains (u, msg) && S.verify keys.1 u msg sig
 
 /-- Running an oracle-PPT indexed forger against `indexedSigningOracle` is uniformly strict PPT in
 the unary security parameter, the public key and the secret key. -/

Complexity/Crypto/Computational/IndexedSignature/Counter.lean

@@ -111,7 +111,9 @@ def counterEufCmaGame (adversary : Forger) (n : ℕ) : ProbComp Bool := do
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.counterSigningOracle n keys.2)) (adversary n keys.1)).run (0, [])
-  return !out.2.2.contains out.1.1 && S.counterVerify keys.1 out.1.1 out.1.2
+  let msig := out.1
+  let state := out.2
+  return !state.2.contains msig.1 && S.counterVerify keys.1 msig.1 msig.2
 
 variable {S}
 
@@ -280,7 +282,8 @@ def counterForger (bound : ℕ → ℕ → ℕ) (adversary : Forger) : IndexedFo
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k)))
       (S.counterHandler n bound)) (adversary n pk)).run 0
-  return ((requestDecoder.decode out.1.2).1, out.1.1, (requestDecoder.decode out.1.2).2)
+  let msig := out.1
+  return ((requestDecoder.decode msig.2).1, msig.1, (requestDecoder.decode msig.2).2)
 
 /-! ### Exact simulation -/
 

Complexity/Crypto/Computational/IndexedSignature/Seeded.lean

@@ -112,9 +112,12 @@ theorem exists_signWith (S : IndexedSignatureScheme) :
       ComputableInPolyTime (fun p : (List Bool × ℕ × List Bool) × List Bool => signWith p.1 p.2)
         (encPair (encPair encBits (encPair encUnary encBits)) encBits) encBits ∧
       ComputableInPolyTime budget (encPair encBits (encPair encUnary encBits)) encUnary ∧
-      (∀ a coins, signWith a coins ∈ (ProbComp.eval (S.sign a.1 a.2.1 a.2.2)).support) ∧
+      (∀ a coins,
+        let (sk, u, msg) := a
+        signWith a coins ∈ (ProbComp.eval (S.sign sk u msg)).support) ∧
       ∀ a length, budget a ≤ length →
-        ProbComp.eval (S.sign a.1 a.2.1 a.2.2) =
+        let (sk, u, msg) := a
+        ProbComp.eval (S.sign sk u msg) =
           (BitString.uniformList length).map (signWith a) := by
   obtain ⟨c, d, evaluate, hpoly, hsupport, hlaw⟩ :=
     IsPPTOn.exists_total_seeded_evaluator S.sign_ppt
@@ -124,21 +127,27 @@ theorem exists_signWith (S : IndexedSignatureScheme) :
 /-- The seeded algorithms of any indexed scheme, read off its strict-PPT certificates. -/
 noncomputable def seeded (S : IndexedSignatureScheme) : S.Seeded :=
   let hk := S.exists_keyGenWith
+  let hk_spec := hk.choose_spec.choose_spec
+  let hk_rest := hk_spec.2
+  let hk_laws := hk_rest.2
   let hs := S.exists_signWith
+  let hs_spec := hs.choose_spec.choose_spec
+  let hs_rest := hs_spec.2
+  let hs_laws := hs_rest.2
   { keyGenWith := hk.choose
     keyGenBudget := hk.choose_spec.choose
     signWith := fun sk u msg coins => hs.choose (sk, u, msg) coins
     signBudget := fun sk u msg => hs.choose_spec.choose (sk, u, msg)
-    keyGenWith_polyTime := hk.choose_spec.choose_spec.1
-    keyGenBudget_polyTime := hk.choose_spec.choose_spec.2.1
-    keyGenWith_mem_support := hk.choose_spec.choose_spec.2.2.1
-    eval_keyGen := hk.choose_spec.choose_spec.2.2.2
-    signWith_polyTime := hs.choose_spec.choose_spec.1
-    signBudget_polyTime := hs.choose_spec.choose_spec.2.1
+    keyGenWith_polyTime := hk_spec.1
+    keyGenBudget_polyTime := hk_rest.1
+    keyGenWith_mem_support := hk_laws.1
+    eval_keyGen := hk_laws.2
+    signWith_polyTime := hs_spec.1
+    signBudget_polyTime := hs_rest.1
     signWith_mem_support := fun sk u msg coins =>
-      hs.choose_spec.choose_spec.2.2.1 (sk, u, msg) coins
+      hs_laws.1 (sk, u, msg) coins
     eval_sign := fun sk u msg length h =>
-      hs.choose_spec.choose_spec.2.2.2 (sk, u, msg) length h }
+      hs_laws.2 (sk, u, msg) length h }
 
 end IndexedSignatureScheme
 

Complexity/Crypto/Computational/MerkleSignature.lean

@@ -130,9 +130,8 @@ verification key opens leaf `u` of the depth-`depth k.length` tree with root `ro
 signature verifies on `H k msg`. -/
 def verify (pk : List Bool) (u : ℕ) (msg sig : List Bool) : Bool :=
   let k := unframe pk
-  let forged := signatureDecoder.decode sig
-  merkleVerify H k (depth k.length) (dropFrame pk) u forged.1 forged.2.2 &&
-    S.verify forged.1 (H k msg) forged.2.1
+  let (vk, ots, path) := signatureDecoder.decode sig
+  merkleVerify H k (depth k.length) (dropFrame pk) u vk path && S.verify vk (H k msg) ots
 
 /-! ### Completeness -/
 
@@ -248,7 +247,7 @@ include hH hlen in
 /-- Merkle signing is uniformly strict PPT. -/
 theorem isPPTOn_sign :
     IsPPTOn (encPair encBits (encPair encUnary encBits)) encBits
-      (fun p => sign S H p.1 p.2.1 p.2.2) := by
+      (fun (sk, u, msg) => sign S H sk u msg) := by
   let E := encPair encBits (encPair encUnary encBits)
   have hdec : ComputableTidilyInPolyTime (fun p : List Bool × ℕ × List Bool =>
       secretKeyDecoder.decode p.1) E (encPair encBits (encList (encPair encBits encBits))) :=
@@ -289,7 +288,8 @@ include hH hlen hcap in
 /-- Merkle verification is computable in polynomial time. -/
 theorem computableInPolyTime_verify :
     ComputableInPolyTime
-      (fun p : List Bool × ℕ × List Bool × List Bool => verify S H depth p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (fun ((pk, u, msg, sig) : List Bool × ℕ × List Bool × List Bool) =>
+        verify S H depth pk u msg sig)
       (encPair encBits (encPair encUnary (encPair encBits encBits))) encBool := by
   apply ComputableInPolyTime.of_tidy
   let E := encPair encBits (encPair encUnary (encPair encBits encBits))

Complexity/Crypto/Computational/MerkleSignature/Security.lean

@@ -103,13 +103,13 @@ keys `keys`: a collision in the tree if the forged verification key is not the o
 and otherwise the forged message with a message signed at leaf `u` with the same digest. -/
 def collisionOf (k : List Bool) (keys : List (List Bool × List Bool))
     (out : (ℕ × List Bool × List Bool) × List (ℕ × List Bool)) : List Bool × List Bool :=
-  let u := out.1.1
-  let forged := signatureDecoder.decode out.1.2.2
+  let ((u, msg, sig), signed) := out
+  let (vk, _, path) := signatureDecoder.decode sig
   let vks := keys.map Prod.fst
-  if forged.1 == vks.getD u [] then
-    (out.1.2.1, (out.2.find? fun e => e.1 == u && H k e.2 == H k out.1.2.1).elim [] Prod.snd)
+  if vk == vks.getD u [] then
+    (msg, (signed.find? fun e => e.1 == u && H k e.2 == H k msg).elim [] Prod.snd)
   else
-    extractMerkleCollision H k forged.1 (vks.getD u []) u forged.2.2 (merklePath H k vks u)
+    extractMerkleCollision H k vk (vks.getD u []) u path (merklePath H k vks u)
 
 /-- The collision finder: given the hash key `k`, generate the one-time keys, answer the forger's
 signing queries honestly, and return `collisionOf` its forgery. -/
@@ -166,7 +166,9 @@ noncomputable def oneTimeForgerAt (bound : ℕ → ℕ) (adversary : IndexedForg
     (ProbOracleComp.handler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j)))
       (plantedHandler S H depth n setup.1 setup.2 i (bound n)))
     (adversary n (publicKey H setup.1 setup.2))).run []
-  return (H setup.1 out.1.2.1, (signatureDecoder.decode out.1.2.2).2.1)
+  let ((_, msg, sig), _) := out
+  let (_, ots, _) := signatureDecoder.decode sig
+  return (H setup.1 msg, ots)
 
 /-- The one-time forger: plant the challenge at a uniform leaf. -/
 noncomputable def oneTimeForger (bound : ℕ → ℕ) (adversary : IndexedForger) : Forger :=

Complexity/Crypto/Computational/OneWayToSignature.lean

@@ -583,7 +583,8 @@ noncomputable def lamportInverter (f : List Bool → List Bool)
     let out ← (OracleComp.interpret
       (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
         ((lamportScheme f hf).oneTimeSigningOracle keys.2)) (adversary n keys.1)).run []
-    return (frames out.1.2).getD (j / 2) []
+    let msig := out.1
+    return (frames msig.2).getD (j / 2) []
   else
     return []
 

Complexity/Crypto/Computational/PedersenCommitment.lean

@@ -182,9 +182,8 @@ theorem pedersenCommit_smul_generator_eq_iff (d : F.Desc) (α m₀ r₀ m₁ r
 /-- Pedersen commitment on encoded group elements: given `(d, encode h, m, r)`, compute
 `encode (m • g + r • h)`. -/
 def encodePedersenCommit (input : F.Desc × List Bool × ℕ × ℕ) : List Bool :=
-  F.add (input.1,
-    F.smul (input.1, input.2.2.1, F.encode input.1 (F.generator input.1)),
-    F.smul (input.1, input.2.2.2, input.2.1))
+  let (d, h, m, r) := input
+  F.add (d, F.smul (d, m, F.encode d (F.generator d)), F.smul (d, r, h))
 
 /-- `encodePedersenCommit` computes `F.encode d (F.pedersenCommit d h m r)` on encoded group
 elements. -/
@@ -510,9 +509,13 @@ Section 10.6.1, Fact 10.3). -/
 theorem pedersenExtractNat_eq_of_isBindingCollision (d : F.Desc) (α : ZMod (F.order d))
     {out : List Bool × (List Bool × List Bool) × (List Bool × List Bool)}
     (hcoll : F.pedersenScheme.isBindingCollision ⟨d, α • F.generator d⟩ out = true) :
+    let openings := out.2
+    let open₀ := openings.1
+    let open₁ := openings.2
     (pedersenExtractNat (F.order d)
-      (ofBits out.2.1.1) (ofBits out.2.1.2)
-      (ofBits out.2.2.1) (ofBits out.2.2.2) : ZMod (F.order d)) = α := by
+      (ofBits open₀.1) (ofBits open₀.2)
+      (ofBits open₁.1) (ofBits open₁.2) : ZMod (F.order d)) = α := by
+  dsimp only
   simp only [CommitmentScheme.isBindingCollision, pedersenScheme, pedersenVerify,
     Bool.and_eq_true, decide_eq_true_eq] at hcoll
   rcases hcoll with ⟨⟨hne, ⟨hm₀_lt, hm₀_bits⟩, hc₀⟩, ⟨hm₁_lt, hm₁_bits⟩, hc₁⟩
@@ -548,9 +551,12 @@ def pedersenToDLAdversary
       ProbComp (List Bool × (List Bool × List Bool) × (List Bool × List Bool)))
     (n : ℕ) (input : F.Desc × List Bool) : ProbComp (List Bool) := do
   let out ← adversary n (encPair F.encDesc encBits input)
+  let openings := out.2
+  let open₀ := openings.1
+  let open₁ := openings.2
   return (pedersenExtractNat (F.order input.1)
-    (ofBits out.2.1.1) (ofBits out.2.1.2)
-    (ofBits out.2.2.1) (ofBits out.2.2.2)).bits
+    (ofBits open₀.1) (ofBits open₀.2)
+    (ofBits open₁.1) (ofBits open₁.2)).bits
 
 /-- **Exact binding-to-discrete-logarithm reduction** ([BonehShoup2023], Section 10.6.1,
 Theorem 10.4, pp. 414–415; [Pedersen1991], Section 3, Theorem 3.1): for every security parameter

Complexity/Crypto/Computational/PedersenCommitment/ProbComp.lean

@@ -68,7 +68,7 @@ public key encoding, and message word. -/
 theorem isPPTOn_pedersenCommitProb :
     IsPPTOn (encPair encUnary (encPair F.pedersenScheme.encodeKey encBits))
       (encPair encBits encBits)
-      (fun p : ℕ × F.PedersenKey × List Bool => F.pedersenCommitProb p.1 p.2.1 p.2.2) := by
+      (fun ((n, key, msg) : ℕ × F.PedersenKey × List Bool) => F.pedersenCommitProb n key msg) := by
   let E := encPair encUnary (encPair F.pedersenScheme.encodeKey encBits)
   have hn := ComputableInPolyTime.fst encUnary (encPair F.pedersenScheme.encodeKey encBits)
   have hrest := ComputableInPolyTime.snd encUnary (encPair F.pedersenScheme.encodeKey encBits)

Complexity/Crypto/Computational/PedersenCommitment/PublicOperations.lean

@@ -52,10 +52,9 @@ opening words. The public element is already encoded; no discrete logarithm or s
 value is supplied to this algorithm. -/
 def encodePedersenVerify
     (input : (F.Desc × List Bool) × List Bool × List Bool × List Bool) : Bool :=
-  decide (ofBits input.2.1 < F.order input.1.1) &&
-    decide ((ofBits input.2.1).bits = input.2.1) &&
-    decide (F.encodePedersenCommit
-      (input.1.1, input.1.2, ofBits input.2.1, ofBits input.2.2.2) = input.2.2.1)
+  let ((d, h), m, c, o) := input
+  decide (ofBits m < F.order d) && decide ((ofBits m).bits = m) &&
+    decide (F.encodePedersenCommit (d, h, ofBits m, ofBits o) = c)
 
 /-- The encoded verifier computes exactly the verifier used by `pedersenScheme`. -/
 @[simp]
@@ -109,7 +108,7 @@ noncomputable def pedersenPublicOperations : F.pedersenScheme.PublicOperations w
       (encPair encBits (encPair encBits encBits))
     have hv := F.computableInPolyTime_encodePedersenVerify.comp (hpublic.prod hrest)
     convert hv using 1
-    funext p
-    exact (F.encodePedersenVerify_encode p.1.1 p.1.2 p.2.1 p.2.2.1 p.2.2.2).symm
+    funext ⟨⟨d, h⟩, m, c, o⟩
+    exact (F.encodePedersenVerify_encode d h m c o).symm
 
 end Cslib.Crypto.PrimeOrderGroupFamily

Complexity/Crypto/Computational/Signature.lean

@@ -173,8 +173,9 @@ def eufCmaGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) :
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.signingOracle keys.2)) (adversary n keys.1)).run []
-  return (out.1.1.length == n) && !out.2.contains out.1.1 &&
-    S.verify keys.1 out.1.1 out.1.2
+  let msig := out.1
+  return (msig.1.length == n) && !out.2.contains msig.1 &&
+    S.verify keys.1 msig.1 msig.2
 
 attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Run the complete EUF-CMA experiment on its unary security parameter for any oracle-PPT
@@ -275,8 +276,9 @@ def eufOneTimeGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) :
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (S.oneTimeSigningOracle keys.2)) (adversary n keys.1)).run []
-  return (out.1.1.length == n) && !out.2.contains out.1.1 &&
-    S.verify keys.1 out.1.1 out.1.2
+  let msig := out.1
+  return (msig.1.length == n) && !out.2.contains msig.1 &&
+    S.verify keys.1 msig.1 msig.2
 
 /-- Running an oracle-PPT forger against `oneTimeSigningOracle` is uniformly strict PPT in the
 unary security parameter, public key, and secret key. -/