refactor(probabilistic): accept plain preprocessing certificates

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

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

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]

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)

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
 

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
 

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

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)

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]
 

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
 

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

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

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

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)

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

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