diff --git a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean
index bd20091bc7..e049eb2a31 100644
--- a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean
+++ b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean
@@ -27,6 +27,7 @@ import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Probabilistic.Sampling
 import Complexity.Probability.PMF.Event
 import Complexity.Probability.PMF.Uniform
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Reductions of promise problems, randomized reductions, and gap problems
@@ -615,7 +616,7 @@ theorem PolyTimeReducible.mem_PromiseBPP (h : PolyTimeReducible encA encB X Y)
   obtain ⟨f, hf, hfyes, hfno⟩ := h
   obtain ⟨M, hM, hyes, hno⟩ := mem_PromiseBPP_iff_exists_isPPTOn.mp hY
   exact mem_PromiseBPP_iff_exists_isPPTOn.mpr
-    ⟨fun a => M (f a), hM.preprocess hf.tidy, fun a ha => hyes (f a) (hfyes ha),
+    ⟨fun a => M (f a), hM.preprocess hf, fun a ha => hyes (f a) (hfyes ha),
       fun a ha => hno (f a) (hfno ha)⟩
 
 /-- **`PromiseRP` is closed under polynomial-time reductions.** -/
@@ -624,7 +625,7 @@ theorem PolyTimeReducible.mem_PromiseRP (h : PolyTimeReducible encA encB X Y)
   obtain ⟨f, hf, hfyes, hfno⟩ := h
   obtain ⟨M, hM, hyes, hno⟩ := mem_PromiseRP_iff_exists_isPPTOn.mp hY
   exact mem_PromiseRP_iff_exists_isPPTOn.mpr
-    ⟨fun a => M (f a), hM.preprocess hf.tidy, fun a ha => hyes (f a) (hfyes ha),
+    ⟨fun a => M (f a), hM.preprocess hf, fun a ha => hyes (f a) (hfyes ha),
       fun a ha => hno (f a) (hfno ha)⟩
 
 /-- **`PromiseCoRP` is closed under polynomial-time reductions.** -/
@@ -633,7 +634,7 @@ theorem PolyTimeReducible.mem_PromiseCoRP (h : PolyTimeReducible encA encB X Y)
   obtain ⟨f, hf, hfyes, hfno⟩ := h
   obtain ⟨M, hM, hyes, hno⟩ := mem_PromiseCoRP_iff_exists_isPPTOn.mp hY
   exact mem_PromiseCoRP_iff_exists_isPPTOn.mpr
-    ⟨fun a => M (f a), hM.preprocess hf.tidy, fun a ha => hyes (f a) (hfyes ha),
+    ⟨fun a => M (f a), hM.preprocess hf, fun a ha => hyes (f a) (hfyes ha),
       fun a ha => hno (f a) (hfno ha)⟩
 
 /-! ### Randomized reductions with one-sided error -/
@@ -918,7 +919,7 @@ theorem PolyTimeReducible.trans_rpReducibleWithError {s : β → ℝ}
     RPReducibleWithError encA encC (fun a => s (hXY.choose a)) X Z := by
   have hf := hXY.choose_spec
   obtain ⟨R, hR, hyes, hno⟩ := hYZ
-  exact ⟨fun a => R (hXY.choose a), hR.preprocess hf.1.tidy,
+  exact ⟨fun a => R (hXY.choose a), hR.preprocess hf.1,
     fun a ha c hc => hyes _ (hf.2.1 ha) c hc, fun a ha => hno _ (hf.2.2 ha)⟩
 
 /-- Postcomposing an `RPReducibleWithError` reduction with a deterministic polynomial-time reduction
diff --git a/Complexity/Computability/Probabilistic/Adaptive.lean b/Complexity/Computability/Probabilistic/Adaptive.lean
index c2f4385ea7..1d2b1a2b12 100644
--- a/Complexity/Computability/Probabilistic/Adaptive.lean
+++ b/Complexity/Computability/Probabilistic/Adaptive.lean
@@ -14,6 +14,7 @@ import Complexity.Computability.Probabilistic.Oracle.Composition
 import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Strict PPT adaptive iteration
@@ -139,7 +140,8 @@ theorem IsPPTOn.iterate_of_bounded_growth {initial : α → State} {count : α 
       (stateEncoding next).length ≤ (stateEncoding state).length + growth) :
     IsPPTOn input stateEncoding (fun a => OracleComp.iterate (count a) step (initial a)) :=
   IsPPTOn.iterateWith_of_bounded_growth (step := fun _ => step) hcount hinitial
-    (hstep.preprocess (ComputableTidilyInPolyTime.snd input stateEncoding))
+    (hstep.preprocess (Turing.MultiTapeTM.ComputableInPolyTime.of_tidy
+      (ComputableTidilyInPolyTime.snd input stateEncoding)))
     (.const growth) (fun _ => hgrowth)
 
 /-- Iteration of a step that never increases its encoded state needs no extra size invariant. -/
