From 2a015dc05069204ec13cc448633eb898c12de127 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 14:20:53 +0000
Subject: [PATCH 1/3] feat(Crypto/MAC): complete Carter-Wegman PRF-pad
 admissibility and multi-query fresh-nonce security (#736)

---
 .../Crypto/Protocols/MAC/CarterWegman.lean    | 873 +++++++++++++++++-
 ComplexityTests/Crypto/CarterWegman.lean      |  20 +
 ROADMAP.md                                    |   5 +-
 3 files changed, 875 insertions(+), 23 deletions(-)

diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean
index 30d086c312..9d6fb6d2e4 100644
--- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean
+++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean
@@ -14,8 +14,13 @@ public import Complexity.Probability.BitString.SubsetSum
 public import Complexity.Probability.HashFamily
 public import Complexity.Probability.HashFamily.Polynomial
 public import Complexity.Probability.PairwiseIndependentHash.Universal
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
+import Complexity.Computability.Probabilistic.Oracle.Composition
+import Complexity.Crypto.Negligible.Basic
 import Complexity.Probability.PMF.Bind
 import Complexity.Probability.PMF.Uniform
+import Complexity.Tactic.PPT
+import Complexity.Tactic.PolyTime
 
 /-!
 # Carter–Wegman message authentication codes from Δ-universal hashing
@@ -67,21 +72,36 @@ This module formalizes:
    (`maskedOneTimeGame`, `padDistinguisher`, `maskedOneTimeGame_toReal_le`,
    `maskedOneTimeGame_toReal_le_add_advantage`, `prfPadDist`, `prfOneTimeGame`,
    `prfOneTimeStrongGame`, `prfPadDistinguisher`, `prfOneTimeGame_le`,
-   `prfOneTimeStrongGame_le`, `prfOneTimeGame_ofProbComp_le`)**: replacing the uniform pad
-   `r ← PMF.uniformOfFintype Y` with any pad distribution `padDist : PMF Y` bounds the real forgery
-   probability by `ε.toReal` plus the distinguishing advantage of `padDistinguisher` between
+   `prfOneTimeStrongGame_le`, `prfOneTimeGame_ofProbComp_le`, `isOraclePPT_prfPadDistinguisher`,
+   `wordProbPadTest`, `isPPTOn_wordProbPadTest`,
+   `isOraclePPT_prfPadDistinguisher_wordProbPadTest`,
+   `PseudorandomFunction.negligible_prfOneTimeGame`,
+   `PseudorandomFunction.negligible_prfOneTimeStrongGame`,
+   `PseudorandomFunction.negligible_prfOneTimeGame_wordProbPadTest`,
+   `PseudorandomFunction.negligible_prfOneTimeStrongGame_wordProbPadTest`)**: replacing the uniform
+   pad `r ← PMF.uniformOfFintype Y` with any pad distribution `padDist : PMF Y` bounds the real
+   forgery probability by `ε.toReal` plus the distinguishing advantage of `padDistinguisher` between
    `padDist` and `PMF.uniformOfFintype Y` (after [BonehShoup2023], Section 7.4). In the one-query,
