refactor: replace restatement tests and remove process doc references (#949)

Complexity/Computability/Complexity/Classes/WPP/Robustness.lean

@@ -32,8 +32,8 @@ Thus the proof uses certified word sums and powers, without assuming indexed-pro
 The two-sided acceptance/rejection-target generalization is proved in `WPP.TwoSided`.
 Oracle lowness is a separate result.
 
-The public polynomial-time interfaces use `Turing.MultiTapeTM.ComputableInPolyTime`, following
-the plain-statement convention of #456. Private machine-construction lemmas remain tidy.
+The public polynomial-time interfaces use `Turing.MultiTapeTM.ComputableInPolyTime`. Private
+machine-construction lemmas remain tidy.
 
 ## Main results
 

Complexity/Computability/Complexity/Classes/WPP/TwoSided.lean

@@ -23,8 +23,7 @@ of the differences between rejection targets and the original gap. This vanishes
 and on acceptance takes one of a uniformly computed family of nonzero products. The uniform
 product theorem and one-sided robustness then finish the construction.
 
-The public interfaces ask for `Turing.MultiTapeTM.ComputableInPolyTime` certificates, following
-the plain-statement convention of #456.
+The public interfaces ask for `Turing.MultiTapeTM.ComputableInPolyTime` certificates.
 
 ## Main results
 

Complexity/Computability/GenericRAM/Native/MeasurementFold.lean

@@ -30,7 +30,7 @@ loop. The generic callback may grow its accumulator: polynomial whole-loop works
 actual all-prefix accumulator invariant, not just a polynomial per-visit certificate.
 
 This is the measurement-VALUE enumeration of [OpenAI2026ETH], Lemma 3.2 and Proposition 3.4
-(pp. 22–26), runtime M0.4 of #1226. It is not formal mode-exponent enumeration, subset-pair
+(pp. 22–26). It is not formal mode-exponent enumeration, subset-pair
 traversal, rational coefficient accumulation or a complete runtime/ETH result.
 -/
 

Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean

@@ -617,7 +617,7 @@ theorem exists_fin_selectBestTestRow (countSys : List (List Bool) → ℕ)
   obtain ⟨γ, hγ⟩ := exists_fin_of_lt_candidateTupleCount hjStar
   exact ⟨γ, by rw [hrow, hγ, materializeTestRow_ofFn]⟩
 
-/-! ### Row counts, widths, weights, and CNF `#1234` bridge for `greedyParityRows` -/
+/-! ### Row counts, widths, weights, and CNF bridge for `greedyParityRows` -/
 
 @[simp] theorem length_greedyParityRowsAt (countSys : List (List Bool) → ℕ)
     (m P : ℕ) (initRows : List (List Bool)) (i : ℕ) :
@@ -688,7 +688,8 @@ theorem length_encList_greedyParityRowsAt (countSys : List (List Bool) → ℕ)
     rw [greedyParityRowsAt_succ, encList_append, List.length_append, ih, encList_cons, encList_nil,
       List.append_nil, length_frame, encBits_apply, length_selectBestTestRow]; ring
 
-/-- **Exact bridge from `greedyParityRows` to `CNF.numPassing_greedy` (`#1234`, Lemma 6.2).**
+/-- **Exact bridge from `greedyParityRows` to `CNF.numPassing_greedy`**
+([OpenAI2026ETH], Lemma 6.2).
 Under `hn : 1 ≤ Fintype.card V` and `hP : 1 ≤ P`, when `initRows` has row width `φ.length`,
 `countSys` computes `numPassing φ.violations` on width-`φ.length` candidate row lists of length at
 most `initRows.length + 3 * Fintype.card V` whose appended rows have weight `≤ P`, and `initRows`

Complexity/Probability/HashFamily/Uniform.lean

@@ -19,10 +19,6 @@ A uniformly random function into a finite additive group has uniform differences
 inputs. Negating the complete function preserves its uniform law, and hence the same bound.
 These are information-theoretic laws; they make no efficient-sampling claim.
 
-The uniform-function proof is moved from `Complexity.Crypto.Protocols.Cipher.LubyRackoff`.
-The negated-function proof is extracted from the reviewed #1099 contribution by
-`worker-jetski-fb3f7966`; the proof bodies and their assumptions are retained.
-
 ## Main results
 
 * `Cslib.Probability.isDeltaUniversalHash_uniformOfFintype`: uniform functions are Δ-universal.

ComplexityTests/Crypto/AuthenticatedEncryption.lean

@@ -12,8 +12,8 @@ import Complexity.Crypto.Computational.Encryption.Authenticated
 Provides concrete instantiations of `SymmetricCipher`, verifies oracle behavior on concrete inputs,
 proves that `echoCipher` fails both `INDCPA` (via `not_indcpa_of_ciphertext_length_eq`,
 Boneh–Shoup Example 5.1 / Exercise 5.10(a)) and `CiphertextIntegrity` (via an explicit zero-query
-oracle-PPT adversary), and exercises the runtime certificates (`IsPPT`, `IsOraclePPT`) and
-quantitative/asymptotic security theorems for Boneh–Shoup Theorem 9.1 (`AE ⇒ CCA`).
+oracle-PPT adversary), and exercises the composed runtime certificates (`IsPPT`, `IsOraclePPT`) and
+quantitative security bounds for Boneh–Shoup Theorem 9.1 (`AE ⇒ CCA`) on `echoCipher`.
 -/
 
 namespace ComplexityTests.Crypto.AuthenticatedEncryption
