Skip to content

Commit 2a21c4a

Browse files
quangvdaoquangvdao
committed
refactor: extract helpers, deduplicate proofs, relocate misplaced code
- Extract ENNReal Cauchy-Schwarz inequalities to ToMathlib/Data/ENNReal/SumSquares.lean - Factor out cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey in SymmEncAlg.lean, derive both Shannon theorems and ciphertextRowsEqualAt from it - Remove unused perfectSecrecyAt_iff_allDefs / perfectSecrecy_iff_allDefs lemmas - Move XOR probability lemmas to OracleComp/Constructions/BitVec.lean - Add generic probEvent_liftComp_uniformSample_eq_of_eq helper in SeededOracle.lean, simplify seed-slot collision lemmas in Fork.lean - Extract length_eq_of_mem_support_generateSeed to deduplicate repeated blocks Net -150 lines. Made-with: Cursor
1 parent 6801348 commit 2a21c4a

File tree

7 files changed

+271
-280
lines changed

7 files changed

+271
-280
lines changed

‎Examples/OneTimePad.lean‎

Lines changed: 1 addition & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Devon Tuma
55
-/
66
import VCVio.CryptoFoundations.SymmEncAlg
7-
import VCVio.EvalDist.BitVec
7+
import VCVio.OracleComp.Constructions.BitVec
88
import Mathlib.Data.Vector.Zip
99

1010
/-!
@@ -32,73 +32,6 @@ namespace oneTimePad
3232
lemma complete : (oneTimePad).Complete := by
3333
simp [oneTimePad, SymmEncAlg.Complete, SymmEncAlg.CompleteExp]
3434

