diff --git a/Complexity.lean b/Complexity.lean
index 209115a403..b7de88f47e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1462,6 +1462,7 @@ public import Complexity.Crypto.Computational.ZeroKnowledge
 public import Complexity.Crypto.Game
 public import Complexity.Crypto.Game.Hybrid
 public import Complexity.Crypto.Game.Statistical
+public import Complexity.Crypto.Game.UntilBad
 public import Complexity.Crypto.Negligible
 public import Complexity.Crypto.Negligible.Basic
 public import Complexity.Crypto.Negligible.Dyadic
diff --git a/Complexity/Crypto/Game/UntilBad.lean b/Complexity/Crypto/Game/UntilBad.lean
new file mode 100644
index 0000000000..3236dc0d4e
--- /dev/null
+++ b/Complexity/Crypto/Game/UntilBad.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Game
+public import Complexity.Languages.Probabilistic.UntilBad
+
+/-!
+# Game hops that are identical until bad
+
+Two games that run one program against stateful handlers that agree until a bad state, followed by
+the same final step, have advantage at most the probability of reaching a bad state
+(`OracleComp.IdenticalUntilBad.advantage_le`, [BonehShoup2023], Theorem 4.7). This is the
+two-sided difference lemma `OracleComp.IdenticalUntilBad.abs_sub_le` in the form that composes
+with `Game.advantage_triangle`.
+
+## Main results
+
+* `Cslib.OracleComp.IdenticalUntilBad.advantage_le`: the advantage of an identical-until-bad hop.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Theorem 4.7.
+-/
+
+@[expose] public section
+
+namespace Cslib.OracleComp.IdenticalUntilBad
+
+open Crypto
+
+variable {ι σ α : Type} {spec : ι → Type} {first second : (q : ι) → StateT σ PMF (spec q)}
+  {bad : σ → Prop}
+
+/-- **The difference lemma** ([BonehShoup2023], Theorem 4.7): games that run a program against
+handlers agreeing until a bad state, followed by the same final step, have advantage at most the
+probability of reaching a bad state. -/
+theorem advantage_le (h : IdenticalUntilBad first second bad) (program : OracleComp spec α)
+    (s : σ) (next : α × σ → Game) :
+    (Game.advantage (((interpret first program).run s).bind next)
+        (((interpret second program).run s).bind next) : ℝ) ≤
+      (((interpret first program).run s).toOuterMeasure {x | bad x.2}).toReal := by
+  rw [Game.coe_advantage]
+  simpa only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] using
+    h.abs_sub_le program s next true
+
+end Cslib.OracleComp.IdenticalUntilBad
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean
index 1ec2b61c0a..f7161df88f 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean
@@ -24,24 +24,24 @@ challenge `c := H(m, t)` and responds with `z`; the signature `(t, z)` verifies
 `(t, H(m, t), z)` is an accepting conversation.
 
 Honest signatures verify (`fiatShamir_correct`). With special soundness, special HVZK and
-`δ`-unpredictable commitments ([BonehShoup2023], Definition 19.7), a forger making at most `Q`
-signing and hash calls in total wins the random-oracle EUF-CMA experiment with probability `ε`
+`δ`-unpredictable commitments ([BonehShoup2023], Definition 19.7), a forger making at most `Qs`
+signing calls and `Qro` hash calls wins the random-oracle EUF-CMA experiment with probability `ε`
 bounded by
 
-`ε ≤ C(Q, 2) · δ + (Q + 1) / N + √((Q + 1) · ε')`,
+`ε ≤ Qs · (Qs + Qro) · δ + (Qro + 1) / N + √((Qro + 1) · ε')`,
 
 where `N` is the number of challenges and `ε'` the success probability of an explicit adversary
-in the one-way game for the key generator (`succProbability_eufCmaGame_le`), as in
-[BonehShoup2023], Equation 19.21, which has `Q_s (Q_s + Q_ro + 1) · δ` in place of
-`C(Q, 2) · δ` and `Q_ro` in place of `Q`, for `Q_s` signing and `Q_ro` hash calls.
+in the one-way game for the key generator (`succProbability_eufCmaGame_le`). This is
+[BonehShoup2023], Equation 19.21, with `Qs · (Qs + Qro) · δ` in place of the slightly larger
+`Qs · (Qs + Qro + 1) · δ`.
 
 The proof follows [BonehShoup2023], Theorems 19.7 and 19.16, with the general forking lemma of
 [BellareNeven2006] in place of the reduction through impersonation:
 
 1. The signer is replaced by one that programs the oracle at `(m, t)` with a fresh challenge.
    The two agree until the signer's commitment hits a point already in the oracle's table, which
-   has probability at most `C(Q, 2) · δ` (the difference lemma,
-   `OracleComp.IdenticalUntilBad.bind_apply_le`).
+   has probability at most `Qs · (Qs + Qro) · δ` (the difference lemma,
+   `OracleComp.IdenticalUntilBad.bind_apply_le`, and `OracleComp.toOuterMeasure_bad_le`).
 2. Special HVZK replaces the programming signer by the simulator, which needs no witness.
 3. The simulated transcripts are drawn in advance, one per call
    (`OracleComp.IsQueryBounded.run_interpret_withSampleList`).
