Sign uses At Most Rho Card Omega Queries

theorem sign_usesAtMostRhoCardOmegaQueries    (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m)    (pk : Stmt) (sk : Wit) (msg : M) :    Queries[ (Fischlin σ hr ρ b S M).sign pk sk msg in runtime ] ≤ ρ * FinEnum.card Chal := by  classical  let _ : SampleableType Chal := inferInstance  let repStep : (Fin ρ → Commit × PrvState) → Fin ρ → AddWriterT ℕ m (Commit × Chal × Resp) :=      fun commits i => do    let comVec : Fin ρ → Commit := fun j => (commits j).1    let comList := List.ofFn comVec    let sc_i := (commits i).2    let result ←      fischlinSearchAuxWithUnitCost σ        (runtime := runtime) (pk := pk) (sk := sk) (sc := sc_i) (msg := msg)        (comList := comList) (i := i)        (FinEnum.toList Chal) (none : Option (Chal × Resp × Fin (2 ^ b)))    match result with    | some (ω, resp) => pure (comVec i, ω, resp)    | none => pure (comVec i, default, default)  have hlen : (FinEnum.toList Chal).length = FinEnum.card Chal := by    simp [FinEnum.toList]  have hrep : ∀ commits i,      AddWriterT.QueryBoundedAboveBy (repStep commits i) (FinEnum.card Chal) := by    intro commits i    let comVec : Fin ρ → Commit := fun j => (commits j).1    let comList := List.ofFn comVec    have hsearch :        AddWriterT.QueryBoundedAboveBy          (fischlinSearchAuxWithUnitCost σ            (runtime := runtime) (pk := pk) (sk := sk) (sc := (commits i).2)            (msg := msg) (comList := comList) (i := i)            (FinEnum.toList Chal) (none : Option (Chal × Resp × Fin (2 ^ b))))          (FinEnum.toList Chal).length := by      simpa using        (fischlinSearchAuxWithUnitCost_queryBoundedAboveBy          σ (runtime := runtime) (pk := pk) (sk := sk) (sc := (commits i).2)          (msg := msg) (comList := comList) (i := i)          (challenges := FinEnum.toList Chal) (best := none))    let finish : Option (Chal × Resp) → AddWriterT ℕ m (Commit × Chal × Resp)      | some (ω, resp) => pure (comVec i, ω, resp)      | none => pure (comVec i, default, default)    have hcont :        ∀ result : Option (Chal × Resp), AddWriterT.QueryBoundedAboveBy (finish result) 0 := by      intro result      cases result with      | none =>          simpa [finish] using AddWriterT.queryBoundedAboveBy_pure            (m := m) ((comVec i, default, default) : Commit × Chal × Resp)      | some pair =>          rcases pair with ⟨ω, resp⟩          simpa [finish] using AddWriterT.queryBoundedAboveBy_pure            (m := m) ((comVec i, ω, resp) : Commit × Chal × Resp)    exact AddWriterT.queryBoundedAboveBy_mono      (AddWriterT.queryBoundedAboveBy_bind (n₁ := (FinEnum.toList Chal).length) (n₂ := 0)        hsearch hcont)      (by simp [hlen])  let commitComp : AddWriterT ℕ m (Fin ρ → Commit × PrvState) :=    Fin.mOfFn ρ fun _ => (liftM (σ.commit pk sk) : AddWriterT ℕ m (Commit × PrvState))  have hcommit :      AddWriterT.QueryBoundedAboveBy commitComp 0 := by    have hstep :        AddWriterT.QueryBoundedAboveBy          (liftM (σ.commit pk sk) : AddWriterT ℕ m (Commit × PrvState)) 0 := by      change AddWriterT.QueryBoundedAboveBy        (monadLift (monadLift (σ.commit pk sk) : m (Commit × PrvState)) :          AddWriterT ℕ m (Commit × PrvState)) 0      exact AddWriterT.queryBoundedAboveBy_monadLift _    simpa [commitComp] using      (AddWriterT.queryBoundedAboveBy_fin_mOfFn (n := ρ) (k := 0)        (f := fun _ => (liftM (σ.commit pk sk) : AddWriterT ℕ m (Commit × PrvState)))        (fun _ => hstep))  suffices      AddWriterT.QueryBoundedAboveBy        (commitComp >>= fun commits => Fin.mOfFn ρ (repStep commits))        (ρ * FinEnum.card Chal) by    have hsign :        HasQuery.Program.withUnitCost          (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT ℕ m)] =>            (Fischlin (m := AddWriterT ℕ m) σ hr ρ b S M).sign pk sk msg)          runtime =          (commitComp >>= fun commits => Fin.mOfFn ρ (repStep commits)) := by      simp only [Fischlin, HasQuery.Program.withUnitCost, repStep, commitComp]      refine congrArg        (fun k => commitComp >>= k) ?_      funext commits      refine congrArg        (fun f : Fin ρ → AddWriterT ℕ m (Commit × Chal × Resp) => Fin.mOfFn ρ f) ?_      funext i      let comVec : Fin ρ → Commit := fun j => (commits j).1      let comList := List.ofFn comVec      let finish : AddWriterT ℕ m (Option (Chal × Resp)) →          AddWriterT ℕ m (Commit × Chal × Resp) := fun oa => do        let result ← oa        match result with        | some (ω, resp) => pure (comVec i, ω, resp)        | none => pure (comVec i, default, default)      convert congrArg finish        (fischlinSearchAux_eq_withUnitCost          σ (runtime := runtime) (pk := pk) (sk := sk) (sc := (commits i).2)          (msg := msg) (comList := comList) (i := i)          (challenges := FinEnum.toList Chal) (best := none)) using 1;        rfl    simpa [HasQuery.UsesAtMostQueries, hsign] using this  simpa [Nat.zero_add] using    (AddWriterT.queryBoundedAboveBy_bind (n₁ := 0) (n₂ := ρ * FinEnum.card Chal) hcommit      (fun commits =>        AddWriterT.queryBoundedAboveBy_fin_mOfFn (n := ρ) (k := FinEnum.card Chal)          (fun i => hrep commits i)))