-   fixed-nonce case (after [BonehShoup2023], Section 7.4) where `Y = BitString n` and the pad is
-   generated by evaluating `family` at the fixed nonce `List.replicate n false` under a uniform
-   `n`-bit key (`prfPadDist family n`), the single-query `OracleDistinguisher` adapter
-   `prfPadDistinguisher` realizes the real and ideal pad experiments inside `prfRealGame` and
-   `prfIdealGame` at each parameter `n`, giving an exact single-query reduction that bounds
-   one-time forgery probability by `ε.toReal` plus the concrete PRF distinguishing advantage at
-   `n`. Certifying `IsOraclePPT encBool` admissibility of `prfPadDistinguisher` for uniform
-   word-level forger and hash families, deriving the asymptotic negligible-advantage corollary from
-   `PseudorandomFunction family`, and treating the many-time fresh-nonce PRF-masked Carter–Wegman
-   MAC of [BonehShoup2023], Section 7.4 remain open.
-6. **Concrete instantiations** for Carter–Wegman polynomial hashing (`xpolyHash`, bound
+   fixed-nonce case where `Y = BitString n` and the pad is generated by evaluating `family` at the
+   fixed nonce `List.replicate n false` under a uniform `n`-bit key (`prfPadDist family n`), the
+   single-query `OracleDistinguisher` adapter `prfPadDistinguisher` realizes the real and ideal pad
+   experiments inside `prfRealGame` and `prfIdealGame` at each parameter `n`, is uniformly strict
+   oracle-PPT (`IsOraclePPT encBool`) whenever the pad test is uniformly strict PPT, and yields
+   negligible forgery probability under `PseudorandomFunction family` and `Negligible ε`.
+6. **Multi-query fresh-nonce PRF-masked Carter–Wegman MAC (`counterSeqHandler`,
+   `maskedCounterSlotGame`, `maskedCounterGame`, `maskedCounterStrongGame`,
+   `counterPadSeqDistinguisher`, `prfPadSeqDist`, `prfCounterSlotGame`, `prfCounterGame`,
+   `prfCounterStrongGame`, `prfMultiPadDistinguisher`, `prfCounterSlotGame_le`,
+   `prfCounterGame_le`, `prfCounterStrongGame_le`, `isOraclePPT_prfMultiPadDistinguisher`,
+   `PseudorandomFunction.negligible_prfCounterSlotGame`,
+   `PseudorandomFunction.negligible_prfCounterGame`,
+   `PseudorandomFunction.negligible_prfCounterStrongGame`)**: when the `i`-th signing query uses a
+   PRF pad `BitString.ofList n (prfOracle family n key (nonce n i))` at pairwise distinct `n`-bit
+   nonces `nonce n 0, ..., nonce n (Q n - 1)`, any `Q n`-query-bounded adaptive `CounterForger` has
+   forgery probability at most `ε.toReal` plus the concrete `Q n`-query PRF distinguishing advantage
+   of `prfMultiPadDistinguisher Q nonce test`, and negligible forgery probability when `family` is a
+   `PseudorandomFunction` and `ε` is `Negligible` ([BonehShoup2023], Section 7.4, Theorem 7.4).
+7. **Concrete instantiations** for Carter–Wegman polynomial hashing (`xpolyHash`, bound
    `(ℓ + 1) / |F|`), Boolean-matrix linear hashing (`BitString.LinearHash.hash`, bound `2⁻ᵐ`),
    subset-sum hashing (`BitString.SubsetSum.hash`, bound `1 / |G|`), and pairwise independent
    hash families (`IsPairwiseIndependentHash`, bound `1 / |Y|`).
@@ -102,13 +122,25 @@ This module formalizes:
   Carter–Wegman experiments.
 * `Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame`,
   `Cslib.Crypto.Protocols.CarterWegman.padDistinguisher`,
-  `Cslib.Crypto.Protocols.CarterWegman.probPadTest`: arbitrary-pad one-time Carter–Wegman
+  `Cslib.Crypto.Protocols.CarterWegman.probPadTest`,
+  `Cslib.Crypto.Protocols.CarterWegman.wordProbPadTest`: arbitrary-pad one-time Carter–Wegman
   experiment and its induced `PMF` and `ProbComp` pad distinguishers.
 * `Cslib.Crypto.Protocols.CarterWegman.prfPadDist`,
   `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame`,
   `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame`,
   `Cslib.Crypto.Protocols.CarterWegman.prfPadDistinguisher`: one-query, fixed-nonce PRF-masked
   Carter–Wegman experiments and the single-query `OracleDistinguisher` adapter.
+* `Cslib.Crypto.Protocols.CarterWegman.counterSeqHandler`,
+  `Cslib.Crypto.Protocols.CarterWegman.maskedCounterSlotGame`,
+  `Cslib.Crypto.Protocols.CarterWegman.maskedCounterGame`,
+  `Cslib.Crypto.Protocols.CarterWegman.maskedCounterStrongGame`,
+  `Cslib.Crypto.Protocols.CarterWegman.counterPadSeqDistinguisher`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfPadSeqDist`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfCounterSlotGame`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfCounterGame`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfCounterStrongGame`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfMultiPadDistinguisher`: multi-query fresh-nonce
+  PRF-masked Carter–Wegman experiments and the `Q`-query `OracleDistinguisher` adapter.
 
 ## Main results
 
@@ -131,9 +163,28 @@ This module formalizes:
   `Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfPadDistinguisher`,
   `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le`,
   `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_le`,
-  `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le`: exact single-query reduction
-  to `prfRealGame`/`prfIdealGame` in the one-query, fixed-nonce case (after Boneh–Shoup
+  `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le`,
+  `Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfPadDistinguisher`,
+  `Cslib.Crypto.Protocols.CarterWegman.isPPTOn_wordProbPadTest`,
+  `Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfPadDistinguisher_wordProbPadTest`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeGame`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeGame_wordProbPadTest`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame_wordProbPadTest`: single-query
+  PRF-pad reduction, `IsOraclePPT` admissibility, and asymptotic security (after Boneh–Shoup
   Section 7.4).
+* `Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_counterSeqHandler`,
+  `Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfMultiPadDistinguisher`,
+  `Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfMultiPadDistinguisher`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfCounterSlotGame_le`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfCounterGame_le`,
+  `Cslib.Crypto.Protocols.CarterWegman.prfCounterStrongGame_le`,
+  `Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfMultiPadDistinguisher`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfCounterSlotGame`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame`,
+  `Cslib.Crypto.PseudorandomFunction.negligible_prfCounterStrongGame`: multi-query fresh-nonce
+  PRF-masked Carter–Wegman security, `IsOraclePPT` admissibility, and asymptotic security
+  (Boneh–Shoup Section 7.4, Theorem 7.4).
 * `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_xpolyHash_le`,
   `Cslib.Crypto.Protocols.CarterWegman.counterGame_xpolyHash_le`,
   `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_linearHash_le`,
@@ -156,8 +207,8 @@ This module formalizes:
 
 namespace Cslib.Crypto.Protocols.CarterWegman
 
-open Cslib.Probability Cslib.Probability.PMF
-open scoped ENNReal
+open Cslib.Probability Cslib.Probability.PMF Turing.MultiTapeTM
+open scoped NNReal ENNReal
 
 /-! ### Core Carter–Wegman signing, verification, and pad resampling -/
 
@@ -935,8 +986,792 @@ theorem prfOneTimeStrongGame_ofProbComp_le {n : ℕ} {seed : ProbComp K}
   rw [prfOneTimeStrongGame_eq_prfOneTimeGame]
   exact prfOneTimeGame_ofProbComp_le hh hε family query forge
 
+private theorem ofList_take (n : ℕ) (w : List Bool) :
+    BitString.ofList n (w.take n) = BitString.ofList n w := by
+  funext i
+  simp [BitString.ofList, i.isLt]
+
+/-- `prfPadDistinguisher test` is uniformly strict oracle-PPT (`IsOraclePPT encBool`) whenever
+running `test n` on the `n`-bit view of a raw pad word is uniformly strict PPT in `(n, word)`. -/
+theorem isOraclePPT_prfPadDistinguisher
+    {test : (k : ℕ) → BitString k → ProbComp Bool}
+    (htest : IsPPTOn (encPair encUnary encBits) encBool
+      (fun p : ℕ × List Bool => test p.1 (BitString.ofList p.1 p.2))) :
+    IsOraclePPT encBool (prfPadDistinguisher test) := by
+  have heq : prfPadDistinguisher test =
+      (fun n _ => do
+        let reply ← List.take n <$> ProbOracleComp.query ((), List.replicate n false)
+        ProbOracleComp.sample (test n (BitString.ofList n reply))) := by
+    funext n _
+    simp [prfPadDistinguisher, ofList_take]
+  rw [heq]
+  have hq : IsOraclePPTOn (encPair encUnary encBits) encBits
+      (fun p : ℕ × List Bool =>
+        List.take p.1 <$> ProbOracleComp.query ((), List.replicate p.1 false)) :=
+    IsOraclePPTOn.query_take () (by polytime) (by polytime)
+  exact (hq.bind_with ((htest.preprocess
+    (prepare := fun p : (ℕ × List Bool) × List Bool => (p.1.1, p.2))
+    (by polytime)).isOraclePPTOn)).isOraclePPT
+
+/-- Executable `ProbComp` one-time pad test induced by a uniform word-level hash-key sampler `seed`,
+hash evaluator `hash`, signing query `query`, and forgery program `forge`: at security parameter `n`
+and pad `r : BitString n`, it runs `probPadTest` with digest `BitString.ofList n (hash n k m)` and
+candidate tag `BitString.ofList n p.2`. -/
+def wordProbPadTest (seed : ℕ → ProbComp (List Bool))
+    (hash : ℕ → List Bool → List Bool → List Bool)
+    (query : ℕ → ProbComp (List Bool))
+    (forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool))
+    (n : ℕ) (r : BitString n) : ProbComp Bool :=
+  probPadTest (seed n) (fun k m => BitString.ofList n (hash n k m)) (query n)
+    (fun m t => do
+      let p ← forge n m (List.ofFn t)
+      return (p.1, BitString.ofList n p.2)) r
+
+@[simp]
+theorem eval_wordProbPadTest (seed : ℕ → ProbComp (List Bool))
+    (hash : ℕ → List Bool → List Bool → List Bool)
+    (query : ℕ → ProbComp (List Bool))
+    (forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool))
+    (n : ℕ) (r : BitString n) :
+    ProbComp.eval (wordProbPadTest seed hash query forge n r) =
+      padDistinguisher (ProbComp.eval (seed n))
+        (fun k m => BitString.ofList n (hash n k m))
+        (OneTimeForger.ofProbComp (query n) (fun m t => do
+          let p ← forge n m (List.ofFn t)
+          return (p.1, BitString.ofList n p.2))) r :=
+  eval_probPadTest _ _ _ _ r
+
+/-- If `seed`, `hash`, `query`, and `forge` are uniformly polynomial-time / strict PPT in their
+encoded inputs, then `wordProbPadTest` on the `n`-bit view of a raw pad word is uniformly strict
+PPT. -/
+theorem isPPTOn_wordProbPadTest
+    {seed : ℕ → ProbComp (List Bool)}
+    {hash : ℕ → List Bool → List Bool → List Bool}
+    {query : ℕ → ProbComp (List Bool)}
+    {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)}
+    (hseed : IsPPTOn encUnary encBits seed)
+    (hhash : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2)
+      (encPair encUnary (encPair encBits encBits)) encBits)
+    (hquery : IsPPTOn encUnary encBits query)
+    (hforge : IsPPTOn (encPair encUnary (encPair encBits encBits))
+      (encPair encBits encBits) (fun p => forge p.1 p.2.1 p.2.2)) :
+    IsPPTOn (encPair encUnary encBits) encBool
+      (fun p : ℕ × List Bool =>
+        wordProbPadTest seed hash query forge p.1 (BitString.ofList p.1 p.2)) := by
+  have hhash_tidy := hhash.tidy
+  have heq : (fun p : ℕ × List Bool =>
+      wordProbPadTest seed hash query forge p.1 (BitString.ofList p.1 p.2)) =
+      fun p : ℕ × List Bool => do
+        let k ← seed p.1
+        let m ← query p.1
+        let out ← forge p.1 m (BitString.listXor p.1 [hash p.1 k m, p.2])
+        return (decide (out.1 ≠ m) &&
+          decide (BitString.listXor p.1 [hash p.1 k out.1, p.2] =
+            BitString.listRow p.1 0 out.2)) := by
+    funext ⟨n, rawPad⟩
+    simp only [wordProbPadTest, probPadTest, sign, verify, bind_assoc, pure_bind,
+      BitString.listXor_pair, BitString.listRow_zero, List.ofFn_injective.eq_iff]
+  rw [heq]
+  ppt
+
+/-- `prfPadDistinguisher (wordProbPadTest seed hash query forge)` is uniformly strict oracle-PPT
+(`IsOraclePPT encBool`) for any uniform polynomial-time / strict-PPT family `(seed, hash, query,
+forge)`. -/
+theorem isOraclePPT_prfPadDistinguisher_wordProbPadTest
+    {seed : ℕ → ProbComp (List Bool)}
+    {hash : ℕ → List Bool → List Bool → List Bool}
+    {query : ℕ → ProbComp (List Bool)}
+    {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)}
+    (hseed : IsPPTOn encUnary encBits seed)
+    (hhash : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2)
+      (encPair encUnary (encPair encBits encBits)) encBits)
+    (hquery : IsPPTOn encUnary encBits query)
+    (hforge : IsPPTOn (encPair encUnary (encPair encBits encBits))
+      (encPair encBits encBits) (fun p => forge p.1 p.2.1 p.2.2)) :
+    IsOraclePPT encBool (prfPadDistinguisher (wordProbPadTest seed hash query forge)) :=
+  isOraclePPT_prfPadDistinguisher (isPPTOn_wordProbPadTest hseed hhash hquery hforge)
+
+/-- **Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman EUF-CMA security**
+(after [BonehShoup2023], Section 7.4): if `family` is a `PseudorandomFunction`, each
+`(seed n, hash n)` is `(ε n)`-almost-Δ-universal with `Negligible ε`, and `test` is a uniformly
+strict-PPT pad test realizing `padDistinguisher (seed n) (hash n) (forger n)` at every `n`, then the
+one-time forgery probability `Game.succProbability (prfOneTimeGame ...)` is `Negligible`. -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeGame
+    {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n}
+    {ε : ℕ → ℝ≥0} (hh : ∀ n, IsDeltaUniversalHash (seed n) (hash n) (ε n))
+    (hε : Negligible ε)
+    (forger : (n : ℕ) → OneTimeForger (M n) (BitString n))
+    (test : (k : ℕ) → BitString k → ProbComp Bool)
+    (htest_eval : ∀ n r,
+      padDistinguisher (seed n) (hash n) (forger n) r = ProbComp.eval (test n r))
+    (htest_ppt : IsPPTOn (encPair encUnary encBits) encBool
+      (fun p : ℕ × List Bool => test p.1 (BitString.ofList p.1 p.2))) :
+    Negligible (fun n =>
+      Game.succProbability (prfOneTimeGame (seed n) family n (hash n) (forger n))) := by
+  have hdist := hprf.secure (prfPadDistinguisher test)
+    (isOraclePPT_prfPadDistinguisher htest_ppt)
+  refine negligible_of_le (hε.add hdist) fun n => ?_
+  rw [← NNReal.coe_le_coe, Game.coe_succProbability, Pi.add_apply, NNReal.coe_add]
+  simpa only [ENNReal.coe_toReal] using
+    prfOneTimeGame_le (hh n) ENNReal.coe_ne_top family (forger n) test (htest_eval n)
+
+/-- **Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman SUF-CMA security**
+(after [BonehShoup2023], Section 7.4). -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame
+    {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n}
+    {ε : ℕ → ℝ≥0} (hh : ∀ n, IsDeltaUniversalHash (seed n) (hash n) (ε n))
+    (hε : Negligible ε)
+    (forger : (n : ℕ) → OneTimeForger (M n) (BitString n))
+    (test : (k : ℕ) → BitString k → ProbComp Bool)
+    (htest_eval : ∀ n r,
+      padDistinguisher (seed n) (hash n) (forger n) r = ProbComp.eval (test n r))
+    (htest_ppt : IsPPTOn (encPair encUnary encBits) encBool
+      (fun p : ℕ × List Bool => test p.1 (BitString.ofList p.1 p.2))) :
+    Negligible (fun n =>
+      Game.succProbability (prfOneTimeStrongGame (seed n) family n (hash n) (forger n))) := by
+  simp only [prfOneTimeStrongGame_eq_prfOneTimeGame]
+  exact hprf.negligible_prfOneTimeGame hh hε forger test htest_eval htest_ppt
+
+/-- **Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman EUF-CMA security for uniform
+word-level families** (after [BonehShoup2023], Section 7.4). -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeGame_wordProbPadTest
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : ℕ → ProbComp (List Bool)}
+    {hash : ℕ → List Bool → List Bool → List Bool}
+    {query : ℕ → ProbComp (List Bool)}
+    {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)}
+    {ε : ℕ → ℝ≥0}
+    (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n))
+      (fun k m => BitString.ofList n (hash n k m)) (ε n))
+    (hε : Negligible ε)
+    (hseed : IsPPTOn encUnary encBits seed)
+    (hhash : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2)
+      (encPair encUnary (encPair encBits encBits)) encBits)
+    (hquery : IsPPTOn encUnary encBits query)
+    (hforge : IsPPTOn (encPair encUnary (encPair encBits encBits))
+      (encPair encBits encBits) (fun p => forge p.1 p.2.1 p.2.2)) :
+    Negligible (fun n =>
+      Game.succProbability
+        (prfOneTimeGame (ProbComp.eval (seed n)) family n
+          (fun k m => BitString.ofList n (hash n k m))
+          (OneTimeForger.ofProbComp (query n) fun m t => do
+            let p ← forge n m (List.ofFn t)
+            return (p.1, BitString.ofList n p.2)))) :=
+  hprf.negligible_prfOneTimeGame hh hε _ (wordProbPadTest seed hash query forge)
+    (fun n r => (eval_wordProbPadTest seed hash query forge n r).symm)
+    (isPPTOn_wordProbPadTest hseed hhash hquery hforge)
+
+/-- **Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman SUF-CMA security for uniform
+word-level families** (after [BonehShoup2023], Section 7.4). -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame_wordProbPadTest
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : ℕ → ProbComp (List Bool)}
+    {hash : ℕ → List Bool → List Bool → List Bool}
+    {query : ℕ → ProbComp (List Bool)}
+    {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)}
+    {ε : ℕ → ℝ≥0}
+    (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n))
+      (fun k m => BitString.ofList n (hash n k m)) (ε n))
+    (hε : Negligible ε)
+    (hseed : IsPPTOn encUnary encBits seed)
+    (hhash : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2)
+      (encPair encUnary (encPair encBits encBits)) encBits)
+    (hquery : IsPPTOn encUnary encBits query)
+    (hforge : IsPPTOn (encPair encUnary (encPair encBits encBits))
+      (encPair encBits encBits) (fun p => forge p.1 p.2.1 p.2.2)) :
+    Negligible (fun n =>
+      Game.succProbability
+        (prfOneTimeStrongGame (ProbComp.eval (seed n)) family n
+          (fun k m => BitString.ofList n (hash n k m))
+          (OneTimeForger.ofProbComp (query n) fun m t => do
+            let p ← forge n m (List.ofFn t)
+            return (p.1, BitString.ofList n p.2)))) := by
+  simp only [prfOneTimeStrongGame_eq_prfOneTimeGame]
+  exact hprf.negligible_prfOneTimeGame_wordProbPadTest hh hε hseed hhash hquery hforge
+
 end PRFPad
 