@@ -199,13 +199,14 @@ noncomputable def coins (simulate : Y → C → PMF (T × Z)) (A : Forger Y M (T
 
 variable [DecidableEq C]
 
-/-- **The one-way adversary** built from a forger: fork the forking program, with the `Q + 1`
+/-- **The one-way adversary** built from a forger making at most `Qs` signing and `Qro` hash
+calls: draw one simulated transcript per call, fork the forking program with the `Qro + 1`
 answers of its hash oracle, and extract a witness from the two forgeries. -/
 noncomputable def reduction [Nonempty X] (P : SigmaProtocol X Y T C Z)
     (simulate : Y → C → PMF (T × Z)) (extract : Y → T → C → Z → C → Z → X)
-    (A : Forger Y M (T × Z) (M × T) C) (Q : ℕ) (y : Y) : PMF X :=
-  (Forking.fork (coins simulate A Q y)
-    (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A))).map fun result =>
+    (A : Forger Y M (T × Z) (M × T) C) (Qs Qro : ℕ) (y : Y) : PMF X :=
+  (Forking.fork (coins simulate A (Qs + Qro) y)
+    (forkingAlgorithm (Classical.arbitrary C) (Qro + 1) (forkingProgram P A))).map fun result =>
       match result with
       | none => Classical.arbitrary X
       | some (_, out, out') =>
@@ -364,21 +365,22 @@ private theorem toOuterMeasure_lookup_le (P : SigmaProtocol X Y T C Z) (key : X
           ring
 
 open scoped ENNReal in
-/-- With `δ`-unpredictable commitments, the flag of a forger making at most `Q` calls is raised
-with probability at most `C(Q, 2) · δ`. -/
+/-- With `δ`-unpredictable commitments, the flag of a forger making at most `Qs` signing calls
+and `Q` calls in all is raised with probability at most `Qs · Q · δ`: each signing call hits one of
+the at most `Q` points of the table with probability at most `Q · δ`. -/
 private theorem toOuterMeasure_flag_le (P : SigmaProtocol X Y T C Z) (key : X × Y)
     {δ : ℝ≥0∞} (hcommit : ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ) {α : Type}
-    {program : OracleComp (ForgerSpec M (M × T) (T × Z) C) α} {Q : ℕ}
-    (hQ : IsQueryBounded program Q) :
+    {program : OracleComp (ForgerSpec M (M × T) (T × Z) C) α} {Qs Q : ℕ}
+    (hQs : IsCostBounded signingCost program Qs) (hQ : IsQueryBounded program Q) :
     ((interpret (realHandler P key) program).run (([], []), false)).toOuterMeasure
-      {x | x.2.2 = true} ≤ Q.choose 2 * δ := by
+      {x | x.2.2 = true} ≤ Qs * (Q * δ) := by
   have h := toOuterMeasure_bad_le (handler := realHandler P key) (bad := fun st => st.2 = true)
-    (fun st => st.1.1.length * δ) δ ?_ ?_ hQ (s := (([], []), false)) (by simp)
+    signingCost (fun st => st.1.1.length * δ) δ ?_ ?_ hQ hQs (s := (([], []), false)) (by simp)
   · simpa using h
   · intro q st hst
     cases q with
     | inl m =>
-      rw [realHandler, PMF.toOuterMeasure_bind_apply]
+      rw [signingCost, Nat.cast_one, one_mul, realHandler, PMF.toOuterMeasure_bind_apply]
       calc ∑' ts, (P.commit key.1 key.2) ts *
             ((oracle C (m, ts.1) st.1.1).map fun r => ((ts.1, P.respond key.1 key.2 ts.2 r.1),
               ((r.2, m :: st.1.2), st.2 || (st.1.1.lookup (m, ts.1)).isSome))).toOuterMeasure
@@ -712,13 +714,14 @@ private theorem runWithAnswers_forkingProgram (P : SigmaProtocol X Y T C Z)
         rw [hcount, List.getD_eq_getElem?_getD, List.headD_eq_head?_getD, List.head?_drop]
 
 omit [Fintype C] in
-/-- The forking program asks at most one query per call of the forger, and one more to check the
-forgery. -/
+/-- The forking program asks at most one query per hash call of the forger, and one more to check
+the forgery. -/
 private theorem isQueryBounded_forkingProgram (P : SigmaProtocol X Y T C Z)
-    (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q)
-    (s : Y × A.Coins × List (T × C × Z)) : IsQueryBounded (forkingProgram P A s) (Q + 1) := by
+    (A : Forger Y M (T × Z) (M × T) C) {Qro : ℕ}
+    (hQro : ∀ y s, IsCostBounded hashCost (A.forge y s) Qro)
+    (s : Y × A.Coins × List (T × C × Z)) : IsQueryBounded (forkingProgram P A s) (Qro + 1) := by
   have hhandler (q : M ⊕ (M × T)) (st : ReductionState M T C Z) :
-      IsQueryBounded ((reductionHandler q).run st) 1 := by
+      IsQueryBounded ((reductionHandler q).run st) (hashCost q) := by
     cases q with
     | inl m =>
       rw [run_reductionHandler_inl]
@@ -731,9 +734,7 @@ private theorem isQueryBounded_forkingProgram (P : SigmaProtocol X Y T C Z)
       | none =>
         rw [run_reductionHandler_inr_none hl]
         exact .liftBind _ _ 0 fun _ => .pure _ 0
-  have hforge := (hQ s.1 s.2.1).run_interpret hhandler ⟨[], [], 0, s.2.2⟩
-  rw [Nat.mul_one] at hforge
-  refine hforge.bind fun forged => ?_
+  refine ((hQro s.1 s.2.1).run_interpret hhandler ⟨[], [], 0, s.2.2⟩).bind fun forged => ?_
   cases hl : forged.2.table.lookup (forged.1.1, forged.1.2.1) with
   | some e =>
     rw [finish_of_some hl]
@@ -745,12 +746,13 @@ private theorem isQueryBounded_forkingProgram (P : SigmaProtocol X Y T C Z)
 /-- With its oracle answered uniformly, the forking program wins at most as often as it validly
 names a query. -/
 private theorem map_run_le_accept (P : SigmaProtocol X Y T C Z)
-    (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q)
+    (A : Forger Y M (T × Z) (M × T) C) {Qro : ℕ}
+    (hQro : ∀ y s, IsCostBounded hashCost (A.forge y s) Qro)
     (s : Y × A.Coins × List (T × C × Z)) :
     ((interpret countingUniform (forkingProgram P A s)).run 0).map (fun run => run.1.2.1) true ≤
       ((interpret countingUniform (forkingProgram P A s)).run 0).bind
-        (fun run => PMF.pure (validIndex (Q + 1) run.2 run.1.1).isSome) true := by
-  have hbound := isQueryBounded_forkingProgram P A hQ s
+        (fun run => PMF.pure (validIndex (Qro + 1) run.2 run.1.1).isSome) true := by
+  have hbound := isQueryBounded_forkingProgram P A hQro s
   rw [run_interpret_countingUniform_eq (Classical.arbitrary C) _
     (hbound.hasQueryBounds (size := fun _ => 0) (maxSize := 0) fun _ => le_rfl)]
   simp only [← PMF.bind_pure_comp, PMF.bind_bind, PMF.pure_bind, Function.comp_def]
@@ -762,7 +764,7 @@ private theorem map_run_le_accept (P : SigmaProtocol X Y T C Z)
     have hlt : j < (runWithAnswers (Classical.arbitrary C) (forkingProgram P A s)
         (List.ofFn h)).2.length := (List.getElem?_eq_some_iff.mp (hnamed j hj).1).1
     have hle := hbound.length_runWithAnswers_le (Classical.arbitrary C) (List.ofFn h)
-    have hvalid : (validIndex (Q + 1) (0 + (runWithAnswers (Classical.arbitrary C)
+    have hvalid : (validIndex (Qro + 1) (0 + (runWithAnswers (Classical.arbitrary C)
         (forkingProgram P A s) (List.ofFn h)).2.length) (runWithAnswers (Classical.arbitrary C)
           (forkingProgram P A s) (List.ofFn h)).1.1).isSome = true := by
       rw [hj, zero_add]
@@ -788,15 +790,15 @@ special soundness turns them into a witness. -/
 private theorem fork_le_oneWayGame [Nonempty X] {P : SigmaProtocol X Y T C Z}
     {keyGen : PMF (X × Y)} {R : X → Y → Prop} [∀ x y, Decidable (R x y)]
     {extract : Y → T → C → Z → C → Z → X} (hsound : P.SpecialSoundOn keyGen R extract)
-    (simulate : Y → C → PMF (T × Z)) (A : Forger Y M (T × Z) (M × T) C) (Q : ℕ) :
-    (Forking.fork (keyGen.bind fun key => coins simulate A Q key.2)
-        (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A))).map
+    (simulate : Y → C → PMF (T × Z)) (A : Forger Y M (T × Z) (M × T) C) (Qs Qro : ℕ) :
+    (Forking.fork (keyGen.bind fun key => coins simulate A (Qs + Qro) key.2)
+        (forkingAlgorithm (Classical.arbitrary C) (Qro + 1) (forkingProgram P A))).map
           Option.isSome true ≤
-      oneWayGame keyGen R (reduction P simulate extract A Q) true := by
-  have hfork : Forking.fork (keyGen.bind fun key => coins simulate A Q key.2)
-      (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A)) =
-      keyGen.bind fun key => Forking.fork (coins simulate A Q key.2)
-        (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A)) := by
+      oneWayGame keyGen R (reduction P simulate extract A Qs Qro) true := by
+  have hfork : Forking.fork (keyGen.bind fun key => coins simulate A (Qs + Qro) key.2)
+      (forkingAlgorithm (Classical.arbitrary C) (Qro + 1) (forkingProgram P A)) =
+      keyGen.bind fun key => Forking.fork (coins simulate A (Qs + Qro) key.2)
+        (forkingAlgorithm (Classical.arbitrary C) (Qro + 1) (forkingProgram P A)) := by
     simp only [Forking.fork, PMF.monad_bind_eq_bind, PMF.bind_bind]
   rw [hfork, PMF.map_bind]
   simp only [oneWayGame, reduction, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_map]
@@ -838,28 +840,30 @@ private theorem bind_apply_le_add {α β : Type} {μ : PMF α} {f g : α → PMF
 
 omit [DecidableEq C] in
 /-- **The game hops** for one key and one choice of the forger's coins: the experiment wins at
-most as often as the forking program, with presampled transcripts, plus `C(Q, 2) · δ`. -/
+most as often as the forking program, with presampled transcripts, plus `Qs · (Qs + Qro) · δ`. -/
 private theorem run_bind_finishGame_le {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)}
     {R : X → Y → Prop} {simulate : Y → C → PMF (T × Z)} (hzk : P.SpecialHVZK R simulate)
     {key : X × Y} (hkey : R key.1 key.2) {δ : ENNReal}
     (hcommit : ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ)
-    (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ} (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q)
+    (A : Forger Y M (T × Z) (M × T) C) {Qs Qro : ℕ} (hA : A.CallBounded Qs Qro)
     (c : A.Coins) :
     ((interpret (handler (fiatShamir P keyGen) key) (A.forge key.2 c)).run ([], [])).bind
         (finishGame P key.2) true ≤
-      ((PMF.iid (simulateConversation simulate key.2) Q).map List.ofFn).bind (fun trs =>
+      ((PMF.iid (simulateConversation simulate key.2) (Qs + Qro)).map List.ofFn).bind (fun trs =>
         ((interpret countingUniform (forkingProgram P A (key.2, c, trs))).run 0).map
-          fun run => run.1.2.1) true + Q.choose 2 * δ := by
+          fun run => run.1.2.1) true + (Qs * (Qs + Qro) : ℕ) * δ := by
   have h0 := run_interpret_map_state (realHandler P key) (handler (fiatShamir P keyGen) key)
     Prod.fst (realHandler_map P keyGen key) (A.forge key.2 c) (([], []), false)
   have h1 := run_interpret_map_state (programHandler P key)
     (fun q st => (simulateConversation simulate key.2).bind fun v => simulatedHandler v q st)
     Prod.fst (programHandler_map hzk hkey) (A.forge key.2 c) (([], []), false)
-  have h2 := (hQ key.2 c).run_interpret_withSampleList (simulateConversation simulate key.2)
-    (Classical.arbitrary _) simulatedHandler ([], [])
+  have h2 := (hA.isQueryBounded key.2 c).run_interpret_withSampleList
+    (simulateConversation simulate key.2) (Classical.arbitrary _) simulatedHandler ([], [])
+  have hflag := toOuterMeasure_flag_le P key hcommit (hA key.2 c).1 (hA.isQueryBounded key.2 c)
+  rw [show (Qs : ENNReal) * ((Qs + Qro : ℕ) * δ) = (Qs * (Qs + Qro) : ℕ) * δ by
+    push_cast; ring] at hflag
   rw [← h0, PMF.bind_map]
-  refine ((identicalUntilBad P key).bind_apply_le _ _ _ _).trans
-    (add_le_add (le_of_eq ?_) (toOuterMeasure_flag_le P key hcommit (hQ key.2 c)))
+  refine ((identicalUntilBad P key).bind_apply_le _ _ _ _).trans (add_le_add (le_of_eq ?_) hflag)
   rw [← PMF.bind_map, h1, ← h2, PMF.bind_bind]
   refine congrArg (fun p : PMF Bool => p true) (congrArg (PMF.bind _) (funext fun trs => ?_))
   rw [PMF.bind_map, map_run_forkingProgram]
@@ -872,10 +876,11 @@ open scoped NNReal in
 /-- **Security of Fiat–Shamir signatures** ([BonehShoup2023], Theorem 19.16 with Equation 19.21,
 via [BellareNeven2006], Lemma 1). Let the Sigma protocol be special sound on the generated keys
 with extractor `extract`, special HVZK with simulator `simulate`, and have `δ`-unpredictable
-commitments, and let the key generator produce pairs in the relation. A forger making at most `Q`
-signing and hash calls in total wins the random-oracle EUF-CMA experiment with probability at
-most `C(Q, 2) · δ + (Q + 1) / N + √((Q + 1) · ε')`, where `N` is the number of challenges and `ε'`
-is the probability that the reduction outputs a witness for a generated statement. -/
+commitments, and let the key generator produce pairs in the relation. A forger making at most `Qs`
+signing calls and `Qro` hash calls wins the random-oracle EUF-CMA experiment with probability at
+most `Qs · (Qs + Qro) · δ + (Qro + 1) / N + √((Qro + 1) · ε')`, where `N` is the number of
+challenges and `ε'` is the probability that the reduction outputs a witness for a generated
+statement. -/
 theorem succProbability_eufCmaGame_le [Nonempty X] [Nonempty T] [Nonempty Z] [DecidableEq C]
     {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)} {R : X → Y → Prop}
     [∀ x y, Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X}
@@ -883,51 +888,53 @@ theorem succProbability_eufCmaGame_le [Nonempty X] [Nonempty T] [Nonempty Z] [De
     (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) (hsound : P.SpecialSoundOn keyGen R extract)
     (hzk : P.SpecialHVZK R simulate)
     (hcommit : ∀ key ∈ keyGen.support, ∀ t, (P.commit key.1 key.2).map Prod.fst t ≤ δ)
-    (A : Forger Y M (T × Z) (M × T) C) {Q : ℕ}
-    (hQ : ∀ y s, IsQueryBounded (A.forge y s) Q) :
+    (A : Forger Y M (T × Z) (M × T) C) {Qs Qro : ℕ} (hA : A.CallBounded Qs Qro) :
     (Game.succProbability (eufCmaGame (fiatShamir P keyGen) A) : ℝ) ≤
-      Q.choose 2 * δ + (Q + 1) / Fintype.card C +
-        √((Q + 1) * Game.succProbability
-          (oneWayGame keyGen R (reduction P simulate extract A Q))) := by
+      Qs * (Qs + Qro) * δ + (Qro + 1) / Fintype.card C +
+        √((Qro + 1) * Game.succProbability
+          (oneWayGame keyGen R (reduction P simulate extract A Qs Qro))) := by
   classical
-  set first := keyGen.bind fun key => coins simulate A Q key.2 with hfirst
-  have hA : eufCmaGame (fiatShamir P keyGen) A true ≤
+  set first := keyGen.bind fun key => coins simulate A (Qs + Qro) key.2 with hfirst
+  have hA' : eufCmaGame (fiatShamir P keyGen) A true ≤
       first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).map
-        fun run => run.1.2.1) true + Q.choose 2 * (δ : ENNReal) := by
+        fun run => run.1.2.1) true + (Qs * (Qs + Qro) : ℕ) * (δ : ENNReal) := by
     rw [eufCmaGame_fiatShamir, hfirst]
     simp only [coins, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind,
       PMF.pure_bind]
     refine bind_apply_le_add fun key hkey' => bind_apply_le_add fun c _ => ?_
