Skip to content

Commit d826265

Browse files
quangvdaoquangvdao
committed
feat(Fork): complete forking lemma proof and seeded oracle infrastructure
Prove the full forking lemma (`le_probOutput_fork`, `probOutput_none_fork_le`) by establishing seeded oracle faithfulness, the addValue/takeAtIndex factorization lemmas, and a Cauchy-Schwarz bound for ENNReal tsum. Also adds QuerySeed operations (pop, prependValues, takeAtIndex) and the generateSeedCounts seed generator. Made-with: Cursor
1 parent df65d1a commit d826265

File tree

5 files changed

+861
-11
lines changed

5 files changed

+861
-11
lines changed

‎ToMathlib/Data/ENNReal/SumSquares.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,4 +53,48 @@ lemma sq_sum_le_card_mul_sum_sq {ι' : Type*}
5353
Finset.mul_sum]
5454
_ = 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) := by rw [← two_mul]
5555

56+
private lemma tsum_mul_tsum_eq {α : Type*} (g h : α → ℝ≥0∞) :
57+
(∑' a, g a) * (∑' b, h b) = ∑' a, ∑' b, g a * h b := by
58+
rw [← ENNReal.tsum_mul_right]; congr 1; ext a
59+
exact ENNReal.tsum_mul_left.symm
60+
61+
lemma sq_tsum_le_tsum_mul_tsum {α : Type*} (w f : α → ℝ≥0∞) :
62+
(∑' a, w a * f a) ^ 2 ≤ (∑' a, w a) * ∑' a, w a * f a ^ 2 := by
63+
rw [sq, tsum_mul_tsum_eq, tsum_mul_tsum_eq]
64+
have h2 : (2 : ℝ≥0∞) ≠ 0 := two_ne_zero
65+
have h2' : (2 : ℝ≥0∞) ≠ ⊤ := by norm_num
66+
suffices h : 2 * ∑' a, ∑' b, (w a * f a) * (w b * f b) ≤
67+
2 * ∑' a, ∑' b, w a * (w b * f b ^ 2) by
68+
calc ∑' a, ∑' b, (w a * f a) * (w b * f b)
69+
_ = 2⁻¹ * (2 * ∑' a, ∑' b, (w a * f a) * (w b * f b)) := by
70+
rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
71+
_ ≤ 2⁻¹ * (2 * ∑' a, ∑' b, w a * (w b * f b ^ 2)) := by gcongr
72+
_ = ∑' a, ∑' b, w a * (w b * f b ^ 2) := by
73+
rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
74+
calc 2 * ∑' a, ∑' b, (w a * f a) * (w b * f b)
75+
_ = ∑' a, ∑' b, 2 * ((w a * f a) * (w b * f b)) := by
76+
rw [← ENNReal.tsum_mul_left]; congr 1; ext
77+
rw [← ENNReal.tsum_mul_left]
78+
_ ≤ ∑' a, ∑' b, (w a * (w b * f b ^ 2) + w b * (w a * f a ^ 2)) := by
79+
gcongr with a b
80+
calc 2 * ((w a * f a) * (w b * f b))
81+
_ = w a * w b * (2 * f a * f b) := by ring
82+
_ ≤ w a * w b * (f a ^ 2 + f b ^ 2) := by
83+
gcongr; exact two_mul_le_add_sq (f a) (f b)
84+
_ = w a * (w b * f b ^ 2) + w b * (w a * f a ^ 2) := by ring
85+
_ = (∑' a, ∑' b, w a * (w b * f b ^ 2)) +
86+
∑' a, ∑' b, w b * (w a * f a ^ 2) := by
87+
simp_rw [← ENNReal.tsum_add]
88+
_ = (∑' a, ∑' b, w a * (w b * f b ^ 2)) +
89+
∑' b, ∑' a, w b * (w a * f a ^ 2) := by
90+
congr 1; exact ENNReal.tsum_comm
91+
_ = 2 * ∑' a, ∑' b, w a * (w b * f b ^ 2) := by rw [two_mul]
92+
93+
lemma sq_tsum_le_tsum_sq {α : Type*} (w f : α → ℝ≥0∞) (hw : ∑' a, w a ≤ 1) :
94+
(∑' a, w a * f a) ^ 2 ≤ ∑' a, w a * f a ^ 2 :=
95+
calc (∑' a, w a * f a) ^ 2
96+
_ ≤ (∑' a, w a) * ∑' a, w a * f a ^ 2 := sq_tsum_le_tsum_mul_tsum w f
97+
_ ≤ 1 * ∑' a, w a * f a ^ 2 := by gcongr
98+
_ = ∑' a, w a * f a ^ 2 := one_mul _
99+
56100
end ENNReal

‎VCVio/CryptoFoundations/FiatShamir.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/-
22
Copyright (c) 2024 Devon Tuma. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Devon Tuma
4+
Authors: Devon Tuma, Quang Dao
55
-/
66
import VCVio.CryptoFoundations.SigmaAlg
77
import VCVio.CryptoFoundations.SignatureAlg

‎VCVio/CryptoFoundations/Fork.lean‎

Lines changed: 136 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/-
22
Copyright (c) 2024 Devon Tuma. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Devon Tuma
4+
Authors: Devon Tuma, Quang Dao
55
-/
66
import VCVio.CryptoFoundations.SecExp
77
import VCVio.OracleComp.QueryTracking.SeededOracle
@@ -261,7 +261,6 @@ private lemma probOutput_collision_le_main_div (s : Fin (qb i + 1)) :
261261
(qc := qb) (js := js) (oa := main) (f := cf)
262262
(y := (some s : Option (Fin (qb i + 1)))))
263263

264-
set_option maxHeartbeats 800000 in
265264
/-- Key bound of the forking lemma: the probability that both runs succeed with fork point `s`
266265
is at least `Pr[cf(main) = s]² - Pr[cf(main) = s] / |Range i|`. -/
267266
theorem le_probOutput_fork (s : Fin (qb i + 1)) :
@@ -402,8 +401,8 @@ theorem le_probOutput_fork (s : Fin (qb i + 1)) :
402401
let a_1 ← (simulateQ seededOracle main).run
403402
((seed.takeAtIndex i ↑s).addValue i u)
404403
if cf a_1.1 = some s then pure (some (a.1, a_1.1)) else pure none] + 1 := by
405-
simpa using (add_le_add_right hnonneg (1 : ℝ≥0∞))
406-
simpa [hu'] using haux
404+
simp
405+
simp [hu']
407406
exact le_trans h1 h2
408407
· have hmono :
409408
Pr[= z |
@@ -417,7 +416,7 @@ theorem le_probOutput_fork (s : Fin (qb i + 1)) :
417416
refine probOutput_bind_mono ?_
418417
intro x hx
419418
by_cases hxs : cf x.1 = some s
420-
· simpa [hxs, hca, z]
419+
· simp [hxs, hca, z]
421420
· have hrhs_nonneg :
422421
0 ≤ Pr[= z |
423422
(fun r ↦ Option.map (Prod.map cf cf) r) <$>
@@ -426,7 +425,7 @@ theorem le_probOutput_fork (s : Fin (qb i + 1)) :
426425
else pure none)] := zero_le _
427426
have hxs' : (some s : Option (Fin (qb i + 1))) ≠ cf x.1 := by
428427
simpa [eq_comm] using hxs
429-
simpa [hxs, hxs', z] using hrhs_nonneg
428+
simp [hxs, hxs', z]
430429
have hu'' : (seed i)[↑s]? ≠ some u := by simpa using hu'
431430
have hif :
432431
(if (seed i)[↑s]? = some u then
@@ -496,8 +495,137 @@ theorem le_probOutput_fork (s : Fin (qb i + 1)) :
496495
exact (tsub_le_iff_right).2 hNoGuardLeAdd
497496
have hNoGuardGeSquare :
498497
Pr[= s | cf <$> main] ^ 2 ≤ Pr[= z | noGuardComp] := by
499-
-- Remaining core: seed-factorization and weighted-square lower bound.
500-
sorry
498+
-- Step 1: Express Pr[= s | cf <$> main] as E_σ[P(σ)] via seeded oracle factorization
499+
have hMain : (Pr[= s | cf <$> main] : ℝ≥0∞) =
500+
∑' σ, Pr[= σ | generateSeed spec qb js] *
501+
Pr[= (some s : Option (Fin (qb i + 1))) |
502+
cf <$> (simulateQ seededOracle main).run' σ] := by
503+
rw [show (Pr[= s | cf <$> main] : ℝ≥0∞) =
504+
Pr[= (some s : Option (Fin (qb i + 1))) |
505+
(do let seed ← liftComp (generateSeed spec qb js) spec
506+
cf <$> (simulateQ seededOracle main).run' seed :
507+
OracleComp spec (Option (Fin (qb i + 1))))] from by
508+
simpa using (seededOracle.probOutput_generateSeed_bind_map_simulateQ
509+
(qc := qb) (js := js) (oa := main) (f := cf)
510+
(y := (some s : Option (Fin (qb i + 1))))).symm]
511+
rw [probOutput_bind_eq_tsum]
512+
simp_rw [probOutput_liftComp]
513+
-- Step 2: Factor Pr[= z | noGuardComp] = ∑' σ, w(σ) * P(σ) * P(take(σ))
514+
-- Uses conditional independence (probOutput_bind_bind_prod_mk_eq_mul')
515+
-- and the addValue factorization lemma.
516+
have hFactor : Pr[= z | noGuardComp] =
517+
∑' σ, Pr[= σ | generateSeed spec qb js] *
518+
(Pr[= (some s : Option (Fin (qb i + 1))) |
519+
cf <$> (simulateQ seededOracle main).run' σ] *
520+
Pr[= (some s : Option (Fin (qb i + 1))) |
521+
cf <$> (simulateQ seededOracle main).run'
522+
(σ.takeAtIndex i ↑s)]) := by
523+
simp only [noGuardComp, z]
524+
rw [probOutput_bind_eq_tsum]
525+
simp_rw [probOutput_liftComp]
526+
congr 1; ext σ; congr 1
527+
have hcomp : (do let x₁ ← (simulateQ seededOracle main).run' σ
528+
let u ← liftComp ($ᵗ spec.Range i) spec
529+
let x₂ ← (simulateQ seededOracle main).run'
530+
((σ.takeAtIndex i ↑s).addValue i u)
531+
pure (some (cf x₁, cf x₂)) : OracleComp spec _) =
532+
some <$> (do let x₁ ← (simulateQ seededOracle main).run' σ
533+
let x₂ ← (liftComp ($ᵗ spec.Range i) spec >>= fun u =>
534+
(simulateQ seededOracle main).run'
535+
((σ.takeAtIndex i ↑s).addValue i u))
536+
pure (cf x₁, cf x₂)) := by
537+
simp only [map_eq_bind_pure_comp, bind_assoc, Function.comp, pure_bind]
538+
rw [hcomp, probOutput_some_map_some, probOutput_bind_bind_prod_mk_eq_mul']
539+
congr 1
540+
have h := seededOracle.evalDist_liftComp_uniformSample_bind_simulateQ_run'_addValue
541+
(σ.takeAtIndex i ↑s) i main
542+
exact congrFun (congrArg DFunLike.coe (by simp only [evalDist_map, h])) (some s)
543+
-- Step 3: Jensen/Cauchy-Schwarz via prefix grouping
544+
-- (∑ w * P)² ≤ ∑ w * P * P(take) by decomposing into prefix groups
545+
-- and applying sq_tsum_le_tsum_sq.
546+
have hJensen :
547+
(∑' σ, Pr[= σ | generateSeed spec qb js] *
548+
Pr[= (some s : Option (Fin (qb i + 1))) |
549+
cf <$> (simulateQ seededOracle main).run' σ]) ^ 2 ≤
550+
∑' σ, Pr[= σ | generateSeed spec qb js] *
551+
(Pr[= (some s : Option (Fin (qb i + 1))) |
552+
cf <$> (simulateQ seededOracle main).run' σ] *
553+
Pr[= (some s : Option (Fin (qb i + 1))) |
554+
cf <$> (simulateQ seededOracle main).run'
555+
(σ.takeAtIndex i ↑s)]) := by
556+
-- Notation: w(σ) = Pr[=σ|gen], P(σ) = Pr[=y|run'(σ)], Q(σ) = Pr[=y|run'(take(σ))]
557+
-- hEq: ∑ w * P = ∑ w * Q (both equal Pr[= some s | cf <$> main])
558+
have hMainTake : ∑' σ, Pr[= σ | generateSeed spec qb js] *
559+
Pr[= (some s : Option (Fin (qb i + 1))) |
560+
cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)] =
561+
Pr[= (some s : Option (Fin (qb i + 1))) | cf <$> main] := by
562+
have hTake :=
563+
seededOracle.probOutput_generateSeed_bind_map_simulateQ_takeAtIndex
564+
(qc := qb) (js := js) (i₀ := i) (k := ↑s) (oa := main) (f := cf)
565+
(y := (some s : Option (Fin (qb i + 1))))
566+
rw [probOutput_bind_eq_tsum] at hTake
567+
simp_rw [probOutput_liftComp] at hTake
568+
exact hTake
569+
have hEq : ∑' σ, Pr[= σ | generateSeed spec qb js] *
570+
Pr[= (some s : Option (Fin (qb i + 1))) |
571+
cf <$> (simulateQ seededOracle main).run' σ] =
572+
∑' σ, Pr[= σ | generateSeed spec qb js] *
573+
Pr[= (some s : Option (Fin (qb i + 1))) |
574+
cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)] :=
575+
by
576+
calc
577+
∑' σ, Pr[= σ | generateSeed spec qb js] *
578+
Pr[= (some s : Option (Fin (qb i + 1))) |
579+
cf <$> (simulateQ seededOracle main).run' σ]
580+
= Pr[= (some s : Option (Fin (qb i + 1))) | cf <$> main] := by
581+
simpa using hMain.symm
582+
_ = ∑' σ, Pr[= σ | generateSeed spec qb js] *
583+
Pr[= (some s : Option (Fin (qb i + 1))) |
584+
cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)] := by
585+
simpa using hMainTake.symm
586+
-- Jensen: (∑ w * Q)² ≤ ∑ w * Q²
587+
set w : QuerySeed spec → ℝ≥0∞ := fun σ => Pr[= σ | generateSeed spec qb js]
588+
set Q : QuerySeed spec → ℝ≥0∞ := fun σ =>
589+
Pr[= (some s : Option (Fin (qb i + 1))) |
590+
cf <$> (simulateQ seededOracle main).run' (σ.takeAtIndex i ↑s)]
591+
have hw : ∑' σ, w σ ≤ 1 := tsum_probOutput_le_one
592+
-- hEq2: ∑ w * Q² = ∑ w * (P * Q) via weighted takeAtIndex faithfulness
593+
have hEq2 : ∑' σ, w σ * Q σ ^ 2 =
594+
∑' σ, w σ *
595+
(Pr[= (some s : Option (Fin (qb i + 1))) |
596+
cf <$> (simulateQ seededOracle main).run' σ] * Q σ) := by
597+
simp only [sq, Q, w]
598+
have hSim : ∀ σ', (simulateQ seededOracle (cf <$> main :
599+
OracleComp spec (Option (Fin (qb i + 1))))).run' σ' =
600+
cf <$> (simulateQ seededOracle main).run' σ' := by
601+
intro σ'
602+
simp only [simulateQ_map]
603+
show Prod.fst <$> (Prod.map cf id <$> (simulateQ seededOracle main).run σ') =
604+
cf <$> (Prod.fst <$> (simulateQ seededOracle main).run σ')
605+
simp [Functor.map_map]
606+
have hWF := seededOracle.tsum_probOutput_generateSeed_weight_takeAtIndex
607+
qb js i (↑s) (cf <$> main : OracleComp spec (Option (Fin (qb i + 1))))
608+
(some s : Option (Fin (qb i + 1)))
609+
(fun τ => Pr[= (some s : Option (Fin (qb i + 1))) |
610+
(simulateQ seededOracle (cf <$> main :
611+
OracleComp spec (Option (Fin (qb i + 1))))).run' τ])
612+
simp_rw [hSim] at hWF
613+
exact hWF.symm.trans (by congr 1; ext σ; congr 1; exact mul_comm _ _)
614+
calc _ = (∑' σ, w σ * Q σ) ^ 2 := by rw [hEq]
615+
_ ≤ ∑' σ, w σ * Q σ ^ 2 := ENNReal.sq_tsum_le_tsum_sq w Q hw
616+
_ = _ := hEq2
617+
calc Pr[= s | cf <$> main] ^ 2
618+
= (∑' σ, Pr[= σ | generateSeed spec qb js] *
619+
Pr[= (some s : Option (Fin (qb i + 1))) |
620+
cf <$> (simulateQ seededOracle main).run' σ]) ^ 2 := by
621+
rw [hMain]
622+
_ ≤ ∑' σ, Pr[= σ | generateSeed spec qb js] *
623+
(Pr[= (some s : Option (Fin (qb i + 1))) |
624+
cf <$> (simulateQ seededOracle main).run' σ] *
625+
Pr[= (some s : Option (Fin (qb i + 1))) |
626+
cf <$> (simulateQ seededOracle main).run'
627+
(σ.takeAtIndex i ↑s)]) := hJensen
628+
_ = Pr[= z | noGuardComp] := hFactor.symm
501629
exact le_trans
502630
(tsub_le_tsub_right hNoGuardGeSquare (Pr[= (some s : Option (Fin (qb i + 1))) | collisionComp]))
503631
hNoGuardMinusLeRhs

0 commit comments

Comments
 (0)