35-
lemma probOutput_xor_uniform (sp : ℕ) (msg σ : BitVec sp) :
36-
Pr[= σ | (fun k : BitVec sp => k ^^^ msg) <$> ($ᵗ BitVec sp)] =
37-
(Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := by
38-
calc
39-
Pr[= σ | (fun k : BitVec sp => k ^^^ msg) <$> ($ᵗ BitVec sp)] =
40-
Pr[= σ | (msg ^^^ ·) <$> ($ᵗ BitVec sp)] := by
41-
simp [BitVec.xor_comm]
42-
_ = Pr[= msg ^^^ σ | ($ᵗ BitVec sp)] := by
43-
simpa using probOutput_xor_map (mx := ($ᵗ BitVec sp)) (x := msg) (y := σ)
44-
_ = (Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := by
45-
simp [probOutput_uniformSample]
46-
47-
lemma probOutput_pair_xor_uniform (sp : ℕ) (mx : ProbComp (BitVec sp))
48-
(msg σ : BitVec sp) :
49-
Pr[= (msg, σ) | do
50-
let msg' ← mx
51-
let k ← $ᵗ BitVec sp
52-
return (msg', k ^^^ msg')] =
53-
Pr[= msg | mx] * (Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := by
54-
let inv : ℝ≥0∞ := (Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹
55-
rw [probOutput_bind_eq_tsum]
56-
have hinner (msg' : BitVec sp) :
57-
Pr[= (msg, σ) | do
58-
let k ← $ᵗ BitVec sp
59-
return (msg', k ^^^ msg')] = if msg = msg' then inv else 0 := by
60-
calc
61-
Pr[= (msg, σ) | do
62-
let k ← $ᵗ BitVec sp
63-
return (msg', k ^^^ msg')] =
64-
Pr[= (msg, σ) | (msg', ·) <$> ((fun k : BitVec sp => k ^^^ msg') <$> ($ᵗ BitVec sp))] := by
65-
simp
66-
_ = if msg = msg' then
67-
Pr[= σ | (fun k : BitVec sp => k ^^^ msg') <$> ($ᵗ BitVec sp)] else 0 := by
68-
simpa using
69-
(probOutput_prod_mk_snd_map
70-
(my := (fun k : BitVec sp => k ^^^ msg') <$> ($ᵗ BitVec sp))
71-
(x := msg') (z := (msg, σ)))
72-
_ = if msg = msg' then inv else 0 := by
73-
by_cases h : msg = msg' <;> simp [h, inv, probOutput_xor_uniform]
74-
simp_rw [hinner]
75-
calc
76-
∑' msg', Pr[= msg' | mx] * (if msg = msg' then inv else 0) =
77-
∑' msg', (Pr[= msg' | mx] * (if msg = msg' then 1 else 0)) * inv := by
78-
refine tsum_congr fun msg' => ?_
79-
by_cases h : msg = msg' <;> simp [h, inv, mul_comm]
80-
_ = (∑' msg', Pr[= msg' | mx] * (if msg = msg' then 1 else 0)) * inv := by
81-
rw [ENNReal.tsum_mul_right]
82-
_ = Pr[= msg | mx] * inv := by
83-
have hsum :
84-
∑' msg', Pr[= msg' | mx] * (if msg = msg' then 1 else 0) =
85-
Pr[= msg | mx] := by
86-
simp
87-
rw [hsum]
88-
89-
lemma probOutput_cipher_from_pair_uniform (sp : ℕ) (mx : ProbComp (BitVec sp))
90-
(σ : BitVec sp) :
91-
Pr[= σ | do
92-
let msg' ← mx
93-
let k ← $ᵗ BitVec sp
94-
return (k ^^^ msg')] =
95-
(Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := by
96-
rw [probOutput_bind_of_const (mx := mx)
97-
(y := σ) (r := (Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹)]
98-
· simp
99-
· intro msg hmsg
100-
simpa using probOutput_xor_uniform sp msg σ
101-
10235
lemma probOutput_cipher_uniform (sp : ℕ)
10336
(mgen : OracleComp oneTimePad.spec (BitVec sp)) (σ : BitVec sp) :
10437
Pr[= σ | oneTimePad.PerfectSecrecyCipherExp sp mgen] =

‎ToMathlib/Data/ENNReal/SumSquares.lean‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
/-
2+
Copyright (c) 2026 Quang Dao. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Quang Dao
5+
-/
6+
import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
7+
8+
/-!
9+
# Sum-of-squares inequalities for `ℝ≥0∞`
10+
11+
Cauchy-Schwarz-style inequalities relating sums, products, and squares over `ℝ≥0∞`.
12+
These are used in the forking lemma and other game-hopping arguments.
13+
-/
14+
15+
open Finset ENNReal
16+
17+
namespace ENNReal
18+
19+
lemma two_mul_le_add_sq (a b : ℝ≥0∞) :
20+
2 * a * b ≤ a ^ 2 + b ^ 2 := by
21+
rcases eq_or_ne a ⊤ with rfl | ha
22+
· simp [top_pow, top_add, le_top]
23+
rcases eq_or_ne b ⊤ with rfl | hb
24+
· simp [top_pow, add_top, le_top]
25+
rw [← ENNReal.coe_toNNReal ha, ← ENNReal.coe_toNNReal hb]
26+
exact_mod_cast _root_.two_mul_le_add_sq a.toNNReal b.toNNReal
27+
28+
lemma sq_sum_le_card_mul_sum_sq {ι' : Type*}
29+
(s : Finset ι') (f : ι' → ℝ≥0∞) :
30+
(∑ i ∈ s, f i) ^ 2 ≤ s.card * ∑ i ∈ s, f i ^ 2 := by
31+
rw [sq, Finset.sum_mul_sum]
32+
suffices h : 2 * ∑ i ∈ s, ∑ j ∈ s, f i * f j ≤ 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) by
33+
have h2 : (2 : ℝ≥0∞) ≠ 0 := by norm_num
34+
have h2' : (2 : ℝ≥0∞) ≠ ⊤ := by norm_num
35+
calc ∑ i ∈ s, ∑ j ∈ s, f i * f j
36+
_ = 2⁻¹ * (2 * ∑ i ∈ s, ∑ j ∈ s, f i * f j) := by
37+
rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
38+
_ ≤ 2⁻¹ * (2 * (↑s.card * ∑ i ∈ s, f i ^ 2)) := by gcongr
39+
_ = ↑s.card * ∑ i ∈ s, f i ^ 2 := by
40+
rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
41+
calc 2 * ∑ i ∈ s, ∑ j ∈ s, f i * f j
42+
_ = ∑ i ∈ s, ∑ j ∈ s, 2 * (f i * f j) := by
43+
rw [Finset.mul_sum]; congr 1; ext i; rw [Finset.mul_sum]
44+
_ ≤ ∑ i ∈ s, ∑ j ∈ s, (f i ^ 2 + f j ^ 2) := by
45+
gcongr with i _ j _
46+
calc 2 * (f i * f j) = 2 * f i * f j := (mul_assoc ..).symm
47+
_ ≤ f i ^ 2 + f j ^ 2 := ENNReal.two_mul_le_add_sq (f i) (f j)
48+
_ = ∑ i ∈ s, (↑s.card * f i ^ 2 + ∑ j ∈ s, f j ^ 2) := by
49+
congr 1; ext i
50+
rw [Finset.sum_add_distrib, Finset.sum_const, nsmul_eq_mul]
51+
_ = ↑s.card * ∑ i ∈ s, f i ^ 2 + ↑s.card * ∑ i ∈ s, f i ^ 2 := by
52+
rw [Finset.sum_add_distrib, Finset.mul_sum, Finset.sum_const, nsmul_eq_mul,
53+
Finset.mul_sum]
54+
_ = 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) := by rw [← two_mul]
55+
56+
end ENNReal

‎VCVio/CryptoFoundations/Fork.lean‎

Lines changed: 16 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import VCVio.CryptoFoundations.SecExp
77
import VCVio.OracleComp.QueryTracking.SeededOracle
88
import VCVio.OracleComp.QueryTracking.LoggingOracle
99
import VCVio.OracleComp.Coercions.Add
10+
import ToMathlib.Data.ENNReal.SumSquares
1011

1112
/-!
1213
# Forking Lemma
@@ -26,45 +27,6 @@ then re-samples one oracle response, bounding the probability that both runs suc
2627

2728
open OracleSpec OracleComp ENNReal Function Finset
2829

29-
/-! ### ENNReal Cauchy-Schwarz inequality -/
30-
31-
private lemma ENNReal.two_mul_le_add_sq (a b : ℝ≥0∞) :
32-
2 * a * b ≤ a ^ 2 + b ^ 2 := by
33-
rcases eq_or_ne a ⊤ with rfl | ha
34-
· simp [top_pow, top_add, le_top]
35-
rcases eq_or_ne b ⊤ with rfl | hb
36-
· simp [top_pow, add_top, le_top]
37-
rw [← ENNReal.coe_toNNReal ha, ← ENNReal.coe_toNNReal hb]
38-
exact_mod_cast _root_.two_mul_le_add_sq a.toNNReal b.toNNReal
39-
40-
private lemma ENNReal.sq_sum_le_card_mul_sum_sq {ι' : Type*}
41-
(s : Finset ι') (f : ι' → ℝ≥0∞) :
42-
(∑ i ∈ s, f i) ^ 2 ≤ s.card * ∑ i ∈ s, f i ^ 2 := by
43-
rw [sq, Finset.sum_mul_sum]
44-
suffices h : 2 * ∑ i ∈ s, ∑ j ∈ s, f i * f j ≤ 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) by
45-
have h2 : (2 : ℝ≥0∞) ≠ 0 := by norm_num
46-
have h2' : (2 : ℝ≥0∞) ≠ ⊤ := by norm_num
47-
calc ∑ i ∈ s, ∑ j ∈ s, f i * f j
48-
_ = 2⁻¹ * (2 * ∑ i ∈ s, ∑ j ∈ s, f i * f j) := by
49-
rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
50-
_ ≤ 2⁻¹ * (2 * (↑s.card * ∑ i ∈ s, f i ^ 2)) := by gcongr
51-
_ = ↑s.card * ∑ i ∈ s, f i ^ 2 := by
52-
rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
53-
calc 2 * ∑ i ∈ s, ∑ j ∈ s, f i * f j
54-
_ = ∑ i ∈ s, ∑ j ∈ s, 2 * (f i * f j) := by
55-
rw [Finset.mul_sum]; congr 1; ext i; rw [Finset.mul_sum]
56-
_ ≤ ∑ i ∈ s, ∑ j ∈ s, (f i ^ 2 + f j ^ 2) := by
57-
gcongr with i _ j _
58-
calc 2 * (f i * f j) = 2 * f i * f j := (mul_assoc ..).symm
59-
_ ≤ f i ^ 2 + f j ^ 2 := ENNReal.two_mul_le_add_sq (f i) (f j)
60-
_ = ∑ i ∈ s, (↑s.card * f i ^ 2 + ∑ j ∈ s, f j ^ 2) := by
61-
congr 1; ext i
62-
rw [Finset.sum_add_distrib, Finset.sum_const, nsmul_eq_mul]
63-
_ = ↑s.card * ∑ i ∈ s, f i ^ 2 + ↑s.card * ∑ i ∈ s, f i ^ 2 := by
64-
rw [Finset.sum_add_distrib, Finset.mul_sum, Finset.sum_const, nsmul_eq_mul,
65-
Finset.mul_sum]
66-
_ = 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) := by rw [← two_mul]
67-
6830
namespace OracleComp
6931

7032
variable {ι : Type} [DecidableEq ι] {spec : OracleSpec ι}
@@ -146,7 +108,7 @@ private lemma probEvent_fork_fst_eq_probEvent_pair (s : Fin (qb i + 1)) :
146108
x₁ x₂ hmem with ⟨t, h₁, h₂⟩
147109
simp [h₁, h₂]
148110

149-
omit [DecidableEq ι] [spec.DecidableEq] in
111+
omit [spec.DecidableEq] in
150112
private lemma probEvent_uniform_eq_seedSlot_le_inv (s : Fin (qb i + 1))
151113
(seed : QuerySeed spec) :
152114
let h : ℝ≥0∞ := ↑(Fintype.card (spec.Range i))
@@ -156,44 +118,27 @@ private lemma probEvent_uniform_eq_seedSlot_le_inv (s : Fin (qb i + 1))
156118
· simp [hnone]
157119
· rcases Option.ne_none_iff_exists'.mp hnone with ⟨u₀, hu₀⟩
158120
rw [hu₀]
159-
calc
160-
Pr[fun u : spec.Range i => (some u₀ : Option (spec.Range i)) = some u |
161-
liftComp ($ᵗ spec.Range i) spec]
162-
= Pr[fun u : spec.Range i => u₀ = u | liftComp ($ᵗ spec.Range i) spec] := by simp
163-
_ = (↑(Fintype.card (spec.Range i)) : ℝ≥0∞)⁻¹ := by
164-
rw [probEvent_eq_eq_probOutput']
165-
have hLift :
166-
Pr[= u₀ | liftComp (($ᵗ spec.Range i : ProbComp (spec.Range i))) spec] =
167-
Pr[= u₀ | ($ᵗ spec.Range i : ProbComp (spec.Range i))] := by
168-
simpa using
169-
(probOutput_liftComp (spec := unifSpec) (superSpec := spec)
170-
(mx := ($ᵗ spec.Range i : ProbComp (spec.Range i))) (x := u₀))
171-
rw [hLift]
172-
simp [probOutput_uniformSample]
173-
_ ≤ (↑(Fintype.card (spec.Range i)) : ℝ≥0∞)⁻¹ := le_rfl
174-
175-
omit [DecidableEq ι] [spec.DecidableEq] in
121+
have : Pr[fun u : spec.Range i => (some u₀ : Option (spec.Range i)) = some u |
122+
liftComp ($ᵗ spec.Range i) spec] =
123+
Pr[fun u : spec.Range i => u₀ = u | liftComp ($ᵗ spec.Range i) spec] := by
124+
congr 1; ext; simp
125+
rw [this]
126+
exact le_of_eq (seededOracle.probEvent_liftComp_uniformSample_eq_of_eq u₀)
127+
128+
omit [spec.DecidableEq] in
176129
private lemma probEvent_uniform_eq_seedSlot_eq_inv_of_get (s : Fin (qb i + 1))
177130
(seed : QuerySeed spec) {u₀ : spec.Range i}
178131
(hu₀ : (seed i)[↑s]? = some u₀) :
179132
let h : ℝ≥0∞ := ↑(Fintype.card (spec.Range i))
180133
Pr[fun u : spec.Range i => (seed i)[↑s]? = some u | liftComp ($ᵗ spec.Range i) spec] = h⁻¹ := by
181134
simp only
182135
rw [hu₀]
183-
calc
184-
Pr[fun u : spec.Range i => (some u₀ : Option (spec.Range i)) = some u |
185-
liftComp ($ᵗ spec.Range i) spec]
186-
= Pr[fun u : spec.Range i => u₀ = u | liftComp ($ᵗ spec.Range i) spec] := by simp
187-
_ = (↑(Fintype.card (spec.Range i)) : ℝ≥0∞)⁻¹ := by
188-
rw [probEvent_eq_eq_probOutput']
189-
have hLift :
190-
Pr[= u₀ | liftComp (($ᵗ spec.Range i : ProbComp (spec.Range i))) spec] =
191-
Pr[= u₀ | ($ᵗ spec.Range i : ProbComp (spec.Range i))] := by
192-
simpa using
193-
(probOutput_liftComp (spec := unifSpec) (superSpec := spec)
194-
(mx := ($ᵗ spec.Range i : ProbComp (spec.Range i))) (x := u₀))
195-
rw [hLift]
196-
simp [probOutput_uniformSample]
136+
have : Pr[fun u : spec.Range i => (some u₀ : Option (spec.Range i)) = some u |
137+
liftComp ($ᵗ spec.Range i) spec] =
138+
Pr[fun u : spec.Range i => u₀ = u | liftComp ($ᵗ spec.Range i) spec] := by
139+
congr 1; ext; simp
140+
rw [this]
141+
exact seededOracle.probEvent_liftComp_uniformSample_eq_of_eq u₀
197142

198143
private lemma probOutput_collision_given_seed_le (s : Fin (qb i + 1))
199144
(seed : QuerySeed spec) :

0 commit comments

Comments
 (0)