-    exact run_bind_finishGame_le hzk (hkey key hkey') (hcommit key hkey') A hQ c
+    exact run_bind_finishGame_le hzk (hkey key hkey') (hcommit key hkey') A hA c
+  have hQro (y : Y) (s : A.Coins) : IsCostBounded hashCost (A.forge y s) Qro := (hA y s).2
   have hB : first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).map
         fun run => run.1.2.1) true ≤
       first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).bind
-        fun run => PMF.pure (validIndex (Q + 1) run.2 run.1.1).isSome) true :=
-    Probability.PMF.bind_apply_mono_on_support _ _ fun s _ => map_run_le_accept P A hQ s
+        fun run => PMF.pure (validIndex (Qro + 1) run.2 run.1.1).isSome) true :=
+    Probability.PMF.bind_apply_mono_on_support _ _ fun s _ => map_run_le_accept P A hQro s
   have hC := le_add_sqrt_fork first (forkingProgram P A) (Classical.arbitrary C)
-    (fun s => (isQueryBounded_forkingProgram P A hQ s).hasQueryBounds (size := fun _ => 0)
+    (fun s => (isQueryBounded_forkingProgram P A hQro s).hasQueryBounds (size := fun _ => 0)
       (maxSize := 0) fun _ => le_rfl)
-  have hD := fork_le_oneWayGame (P := P) hsound simulate A Q
+  have hD := fork_le_oneWayGame (P := P) hsound simulate A Qs Qro
   simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] at hC
   simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