+/-! ### Multi-query fresh-nonce PRF-masked Carter–Wegman MAC (Boneh–Shoup Section 7.4) -/
+
+section PRFCounter
+
+variable {K M Y : Type} [AddGroup Y]
+
+/-- Counter Carter–Wegman signing handler driven by a deterministic pad sequence `padSeq : ℕ → Y`:
+on the `i`-th query `m` (`i = pads.length`), it uses the pad `r = padSeq pads.length`, appends
+`(m, r)` to the pad log, and returns `sign hash k r m`. -/
+noncomputable def counterSeqHandler (hash : K → M → Y) (k : K) (padSeq : ℕ → Y) (m : M) :
+    StateT (List (M × Y)) PMF Y := fun pads =>
+  let r := padSeq pads.length
+  PMF.pure (sign hash k r m, pads ++ [(m, r)])
+
+@[simp]
+theorem run_counterSeqHandler (hash : K → M → Y) (k : K) (padSeq : ℕ → Y) (m : M)
+    (pads : List (M × Y)) :
+    (counterSeqHandler hash k padSeq m).run pads =
+      PMF.pure (sign hash k (padSeq pads.length) m, pads ++ [(m, padSeq pads.length)]) := rfl
+
+@[simp]
+theorem run_counterRealHandler [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (m : M)
+    (pads : List (M × Y)) :
+    (counterRealHandler hash k m).run pads =
+      (PMF.uniformOfFintype Y).bind fun r => PMF.pure (sign hash k r m, pads ++ [(m, r)]) := rfl
+
+/-- If `prog` makes at most `Q` queries, then running `prog` against `counterSeqHandler` from `pads`
+depends only on the pads `padSeq i` for `i ∈ [pads.length, pads.length + Q)`. -/
+theorem run_interpret_counterSeqHandler_congr {α : Type} (hash : K → M → Y) (k : K)
+    {padSeq₁ padSeq₂ : ℕ → Y} {prog : OracleComp (fun _ : M => Y) α} {Q : ℕ}
+    (hprog : prog.IsQueryBounded Q) (pads : List (M × Y))
+    (hpad : ∀ i, pads.length ≤ i → i < pads.length + Q → padSeq₁ i = padSeq₂ i) :
+    (OracleComp.interpret (counterSeqHandler hash k padSeq₁) prog).run pads =
+      (OracleComp.interpret (counterSeqHandler hash k padSeq₂) prog).run pads := by
+  induction hprog generalizing pads with
+  | pure a Q => rfl
+  | liftBind m cont Q hcont ih =>
+    simp only [OracleComp.interpret_bind, OracleComp.interpret_query, StateT.run_bind,
+      PMF.monad_bind_eq_bind, run_counterSeqHandler, PMF.pure_bind]
+    have h0 : padSeq₁ pads.length = padSeq₂ pads.length :=
+      hpad pads.length (le_refl _) (by omega)
+    rw [h0]
+    exact ih (sign hash k (padSeq₂ pads.length) m) (pads ++ [(m, padSeq₂ pads.length)])
+      fun i hlo hhi => by
+        simp only [List.length_append, List.length_singleton] at hlo hhi
+        exact hpad i (by omega) (by omega)
+
+/-- When `table ← PMF.uniformOfFintype (ι → Y)` is a uniformly random function and `nonce : ℕ → ι`
+is injective on `[pads.length, pads.length + Q)`, running any `Q`-query-bounded program `prog`
+against `counterSeqHandler hash k (fun i => table (nonce i))` from `pads` has the exact same
+distribution as running `prog` against `counterRealHandler hash k` from `pads`. -/
+theorem uniform_bind_run_interpret_counterSeqHandler
+    {ι α : Type} [DecidableEq ι] [Fintype ι] [Fintype Y] [Nonempty Y]
+    (hash : K → M → Y) (k : K) (nonce : ℕ → ι)
+    {prog : OracleComp (fun _ : M => Y) α} {Q : ℕ}
+    (hprog : prog.IsQueryBounded Q) (pads : List (M × Y))
+    (hinj : ∀ i, pads.length ≤ i → i < pads.length + Q →
+      ∀ j, pads.length ≤ j → j < pads.length + Q → nonce i = nonce j → i = j) :
+    ((PMF.uniformOfFintype (ι → Y)).bind fun table =>
+      (OracleComp.interpret (counterSeqHandler hash k (fun i => table (nonce i))) prog).run pads) =
+      (OracleComp.interpret (counterRealHandler hash k) prog).run pads := by
+  induction hprog generalizing pads with
+  | pure a Q =>
+    simp [PMF.monad_pure_eq_pure]
+  | liftBind m cont Q hcont ih =>
+    rw [← PMF.uniformOfFintype_update (γ := Y) (nonce pads.length), PMF.bind_bind]
+    simp only [PMF.bind_map, Function.comp_def, OracleComp.interpret_bind,
+      OracleComp.interpret_query, StateT.run_bind, PMF.monad_bind_eq_bind,
+      run_counterSeqHandler, run_counterRealHandler, PMF.bind_bind, PMF.pure_bind,
+      Function.update_self]
+    congr 1
+    funext r
+    have hcongr (table : ι → Y) :
+        (OracleComp.interpret
+          (counterSeqHandler hash k fun i => Function.update table (nonce pads.length) r (nonce i))
+          (cont (sign hash k r m))).run (pads ++ [(m, r)]) =
+        (OracleComp.interpret
+          (counterSeqHandler hash k fun i => table (nonce i))
+          (cont (sign hash k r m))).run (pads ++ [(m, r)]) := by
+      refine run_interpret_counterSeqHandler_congr hash k (hcont (sign hash k r m))
+        (pads ++ [(m, r)]) fun i hlo hhi => ?_
+      simp only [List.length_append, List.length_singleton] at hlo hhi
+      have hne : nonce i ≠ nonce pads.length := fun heq => by
+        have := hinj i (by omega) (by omega) pads.length (le_refl _) (by omega) heq
+        omega
+      exact Function.update_of_ne hne r table
+    simp only [hcongr]
+    exact ih (sign hash k r m) (pads ++ [(m, r)]) fun i hi₁ hi₂ j hj₁ hj₂ heq => by
+      simp only [List.length_append, List.length_singleton] at hi₁ hi₂ hj₁ hj₂
+      exact hinj i (by omega) (by omega) j (by omega) (by omega) heq
+
+variable [DecidableEq M] [DecidableEq Y]
+
+/-- The issued-slot EUF-CMA experiment for the counter Carter–Wegman MAC under an arbitrary
+pad-sequence distribution `padSeqDist : PMF (ℕ → Y)`. -/
+noncomputable def maskedCounterSlotGame (seed : PMF K) (padSeqDist : PMF (ℕ → Y))
+    (hash : K → M → Y) (forger : CounterForger M Y) : PMF Bool := do
+  let k ← seed
+  let padSeq ← padSeqDist
+  let s ← forger.coins
+  let res ← (OracleComp.interpret (counterSeqHandler hash k padSeq) (forger.forge s)).run []
+  return checkCounterSlot hash k res.2 res.1
+
+/-- The issued-counter global-message-freshness EUF-CMA experiment under an arbitrary
+pad-sequence distribution `padSeqDist : PMF (ℕ → Y)`. -/
+noncomputable def maskedCounterGame (seed : PMF K) (padSeqDist : PMF (ℕ → Y))
+    (hash : K → M → Y) (forger : CounterForger M Y) : PMF Bool := do
+  let k ← seed
+  let padSeq ← padSeqDist
+  let s ← forger.coins
+  let res ← (OracleComp.interpret (counterSeqHandler hash k padSeq) (forger.forge s)).run []
+  return checkCounterEUF hash k res.2 res.1
+
+/-- The issued-slot strong SUF-CMA experiment under an arbitrary pad-sequence distribution
+`padSeqDist : PMF (ℕ → Y)`. -/
+noncomputable def maskedCounterStrongGame (seed : PMF K) (padSeqDist : PMF (ℕ → Y))
+    (hash : K → M → Y) (forger : CounterForger M Y) : PMF Bool := do
+  let k ← seed
+  let padSeq ← padSeqDist
+  let s ← forger.coins
+  let res ← (OracleComp.interpret (counterSeqHandler hash k padSeq) (forger.forge s)).run []
+  return checkCounterSUF hash k res.2 res.1
+
+theorem maskedCounterStrongGame_eq_maskedCounterSlotGame (seed : PMF K)
+    (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
+    maskedCounterStrongGame seed padSeqDist hash forger =
+      maskedCounterSlotGame seed padSeqDist hash forger := by
+  dsimp only [maskedCounterStrongGame, maskedCounterSlotGame, PMF.monad_bind_eq_bind,
+    PMF.monad_pure_eq_pure]
+  congr 1; funext k; congr 1; funext padSeq; congr 1; funext s; congr 1; funext res
+  rw [checkCounterSUF_eq_checkCounterSlot]
+
+theorem maskedCounterGame_le_maskedCounterSlotGame (seed : PMF K) (padSeqDist : PMF (ℕ → Y))
+    (hash : K → M → Y) (forger : CounterForger M Y) :
+    maskedCounterGame seed padSeqDist hash forger true ≤
+      maskedCounterSlotGame seed padSeqDist hash forger true := by
+  dsimp only [maskedCounterGame, maskedCounterSlotGame, PMF.monad_bind_eq_bind,
+    PMF.monad_pure_eq_pure]
+  refine bind_apply_mono_on_support seed true fun k _ => ?_
+  refine bind_apply_mono_on_support padSeqDist true fun padSeq _ => ?_
+  refine bind_apply_mono_on_support forger.coins true fun s _ => ?_
+  refine bind_apply_mono_on_support
+    ((OracleComp.interpret (counterSeqHandler hash k padSeq) (forger.forge s)).run []) true
+    fun res _ => ?_
+  by_cases h : checkCounterEUF hash k res.2 res.1 = true
+  · rw [h, checkCounterEUF_imp_checkCounterSlot hash k res.2 res.1 h]
+  · simp [Bool.eq_false_iff.mpr h]
+
+/-- The induced multi-query pad-sequence distinguisher `(ℕ → Y) → PMF Bool` that samples `k ← seed`
+and `s ← forger.coins`, simulates `forger.forge s` using `counterSeqHandler hash k padSeq`, and
+evaluates `checkCounterSlot hash k`. -/
+noncomputable def counterPadSeqDistinguisher (seed : PMF K) (hash : K → M → Y)
+    (forger : CounterForger M Y) (padSeq : ℕ → Y) : PMF Bool := do
+  let k ← seed
+  let s ← forger.coins
+  let res ← (OracleComp.interpret (counterSeqHandler hash k padSeq) (forger.forge s)).run []
+  return checkCounterSlot hash k res.2 res.1
+
+theorem maskedCounterSlotGame_eq_bind_counterPadSeqDistinguisher (seed : PMF K)
+    (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
+    maskedCounterSlotGame seed padSeqDist hash forger =
+      padSeqDist.bind (counterPadSeqDistinguisher seed hash forger) :=
+  PMF.bind_comm seed padSeqDist _
+
+/-- If `forger` makes at most `Q` signing queries, then `counterPadSeqDistinguisher` depends only on
+the first `Q` pads `padSeq 0, ..., padSeq (Q - 1)`. -/
+theorem counterPadSeqDistinguisher_congr (seed : PMF K) (hash : K → M → Y)
+    {forger : CounterForger M Y} {Q : ℕ} (hforger : ∀ s, (forger.forge s).IsQueryBounded Q)
+    {padSeq₁ padSeq₂ : ℕ → Y} (hpad : ∀ i < Q, padSeq₁ i = padSeq₂ i) :
+    counterPadSeqDistinguisher seed hash forger padSeq₁ =
+      counterPadSeqDistinguisher seed hash forger padSeq₂ := by
+  dsimp only [counterPadSeqDistinguisher, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure]
+  congr 1; funext k; congr 1; funext s
+  rw [run_interpret_counterSeqHandler_congr hash k (hforger s) []
+    (fun i _ hi => hpad i (by simpa using hi))]
+
+/-- When `table ← PMF.uniformOfFintype (ι → Y)` and `nonce : ℕ → ι` is injective on
+`{0, ..., Q - 1}`, sampling `table` and running `counterPadSeqDistinguisher` on
+`fun i => table (nonce i)` has the exact same distribution as `counterSlotGame seed hash forger`. -/
+theorem uniform_bind_counterPadSeqDistinguisher
+    {ι : Type} [DecidableEq ι] [Fintype ι] [Fintype Y] [Nonempty Y]
+    (seed : PMF K) (hash : K → M → Y) (nonce : ℕ → ι)
+    {forger : CounterForger M Y} {Q : ℕ} (hforger : ∀ s, (forger.forge s).IsQueryBounded Q)
+    (hinj : ∀ i < Q, ∀ j < Q, nonce i = nonce j → i = j) :
+    ((PMF.uniformOfFintype (ι → Y)).bind fun table =>
+      counterPadSeqDistinguisher seed hash forger (fun i => table (nonce i))) =
+      counterSlotGame seed hash forger := by
+  dsimp only [counterPadSeqDistinguisher, counterSlotGame, PMF.monad_bind_eq_bind,
+    PMF.monad_pure_eq_pure]
+  rw [PMF.bind_comm (PMF.uniformOfFintype (ι → Y)) seed]
+  congr 1; funext k
+  rw [PMF.bind_comm (PMF.uniformOfFintype (ι → Y)) forger.coins]
+  congr 1; funext s
+  rw [← PMF.bind_bind,
+    uniform_bind_run_interpret_counterSeqHandler hash k nonce (hforger s) []
+      (fun i _ hi j _ hj heq => hinj i (by simpa using hi) j (by simpa using hj) heq)]
+
+/-- The multi-query pad-sequence distribution on `ℕ → BitString n` obtained by sampling a uniform
+`n`-bit PRF key `key ← BitString.uniformList n` and evaluating `prfOracle family n key (nonce i)` at
+each counter index `i`. -/
+noncomputable def prfPadSeqDist (family : List Bool → List Bool → List Bool) (n : ℕ)
+    (nonce : ℕ → List Bool) : PMF (ℕ → BitString n) :=
+  (BitString.uniformList n).map fun key i =>
+    BitString.ofList n (prfOracle family n key (nonce i))
+
+/-- The multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot EUF-CMA experiment
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+noncomputable def prfCounterSlotGame (seed : PMF K) (family : List Bool → List Bool → List Bool)
+    (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n)
+    (forger : CounterForger M (BitString n)) : PMF Bool :=
+  maskedCounterSlotGame seed (prfPadSeqDist family n nonce) hash forger
+
+/-- The multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA experiment
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+noncomputable def prfCounterGame (seed : PMF K) (family : List Bool → List Bool → List Bool)
+    (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n)
+    (forger : CounterForger M (BitString n)) : PMF Bool :=
+  maskedCounterGame seed (prfPadSeqDist family n nonce) hash forger
+
+/-- The multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot strong SUF-CMA experiment
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+noncomputable def prfCounterStrongGame (seed : PMF K) (family : List Bool → List Bool → List Bool)
+    (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n)
+    (forger : CounterForger M (BitString n)) : PMF Bool :=
+  maskedCounterStrongGame seed (prfPadSeqDist family n nonce) hash forger
+
+theorem prfCounterStrongGame_eq_prfCounterSlotGame (seed : PMF K)
+    (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool)
+    (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
+    prfCounterStrongGame seed family n nonce hash forger =
+      prfCounterSlotGame seed family n nonce hash forger :=
+  maskedCounterStrongGame_eq_maskedCounterSlotGame seed (prfPadSeqDist family n nonce) hash forger
+
+theorem prfCounterGame_le_prfCounterSlotGame (seed : PMF K)
+    (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool)
+    (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
+    prfCounterGame seed family n nonce hash forger true ≤
+      prfCounterSlotGame seed family n nonce hash forger true :=
+  maskedCounterGame_le_maskedCounterSlotGame seed (prfPadSeqDist family n nonce) hash forger
+
+/-- One step of multi-pad collection at security parameter `n` under nonce schedule `nonce`:
+query the external oracle at `nonce n pads.length`, take at most `n` reply bits, and append the
+reply to `pads`. -/
+def prfPadCollectStep (n : ℕ) (nonce : ℕ → ℕ → List Bool) (pads : List (List Bool)) :
+    WordOracleComp Unit (List (List Bool)) :=
+  (fun reply => pads ++ [reply]) <$>
+    (List.take n <$> ProbOracleComp.query ((), nonce n pads.length))
+
+/-- Multi-query PRF `OracleDistinguisher` for a query budget `Q : ℕ → ℕ`, nonce schedule
+`nonce : ℕ → ℕ → List Bool`, and pad-sequence test
+`test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool`: at security parameter `n`, collect `Q n`
+oracle replies at `nonce n 0, ..., nonce n (Q n - 1)` and run `test n` on the `n`-bit views of the
+collected replies. -/
+def prfMultiPadDistinguisher (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) : OracleDistinguisher :=
+  fun n _ => do
+    let replies ← OracleComp.iterate (Q n) (prfPadCollectStep n nonce) []
+    ProbOracleComp.sample (test n (fun i => BitString.ofList n (replies.getD i [])))
+
+private theorem interpret_iterate_prfPadCollectStep (n : ℕ) (nonce : ℕ → ℕ → List Bool)
+    (f : List Bool → List Bool) (q : ℕ) (init : List (List Bool)) :
+    OracleComp.interpret
+      (ProbOracleComp.handler ProbComp.unifFin (fun request => pure (f request.2)))
+      (OracleComp.iterate q (prfPadCollectStep n nonce) init) =
+      pure (init ++ (List.range q).map (fun i => (f (nonce n (init.length + i))).take n)) := by
+  induction q generalizing init with
+  | zero =>
+    simp [OracleComp.iterate]
+  | succ q ih =>
+    simp only [OracleComp.iterate_succ, prfPadCollectStep, OracleComp.interpret_bind,
+      OracleComp.interpret_map, ProbOracleComp.interpret_query, pure_bind, Functor.map_map,
+      map_pure, ih, List.length_append, List.length_map, List.length_range, List.range_succ,
+      List.map_append, List.map_singleton, List.append_assoc]
+
+private theorem ofList_getD_map_range_take (n q : ℕ) (g : ℕ → List Bool) {i : ℕ} (hi : i < q) :
+    BitString.ofList n (((List.range q).map (fun j => (g j).take n)).getD i []) =
+      BitString.ofList n (g i) := by
+  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by simp [hi]), Option.getD_some,
+    List.getElem_map, List.getElem_range, ofList_take]
+
+/-- In `prfRealGame`, when `forger` makes at most `Q n` signing queries and `test n` realizes
+`counterPadSeqDistinguisher seed hash forger`, `prfMultiPadDistinguisher Q nonce test` has the exact
+outcome distribution of `prfCounterSlotGame seed family n (nonce n) hash forger`. -/
+theorem eval_prfRealGame_prfMultiPadDistinguisher {n : ℕ} (seed : PMF K)
+    (family : List Bool → List Bool → List Bool) (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool)
+    (hash : K → M → BitString n) {forger : CounterForger M (BitString n)}
+    (hforger : ∀ s, (forger.forge s).IsQueryBounded (Q n))
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest : ∀ padSeq, counterPadSeqDistinguisher seed hash forger padSeq =
+      ProbComp.eval (test n padSeq)) :
+    ProbComp.eval (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n) =
+      prfCounterSlotGame seed family n (nonce n) hash forger := by
+  rw [prfCounterSlotGame, maskedCounterSlotGame_eq_bind_counterPadSeqDistinguisher]
+  simp only [prfRealGame, prfMultiPadDistinguisher, prfPadSeqDist,
+    OracleComp.interpret_bind, interpret_iterate_prfPadCollectStep, List.nil_append,
+    List.length_nil, Nat.zero_add, pure_bind, ProbOracleComp.interpret_sample,
+    ProbComp.eval_bind, BitString.eval_sampleList, PMF.bind_map, Function.comp_def]
+  simp only [show ProbComp.unifFin = OracleComp.query from rfl, OracleComp.interpret_query_eq_self]
+  congr 1; funext key
+  rw [← htest]
+  exact counterPadSeqDistinguisher_congr seed hash hforger fun i hi =>
+    ofList_getD_map_range_take n (Q n) (fun j => prfOracle family n key (nonce n j)) hi
+
+/-- In `prfIdealGame`, when `forger` makes at most `Q n` signing queries, each `nonce n i`
+(`i < Q n`) has length `n`, the `Q n` nonces are pairwise distinct on `{0, ..., Q n - 1}`, and
+`test n` realizes `counterPadSeqDistinguisher seed hash forger`,
+`prfMultiPadDistinguisher Q nonce test` has the exact outcome distribution of the ideal
+`counterSlotGame seed hash forger`. -/
+theorem eval_prfIdealGame_prfMultiPadDistinguisher {n : ℕ} (seed : PMF K)
+    (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) (hash : K → M → BitString n)
+    {forger : CounterForger M (BitString n)}
+    (hforger : ∀ s, (forger.forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest : ∀ padSeq, counterPadSeqDistinguisher seed hash forger padSeq =
+      ProbComp.eval (test n padSeq)) :
+    ProbComp.eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n) =
+      counterSlotGame seed hash forger := by
+  simp only [prfIdealGame, prfMultiPadDistinguisher,
+    OracleComp.interpret_bind, interpret_iterate_prfPadCollectStep, List.nil_append,
+    List.length_nil, Nat.zero_add, pure_bind, ProbOracleComp.interpret_sample,
+    ProbComp.eval_bind, ProbComp.eval_uniform]
+  simp only [show ProbComp.unifFin = OracleComp.query from rfl, OracleComp.interpret_query_eq_self]
+  have htable (table : BitString n → BitString n) :
+      ProbComp.eval
+        (test n fun i =>
+          BitString.ofList n
+            (((List.range (Q n)).map fun j =>
+              (randomFunctionOracle n table (nonce n j)).take n).getD i [])) =
+      counterPadSeqDistinguisher seed hash forger
+        (fun i => table (BitString.ofList n (nonce n i))) := by
+    rw [← htest]
+    refine counterPadSeqDistinguisher_congr seed hash hforger fun i hi => ?_
+    rw [ofList_getD_map_range_take n (Q n) (fun j => randomFunctionOracle n table (nonce n j)) hi]
+    simp [randomFunctionOracle, hnonce_len i hi]
+  simp only [htable]
+  refine uniform_bind_counterPadSeqDistinguisher seed hash
+    (fun i => BitString.ofList n (nonce n i)) hforger fun i hi j hj heq => ?_
+  apply hnonce_inj i hi j hj
+  rw [← BitString.ofFn_ofList (hnonce_len i hi), ← BitString.ofFn_ofList (hnonce_len j hj), heq]
+
+/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot reduction**
+([BonehShoup2023], Section 7.4, Theorem 7.4): when `hash` is `ε`-almost-Δ-universal (`ε ≠ ⊤`),
+`forger` makes at most `Q n` signing queries, and `nonce n 0, ..., nonce n (Q n - 1)` are pairwise
+distinct `n`-bit nonces, the real-valued forgery probability in `prfCounterSlotGame` is at most
+`ε.toReal` plus the concrete PRF distinguishing advantage of `prfMultiPadDistinguisher Q nonce test`
+at parameter `n`. -/
+theorem prfCounterSlotGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞}
+    (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤)
+    (family : List Bool → List Bool → List Bool)
+    (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool)
+    {forger : CounterForger M (BitString n)}
+    (hforger : ∀ s, (forger.forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest : ∀ padSeq, counterPadSeqDistinguisher seed hash forger padSeq =
+      ProbComp.eval (test n padSeq)) :
+    (prfCounterSlotGame seed family n (nonce n) hash forger true).toReal ≤
+      ε.toReal +
+        (Game.advantage
+          (ProbComp.eval (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n))
+          (ProbComp.eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n)) : ℝ) := by
+  rw [eval_prfRealGame_prfMultiPadDistinguisher seed family Q nonce hash hforger test htest,
+    eval_prfIdealGame_prfMultiPadDistinguisher seed Q nonce hash hforger hnonce_len hnonce_inj
+      test htest,
+    Game.coe_advantage, Game.coe_succProbability, Game.coe_succProbability]
+  have hle : (counterSlotGame seed hash forger true).toReal ≤ ε.toReal :=
+    ENNReal.toReal_mono hε (counterSlotGame_le hh forger)
+  linarith [le_abs_self ((prfCounterSlotGame seed family n (nonce n) hash forger true).toReal -
+    (counterSlotGame seed hash forger true).toReal)]
+
+/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman EUF-CMA reduction**
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+theorem prfCounterGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞}
+    (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤)
+    (family : List Bool → List Bool → List Bool)
+    (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool)
+    {forger : CounterForger M (BitString n)}
+    (hforger : ∀ s, (forger.forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest : ∀ padSeq, counterPadSeqDistinguisher seed hash forger padSeq =
+      ProbComp.eval (test n padSeq)) :
+    (prfCounterGame seed family n (nonce n) hash forger true).toReal ≤
+      ε.toReal +
+        (Game.advantage
+          (ProbComp.eval (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n))
+          (ProbComp.eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n)) : ℝ) := by
+  have hmono : (prfCounterGame seed family n (nonce n) hash forger true).toReal ≤
+      (prfCounterSlotGame seed family n (nonce n) hash forger true).toReal :=
+    ENNReal.toReal_mono (PMF.apply_ne_top _ _)
+      (prfCounterGame_le_prfCounterSlotGame seed family n (nonce n) hash forger)
+  exact hmono.trans
+    (prfCounterSlotGame_le hh hε family Q nonce hforger hnonce_len hnonce_inj test htest)
+
+/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman SUF-CMA reduction**
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+theorem prfCounterStrongGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞}
+    (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤)
+    (family : List Bool → List Bool → List Bool)
+    (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool)
+    {forger : CounterForger M (BitString n)}
+    (hforger : ∀ s, (forger.forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest : ∀ padSeq, counterPadSeqDistinguisher seed hash forger padSeq =
+      ProbComp.eval (test n padSeq)) :
+    (prfCounterStrongGame seed family n (nonce n) hash forger true).toReal ≤
+      ε.toReal +
+        (Game.advantage
+          (ProbComp.eval (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n))
+          (ProbComp.eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n)) : ℝ) := by
+  rw [prfCounterStrongGame_eq_prfCounterSlotGame]
+  exact prfCounterSlotGame_le hh hε family Q nonce hforger hnonce_len hnonce_inj test htest
+
+/-- `prfMultiPadDistinguisher Q nonce test` is uniformly strict oracle-PPT (`IsOraclePPT encBool`)
+whenever the query budget `Q`, the nonce schedule `nonce`, and the pad-list test `test` are
+uniformly polynomial-time / strict PPT. -/
+theorem isOraclePPT_prfMultiPadDistinguisher
+    {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
+    {test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool}
+    (hQ : ComputableInPolyTime Q encUnary encUnary)
+    (hnonce : ComputableInPolyTime (fun p : ℕ × ℕ => nonce p.1 p.2)
+      (encPair encUnary encUnary) encBits)
+    (htest : IsPPTOn (encPair encUnary (encList encBits)) encBool
+      (fun p : ℕ × List (List Bool) =>
+        test p.1 (fun i => BitString.ofList p.1 (p.2.getD i [])))) :
+    IsOraclePPT encBool (prfMultiPadDistinguisher Q nonce test) := by
+  have hQ_tidy := hQ.tidy
+  have hnonce_tidy := hnonce.tidy
+  have hq : IsOraclePPTOn
+      (encPair (encPair encUnary encBits) (encList encBits))
+      encBits
+      (fun p : (ℕ × List Bool) × List (List Bool) =>
+        List.take p.1.1 <$> ProbOracleComp.query ((), nonce p.1.1 p.2.length)) :=
+    IsOraclePPTOn.query_take () (by polytime) (by polytime)
+  have hstep : IsOraclePPTOn
+      (encPair (encPair encUnary encBits) (encList encBits))
+      (encList encBits)
+      (fun p : (ℕ × List Bool) × List (List Bool) =>
+        prfPadCollectStep p.1.1 nonce p.2) := by
+    unfold prfPadCollectStep
+    exact hq.map_with
+      (f := fun (p : (ℕ × List Bool) × List (List Bool)) reply => p.2 ++ [reply])
+      (by polytime)
+  have hpoly : PolyBounded (fun p : ℕ × List Bool => (encPair encUnary encBits p).length)
+      (fun p : ℕ × List Bool => 2 * p.1 + 2) := by
+    have h1 : ComputableTidilyInPolyTime (fun p : ℕ × List Bool => 2 * p.1 + 2)
+        (encPair encUnary encBits) encUnary := by polytime
+    simpa only [encUnary_apply, List.length_replicate] using h1.polyBounded_length
+  have hiter : IsOraclePPTOn (encPair encUnary encBits) (encList encBits)
+      (fun p : ℕ × List Bool =>
+        OracleComp.iterate (Q p.1) (prfPadCollectStep p.1 nonce) []) := by
+    refine IsOraclePPTOn.iterateWith_of_bounded_growth
+      (initial := fun _ : ℕ × List Bool => ([] : List (List Bool)))
+      (count := fun p : ℕ × List Bool => Q p.1)
+      (step := fun (p : ℕ × List Bool) pads => prfPadCollectStep p.1 nonce pads)
+      (by polytime) (by polytime) hstep hpoly ?_
+    intro p pads next hnext
+    unfold prfPadCollectStep at hnext
+    obtain ⟨reply, hreply, rfl⟩ := ProbOracleComp.mem_support_map hnext
+    obtain ⟨rawReply, _, rfl⟩ := ProbOracleComp.mem_support_map hreply
+    have hlen : (rawReply.take p.1).length ≤ p.1 := List.length_take_le _ _
+    simp only [encList_append, encList_cons, encList_nil, List.append_nil, List.length_append,
+      length_frame, encBits_apply]
+    omega
+  unfold prfMultiPadDistinguisher
+  exact (hiter.bind_with ((htest.preprocess
+    (prepare := fun p : (ℕ × List Bool) × List (List Bool) => (p.1.1, p.2))
+    (by polytime)).isOraclePPTOn)).isOraclePPT
+
+/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot security**
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterSlotGame
+    {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n}
+    {ε : ℕ → ℝ≥0} (hh : ∀ n, IsDeltaUniversalHash (seed n) (hash n) (ε n))
+    (hε : Negligible ε)
+    {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
+    (forger : (n : ℕ) → CounterForger (M n) (BitString n))
+    (hforger : ∀ n s, ((forger n).forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ n i, i < Q n → (nonce n i).length = n)
+    (hnonce_inj : ∀ n i, i < Q n → ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest_eval : ∀ n padSeq,
+      counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq =
+        ProbComp.eval (test n padSeq))
+    (hQ : ComputableInPolyTime Q encUnary encUnary)
+    (hnonce : ComputableInPolyTime (fun p : ℕ × ℕ => nonce p.1 p.2)
+      (encPair encUnary encUnary) encBits)
+    (htest_ppt : IsPPTOn (encPair encUnary (encList encBits)) encBool
+      (fun p : ℕ × List (List Bool) =>
+        test p.1 (fun i => BitString.ofList p.1 (p.2.getD i [])))) :
+    Negligible (fun n =>
+      Game.succProbability
+        (prfCounterSlotGame (seed n) family n (nonce n) (hash n) (forger n))) := by
+  have hdist := hprf.secure (prfMultiPadDistinguisher Q nonce test)
+    (isOraclePPT_prfMultiPadDistinguisher hQ hnonce htest_ppt)
+  refine negligible_of_le (hε.add hdist) fun n => ?_
+  rw [← NNReal.coe_le_coe, Game.coe_succProbability, Pi.add_apply, NNReal.coe_add]
+  simpa only [ENNReal.coe_toReal] using
+    prfCounterSlotGame_le (hh n) ENNReal.coe_ne_top family Q nonce (hforger n)
+      (hnonce_len n) (hnonce_inj n) test (htest_eval n)
+
+/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman EUF-CMA security**
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame
+    {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n}
+    {ε : ℕ → ℝ≥0} (hh : ∀ n, IsDeltaUniversalHash (seed n) (hash n) (ε n))
+    (hε : Negligible ε)
+    {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
+    (forger : (n : ℕ) → CounterForger (M n) (BitString n))
+    (hforger : ∀ n s, ((forger n).forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ n i, i < Q n → (nonce n i).length = n)
+    (hnonce_inj : ∀ n i, i < Q n → ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest_eval : ∀ n padSeq,
+      counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq =
+        ProbComp.eval (test n padSeq))
+    (hQ : ComputableInPolyTime Q encUnary encUnary)
+    (hnonce : ComputableInPolyTime (fun p : ℕ × ℕ => nonce p.1 p.2)
+      (encPair encUnary encUnary) encBits)
+    (htest_ppt : IsPPTOn (encPair encUnary (encList encBits)) encBool
+      (fun p : ℕ × List (List Bool) =>
+        test p.1 (fun i => BitString.ofList p.1 (p.2.getD i [])))) :
+    Negligible (fun n =>
+      Game.succProbability
+        (prfCounterGame (seed n) family n (nonce n) (hash n) (forger n))) := by
+  refine negligible_of_le
+    (hprf.negligible_prfCounterSlotGame hh hε forger hforger hnonce_len hnonce_inj test
+      htest_eval hQ hnonce htest_ppt) fun n => ?_
+  exact ENNReal.toNNReal_mono (PMF.apply_ne_top _ _)
+    (prfCounterGame_le_prfCounterSlotGame (seed n) family n (nonce n) (hash n) (forger n))
+
+/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman SUF-CMA security**
+([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterStrongGame
+    {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
+    {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n}
+    {ε : ℕ → ℝ≥0} (hh : ∀ n, IsDeltaUniversalHash (seed n) (hash n) (ε n))
+    (hε : Negligible ε)
+    {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
+    (forger : (n : ℕ) → CounterForger (M n) (BitString n))
+    (hforger : ∀ n s, ((forger n).forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ n i, i < Q n → (nonce n i).length = n)
+    (hnonce_inj : ∀ n i, i < Q n → ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
+    (htest_eval : ∀ n padSeq,
+      counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq =
+        ProbComp.eval (test n padSeq))
+    (hQ : ComputableInPolyTime Q encUnary encUnary)
+    (hnonce : ComputableInPolyTime (fun p : ℕ × ℕ => nonce p.1 p.2)
+      (encPair encUnary encUnary) encBits)
+    (htest_ppt : IsPPTOn (encPair encUnary (encList encBits)) encBool
+      (fun p : ℕ × List (List Bool) =>
+        test p.1 (fun i => BitString.ofList p.1 (p.2.getD i [])))) :
+    Negligible (fun n =>
+      Game.succProbability
+        (prfCounterStrongGame (seed n) family n (nonce n) (hash n) (forger n))) := by
+  simp only [prfCounterStrongGame_eq_prfCounterSlotGame]
+  exact hprf.negligible_prfCounterSlotGame hh hε forger hforger hnonce_len hnonce_inj test
+    htest_eval hQ hnonce htest_ppt
+
+end PRFCounter
+
 /-! ### Concrete Carter–Wegman instantiations -/
 
 section Instantiations
diff --git a/ComplexityTests/Crypto/CarterWegman.lean b/ComplexityTests/Crypto/CarterWegman.lean
index 54156fd2e2..a070db37fd 100644
--- a/ComplexityTests/Crypto/CarterWegman.lean
+++ b/ComplexityTests/Crypto/CarterWegman.lean
@@ -5,6 +5,8 @@ Authors: Samuel Schlesinger
 -/
 
 import Complexity.Crypto.Protocols.MAC.CarterWegman
+import Complexity.Tactic.PPT
+import Complexity.Tactic.PolyTime
 import Mathlib.Algebra.Field.ZMod
 
 /-!
@@ -197,4 +199,22 @@ example :
     sign, verify, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.pure_bind, ProbComp.eval_pure]
   congr 1
 
+-- Concrete `IsOraclePPT` admissibility check for `wordProbPadTest` and `prfPadDistinguisher`.
+example :
+    IsOraclePPT Turing.MultiTapeTM.encBool
+      (prfPadDistinguisher
+        (wordProbPadTest
+          (fun n => BitString.sampleList n)
+          (fun _ k _ => k)
+          (fun _ => pure [])
+          (fun _ _ t => pure ([true], t)))) :=
+  isOraclePPT_prfPadDistinguisher_wordProbPadTest (by ppt) (by polytime) (by ppt) (by ppt)
+
+-- Concrete `IsOraclePPT` admissibility check for `prfMultiPadDistinguisher`.
+example :
+    IsOraclePPT Turing.MultiTapeTM.encBool
+      (prfMultiPadDistinguisher (fun n => n) (fun n _ => List.replicate n false)
+        (fun _ _ => pure false)) :=
+  isOraclePPT_prfMultiPadDistinguisher (by polytime) (by polytime) (by ppt)
+
 end ComplexityTests.Crypto.CarterWegman
diff --git a/ROADMAP.md b/ROADMAP.md
index 4965af0135..763d630976 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -130,10 +130,7 @@ families and full-input native runtime.
   2012); strict-PPT samplers for integer boxes; identification security under SIS; efficiency
   certificates for the simulator and extractor; full interactive-view simulation; SIS for
   general moduli; module SIS and module LWE toward Dilithium-style schemes, as theory.
-- **Symmetric:** `IsOraclePPT` admissibility of the PRF-pad reduction, uniform word-level
-  forger and hash families, the asymptotic `PseudorandomFunction` corollary and fresh-nonce
-  multi-query Carter–Wegman security ([#736]); the 4-round strong Feistel bound ([#748]); the
-  Naor–Reingold PRF from DDH.
+- **Symmetric:** the 4-round strong Feistel bound ([#748]); the Naor–Reingold PRF from DDH.
 - **General:** reusable adaptive reductions, public-key encryption, universal-instance zero
   knowledge, hard-core predicates and hardness amplification, and connections to learning and
   average-case hardness.

From 7b5a814feba828bcd7a7e5cc845df1fd8a625dd9 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 14:47:53 +0000
Subject: [PATCH 2/3] fix(crypto): update Carter-Wegman citations and weaken
 asymptotic hypotheses to atTop (#736)

---
 .../Crypto/Protocols/MAC/CarterWegman.lean    | 100 +++++++++++-------
 ComplexityTests/Crypto/CarterWegman.lean      |  47 +++++++-
 2 files changed, 102 insertions(+), 45 deletions(-)

diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean
index 9d6fb6d2e4..8433b506c8 100644
--- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean
+++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean
@@ -43,7 +43,7 @@ verifies under `r = -hash k m + t` if and only if
 
 Since the adversary's view `(m, t)` is independent of `k`, `IsDeltaUniversalHash seed hash ε`
 bounds the probability of this difference equation over `k ← seed` by at most `ε`
-([BonehShoup2023], Section 7.4, Theorem 7.3).
+([BonehShoup2023], Section 7.6, Lemma 7.11 and Theorem 7.12).
 
 This module formalizes:
 
@@ -55,7 +55,7 @@ This module formalizes:
    `oneTimeStrongGame`, `oneTimeStrongGame_eq_oneTimeGame`, `oneTimeGame_le`,
    `oneTimeStrongGame_le`)**: because each `(k, r, m)` admits a unique valid tag, strong
    unforgeability (`(m', t') ≠ (m, t)`) and ordinary unforgeability (`m' ≠ m`) coincide and are
-   bounded by `ε` ([BonehShoup2023], Theorem 7.3).
+   bounded by `ε` ([BonehShoup2023], Section 7.6, Lemma 7.11 and Theorem 7.12).
 4. **Adaptive multi-query issued-counter / issued-slot Carter–Wegman MAC (`CounterForger`,
    `counterSlotGame`, `counterGame`, `counterStrongGame`, `counterStrongGame_eq_counterSlotGame`,
    `counterSlotGame_le`, `counterGame_le`, `counterStrongGame_le`)**: when each signing query draws
@@ -100,7 +100,13 @@ This module formalizes:
    nonces `nonce n 0, ..., nonce n (Q n - 1)`, any `Q n`-query-bounded adaptive `CounterForger` has
    forgery probability at most `ε.toReal` plus the concrete `Q n`-query PRF distinguishing advantage
    of `prfMultiPadDistinguisher Q nonce test`, and negligible forgery probability when `family` is a
-   `PseudorandomFunction` and `ε` is `Negligible` ([BonehShoup2023], Section 7.4, Theorem 7.4).
+   `PseudorandomFunction` and `ε` is `Negligible` (after [BonehShoup2023], Section 7.5,
+   Theorem 7.10). This models the nonce-based Carter–Wegman construction under two restrictions
+   compared to Boneh–Shoup Attack Game 7.4: (a) the signer's counter schedule `nonce n i` fixes the
+   nonces rather than letting the adversary choose distinct nonces, and (b) `checkCounterSlot` /
+   `checkCounterGlobal` / `checkCounterStrong` accept forgeries only at issued counter slots
+   (`pads[idx]? = some r`) and reject unissued `idx`, which removes the `1 / |T|` unissued-nonce
+   guessing term.
 7. **Concrete instantiations** for Carter–Wegman polynomial hashing (`xpolyHash`, bound
    `(ℓ + 1) / |F|`), Boolean-matrix linear hashing (`BitString.LinearHash.hash`, bound `2⁻ᵐ`),
    subset-sum hashing (`BitString.SubsetSum.hash`, bound `1 / |G|`), and pairwise independent
@@ -148,7 +154,8 @@ This module formalizes:
   forgery probability.
 * `Cslib.Crypto.Protocols.CarterWegman.oneTimeStrongGame_eq_oneTimeGame`,
   `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_le`,
-  `Cslib.Crypto.Protocols.CarterWegman.oneTimeStrongGame_le`: Boneh–Shoup Theorem 7.3 (`≤ ε`).
+  `Cslib.Crypto.Protocols.CarterWegman.oneTimeStrongGame_le`: Boneh–Shoup Section 7.6, Lemma 7.11
+  and Theorem 7.12 (`≤ ε`).
 * `Cslib.Crypto.Protocols.CarterWegman.run_interpret_counterRealHandler`: simulation equivalence
   between real and simulated signing handlers under transcript mapping.
 * `Cslib.Crypto.Protocols.CarterWegman.counterStrongGame_eq_counterSlotGame`,
@@ -184,7 +191,7 @@ This module formalizes:
   `Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame`,
   `Cslib.Crypto.PseudorandomFunction.negligible_prfCounterStrongGame`: multi-query fresh-nonce
   PRF-masked Carter–Wegman security, `IsOraclePPT` admissibility, and asymptotic security
-  (Boneh–Shoup Section 7.4, Theorem 7.4).
+  (after Boneh–Shoup Section 7.5, Theorem 7.10).
 * `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_xpolyHash_le`,
   `Cslib.Crypto.Protocols.CarterWegman.counterGame_xpolyHash_le`,
   `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_linearHash_le`,
@@ -200,7 +207,7 @@ This module formalizes:
 * [M. N. Wegman, J. L. Carter, *New Hash Functions and Their Use in Authentication and Set
   Equality*][WegmanCarter1981]
 * [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
-  Version 0.6][BonehShoup2023], Section 7.4.
+  Version 0.6][BonehShoup2023], Sections 7.4–7.6.
 -/
 
 @[expose] public section
@@ -351,7 +358,7 @@ theorem zeroQueryGame_apply_true (seed : PMF K) (hash : K → M → Y) (forger :
 
 end ZeroQuery
 
-/-! ### Adaptive one-time Carter–Wegman EUF-CMA and SUF-CMA (Boneh–Shoup Theorem 7.3) -/
+/-! ### Adaptive one-time Carter–Wegman EUF-CMA and SUF-CMA (Boneh–Shoup Section 7.6) -/
 
 section OneTime
 
@@ -366,8 +373,8 @@ structure OneTimeForger (M Y : Type) where
   /-- Forgery distribution given the queried message `m` and its tag `t`. -/
   forge : M → Y → PMF (M × Y)
 
-/-- The adaptive one-time EUF-CMA experiment ([BonehShoup2023], Section 7.4, Theorem 7.3):
-the forger wins if `m' ≠ m` and `verify hash k r m' t' = true`. -/
+/-- The adaptive one-time EUF-CMA experiment ([BonehShoup2023], Section 7.6, Lemma 7.11 and
+Theorem 7.12): the forger wins if `m' ≠ m` and `verify hash k r m' t' = true`. -/
 noncomputable def oneTimeGame (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) :
     PMF Bool := do
   let k ← seed
@@ -430,8 +437,8 @@ theorem oneTimeGame_eq_bind_uniform (seed : PMF K) (hash : K → M → Y)
   congr 1; funext t
   rw [PMF.bind_comm seed (forger.forge m t)]
 
-/-- **One-time Carter–Wegman EUF-CMA security** ([BonehShoup2023], Section 7.4, Theorem 7.3;
-[WegmanCarter1981]): if `hash` is `ε`-almost-Δ-universal under `seed`
+/-- **One-time Carter–Wegman EUF-CMA security** ([BonehShoup2023], Section 7.6, Lemma 7.11 and
+Theorem 7.12; [WegmanCarter1981]): if `hash` is `ε`-almost-Δ-universal under `seed`
 (`IsDeltaUniversalHash seed hash ε`), then every adaptive one-time forger succeeds with
 probability at most `ε`. -/
 theorem oneTimeGame_le {seed : PMF K} {hash : K → M → Y} {ε : ℝ≥0∞}
@@ -1199,7 +1206,7 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame
 
 end PRFPad
 
-/-! ### Multi-query fresh-nonce PRF-masked Carter–Wegman MAC (Boneh–Shoup Section 7.4) -/
+/-! ### Multi-query fresh-nonce PRF-masked Carter–Wegman MAC (after Boneh–Shoup Section 7.5) -/
 
 section PRFCounter
 
@@ -1405,21 +1412,27 @@ noncomputable def prfPadSeqDist (family : List Bool → List Bool → List Bool)
     BitString.ofList n (prfOracle family n key (nonce i))
 
 /-- The multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot EUF-CMA experiment
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+(after [BonehShoup2023], Section 7.5, Theorem 7.10), where the signer's counter schedule `nonce`
+fixes the nonces and `checkCounterSlot` accepts only issued counter indices (`pads[idx]? = some r`),
+rejecting unissued `idx`. -/
 noncomputable def prfCounterSlotGame (seed : PMF K) (family : List Bool → List Bool → List Bool)
     (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n)
     (forger : CounterForger M (BitString n)) : PMF Bool :=
   maskedCounterSlotGame seed (prfPadSeqDist family n nonce) hash forger
 
 /-- The multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA experiment
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+(after [BonehShoup2023], Section 7.5, Theorem 7.10), where the signer's counter schedule `nonce`
+fixes the nonces and `checkCounterGlobal` accepts only issued counter indices
+(`pads[idx]? = some r`), rejecting unissued `idx`. -/
 noncomputable def prfCounterGame (seed : PMF K) (family : List Bool → List Bool → List Bool)
     (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n)
     (forger : CounterForger M (BitString n)) : PMF Bool :=
   maskedCounterGame seed (prfPadSeqDist family n nonce) hash forger
 
 /-- The multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot strong SUF-CMA experiment
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+(after [BonehShoup2023], Section 7.5, Theorem 7.10), where the signer's counter schedule `nonce`
+fixes the nonces and `checkCounterStrong` accepts only issued counter indices
+(`pads[idx]? = some r`), rejecting unissued `idx`. -/
 noncomputable def prfCounterStrongGame (seed : PMF K) (family : List Bool → List Bool → List Bool)
     (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n)
     (forger : CounterForger M (BitString n)) : PMF Bool :=
@@ -1542,11 +1555,12 @@ theorem eval_prfIdealGame_prfMultiPadDistinguisher {n : ℕ} (seed : PMF K)
   rw [← BitString.ofFn_ofList (hnonce_len i hi), ← BitString.ofFn_ofList (hnonce_len j hj), heq]
 
 /-- **Multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot reduction**
-([BonehShoup2023], Section 7.4, Theorem 7.4): when `hash` is `ε`-almost-Δ-universal (`ε ≠ ⊤`),
-`forger` makes at most `Q n` signing queries, and `nonce n 0, ..., nonce n (Q n - 1)` are pairwise
-distinct `n`-bit nonces, the real-valued forgery probability in `prfCounterSlotGame` is at most
-`ε.toReal` plus the concrete PRF distinguishing advantage of `prfMultiPadDistinguisher Q nonce test`
-at parameter `n`. -/
+(after [BonehShoup2023], Section 7.5, Theorem 7.10): when `hash` is `ε`-almost-Δ-universal
+(`ε ≠ ⊤`), `forger` makes at most `Q n` signing queries, and `nonce n 0, ..., nonce n (Q n - 1)`
+are pairwise distinct `n`-bit nonces fixed by the signer's counter schedule, the real-valued
+issued-slot forgery probability in `prfCounterSlotGame` is at most `ε.toReal` plus the concrete PRF
+distinguishing advantage of `prfMultiPadDistinguisher Q nonce test` at parameter `n` (with
+unissued counter indices rejected by `checkCounterSlot`). -/
 theorem prfCounterSlotGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞}
     (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤)
     (family : List Bool → List Bool → List Bool)
@@ -1572,8 +1586,8 @@ theorem prfCounterSlotGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitSt
   linarith [le_abs_self ((prfCounterSlotGame seed family n (nonce n) hash forger true).toReal -
     (counterSlotGame seed hash forger true).toReal)]
 
-/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman EUF-CMA reduction**
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA reduction**
+(after [BonehShoup2023], Section 7.5, Theorem 7.10). -/
 theorem prfCounterGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞}
     (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤)
     (family : List Bool → List Bool → List Bool)
@@ -1597,8 +1611,8 @@ theorem prfCounterGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString
   exact hmono.trans
     (prfCounterSlotGame_le hh hε family Q nonce hforger hnonce_len hnonce_inj test htest)
 
-/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman SUF-CMA reduction**
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+/-- **Multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot SUF-CMA reduction**
+(after [BonehShoup2023], Section 7.5, Theorem 7.10). -/
 theorem prfCounterStrongGame_le {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ℝ≥0∞}
     (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤)
     (family : List Bool → List Bool → List Bool)
@@ -1675,7 +1689,10 @@ theorem isOraclePPT_prfMultiPadDistinguisher
     (by polytime)).isOraclePPTOn)).isOraclePPT
 
 /-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot security**
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+(after [BonehShoup2023], Section 7.5, Theorem 7.10). The query bound `hforger` and nonce
+conditions `hnonce_len`, `hnonce_inj` are required only eventually (`∀ᶠ n in Filter.atTop`), so
+any polynomial query budget `Q n` (where `Q n ≤ 2 ^ n` holds for all sufficiently large `n`) is
+covered without patching small `n`. -/
 theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterSlotGame
     {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
     {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
@@ -1684,9 +1701,9 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterSlotGame
     (hε : Negligible ε)
     {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
     (forger : (n : ℕ) → CounterForger (M n) (BitString n))
-    (hforger : ∀ n s, ((forger n).forge s).IsQueryBounded (Q n))
-    (hnonce_len : ∀ n i, i < Q n → (nonce n i).length = n)
-    (hnonce_inj : ∀ n i, i < Q n → ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (hforger : ∀ᶠ n in Filter.atTop, ∀ s, ((forger n).forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ᶠ n in Filter.atTop, ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ᶠ n in Filter.atTop, ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
     (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
     (htest_eval : ∀ n padSeq,
       counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq =
@@ -1702,14 +1719,15 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterSlotGame
         (prfCounterSlotGame (seed n) family n (nonce n) (hash n) (forger n))) := by
   have hdist := hprf.secure (prfMultiPadDistinguisher Q nonce test)
     (isOraclePPT_prfMultiPadDistinguisher hQ hnonce htest_ppt)
-  refine negligible_of_le (hε.add hdist) fun n => ?_
+  refine negligible_of_eventually_le (hε.add hdist) ?_
+  filter_upwards [hforger, hnonce_len, hnonce_inj] with n hforger_n hlen_n hinj_n
   rw [← NNReal.coe_le_coe, Game.coe_succProbability, Pi.add_apply, NNReal.coe_add]
   simpa only [ENNReal.coe_toReal] using
-    prfCounterSlotGame_le (hh n) ENNReal.coe_ne_top family Q nonce (hforger n)
-      (hnonce_len n) (hnonce_inj n) test (htest_eval n)
+    prfCounterSlotGame_le (hh n) ENNReal.coe_ne_top family Q nonce hforger_n
+      hlen_n hinj_n test (htest_eval n)
 
-/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman EUF-CMA security**
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA security**
+(after [BonehShoup2023], Section 7.5, Theorem 7.10). -/
 theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame
     {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
     {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
@@ -1718,9 +1736,9 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame
     (hε : Negligible ε)
     {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
     (forger : (n : ℕ) → CounterForger (M n) (BitString n))
-    (hforger : ∀ n s, ((forger n).forge s).IsQueryBounded (Q n))
-    (hnonce_len : ∀ n i, i < Q n → (nonce n i).length = n)
-    (hnonce_inj : ∀ n i, i < Q n → ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (hforger : ∀ᶠ n in Filter.atTop, ∀ s, ((forger n).forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ᶠ n in Filter.atTop, ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ᶠ n in Filter.atTop, ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
     (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
     (htest_eval : ∀ n padSeq,
       counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq =
@@ -1740,8 +1758,8 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame
   exact ENNReal.toNNReal_mono (PMF.apply_ne_top _ _)
     (prfCounterGame_le_prfCounterSlotGame (seed n) family n (nonce n) (hash n) (forger n))
 
-/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman SUF-CMA security**
-([BonehShoup2023], Section 7.4, Theorem 7.4). -/
+/-- **Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot SUF-CMA security**
+(after [BonehShoup2023], Section 7.5, Theorem 7.10). -/
 theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterStrongGame
     {K M : ℕ → Type} [∀ n, DecidableEq (M n)]
     {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
@@ -1750,9 +1768,9 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfCounterStrongGame
     (hε : Negligible ε)
     {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool}
     (forger : (n : ℕ) → CounterForger (M n) (BitString n))
-    (hforger : ∀ n s, ((forger n).forge s).IsQueryBounded (Q n))
-    (hnonce_len : ∀ n i, i < Q n → (nonce n i).length = n)
-    (hnonce_inj : ∀ n i, i < Q n → ∀ j < Q n, nonce n i = nonce n j → i = j)
+    (hforger : ∀ᶠ n in Filter.atTop, ∀ s, ((forger n).forge s).IsQueryBounded (Q n))
+    (hnonce_len : ∀ᶠ n in Filter.atTop, ∀ i < Q n, (nonce n i).length = n)
+    (hnonce_inj : ∀ᶠ n in Filter.atTop, ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j)
     (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool)
     (htest_eval : ∀ n padSeq,
       counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq =
diff --git a/ComplexityTests/Crypto/CarterWegman.lean b/ComplexityTests/Crypto/CarterWegman.lean
index a070db37fd..cef09f90fe 100644
--- a/ComplexityTests/Crypto/CarterWegman.lean
+++ b/ComplexityTests/Crypto/CarterWegman.lean
@@ -210,11 +210,50 @@ example :
           (fun _ _ t => pure ([true], t)))) :=
   isOraclePPT_prfPadDistinguisher_wordProbPadTest (by ppt) (by polytime) (by ppt) (by ppt)
 
--- Concrete `IsOraclePPT` admissibility check for `prfMultiPadDistinguisher`.
+/-- Two-slot `n`-bit nonce schedule: slot `0` has leading bit `false` and slot `1` has leading bit
+`true`, padded with `n - 1` `false` bits. For every `n ≥ 1`, both nonces have length `n` and are
+distinct on `{0, 1}`. -/
+def twoSlotNonce (n i : ℕ) : List Bool :=
+  decide (i = 1) :: List.replicate (n - 1) false
+
+/-- Trivial counter forger that makes `0 ≤ 2` signing queries and outputs `(0, (0, 0))`. -/
+noncomputable def zeroQueryCounterForger (n : ℕ) :
+    CounterForger (BitString n) (BitString n) where
+  Coins := Unit
+  coins := PMF.pure ()
+  forge _ := pure (0, (0, 0))
+
+-- Concrete `IsOraclePPT` admissibility check for `prfMultiPadDistinguisher` with `twoSlotNonce`.
 example :
     IsOraclePPT Turing.MultiTapeTM.encBool
-      (prfMultiPadDistinguisher (fun n => n) (fun n _ => List.replicate n false)
-        (fun _ _ => pure false)) :=
-  isOraclePPT_prfMultiPadDistinguisher (by polytime) (by polytime) (by ppt)
+      (prfMultiPadDistinguisher (fun _ => 2) twoSlotNonce (fun _ _ => pure false)) :=
+  isOraclePPT_prfMultiPadDistinguisher (by polytime) (by unfold twoSlotNonce; polytime) (by ppt)
+
+-- End-to-end check of `PseudorandomFunction.negligible_prfCounterGame` with `twoSlotNonce`,
+-- exercising `hforger`, `hnonce_len`, `hnonce_inj`, `htest_eval`, `hQ`, `hnonce`, and `htest_ppt`.
+example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family)
+    {ε : ℕ → NNReal}
+    (hh : ∀ n, IsDeltaUniversalHash
+      (PMF.uniformOfFintype (Fin n → BitString n)) (BitString.LinearHash.hash (n := n) (m := n))
+      (ε n))
+    (hε : Negligible ε) :
+    Negligible (fun n =>
+      Game.succProbability
+        (prfCounterGame (PMF.uniformOfFintype (Fin n → BitString n)) family n (twoSlotNonce n)
+          BitString.LinearHash.hash (zeroQueryCounterForger n))) := by
+  refine hprf.negligible_prfCounterGame hh hε (Q := fun _ => 2) (nonce := twoSlotNonce)
+    zeroQueryCounterForger
+    (Filter.Eventually.of_forall fun _ _ => .pure _ _)
+    ?_ ?_ (fun _ _ => pure false) ?_
+    (by polytime) (by unfold twoSlotNonce; polytime) (by ppt)
+  · filter_upwards [Filter.eventually_ge_atTop 1] with n hn i _
+    simp [twoSlotNonce]
+    omega
+  · filter_upwards [Filter.eventually_ge_atTop 1] with n _ i hi j hj heq
+    have hhead : decide (i = 1) = decide (j = 1) := List.cons.inj heq |>.1
+    by_cases hi1 : i = 1 <;> by_cases hj1 : j = 1 <;> simp_all
+    omega
+  · intro n padSeq
+    simp [counterPadSeqDistinguisher, zeroQueryCounterForger, checkCounterSlot]
 
 end ComplexityTests.Crypto.CarterWegman

From b9bd5f8b039c58fc76421a0513e9aaa80a1dec0e Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 14:47:53 +0000
Subject: [PATCH 3/3] docs(roadmap): keep full nonce-based and randomized
 Carter-Wegman items open (#736)

---
 ROADMAP.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/ROADMAP.md b/ROADMAP.md
index 763d630976..8ef1bb80b6 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -130,7 +130,10 @@ families and full-input native runtime.
   2012); strict-PPT samplers for integer boxes; identification security under SIS; efficiency
   certificates for the simulator and extractor; full interactive-view simulation; SIS for
   general moduli; module SIS and module LWE toward Dilithium-style schemes, as theory.
-- **Symmetric:** the 4-round strong Feistel bound ([#748]); the Naor–Reingold PRF from DDH.
+- **Symmetric:** full nonce-based Carter–Wegman security with adversary-chosen distinct nonces and
+  forgeries at arbitrary nonces (Boneh–Shoup Attack Game 7.4, Theorem 7.10) and randomized
+  Carter–Wegman security (Theorem 7.9) ([#736]); the 4-round strong Feistel bound ([#748]); the
+  Naor–Reingold PRF from DDH.
 - **General:** reusable adaptive reductions, public-key encryption, universal-instance zero
   knowledge, hard-core predicates and hardness amplification, and connections to learning and
   average-case hardness.