Sign uses Weighted Query Cost At Most

theorem sign_usesWeightedQueryCostAtMost    {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ]    [CanonicallyOrderedAdd κ]    (runtime : QueryImpl (fischlinROSpec Stmt Commit Chal Resp ρ b M) m)    (pk : Stmt) (sk : Wit) (msg : M)    (costFn : (fischlinROSpec Stmt Commit Chal Resp ρ b M).Domain → κ) (w : κ)    (hcost : ∀ t, costFn t ≤ w) :    QueryCost[ (Fischlin σ hr ρ b S M).sign pk sk msg in runtime by costFn ] ≤      ρ • (FinEnum.card Chal • w) := by  classical  let _ : SampleableType Chal := inferInstance  have hlen : (FinEnum.toList Chal).length = FinEnum.card Chal := by    simp [FinEnum.toList]  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 ←      fischlinSearchAuxWithAddCost σ        (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))) costFn    match result with    | some (ω, resp) => pure (comVec i, ω, resp)    | none => pure (comVec i, default, default)  have hrep : ∀ commits i,      AddWriterT.PathwiseCostAtMost (repStep commits i) (FinEnum.card Chal • w) := by    intro commits i    let comVec : Fin ρ → Commit := fun j => (commits j).1    let comList := List.ofFn comVec    have hsearch :        AddWriterT.PathwiseCostAtMost          (fischlinSearchAuxWithAddCost σ            (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))) costFn)          ((FinEnum.toList Chal).length • w) :=      fischlinSearchAuxWithAddCost_pathwiseCostAtMost        σ (κ := κ) (runtime := runtime) (pk := pk) (sk := sk) (sc := (commits i).2)        (msg := msg) (comList := comList) (i := i)        (challenges := FinEnum.toList Chal) (best := none) (costFn := costFn) (w := w)        (hcost := hcost)    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.PathwiseCostAtMost (finish result) 0 := by      intro result      cases result with      | none =>          simpa [finish] using AddWriterT.pathwiseCostAtMost_pure            (m := m) ((comVec i, default, default) : Commit × Chal × Resp)      | some pair =>          rcases pair with ⟨ω, resp⟩          simpa [finish] using AddWriterT.pathwiseCostAtMost_pure            (m := m) ((comVec i, ω, resp) : Commit × Chal × Resp)    refine AddWriterT.pathwiseCostAtMost_mono      (AddWriterT.pathwiseCostAtMost_bind (w₁ := (FinEnum.toList Chal).length • w) (w₂ := 0)        hsearch hcont) ?_    simp [hlen]  let commitComp : AddWriterT κ m (Fin ρ → Commit × PrvState) :=    Fin.mOfFn ρ fun _ => (liftM (σ.commit pk sk) : AddWriterT κ m (Commit × PrvState))  have hcommit :      AddWriterT.PathwiseCostAtMost commitComp 0 := by    have hstep :        AddWriterT.PathwiseCostAtMost          (liftM (σ.commit pk sk) : AddWriterT κ m (Commit × PrvState)) 0 := by      change AddWriterT.PathwiseCostAtMost        (monadLift (monadLift (σ.commit pk sk) : m (Commit × PrvState)) :          AddWriterT κ m (Commit × PrvState)) 0      exact AddWriterT.pathwiseCostAtMost_monadLift _    simpa [commitComp] using      (AddWriterT.pathwiseCostAtMost_fin_mOfFn (n := ρ) (k := 0)        (f := fun _ => (liftM (σ.commit pk sk) : AddWriterT κ m (Commit × PrvState)))        (fun _ => hstep))  suffices      AddWriterT.PathwiseCostAtMost        (commitComp >>= fun commits => Fin.mOfFn ρ (repStep commits))        (ρ • (FinEnum.card Chal • w)) by    have hsign :        HasQuery.Program.withAddCost          (fun [HasQuery (fischlinROSpec Stmt Commit Chal Resp ρ b M) (AddWriterT κ m)] =>            (Fischlin (m := AddWriterT κ m) σ hr ρ b S M).sign pk sk msg)          runtime costFn =          (commitComp >>= fun commits => Fin.mOfFn ρ (repStep commits)) := by      simp only [Fischlin, HasQuery.Program.withAddCost, 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_withAddCost          σ (runtime := runtime) (pk := pk) (sk := sk) (sc := (commits i).2)          (msg := msg) (comList := comList) (i := i)          (challenges := FinEnum.toList Chal) (best := none) (costFn := costFn)) using 1;        rfl    simpa [HasQuery.UsesCostAtMost, hsign] using this  simpa [zero_add] using    (AddWriterT.pathwiseCostAtMost_bind (w₁ := 0) (w₂ := ρ • (FinEnum.card Chal • w)) hcommit      (fun commits =>        AddWriterT.pathwiseCostAtMost_fin_mOfFn (n := ρ) (k := FinEnum.card Chal • w)          (fun i => hrep commits i)))