-  have hK : (Q.choose 2 * (δ : ENNReal)).toReal = Q.choose 2 * δ := by
+  have hK : (((Qs * (Qs + Qro) : ℕ) : ENNReal) * δ).toReal = Qs * (Qs + Qro) * δ := by
     rw [ENNReal.toReal_mul, ENNReal.toReal_natCast, ENNReal.coe_toReal]
+    push_cast
+    ring
   calc (eufCmaGame (fiatShamir P keyGen) A true).toReal
       ≤ (first.bind (fun s => ((interpret countingUniform (forkingProgram P A s)).run 0).bind
-          fun run => PMF.pure (validIndex (Q + 1) run.2 run.1.1).isSome) true).toReal +
-          Q.choose 2 * δ := by
+          fun run => PMF.pure (validIndex (Qro + 1) run.2 run.1.1).isSome) true).toReal +
+          Qs * (Qs + Qro) * δ := by
         rw [← hK, ← ENNReal.toReal_add (PMF.apply_ne_top _ _)
           (ENNReal.mul_ne_top (ENNReal.natCast_ne_top _) ENNReal.coe_ne_top)]
         exact ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨PMF.apply_ne_top _ _,
           ENNReal.mul_ne_top (ENNReal.natCast_ne_top _) ENNReal.coe_ne_top⟩)
-          (hA.trans (add_le_add hB le_rfl))
-    _ ≤ ((Q + 1 : ℕ) / Fintype.card C + √((Q + 1 : ℕ) * ((Forking.fork first
-          (forkingAlgorithm (Classical.arbitrary C) (Q + 1) (forkingProgram P A))).map
-            Option.isSome true).toReal)) + Q.choose 2 * δ := add_le_add hC le_rfl
+          (hA'.trans (add_le_add hB le_rfl))
+    _ ≤ ((Qro + 1 : ℕ) / Fintype.card C + √((Qro + 1 : ℕ) * ((Forking.fork first
+          (forkingAlgorithm (Classical.arbitrary C) (Qro + 1) (forkingProgram P A))).map
+            Option.isSome true).toReal)) + Qs * (Qs + Qro) * δ := add_le_add hC le_rfl
     _ ≤ _ := by
         push_cast
         have hsqrt := Real.sqrt_le_sqrt (mul_le_mul_of_nonneg_left
-          (ENNReal.toReal_mono (PMF.apply_ne_top _ _) hD) (by positivity : (0 : ℝ) ≤ Q + 1))
+          (ENNReal.toReal_mono (PMF.apply_ne_top _ _) hD) (by positivity : (0 : ℝ) ≤ Qro + 1))
         linarith
 
 end Cslib.Crypto.Protocols.SigmaProtocol
diff --git a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean
index bc9f577863..d7ec9b9f49 100644
--- a/Complexity/Crypto/Protocols/Signature/RandomOracle.lean
+++ b/Complexity/Crypto/Protocols/Signature/RandomOracle.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Foundations.Control.Monad.Memoize
 public import Complexity.Languages.Probabilistic.Basic
+public import Complexity.Languages.Probabilistic.QueryCount
 public import Cslib.Probability.PMF
 import Complexity.Probability.PMF
 
@@ -26,16 +27,27 @@ The existential-unforgeability experiment (`eufCmaGame`, [BonehShoup2023], Attac
 its random-oracle version) gives a forger the public key and oracle access to the signer and to
 `H`; the forger wins with a valid signature on a message it never asked to have signed. A
 `Forger` has explicit coins, drawn first, and is otherwise a deterministic `OracleComp` program;
-this is the form in which a forger can be rerun on the same coins, as forking needs.
+this is the form in which a forger can be rerun on the same coins, as forking needs. Its signing
+and hash calls are counted separately (`Forger.CallBounded`), as security bounds depend on them
+differently.
 
 These are exact probability laws for one scheme and one forger, with no efficiency claim. The
 oracle interface is the library's `OracleComp`; it is meant to be re-expressed in the shared
 interactive-protocol core of #643 once that core exists.
 
+This interface is separate from the computational `Cslib.Crypto.SignatureScheme`, which packages
+word encodings, strict PPT certificates and verification without an oracle. Here the key and
+signing coins are arbitrary typed laws, and signing and verification share the hash oracle. A
+computational statement about a scheme of this form needs encodings, an efficient realization of
+the oracle and resource certificates on top of the exact bound; the two notions are not competing
+computational interfaces.
+
 ## Main definitions
 
 * `Cslib.Crypto.Protocols.ROMSignature.Scheme`: key generation, signing and verification.
 * `Cslib.Crypto.Protocols.ROMSignature.Forger`: a forger with explicit coins.
+* `Cslib.Crypto.Protocols.ROMSignature.Forger.CallBounded`: bounds on a forger's signing and hash
+  calls.
 * `Cslib.Crypto.Protocols.ROMSignature.oracle`: the lazily sampled uniform random oracle.
 * `Cslib.Crypto.Protocols.ROMSignature.eufCmaGame`: the random-oracle EUF-CMA experiment.
 * `Cslib.Crypto.Protocols.ROMSignature.Scheme.Correct`: honest signatures verify.
@@ -82,7 +94,32 @@ structure Forger (PK M Sig Query Digest : Type) where
   /-- Forge, calling the signer and the oracle. -/
   forge : PK → Coins → OracleComp (ForgerSpec M Query Sig Digest) (M × Sig)
 
-variable {PK SK M Sig Query Digest : Type} [DecidableEq Query] [Fintype Digest] [Nonempty Digest]
+variable {PK SK M Sig Query Digest : Type}
+
+/-- A forger's call costs one when it is a signing call. -/
+def signingCost : M ⊕ Query → ℕ
+  | .inl _ => 1
+  | .inr _ => 0
+
+/-- A forger's call costs one when it is a hash call. -/
+def hashCost : M ⊕ Query → ℕ
+  | .inl _ => 0
+  | .inr _ => 1
+
+/-- The forger makes at most `signs` signing calls and at most `hashes` hash calls on every path,
+for every public key and every choice of its coins. -/
+def Forger.CallBounded (A : Forger PK M Sig Query Digest) (signs hashes : ℕ) : Prop :=
+  ∀ pk coins, IsCostBounded signingCost (A.forge pk coins) signs ∧
+    IsCostBounded hashCost (A.forge pk coins) hashes
+
+/-- A forger making at most `signs` signing and `hashes` hash calls makes at most
+`signs + hashes` calls. -/
+theorem Forger.CallBounded.isQueryBounded {A : Forger PK M Sig Query Digest} {signs hashes : ℕ}
+    (h : A.CallBounded signs hashes) (pk : PK) (coins : A.Coins) :
+    IsQueryBounded (A.forge pk coins) (signs + hashes) :=
+  ((h pk coins).1.add (h pk coins).2).of_le fun q => by cases q <;> simp [signingCost, hashCost]
+
+variable [DecidableEq Query] [Fintype Digest] [Nonempty Digest]
 
 variable (Digest) in
 /-- The random oracle: a uniform digest for each new point, remembered thereafter. -/
diff --git a/Complexity/Languages/Probabilistic/QueryCount.lean b/Complexity/Languages/Probabilistic/QueryCount.lean
index 214e334643..68e995adfd 100644
--- a/Complexity/Languages/Probabilistic/QueryCount.lean
+++ b/Complexity/Languages/Probabilistic/QueryCount.lean
@@ -15,13 +15,15 @@ import Complexity.Probability.PMF
 /-!
 # Counting oracle calls structurally
 