@@ -104,82 +104,111 @@ theorem not_authenticatedEncryption_echoCipher :
     ¬ echoCipher.AuthenticatedEncryption :=
   fun hae => not_ciphertextIntegrity_echoCipher hae.2
 
-/-! ### API and Certificate Smoke Checks -/
+/-! ### Concrete Reduction Certificates and Quantitative Bounds on `echoCipher` -/
 
-section CertificatesAndReductions
+/-- Zero-query CCA adversary that always outputs `false`. -/
+def zeroCCAAdversary : CCAAdversary :=
+  fun _ _ => ProbOracleComp.sample (pure false)
 
-variable (E : SymmetricCipher)
-  {ctBound Q : ℕ → ℕ}
-  (hctBound : ComputableInPolyTime ctBound encUnary encUnary)
-  (hQ : ComputableInPolyTime Q encUnary encUnary)
-  {cpaAdv : OracleDistinguisher} (hcpaAdv : IsOraclePPT encBool cpaAdv)
-  {ciAdv : CIAdversary} (hciAdv : IsOraclePPT encBits ciAdv)
-  {ccaAdv : CCAAdversary} (hccaAdv : IsOraclePPT encBool ccaAdv)
+theorem isOraclePPT_zeroCCAAdversary : IsOraclePPT encBool zeroCCAAdversary := by
+  have hbody : IsPPTOn (encPair encUnary encBits) encBool
+      (fun _ : ℕ × List Bool => (pure false : ProbComp Bool)) :=
+    (ComputableTidilyInPolyTime.const false).isPPTOn
+  exact hbody.isOraclePPTOn.isOraclePPT
 
--- Closed game `IsPPT` certificates.
-example (bit : Bool) : IsPPT encBool (fun n _ => E.cpaGame cpaAdv bit n) :=
-  E.isPPT_cpaGame hcpaAdv bit
-
-example : IsPPT encBool (fun n _ => E.ciGame ciAdv n) :=
-  E.isPPT_ciGame hciAdv
-
-example (bit : Bool) : IsPPT encBool (fun n _ => E.ccaGame ccaAdv bit n) :=
-  E.isPPT_ccaGame hccaAdv bit
-
--- Theorem 9.1 reduction `IsOraclePPT` certificates.
-example : IsOraclePPT encBool (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) :=
-  SymmetricCipher.isOraclePPT_ccaToCPAAdversary hctBound hccaAdv
+theorem isQueryBounded_zeroCCAAdversary (n : ℕ) :
+    (zeroCCAAdversary n []).IsQueryBounded 0 :=
+  ProbOracleComp.IsQueryBounded.sample (pure false)
 
