From 1274b0bbd382ac50d136d963e0e8d02307d0a4f9 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 06:17:52 +0000 Subject: [PATCH 1/2] refactor(wordram): state transport_inO plainly (#456) --- Complexity/Computability/WordRAM/Native.lean | 7 ++++--- ComplexityTests/GenericRAMSimulation.lean | 4 ++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/WordRAM/Native.lean b/Complexity/Computability/WordRAM/Native.lean index 8a5515cfb..08dfbdfed 100644 --- a/Complexity/Computability/WordRAM/Native.lean +++ b/Complexity/Computability/WordRAM/Native.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.WordRAM.Generic public import Complexity.Computability.GenericRAM.Simulation.Run +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pi public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option @@ -395,7 +396,7 @@ def transportCertificate (enc : B.genericModel.Encoding) (N : B.genericModel.Nat rw [hden a] exact ⟨m, hm, executes_toGeneric_iff.mpr hex⟩ -/-- Parameterized `ComputableTidilyInO` transport theorem from `WordRAM.Executes`. -/ +/-- Parameterized `ComputableInO` transport theorem from `WordRAM.Executes`. -/ theorem transport_inO (enc : B.genericModel.Encoding) (N : B.genericModel.NativePrimitives enc) (p : Program B r) {f : α → ℕ} {cfg : α → ℕ} {initState : α → FiniteState B.genericModel r} {u : α → State r} {steps : α → ℕ} @@ -404,12 +405,12 @@ theorem transport_inO (enc : B.genericModel.Encoding) (N : B.genericModel.Native (cInit : NativeCertificate initState ei (FiniteState.encoding enc)) (hden : ∀ a, (initState a).denote = (u a).toGeneric B) (hExec : ∀ a, ∃ m ≤ steps a, Executes (cfg a) p (u a) (f a) m) : - ComputableTidilyInO f ei enc.value + Turing.MultiTapeTM.ComputableInO f ei enc.value (fun a => cSteps.time a + (cCfg.time a + cInit.time a) + FiniteState.runTime enc N p.toGeneric (steps a, (cfg a, initState a))) (fun a => cSteps.space a + (cCfg.space a + cInit.space a) + FiniteState.runSpace enc N p.toGeneric (steps a, (cfg a, initState a))) := - (transportCertificate enc N p cSteps cCfg cInit hden hExec).computes + .of_tidy (transportCertificate enc N p cSteps cCfg cInit hden hExec).computes /-- Automatic `ComputableInPolyTime` transport corollary from `WordRAM.Executes`. -/ theorem transport_polyTime (enc : B.genericModel.Encoding) diff --git a/ComplexityTests/GenericRAMSimulation.lean b/ComplexityTests/GenericRAMSimulation.lean index e13ca96fe..60a7d9f0b 100644 --- a/ComplexityTests/GenericRAMSimulation.lean +++ b/ComplexityTests/GenericRAMSimulation.lean @@ -455,10 +455,10 @@ theorem wordDoubleProgram_executes (x : ℕ) : obtain ⟨m, hm, hex⟩ := FiniteState.executes_of_run_eq_inr (wordDoubleProgram_run x) exact ⟨m, hm, Cslib.WordRAM.executes_toGeneric_iff.mp hex⟩ -/-- Whole-run `ComputableTidilyInO` bound transported from `wordDoubleProgram` via +/-- Whole-run `ComputableInO` bound transported from `wordDoubleProgram` via `Cslib.WordRAM.transport_inO` and `Basis.standard.nativePrimitives`. -/ theorem wordDouble_inO : - ComputableTidilyInO (fun x : ℕ => x + x) encNat encNat + Turing.MultiTapeTM.ComputableInO (fun x : ℕ => x + x) encNat encNat (fun x => wordDoubleStepsCert.time x + (wordDoubleWidthCert.time x + wordDoubleInitCert.time x) + FiniteState.runTime Cslib.WordRAM.Basis.standard.encoding From ac5ddc21c0731222b772a2f415d3cd029d0b2135 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 07:36:08 +0000 Subject: [PATCH 2/2] chore(wordram): drop Native.lean from tidy surface baseline (#456) --- scripts/tidy_surface_baseline.json | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 1049fe2f6..adec39e90 100644 --- a/scripts/tidy_surface_baseline.json +++ b/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/Computability/WordRAM/Native.lean": 1, "Complexity/Crypto/Computational/Basic.lean": 1, "Complexity/Crypto/Computational/Commitment.lean": 13, "Complexity/Crypto/Computational/Encryption/PolyTime.lean": 2,