chore: add Quang Dao to author headers across 24 files

quangvdao · quangvdao · commit 25b8aef1d550 · 2026-02-28T16:30:00.000-08:00
Add co-authorship credit for substantial contributions across
OracleComp, EvalDist, CryptoFoundations, and Examples modules.

Made-with: Cursor
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/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/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
diff --git a/VCVio/OracleComp/SimSemantics/Constructions.lean b/VCVio/OracleComp/SimSemantics/Constructions.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.Constructions.SampleableType
diff --git a/VCVio/OracleComp/SimSemantics/SimulateQ.lean b/VCVio/OracleComp/SimSemantics/SimulateQ.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.QueryImpl
 import ToMathlib.Control.OptionT
