refactor(crypto): accept plain certificates in security constructors

Complexity/Crypto/Computational/Basic.lean

@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 public import Complexity.Computability.Probabilistic.Parameter
 public import Complexity.Crypto.Game
 import Complexity.Crypto.Negligible.Basic
@@ -137,7 +138,7 @@ theorem ComputationallyIndistinguishable.bind {X Y : ℕ → PMF (List Bool)}
 /-- Efficient parameter-dependent deterministic postprocessing preserves indistinguishability. -/
 theorem ComputationallyIndistinguishable.map {X Y : ℕ → PMF (List Bool)}
     (h : ComputationallyIndistinguishable X Y) {f : ℕ → List Bool → List Bool}
-    (hf : ComputableTidilyInPolyTime (fun p : ℕ × List Bool => f p.1 p.2)
+    (hf : ComputableInPolyTime (fun p : ℕ × List Bool => f p.1 p.2)
       (encPair encUnary encBits) encBits) :
     ComputationallyIndistinguishable (fun n => (X n).map (f n)) (fun n => (Y n).map (f n)) := by
   have hp : IsPPT encBits (fun n word => pure (f n word)) := by ppt

Complexity/Crypto/Computational/Commitment.lean

@@ -182,7 +182,8 @@ theorem PseudorandomGenerator.naorCommit_indistinguishable_uniform
       (fun p : ℕ × List Bool => naorCommit id (r p.1) (b p.1) p.2)
       (encPair encUnary encBits) encBits := by
     apply computableTidilyInPolyTime_naorCommit <;> fun_prop
-  have hind := hG.indistinguishable.map (f := fun n y => naorCommit id (r n) (b n) y) hmap
+  have hind := hG.indistinguishable.map (f := fun n y => naorCommit id (r n) (b n) y)
+    (.of_tidy hmap)
   simpa only [← naorCommitEnsemble_eq_map, uniformList_map_naorCommit_id] using hind
 
 /-- **Computational hiding of Naor bit commitment (deterministic-family formulation).**

Complexity/Crypto/Computational/OneWay.lean

@@ -108,11 +108,11 @@ theorem OneWay.inversion_negligible {f : List Bool → List Bool} (h : OneWay f)
 
 /-- Establish one-wayness by bounding every efficient inverter's success probability. -/
 theorem OneWay.of_inversion_negligible {f : List Bool → List Bool}
-    (hf : ComputableTidilyInPolyTime f encBits encBits)
+    (hf : ComputableInPolyTime f encBits encBits)
     (h : ∀ adversary : Inverter, IsPPT encBits adversary →
       Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f adversary n)))) :
     OneWay f := by
-  refine ⟨.of_tidy hf, fun adversary hPPT => ?_⟩
+  refine ⟨hf, fun adversary hPPT => ?_⟩
   simpa only [Game.advantage_pure_false] using h adversary hPPT
 
 /-- A length-preserving permutation that is one-way against every uniform PPT inverter. -/

Complexity/Crypto/Computational/OneWay/Normalize.lean

