Ind cpa one time bias advantage compose with dem le

theorem ind_cpa_one_time_bias_advantage_compose_with_dem_le    (kem : KEMScheme (OracleComp spec) K PK SK CKEM)    (dem : DEMScheme (OracleComp spec) K M CDEM)    (runtime : ProbCompRuntime (OracleComp spec))    (adversary : AsymmEncAlg.IND_CPA_Adv (kem.composeWithDEM dem))    (heval_pure : ∀ {α : Type} (a : α),        runtime.evalDist (pure a : OracleComp spec α) = pure a)    (heval_bind : ∀ {α β : Type} (mx : OracleComp spec α)        (f : α → OracleComp spec β),        runtime.evalDist (mx >>= f) =        runtime.evalDist mx >>= fun a => runtime.evalDist (f a))    (heval_liftProbComp : ∀ {α : Type} (pc : ProbComp α),        runtime.evalDist (runtime.liftProbComp pc) = 𝒟[pc])    (hno_fail : ∀ (mx : OracleComp spec Bool),        Pr[= true | runtime.evalDist mx] +        Pr[= false | runtime.evalDist mx] = 1) :    AsymmEncAlg.IND_CPA_OneTime_biasAdvantage (kem.composeWithDEM dem) runtime adversary ≤      kem.IND_CPA_Advantage runtime (kem.composeWithDEM_toKEMLeftReduction dem adversary) +      kem.IND_CPA_Advantage runtime (kem.composeWithDEM_toKEMRightReduction dem adversary) +      dem.IND_CPA_Advantage runtime        (kem.composeWithDEM_toDEMReduction dem adversary) := by  let real_m₀ : SPMF Bool := runtime.evalDist do    let (pk, _) ← kem.keygen    let (m₀, _, st) ← adversary.chooseMessages pk    let (kc, k) ← kem.encaps pk    let dc ← dem.encrypt k m₀    adversary.distinguish st (kc, dc)  let rand_m₀ : SPMF Bool := runtime.evalDist do    let (pk, _) ← kem.keygen    let (m₀, _, st) ← adversary.chooseMessages pk    let (kc, _) ← kem.encaps pk    let kR ← runtime.liftProbComp ($ᵗ K)    let dc ← dem.encrypt kR m₀    adversary.distinguish st (kc, dc)  let rand_m₁ : SPMF Bool := runtime.evalDist do    let (pk, _) ← kem.keygen    let (_, m₁, st) ← adversary.chooseMessages pk    let (kc, _) ← kem.encaps pk    let kR ← runtime.liftProbComp ($ᵗ K)    let dc ← dem.encrypt kR m₁    adversary.distinguish st (kc, dc)  let real_m₁ : SPMF Bool := runtime.evalDist do    let (pk, _) ← kem.keygen    let (_, m₁, st) ← adversary.chooseMessages pk    let (kc, k) ← kem.encaps pk    let dc ← dem.encrypt k m₁    adversary.distinguish st (kc, dc)  have bind_swap : ∀ {α β γ : Type} (mx : SPMF α) (my : SPMF β) (f : α → β → SPMF γ),      (mx >>= fun a => my >>= fun b => f a b) =      (my >>= fun b => mx >>= fun a => f a b) := by    intro α β γ mx my f    ext x; exact probOutput_bind_bind_swap mx my (fun a b => f a b) x  have hite_false : (false : Bool) = true ↔ False := ⟨Bool.noConfusion, False.elim⟩  have hite_true : (true : Bool) = true ↔ True := ⟨fun _ => trivial, fun _ => rfl⟩  have coin_branch : ∀ X Y : SPMF Bool, Pr[= true | X] + Pr[= false | X] = 1 →      Pr[= true | Y] + Pr[= false | Y] = 1 →      (𝒟[$ᵗ Bool] >>= fun b =>          (if b then X else Y) >>= fun z => pure (b == z)).boolBiasAdvantage =        SPMF.boolDistAdvantage X Y := fun X Y hX hY =>    SPMF.boolBiasAdvantage_eq_boolDistAdvantage_coin_branch (𝒟[$ᵗ Bool]) X Y      (by simp [Fintype.card_bool]) (by simp [Fintype.card_bool]) hX hY  have h_composed : AsymmEncAlg.IND_CPA_OneTime_biasAdvantage      (kem.composeWithDEM dem) runtime adversary =      SPMF.boolDistAdvantage real_m₀ real_m₁ := by    have hspmf : AsymmEncAlg.IND_CPA_OneTime_Game (encAlg := kem.composeWithDEM dem)        adversary runtime =        𝒟[$ᵗ Bool] >>= fun b =>          (if b then real_m₀ else real_m₁) >>= fun z => pure (b == z) := by      simp only [AsymmEncAlg.IND_CPA_OneTime_Game, KEMScheme.composeWithDEM,        heval_bind, heval_liftProbComp]      congr 1; funext b      simp only [heval_pure]      cases b      · simp only [hite_false, ite_false, bind_assoc, pure_bind]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (_, m₁, st) ← adversary.chooseMessages pk          let (kc, k) ← kem.encaps pk; let dc ← dem.encrypt k m₁          adversary.distinguish st (kc, dc)) >>= fun a => pure (false == a)        simp only [heval_bind, bind_assoc]      · simp only [ite_true, bind_assoc, pure_bind]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (m₀, _, st) ← adversary.chooseMessages pk          let (kc, k) ← kem.encaps pk; let dc ← dem.encrypt k m₀          adversary.distinguish st (kc, dc)) >>= fun a => pure (true == a)        simp only [heval_bind, bind_assoc]    change (AsymmEncAlg.IND_CPA_OneTime_Game (encAlg := kem.composeWithDEM dem) adversary        runtime).boolBiasAdvantage = _    rw [hspmf, coin_branch _ _ (hno_fail _) (hno_fail _)]  have h_kem_left : kem.IND_CPA_Advantage runtime      (kem.composeWithDEM_toKEMLeftReduction dem adversary) =      SPMF.boolDistAdvantage real_m₀ rand_m₀ := by    have hspmf : KEMScheme.IND_CPA_Game runtime        (kem.composeWithDEM_toKEMLeftReduction dem adversary) =        𝒟[$ᵗ Bool] >>= fun b =>          (if b then real_m₀ else rand_m₀) >>= fun z => pure (b == z) := by      simp only [KEMScheme.IND_CPA_Game, composeWithDEM_toKEMLeftReduction,        heval_bind, heval_pure, heval_liftProbComp]      simp_rw [bind_swap (my := 𝒟[$ᵗ Bool])]      congr 1; funext b      conv_lhs => simp only [bind_assoc, pure_bind]      cases b      · simp only [hite_false, ite_false]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (m₀, _, st) ← adversary.chooseMessages pk          let (kc, _) ← kem.encaps pk; let kR ← runtime.liftProbComp ($ᵗ K)          let dc ← dem.encrypt kR m₀; adversary.distinguish st (kc, dc)) >>= fun z =>          pure (false == z)        simp only [heval_bind, heval_liftProbComp, bind_assoc]      · simp only [ite_true]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (m₀, _, st) ← adversary.chooseMessages pk          let (kc, k) ← kem.encaps pk          let dc ← dem.encrypt k m₀; adversary.distinguish st (kc, dc)) >>= fun z =>          pure (true == z)        simp only [heval_bind, bind_assoc]        congr 1; funext pksk; congr 1; funext cms; congr 1; funext ckr        exact OracleComp.ProgramLogic.Relational.spmf_bind_const_of_no_failure          (OracleComp.ProgramLogic.Relational.probFailure_evalDist_eq_zero _) _    change (KEMScheme.IND_CPA_Game runtime _).boolBiasAdvantage = _    rw [hspmf, coin_branch _ _ (hno_fail _) (hno_fail _)]  have h_kem_right : kem.IND_CPA_Advantage runtime      (kem.composeWithDEM_toKEMRightReduction dem adversary) =      SPMF.boolDistAdvantage real_m₁ rand_m₁ := by    have hspmf : KEMScheme.IND_CPA_Game runtime        (kem.composeWithDEM_toKEMRightReduction dem adversary) =        𝒟[$ᵗ Bool] >>= fun b =>          (if b then real_m₁ else rand_m₁) >>= fun z => pure (b == z) := by      simp only [KEMScheme.IND_CPA_Game, composeWithDEM_toKEMRightReduction,        heval_bind, heval_pure, heval_liftProbComp]      simp_rw [bind_swap (my := 𝒟[$ᵗ Bool])]      congr 1; funext b      conv_lhs => simp only [bind_assoc, pure_bind]      cases b      · simp only [hite_false, ite_false]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (_, m₁, st) ← adversary.chooseMessages pk          let (kc, _) ← kem.encaps pk; let kR ← runtime.liftProbComp ($ᵗ K)          let dc ← dem.encrypt kR m₁; adversary.distinguish st (kc, dc)) >>= fun z =>          pure (false == z)        simp only [heval_bind, heval_liftProbComp, bind_assoc]      · simp only [ite_true]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (_, m₁, st) ← adversary.chooseMessages pk          let (kc, k) ← kem.encaps pk          let dc ← dem.encrypt k m₁; adversary.distinguish st (kc, dc)) >>= fun z =>          pure (true == z)        simp only [heval_bind, bind_assoc]        congr 1; funext pksk; congr 1; funext cms; congr 1; funext ckr        exact OracleComp.ProgramLogic.Relational.spmf_bind_const_of_no_failure          (OracleComp.ProgramLogic.Relational.probFailure_evalDist_eq_zero _) _    change (KEMScheme.IND_CPA_Game runtime _).boolBiasAdvantage = _    rw [hspmf, coin_branch _ _ (hno_fail _) (hno_fail _)]  have h_dem : dem.IND_CPA_Advantage runtime      (kem.composeWithDEM_toDEMReduction dem adversary) =      SPMF.boolDistAdvantage rand_m₀ rand_m₁ := by    have hspmf : DEMScheme.IND_CPA_Game runtime        (kem.composeWithDEM_toDEMReduction dem adversary) =        𝒟[$ᵗ Bool] >>= fun b =>          (if b then rand_m₁ else rand_m₀) >>= fun z => pure (b == z) := by      simp only [DEMScheme.IND_CPA_Game, KEMScheme.composeWithDEM_toDEMReduction,        heval_bind, heval_pure, heval_liftProbComp]      congr 1; funext b      conv_lhs => rw [bind_swap]      conv_lhs => simp only [bind_assoc, pure_bind]      cases b      · simp only [hite_false, ite_false]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (m₀, _, st) ← adversary.chooseMessages pk          let (kc, _) ← kem.encaps pk; let kR ← runtime.liftProbComp ($ᵗ K)          let dc ← dem.encrypt kR m₀; adversary.distinguish st (kc, dc)) >>= fun a =>          pure (false == a)        simp only [heval_bind, heval_liftProbComp, bind_assoc]      · simp only [ite_true]        change _ = (runtime.evalDist do          let (pk, _) ← kem.keygen; let (_, m₁, st) ← adversary.chooseMessages pk          let (kc, _) ← kem.encaps pk; let kR ← runtime.liftProbComp ($ᵗ K)          let dc ← dem.encrypt kR m₁; adversary.distinguish st (kc, dc)) >>= fun a =>          pure (true == a)        simp only [heval_bind, heval_liftProbComp, bind_assoc]    change (DEMScheme.IND_CPA_Game runtime _).boolBiasAdvantage = _    rw [hspmf, coin_branch _ _ (hno_fail _) (hno_fail _)]    unfold SPMF.boolDistAdvantage; rw [abs_sub_comm]  rw [h_composed]  calc SPMF.boolDistAdvantage real_m₀ real_m₁    _ ≤ SPMF.boolDistAdvantage real_m₀ rand_m₀ +        SPMF.boolDistAdvantage rand_m₀ rand_m₁ +        SPMF.boolDistAdvantage rand_m₁ real_m₁ := by      have := SPMF.boolDistAdvantage_triangle real_m₀ rand_m₀ real_m₁      have := SPMF.boolDistAdvantage_triangle rand_m₀ rand_m₁ real_m₁      linarith    _ = kem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toKEMLeftReduction dem adversary) +        SPMF.boolDistAdvantage rand_m₀ rand_m₁ +        SPMF.boolDistAdvantage rand_m₁ real_m₁ := by rw [← h_kem_left]    _ = kem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toKEMLeftReduction dem adversary) +        dem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toDEMReduction dem adversary) +        SPMF.boolDistAdvantage rand_m₁ real_m₁ := by rw [← h_dem]    _ = kem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toKEMLeftReduction dem adversary) +        dem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toDEMReduction dem adversary) +        SPMF.boolDistAdvantage real_m₁ rand_m₁ := by      congr 1; unfold SPMF.boolDistAdvantage; rw [abs_sub_comm]    _ = kem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toKEMLeftReduction dem adversary) +        kem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toKEMRightReduction dem adversary) +        dem.IND_CPA_Advantage runtime          (kem.composeWithDEM_toDEMReduction dem adversary) := by      rw [← h_kem_right]; ring