diff --git a/Complexity/Computability/Probabilistic/BoundedUniform.lean b/Complexity/Computability/Probabilistic/BoundedUniform.lean
index 29d9b9c21a..67884f8e8a 100644
--- a/Complexity/Computability/Probabilistic/BoundedUniform.lean
+++ b/Complexity/Computability/Probabilistic/BoundedUniform.lean
@@ -79,7 +79,7 @@ theorem isPPTOn_sampleUniformInterval_binary {α : Type} {input : α ↪ List Bo
     funext p
     simp only [min_def, Function.comp_def, decide_eq_true_eq]
   have hs : IsPPTOn input encNat (fun a => sampleBoundedIndex (bound a)) := by
-    apply ((isPPTOn_sampleBinaryNat.preprocess hw).map_with
+    apply ((isPPTOn_sampleBinaryNat.preprocess (ComputableInPolyTime.of_tidy hw)).map_with
       (f := fun a value => min (bound a) value) (.of_tidy hmin)).congr
     intro a
     rw [sampleBoundedIndex_eq_binary, ← hwidth_eq a]
diff --git a/Complexity/Computability/Probabilistic/CenteredBinomial.lean b/Complexity/Computability/Probabilistic/CenteredBinomial.lean
index 004d32d355..ca248d5608 100644
--- a/Complexity/Computability/Probabilistic/CenteredBinomial.lean
+++ b/Complexity/Computability/Probabilistic/CenteredBinomial.lean
@@ -13,6 +13,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.IntBi
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary
 import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Probabilistic.Sampling
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Native centered binomial sampling
@@ -55,7 +56,7 @@ theorem isPPTOn_sampleCenteredBinomial :
       ((hcast.comp ((ComputableTidilyInPolyTime.fst _ _).snd')).prod
         (hcast.comp (ComputableTidilyInPolyTime.snd _ _)))
   have hsecond := (hcount.preprocess
-    (ComputableTidilyInPolyTime.fst encUnary encUnary)).map_with
+    (ComputableInPolyTime.fst encUnary encUnary)).map_with
       (f := fun (p : ℕ × ℕ) (negative : ℕ) => (p.2 : ℤ) - negative) (.of_tidy hsub)
   unfold sampleCenteredBinomial
   apply hcount.bind_with
@@ -70,4 +71,5 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleCenteredBinomial {α
     (hparameter : ComputableTidilyInPolyTime parameter input encUnary) :
     Cslib.Probability.IsPPTOn input encIntBin
       (fun a => Cslib.ProbComp.sampleCenteredBinomial (parameter a)) :=
-  Cslib.Probability.isPPTOn_sampleCenteredBinomial.preprocess hparameter
+  Cslib.Probability.isPPTOn_sampleCenteredBinomial.preprocess
+    (Turing.MultiTapeTM.ComputableInPolyTime.of_tidy hparameter)
diff --git a/Complexity/Computability/Probabilistic/PPT/Composition.lean b/Complexity/Computability/Probabilistic/PPT/Composition.lean
index df5076b095..b93588e00a 100644
--- a/Complexity/Computability/Probabilistic/PPT/Composition.lean
+++ b/Complexity/Computability/Probabilistic/PPT/Composition.lean
@@ -9,6 +9,8 @@ module
 
 public import Complexity.Computability.Probabilistic.PPT.Clock
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition
+public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Probabilistic.Oracle.Composition
 
 /-!
@@ -42,7 +44,7 @@ calculus.
 
 namespace Cslib.Probability
 
-open Turing.MultiTapeTM (ComputableTidilyInPolyTime)
+open Turing.MultiTapeTM (ComputableInPolyTime ComputableTidilyInPolyTime)
 
 variable {α β γ : Type} {input : α ↪ List Bool} {middle : β ↪ List Bool}
   {output : γ ↪ List Bool}
@@ -64,7 +66,7 @@ theorem IsPPTOn.bind {first : α → ProbComp β} {second : β → ProbComp γ}
 @[fun_prop]
 theorem IsPPTOn.preprocess {program : β → ProbComp γ} {prepare : α → β}
     (hprogram : IsPPTOn middle output program)
-    (hprepare : ComputableTidilyInPolyTime prepare input middle) :
+    (hprepare : ComputableInPolyTime prepare input middle) :
     IsPPTOn input output (fun a => program (prepare a)) := by
   simpa only [pure_bind] using hprepare.isPPTOn.bind hprogram
 
diff --git a/Complexity/Computability/Probabilistic/Parameter.lean b/Complexity/Computability/Probabilistic/Parameter.lean
index 2cd0d31167..40a33bb673 100644
--- a/Complexity/Computability/Probabilistic/Parameter.lean
+++ b/Complexity/Computability/Probabilistic/Parameter.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Probabilistic.PPT
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
 import Complexity.Computability.Probabilistic.PPT.Composition
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Uniform PPT with a security parameter
@@ -71,7 +72,8 @@ theorem IsPPT.preprocess {α : Type} {input : α ↪ List Bool}
     (hparameter : ComputableTidilyInPolyTime parameter input encUnary)
     (hauxiliary : ComputableTidilyInPolyTime auxiliary input encBits) :
     IsPPTOn input output (fun a => program (parameter a) (auxiliary a)) :=
-  h.on.preprocess (hparameter.prod hauxiliary)
+  h.on.preprocess
+    (Turing.MultiTapeTM.ComputableInPolyTime.of_tidy (hparameter.prod hauxiliary))
 
 end Cslib.Probability
 
diff --git a/Complexity/Computability/Probabilistic/Presample.lean b/Complexity/Computability/Probabilistic/Presample.lean
index 330dbf4346..c6cd66b2a4 100644
--- a/Complexity/Computability/Probabilistic/Presample.lean
+++ b/Complexity/Computability/Probabilistic/Presample.lean
@@ -12,6 +12,7 @@ public import Complexity.Languages.Probabilistic.Presample
 import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Efficient oracle substitution with saved samples
diff --git a/Complexity/Computability/Probabilistic/Sampling.lean b/Complexity/Computability/Probabilistic/Sampling.lean
index cde1a48fe3..2de19384ff 100644
--- a/Complexity/Computability/Probabilistic/Sampling.lean
+++ b/Complexity/Computability/Probabilistic/Sampling.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Probabilistic.PPT.Composition
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Sampling
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Certified fair-bit and word sampling
@@ -68,4 +69,5 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleList {α : Type}
     {input : α ↪ List Bool} {count : α → ℕ}
     (hcount : ComputableTidilyInPolyTime count input encUnary) :
     Cslib.Probability.IsPPTOn input encBits (fun a => Cslib.BitString.sampleList (count a)) :=
-  Cslib.Probability.isPPTOn_sampleList.preprocess hcount
+  Cslib.Probability.isPPTOn_sampleList.preprocess
+    (Turing.MultiTapeTM.ComputableInPolyTime.of_tidy hcount)
diff --git a/Complexity/Computability/Probabilistic/Traverse.lean b/Complexity/Computability/Probabilistic/Traverse.lean
index 846afc4e74..717f2ccb1f 100644
--- a/Complexity/Computability/Probabilistic/Traverse.lean
+++ b/Complexity/Computability/Probabilistic/Traverse.lean
@@ -17,6 +17,7 @@ import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Tactic.PolyTime.Init
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Strict PPT list traversal
@@ -116,7 +117,7 @@ theorem IsPPTOn.mapMWith {α β γ : Type} {input : α ↪ List Bool}
     IsPPTOn input (encList output) (fun a => (list a).mapM (program a)) := by
   have hpairs : ComputableTidilyInPolyTime (fun a => (list a).map fun b => (a, b))
       input (encList (encPair input element)) := by fun_prop
-  apply (hprogram.mapM.preprocess hpairs).congr
+  apply (hprogram.mapM.preprocess (ComputableInPolyTime.of_tidy hpairs)).congr
   intro a
   simp only [List.mapM_map, Function.comp_def]
 
diff --git a/Complexity/Computability/Probabilistic/UniformNat.lean b/Complexity/Computability/Probabilistic/UniformNat.lean
index 9aeaf1d3ee..3b90ec917b 100644
--- a/Complexity/Computability/Probabilistic/UniformNat.lean
+++ b/Complexity/Computability/Probabilistic/UniformNat.lean
@@ -111,7 +111,7 @@ theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleBinaryNat {α : Type
     (hwidth : ComputableTidilyInPolyTime width input encUnary) :
     Cslib.Probability.IsPPTOn input encNat
       (fun a => Cslib.ProbComp.sampleBinaryNat (width a)) :=
-  Cslib.Probability.isPPTOn_sampleBinaryNat.preprocess hwidth
+  Cslib.Probability.isPPTOn_sampleBinaryNat.preprocess (.of_tidy hwidth)
 
 namespace Cslib.Probability
 
diff --git a/Complexity/Crypto/Computational/CollisionResistant.lean b/Complexity/Crypto/Computational/CollisionResistant.lean
index f33f4abd1d..15853cdc80 100644
--- a/Complexity/Crypto/Computational/CollisionResistant.lean
+++ b/Complexity/Crypto/Computational/CollisionResistant.lean
@@ -185,7 +185,7 @@ theorem isPPT_collisionGame {H : List Bool → List Bool → List Bool}
       (encPair encUnary encBits) encBool)
     (ha : IsPPT (encPair encBits encBits) adversary) :
     IsPPT encBool (fun n _ => collisionGame H valid adversary n) :=
-  ((isPPTOn_collisionGame hH hvalid ha).preprocess (ComputableTidilyInPolyTime.fst _ _)).isPPT
+  ((isPPTOn_collisionGame hH hvalid ha).preprocess (ComputableInPolyTime.fst _ _)).isPPT
 
 /-- Collision resistance of a keyed hash family `H` on the valid input domain `valid`: every
 uniform strict PPT collision finder has negligible success probability. -/
diff --git a/Complexity/Crypto/Computational/GeneratorXor.lean b/Complexity/Crypto/Computational/GeneratorXor.lean
index e3831f1feb..bdb8d5b61c 100644
--- a/Complexity/Crypto/Computational/GeneratorXor.lean
+++ b/Complexity/Crypto/Computational/GeneratorXor.lean
@@ -15,6 +15,7 @@ public import Complexity.Crypto.Computational.Basic
 import Complexity.Probability.Product
 import Complexity.Probability.Uniform
 import Complexity.Tactic.PPT
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # XOR combination of independently seeded generators
@@ -202,6 +203,7 @@ theorem isPPTOn_test {α : Type} {input : α ↪ List Bool}
   apply hadversary.preprocess (prepare := fun p : α × List Bool =>
     (p.1, generate (count p.1) (seedBits p.1) (outputBits p.1)
       (fun j coins => if j = index p.1 then challenge p.1 else generator p.1 j coins) p.2))
+  apply ComputableInPolyTime.of_tidy
   apply ComputableTidilyInPolyTime.prod (by fun_prop)
   apply isPolyTime_generate (by fun_prop) (by fun_prop) (by fun_prop) ?_ (by fun_prop)
   have hgen := hgenerator.comp
diff --git a/Complexity/Crypto/Computational/Homomorphic/Efficiency.lean b/Complexity/Crypto/Computational/Homomorphic/Efficiency.lean
index dc6ba933e0..59ef6698bb 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Efficiency.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Efficiency.lean
@@ -12,6 +12,7 @@ public import Complexity.Crypto.Computational.Homomorphic.Circuit.PolyTime
 public import Complexity.Computability.Probabilistic.Traverse
 import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Uniform polynomial-time homomorphic refresh
@@ -61,9 +62,10 @@ theorem isPPTOn_encryptBits
     (hbits : ComputableTidilyInPolyTime bits input encBits) :
     IsPPTOn input (encList encBits) (fun a => E.encryptBits (n a) (pk a) (bits a)) := by
   apply IsPPTOn.mapMWith (element := encBool)
-  · exact hencrypt.preprocess (show ComputableTidilyInPolyTime
-      (fun p : α × Bool => (n p.1, pk p.1, p.2))
-      (encPair input encBool) (encPair encUnary (encPair encBits encBool)) by fun_prop)
+  · exact hencrypt.preprocess (ComputableInPolyTime.of_tidy
+      (show ComputableTidilyInPolyTime
+        (fun p : α × Bool => (n p.1, pk p.1, p.2))
+        (encPair input encBool) (encPair encUnary (encPair encBits encBool)) by fun_prop))
   · exact ComputableTidilyInPolyTime.bitsToList.comp hbits
 
 variable {secretWidth ciphertextWidth : ℕ → ℕ}
@@ -88,13 +90,14 @@ theorem isPPTOn_refresh
   have hparameter := hn.comp
     (ComputableTidilyInPolyTime.fst input (encList encBits))
   have hcircuit := hD.comp hparameter
-  exact hevaluate.preprocess (show ComputableTidilyInPolyTime
-    (fun p : α × List (List Bool) =>
-      (n p.1, pk p.1, ⟨_, D.circuit (n p.1)⟩, encryptedKey p.1 ++ p.2))
-    (encPair input (encList encBits))
-    (encPair encUnary (encPair encBits (encPair (Boolean.encCircuit 1) (encList encBits)))) by
-    exact hparameter.prod ((hpk.comp (ComputableTidilyInPolyTime.fst _ _)).prod
-      (hcircuit.prod (by fun_prop))))
+  exact hevaluate.preprocess (ComputableInPolyTime.of_tidy
+      (show ComputableTidilyInPolyTime
+      (fun p : α × List (List Bool) =>
+        (n p.1, pk p.1, ⟨_, D.circuit (n p.1)⟩, encryptedKey p.1 ++ p.2))
+      (encPair input (encList encBits))
+      (encPair encUnary (encPair encBits (encPair (Boolean.encCircuit 1) (encList encBits)))) by
+      exact hparameter.prod ((hpk.comp (ComputableTidilyInPolyTime.fst _ _)).prod
+        (hcircuit.prod (by fun_prop)))))
 
 /-- NAND refresh is strict PPT. The certificate constructs the augmented circuit and charges
 both bit-encryption traversals and both copies of the encrypted secret key. -/
@@ -111,18 +114,19 @@ theorem isPPTOn_refreshNand
   have hsecond' : IsPPTOn (encPair input (encList encBits)) (encList encBits)
       (fun p : α × List (List Bool) => E.encryptBits (n p.1) (pk p.1) (second p.1)) :=
     (isPPTOn_encryptBits hencrypt hn hpk hsecond).preprocess
-      (ComputableTidilyInPolyTime.fst _ _)
+      (ComputableInPolyTime.fst _ _)
   apply hsecond'.bind_with
   have hparameter := hn.comp
     ((ComputableTidilyInPolyTime.fst (encPair input (encList encBits)) (encList encBits)).fst')
   have haug := (computableTidilyInPolyTime_augmentNand.comp hD).comp hparameter
-  exact hevaluate.preprocess (show ComputableTidilyInPolyTime
-    (fun p : (α × List (List Bool)) × List (List Bool) =>
-      (n p.1.1, pk p.1.1, ⟨_, augmentNand (D.circuit (n p.1.1))⟩,
-        (encryptedKey p.1.1 ++ p.1.2) ++ (encryptedKey p.1.1 ++ p.2)))
-    (encPair (encPair input (encList encBits)) (encList encBits))
-    (encPair encUnary (encPair encBits (encPair (Boolean.encCircuit 1) (encList encBits)))) by
-    exact hparameter.prod ((hpk.comp
-      ((ComputableTidilyInPolyTime.fst _ _).fst')).prod (haug.prod (by fun_prop))))
+  exact hevaluate.preprocess (ComputableInPolyTime.of_tidy
+      (show ComputableTidilyInPolyTime
+      (fun p : (α × List (List Bool)) × List (List Bool) =>
+        (n p.1.1, pk p.1.1, ⟨_, augmentNand (D.circuit (n p.1.1))⟩,
+          (encryptedKey p.1.1 ++ p.1.2) ++ (encryptedKey p.1.1 ++ p.2)))
+      (encPair (encPair input (encList encBits)) (encList encBits))
+      (encPair encUnary (encPair encBits (encPair (Boolean.encCircuit 1) (encList encBits)))) by
+      exact hparameter.prod ((hpk.comp
+        ((ComputableTidilyInPolyTime.fst _ _).fst')).prod (haug.prod (by fun_prop)))))
 
 end Cslib.Crypto.Homomorphic.Scheme
diff --git a/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
index a2ecd5c5ca..d4716e2bfe 100644
--- a/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
@@ -11,6 +11,7 @@ public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Basic
 public import Complexity.Crypto.Computational.Homomorphic.Evaluation.PolyTime
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
 public import Complexity.Computability.Circuit.Boolean.DepthTime.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Probabilistic.PPT.Capture
 
 /-!
@@ -60,7 +61,7 @@ The key generator has no circuit-size or depth parameter. -/
 theorem isPPTOn_keyGen
     (hn : ComputableTidilyInPolyTime n input encUnary) :
     IsPPTOn input (encPair encBits encBits) (fun a => keyGen E (n a)) := by
-  apply (hkeyGen.preprocess hn).bind_with
+  apply (hkeyGen.preprocess (.of_tidy hn)).bind_with
   have hbits := Scheme.isPPTOn_encryptBits hencrypt
     (show ComputableTidilyInPolyTime
       (fun p : α × (List Bool × List Bool) => n p.1)
@@ -86,7 +87,7 @@ theorem isPPTOn_encrypt {bit : α → Bool}
     (hbit : ComputableTidilyInPolyTime bit input encBool) :
     IsPPTOn input encBits (fun a => encrypt E (n a) (pk a) (bit a)) := by
   have hpublic := publicKeyDecoder.computableTidilyInPolyTime.comp hpk
-  exact hencrypt.preprocess (hn.prod (hpublic.fst'.prod hbit))
+  exact hencrypt.preprocess (.of_tidy (hn.prod (hpublic.fst'.prod hbit)))
 
 variable {secretWidth ciphertextWidth : ℕ → ℕ}
   (D : DecryptionCircuits E secretWidth ciphertextWidth)
diff --git a/Complexity/Crypto/Computational/Homomorphic/FixedKey/Reduction.lean b/Complexity/Crypto/Computational/Homomorphic/FixedKey/Reduction.lean
index c24cc39a1e..c50105f43e 100644
--- a/Complexity/Crypto/Computational/Homomorphic/FixedKey/Reduction.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/FixedKey/Reduction.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Encoding
 public import Complexity.Crypto.Computational.Homomorphic.Efficiency
 import Complexity.Probability.PMF.Bind
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Tactic.PPT
 
 /-!
@@ -92,7 +93,7 @@ theorem isPPT_zeroAdversary
   · change IsPPTOn (encPair encUnary encBits) (encPair (encPair encBool encBool) encBits)
       (fun p => (zeroAdversary E adversary).choose p.1 p.2)
     dsimp only [zeroAdversary]
-    apply (hkeyGen.preprocess (ComputableTidilyInPolyTime.fst encUnary encBits)).bind_with
+    apply (hkeyGen.preprocess (ComputableInPolyTime.fst encUnary encBits)).bind_with
     have hbits : IsPPTOn
         (encPair (encPair encUnary encBits) (encPair encBits encBits)) (encList encBits)
         (fun p => E.encryptBits p.1.1 p.1.2 (List.replicate p.2.2.length false)) := by
diff --git a/Complexity/Crypto/Computational/Homomorphic/FixedKey/Security.lean b/Complexity/Crypto/Computational/Homomorphic/FixedKey/Security.lean
index 50717c2764..b7d87d3465 100644
--- a/Complexity/Crypto/Computational/Homomorphic/FixedKey/Security.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/FixedKey/Security.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Reduction
 public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Basic
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Probabilistic.PPT.Composition
 
 /-!
@@ -86,9 +87,10 @@ theorem negligible_publicKeyGame {E : Scheme}
   have hgame := isPPTOn_publicKeyGame hencrypt hadversary bit
   have htest : IsPPT encBool (fun n word =>
       publicKeyGame E adversary bit n (publicKeyDecoder.decode word)) :=
-    hgame.preprocess ((ComputableTidilyInPolyTime.fst encUnary encBits).prod
+    hgame.preprocess (ComputableInPolyTime.of_tidy
+      ((ComputableTidilyInPolyTime.fst encUnary encBits).prod
       (publicKeyDecoder.computableTidilyInPolyTime.comp
-        (ComputableTidilyInPolyTime.snd encUnary encBits)))
+        (ComputableTidilyInPolyTime.snd encUnary encBits))))
   have h := hcircular _ htest
   simpa only [distinguishingGame, PMF.monad_bind_eq_bind, PMF.bind_map, Function.comp_def,
     publicKeyDecoder.decode_enc, ProbComp.eval_bind] using h
diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/PolyTime.lean
index b4646d9965..80c5cb9b2a 100644
--- a/Complexity/Crypto/Computational/Homomorphic/KeyChain/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/KeyChain/PolyTime.lean
@@ -11,6 +11,7 @@ public import Complexity.Crypto.Computational.Homomorphic.KeyChain
 public import Complexity.Crypto.Computational.Homomorphic.Efficiency
 import Complexity.Computability.Probabilistic.PPT.Capture
 import Complexity.Computability.Probabilistic.Repeat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 
 /-!
@@ -54,7 +55,7 @@ theorem isPPTOn_generateKeys
     (hdepth : ComputableTidilyInPolyTime depth input encUnary) :
     IsPPTOn input (encList (encPair encBits encBits))
       (fun a => E.generateKeys (n a) (depth a)) := by
-  exact (hkeyGen.preprocess hn).replicate (by fun_prop)
+  exact (hkeyGen.preprocess (.of_tidy hn)).replicate (by fun_prop)
 
 include hencrypt in
 /-- Encrypt every adjacent secret-key link, including all copied public keys and key bits. -/
diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/PolyTime.lean
index c32e198890..c6fa786663 100644
--- a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/PolyTime.lean
@@ -11,6 +11,7 @@ public import Complexity.Crypto.Computational.Homomorphic.KeyChain.Reduction
 public import Complexity.Crypto.Computational.Homomorphic.KeyChain.Hybrid.PolyTime
 public import Complexity.Computability.Probabilistic.UniformNat
 import Complexity.Computability.Probabilistic.Repeat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Tactic.PPT
 
 /-!
@@ -63,13 +64,13 @@ theorem isPPTOn_chooseLinkAt {n beforeCount afterCount bitIndex : α → ℕ}
     IsPPTOn input (encPair (encPair encBool encBool) encBits)
       (fun a => E.chooseLinkAt (n a) (beforeCount a) (afterCount a) (bitIndex a)
         (challengePk a)) := by
-  have hkey := hkeyGen.preprocess hn
+  have hkey := hkeyGen.preprocess (.of_tidy hn)
   have hfront := hkey.replicate hbefore
   have hback := hkey.replicate hafter
   unfold chooseLinkAt
   apply hfront.bind_with
-  apply (hkey.preprocess (ComputableTidilyInPolyTime.fst _ _)).bind_with
-  apply (hback.preprocess (ComputableTidilyInPolyTime.fst _ _).fst').bind_with
+  apply (hkey.preprocess (ComputableInPolyTime.fst _ _)).bind_with
+  apply (hback.preprocess (ComputableInPolyTime.fst _ _).fst').bind_with
   have hstate : ComputableTidilyInPolyTime
       (fun p : ((α × List (List Bool × List Bool)) × (List Bool × List Bool)) ×
         List (List Bool × List Bool) =>
@@ -116,7 +117,7 @@ theorem isPPTOn_guessLink {n : α → ℕ} {state challengeCiphertext : α → L
   unfold guessLink
   apply IsPPTOn.cond hcontext.fst'
   · apply hlinks.bind_with
-    exact htest.preprocess (show ComputableTidilyInPolyTime
+    exact htest.preprocess (ComputableInPolyTime.of_tidy (show ComputableTidilyInPolyTime
       (fun p : α × List (List (List Bool)) => (n p.1,
         ((linkStateDecoder.decode (state p.1)).2.1 ++
           (linkStateDecoder.decode (state p.1)).2.2.1 ::
@@ -127,7 +128,7 @@ theorem isPPTOn_guessLink {n : α → ℕ} {state challengeCiphertext : α → L
       (encPair encUnary (encPair (encList encBits) (encList (encList encBits)))) by
         exact (hn.comp (ComputableTidilyInPolyTime.fst _ _)).prod
           ((hpublic.comp (ComputableTidilyInPolyTime.fst _ _)).prod
-            (ComputableTidilyInPolyTime.snd _ _)))
+            (ComputableTidilyInPolyTime.snd _ _))))
   · ppt
 
 include hkeyGen hencrypt htest
diff --git a/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean
index 665daa374a..9594bd74b8 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean
@@ -95,7 +95,7 @@ theorem isPPTOn_evaluateNode
     · apply IsPPTOn.cond hcode.fst'.snd'
       · exact isPPTOn_refreshNand hencrypt hevaluate D hD hn hpk hek hfirst hsecond
       · exact isPPTOn_refresh hencrypt hevaluate D hD hn hpk hek hfirst
-    · exact hencrypt.preprocess (hn.prod (hpk.prod hcode.fst'.snd'))
+    · exact hencrypt.preprocess (.of_tidy (hn.prod (hpk.prod hcode.fst'.snd')))
   have hcap := (computableTidilyInPolyTime_decryptionArity D hD).comp hn
   have hbounded := hraw.map_with (f := fun a ciphertext =>
     ciphertext.take (secretWidth (n a) + ciphertextWidth (n a)))
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
index 380491a976..8875b3c15b 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
@@ -97,7 +97,7 @@ theorem isPPTOn_encrypt {bit : α → Bool}
   have hpublic := publicKeyDecoder.computableTidilyInPolyTime.comp hpk
   have hfirst := (ComputableTidilyInPolyTime.listGetD (encA := encBits) []).comp
     (hpublic.fst'.prod (ComputableTidilyInPolyTime.const 0))
-  exact (hencrypt.preprocess (hn.prod (hfirst.prod hbit))).map (by fun_prop)
+  exact (hencrypt.preprocess (.of_tidy (hn.prod (hfirst.prod hbit)))).map (by fun_prop)
 
 variable {secretWidth ciphertextWidth : ℕ → ℕ}
   (D : DecryptionCircuits E secretWidth ciphertextWidth)
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/PolyTime.lean
index a12a969391..ff5e8a7e3e 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/PolyTime.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.Homomorphic.Leveled.Reduction
 public import Complexity.Crypto.Computational.Homomorphic.KeyChain.Hybrid.PolyTime
 import Complexity.Computability.Probabilistic.Repeat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Tactic.PPT
 
 /-!
@@ -48,7 +49,8 @@ theorem isPPTOn_publicKeyGame (bit : Bool) :
       (fun p => publicKeyGame E adversary bit p.1 p.2) := by
   have hchoose := hadversary.choose
   have hguess := hadversary.guess
-  have hpublic := (ComputableTidilyInPolyTime.snd encUnary encPublicKey).encoded
+  have hpublic := ComputableInPolyTime.of_tidy
+    (ComputableTidilyInPolyTime.snd encUnary encPublicKey).encoded
   unfold publicKeyGame
   dsimp only [encPublicKey] at hpublic ⊢
   ppt
@@ -66,7 +68,7 @@ theorem isPPT_zeroLinkAdversary
       (fun p => (zeroLinkAdversary E depth adversary).choose p.1 p.2)
     dsimp only [zeroLinkAdversary]
     have hrest := (hkeyGen.preprocess
-      (ComputableTidilyInPolyTime.fst encUnary encBits)).replicate
+      (ComputableInPolyTime.fst encUnary encBits)).replicate
         (hdepth.comp (ComputableTidilyInPolyTime.fst encUnary encBits))
     apply hrest.bind_with
     have hlinks : IsPPTOn
diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean
index 4b08f4689f..4dae8e58e9 100644
--- a/Complexity/Crypto/Computational/MAC.lean
+++ b/Complexity/Crypto/Computational/MAC.lean
@@ -19,6 +19,7 @@ import Complexity.Languages.Probabilistic.Oracle.Simulation
 import Complexity.Probability.PMF
 import Complexity.Tactic.PolyTime
 import Complexity.Tactic.PPT
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Uniform message authentication codes and PRF-based MACs
@@ -167,7 +168,7 @@ attribute [program_certificate] keyGen_ppt sign_ppt verify_polyTime
 private theorem isPPTOn_keyGen_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ List Bool}
     {n : γ → ℕ} (hn : ComputableTidilyInPolyTime n encIn encUnary) :
     IsPPTOn encIn encBits (fun a => M.keyGen (n a)) :=
-  M.keyGen_ppt.preprocess hn
+  M.keyGen_ppt.preprocess (ComputableInPolyTime.of_tidy hn)
 
 @[local fun_prop]
 private theorem isPPTOn_sign_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ List Bool}
@@ -175,7 +176,7 @@ private theorem isPPTOn_sign_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ Li
     (hsk : ComputableTidilyInPolyTime sk encIn encBits)
     (hmsg : ComputableTidilyInPolyTime msg encIn encBits) :
     IsPPTOn encIn encBits (fun a => M.sign (sk a) (msg a)) :=
-  M.sign_ppt.preprocess (hsk.prod hmsg)
+  M.sign_ppt.preprocess (ComputableInPolyTime.of_tidy (hsk.prod hmsg))
 
 @[local fun_prop]
 private theorem computableTidilyInPolyTime_verify_comp (M : MACScheme)
@@ -264,7 +265,7 @@ theorem isPPTOn_eufCmaGame (M : MACScheme) {adversary : Forger}
 theorem isPPT_eufCmaGame (M : MACScheme) {adversary : Forger}
     (hadversary : IsOraclePPT (encPair encBits encBits) adversary) :
     IsPPT encBool (fun n _ => M.eufCmaGame adversary n) :=
-  ((M.isPPTOn_eufCmaGame hadversary).preprocess (ComputableTidilyInPolyTime.fst _ _)).isPPT
+  ((M.isPPTOn_eufCmaGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT
 
 /-- Fresh-message existential unforgeability under adaptive chosen-message attack (`EUFCMA`) for a
 symmetric MAC against uniform strict oracle-PPT adversaries.
@@ -383,7 +384,7 @@ input. -/
 theorem isPPT_eufOneTimeGame (M : MACScheme) {adversary : Forger}
     (hadversary : IsOraclePPT (encPair encBits encBits) adversary) :
     IsPPT encBool (fun n _ => M.eufOneTimeGame adversary n) :=
-  ((M.isPPTOn_eufOneTimeGame hadversary).preprocess (ComputableTidilyInPolyTime.fst _ _)).isPPT
+  ((M.isPPTOn_eufOneTimeGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT
 
 /-- Existential unforgeability under one-time adaptive chosen-message attack for a symmetric MAC. -/
 def OneTimeEUFCMA (M : MACScheme) : Prop :=
@@ -660,7 +661,7 @@ theorem isPPTOn_sufCmaGame (M : MACScheme) {adversary : Forger}
 theorem isPPT_sufCmaGame (M : MACScheme) {adversary : Forger}
     (hadversary : IsOraclePPT (encPair encBits encBits) adversary) :
     IsPPT encBool (fun n _ => M.sufCmaGame adversary n) :=
-  ((M.isPPTOn_sufCmaGame hadversary).preprocess (ComputableTidilyInPolyTime.fst _ _)).isPPT
+  ((M.isPPTOn_sufCmaGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT
 
 /-- Strong (fresh-pair) existential unforgeability under adaptive chosen-message attack (`SUFCMA`)
 for a symmetric MAC against uniform strict oracle-PPT adversaries
diff --git a/Complexity/Crypto/Computational/OneWay/MCSP.lean b/Complexity/Crypto/Computational/OneWay/MCSP.lean
index 4b484a5c47..879089e088 100644
--- a/Complexity/Crypto/Computational/OneWay/MCSP.lean
+++ b/Complexity/Crypto/Computational/OneWay/MCSP.lean
@@ -29,6 +29,7 @@ import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 import Complexity.Probability.PMF.Expect
 import Complexity.Probability.PMF.Map
 import Complexity.Probability.Uniform
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # MCSP in BPP rules out one-way functions
@@ -299,7 +300,8 @@ theorem isOraclePPT_mcspDistinguisher (d : ℕ)
   apply IsOraclePPTOn.isOraclePPT
   exact IsOraclePPTOn.bind_with
     (isOraclePPTOn_queryTable.preprocess (computableTidilyInPolyTime_tableQueries d))
-    ((isPPTOn_mcspRun hV).preprocess (computableTidilyInPolyTime_tableInstance d)).isOraclePPTOn
+    ((isPPTOn_mcspRun hV).preprocess
+      (ComputableInPolyTime.of_tidy (computableTidilyInPolyTime_tableInstance d))).isOraclePPTOn
 
 /-! ### The advantage of the distinguisher -/
 
diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean
index efcf3a1a49..1365d98e43 100644
--- a/Complexity/Crypto/Computational/OneWayToSignature.lean
+++ b/Complexity/Crypto/Computational/OneWayToSignature.lean
@@ -24,6 +24,7 @@ import Complexity.Crypto.Negligible.Basic
 import Complexity.Probability.PMF
 import Complexity.Tactic.PolyTime
 import Complexity.Tactic.PPT
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Equivalence between one-way functions and one-time digital signatures, and necessity for EUF-CMA
@@ -178,7 +179,7 @@ theorem SignatureScheme.OneTimeEUFCMA.exists_oneWay {S : SignatureScheme}
     have hcand : IsPPTOn (encPair (encPair encUnary encBits) encUnary) encBits
         (fun q : (ℕ × List Bool) × ℕ =>
           adversary q.2 (encPair encUnary encBits (q.1.1, q.1.2))) :=
-      hadversary.on.preprocess hprep_cand
+      hadversary.on.preprocess (ComputableInPolyTime.of_tidy hprep_cand)
     have hsk : ComputableTidilyInPolyTime
         (fun r : ((ℕ × List Bool) × ℕ) × List Bool => (evaluate r.1.1.1 r.2).2)
         (encPair (encPair (encPair encUnary encBits) encUnary) encBits) encBits := by
@@ -646,7 +647,7 @@ theorem isPPT_lamportInverter {f : List Bool → List Bool}
           ((ComputableTidilyInPolyTime.fst _ _).comp (ComputableTidilyInPolyTime.fst _ _))
       exact listGetDWithInput (computableTidilyInPolyTime_frames hsig)
         ((ComputableTidilyInPolyTime.unary_div_const 2).comp hj_proj) []
-    exact (hrun_base.preprocess hprep).bind_with hpost.isPPTOn
+    exact (hrun_base.preprocess (ComputableInPolyTime.of_tidy hprep)).bind_with hpost.isPPTOn
   have hbranch : IsPPTOn (encPair (encPair encUnary encBits) encUnary) encBits
       (fun q : (ℕ × List Bool) × ℕ =>
         if q.2 < 2 * q.1.1 then do
diff --git a/Complexity/Crypto/Computational/Signature.lean b/Complexity/Crypto/Computational/Signature.lean
index 4fc5279590..7f6f04a6a5 100644
--- a/Complexity/Crypto/Computational/Signature.lean
+++ b/Complexity/Crypto/Computational/Signature.lean
@@ -121,7 +121,7 @@ attribute [program_certificate] keyGen_ppt sign_ppt verify_polyTime
 theorem isPPTOn_keyGen_comp (S : SignatureScheme) {γ : Type} {encIn : γ ↪ List Bool}
     {n : γ → ℕ} (hn : ComputableTidilyInPolyTime n encIn encUnary) :
     IsPPTOn encIn (encPair encBits encBits) (fun a => S.keyGen (n a)) :=
-  S.keyGen_ppt.preprocess hn
+  S.keyGen_ppt.preprocess (ComputableInPolyTime.of_tidy hn)
 
 @[program_certificate, fun_prop]
 theorem isPPTOn_sign_comp (S : SignatureScheme) {γ : Type} {encIn : γ ↪ List Bool}
@@ -129,7 +129,7 @@ theorem isPPTOn_sign_comp (S : SignatureScheme) {γ : Type} {encIn : γ ↪ List
     (hsk : ComputableTidilyInPolyTime sk encIn encBits)
     (hmsg : ComputableTidilyInPolyTime msg encIn encBits) :
     IsPPTOn encIn encBits (fun a => S.sign (sk a) (msg a)) :=
-  S.sign_ppt.preprocess (hsk.prod hmsg)
+  S.sign_ppt.preprocess (ComputableInPolyTime.of_tidy (hsk.prod hmsg))
 
 @[program_certificate, fun_prop]
 theorem computableTidilyInPolyTime_verify_comp (S : SignatureScheme)
@@ -228,7 +228,7 @@ theorem isPPTOn_eufCmaGame (S : SignatureScheme) {adversary : Forger}
 theorem isPPT_eufCmaGame (S : SignatureScheme) {adversary : Forger}
     (hadversary : IsOraclePPT (encPair encBits encBits) adversary) :
     IsPPT encBool (fun n _ => S.eufCmaGame adversary n) :=
-  ((S.isPPTOn_eufCmaGame hadversary).preprocess (ComputableTidilyInPolyTime.fst _ _)).isPPT
+  ((S.isPPTOn_eufCmaGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT
 
 /-- Existential unforgeability under adaptive chosen-message attack (EUF-CMA) against uniform
 strict oracle-PPT adversaries. -/
@@ -344,7 +344,7 @@ input. -/
 theorem isPPT_eufOneTimeGame (S : SignatureScheme) {adversary : Forger}
     (hadversary : IsOraclePPT (encPair encBits encBits) adversary) :
     IsPPT encBool (fun n _ => S.eufOneTimeGame adversary n) :=
-  ((S.isPPTOn_eufOneTimeGame hadversary).preprocess (ComputableTidilyInPolyTime.fst _ _)).isPPT
+  ((S.isPPTOn_eufOneTimeGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT
 
 /-- Existential unforgeability under one-time adaptive chosen-message attack against uniform strict
 oracle-PPT adversaries. -/
diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean
index b922fc5294..e66f82a230 100644
--- a/Complexity/Crypto/Computational/Stretch.lean
+++ b/Complexity/Crypto/Computational/Stretch.lean
@@ -15,6 +15,7 @@ import Complexity.Crypto.Game.Hybrid
 import Complexity.Computability.Probabilistic.UniformNat
 import Complexity.Probability.PMF.Map
 import Complexity.Tactic.PPT
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Polynomial stretch from one-bit pseudorandom generators
@@ -335,7 +336,7 @@ theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → Lis
       encBool (fun input => reduction input.1.1 input.1.2 input.2) := by
     unfold reduction
     exact isPPT_test (hgenerator.comp hprepare) (by polytime) (by polytime)
-      (hadversary.preprocess hprepare) (by polytime)
+      (hadversary.preprocess (ComputableInPolyTime.of_tidy hprepare)) (by polytime)
   have h := (hsecure reduction hreduce).polynomiallyBounded_mul (loss_polynomial hcount)
   exact h.congr' (Filter.Eventually.of_forall (fun n => (test_advantage_eq _ _ _ _).symm))
 
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index 367a9da0c6..c5abe7bc52 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -346,6 +346,7 @@ import ComplexityTests.PartialMCSP
 import ComplexityTests.PlainAutomationSupport
 import ComplexityTests.PlainCapturedMap
 import ComplexityTests.PlainLawfulBEq
+import ComplexityTests.PlainPPTPreprocess
 import ComplexityTests.PlainPurePPT
 import ComplexityTests.PolySpaceFold
 import ComplexityTests.PolyTimeBinaryWord
diff --git a/ComplexityTests/Crypto/FixedKeySecurity.lean b/ComplexityTests/Crypto/FixedKeySecurity.lean
index 429d86539f..81937fe542 100644
--- a/ComplexityTests/Crypto/FixedKeySecurity.lean
+++ b/ComplexityTests/Crypto/FixedKeySecurity.lean
@@ -35,7 +35,8 @@ private theorem readSelf_ppt : IsPPT encBool readSelf := by
       encBits encBool :=
     (ComputableTidilyInPolyTime.headD (encA := encBool) (encL := encBits) false).comp
       ((ComputableTidilyInPolyTime.headD (encA := encBits) []).comp hdecode.snd')
-  exact hread.isPPTOn.preprocess (ComputableTidilyInPolyTime.snd encUnary encBits)
+  exact hread.isPPTOn.preprocess
+    (.of_tidy (ComputableTidilyInPolyTime.snd encUnary encBits))
 
 private theorem eval_readSelf (real : Bool) (n : ℕ) :
     distinguishingGame
@@ -79,7 +80,8 @@ private theorem readJoint_ppt : IsPPT encBool readJoint := by
       (fun word => (FixedKey.publicKeyDecoder.decode word).1.headD false ^^
         ((FixedKey.publicKeyDecoder.decode word).2.headD []).headD false)
       encBits encBool := by fun_prop
-  exact hread.isPPTOn.preprocess (ComputableTidilyInPolyTime.snd encUnary encBits)
+  exact hread.isPPTOn.preprocess
+    (.of_tidy (ComputableTidilyInPolyTime.snd encUnary encBits))
 
 private theorem eval_masked (real : Bool) (n : ℕ) :
     ProbComp.eval (Encryption.circularPublicKey maskedKeyGen maskedEncrypt real n) =
diff --git a/ComplexityTests/OraclePPT.lean b/ComplexityTests/OraclePPT.lean
index f5747b5c76..d359d07ed9 100644
--- a/ComplexityTests/OraclePPT.lean
+++ b/ComplexityTests/OraclePPT.lean
@@ -238,8 +238,8 @@ example : IsPPTOn (encList encBool) (encPair encBits encBits) (fun word =>
         unfold respond
         fun_prop
       apply h.preprocess
-      exact (ComputableTidilyInPolyTime.listToBits.comp
-        (ComputableTidilyInPolyTime.fst _ _)).prod (ComputableTidilyInPolyTime.snd _ _))
+      exact ComputableInPolyTime.of_tidy ((ComputableTidilyInPolyTime.listToBits.comp
+        (ComputableTidilyInPolyTime.fst _ _)).prod (ComputableTidilyInPolyTime.snd _ _)))
     (by fun_prop)
     (fun caller state => caller.length ≤ state.length) (fun _ => le_rfl) (by fun_prop)
   intro caller request state hstate result hresult
diff --git a/ComplexityTests/PlainPPTPreprocess.lean b/ComplexityTests/PlainPPTPreprocess.lean
new file mode 100644
index 0000000000..389db16bc3
--- /dev/null
+++ b/ComplexityTests/PlainPPTPreprocess.lean
@@ -0,0 +1,27 @@
+/-
+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.Computability.Probabilistic.PPT.Composition
+
+/-! Ordinary preprocessing retains complete input, intermediate and output encodings. -/
+
+open Turing.MultiTapeTM Cslib.Probability
+
+example {α β γ : Type} {input : α ↪ List Bool} {middle : β ↪ List Bool}
+    {output : γ ↪ List Bool} {program : β → Cslib.ProbComp γ} {prepare : α → β}
+    (hprogram : IsPPTOn middle output program)
+    (hprepare : ComputableInPolyTime prepare input middle) :
+    IsPPTOn input output (fun a => program (prepare a)) :=
+  hprogram.preprocess hprepare
+
+example {α β γ : Type} {input : α ↪ List Bool} {middle : β ↪ List Bool}
+    {output : γ ↪ List Bool} {program : β → Cslib.ProbComp γ} {prepare : α → β}
+    (hprogram : IsPPTOn middle output program)
+    (hprepare : ComputableInPolyTime prepare input middle) :
+    IsPPTOn input output (fun a => program (prepare a)) := by
+  fail_if_success (clear hprepare; fun_prop)
+  fail_if_success (clear hprogram; fun_prop)
+  fun_prop
diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json
index 787f3a8863..873dd974e7 100644
--- a/scripts/tidy_surface_baseline.json
+++ b/scripts/tidy_surface_baseline.json
@@ -130,7 +130,7 @@
  "Complexity/Computability/Probabilistic/OracleSimulation.lean": 1,
  "Complexity/Computability/Probabilistic/PPT.lean": 1,
  "Complexity/Computability/Probabilistic/PPT/Capture.lean": 4,
- "Complexity/Computability/Probabilistic/PPT/Composition.lean": 2,
+ "Complexity/Computability/Probabilistic/PPT/Composition.lean": 1,
  "Complexity/Computability/Probabilistic/Parameter.lean": 2,
  "Complexity/Computability/Probabilistic/Presample.lean": 2,
  "Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean": 1,