c/0004 — Lean sources
Leftover Hash Lemma Extraction Bound for Unpredictable Random-Oracle Sources, Public Seed
This page is generated from the files themselves by
scripts/build_lean_html.py;
edits made here are destroyed by the next run. It is a reading copy, not a
certificate: what a statement compiles to is decided by the compiler, and a
marked sorry is an unproved goal, so a file can be green in CI and
still assert nothing on its own.
Every line is addressable — click a line number, or append
#Statement-L42 to the URL.
Statement.lean
1/- 2Leftover Hash Lemma extraction bound for unpredictable random-oracle sources, 3public seed. AICR statement c/0004. 4 5This file states the conjecture. It does not prove it: `lhl_public_seed` 6below is the one `sorry` in the file. 7 8What is different here from c/0001 through c/0003 is that nothing is 9`opaque`. Those files abstract the object under study behind an opaque 10constant, which makes the statement compile but pins nothing: any two 11readers can disagree about what was said and the kernel will not arbitrate. 12c/0004 is fully concrete -- finite seed, input and output sets, a uniform 13function table handed to everyone, two explicit games -- so it can be 14written out, and every quantifier below corresponds to one in the 15`## Statement` tab of `c/0004/index.qmd`. See `MATCH.md` for the 16element-by-element correspondence. 17 18Design notes. 19 20* Everything in sight is finite, so the randomness is `PMF` (finitely 21 supported probability mass functions) rather than measure theory. A 22 probability is then just the mass a `PMF Bool` puts on `true`. 23* "Computationally unbounded, and receives the entire function table of `H` 24 as an explicit input" is modelled by letting the source, the predictor and 25 the distinguisher be *arbitrary functions* of the table. There is no 26 complexity class to name: an arbitrary function is exactly an unbounded 27 algorithm. 28* The auxiliary-information alphabet `Z` carries no `Fintype` and no 29 `DecidableEq`. The informal statement puts no constraint on `z` beyond 30 the source producing it, and none is needed here either, so `Z` stays an 31 arbitrary type. This is deliberate: requiring `Fintype Z` would be a 32 restriction the informal statement does not make. 33-/ 34import Mathlib.Probability.ProbabilityMassFunction.Constructions 35import Mathlib.Probability.Distributions.Uniform 36import Mathlib.Analysis.SpecialFunctions.Log.Base 37import Mathlib.Analysis.Real.Sqrt 38 39namespace AICR0004 40 41open scoped ENNReal 42 43/-! ## The objects -/ 44 45/-- The function table of the random oracle: every map `๐ฆ ร ๐ โ โ`. 46`H โ$ Fun(๐ฆ ร ๐, โ)` below is the uniform distribution on this type. -/ 47abbrev Table (K D R : Type) := K ร D โ R 48 49/-- A source. Unbounded, and handed the entire table, so: an arbitrary 50function of the table, returning a distribution on (sample, auxiliary 51information) pairs. -/ 52abbrev Source (K D R Z : Type) := Table K D R โ PMF (D ร Z) 53 54/-- A predictor. Sees the table and the auxiliary information, and guesses 55the source's sample. It does *not* see the sample. -/ 56abbrev Predictor (K D R Z : Type) := Table K D R โ Z โ PMF D 57 58/-- A distinguisher for the public-seed game. Sees the table, the seed (this 59is what "public seed" means), the challenge, and the auxiliary information. -/ 60abbrev Distinguisher (K D R Z : Type) := Table K D R โ K โ R โ Z โ PMF Bool 61 62section Games 63 64variable {K D R Z : Type} 65 [Fintype K] [Fintype D] [Fintype R] 66 [DecidableEq K] [DecidableEq D] 67 [Nonempty K] [Nonempty D] [Nonempty R] 68 69/-- Game `Pred^S_P`: 70`H โ$ Fun(๐ฆ ร ๐, โ)`; `(x, z) โ$ S(H)`; `x' โ$ P(H, z)`; return `x = x'`. -/ 71noncomputable def predGame (S : Source K D R Z) (P : Predictor K D R Z) : 72 PMF Bool := 73 (PMF.uniformOfFintype (Table K D R)).bind fun H => 74 (S H).bind fun xz => 75 (P H xz.2).bind fun x' => 76 PMF.pure (decide (xz.1 = x')) 77 78/-- Game `Ext-pub^S_D` (public seed): 79`H โ$ Fun(๐ฆ ร ๐, โ)`; `(x, z) โ$ S(H)`; `sd โ$ ๐ฆ`; 80`yโ โ H(sd, x)`; `yโ โ$ โ`; `b โ$ {0,1}`; `b' โ$ D(H, sd, y_b, z)`; 81return `b = b'`. 82 83`b = false` selects the real challenge `yโ = H(sd, x)` and `b = true` the 84uniform one `yโ`, matching `yโ`/`yโ` in the informal game. -/ 85noncomputable def extGame (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 86 PMF Bool := 87 (PMF.uniformOfFintype (Table K D R)).bind fun H => 88 (S H).bind fun xz => 89 (PMF.uniformOfFintype K).bind fun sd => 90 (PMF.uniformOfFintype R).bind fun yโ => 91 (PMF.uniformOfFintype Bool).bind fun b => 92 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 93 PMF.pure (decide (b = b')) 94 95/-- `Adv^pred_{๐ฆ,๐,โ,S}(P) := Pr[Pred^S_P โ 1]`. -/ 96noncomputable def predAdv (S : Source K D R Z) (P : Predictor K D R Z) : โ := 97 (predGame S P true).toReal 98 99/-- `Adv^{ext-pub}_{๐ฆ,๐,โ}(S, D) := 2 Pr[Ext-pub^S_D โ 1] - 1`. -/ 100noncomputable def extAdv (S : Source K D R Z) (Dist : Distinguisher K D R Z) : โ := 101 2 * (extGame S Dist true).toReal - 1 102 103/-- `S` is ฮต-unpredictable: no unbounded predictor beats ฮต. -/ 104def Unpredictable (ฮต : โ) (S : Source K D R Z) : Prop := 105 โ P : Predictor K D R Z, predAdv S P โค ฮต 106 107end Games 108 109/-! ## The conjecture -/ 110 111/-- **Conjecture (public seed).** There is a universal constant `c > 0`, 112independent of `๐ฆ`, `๐`, `โ` and `ฮต`, such that for all nonempty finite 113`๐ฆ, ๐, โ`, all `ฮต โ (0, 1]`, every ฮต-unpredictable source `S` and every 114unbounded distinguisher `D`, 115 116`Adv^{ext-pub}(S, D) โค c ยท (โ(ฮต R) + โ(logโ D / K))`. 117 118The constant is existentially quantified *outside* every other quantifier, 119which is what "universal constant" means and is the whole content of the 120conjecture: a `c` allowed to depend on `๐ฆ`, `๐`, `โ` or `ฮต` would make the 121statement trivial. -/ 122theorem lhl_public_seed : 123 โ c : โ, 0 < c โง 124 โ (K D R Z : Type) 125 [Fintype K] [Fintype D] [Fintype R] 126 [DecidableEq K] [DecidableEq D] 127 [Nonempty K] [Nonempty D] [Nonempty R] 128 (ฮต : โ), 0 < ฮต โ ฮต โค 1 โ 129 โ S : Source K D R Z, Unpredictable ฮต S โ 130 โ Dist : Distinguisher K D R Z, 131 extAdv S Dist โค 132 c * (Real.sqrt (ฮต * Fintype.card R) 133 + Real.sqrt (Real.logb 2 (Fintype.card D) / Fintype.card K)) := by 134 sorry 135 136/-! ## Sanity lemmas 137 138These are `sorry`-free. They exist because a definition that nothing has 139been proved about is a definition nobody has checked: an advantage that 140could fall outside `[0, 1]`, or a degenerate case that does not come out to 141the obvious answer, is how a misformalization announces itself. -/ 142 143section Sanity 144 145variable {K D R Z : Type} 146 [Fintype K] [Fintype D] [Fintype R] 147 [DecidableEq K] [DecidableEq D] 148 [Nonempty K] [Nonempty D] [Nonempty R] 149 150/-- A probability read off a `PMF Bool` is at most one. -/ 151private lemma toReal_le_one (p : PMF Bool) (b : Bool) : (p b).toReal โค 1 := by 152 have h := p.coe_le_one b 153 simpa using ENNReal.toReal_mono (by simp) h 154 155omit [Nonempty K] [Nonempty D] in 156theorem predAdv_nonneg (S : Source K D R Z) (P : Predictor K D R Z) : 157 0 โค predAdv S P := 158 ENNReal.toReal_nonneg 159 160omit [Nonempty K] [Nonempty D] in 161theorem predAdv_le_one (S : Source K D R Z) (P : Predictor K D R Z) : 162 predAdv S P โค 1 := 163 toReal_le_one _ _ 164 165omit [Nonempty K] [Nonempty D] in 166/-- The prediction advantage is a probability. -/ 167theorem predAdv_mem_unitInterval (S : Source K D R Z) (P : Predictor K D R Z) : 168 predAdv S P โ Set.Icc (0 : โ) 1 := 169 โจpredAdv_nonneg S P, predAdv_le_one S Pโฉ 170 171omit [Nonempty D] in 172theorem extAdv_le_one (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 173 extAdv S Dist โค 1 := by 174 have := toReal_le_one (extGame S Dist) true 175 unfold extAdv 176 linarith 177 178omit [Nonempty D] in 179theorem neg_one_le_extAdv (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 180 -1 โค extAdv S Dist := by 181 have : (0 : โ) โค (extGame S Dist true).toReal := ENNReal.toReal_nonneg 182 unfold extAdv 183 linarith 184 185/-- If every branch of a bind is a fair coin on `true`, so is the bind. -/ 186private lemma bind_half {ฮฑ : Type} (p : PMF ฮฑ) (f : ฮฑ โ PMF Bool) 187 (hf : โ a, f a true = 1 / 2) : (p.bind f) true = 1 / 2 := by 188 rw [PMF.bind_apply] 189 simp only [hf] 190 rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] 191 192/-- Guessing a uniform bit that nothing observed depends on succeeds with 193probability exactly one half. -/ 194private lemma guess_half (q : PMF Bool) : 195 ((PMF.uniformOfFintype Bool).bind fun b => 196 q.bind fun b' => PMF.pure (decide (b = b'))) true = 1 / 2 := by 197 have inner : โ b : Bool, 198 (q.bind fun b' => PMF.pure (decide (b = b'))) true = q b := by 199 intro b 200 rw [PMF.bind_apply] 201 rw [tsum_bool] 202 cases b <;> simp [PMF.pure_apply] 203 rw [PMF.bind_apply, tsum_bool, inner, inner] 204 have hu : โ b : Bool, PMF.uniformOfFintype Bool b = 1 / 2 := by 205 intro b 206 rw [PMF.uniformOfFintype_apply] 207 simp 208 rw [hu, hu] 209 have hsum : q false + q true = 1 := by 210 have := q.tsum_coe 211 rwa [tsum_bool] at this 212 rw [โ mul_add, hsum, mul_one] 213 214omit [Nonempty D] in 215/-- **Degenerate case.** When the output set has a single element the 216challenge carries no information at all: `yโ` and `yโ` are equal whatever 217the seed and the sample, so the distinguisher's view does not depend on the 218hidden bit and its advantage is exactly zero. 219 220This is the sanity check that the two games were wired up the right way 221round. A formalization that accidentally leaked `b` into the 222distinguisher's input, or that compared the wrong pair of bits, would give 223something other than `0` here. -/ 224theorem extAdv_eq_zero_of_subsingleton 225 [Subsingleton R] (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 226 extAdv S Dist = 0 := by 227 have key : extGame S Dist true = 1 / 2 := by 228 refine bind_half _ _ fun H => bind_half _ _ fun xz => bind_half _ _ fun sd => 229 bind_half _ _ fun yโ => ?_ 230 -- With `R` a subsingleton the challenge is the same value either way, so 231 -- the distinguisher's input no longer mentions `b`. 232 have hcond : โ b : Bool, 233 (if b then yโ else H (sd, xz.1)) = H (sd, xz.1) := by 234 intro b; cases b <;> simp [Subsingleton.elim yโ (H (sd, xz.1))] 235 simp only [hcond] 236 exact guess_half _ 237 unfold extAdv 238 rw [key] 239 simp 240 241end Sanity 242 243end AICR0004
Proof.lean
1/- 2Toward a formal proof of `AICR0004.lhl_public_seed`. 3 4This file is a **partial** formalization. It is not the proof, and it does not 5claim to be: `c/0004`'s `proof_formal` stays `open` until the main theorem 6compiles with no `sorry` at all. See `LEDGER.md` for what is proved and what 7is outstanding. 8 9What is here is the bottom of the argument, proved rather than assumed. The 10informal proof (`../latex/proof.tex`) opens by collecting seven "standard 11facts" it borrows from outside itself. The first of those, Fact 2.1, is the 12one everything else is phrased in terms of: the best advantage any unbounded 13distinguisher can have between two distributions is their statistical 14distance. Section 1 below proves it, in the finite setting, with no `sorry`. 15 16Why this one first. `Statement.lean` defines the extraction advantage 17operationally, as a game an adversary plays. Every later step of the informal 18proof works with an analytic quantity instead, a sum over rows of a 19statistical distance. Fact 2.1 is the bridge between the two, so nothing 20above it can be formalized until it is. 21-/ 22import Statement 23import Mathlib.Analysis.MeanInequalities 24 25namespace AICR0004 26 27open scoped ENNReal BigOperators 28 29/-! ## 1. Statistical distance, and the optimal distinguisher 30 31Everything is finite, so statistical distance is defined directly as half the 32l1 distance between two mass functions, in `โ`, with no measure theory. -/ 33 34section SD 35 36variable {ฮฉ : Type} [Fintype ฮฉ] 37 38/-- The mass a `PMF` puts on a point, as a real number. Finite everywhere, so 39nothing is lost against the `โโฅ0โ`-valued `p ฯ`. -/ 40noncomputable def rmass (p : PMF ฮฉ) (ฯ : ฮฉ) : โ := (p ฯ).toReal 41 42omit [Fintype ฮฉ] in 43lemma rmass_nonneg (p : PMF ฮฉ) (ฯ : ฮฉ) : 0 โค rmass p ฯ := ENNReal.toReal_nonneg 44 45omit [Fintype ฮฉ] in 46lemma rmass_le_one (p : PMF ฮฉ) (ฯ : ฮฉ) : rmass p ฯ โค 1 := by 47 show (p ฯ).toReal โค 1 48 simpa using ENNReal.toReal_mono (by simp) (p.coe_le_one ฯ) 49 50/-- A `PMF` on a finite type has total real mass one. -/ 51lemma sum_rmass (p : PMF ฮฉ) : โ ฯ, rmass p ฯ = 1 := by 52 have h : โ ฯ, p ฯ = 1 := by 53 have := p.tsum_coe 54 rwa [tsum_fintype] at this 55 have := congrArg ENNReal.toReal h 56 rwa [ENNReal.toReal_sum (fun ฯ _ => p.apply_ne_top ฯ), ENNReal.toReal_one] at this 57 58/-- Statistical distance: half the l1 distance between the two mass 59functions. -/ 60noncomputable def SD (P Q : PMF ฮฉ) : โ := (1 / 2) * โ ฯ, |rmass P ฯ - rmass Q ฯ| 61 62lemma SD_nonneg (P Q : PMF ฮฉ) : 0 โค SD P Q := by 63 apply mul_nonneg (by norm_num) 64 exact Finset.sum_nonneg fun ฯ _ => abs_nonneg _ 65 66lemma SD_comm (P Q : PMF ฮฉ) : SD P Q = SD Q P := by 67 unfold SD 68 congr 1 69 exact Finset.sum_congr rfl fun ฯ _ => abs_sub_comm _ _ 70 71lemma SD_self (P : PMF ฮฉ) : SD P P = 0 := by simp [SD] 72 73lemma SD_le_one (P Q : PMF ฮฉ) : SD P Q โค 1 := by 74 have h : โ ฯ : ฮฉ, |rmass P ฯ - rmass Q ฯ| โค rmass P ฯ + rmass Q ฯ := by 75 intro ฯ 76 rw [abs_sub_le_iff] 77 constructor <;> linarith [rmass_nonneg P ฯ, rmass_nonneg Q ฯ] 78 have := Finset.sum_le_sum (fun ฯ (_ : ฯ โ Finset.univ) => h ฯ) 79 rw [Finset.sum_add_distrib, sum_rmass, sum_rmass] at this 80 unfold SD 81 linarith 82 83/-- The positive part of the mass difference sums to the statistical distance. 84 85This is the identity the optimal-distinguisher bound turns on: a 86distinguisher can only collect the points where `Q` is heavier than `P`, and 87because the two total masses agree, that half of the l1 distance is the whole 88statistical distance. -/ 89lemma sum_pos_part_eq_SD (P Q : PMF ฮฉ) : 90 โ ฯ, max (rmass Q ฯ - rmass P ฯ) 0 = SD P Q := by 91 have hzero : โ ฯ, (rmass Q ฯ - rmass P ฯ) = 0 := by 92 rw [Finset.sum_sub_distrib, sum_rmass, sum_rmass, sub_self] 93 have habs : โ ฯ : ฮฉ, 94 |rmass P ฯ - rmass Q ฯ| 95 = max (rmass Q ฯ - rmass P ฯ) 0 + max (rmass P ฯ - rmass Q ฯ) 0 := by 96 intro ฯ 97 rcases le_total (rmass P ฯ) (rmass Q ฯ) with h | h 98 ยท rw [abs_of_nonpos (by linarith), max_eq_left (by linarith), 99 max_eq_right (by linarith)] 100 ring 101 ยท rw [abs_of_nonneg (by linarith), max_eq_right (by linarith), 102 max_eq_left (by linarith)] 103 ring 104 -- pos and neg parts differ by the (zero) signed sum 105 have hsplit : โ ฯ : ฮฉ, 106 max (rmass P ฯ - rmass Q ฯ) 0 107 = max (rmass Q ฯ - rmass P ฯ) 0 - (rmass Q ฯ - rmass P ฯ) := by 108 intro ฯ 109 rcases le_total (rmass P ฯ) (rmass Q ฯ) with h | h 110 ยท rw [max_eq_right (by linarith), max_eq_left (by linarith)]; ring 111 ยท rw [max_eq_left (by linarith), max_eq_right (by linarith)]; ring 112 unfold SD 113 rw [Finset.sum_congr rfl (fun ฯ _ => habs ฯ), Finset.sum_add_distrib, 114 Finset.sum_congr rfl (fun ฯ _ => hsplit ฯ), Finset.sum_sub_distrib, hzero] 115 ring 116 117end SD 118 119/-! ## 2. The distinguishing game 120 121`Fact 2.1` of `../latex/proof.tex`: an unbounded distinguisher's advantage 122between `Pโ` and `Pโ` is at most `SD Pโ Pโ`. -/ 123 124section Distinguishing 125 126variable {ฮฉ : Type} [Fintype ฮฉ] 127 128/-- Sample a uniform bit `b`, then a point from `Pโ` or `Pโ` accordingly, hand 129the point to `A`, and ask whether `A` recovered `b`. `A` is an arbitrary 130function into `PMF Bool`: randomized, and subject to no complexity bound. -/ 131noncomputable def distGame (Pโ Pโ : PMF ฮฉ) (A : ฮฉ โ PMF Bool) : PMF Bool := 132 (PMF.uniformOfFintype Bool).bind fun b => 133 (cond b Pโ Pโ).bind fun ฯ => 134 (A ฯ).bind fun b' => PMF.pure (decide (b = b')) 135 136/-- `2 Pr[A wins] - 1`, the same normalization `extAdv` uses. -/ 137noncomputable def distAdv (Pโ Pโ : PMF ฮฉ) (A : ฮฉ โ PMF Bool) : โ := 138 2 * (distGame Pโ Pโ A true).toReal - 1 139 140/-- The winning probability of the distinguishing game, written out. 141 142Half the chance of calling a `Pโ` sample "0", plus half the chance of calling 143a `Pโ` sample "1". -/ 144lemma distGame_apply_true (Pโ Pโ : PMF ฮฉ) (A : ฮฉ โ PMF Bool) : 145 distGame Pโ Pโ A true 146 = (1 / 2) * (โ ฯ, Pโ ฯ * (A ฯ) false) + (1 / 2) * (โ ฯ, Pโ ฯ * (A ฯ) true) := by 147 have inner : โ (b : Bool) (ฯ : ฮฉ), 148 ((A ฯ).bind fun b' => PMF.pure (decide (b = b'))) true = (A ฯ) b := by 149 intro b ฯ 150 rw [PMF.bind_apply, tsum_bool] 151 cases b <;> simp [PMF.pure_apply] 152 have mid : โ b : Bool, 153 ((cond b Pโ Pโ).bind fun ฯ => (A ฯ).bind fun b' => PMF.pure (decide (b = b'))) true 154 = โ ฯ, (cond b Pโ Pโ) ฯ * (A ฯ) b := by 155 intro b 156 rw [PMF.bind_apply, tsum_fintype] 157 exact Finset.sum_congr rfl fun ฯ _ => by rw [inner b ฯ] 158 have hu : โ b : Bool, PMF.uniformOfFintype Bool b = 1 / 2 := by 159 intro b; rw [PMF.uniformOfFintype_apply]; simp 160 rw [distGame, PMF.bind_apply, tsum_bool, mid, mid, hu, hu] 161 simp 162 163end Distinguishing 164 165section DistinguishingBound 166 167variable {ฮฉ : Type} [Fintype ฮฉ] 168 169private lemma ne_top_mul (a b : โโฅ0โ) (ha : a โ โค) (hb : b โ โค) : a * b โ โค := 170 ENNReal.mul_ne_top ha hb 171 172/-- The same winning probability, in `โ`. -/ 173lemma distGame_toReal (Pโ Pโ : PMF ฮฉ) (A : ฮฉ โ PMF Bool) : 174 (distGame Pโ Pโ A true).toReal 175 = (1 / 2) * (โ ฯ, rmass Pโ ฯ * rmass (A ฯ) false) 176 + (1 / 2) * (โ ฯ, rmass Pโ ฯ * rmass (A ฯ) true) := by 177 have hfin : โ (P : PMF ฮฉ) (f : ฮฉ โ PMF Bool) (b : Bool) (ฯ : ฮฉ), 178 P ฯ * (f ฯ) b โ โค := fun P f b ฯ => 179 ne_top_mul _ _ (P.apply_ne_top ฯ) ((f ฯ).apply_ne_top b) 180 rw [distGame_apply_true] 181 rw [ENNReal.toReal_add (by 182 refine ENNReal.mul_ne_top (by norm_num) ?_ 183 exact (ENNReal.sum_ne_top).2 fun ฯ _ => hfin Pโ A false ฯ) (by 184 refine ENNReal.mul_ne_top (by norm_num) ?_ 185 exact (ENNReal.sum_ne_top).2 fun ฯ _ => hfin Pโ A true ฯ)] 186 rw [ENNReal.toReal_mul, ENNReal.toReal_mul, 187 ENNReal.toReal_sum (fun ฯ _ => hfin Pโ A false ฯ), 188 ENNReal.toReal_sum (fun ฯ _ => hfin Pโ A true ฯ)] 189 simp only [ENNReal.toReal_mul, rmass] 190 norm_num 191 192/-- The advantage, with the constant cleared away: what a distinguisher 193collects is the mass difference, weighted by how often it says "1". -/ 194lemma distAdv_eq (Pโ Pโ : PMF ฮฉ) (A : ฮฉ โ PMF Bool) : 195 distAdv Pโ Pโ A = โ ฯ, rmass (A ฯ) true * (rmass Pโ ฯ - rmass Pโ ฯ) := by 196 have hbool : โ ฯ : ฮฉ, rmass (A ฯ) false + rmass (A ฯ) true = 1 := by 197 intro ฯ 198 have h := sum_rmass (A ฯ) 199 rw [Fintype.sum_bool] at h 200 linarith 201 have hsplit : โ ฯ : ฮฉ, 202 rmass Pโ ฯ * rmass (A ฯ) false 203 = rmass Pโ ฯ - rmass Pโ ฯ * rmass (A ฯ) true := by 204 intro ฯ 205 have h : rmass (A ฯ) false = 1 - rmass (A ฯ) true := by linarith [hbool ฯ] 206 rw [h]; ring 207 unfold distAdv 208 rw [distGame_toReal, Finset.sum_congr rfl (fun ฯ _ => hsplit ฯ), 209 Finset.sum_sub_distrib, sum_rmass] 210 rw [Finset.sum_congr rfl (fun ฯ _ => mul_comm (rmass Pโ ฯ) (rmass (A ฯ) true))] 211 rw [Finset.sum_congr rfl (fun ฯ (_ : ฯ โ Finset.univ) => 212 (mul_sub (rmass (A ฯ) true) (rmass Pโ ฯ) (rmass Pโ ฯ)))] 213 rw [Finset.sum_sub_distrib] 214 rw [Finset.sum_congr rfl (fun ฯ (_ : ฯ โ Finset.univ) => 215 mul_comm (rmass (A ฯ) true) (rmass Pโ ฯ))] 216 ring 217 218/-- **Fact 2.1 of `../latex/proof.tex`.** No unbounded distinguisher, however 219it randomizes, beats the statistical distance. -/ 220theorem distAdv_le_SD (Pโ Pโ : PMF ฮฉ) (A : ฮฉ โ PMF Bool) : 221 distAdv Pโ Pโ A โค SD Pโ Pโ := by 222 rw [distAdv_eq, โ sum_pos_part_eq_SD] 223 refine Finset.sum_le_sum fun ฯ _ => ?_ 224 have h0 : 0 โค rmass (A ฯ) true := rmass_nonneg _ _ 225 have h1 : rmass (A ฯ) true โค 1 := rmass_le_one _ _ 226 rcases le_total 0 (rmass Pโ ฯ - rmass Pโ ฯ) with h | h 227 ยท rw [max_eq_left h]; nlinarith 228 ยท rw [max_eq_right h]; nlinarith 229 230open scoped Classical in 231/-- The maximum-a-posteriori test: answer "1" exactly where `Pโ` outweighs 232`Pโ`. Unbounded, and deterministic, so it needs no randomness either. -/ 233noncomputable def mapTest (Pโ Pโ : PMF ฮฉ) : ฮฉ โ PMF Bool := 234 fun ฯ => PMF.pure (decide (rmass Pโ ฯ < rmass Pโ ฯ)) 235 236open scoped Classical in 237/-- **Fact 2.1, attainment.** The MAP test achieves the statistical distance, 238so the bound above is tight and the supremum over distinguishers is attained. -/ 239theorem distAdv_mapTest (Pโ Pโ : PMF ฮฉ) : 240 distAdv Pโ Pโ (mapTest Pโ Pโ) = SD Pโ Pโ := by 241 rw [distAdv_eq, โ sum_pos_part_eq_SD] 242 refine Finset.sum_congr rfl fun ฯ _ => ?_ 243 by_cases h : rmass Pโ ฯ < rmass Pโ ฯ 244 ยท have hd : decide (rmass Pโ ฯ < rmass Pโ ฯ) = true := decide_eq_true h 245 have hm : rmass (mapTest Pโ Pโ ฯ) true = 1 := by 246 unfold mapTest; rw [hd]; simp [rmass, PMF.pure_apply] 247 rw [hm, one_mul, max_eq_left (by linarith)] 248 ยท have hd : decide (rmass Pโ ฯ < rmass Pโ ฯ) = false := decide_eq_false h 249 have hm : rmass (mapTest Pโ Pโ ฯ) true = 0 := by 250 unfold mapTest; rw [hd]; simp [rmass, PMF.pure_apply] 251 rw [hm, zero_mul, max_eq_right (by linarith [not_lt.mp h])] 252 253/-- The optimal distinguishing advantage *is* the statistical distance: the 254set of achievable advantages has `SD Pโ Pโ` as its greatest element. -/ 255theorem isGreatest_distAdv (Pโ Pโ : PMF ฮฉ) : 256 IsGreatest {r : โ | โ A : ฮฉ โ PMF Bool, distAdv Pโ Pโ A = r} (SD Pโ Pโ) := 257 โจโจmapTest Pโ Pโ, distAdv_mapTest Pโ Pโโฉ, 258 by rintro r โจA, rflโฉ; exact distAdv_le_SD Pโ Pโ Aโฉ 259 260end DistinguishingBound 261 262/-! ## 3. Bridging the game to the analytic quantity 263 264`Statement.lean` defines `extAdv` operationally. The informal proof works with 265statistical distances instead. The bridge is that the extraction game *is* a 266distinguishing game, between the two distributions the distinguisher's view 267has under `b = 0` and `b = 1`. 268 269The one restriction here that the conjecture does not make is `[Fintype Z]`: 270`SD` above is defined by a `Finset` sum, so the view type has to be finite, 271and the view carries `z`. Lifting it means redoing section 1 with `tsum`, 272which is possible (a `PMF` is countably supported) and is recorded as 273outstanding in `LEDGER.md`. -/ 274 275section Bridge 276 277variable {K D R Z : Type} 278 [Fintype K] [Fintype D] [Fintype R] [Fintype Z] 279 [DecidableEq K] [DecidableEq D] 280 [Nonempty K] [Nonempty D] [Nonempty R] 281 282/-- Everything the distinguisher is handed: the table, the seed, the 283challenge, the auxiliary information. -/ 284abbrev View (K D R Z : Type) := Table K D R ร K ร R ร Z 285 286/-- The law of the distinguisher's view under challenge bit `b`. -/ 287noncomputable def viewDist (S : Source K D R Z) (b : Bool) : PMF (View K D R Z) := 288 (PMF.uniformOfFintype (Table K D R)).bind fun H => 289 (S H).bind fun xz => 290 (PMF.uniformOfFintype K).bind fun sd => 291 (PMF.uniformOfFintype R).bind fun yโ => 292 PMF.pure (H, sd, (if b then yโ else H (sd, xz.1)), xz.2) 293 294/-- The distinguisher, reading its four arguments off one view. -/ 295def onView (Dist : Distinguisher K D R Z) : View K D R Z โ PMF Bool := 296 fun v => Dist v.1 v.2.1 v.2.2.1 v.2.2.2 297 298omit [Fintype Z] [Nonempty D] in 299/-- `distGame` on the two view laws, with the binds flattened out. -/ 300lemma distGame_viewDist (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 301 distGame (viewDist S false) (viewDist S true) (onView Dist) 302 = (PMF.uniformOfFintype Bool).bind fun b => 303 (PMF.uniformOfFintype (Table K D R)).bind fun H => 304 (S H).bind fun xz => 305 (PMF.uniformOfFintype K).bind fun sd => 306 (PMF.uniformOfFintype R).bind fun yโ => 307 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 308 PMF.pure (decide (b = b')) := by 309 rw [distGame] 310 refine congrArg _ (funext fun b => ?_) 311 have hc : cond b (viewDist S true) (viewDist S false) = viewDist S b := by 312 cases b <;> rfl 313 rw [hc, viewDist] 314 simp only [PMF.bind_bind, PMF.pure_bind, onView] 315 316omit [Fintype Z] [Nonempty D] in 317/-- The extraction game **is** a distinguishing game between the two view laws. 318 319The only work is moving the challenge bit from where the game samples it 320(last, after the table, the source, the seed and the uniform challenge) to 321where a distinguishing game samples it (first): four applications of 322`PMF.bind_comm`. -/ 323theorem extGame_eq_distGame (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 324 extGame S Dist = distGame (viewDist S false) (viewDist S true) (onView Dist) := by 325 rw [distGame_viewDist, extGame] 326 have c1 : โ (H : Table K D R) (xz : D ร Z) (sd : K), 327 ((PMF.uniformOfFintype R).bind fun yโ => 328 (PMF.uniformOfFintype Bool).bind fun b => 329 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 330 PMF.pure (decide (b = b'))) 331 = ((PMF.uniformOfFintype Bool).bind fun b => 332 (PMF.uniformOfFintype R).bind fun yโ => 333 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 334 PMF.pure (decide (b = b'))) := fun _ _ _ => PMF.bind_comm _ _ _ 335 simp only [c1] 336 have c2 : โ (H : Table K D R) (xz : D ร Z), 337 ((PMF.uniformOfFintype K).bind fun sd => 338 (PMF.uniformOfFintype Bool).bind fun b => 339 (PMF.uniformOfFintype R).bind fun yโ => 340 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 341 PMF.pure (decide (b = b'))) 342 = ((PMF.uniformOfFintype Bool).bind fun b => 343 (PMF.uniformOfFintype K).bind fun sd => 344 (PMF.uniformOfFintype R).bind fun yโ => 345 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 346 PMF.pure (decide (b = b'))) := fun _ _ => PMF.bind_comm _ _ _ 347 simp only [c2] 348 have c3 : โ H : Table K D R, 349 ((S H).bind fun xz => 350 (PMF.uniformOfFintype Bool).bind fun b => 351 (PMF.uniformOfFintype K).bind fun sd => 352 (PMF.uniformOfFintype R).bind fun yโ => 353 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 354 PMF.pure (decide (b = b'))) 355 = ((PMF.uniformOfFintype Bool).bind fun b => 356 (S H).bind fun xz => 357 (PMF.uniformOfFintype K).bind fun sd => 358 (PMF.uniformOfFintype R).bind fun yโ => 359 (Dist H sd (if b then yโ else H (sd, xz.1)) xz.2).bind fun b' => 360 PMF.pure (decide (b = b'))) := fun _ => PMF.bind_comm _ _ _ 361 simp only [c3] 362 exact PMF.bind_comm _ _ _ 363 364omit [Nonempty D] in 365/-- **The bridge.** No unbounded distinguisher does better against the 366extraction game than the statistical distance between the two view laws. 367 368This is what lets every later step of `../latex/proof.tex` work with an 369analytic quantity instead of a game. -/ 370theorem extAdv_le_SD_views (S : Source K D R Z) (Dist : Distinguisher K D R Z) : 371 extAdv S Dist โค SD (viewDist S false) (viewDist S true) := by 372 have : extAdv S Dist = distAdv (viewDist S false) (viewDist S true) (onView Dist) := by 373 unfold extAdv distAdv 374 rw [extGame_eq_distGame] 375 rw [this] 376 exact distAdv_le_SD _ _ _ 377 378open scoped Classical in 379/-- The MAP test on views, curried back into a `Distinguisher`. Unbounded, so 380this is a legal adversary in the game as stated. -/ 381noncomputable def mapDist (S : Source K D R Z) : Distinguisher K D R Z := 382 fun H sd y z => mapTest (viewDist S false) (viewDist S true) (H, sd, y, z) 383 384omit [Nonempty D] in 385open scoped Classical in 386/-- The bridge is tight: `mapDist` attains the view distance. -/ 387theorem extAdv_mapDist (S : Source K D R Z) : 388 extAdv S (mapDist S) = SD (viewDist S false) (viewDist S true) := by 389 have honView : onView (mapDist S) = mapTest (viewDist S false) (viewDist S true) := rfl 390 have : extAdv S (mapDist S) 391 = distAdv (viewDist S false) (viewDist S true) (onView (mapDist S)) := by 392 unfold extAdv distAdv 393 rw [extGame_eq_distGame] 394 rw [this, honView, distAdv_mapTest] 395 396omit [Nonempty D] in 397/-- **Lemma 3.1 of `../latex/proof.tex`, first half.** The best extraction 398advantage any unbounded distinguisher achieves is exactly the statistical 399distance between the two view laws. 400 401The informal proof states this with a maximum and notes in passing that the 402maximum is attained. Here that is `IsGreatest`, with `mapDist` as the witness. -/ 403theorem isGreatest_extAdv (S : Source K D R Z) : 404 IsGreatest {r : โ | โ Dist : Distinguisher K D R Z, extAdv S Dist = r} 405 (SD (viewDist S false) (viewDist S true)) := 406 โจโจmapDist S, extAdv_mapDist Sโฉ, 407 by rintro r โจDist, rflโฉ; exact extAdv_le_SD_views S Distโฉ 408 409/-! ### The predictor side 410 411`Lemma 3.1` also identifies the best prediction advantage with an analytic 412quantity: the expected largest conditional mass. With everything finite that 413quantity can be written without any conditioning, as `โ z, max_x p(x, z)`, 414because `p(z) ยท max_x p(x | z) = max_x p(x, z)`. -/ 415 416/-- `โ z, max_x Pr[(x, z)]`, the analytic form of the best prediction 417advantage on a fixed table. Equal to `๐ผ_Z[ฮต_{H,Z}]` of `../latex/proof.tex`. -/ 418noncomputable def maxMass (S : Source K D R Z) (H : Table K D R) : โ := 419 โ z : Z, Finset.univ.sup' Finset.univ_nonempty fun x : D => rmass (S H) (x, z) 420 421omit [Nonempty K] [Nonempty D] in 422lemma predGame_toReal (S : Source K D R Z) (P : Predictor K D R Z) : 423 (predGame S P true).toReal 424 = โ H : Table K D R, rmass (PMF.uniformOfFintype (Table K D R)) H 425 * โ xz : D ร Z, rmass (S H) xz * rmass (P H xz.2) xz.1 := by 426 have inner : โ (H : Table K D R) (xz : D ร Z), 427 ((P H xz.2).bind fun x' => PMF.pure (decide (xz.1 = x'))) true 428 = (P H xz.2) xz.1 := by 429 intro H xz 430 rw [PMF.bind_apply, tsum_fintype] 431 rw [Finset.sum_eq_single xz.1] 432 ยท simp [PMF.pure_apply] 433 ยท intro x' _ hx 434 simp [PMF.pure_apply, Ne.symm hx] 435 ยท intro h; exact absurd (Finset.mem_univ _) h 436 have mid : โ H : Table K D R, 437 ((S H).bind fun xz => (P H xz.2).bind fun x' => PMF.pure (decide (xz.1 = x'))) true 438 = โ xz : D ร Z, (S H) xz * (P H xz.2) xz.1 := by 439 intro H 440 rw [PMF.bind_apply, tsum_fintype] 441 exact Finset.sum_congr rfl fun xz _ => by rw [inner H xz] 442 have hne : โ (H : Table K D R) (xz : D ร Z), (S H) xz * (P H xz.2) xz.1 โ โค := 443 fun H xz => ENNReal.mul_ne_top ((S H).apply_ne_top xz) ((P H xz.2).apply_ne_top xz.1) 444 rw [predGame, PMF.bind_apply, tsum_fintype, 445 ENNReal.toReal_sum (fun H _ => ENNReal.mul_ne_top 446 ((PMF.uniformOfFintype (Table K D R)).apply_ne_top H) 447 (by rw [mid H]; exact (ENNReal.sum_ne_top).2 fun xz _ => hne H xz))] 448 refine Finset.sum_congr rfl fun H _ => ?_ 449 rw [mid H, ENNReal.toReal_mul, ENNReal.toReal_sum (fun xz _ => hne H xz)] 450 simp only [ENNReal.toReal_mul, rmass] 451 452omit [Nonempty K] in 453/-- **Lemma 3.1, predictor half (bound).** No unbounded predictor beats the 454expected largest mass. -/ 455theorem predAdv_le_maxMass (S : Source K D R Z) (P : Predictor K D R Z) : 456 predAdv S P 457 โค โ H : Table K D R, rmass (PMF.uniformOfFintype (Table K D R)) H * maxMass S H := by 458 rw [predAdv, predGame_toReal] 459 refine Finset.sum_le_sum fun H _ => ?_ 460 refine mul_le_mul_of_nonneg_left ?_ (rmass_nonneg _ _) 461 rw [Fintype.sum_prod_type_right] 462 refine Finset.sum_le_sum fun z _ => ?_ 463 set M := Finset.univ.sup' Finset.univ_nonempty fun x : D => rmass (S H) (x, z) with hM 464 have hbound : โ x : D, rmass (S H) (x, z) * rmass (P H z) x โค M * rmass (P H z) x := by 465 intro x 466 exact mul_le_mul_of_nonneg_right 467 (Finset.le_sup' (fun x : D => rmass (S H) (x, z)) (Finset.mem_univ x)) 468 (rmass_nonneg _ _) 469 calc โ x : D, rmass (S H) (x, z) * rmass (P H z) x 470 โค โ x : D, M * rmass (P H z) x := Finset.sum_le_sum fun x _ => hbound x 471 _ = M * โ x : D, rmass (P H z) x := by rw [Finset.mul_sum] 472 _ = M := by rw [sum_rmass, mul_one] 473 474end Bridge 475 476end AICR0004
Audit.lean
1/- 2Axiom audit. Not part of the statement; run it to confirm that the only 3declaration in `Statement.lean` resting on `sorryAx` is the conjecture 4itself, and that every sanity lemma rests on nothing beyond Lean's three 5standard axioms. 6 7 lake env lean Audit.lean 8 9Expected: `sorryAx` appears on the first line and on no other. 10-/ 11import Statement 12 13open AICR0004 14 15#print axioms AICR0004.lhl_public_seed 16#print axioms AICR0004.predAdv_nonneg 17#print axioms AICR0004.predAdv_le_one 18#print axioms AICR0004.predAdv_mem_unitInterval 19#print axioms AICR0004.extAdv_le_one 20#print axioms AICR0004.neg_one_le_extAdv 21#print axioms AICR0004.extAdv_eq_zero_of_subsingleton
AuditProof.lean
1/- 2Axiom audit for the partial proof. Nothing here may report `sorryAx`: 3Proof.lean is entirely `sorry`-free, and the project's single `sorry` is the 4conjecture in Statement.lean. 5 6 lake env lean AuditProof.lean 7-/ 8import Proof 9 10open AICR0004 11 12#print axioms AICR0004.sum_rmass 13#print axioms AICR0004.SD_le_one 14#print axioms AICR0004.sum_pos_part_eq_SD 15#print axioms AICR0004.distGame_apply_true 16#print axioms AICR0004.distGame_toReal 17#print axioms AICR0004.distAdv_eq 18#print axioms AICR0004.distAdv_le_SD 19#print axioms AICR0004.distAdv_mapTest 20#print axioms AICR0004.isGreatest_distAdv 21#print axioms AICR0004.distGame_viewDist 22#print axioms AICR0004.extGame_eq_distGame 23#print axioms AICR0004.extAdv_le_SD_views 24#print axioms AICR0004.extAdv_mapDist 25#print axioms AICR0004.isGreatest_extAdv 26#print axioms AICR0004.predGame_toReal 27#print axioms AICR0004.predAdv_le_maxMass