feat(crypto): Fiat–Shamir bound with separate signing and hash budgets (#581 3b-i follow-up)

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

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

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. -/

Complexity/Languages/Probabilistic/QueryCount.lean

@@ -15,27 +15,32 @@ 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
 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