-`OracleComp.IsQueryBounded program n` says that `program` makes at most `n` oracle calls on every
-path through its tree of calls, whatever the answers. This is the structural form of a call
-budget: it is preserved by sequencing (`IsQueryBounded.bind`) and proved by induction on the
-program, and it gives the semantic, handler-quantified bound
+`OracleComp.IsCostBounded cost program n` says that the calls of `program` cost at most `n` in
+total on every path through its tree of calls, whatever the answers, where a call `q` costs
+`cost q`. With unit costs this is `OracleComp.IsQueryBounded program n`: at most `n` calls on every
+path. Other costs count calls of one kind only, such as the signing calls of a forger. Budgets are
+preserved by sequencing (`IsCostBounded.bind`), add over costs (`IsCostBounded.add`) and are proved
+by induction on the program. A call budget gives the semantic, handler-quantified bound
 `ProbOracleComp.HasQueryBounds` for the program's external calls
-(`IsQueryBounded.hasQueryBounds`). Running a program through a handler multiplies budgets
-(`IsQueryBounded.run_interpret`).
+(`IsQueryBounded.hasQueryBounds`), and running a program through a handler whose calls make at
+most `cost q` calls gives a call budget (`IsCostBounded.run_interpret`).
 
 A budget also justifies presampling: a handler that draws one sample per call can read its
 samples from a list of independent draws made in advance, with the same law of the result and the
@@ -29,13 +31,16 @@ final state (`IsQueryBounded.run_interpret_withSampleList`).
 
 ## Main definitions
 
+* `Cslib.OracleComp.IsCostBounded`: calls costing at most `n` on every path.
 * `Cslib.OracleComp.IsQueryBounded`: at most `n` calls on every path.
 
 ## Main results
 
-* `Cslib.OracleComp.IsQueryBounded.bind`: budgets add under sequencing.
+* `Cslib.OracleComp.IsCostBounded.bind`: budgets add under sequencing.
+* `Cslib.OracleComp.IsCostBounded.add`: budgets for two costs give a budget for their sum.
+* `Cslib.OracleComp.IsCostBounded.run_interpret`: the call budget of a program run through a
+  handler.
 * `Cslib.OracleComp.IsQueryBounded.hasQueryBounds`: the semantic external call bound.
-* `Cslib.OracleComp.IsQueryBounded.run_interpret`: the budget of a program run through a handler.
 * `Cslib.OracleComp.IsQueryBounded.run_interpret_withSampleList`: presampling a handler's draws.
 -/
 
@@ -47,41 +52,97 @@ universe u v
 
 variable {ι : Type u} {spec : OracleSpec.{u, v} ι} {α β : Type v}
 
-/-- The program makes at most `n` oracle calls on every path, whatever the answers. -/
-inductive IsQueryBounded : OracleComp spec α → ℕ → Prop
+/-- The calls of the program cost at most `n` in total on every path, whatever the answers, where
+a call `q` costs `cost q`. -/
+inductive IsCostBounded (cost : ι → ℕ) : OracleComp spec α → ℕ → Prop
   /-- Returning a value makes no call. -/
-  | pure (a : α) (n : ℕ) : IsQueryBounded (PFunctor.FreeM.pure a) n
-  /-- A call followed by continuations that each make at most `n` calls. -/
+  | pure (a : α) (n : ℕ) : IsCostBounded cost (PFunctor.FreeM.pure a) n
+  /-- A call followed by continuations whose calls each cost at most `n`. -/
   | liftBind (q : ι) (cont : spec q → OracleComp spec α) (n : ℕ)
-      (hcont : ∀ a, IsQueryBounded (cont a) n) :
-      IsQueryBounded (PFunctor.FreeM.liftBind q cont) (n + 1)
+      (hcont : ∀ a, IsCostBounded cost (cont a) n) :
+      IsCostBounded cost (PFunctor.FreeM.liftBind q cont) (n + cost q)
+
+/-- The program makes at most `n` oracle calls on every path, whatever the answers. -/
+abbrev IsQueryBounded (program : OracleComp spec α) (n : ℕ) : Prop :=
+  IsCostBounded (fun _ => 1) program n
 
-namespace IsQueryBounded
+namespace IsCostBounded
+
+variable {cost : ι → ℕ}
 
 /-- A larger budget is still a budget. -/
-theorem mono {program : OracleComp spec α} {n m : ℕ} (h : IsQueryBounded program n)
-    (hnm : n ≤ m) : IsQueryBounded program m := by
+theorem mono {program : OracleComp spec α} {n m : ℕ} (h : IsCostBounded cost program n)
+    (hnm : n ≤ m) : IsCostBounded cost program m := by
   induction h generalizing m with
   | pure a n => exact .pure a m
   | liftBind q cont n _ ih =>
-    obtain ⟨m, rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
+    obtain ⟨m, rfl⟩ : ∃ m', m = m' + cost q := ⟨m - cost q, by omega⟩
     exact .liftBind q cont m fun a => ih a (by omega)
 
-/-- One call. -/
-theorem query (q : ι) : IsQueryBounded (OracleComp.query (spec := spec) q) 1 :=
-  .liftBind q _ 0 fun a => .pure a 0
+/-- A budget for a call's continuations, from a budget for the call. -/
+theorem liftBind_iff {q : ι} {cont : spec q → OracleComp spec α} {n : ℕ} :
+    IsCostBounded cost (PFunctor.FreeM.liftBind q cont) n ↔
+      cost q ≤ n ∧ ∀ a, IsCostBounded cost (cont a) (n - cost q) := by
+  constructor
+  · rintro (_ | ⟨_, _, n, hcont⟩)
+    exact ⟨by omega, fun a => by rw [Nat.add_sub_cancel]; exact hcont a⟩
+  · rintro ⟨hle, hcont⟩
+    rw [show n = n - cost q + cost q by omega]
+    exact .liftBind q cont _ hcont
+
+/-- One call costs its cost. -/
+theorem query (q : ι) : IsCostBounded cost (OracleComp.query (spec := spec) q) (cost q) := by
+  have h := IsCostBounded.liftBind (spec := spec) (cost := cost) q
+    (fun a : spec q => PFunctor.FreeM.pure a) 0 fun a => .pure a 0
+  rw [Nat.zero_add] at h
+  exact h
 
 /-- Budgets add under sequencing. -/
 theorem bind {program : OracleComp spec α} {next : α → OracleComp spec β} {n m : ℕ}
-    (h : IsQueryBounded program n) (hnext : ∀ a, IsQueryBounded (next a) m) :
-    IsQueryBounded (program >>= next) (n + m) := by
+    (h : IsCostBounded cost program n) (hnext : ∀ a, IsCostBounded cost (next a) m) :
+    IsCostBounded cost (program >>= next) (n + m) := by
   induction h with
   | pure a n => exact (hnext a).mono (by omega)
   | liftBind q cont n _ ih =>
-    rw [show n + 1 + m = n + m + 1 by omega]
+    rw [show n + cost q + m = n + m + cost q by omega]
     exact .liftBind q _ (n + m) ih
 
