Binding cond le t sdh cond

lemma binding_cond_le_t_sdh_cond {n : ℕ} {AuxState : Type} [SampleableType G₁]    (hg₁ : g₁ ≠ 1) (hpair : pairing g₁ g₂ ≠ 0)    (adversary : KzgBindingAdversary p G₁ G₂ n unifSpec AuxState) :    Pr[bindingCondExt (p := p) (n := n) | bindingGameExt (g₁ := g₁) (g₂ := g₂)      AuxState adversary (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))]    ≤ Pr[(Groups.tSdhCondition (p := p) (g₁ := g₁)) ∘ mapBindingToTsdh (p := p)        (n := n) |      bindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary        (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing))] := by  let pSpec' : ProtocolSpec 1 := ⟨!v[.P_to_V], !v[G₁]⟩  let impl : QueryImpl _ (StateT unifSpec.QueryCache ProbComp) :=    QueryImpl.addLift      (randomOracle : QueryImpl unifSpec (StateT unifSpec.QueryCache ProbComp))      (challengeQueryImpl (pSpec := pSpec'))  let Claim : Type :=    G₁ × (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×      OracleInterface.Response q × OracleInterface.Response q × AuxState × AuxState  letI : ∀ i, OracleInterface (pSpec'.Challenge i) := ProtocolSpec.challengeOracleInterface  let RunResult : Type := (FullTranscript pSpec' × Bool × Unit) × Bool  let spec' := unifSpec + [pSpec'.Challenge]ₒ  let sample : ProbComp (ZMod p) := Groups.sampleNonzeroZMod (p := p)  let body : ZMod p → OracleComp spec' Claim := fun τ =>    liftComp (adversary.claim (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)) spec'  let run₁ : ZMod p → Claim → OracleComp spec' (Option RunResult) := fun τ claim =>    (Reduction.run      (claim.1, (⟨claim.2.1, claim.2.2.1⟩ :        (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) × OracleInterface.Response q))      claim.2.2.2.2.1      (Reduction.mk        (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ))        ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening          (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ,           Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)).verifier)).run  let run₂ : ZMod p → Claim → OracleComp spec' (Option RunResult) := fun τ claim =>    (Reduction.run      (claim.1, (⟨claim.2.1, claim.2.2.2.1⟩ :        (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) × OracleInterface.Response q))      claim.2.2.2.2.2      (Reduction.mk (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ))        ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening          (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ,           Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)).verifier)).run  let pack : ZMod p → Claim → Option RunResult → Option RunResult →      BindingExtOutput (p := p) n G₁ G₂ := fun τ claim result₁ result₂ =>    (τ, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ, claim.1, claim.2.1,      claim.2.2.1,      claim.2.2.2.1, (Option.map (fun result => result.2) result₁).getD false,      (Option.map (fun result => result.2) result₂).getD false,      (Option.map (fun result => result.1.1 0) result₁).getD (1 : G₁),      (Option.map (fun result => result.1.1 0) result₂).getD (1 : G₁))  let gameComp : ZMod p → OracleComp spec' (Option (BindingExtOutput (p := p) n G₁ G₂)) :=    fun τ => do      let claim ← body τ      let result₁ ← run₁ τ claim      let result₂ ← run₂ τ claim      pure (some (pack τ claim result₁ result₂))  let P : BindingExtOutput (p := p) n G₁ G₂ → Prop := bindingCondExt (p := p) (n := n)  let Q : BindingExtOutput (p := p) n G₁ G₂ → Prop :=    (Groups.tSdhCondition (p := p) (g₁ := g₁)) ∘ mapBindingToTsdh (p := p) (n := n)  have hmono :      Pr[P | OptionT.mk (do        let τ ← sample        (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]      ≤ Pr[Q | OptionT.mk (do        let τ ← sample        (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))] := by    apply probEvent_mono    intro y hy hP    obtain ⟨τ, _, hy⟩ := OptionT.mem_support_bind_mk _ _ hy    refine OptionT.aux_mem_support_simulateQ_run' impl (gameComp τ)      (∅ : unifSpec.QueryCache) (fun y => P y → Q y) ?_ hy hP    intro x hx y' hxy hP'    rw [hxy] at hx    dsimp only [gameComp] at hx    obtain ⟨claim, _, hx⟩ :=      support_bind_exists (x := body τ)        (f := fun claim => do          let result₁ ← run₁ τ claim          let result₂ ← run₂ τ claim          pure (some (pack τ claim result₁ result₂))) hx    obtain ⟨result₁, hresult₁, hx⟩ :=      support_bind_exists (x := run₁ τ claim)        (f := fun result₁ => do          let result₂ ← run₂ τ claim          pure (some (pack τ claim result₁ result₂))) hx    obtain ⟨result₂, hresult₂, hx⟩ :=      support_bind_exists (x := run₂ τ claim)        (f := fun result₂ => pure (some (pack τ claim result₁ result₂))) hx    have hy' : y' = pack τ claim result₁ result₂ := by      have : some y' = some (pack τ claim result₁ result₂) := by        simpa [mem_support_pure_iff] using hx      exact Option.some.inj this    subst y'    clear hxy hx hy    rcases claim with ⟨cm, query, resp₁, resp₂, st₁, st₂⟩    dsimp [P, pack, bindingCondExt, Commitment.bindingCondition] at hP'    rcases hP' with ⟨hresp, haccept₁, haccept₂⟩    obtain ⟨out₁, hrun₁, haccept₁⟩ :=      exists_of_option_map_get_d_true (fun result : RunResult => result.2) result₁        haccept₁    obtain ⟨out₂, hrun₂, haccept₂⟩ :=      exists_of_option_map_get_d_true (fun result : RunResult => result.2) result₂        haccept₂    dsimp [run₁] at hresult₁    dsimp [run₂] at hresult₂    have hverify₁ :        KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)          (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).2 cm          ((Option.map (fun result : RunResult => result.1.1 0) result₁).getD (1 : G₁))          query resp₁ := by      rw [hrun₁] at hresult₁      have hverif :=        Reduction.support_run_pure_verifier          (Reduction.mk            (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ))            ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ,               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)).verifier)          (fun stmt td =>            KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).2 stmt.1              (td ⟨0, by decide⟩) stmt.2.1 stmt.2.2)          (by intros; rfl)          (cm, (⟨query, resp₁⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×              OracleInterface.Response q))          st₁ hresult₁ rfl      have hproof :          (Option.map (fun result : RunResult => result.1.1 0) result₁).getD (1 : G₁) =            out₁.1.1 0 := by simp [hrun₁]      rw [hproof]      exact hverif.symm.trans haccept₁    have hverify₂ :        KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)          (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).2 cm          ((Option.map (fun result : RunResult => result.1.1 0) result₂).getD (1 : G₁))          query resp₂ := by      rw [hrun₂] at hresult₂      have hverif :=        Reduction.support_run_pure_verifier          (Reduction.mk            (adversary.prover (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ))            ((kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)).opening              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ,               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ)).verifier)          (fun stmt td =>            KZG.verifyOpening (g₁ := g₁) (g₂ := g₂) (pairing := pairing)              (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).2 stmt.1              (td ⟨0, by decide⟩) stmt.2.1 stmt.2.2)          (by intros; rfl)          (cm, (⟨query, resp₂⟩ :            (q : OracleInterface.Query (Fin (n + 1) → ZMod p)) ×              OracleInterface.Response q))          st₂ hresult₂ rfl      have hproof :          (Option.map (fun result : RunResult => result.1.1 0) result₂).getD (1 : G₁) =            out₂.1.1 0 := by simp [hrun₂]      rw [hproof]      exact hverif.symm.trans haccept₂    exact map_binding_to_t_sdh_of_two_valid_openings (p := p) (g₁ := g₁) (g₂ := g₂)      (pairing := pairing) τ query resp₁ resp₂ cm      ((Option.map (fun result : RunResult => result.1.1 0) result₁).getD (1 : G₁))      ((Option.map (fun result : RunResult => result.1.1 0) result₂).getD (1 : G₁))      ((Option.map (fun result : RunResult => result.2) result₁).getD false)      ((Option.map (fun result : RunResult => result.2) result₂).getD false)      (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ) rfl hresp hg₁ hpair      hverify₁ hverify₂  change    Pr[P | OptionT.mk (do      let τ ← sample      (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]    ≤ Pr[Q | OptionT.mk (do      let τ ← sample      (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]  exact hmono