+-- Composed closed-game `IsPPT` and Theorem 9.1 reduction `IsOraclePPT` certificates on
+-- `echoCipher` with `ctBound = id` and `Q = 0`.
 example (bit : Bool) :
-    IsOraclePPT encBits (SymmetricCipher.ccaToCIAdversary ctBound Q bit ccaAdv) :=
-  SymmetricCipher.isOraclePPT_ccaToCIAdversary hctBound hQ bit hccaAdv
+    IsPPT encBool
+      (fun n _ =>
+        echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) bit n) :=
+  echoCipher.isPPT_cpaGame
+    (SymmetricCipher.isOraclePPT_ccaToCPAAdversary ComputableInPolyTime.id'
+      isOraclePPT_zeroCCAAdversary)
+    bit
 
-example : IsOraclePPT encBits (SymmetricCipher.ccaToCIHiddenBitAdversary ctBound Q ccaAdv) :=
-  SymmetricCipher.isOraclePPT_ccaToCIHiddenBitAdversary hctBound hQ hccaAdv
+example (bit : Bool) :
+    IsPPT encBool
+      (fun n _ =>
+        echoCipher.ciGame
+          (SymmetricCipher.ccaToCIAdversary id (fun _ => 0) bit zeroCCAAdversary) n) :=
+  echoCipher.isPPT_ciGame
+    (SymmetricCipher.isOraclePPT_ccaToCIAdversary ComputableInPolyTime.id'
+      (ComputableInPolyTime.const 0) bit isOraclePPT_zeroCCAAdversary)
 
--- Quantitative security bounds (Theorem 9.1).
-example (n : ℕ)
-    (hq : (ccaAdv n []).IsQueryBounded (Q n))
-    (hctBoundN : ∀ k ∈ (ProbComp.eval (E.keyGen n)).support,
-      ∀ msg, msg.length = n →
-      ∀ ct ∈ (ProbComp.eval (E.encrypt n k msg)).support, ct.length ≤ ctBound n) :
-    (Game.advantage (ProbComp.eval (E.ccaGame ccaAdv false n))
-        (ProbComp.eval (E.ccaGame ccaAdv true n)) : ℝ) ≤
-      (dyadicSize (Q n) : ℝ) *
+example :
+    IsPPT encBool
+      (fun n _ =>
+        echoCipher.ciGame
+          (SymmetricCipher.ccaToCIHiddenBitAdversary id (fun _ => 0) zeroCCAAdversary) n) :=
+  echoCipher.isPPT_ciGame
+    (SymmetricCipher.isOraclePPT_ccaToCIHiddenBitAdversary ComputableInPolyTime.id'
+      (ComputableInPolyTime.const 0) isOraclePPT_zeroCCAAdversary)
+
+-- Quantitative Theorem 9.1 bounds instantiated on `echoCipher` and `zeroCCAAdversary`, with
+-- `dyadicSize 0 = 2` evaluated and `echoCipher_ctLen` discharging the ciphertext-length premise.
+example (n : ℕ) :
+    (Game.advantage (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary false n))
+        (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary true n)) : ℝ) ≤
+      2 *
         (Game.succProbability
-          (ProbComp.eval (E.ciGame (SymmetricCipher.ccaToCIAdversary ctBound Q false ccaAdv) n)) :
+          (ProbComp.eval
+            (echoCipher.ciGame
+              (SymmetricCipher.ccaToCIAdversary id (fun _ => 0) false zeroCCAAdversary) n)) :
             ℝ) +
       (Game.advantage
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) false n))
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) true n)) :
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) false n))
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) true n)) :
           ℝ) +