-end IsQueryBounded
+/-- A budget for a cost is one for every smaller cost. -/
+theorem of_le {cost' : ι → ℕ} {program : OracleComp spec α} {n : ℕ}
+    (h : IsCostBounded cost program n) (hcost : ∀ q, cost' q ≤ cost q) :
+    IsCostBounded cost' program n := by
+  induction h with
+  | pure a n => exact .pure a n
+  | liftBind q cont n _ ih => exact (IsCostBounded.liftBind q cont n ih).mono (by simp [hcost q])
+
+/-- Budgets for two costs give a budget for their sum. -/
+theorem add {cost' : ι → ℕ} {program : OracleComp spec α} {n n' : ℕ}
+    (h : IsCostBounded cost program n) (h' : IsCostBounded cost' program n') :
+    IsCostBounded (fun q => cost q + cost' q) program (n + n') := by
+  induction h generalizing n' with
+  | pure a n => exact .pure a _
+  | liftBind q cont n _ ih =>
+    obtain ⟨hle, hcont⟩ := liftBind_iff.mp h'
+    rw [show n + cost q + n' = n + (n' - cost' q) + (cost q + cost' q) by omega]
+    exact .liftBind q cont _ fun a => ih a (hcont a)
+
+/-- A program run through a stateful handler, each of whose calls `q` makes at most `cost q`
+calls to the target oracle, makes at most `n` target calls when its own calls cost at most
+`n`. -/
+theorem run_interpret {κ : Type u} {target : OracleSpec.{u, v} κ} {σ : Type v}
+    {handler : (q : ι) → StateT σ (OracleComp target) (spec q)}
+    (hhandler : ∀ q s, IsQueryBounded ((handler q).run s) (cost q)) {program : OracleComp spec α}
+    {n : ℕ} (h : IsCostBounded cost program n) (s : σ) :
+    IsQueryBounded ((interpret handler program).run s) n := by
+  induction h generalizing s with
+  | pure a n => exact .pure (a, s) _
+  | liftBind q cont n _ ih =>
+    change IsQueryBounded ((interpret handler (OracleComp.query q >>= cont)).run s) _
+    simp only [interpret_bind, interpret_query, StateT.run_bind]
+    rw [Nat.add_comm]
+    exact (hhandler q s).bind fun result => ih result.1 result.2
+
+end IsCostBounded
 
 /-- A structural budget bounds the external calls of the program run with private
 randomness, for every size bound on its queries. -/
@@ -98,21 +159,6 @@ theorem IsQueryBounded.hasQueryBounds {Query : Type} {Response : Query → Type}
     rw [show 1 + n = n + 1 by omega] at hbind
     exact hbind
 
-/-- A program run through a stateful handler, each of whose calls makes at most `k` calls to the
-target oracle, makes at most `n * k` target calls when the program makes at most `n` calls. -/
-theorem IsQueryBounded.run_interpret {κ : Type u} {target : OracleSpec.{u, v} κ} {σ : Type v}
-    {handler : (q : ι) → StateT σ (OracleComp target) (spec q)} {k : ℕ}
-    (hhandler : ∀ q s, IsQueryBounded ((handler q).run s) k) {program : OracleComp spec α}
-    {n : ℕ} (h : IsQueryBounded program n) (s : σ) :
-    IsQueryBounded ((interpret handler program).run s) (n * k) := by
-  induction h generalizing s with
-  | pure a n => exact .pure (a, s) _
-  | liftBind q cont n _ ih =>
-    change IsQueryBounded ((interpret handler (OracleComp.query q >>= cont)).run s) _
-    simp only [interpret_bind, interpret_query, StateT.run_bind]
-    rw [show (n + 1) * k = k + n * k by ring]
-    exact (hhandler q s).bind fun result => ih result.1 result.2
-
 /-- **Presampling a handler's randomness.** A handler that draws one sample per call from
 `source` can instead read the samples from a list of independent draws, made in advance: for a
 program making at most `n` calls, `n` presampled draws give the same law of the result and the
diff --git a/Complexity/Languages/Probabilistic/UntilBad.lean b/Complexity/Languages/Probabilistic/UntilBad.lean
index 0c8c11a62c..c477d0b062 100644
--- a/Complexity/Languages/Probabilistic/UntilBad.lean
+++ b/Complexity/Languages/Probabilistic/UntilBad.lean
@@ -20,14 +20,17 @@ the two interpretations of any program give the same probability to every outcom
 final state (`IdenticalUntilBad.run_apply`). Consequently, an experiment that continues the run
 accepts with the first handler at most as often as with the second, plus the probability of
 reaching a bad state ([BonehShoup2023], Theorem 4.7, the difference lemma), with no bound on the
-program's number of calls (`IdenticalUntilBad.bind_apply_le`).
+program's number of calls (`IdenticalUntilBad.bind_apply_le`). Both handlers reach a bad state with
+the same probability (`IdenticalUntilBad.bad_eq`), so the two acceptance probabilities differ by
+at most that probability (`IdenticalUntilBad.abs_sub_le`), and the bad event may be bounded in
+whichever run is easier.
 
-The probability of reaching a bad state is bounded by summing over the calls: if each call from a
-good state turns bad with probability at most `budget s`, and each call raises the budget by at
-most `δ`, then a program making at most `n` calls reaches a bad state with probability at most
-`n · budget s + C(n, 2) · δ` (`toOuterMeasure_bad_le`). This is the union bound for a growing
-collision set, such as a random oracle that is programmed at points that may already be
-defined.
+The probability of reaching a bad state is bounded by summing over the calls: if each call `q`
+from a good state turns bad with probability at most `cost q · budget s`, and each call raises the
+budget by at most `δ`, then a program making at most `n` calls, whose calls cost at most `k`,
+reaches a bad state with probability at most `k · (budget s + n · δ)` (`toOuterMeasure_bad_le`).
+This is the union bound for a growing collision set, such as a random oracle that is programmed,
+at some calls only, at points that may already be defined.
 
 ## Main definitions
 
@@ -37,6 +40,9 @@ defined.
 
 * `Cslib.OracleComp.IdenticalUntilBad.run_apply`: equal outcome probabilities at good states.
 * `Cslib.OracleComp.IdenticalUntilBad.bind_apply_le`: the difference lemma.
+* `Cslib.OracleComp.IdenticalUntilBad.bad_eq`, `Cslib.OracleComp.IdenticalUntilBad.abs_sub_le`:
+  the bad event has the same probability under both handlers, and the two-sided difference
+  lemma.
 * `Cslib.OracleComp.toOuterMeasure_bad_le`: the accumulated probability of a bad state.
 
 ## References
@@ -136,32 +142,90 @@ theorem bind_apply_le (h : IdenticalUntilBad first second bad) (program : Oracle
     rw [Set.indicator_of_notMem hgood, add_zero, show x = (x.1, x.2) from rfl,
       h.run_apply program s x.1 x.2 hx]
 
+/-- Identical until bad is symmetric. -/
+theorem symm (h : IdenticalUntilBad first second bad) : IdenticalUntilBad second first bad where
+  agree q s hs a s' hs' := (h.agree q s hs a s' hs').symm
+  absorb_first := h.absorb_second
+  absorb_second := h.absorb_first
+
+/-- A run gives the bad states and the good states total probability one. -/
+private theorem toOuterMeasure_bad_add_good (p : PMF (α × σ)) :
+    p.toOuterMeasure {x | bad x.2} + p.toOuterMeasure {x | ¬bad x.2} = 1 := by
+  classical
+  simp only [PMF.toOuterMeasure_apply]
+  rw [← ENNReal.tsum_add, ← p.tsum_coe]
+  refine tsum_congr fun x => ?_
+  by_cases hx : bad x.2
+  · rw [Set.indicator_of_mem (show x ∈ {x : α × σ | bad x.2} from hx),
+      Set.indicator_of_notMem (show x ∉ {x : α × σ | ¬bad x.2} from fun h => h hx), add_zero]
+  · rw [Set.indicator_of_notMem (show x ∉ {x : α × σ | bad x.2} from hx),
+      Set.indicator_of_mem (show x ∈ {x : α × σ | ¬bad x.2} from hx), zero_add]
+
+/-- Handlers that agree until a bad state reach a bad state with the same probability. -/
+theorem bad_eq (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) (s : σ) :
+    ((interpret first program).run s).toOuterMeasure {x | bad x.2} =
+      ((interpret second program).run s).toOuterMeasure {x | bad x.2} := by
+  have hgood : ((interpret first program).run s).toOuterMeasure {x | ¬bad x.2} =
+      ((interpret second program).run s).toOuterMeasure {x | ¬bad x.2} := by
+    simp only [PMF.toOuterMeasure_apply]
+    refine tsum_congr fun x => ?_
+    by_cases hx : bad x.2
+    · rw [Set.indicator_of_notMem (show x ∉ {x : α × σ | ¬bad x.2} from fun h => h hx),
+        Set.indicator_of_notMem (show x ∉ {x : α × σ | ¬bad x.2} from fun h => h hx)]
+    · rw [Set.indicator_of_mem (show x ∈ {x : α × σ | ¬bad x.2} from hx),
+        Set.indicator_of_mem (show x ∈ {x : α × σ | ¬bad x.2} from hx),
+        show x = (x.1, x.2) from rfl, h.run_apply program s x.1 x.2 hx]
+  have hfirst := toOuterMeasure_bad_add_good (bad := bad) ((interpret first program).run s)
+  have hsecond := toOuterMeasure_bad_add_good (bad := bad) ((interpret second program).run s)
+  rw [hgood] at hfirst
+  exact (ENNReal.add_left_inj (Probability.PMF.toOuterMeasure_ne_top _ _)).mp
+    (hfirst.trans hsecond.symm)
+
+/-- **The difference lemma, two-sided** ([BonehShoup2023], Theorem 4.7): any experiment continuing
+the run of a program accepts with probabilities, under the two handlers, that differ by at most the
+probability of reaching a bad state, which is the same under both. -/
+theorem abs_sub_le (h : IdenticalUntilBad first second bad) (program : OracleComp spec α)
+    (s : σ) {β : Type} (next : α × σ → PMF β) (b : β) :
+    |(((interpret first program).run s).bind next b).toReal -
+        (((interpret second program).run s).bind next b).toReal| ≤
+      (((interpret first program).run s).toOuterMeasure {x | bad x.2}).toReal := by
+  have hle := h.bind_apply_le program s next b
+  have hle' := h.symm.bind_apply_le program s next b
+  rw [← h.bad_eq] at hle'
+  have hbad := Probability.PMF.toOuterMeasure_ne_top ((interpret first program).run s)
+    {x | bad x.2}
+  have h1 := ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨PMF.apply_ne_top _ _, hbad⟩) hle
+  have h2 := ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨PMF.apply_ne_top _ _, hbad⟩) hle'
+  rw [ENNReal.toReal_add (PMF.apply_ne_top _ _) hbad] at h1 h2
+  exact abs_sub_le_iff.mpr ⟨by linarith, by linarith⟩
+
 end IdenticalUntilBad
 
-/-- **The accumulated probability of a bad state.** If each call from a good state turns bad with
-probability at most `budget s` and raises the budget by at most `δ`, a program making at most `n`
-calls from a good state reaches a bad state with probability at most
-`n · budget s + C(n, 2) · δ`. -/
+/-- **The accumulated probability of a bad state.** Let each call `q` from a good state turn bad
+with probability at most `cost q · budget s`, and raise the budget by at most `δ`. Then a program
+making at most `n` calls, whose calls cost at most `k`, reaches a bad state from a good state with
+probability at most `k · (budget s + n · δ)`. -/
 theorem toOuterMeasure_bad_le {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop}
-    (budget : σ → ℝ≥0∞) (δ : ℝ≥0∞)
-    (hstep : ∀ q s, ¬bad s → (handler q s).toOuterMeasure {x | bad x.2} ≤ budget s)
+    (cost : ι → ℕ) (budget : σ → ℝ≥0∞) (δ : ℝ≥0∞)
+    (hstep : ∀ q s, ¬bad s → (handler q s).toOuterMeasure {x | bad x.2} ≤ cost q * budget s)
     (hgrow : ∀ q s, ¬bad s → ∀ x ∈ (handler q s).support, ¬bad x.2 →
       budget x.2 ≤ budget s + δ)
-    {program : OracleComp spec α} {n : ℕ} (hn : IsQueryBounded program n) {s : σ}
-    (hs : ¬bad s) :
+    {program : OracleComp spec α} {n k : ℕ} (hn : IsQueryBounded program n)
+    (hk : IsCostBounded cost program k) {s : σ} (hs : ¬bad s) :
     ((interpret handler program).run s).toOuterMeasure {x | bad x.2} ≤
-      n * budget s + n.choose 2 * δ := by
-  induction hn generalizing s with
+      k * (budget s + n * δ) := by
+  induction hn generalizing s k with
   | pure a n =>
     rw [show (interpret handler (PFunctor.FreeM.pure a)).run s = PMF.pure (a, s) from rfl,
       PMF.toOuterMeasure_pure_apply, ite_eq_right (show (a, s) ∉ {x : α × σ | bad x.2} from hs)]
     exact zero_le
   | liftBind q cont n _ ih =>
     classical
+    obtain ⟨hle, hcont⟩ := IsCostBounded.liftBind_iff.mp hk
     change ((handler q s).bind fun y => (interpret handler (cont y.1)).run y.2).toOuterMeasure
       {x | bad x.2} ≤ _
     rw [PMF.toOuterMeasure_bind_apply]
-    set K : ℝ≥0∞ := n * (budget s + δ) + n.choose 2 * δ
+    set K : ℝ≥0∞ := (k - cost q : ℕ) * (budget s + δ + n * δ)
     have hterm (y : spec q × σ) : (handler q s) y *
         ((interpret handler (cont y.1)).run y.2).toOuterMeasure {x | bad x.2} ≤
         (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := by
@@ -173,7 +237,7 @@ theorem toOuterMeasure_bad_le {handler : (q : ι) → StateT σ PMF (spec q)} {b
           exact (Probability.PMF.toOuterMeasure_le_one _ _).trans le_self_add
         · have : y ∉ {x : spec q × σ | bad x.2} := hy
           rw [Set.indicator_of_notMem this, zero_add]
-          refine (ih y.1 hy).trans ?_
+          refine (ih y.1 (hcont y.1) hy).trans ?_
           simp only [K]
           gcongr
           exact hgrow q s hs y hmem hy
@@ -190,9 +254,14 @@ theorem toOuterMeasure_bad_le {handler : (q : ι) → StateT σ PMF (spec q)} {b
           by_cases hy : y ∈ {x : spec q × σ | bad x.2}
           · rw [Set.indicator_of_mem hy, Set.indicator_of_mem hy, Pi.one_apply, mul_one]
           · rw [Set.indicator_of_notMem hy, Set.indicator_of_notMem hy, mul_zero]
-      _ ≤ budget s + K := add_le_add (hstep q s hs) le_rfl
-      _ = (n + 1 : ℕ) * budget s + (n + 1).choose 2 * δ := by
-          simp only [K, Nat.choose_succ_succ', Nat.choose_one_right, Nat.cast_add, Nat.cast_one]
-          ring
+      _ ≤ cost q * (budget s + (n + 1 : ℕ) * δ) +
+            (k - cost q : ℕ) * (budget s + (n + 1 : ℕ) * δ) := by
+          refine add_le_add ((hstep q s hs).trans ?_) (le_of_eq ?_)
+          · gcongr
+            exact le_self_add
+          · simp only [K, Nat.cast_add, Nat.cast_one]
+            ring
+      _ = k * (budget s + (n + 1 : ℕ) * δ) := by
+          rw [← add_mul, ← Nat.cast_add, Nat.add_sub_cancel' hle]
 
 end Cslib.OracleComp
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index b78011befd..599c2dd7e4 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -121,6 +121,7 @@ import ComplexityTests.Crypto.SchnorrDiscreteLog
 import ComplexityTests.Crypto.SigmaIdentification
 import ComplexityTests.Crypto.SigmaProtocol
 import ComplexityTests.Crypto.Signature
+import ComplexityTests.Crypto.UntilBad
 import ComplexityTests.Crypto.ZeroKnowledge
 import ComplexityTests.CyclicFeedback
 import ComplexityTests.DataStructure
diff --git a/ComplexityTests/Crypto/FiatShamir.lean b/ComplexityTests/Crypto/FiatShamir.lean
index 8c2d0eaa74..9b2afad596 100644
--- a/ComplexityTests/Crypto/FiatShamir.lean
+++ b/ComplexityTests/Crypto/FiatShamir.lean
@@ -100,22 +100,22 @@ theorem succProbability_knower : Game.succProbability (eufCmaGame scheme knower)
   simp only [hverify]
   simp
 
-/-- The knowing forger makes one call. -/
-theorem knower_isQueryBounded (u r : ZMod 11) : OracleComp.IsQueryBounded (knower.forge u r) 1 :=
-  .liftBind _ _ 0 fun _ => .pure _ 0
+/-- The knowing forger makes no signing call and one hash call. -/
+theorem knower_callBounded : knower.CallBounded 0 1 :=
+  fun _ _ => ⟨.liftBind _ _ 0 fun _ => .pure _ 0, .liftBind _ _ 0 fun _ => .pure _ 0⟩
 
 /-- The reduction built from the knowing forger computes a discrete logarithm with probability at
-least `81 / 242`: the security bound reads `1 ≤ 0 + 2 / 11 + √(2 · ε')`. -/
+least `81 / 242`: the security bound, with no signing call and one hash call, reads
+`1 ≤ 0 + 2 / 11 + √(2 · ε')`. -/
 example : (81 / 242 : ℝ) ≤ Game.succProbability (oneWayGame (schnorrKeyGen (2 : ZMod 11))
     (fun α u => α • (2 : ZMod 11) = u)
     (FiatShamir.reduction (schnorr ι (2 : ZMod 11))
       (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod 11) (ZMod 11) 2) id ι)
-      (linearExtract ι) knower 1)) := by
+      (linearExtract ι) knower 0 1)) := by
   have h := succProbability_eufCmaGame_le (δ := 11⁻¹)
     (fun _ h => mem_support_schnorrKeyGen h)
     ((schnorr_specialSoundness (ι := ι) (g := (2 : ZMod 11))).specialSoundOn (schnorrKeyGen 2))
-    schnorr_specialHVZK (fun key _ t => commit_unpredictable key t) knower
-    knower_isQueryBounded
+    schnorr_specialHVZK (fun key _ t => commit_unpredictable key t) knower knower_callBounded
   have hknower : Game.succProbability (eufCmaGame (fiatShamir (M := Bool)
       (schnorr ι (2 : ZMod 11)) (schnorrKeyGen 2)) knower) = 1 := succProbability_knower
   rw [hknower, ZMod.card] at h
@@ -123,10 +123,10 @@ example : (81 / 242 : ℝ) ≤ Game.succProbability (oneWayGame (schnorrKeyGen (
     (fun α u => α • (2 : ZMod 11) = u)
     (FiatShamir.reduction (schnorr ι (2 : ZMod 11))
       (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod 11) (ZMod 11) 2) id ι)
-      (linearExtract ι) knower 1)) : ℝ) with hε
+      (linearExtract ι) knower 0 1)) : ℝ) with hε
   have hε0 : 0 ≤ ε := NNReal.coe_nonneg _
