From 8f6fa4d43a3310c4f64019d740ffbe513a037c9d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 26 Oct 2026 18:10:19 -0400 Subject: [PATCH 1/2] feat(crypto): add hidden-bit XOR game-hop laws in Game.lean (#1047, #733) --- Complexity/Crypto/Game.lean | 59 ++++++++++++++++++++++++++ ComplexityTests/Crypto/GameBounds.lean | 39 +++++++++++++++++ 2 files changed, 98 insertions(+) diff --git a/Complexity/Crypto/Game.lean b/Complexity/Crypto/Game.lean index 70e93dae3..e289aabc6 100644 --- a/Complexity/Crypto/Game.lean +++ b/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 diff --git a/ComplexityTests/Crypto/GameBounds.lean b/ComplexityTests/Crypto/GameBounds.lean index 6b5124eab..b1282c993 100644 --- a/ComplexityTests/Crypto/GameBounds.lean +++ b/ComplexityTests/Crypto/GameBounds.lean @@ -59,4 +59,43 @@ 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 +-- Hidden-bit XOR mixture bound `advantage_le_two_mul_uniform_bool_xor`. +example (g₀ g₁ : Bool → Game) : + 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 g₀ g₁ + +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 From 3e6ef9f09d2c60e4935afdfcf7ffc17e1a4ba0c2 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 26 Oct 2026 18:34:23 -0400 Subject: [PATCH 2/2] test(Crypto/GameBounds): exercise concrete instance of advantage_le_two_mul_uniform_bool_xor --- ComplexityTests/Crypto/GameBounds.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/ComplexityTests/Crypto/GameBounds.lean b/ComplexityTests/Crypto/GameBounds.lean index b1282c993..514fe83d1 100644 --- a/ComplexityTests/Crypto/GameBounds.lean +++ b/ComplexityTests/Crypto/GameBounds.lean @@ -71,14 +71,17 @@ example : simp [Game.succProbability] open Cslib.Probability in --- Hidden-bit XOR mixture bound `advantage_le_two_mul_uniform_bool_xor`. -example (g₀ g₁ : Bool → Game) : +-- 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 g₀ g₁ + 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