@@ -91,7 +91,8 @@ theorem OneWay.normalize {f : List Bool → List Bool} (hf : OneWay f) (bound :
     (hbound : ComputableTidilyInPolyTime bound encUnary encUnary) :
     OneWay (OneWayNormalization.normalize f bound) := by
   apply OneWay.of_inversion_negligible
-    (OneWayNormalization.computableTidilyInPolyTime_normalize hf.polyTime.tidy hbound)
+    (.of_tidy <|
+      OneWayNormalization.computableTidilyInPolyTime_normalize hf.polyTime.tidy hbound)
   intro adversary hPPT
   have hreduce : IsPPT encBits (fun n image =>
       adversary n (BitString.padWord (bound n) image)) := by ppt

Complexity/Crypto/Computational/OneWayToSignature.lean

@@ -148,7 +148,7 @@ theorem SignatureScheme.OneTimeEUFCMA.exists_oneWay {S : SignatureScheme}
   have hf : ComputableTidilyInPolyTime f encBits encBits :=
     (ComputableTidilyInPolyTime.of_eq (encIn := encPair encUnary encBits) (encMid := encBits)
       fun _ => rfl).comp (hparam.prod hpk)
-  refine ⟨f, OneWay.of_inversion_negligible hf ?_⟩
+  refine ⟨f, OneWay.of_inversion_negligible (.of_tidy hf) ?_⟩
   intro adversary hadversary
   let forgerBody (n : ℕ) (pk : List Bool) : ProbComp (List Bool × List Bool) := do
     let size ← sampleDyadicIndex (schedule (n + 1))

Complexity/Crypto/Computational/PRGToOneWay.lean

@@ -148,7 +148,7 @@ theorem PseudorandomGenerator.oneWay_of_card_le {generator : List Bool → List
     (hgenerator : PseudorandomGenerator generator ℓ) {ε : ℕ → ℝ≥0} (hε : Negligible ε)
     (P : ℕ → Finset (List Bool)) (hP : ∀ n (x : List Bool), ℓ x.length = ℓ n → x ∈ P n)
     (hcard : ∀ n, (#(P n) : ℝ≥0) ≤ ε n * 2 ^ ℓ n) : OneWay generator := by
-  refine OneWay.of_inversion_negligible hgenerator.polyTime.tidy fun adversary hadversary => ?_
+  refine OneWay.of_inversion_negligible hgenerator.polyTime fun adversary hadversary => ?_
   have hind := hgenerator.indistinguishable (test generator adversary)
     (isPPT_test hgenerator.polyTime.tidy hadversary)
   refine negligible_of_le (hind.add_fun hε) fun n => ?_

ComplexityTests.lean

@@ -118,6 +118,7 @@ import ComplexityTests.Crypto.KeyChainSecurity
 import ComplexityTests.Crypto.LeveledSecurity
 import ComplexityTests.Crypto.MAC
 import ComplexityTests.Crypto.MerkleDamgard
+import ComplexityTests.Crypto.PlainConstructors
 import ComplexityTests.Crypto.SchnorrDiscreteLog
 import ComplexityTests.Crypto.SigmaIdentification
 import ComplexityTests.Crypto.SigmaProtocol

ComplexityTests/Crypto/PlainConstructors.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Crypto.Computational.PRGToOneWay
+
+/-! Public cryptographic constructors accept ordinary deterministic certificates. -/
+
+open Cslib Cslib.Crypto Cslib.Probability Turing.MultiTapeTM
+
+example {f : List Bool → List Bool} (hf : ComputableInPolyTime f encBits encBits)
+    (hnegligible : ∀ adversary : Inverter, IsPPT encBits adversary →
+      Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f adversary n)))) :
+    OneWay f := OneWay.of_inversion_negligible hf hnegligible
+
+-- The real reduction uses the PRG's existing plain field, without a public tidy conversion.
+example {generator : List Bool → List Bool} {length : ℕ → ℕ}
+    (hgenerator : PseudorandomGenerator generator length) (hdouble : ∀ n, 2 * n ≤ length n) :
+    OneWay generator := hgenerator.oneWay hdouble
+
+-- Both the unary parameter and arbitrary sample word are part of the certified input.
+example {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) :
+    ComputationallyIndistinguishable (fun n => (X n).map (fun word => word.take n))
+      (fun n => (Y n).map (fun word => word.take n)) :=
+  h.map (by polytime)
+
+/-- info: 'Cslib.Crypto.OneWay.of_inversion_negligible' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs (whitespace := lax) in
+#print axioms OneWay.of_inversion_negligible

abstracts/ComplexityAbstracts/CryptographyBridge.lean

@@ -125,7 +125,7 @@ def OneWay (f : List Bool → List Bool) : Prop :=
 theorem oneWay_iff {f : List Bool → List Bool} : OneWay f ↔ Crypto.OneWay f := by
   constructor
   · rintro ⟨hf, hsecure⟩
-    apply Crypto.OneWay.of_inversion_negligible (polyTime_iff.mp hf)
+    apply Crypto.OneWay.of_inversion_negligible (.of_tidy (polyTime_iff.mp hf))
     intro adversary ha
     have h := hsecure (fun n word => ProbComp.eval (adversary n word))
       (strictPPT_iff.mpr ⟨fun p => adversary p.1 p.2, ha, fun _ => rfl⟩)

scripts/tidy_surface_baseline.json

@@ -335,7 +335,6 @@
  "Complexity/Computability/TreeEval/Space.lean": 2,
  "Complexity/Computability/USTCON/Reader/Cert.lean": 3,
  "Complexity/Computability/USTCON/Space.lean": 1,
- "Complexity/Crypto/Computational/Basic.lean": 1,
  "Complexity/Crypto/Computational/Commitment.lean": 13,
  "Complexity/Crypto/Computational/Encryption/PolyTime.lean": 2,
  "Complexity/Crypto/Computational/GGM/Evaluation.lean": 3,
@@ -376,7 +375,7 @@
  "Complexity/Crypto/Computational/Homomorphic/Leveled/Security.lean": 3,
  "Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean": 6,
  "Complexity/Crypto/Computational/Hybrid/Sequence.lean": 4,
- "Complexity/Crypto/Computational/OneWay.lean": 4,
+ "Complexity/Crypto/Computational/OneWay.lean": 3,
  "Complexity/Crypto/Computational/OneWay/BPP.lean": 1,
  "Complexity/Crypto/Computational/OneWay/MCSP.lean": 6,
  "Complexity/Crypto/Computational/OneWay/NP.lean": 6,