-  have hchoose : ((Nat.choose 1 2 : ℕ) : ℝ) = 0 := by norm_num
-  rw [hchoose, zero_mul, zero_add, Nat.cast_one, show (1 : ℝ) + 1 = 2 by norm_num] at h
+  simp only [Nat.cast_zero, zero_mul, zero_add, Nat.cast_one,
+    show (1 : ℝ) + 1 = 2 by norm_num] at h
   have hsqrt : (9 / 11 : ℝ) ≤ √(2 * ε) := by
     simp only [NNReal.coe_one, Nat.cast_ofNat] at h
     linarith
diff --git a/ComplexityTests/Crypto/UntilBad.lean b/ComplexityTests/Crypto/UntilBad.lean
new file mode 100644
index 0000000000..17e844f613
--- /dev/null
+++ b/ComplexityTests/Crypto/UntilBad.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Crypto.Game.UntilBad
+import Complexity.Probability.PMF
+
+/-!
+# Tests for identical-until-bad hops
+
+One handler answers a fair bit and raises a flag when the bit is `true`; the other draws the same
+bit for the flag but always answers `false`. They agree until the flag is raised. For the program
+that asks once and returns the answer, the difference lemma is tight: the success probabilities
+are `1 / 2` and `0`, and the flag is raised with probability `1 / 2` under both handlers.
+-/
+
+namespace ComplexityTests.Crypto.UntilBad
+
+open Cslib Cslib.Probability Cslib.OracleComp
+
+/-- Answer a fair bit, raising the flag when it is `true`. -/
+noncomputable def honest (_ : Unit) : StateT Bool PMF Bool := fun s =>
+  (PMF.uniformOfFintype Bool).map fun b => (b, s || b)
+
+/-- Answer `false`, raising the flag on a fair bit. -/
+noncomputable def silent (_ : Unit) : StateT Bool PMF Bool := fun s =>
+  (PMF.uniformOfFintype Bool).map fun b => (false, s || b)
+
+/-- The two handlers agree until the flag is raised. -/
+theorem identicalUntilBad :
+    IdenticalUntilBad (spec := fun _ : Unit => Bool) honest silent fun s => s = true where
+  agree q s hs a s' hs' := by
+    simp only [Bool.not_eq_true] at hs hs'
+    subst hs hs'
+    cases a <;> simp [honest, silent, PMF.uniformOfFintype_apply]
+  absorb_first q s hs x hx := by
+    obtain ⟨b, -, rfl⟩ := (_root_.PMF.mem_support_map_iff _ _ _).mp hx
+    simp [hs]
+  absorb_second q s hs x hx := by
+    obtain ⟨b, -, rfl⟩ := (_root_.PMF.mem_support_map_iff _ _ _).mp hx
+    simp [hs]
+
+/-- Ask once and return the answer. -/
+abbrev askOnce : OracleComp (fun _ : Unit => Bool) Bool := query ()
+
+/-- The flag is raised with probability `1 / 2`. -/
+theorem toOuterMeasure_bad :
+    ((interpret honest askOnce).run false).toOuterMeasure {x | x.2 = true} = 1 / 2 := by
+  classical
+  rw [askOnce, interpret_query]
+  change ((honest ()) false).toOuterMeasure {x | x.2 = true} = 1 / 2
+  rw [honest, _root_.PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_uniformOfFintype]
+  norm_num
+  rw [Finset.card_eq_one.mpr ⟨true, by ext a; cases a <;> simp⟩]
+  simp
+
+/-- The difference lemma is tight here: success `1 / 2` against `0`, with bad probability `1 / 2`
+under both handlers. -/
+example : |(((interpret honest askOnce).run false).bind (fun x => PMF.pure x.1) true).toReal -
+    (((interpret silent askOnce).run false).bind (fun x => PMF.pure x.1) true).toReal| ≤ 1 / 2 := by
+  have h := identicalUntilBad.abs_sub_le askOnce false (fun x => PMF.pure x.1) true
+  rwa [toOuterMeasure_bad, ENNReal.toReal_div, ENNReal.toReal_one, ENNReal.toReal_ofNat] at h
+
+example : ((interpret silent askOnce).run false).toOuterMeasure {x | x.2 = true} = 1 / 2 := by
+  rw [← identicalUntilBad.bad_eq, toOuterMeasure_bad]
+
+end ComplexityTests.Crypto.UntilBad
diff --git a/ROADMAP.md b/ROADMAP.md
index 28d46d6ae6..79b6c39d27 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -1190,7 +1190,8 @@ Jukna coverage below is an additional target beyond the V1 port:
   presampled answers. [Fiat–Shamir signatures](Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean)
   in the [random-oracle model](Complexity/Crypto/Protocols/Signature/RandomOracle.lean) are
   correct and, exactly, EUF-CMA secure with the bound
-  `C(Q, 2) · δ + (Q + 1)/N + √((Q + 1) · ε')` of Theorem 19.16 and Equation 19.21, by the
+  `Qs · (Qs + Qro) · δ + (Qro + 1)/N + √((Qro + 1) · ε')` of Theorem 19.16 and Equation 19.21,
+  by the
   [difference lemma](Complexity/Languages/Probabilistic/UntilBad.lean), presampling and forking.
   Open (see #640): computational Schnorr signatures under discrete log for strict PPT forgers,
   and security against eavesdropping in the strict-PPT model, where simulating transcripts needs