Verified-zkEVM · quangvdao · Mar 1, 2026 · Feb 28, 2026 · Mar 1, 2026 · Mar 1, 2026
diff --git a/Examples/OneTimePad.lean b/Examples/OneTimePad.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SymmEncAlg
 import VCVio.OracleComp.Constructions.BitVec

diff --git a/ToMathlib/Data/ENNReal/SumSquares.lean b/ToMathlib/Data/ENNReal/SumSquares.lean
@@ -53,4 +53,48 @@ lemma sq_sum_le_card_mul_sum_sq {ι' : Type*}
           Finset.mul_sum]
     _ = 2 * (↑s.card * ∑ i ∈ s, f i ^ 2) := by rw [← two_mul]
 
+private lemma tsum_mul_tsum_eq {α : Type*} (g h : α → ℝ≥0∞) :
+    (∑' a, g a) * (∑' b, h b) = ∑' a, ∑' b, g a * h b := by
+  rw [← ENNReal.tsum_mul_right]; congr 1; ext a
+  exact ENNReal.tsum_mul_left.symm
+
+lemma sq_tsum_le_tsum_mul_tsum {α : Type*} (w f : α → ℝ≥0∞) :
+    (∑' a, w a * f a) ^ 2 ≤ (∑' a, w a) * ∑' a, w a * f a ^ 2 := by
+  rw [sq, tsum_mul_tsum_eq, tsum_mul_tsum_eq]
+  have h2 : (2 : ℝ≥0∞) ≠ 0 := two_ne_zero
+  have h2' : (2 : ℝ≥0∞) ≠ ⊤ := by norm_num
+  suffices h : 2 * ∑' a, ∑' b, (w a * f a) * (w b * f b) ≤
+      2 * ∑' a, ∑' b, w a * (w b * f b ^ 2) by
+    calc ∑' a, ∑' b, (w a * f a) * (w b * f b)
+      _ = 2⁻¹ * (2 * ∑' a, ∑' b, (w a * f a) * (w b * f b)) := by
+          rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
+      _ ≤ 2⁻¹ * (2 * ∑' a, ∑' b, w a * (w b * f b ^ 2)) := by gcongr
+      _ = ∑' a, ∑' b, w a * (w b * f b ^ 2) := by
+          rw [← mul_assoc, ENNReal.inv_mul_cancel h2 h2', one_mul]
+  calc 2 * ∑' a, ∑' b, (w a * f a) * (w b * f b)
+    _ = ∑' a, ∑' b, 2 * ((w a * f a) * (w b * f b)) := by
+        rw [← ENNReal.tsum_mul_left]; congr 1; ext
+        rw [← ENNReal.tsum_mul_left]
+    _ ≤ ∑' a, ∑' b, (w a * (w b * f b ^ 2) + w b * (w a * f a ^ 2)) := by
+        gcongr with a b
+        calc 2 * ((w a * f a) * (w b * f b))
+          _ = w a * w b * (2 * f a * f b) := by ring
+          _ ≤ w a * w b * (f a ^ 2 + f b ^ 2) := by
+              gcongr; exact two_mul_le_add_sq (f a) (f b)
+          _ = w a * (w b * f b ^ 2) + w b * (w a * f a ^ 2) := by ring
+    _ = (∑' a, ∑' b, w a * (w b * f b ^ 2)) +
+          ∑' a, ∑' b, w b * (w a * f a ^ 2) := by
+        simp_rw [← ENNReal.tsum_add]
+    _ = (∑' a, ∑' b, w a * (w b * f b ^ 2)) +
+          ∑' b, ∑' a, w b * (w a * f a ^ 2) := by
+        congr 1; exact ENNReal.tsum_comm
+    _ = 2 * ∑' a, ∑' b, w a * (w b * f b ^ 2) := by rw [two_mul]
+
+lemma sq_tsum_le_tsum_sq {α : Type*} (w f : α → ℝ≥0∞) (hw : ∑' a, w a ≤ 1) :
+    (∑' a, w a * f a) ^ 2 ≤ ∑' a, w a * f a ^ 2 :=
+  calc (∑' a, w a * f a) ^ 2
+    _ ≤ (∑' a, w a) * ∑' a, w a * f a ^ 2 := sq_tsum_le_tsum_mul_tsum w f
+    _ ≤ 1 * ∑' a, w a * f a ^ 2 := by gcongr
+    _ = ∑' a, w a * f a ^ 2 := one_mul _
+
 end ENNReal
diff --git a/VCVio/CryptoFoundations/AsymmEncAlg.lean b/VCVio/CryptoFoundations/AsymmEncAlg.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.ProbComp

diff --git a/VCVio/CryptoFoundations/FiatShamir.lean b/VCVio/CryptoFoundations/FiatShamir.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SigmaAlg
 import VCVio.CryptoFoundations.SignatureAlg
@@ -52,7 +52,21 @@ def FiatShamir (sigmaAlg : SigmaAlg X W PC SC Ω P p)
       (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp)
     StateT.run' (simulateQ (idImpl + ro) comp) ∅
   lift_probComp := monadLift
-  exec_lift_probComp c := by sorry
+  exec_lift_probComp c := by
+    let ro : QueryImpl (M × PC →ₒ Ω)
+      (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp) := randomOracle
+    let idImpl := (QueryImpl.ofLift unifSpec ProbComp).liftTarget
+      (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp)
+    change StateT.run' (simulateQ (idImpl + ro) (monadLift c)) ∅ = c
+    rw [show simulateQ (idImpl + ro) (monadLift c) = simulateQ idImpl c by
+      simpa [MonadLift.monadLift] using
+        (QueryImpl.simulateQ_add_liftComp_left (impl₁' := idImpl) (impl₂' := ro) c)]
+    have hid : ∀ t s, (idImpl t).run' s = query t := by
+      intro t s
+      rfl
+    simpa using
+      (StateT_run'_simulateQ_eq_self (so := idImpl) (h := hid) (oa := c)
+        (s := (∅ : (M × PC →ₒ Ω).QueryCache)))
 
 namespace FiatShamir
 

diff --git a/VCVio/CryptoFoundations/Fork.lean b/VCVio/CryptoFoundations/Fork.lean
diff --git a/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean b/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.HardnessAssumptions.HardHomogeneousSpace
 

diff --git a/VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean b/VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.ProbComp

diff --git a/VCVio/CryptoFoundations/SecExp.lean b/VCVio/CryptoFoundations/SecExp.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.ExecutionMethod
 import VCVio.OracleComp.ProbComp

diff --git a/VCVio/CryptoFoundations/SignatureAlg.lean b/VCVio/CryptoFoundations/SignatureAlg.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.OracleComp.ProbComp

diff --git a/VCVio/CryptoFoundations/SymmEncAlg.lean b/VCVio/CryptoFoundations/SymmEncAlg.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.CryptoFoundations.SecExp
 import VCVio.EvalDist.Prod

diff --git a/VCVio/EvalDist/Defs/Basic.lean b/VCVio/EvalDist/Defs/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.Support
 

diff --git a/VCVio/EvalDist/Instances/OptionT.lean b/VCVio/EvalDist/Instances/OptionT.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import ToMathlib.Control.OptionT
 import VCVio.EvalDist.Option

diff --git a/VCVio/EvalDist/List.lean b/VCVio/EvalDist/List.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.NeverFails
 import ToMathlib.General

diff --git a/VCVio/EvalDist/Monad/Basic.lean b/VCVio/EvalDist/Monad/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.Basic
 

diff --git a/VCVio/EvalDist/Monad/Seq.lean b/VCVio/EvalDist/Monad/Seq.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Monad.Map
 

diff --git a/VCVio/OracleComp/Coercions/Add.lean b/VCVio/OracleComp/Coercions/Add.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.Coercions.SubSpec
 import VCVio.OracleComp.ProbComp

diff --git a/VCVio/OracleComp/Coercions/SubSpec.lean b/VCVio/OracleComp/Coercions/SubSpec.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.SimulateQ
 import VCVio.OracleComp.EvalDist

diff --git a/VCVio/OracleComp/Constructions/GenerateSeed.lean b/VCVio/OracleComp/Constructions/GenerateSeed.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.Constructions.Replicate
 import VCVio.OracleComp.Constructions.SampleableType

diff --git a/VCVio/OracleComp/Constructions/SampleableType.lean b/VCVio/OracleComp/Constructions/SampleableType.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.ProbComp
 import VCVio.EvalDist.BitVec

diff --git a/VCVio/OracleComp/EvalDist.lean b/VCVio/OracleComp/EvalDist.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.EvalDist.Defs.NeverFails
 import VCVio.EvalDist.Instances.OptionT

diff --git a/VCVio/OracleComp/OracleComp.lean b/VCVio/OracleComp/OracleComp.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.OracleQuery
 import ToMathlib.PFunctor.Free

diff --git a/VCVio/OracleComp/ProbComp.lean b/VCVio/OracleComp/ProbComp.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.EvalDist
 import Batteries.Control.OptionT

diff --git a/VCVio/OracleComp/QueryTracking/CachingOracle.lean b/VCVio/OracleComp/QueryTracking/CachingOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.QueryTracking.Structures
 import VCVio.OracleComp.SimSemantics.Constructions

diff --git a/VCVio/OracleComp/QueryTracking/CountingOracle.lean b/VCVio/OracleComp/QueryTracking/CountingOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.QueryTracking.Structures
 import VCVio.OracleComp.SimSemantics.WriterT

diff --git a/VCVio/OracleComp/QueryTracking/LoggingOracle.lean b/VCVio/OracleComp/QueryTracking/LoggingOracle.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma
+Authors: Devon Tuma, Quang Dao
 -/
 import VCVio.OracleComp.SimSemantics.WriterT
 import VCVio.OracleComp.SimSemantics.Constructions