Cma Real cma Sim tv sign le cma Sign Eps Core of valid

theorem cmaReal_cmaSim_tv_sign_le_cmaSignEpsCore_of_valid    (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel)    (hr : GenerableRelation Stmt Wit rel)    (simT : Stmt → ProbComp (Commit × Chal × Resp))    (ζ_zk β : ℝ≥0∞) (hζ_zk : ζ_zk < ∞)    (hHVZK : σ.HVZK simT ζ_zk.toReal)    (hCommit : σ.simCommitPredictability simT β)    (m : M) (s : CmaData M Commit Chal Stmt Wit)    (hvalid : CmaData.Valid (rel := rel) s) :    ENNReal.ofReal (tvDist      (((cmaReal M Commit Chal σ hr) (CmaQuery.sign m)).run (s, false))      (((cmaSim M Commit Chal hr simT) (CmaQuery.sign m)).run (s, false)))      ≤ cmaSignEpsCore M Commit Chal ζ_zk β s := by  let realGhost := cmaRealSignGhostDist M Commit Chal σ hr m s  let simPub := cmaSimSignPublicDist M Commit Chal hr simT s  let realOut :      CmaRealSignGhost Stmt Wit Commit PrvState Chal Resp →        (Commit × Resp) × CmaState M Commit Chal Stmt Wit :=    cmaRealSignGhostOut M Commit Chal m s  let simOut :      CmaSignPublic Stmt Wit Commit Chal Resp →        (Commit × Resp) × CmaState M Commit Chal Stmt Wit :=    cmaSimSignPublicOut M Commit Chal m s  let bad : CmaSignPublic Stmt Wit Commit Chal Resp → Prop :=    cmaSimSignPublicBad M Commit Chal m s  have hreal :      𝒟[((cmaReal M Commit Chal σ hr) (CmaQuery.sign m)).run (s, false)] =        𝒟[realOut <$> realGhost] := by    simpa [realGhost, realOut] using      cmaRealSignStep_evalDist_eq_ghost M Commit Chal σ hr m s  have hsim :      𝒟[((cmaSim M Commit Chal hr simT) (CmaQuery.sign m)).run (s, false)] =        𝒟[simOut <$> simPub] := by    simpa [simPub, simOut] using      cmaSimSignStep_evalDist_eq_public M Commit Chal hr simT m s  have hstep :      ENNReal.ofReal (tvDist        (((cmaReal M Commit Chal σ hr) (CmaQuery.sign m)).run (s, false))        (((cmaSim M Commit Chal hr simT) (CmaQuery.sign m)).run (s, false))) =      ENNReal.ofReal (tvDist (realOut <$> realGhost) (simOut <$> simPub)) := by    unfold tvDist    rw [hreal, hsim]  have hprivate :      ENNReal.ofReal (tvDist (realOut <$> realGhost) (simOut <$> simPub))        ≤ ENNReal.ofReal (tvDist (CmaRealSignGhost.public <$> realGhost) simPub) +            Pr[bad | simPub] :=    ofReal_tvDist_map_private_right_bad_le (oa := realGhost) (ob := simPub)      (pub := CmaRealSignGhost.public) (fa := realOut) (fb := simOut) (bad := bad)      fun x y hpub hbad =>        cmaRealSignGhostOut_eq_cmaSimSignPublicOut_of_not_bad M Commit Chal m s x y hpub hbad  have hpublic :      ENNReal.ofReal (tvDist (CmaRealSignGhost.public <$> realGhost) simPub) ≤ ζ_zk := by    have hpub_eval :        𝒟[CmaRealSignGhost.public <$> realGhost] =          𝒟[cmaRealSignPublicDist M Commit Chal σ hr s] := by      simpa [realGhost] using        cmaRealSignGhost_public_evalDist_eq_publicDist M Commit Chal σ hr m s    simpa [tvDist, simPub, hpub_eval] using      cmaSignPublicDist_tv_le_hvzk M Commit Chal σ hr simT ζ_zk hζ_zk hHVZK s hvalid  have hbad :      Pr[bad | simPub] ≤ QueryCache.enncard s.2.1 * β := by    simpa [bad, simPub] using      cmaSimSignPublicBad_prob_le_roCacheCount_mul M Commit Chal σ hr simT β        hCommit m s  rw [hstep]  exact (hprivate.trans (add_le_add hpublic hbad)).trans_eq rfl