cleanup legacy comments and restore CountingOracle support lemmas

Author: quangvdao

VCVio/CryptoFoundations/AsymmEncAlg.lean

@@ -53,16 +53,6 @@ def CorrectExp (msg : M) : m Bool := do
 def PerfectlyCorrect [HasEvalSPMF m] : Prop :=
   ∀ (msg : M), Pr[= true | encAlg.exec (encAlg.CorrectExp msg)] = 1
 
--- Old definitions (used `guard` + `AlternativeMonad`, which is now `OptionT`):
--- @[reducible, inline]
--- def CorrectExp (encAlg : AsymmEncAlg m M PK SK C) (msg : M) :
---     ProbComp Unit := encAlg.exec do
---   let (pk, sk) ← encAlg.keygen
---   guard (encAlg.decrypt sk (← encAlg.encrypt pk msg) = msg)
---
--- def PerfectlyCorrect (encAlg : AsymmEncAlg m M PK SK C) : Prop :=
---   ∀ (msg : M), [⊥ | CorrectExp encAlg msg] = 0
-
 end Correct
 
 section IND_CPA_Oracle
@@ -112,25 +102,6 @@ noncomputable def IND_CPA_advantage {encAlg : AsymmEncAlg ProbComp M PK SK C}
     (adversary : encAlg.IND_CPA_adversary) : ℝ≥0∞ :=
   Pr[= true | IND_CPA_experiment adversary] - 1 / 2
 
