feat(crypto): add hidden-bit XOR game-hop laws in Game.lean

Complexity/Crypto/Game.lean

@@ -46,6 +46,9 @@ directly, and computational definitions over infinite sample spaces can reuse th
   `Cslib.Crypto.Game.advantage_bind_le_of_support`,
   `Cslib.Crypto.Game.advantage_bind_comm`: `ℝ≥0` mixture, pointwise error-averaging, support,
   and `PMF.bind_comm` advantage lemmas, extracted from the reviewed support in PR #1169.
+* `Cslib.Crypto.Game.succProbability_uniform_bool_xor`,
+  `Cslib.Crypto.Game.advantage_le_two_mul_uniform_bool_xor`: hidden-bit XOR mixture success
+  probability and factor-of-two game-hop bound.
 
 ## References
 
@@ -404,5 +407,61 @@ theorem advantage_bind_comm {α β : Type*} (p : PMF α) (q : PMF β) (f g : α
       (q.bind fun b => p.bind fun a => g a b) := by
   rw [PMF.bind_comm p q f, PMF.bind_comm p q g]
 
+open Probability in
+/-- For any Boolean-indexed family of games `g : Bool → Game`, sampling a uniform hidden bit
+`bit ← PMF.uniformOfFintype Bool` and outputting `guess ^^ bit` for `guess ← g bit` succeeds with
+probability `(1 + succProbability (g false) - succProbability (g true)) / 2`. -/
+theorem succProbability_uniform_bool_xor (g : Bool → Game) :
+    (succProbability
+      ((PMF.uniformOfFintype Bool).bind fun bit => (g bit).map (fun guess => guess ^^ bit)) : ℝ) =
+      (1 + (succProbability (g false) : ℝ) - succProbability (g true)) / 2 := by
+  have h1 :
+      ((PMF.uniformOfFintype Bool).bind fun bit =>
+        (g bit).map (fun guess => guess ^^ bit)) true =
+      2⁻¹ * g false true + 2⁻¹ * g true false := by
+    rw [PMF.bind_apply, tsum_bool]
+    simp [PMF.uniformOfFintype_apply, PMF.map_apply]
+  have hfalse : (g true false).toReal = 1 - (g true true).toReal := by
+    have hsum := succProbability_add_failProbability (g true)
+    have hsumR := congrArg (fun x : ℝ≥0 => (x : ℝ)) hsum
+    simp only [NNReal.coe_add, NNReal.coe_one, succProbability, failProbability,
+      ENNReal.coe_toNNReal_eq_toReal] at hsumR
+    linarith
+  rw [coe_succProbability, h1, ENNReal.toReal_add
+    (ENNReal.mul_ne_top (by simp) (PMF.apply_ne_top _ _))
+    (ENNReal.mul_ne_top (by simp) (PMF.apply_ne_top _ _)),
+    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_inv, ENNReal.toReal_ofNat,
+    hfalse, coe_succProbability, coe_succProbability]
+  ring
+
+open Probability in
+/-- For any two Boolean-indexed game families `g₀, g₁ : Bool → Game`, the advantage
+`advantage (g₀ false) (g₀ true)` is bounded by twice the distinguishing advantage between their
+uniform hidden-bit XOR mixtures plus `advantage (g₁ false) (g₁ true)`. -/
+theorem advantage_le_two_mul_uniform_bool_xor (g₀ g₁ : Bool → Game) :
+    advantage (g₀ false) (g₀ true) ≤
+      2 * advantage
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₀ bit).map (fun guess => guess ^^ bit))
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₁ bit).map (fun guess => guess ^^ bit)) +
+      advantage (g₁ false) (g₁ true) := by
+  rw [← NNReal.coe_le_coe]
+  simp only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_ofNat, coe_advantage,
+    succProbability_uniform_bool_xor]
+  have hle :
+      |((succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) -
+        ((succProbability (g₁ false) : ℝ) - succProbability (g₁ true))| =
+      2 * |(1 + (succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) / 2 -
+        (1 + (succProbability (g₁ false) : ℝ) - succProbability (g₁ true)) / 2| := by
+    rw [show (1 + (succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) / 2 -
+        (1 + (succProbability (g₁ false) : ℝ) - succProbability (g₁ true)) / 2 =
+      (((succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) -
+        ((succProbability (g₁ false) : ℝ) - succProbability (g₁ true))) / 2 by ring,
+      abs_div, Nat.abs_ofNat]
+    ring
+  have htri := abs_sub_abs_le_abs_sub
+    ((succProbability (g₀ false) : ℝ) - succProbability (g₀ true))
+    ((succProbability (g₁ false) : ℝ) - succProbability (g₁ true))
+  linarith
+
 end Game
 end Cslib.Crypto

ComplexityTests/Crypto/GameBounds.lean

@@ -59,4 +59,46 @@ example {α β : Type*} (p : PMF α) (q : PMF β) (f g : α → β → Game) :
       (q.bind fun b => p.bind fun a => g a b) :=
   Game.advantage_bind_comm p q f g
 
+open Cslib.Probability in
+-- Concrete check of `succProbability_uniform_bool_xor`: when `g false = PMF.pure true` and
+-- `g true = PMF.pure false`, `guess ^^ bit` is always `true`, so the success probability is `1`.
+example :
+    (Game.succProbability
+      ((PMF.uniformOfFintype Bool).bind fun bit =>
+        ((if bit then PMF.pure false else PMF.pure true : Game)).map
+          (fun guess => guess ^^ bit)) : ℝ) = 1 := by
+  rw [Game.succProbability_uniform_bool_xor]
+  simp [Game.succProbability]
+
+open Cslib.Probability in
+-- Concrete application of `advantage_le_two_mul_uniform_bool_xor` on `g₀ bit = PMF.pure (!bit)` and
+-- `g₁ _ = PMF.pure false` (where the inequality holds with equality `1 ≤ 2 * (1 / 2) + 0`).
+example :
+    let g₀ : Bool → Game := fun bit => PMF.pure (!bit)
+    let g₁ : Bool → Game := fun _ => PMF.pure false
+    Game.advantage (g₀ false) (g₀ true) ≤
+      2 * Game.advantage
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₀ bit).map (fun guess => guess ^^ bit))
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₁ bit).map (fun guess => guess ^^ bit)) +
+      Game.advantage (g₁ false) (g₁ true) :=
+  Game.advantage_le_two_mul_uniform_bool_xor (fun bit => PMF.pure (!bit)) (fun _ => PMF.pure false)
+
+open Cslib.Probability in
+-- Tightness / refutation test: the factor `2` in `advantage_le_two_mul_uniform_bool_xor` cannot be
+-- replaced by `1`. For `g₀ bit = PMF.pure (!bit)` and `g₁ _ = PMF.pure false`, the game gap of `g₀`
+-- is `1`, the game gap of `g₁` is `0`, and the hidden-bit XOR mixture advantage is `1 / 2`.
+example :
+    let g₀ : Bool → Game := fun bit => PMF.pure (!bit)
+    let g₁ : Bool → Game := fun _ => PMF.pure false
+    ¬ (Game.advantage (g₀ false) (g₀ true) ≤
+      1 * Game.advantage
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₀ bit).map (fun guess => guess ^^ bit))
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₁ bit).map (fun guess => guess ^^ bit)) +
+      Game.advantage (g₁ false) (g₁ true)) := by
+  dsimp only
+  rw [← NNReal.coe_le_coe]
+  simp only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_one, Game.coe_advantage,
+    Game.succProbability_uniform_bool_xor, Game.succProbability]
+  norm_num
+
 end ComplexityTests.GameBounds