-      (dyadicSize (Q n) : ℝ) *
+      2 *
         (Game.succProbability
-          (ProbComp.eval (E.ciGame (SymmetricCipher.ccaToCIAdversary ctBound Q true ccaAdv) n)) :
-            ℝ) :=
-  E.advantage_ccaGame_le ctBound Q ccaAdv n hq hctBoundN
-
-example (n : ℕ)
-    (hq : (ccaAdv n []).IsQueryBounded (Q n))
-    (hctBoundN : ∀ k ∈ (ProbComp.eval (E.keyGen n)).support,
-      ∀ msg, msg.length = n →
-      ∀ ct ∈ (ProbComp.eval (E.encrypt n k msg)).support, ct.length ≤ ctBound n) :
-    (Game.advantage (ProbComp.eval (E.ccaGame ccaAdv false n))
-        (ProbComp.eval (E.ccaGame ccaAdv true n)) : ℝ) ≤
-      2 * (dyadicSize (Q n) : ℝ) *
+          (ProbComp.eval
+            (echoCipher.ciGame
+              (SymmetricCipher.ccaToCIAdversary id (fun _ => 0) true zeroCCAAdversary) n)) :
+            ℝ) := by
+  have hct (k : List Bool) (hk : k ∈ (ProbComp.eval (echoCipher.keyGen n)).support)
+      (msg : List Bool) (hmsg : msg.length = n)
+      (ct : List Bool) (hct : ct ∈ (ProbComp.eval (echoCipher.encrypt n k msg)).support) :
+      ct.length ≤ id n :=
+    (echoCipher_ctLen n k hk msg hmsg ct hct).le
+  have h0 : dyadicSize 0 = 2 := by decide
+  have hd : (dyadicSize 0 : ℝ) = 2 := by exact_mod_cast h0
+  simpa [hd] using
+    echoCipher.advantage_ccaGame_le id (fun _ => 0) zeroCCAAdversary n
+      (isQueryBounded_zeroCCAAdversary n) hct
+
+example (n : ℕ) :
+    (Game.advantage (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary false n))
+        (ProbComp.eval (echoCipher.ccaGame zeroCCAAdversary true n)) : ℝ) ≤
+      4 *
         (Game.succProbability
           (ProbComp.eval
-            (E.ciGame (SymmetricCipher.ccaToCIHiddenBitAdversary ctBound Q ccaAdv) n)) : ℝ) +
+            (echoCipher.ciGame
+              (SymmetricCipher.ccaToCIHiddenBitAdversary id (fun _ => 0) zeroCCAAdversary) n)) :
+            ℝ) +
       (Game.advantage
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) false n))
-        (ProbComp.eval (E.cpaGame (SymmetricCipher.ccaToCPAAdversary ctBound ccaAdv) true n)) :
-          ℝ) :=
-  E.advantage_ccaGame_le_two_mul ctBound Q ccaAdv n hq hctBoundN
-
--- End-to-end asymptotic composition (Theorem 9.1).
-example (hae : E.AuthenticatedEncryption) : E.INDCCA :=
-  hae.indcca
-
-end CertificatesAndReductions
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) false n))
+        (ProbComp.eval
+          (echoCipher.cpaGame (SymmetricCipher.ccaToCPAAdversary id zeroCCAAdversary) true n)) :
+          ℝ) := by
+  have hct (k : List Bool) (hk : k ∈ (ProbComp.eval (echoCipher.keyGen n)).support)
+      (msg : List Bool) (hmsg : msg.length = n)
+      (ct : List Bool) (hct : ct ∈ (ProbComp.eval (echoCipher.encrypt n k msg)).support) :
+      ct.length ≤ id n :=
+    (echoCipher_ctLen n k hk msg hmsg ct hct).le
+  have hd : 2 * (dyadicSize 0 : ℝ) = 4 := by
+    have h0 : dyadicSize 0 = 2 := by decide
+    rw [h0]
+    norm_num
+  simpa [hd] using
+    echoCipher.advantage_ccaGame_le_two_mul id (fun _ => 0) zeroCCAAdversary n
+      (isQueryBounded_zeroCCAAdversary n) hct
 
 end ComplexityTests.Crypto.AuthenticatedEncryption