--- Old lemma (uses guard-based experiment, needs rework for Bool-valued version):
--- /-- The probability of the IND-CPA experiment is the average of the probability of the experiment
--- with the challenge being true and the probability of the experiment with the challenge being false. -/
--- lemma probOutput_IND_CPA_experiment_eq_add {encAlg : AsymmEncAlg ProbComp M PK SK C}
---     (adversary : encAlg.IND_CPA_adversary) :
---     [= () | IND_CPA_experiment adversary] =
---       [= () | do
---         let (pk, _sk) ← encAlg.keygen
---         let b ← (simulateQ (encAlg.IND_CPA_queryImpl' pk true) (adversary pk)).run' ∅
---         guard b] / 2 +
---       [= () | do
---         let (pk, _sk) ← encAlg.keygen
---         let b ← (simulateQ (encAlg.IND_CPA_queryImpl' pk false) (adversary pk)).run' ∅
---         guard ¬b] / 2 := by
---   unfold IND_CPA_experiment
---   rw [probOutput_bind_eq_sum_finSupport]
---   have {x : ℝ≥0∞} : 2⁻¹ * x = x / 2 := by field_simp; rw [mul_comm, mul_div, mul_one]
---   simp [this]
-
 end IND_CPA_Oracle
 
 section decryptionOracle

VCVio/CryptoFoundations/HardnessAssumptions/LWE.lean

@@ -92,17 +92,3 @@ noncomputable def SearchAdvantage (n m p : ℕ) [NeZero p] (errSamp : ProbComp (
   (SearchExperiment n m p errSamp adv).advantage'
 
 end LWE
-
-/-! ## Old commented code (for reference)
-
--- variable (n m p : ℕ) [NeZero p] (errSamp : ProbComp (Fin p))
-
--- def LWE_Distr : ProbComp (Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m) := do
---   let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
---   let s ←$ᵗ Vector (Fin p) n
---   let e ← (Vector.Range m).mapM (fun _ ↦ errSamp)
---   let u := A.vecMul s.get + e.get
---   return (A, Vector.ofFn u)
-
--- (... rest of old LWE code preserved in git history ...)
--/

VCVio/OracleComp/OracleComp.lean

@@ -195,11 +195,6 @@ def isPure {α : Type _} : OracleComp spec α → Bool
 @[simp] lemma pure_ne_query : (pure u : OracleComp spec _) ≠ query t := by simp [query_def]
 @[simp] lemma query_ne_pure : (query t : OracleComp spec _) ≠ pure u := by simp [query_def]
 
--- @[simp] lemma pure_ne_query_bind : pure x ≠ (query t : OracleComp spec _) >>= ou := fun h => by
---   simp [query_def, OracleComp.bind_def] at h
--- @[simp] lemma query_bind_ne_pure : (query t : OracleComp spec _) >>= ou ≠ pure x := fun h => by
---   simp [query_def, OracleComp.bind_def] at h
-
 lemma pure_eq_query_iff_false : pure u = (query t : OracleComp spec _) ↔ False := by simp
 lemma query_eq_pure_iff_false : (query t : OracleComp spec _) = pure u ↔ False := by simp
 
@@ -224,14 +219,6 @@ section inj
 @[simp] lemma pure_inj (x y : α) : pure (f := OracleComp spec) x = pure y ↔ x = y :=
   PFunctor.FreeM.pure_inj x y
 
--- /-- Doing something with a query result is equal iff they query the same oracle
--- and perform identical computations on the output. -/
--- @[simp] lemma queryBind_inj (t t' : spec.Domain) (ob : spec.Range t → OracleComp spec β)
---     (ob' : spec.Range t' → OracleComp spec β) :
---     (query t : OracleComp spec _) >>= ob = (query t' : OracleComp spec _) >>= ob' ↔
---       ∃ h : t = t', h ▸ ob = ob' := by
---   convert PFunctor.FreeM.roll_inj t t' ob ob'
-
 /-- Binding two computations gives a pure operation iff the first computation is pure
 and the second computation does something pure with the result. -/
 @[simp] lemma bind_eq_pure_iff (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) :
@@ -252,34 +239,4 @@ alias ⟨_, pure_eq_bind⟩ := pure_eq_bind_iff
 
 end inj
 
--- /-- If the oracle indexing-type `ι`, output type `α`, and domains of all oracles have
--- `DecidableEq` then `OracleComp spec α` also has `DecidableEq`. -/
--- protected instance instDecidableEq [spec.Fintype] [hd : DecidableEq (spec.Domain)]
---     [hι : DecidableEq ι] [h : DecidableEq α] : DecidableEq (OracleComp spec α) := fun
---   | _ => sorry
-  -- | FreeMonad.pure (Option.some x), FreeMonad.pure (Option.some y) =>
-  --   match h x y with
-  --   | isTrue rfl => isTrue rfl
-  --   | isFalse h => isFalse λ h' ↦ h (by rwa [FreeMonad.pure.injEq, Option.some_inj] at h')
-  -- | FreeMonad.pure Option.none, FreeMonad.pure (Option.some y) => isFalse λ h ↦
-  --     Option.some_ne_none y (by rwa [FreeMonad.pure.injEq, eq_comm] at h)
-  -- | FreeMonad.pure (Option.some x), FreeMonad.pure Option.none => isFalse λ h ↦
-  --     Option.some_ne_none x (by rwa [FreeMonad.pure.injEq] at h)
-  -- | FreeMonad.pure Option.none, FreeMonad.pure Option.none => isTrue rfl
-  -- | FreeMonad.pure x, FreeMonad.roll q r => isFalse <| by simp
-  -- | FreeMonad.roll q r, FreeMonad.pure x => isFalse <| by simp
-  -- | FreeMonad.roll (OracleQuery.query i t) r, FreeMonad.roll (OracleQuery.query i' t') s =>
-  --   match hι i i' with
-  --   | isTrue h => by
-  --       induction h
-  --    rw [FreeMonad.roll.injEq, heq_eq_eq, OracleQuery.query.injEq, eq_self, true_and, heq_eq_eq]
-  --       refine @instDecidableAnd _ _ (hd i t t') ?_
-  --       suffices Decidable (∀ u, r u = s u) from decidable_of_iff' _ funext_iff
-  --       suffices ∀ u, Decidable (r u = s u) from Fintype.decidableForallFintype
-  --       exact λ u ↦ OracleComp.instDecidableEq (r u) (s u)
-  --   | isFalse h => isFalse λ h' ↦ h <|
-  --       match FreeMonad.roll.inj h' with
-  --       | ⟨h1, h2, _⟩ => @congr_heq _ _ ι OracleQuery.index OracleQuery.index
-  --           (query i t) (query i' t') (h1 ▸ HEq.rfl) h2
-
 end OracleComp