From 2cfbb172543810cec43d6373f6e61f69546f60ee Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 10:28:55 -0400 Subject: [PATCH 1/2] feat(WordRAM): explicit-degree overhead for the Turing-machine simulation (#739) Make the degree of the word-RAM => Turing-machine simulation explicit. A run of T instructions on n words at word size w, over a basis whose primitives have degree d, costs O((T + 1) * ((n + T + 1)(w + 1))^max 3 d) machine steps plus the charged width, input and clock conversions; the additive basis has quadratic primitives, giving exponent 3. Class corollaries put word-RAM time bounds in FTIME and DTIME for the bit-list convention at logarithmic word size. - NativeCertificate.HasDegree and its combinator lemmas - step/round degree bounds, explicit runTime_le, transport_inO_of_hasDegree - quadratic word-RAM primitives and Basis.additive.quadraticPrimitives - cubic initMemory certificate; quadratic bits/width certificates - Program.ComputesInTime.mem_FTIME, Program.DecidesInTime.mem_DTIME Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 5 + .../Classes/FunctionTime/WordRAM.lean | 146 ++++++ .../GenericRAM/Native/Degree.lean | 280 +++++++++++ .../GenericRAM/Simulation/Degree.lean | 443 +++++++++++++++++ .../Computability/WordRAM/NativeDegree.lean | 207 ++++++++ .../WordRAM/Turing/Overhead.lean | 466 ++++++++++++++++++ ComplexityTests/WordRAMTuringOverhead.lean | 99 ++++ 7 files changed, 1646 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/FunctionTime/WordRAM.lean create mode 100644 Complexity/Computability/GenericRAM/Native/Degree.lean create mode 100644 Complexity/Computability/GenericRAM/Simulation/Degree.lean create mode 100644 Complexity/Computability/WordRAM/NativeDegree.lean create mode 100644 Complexity/Computability/WordRAM/Turing/Overhead.lean create mode 100644 ComplexityTests/WordRAMTuringOverhead.lean diff --git a/Complexity.lean b/Complexity.lean index b0e895a1a9..5c25f3191e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1170,6 +1170,7 @@ public import Complexity.Computability.Complexity.Classes.EXP public import Complexity.Computability.Complexity.Classes.FewP public import Complexity.Computability.Complexity.Classes.FewP.Machine public import Complexity.Computability.Complexity.Classes.FunctionTime +public import Complexity.Computability.Complexity.Classes.FunctionTime.WordRAM public import Complexity.Computability.Complexity.Classes.Hierarchy public import Complexity.Computability.Complexity.Classes.Hierarchy.LogClock public import Complexity.Computability.Complexity.Classes.Hierarchy.Nondeterministic @@ -1592,6 +1593,7 @@ public import Complexity.Computability.GenericRAM.Native.BooleanFold public import Complexity.Computability.GenericRAM.Native.BooleanSearch public import Complexity.Computability.GenericRAM.Native.Certificate public import Complexity.Computability.GenericRAM.Native.Combinators +public import Complexity.Computability.GenericRAM.Native.Degree public import Complexity.Computability.GenericRAM.Native.ExhaustiveCountFallback public import Complexity.Computability.GenericRAM.Native.HeavyBranchFold public import Complexity.Computability.GenericRAM.Native.IndexFold @@ -1602,6 +1604,7 @@ public import Complexity.Computability.GenericRAM.Native.StackRecursionTree public import Complexity.Computability.GenericRAM.Native.SubsetPairFold public import Complexity.Computability.GenericRAM.Signed public import Complexity.Computability.GenericRAM.Signed.Fits +public import Complexity.Computability.GenericRAM.Simulation.Degree public import Complexity.Computability.GenericRAM.Simulation.Finite public import Complexity.Computability.GenericRAM.Simulation.Run public import Complexity.Computability.GenericRAM.Simulation.Turing @@ -2318,6 +2321,7 @@ public import Complexity.Computability.WordRAM.Multiword.Sub public import Complexity.Computability.WordRAM.Multiword.Transfer public import Complexity.Computability.WordRAM.Multiword.Workspace public import Complexity.Computability.WordRAM.Native +public import Complexity.Computability.WordRAM.NativeDegree public import Complexity.Computability.WordRAM.Notation public import Complexity.Computability.WordRAM.OfTuring public import Complexity.Computability.WordRAM.PackedCount @@ -2347,6 +2351,7 @@ public import Complexity.Computability.WordRAM.Subroutine public import Complexity.Computability.WordRAM.Time public import Complexity.Computability.WordRAM.Trace public import Complexity.Computability.WordRAM.Turing +public import Complexity.Computability.WordRAM.Turing.Overhead public import Complexity.Computability.WordRAM.Width public import Complexity.Crypto.Computational.Basic public import Complexity.Crypto.Computational.CollisionResistant diff --git a/Complexity/Computability/Complexity/Classes/FunctionTime/WordRAM.lean b/Complexity/Computability/Complexity/Classes/FunctionTime/WordRAM.lean new file mode 100644 index 0000000000..c7a919bd2d --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/FunctionTime/WordRAM.lean @@ -0,0 +1,146 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Turing.Overhead +public import Complexity.Computability.Complexity.Classes.FunctionTime +public import Complexity.Computability.Complexity.Classes.Time + +/-! +# Word-RAM time bounds give deterministic time bounds + +A fixed `Basis.additive` program that computes `f` within `T n` instructions on the bits of an +input of length `n`, at every word size of at least the logarithmic threshold `logWidth k n`, gives +`f ∈ FTIME encIn encNat (t + (n + T + 1) ^ 4 · (k (size n + 1) + 1) ^ 3)`, provided the time bound +`T n` itself is computable from the input in time `O(t n)`. For `T n ≥ n` this is +`O(t n + T(n) ^ 4 log³ n)`. The decision version gives the same bound in `DTIME`. + +The simulating machine runs at the word size `k (size n + 1) = Θ(k log n)`, and its overhead is the +explicit polynomial of `Program.ComputesInTime.computableInO_of_width_additive`. The clock +hypothesis on `T` is needed because the machine computes its own step budget. The exponent `4` +comes from the association-list memory of the simulator, whose scans are cubic in the encoded +state; it is not a property of the word-RAM model. + +The input convention is that of `Complexity.Computability.WordRAM.Invariance`: the words are the +bits of `encIn a`, and the size is `|encIn a|`. Together with the converse simulations of +`Complexity.Computability.WordRAM.OfTuring`, this transfers word-RAM running times to the time +classes beyond `P`. + +## Main results + +* `Cslib.WordRAM.Program.ComputesInTime.computableInO_bits`: the simulation as a + `ComputableInO` bound depending only on the input length. +* `Cslib.WordRAM.Program.ComputesInTime.mem_FTIME`: word-RAM time gives function time. +* `Cslib.WordRAM.Program.DecidesInTime.mem_DTIME`: word-RAM decision time gives `DTIME`. + +## References + +* [S. A. Cook and R. A. Reckhow, *Time bounded random access machines*][CookReckhow1973] +-/ + +@[expose] public section + +namespace Cslib.WordRAM + +open Turing.MultiTapeTM Cslib.GenericRAM Cslib.Complexity + +variable {α : Type} {encIn : α ↪ List Bool} {r k : ℕ} + +/-- **The simulation of the bit-list convention at logarithmic word size**, with time +`O(t n + (n + T n + 1) ^ 4 · (k (size n + 1) + 1) ^ 3)` and a space bound depending only on the +input length `n`. -/ +theorem Program.ComputesInTime.computableInO_bits (hk : 1 ≤ k) {p : Program .additive r} + {T t : ℕ → ℕ} {f : α → ℕ} + (h : p.ComputesInTime (fun _ a => (encIn a).map Bool.toNat) (fun a _ => T (encIn a).length) + (fun a w => logWidth k (encIn a).length ≤ w) f) + (hT : (fun a => T (encIn a).length) ∈ FTIME encIn encNat t) : + ∃ S : ℕ → ℕ, Turing.MultiTapeTM.ComputableInO f encIn encNat + (fun a => t (encIn a).length + ((encIn a).length + T (encIn a).length + 1) ^ 4 * + (k * (Nat.size (encIn a).length + 1) + 1) ^ 3) + (fun a => S (encIn a).length) := by + obtain ⟨c₁, c₂, s, hTs⟩ := hT + have hwidth := ((logWidthBound_degree k).of_encIn_eq (encIn' := encIn) (fun a => encIn a) + fun _ => rfl).inO + have hencode := (bitsToNats_degree.of_encIn_eq (encIn' := encIn) (fun a => encIn a) + fun _ => rfl).inO + have hO := h.computableInO_of_width_additive + (width := fun a => k * (Nat.size (encIn a).length + 1)) hwidth + (fun a => logWidth_le_mul_size_succ k _) (fun a => inputFits_map_toNat hk _) hencode + (NativeCertificate.ofTimeAndSpace hTs).computes (fun _ => le_rfl) + refine ⟨fun n => n + 2 * (n + 1) ^ 2 + (s n + (c₁ * t n + c₂)) + + ((n + T n + 1) * (k * (Nat.size n + 1) + 1)) ^ 3, hO.mono (c₁ + c₂ + 5) (fun a => ?_) + (fun a => ?_)⟩ + · simp only [List.length_map, NativeCertificate.ofTimeAndSpace] + obtain ⟨X, hX⟩ : ∃ X, X = ((encIn a).length + T (encIn a).length + 1) ^ 4 * + (k * (Nat.size (encIn a).length + 1) + 1) ^ 3 := ⟨_, rfl⟩ + rw [← hX] + have hw1 : 1 ≤ (k * (Nat.size (encIn a).length + 1) + 1) ^ 3 := Nat.one_le_pow _ _ (by omega) + have hcube : (T (encIn a).length + 1) * (((encIn a).length + T (encIn a).length + 1) * + (k * (Nat.size (encIn a).length + 1) + 1)) ^ 3 ≤ X := by + rw [hX, Nat.mul_pow, ← Nat.mul_assoc] + refine Nat.mul_le_mul_right _ ?_ + calc (T (encIn a).length + 1) * ((encIn a).length + T (encIn a).length + 1) ^ 3 + ≤ ((encIn a).length + T (encIn a).length + 1) * + ((encIn a).length + T (encIn a).length + 1) ^ 3 := + Nat.mul_le_mul_right _ (by omega) + _ = ((encIn a).length + T (encIn a).length + 1) ^ 4 := by ring + have hsq : ((encIn a).length + 1) ^ 2 ≤ X := by + rw [hX] + calc ((encIn a).length + 1) ^ 2 ≤ ((encIn a).length + T (encIn a).length + 1) ^ 4 := + (Nat.pow_le_pow_left (by omega) 2).trans (Nat.pow_le_pow_right (by omega) (by omega)) + _ ≤ _ := Nat.le_mul_of_pos_right _ hw1 + have hn : (encIn a).length ≤ ((encIn a).length + 1) ^ 2 := by nlinarith + have h0 := Nat.zero_le (c₁ * X) + have h1 := Nat.zero_le (c₂ * t (encIn a).length) + have h2 := Nat.zero_le (c₂ * X) + nlinarith + · simp only [List.length_map, NativeCertificate.ofTimeAndSpace] + refine le_trans ?_ (Nat.le_mul_of_pos_left _ (by omega)) + omega + +/-- **Word-RAM time gives function time.** A `Basis.additive` program computing `f` within +`T n` instructions on the bits of an input of length `n`, at every word size of at least +`logWidth k n`, computes a function in `FTIME encIn encNat` with bound +`t n + (n + T n + 1) ^ 4 · (k (size n + 1) + 1) ^ 3`, when `T n` is computable from the input in +time `O(t n)`. -/ +theorem Program.ComputesInTime.mem_FTIME (hk : 1 ≤ k) {p : Program .additive r} + {T t : ℕ → ℕ} {f : α → ℕ} + (h : p.ComputesInTime (fun _ a => (encIn a).map Bool.toNat) (fun a _ => T (encIn a).length) + (fun a w => logWidth k (encIn a).length ≤ w) f) + (hT : (fun a => T (encIn a).length) ∈ FTIME encIn encNat t) : + f ∈ FTIME encIn encNat + (fun n => t n + (n + T n + 1) ^ 4 * (k * (Nat.size n + 1) + 1) ^ 3) := by + obtain ⟨S, c, hc, -⟩ := h.computableInO_bits hk hT + exact ⟨c, c, fun n => c * (S n + 1), hc.mono (fun a => by rw [Nat.mul_add, Nat.mul_one]) + (fun _ => le_rfl)⟩ + +/-- **Word-RAM decision time gives deterministic time.** A `Basis.additive` program deciding `A` +within `T n` instructions on the bits of an input of length `n`, at every word size of at least +`logWidth k n`, puts `A` in `DTIME encIn` with bound +`t n + (n + T n + 1) ^ 4 · (k (size n + 1) + 1) ^ 3`, when `T n` is computable from the input in +time `O(t n)`. -/ +theorem Program.DecidesInTime.mem_DTIME (hk : 1 ≤ k) {p : Program .additive r} + {T t : ℕ → ℕ} {A : Set α} + (h : p.DecidesInTime (fun _ a => (encIn a).map Bool.toNat) A (fun a _ => T (encIn a).length) + (fun a w => logWidth k (encIn a).length ≤ w)) + (hT : (fun a => T (encIn a).length) ∈ FTIME encIn encNat t) : + A ∈ DTIME encIn (fun n => t n + (n + T n + 1) ^ 4 * (k * (Nat.size n + 1) + 1) ^ 3) := by + classical + obtain ⟨S, hO⟩ := h.computesInTime.computableInO_bits hk hT + have hone : Turing.MultiTapeTM.ComputableInO (fun v : ℕ => decide (v = 1)) encNat encBool + (fun v => (encNat v).length) (fun v => (encNat v).length) := + ((ComputableInDegree.of_linear ComputableInLinearTimeAndSpace.natEq).comp + ((ComputableInDegree.of_eq (f := fun v : ℕ => v) (encIn := encNat) (encMid := encNat) + fun _ => rfl).prod (ComputableInDegree.const 1))).mono (d' := 1) (e' := 1) |>.inO_one + have h := setOf_mem_DTIME_of_computableInO (hone.comp_linear hO) + (t := fun n => t n + (n + T n + 1) ^ 4 * (k * (Nat.size n + 1) + 1) ^ 3) fun _ => le_rfl + convert h using 1 + ext a + by_cases ha : a ∈ A <;> simp [ha] + +end Cslib.WordRAM diff --git a/Complexity/Computability/GenericRAM/Native/Degree.lean b/Complexity/Computability/GenericRAM/Native/Degree.lean new file mode 100644 index 0000000000..4d7ce5ac04 --- /dev/null +++ b/Complexity/Computability/GenericRAM/Native/Degree.lean @@ -0,0 +1,280 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.GenericRAM.Native +public import Complexity.Computability.GenericRAM.Native.Combinators + +/-! +# Native certificates with explicit polynomial degrees + +`NativeCertificate.IsPolynomial` says that a certificate's time and space bounds are polynomial in +the encoded input length, without naming a degree. `NativeCertificate.HasDegree c d` names it: the +time and space bounds are at most a constant times `(n + 1) ^ d` on encoded inputs of length `n`, +and the encoded output has linear length. Linear output is what keeps the degree from growing under +composition: a degree-`d` bound evaluated at a linearly long intermediate value is again of degree +`d`. This is the discipline of `Turing.MultiTapeTM.ComputableInDegree` with output degree one, +applied to the input-dependent bounds that certificates carry. + +Every certificate combinator preserves `HasDegree`, so a simulation assembled from them inherits an +explicit degree from its primitives. `Model.NativePrimitives.HasDegree` asks the same of all +primitive certificates of a RAM model. + +## Main definitions + +* `Cslib.GenericRAM.NativeCertificate.HasDegree`: time and space bounds of degree `d`, encoded + output of linear length. +* `Cslib.GenericRAM.NativeCertificate.ofDegree`: the certificate of a degree-`d` computation with + linear output. +* `Cslib.GenericRAM.Model.NativePrimitives.HasDegree`: every primitive certificate has degree `d`. + +## Main results + +* `Cslib.GenericRAM.NativeCertificate.HasDegree.isPolynomial`: a degree bound is polynomial. +* `Cslib.GenericRAM.NativeCertificate.comp_hasDegree`, `.prod_hasDegree`, `.branch_hasDegree`, + `.option_hasDegree` and the other `*_hasDegree` lemmas: the combinators preserve the degree. +-/ + +@[expose] public section + +namespace Cslib.GenericRAM.NativeCertificate + +open Turing.MultiTapeTM + +variable {α β γ δ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} + {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} {d d' : ℕ} + +/-- Time and space bounds of degree `d`, and encoded output of linear length, in the encoded input +length. -/ +structure HasDegree (c : NativeCertificate f ei em) (d : ℕ) : Prop where + /-- The time bound has degree `d`. -/ + time : DegreeBounded (fun a => (ei a).length) c.time d + /-- The space bound has degree `d`. -/ + space : DegreeBounded (fun a => (ei a).length) c.space d + /-- The encoded output has linear length. -/ + length : DegreeBounded (fun a => (ei a).length) (fun a => (em (f a)).length) 1 + +namespace HasDegree + +variable {c : NativeCertificate f ei em} + +/-- Raising the degree keeps the bound. -/ +theorem mono (h : c.HasDegree d) (hd : d ≤ d') : c.HasDegree d' := + ⟨h.time.mono_deg hd, h.space.mono_deg hd, h.length⟩ + +/-- A certificate of some degree is polynomial. -/ +theorem isPolynomial (h : c.HasDegree d) : c.IsPolynomial := + ⟨h.time.polyBounded, h.space.polyBounded⟩ + +/-- Transfer a degree to a certificate with the same bounds for a pointwise equal function. This +sees through certificates defined by case analysis, whose casts block unification. -/ +theorem of_eq {f' : α → β} (c' : NativeCertificate f' ei em) (h : c.HasDegree d) + (ht : c'.time = c.time) (hs : c'.space = c.space) (hf : ∀ a, f a = f' a) : + c'.HasDegree d := + ⟨ht ▸ h.time, hs ▸ h.space, h.length.mono fun a => by rw [hf a]⟩ + +end HasDegree + +/-- A degree-`d` bound evaluated at an intermediate value of linear length has degree `d`. -/ +theorem degreeBounded_comp {size : α → ℕ} {u : β → ℕ} + (hu : DegreeBounded (fun b => (em b).length) u d) + (hf : DegreeBounded size (fun a => (em (f a)).length) 1) : + DegreeBounded size (fun a => u (f a)) d := by + simpa only [one_mul] using hu.comp hf + +/-- A linear-time, linear-space computation has encoded output of linear length. -/ +theorem length_of_linear {h : β → γ} + (hh : ComputableInO h em eo (fun b => (em b).length) (fun b => (em b).length)) : + DegreeBounded (fun b => (em b).length) (fun b => (eo (h b)).length) 1 := by + obtain ⟨k, -, hl⟩ := hh + exact ⟨k, fun b => by simpa only [pow_one] using hl b⟩ + +/-- A certificate with linear space has encoded output of linear length. -/ +theorem length_of_space (c : NativeCertificate f ei em) + (hs : DegreeBounded (fun a => (ei a).length) c.space 1) : + DegreeBounded (fun a => (ei a).length) (fun a => (em (f a)).length) 1 := by + obtain ⟨k, -, hl⟩ := c.computes + obtain ⟨C, hC⟩ := hs + refine ⟨k * (C + 1), fun a => (hl a).trans ?_⟩ + have := hC a + simp only [pow_one] at this ⊢ + nlinarith + +/-- A certificate whose time has degree `d ≥ 1` and whose space is linear has degree `d`. -/ +theorem hasDegree_of_space_linear (c : NativeCertificate f ei em) + (ht : DegreeBounded (fun a => (ei a).length) c.time d) + (hs : DegreeBounded (fun a => (ei a).length) c.space 1) (hd : 1 ≤ d) : c.HasDegree d := + ⟨ht, hs.mono_deg hd, c.length_of_space hs⟩ + +/-- The certificate of a computation in time and space degree `d` with linear output. -/ +def ofDegree (h : ComputableInDegree f ei em d 1) : NativeCertificate f ei em := + ⟨fun a => ((ei a).length + 1) ^ d, fun a => ((ei a).length + 1) ^ d, h.inO⟩ + +@[simp] theorem ofDegree_time (h : ComputableInDegree f ei em d 1) (a : α) : + (ofDegree h).time a = ((ei a).length + 1) ^ d := rfl + +@[simp] theorem ofDegree_space (h : ComputableInDegree f ei em d 1) (a : α) : + (ofDegree h).space a = ((ei a).length + 1) ^ d := rfl + +/-- `ofDegree` keeps the degree of the computation. -/ +theorem ofDegree_hasDegree (h : ComputableInDegree f ei em d 1) : (ofDegree h).HasDegree d := + ⟨⟨1, fun a => by simp⟩, ⟨1, fun a => by simp⟩, h.2⟩ + +/-! ## The combinators preserve the degree -/ + +theorem linear_hasDegree + (h : ComputableInO f ei em (fun a => (ei a).length) (fun a => (ei a).length)) (hd : 1 ≤ d) : + (linear h).HasDegree d := + ⟨DegreeBounded.self.mono_deg hd, DegreeBounded.self.mono_deg hd, length_of_linear h⟩ + +theorem const_hasDegree (b : β) (hd : 1 ≤ d) : (const (ei := ei) (em := em) b).HasDegree d := + linear_hasDegree _ hd + +theorem comp_hasDegree {h : β → γ} (c' : NativeCertificate h em eo) + (c : NativeCertificate f ei em) (hc' : c'.HasDegree d) (hc : c.HasDegree d) : + (c'.comp c).HasDegree d := + ⟨hc.time.add (degreeBounded_comp hc'.time hc.length), + hc.space.add (degreeBounded_comp hc'.space hc.length), + degreeBounded_comp (f := f) hc'.length hc.length⟩ + +theorem prod_hasDegree (c : NativeCertificate f ei em) (c' : NativeCertificate g ei eo) + (hc : c.HasDegree d) (hc' : c'.HasDegree d) : (prod c c').HasDegree d := + ⟨hc.time.add hc'.time, hc.space.add hc'.space, + ((hc.length.smul 2).add_const 1 |>.add hc'.length).mono fun a => by + simp only [length_encPair, le_refl]⟩ + +theorem post_hasDegree {h : β → γ} (c : NativeCertificate f ei em) + (hh : ComputableInO h em eo (fun b => (em b).length) (fun b => (em b).length)) + (hc : c.HasDegree d) : (post c hh).HasDegree d := + ⟨hc.time, hc.space, degreeBounded_comp (f := f) (length_of_linear hh) hc.length⟩ + +theorem fst_hasDegree {f : α → β × γ} (c : NativeCertificate f ei (encPair em eo)) + (hc : c.HasDegree d) : (fst c).HasDegree d := + post_hasDegree c _ hc + +theorem snd_hasDegree {f : α → β × γ} (c : NativeCertificate f ei (encPair em eo)) + (hc : c.HasDegree d) : (snd c).HasDegree d := + post_hasDegree c _ hc + +theorem some_hasDegree (c : NativeCertificate f ei em) (hc : c.HasDegree d) : + (some c).HasDegree d := + post_hasDegree c _ hc + +theorem inl_hasDegree (c : NativeCertificate f ei em) (right : γ ↪ List Bool) + (hc : c.HasDegree d) : (inl c right).HasDegree d := + post_hasDegree c _ hc + +theorem inr_hasDegree (left : γ ↪ List Bool) (c : NativeCertificate f ei em) + (hc : c.HasDegree d) : (inr left c).HasDegree d := + post_hasDegree c _ hc + +theorem congr_hasDegree {f' : α → β} (c : NativeCertificate f ei em) (h : ∀ a, f a = f' a) + (hc : c.HasDegree d) : (congr c h).HasDegree d := + ⟨hc.time, hc.space, hc.length.mono fun a => by rw [← h a]⟩ + +theorem pull_hasDegree {ed : δ ↪ List Bool} (c : NativeCertificate f ei em) + (hc : c.HasDegree d) (hd : 1 ≤ d) : (pull c ed).HasDegree d := + comp_hasDegree c _ hc (linear_hasDegree _ hd) + +theorem payload_hasDegree (input : α ↪ List Bool) (out : β ↪ List Bool) (hd : 1 ≤ d) : + (payload input out).HasDegree d := + linear_hasDegree _ hd + +theorem branch_hasDegree {condition : α → Bool} {f₁ f₂ : α → β} + (test : NativeCertificate condition ei encBool) + (yes : NativeCertificate f₁ ei em) (no : NativeCertificate f₂ ei em) + (ht : test.HasDegree d) (hy : yes.HasDegree d) (hn : no.HasDegree d) : + (branch test yes no).HasDegree d := by + refine ⟨(ht.time.add (hy.time.add hn.time)).mono fun a => ?_, + (ht.space.add (hy.space.add hn.space)).mono fun a => ?_, + (hy.length.add hn.length).mono fun a => ?_⟩ + · simp only [branch_time]; split <;> omega + · simp only [branch_space]; split <;> omega + · split <;> omega + +theorem option_hasDegree {value : α → Option β} {fallback : α → γ} {body : α × β → γ} + (c : NativeCertificate value ei (encOption em)) + (no : NativeCertificate fallback ei eo) + (yes : NativeCertificate body (encPair ei em) eo) + (hc : c.HasDegree d) (hno : no.HasDegree d) (hyes : yes.HasDegree d) (hd : 1 ≤ d) : + (option c no yes).HasDegree d := by + -- The continuation's input `(a, b)` is linearly long when `value a = some b`. + have hL : DegreeBounded (fun a => (ei a).length) + (fun a => 2 * (ei a).length + (encOption em (value a)).length) 1 := + (DegreeBounded.self.smul 2).add hc.length + have hpair (a : α) (b : β) (hv : value a = Option.some b) : + (encPair ei em (a, b)).length = 2 * (ei a).length + (encOption em (value a)).length := by + rw [hv]; simp; omega + -- A bound `C (|(a, b)| + 1) ^ k` on the continuation is of degree `k` in `|ei a|`. + have hsub {k C : ℕ} : DegreeBounded (fun a => (ei a).length) + (fun a => C * (2 * (ei a).length + (encOption em (value a)).length + 1) ^ k) k := by + simpa only [one_mul] using DegreeBounded.comp (size' := id) + (v := fun n => C * (n + 1) ^ k) ⟨C, fun _ => le_rfl⟩ hL + obtain ⟨ct, hyt⟩ := hyes.time + obtain ⟨cs, hys⟩ := hyes.space + obtain ⟨cl, hyl⟩ := hyes.length + refine ⟨((hc.time.smul 2).add (DegreeBounded.self.mono_deg hd) |>.add + (hno.time.add (hsub (C := ct)))).mono fun a => ?_, + ((hc.space.smul 2).add (DegreeBounded.self.mono_deg hd) |>.add + (hno.space.add (hsub (C := cs)))).mono fun a => ?_, + (hno.length.add (hsub (C := cl))).mono fun a => ?_⟩ + · simp only [option_time] + cases hv : value a with + | none => simp + | some b => + have := hyt (a, b) + dsimp only at this + rw [hpair a b hv, hv] at this + simp only [Option.elim_some] + omega + · simp only [option_space] + cases hv : value a with + | none => simp + | some b => + have := hys (a, b) + dsimp only at this + rw [hpair a b hv, hv] at this + simp only [Option.elim_some] + omega + · cases hv : value a with + | none => simp + | some b => + have := hyl (a, b) + dsimp only at this + rw [hpair a b hv, hv] at this + simp only [Option.elim_some, pow_one] at this ⊢ + omega + +end Cslib.GenericRAM.NativeCertificate + +namespace Cslib.GenericRAM.Model + +/-- Every primitive certificate of the bundle has degree `d`. -/ +structure NativePrimitives.HasDegree {M : Model.{0, 0, 0, 0}} {enc : M.Encoding} + (N : M.NativePrimitives enc) (d : ℕ) : Prop where + /-- Every literal symbol's certificate has degree `d`. -/ + constant : ∀ c, (N.constant c).HasDegree d + /-- Every operation symbol's certificate has degree `d`. -/ + operation : ∀ op, (N.operation op).HasDegree d + /-- Every test symbol's certificate has degree `d`. -/ + test : ∀ t, (N.test t).HasDegree d + /-- The address extraction certificate has degree `d`. -/ + address : N.address.HasDegree d + /-- The move validation certificate has degree `d`. -/ + validMove : N.validMove.HasDegree d + /-- The control-label validation certificate has degree `d`. -/ + validPC : N.validPC.HasDegree d + +/-- Raising the degree of a primitive bundle keeps the bound. -/ +theorem NativePrimitives.HasDegree.mono {M : Model.{0, 0, 0, 0}} {enc : M.Encoding} + {N : M.NativePrimitives enc} {d d' : ℕ} (h : N.HasDegree d) (hd : d ≤ d') : + N.HasDegree d' := + ⟨fun c => (h.constant c).mono hd, fun op => (h.operation op).mono hd, + fun t => (h.test t).mono hd, h.address.mono hd, h.validMove.mono hd, h.validPC.mono hd⟩ + +end Cslib.GenericRAM.Model diff --git a/Complexity/Computability/GenericRAM/Simulation/Degree.lean b/Complexity/Computability/GenericRAM/Simulation/Degree.lean new file mode 100644 index 0000000000..83b01e719e --- /dev/null +++ b/Complexity/Computability/GenericRAM/Simulation/Degree.lean @@ -0,0 +1,443 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.GenericRAM.Simulation.Run +public import Complexity.Computability.GenericRAM.Native.Degree + +/-! +# Explicit-degree overhead of the finite-state RAM simulation + +When every primitive certificate of a RAM model has degree `D ≥ 3` +(`Model.NativePrimitives.HasDegree`), one step of the native finite-state simulator has degree `D` +in the encoded runtime configuration and state. The `3` is the sparse-memory scan, which is cubic in +the encoded memory (`SparseMemory.scanTime_le_cube`). A clocked run of `n` steps through states of +encoded length at most `B` therefore costs `O(|input| + (n + 1) · ((B + 1) ^ D + (log n + 1) ^ 2))` +machine steps, and whole-run transport inherits this bound with every constant outside the degree. + +These are the degree analogues of the `*_isPolynomial` lemmas of +`Complexity.Computability.GenericRAM.Simulation.Run`, which give polynomial bounds of unnamed +degree. + +## Main results + +* `Cslib.GenericRAM.FiniteState.stepCertificate_hasDegree`, + `Cslib.GenericRAM.FiniteState.roundCertificate_hasDegree`: one simulated step has degree `D`. +* `Cslib.GenericRAM.FiniteState.runTime_le`, `Cslib.GenericRAM.FiniteState.runSpace_le`: explicit + bounds on a clocked run from per-round bounds and a bound on the visited states. +* `Cslib.GenericRAM.FiniteState.transport_inO_of_hasDegree`: whole-run transport with time + `O(… + (steps + 1) · ((B + 1) ^ D + (log steps + 1) ^ 2))`. + +## References + +* [S. A. Cook and R. A. Reckhow, *Time bounded random access machines*][CookReckhow1973] +-/ + +@[expose] public section + +namespace Cslib.GenericRAM.FiniteState + +open Turing.MultiTapeTM NativeCertificate + +variable {M : Model.{0, 0, 0, 0}} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {D : ℕ} + +namespace Native + +variable {s : α → FiniteState M r} {k : α → M.Config} {v : α → M.Value} + +theorem fields_hasDegree (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) + (hc : c.HasDegree D) : (fields enc c).HasDegree D := + post_hasDegree c _ hc + +theorem register_hasDegree (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) + (i : Fin r) (hc : c.HasDegree D) : (register enc c i).HasDegree D := + post_hasDegree _ _ (fst_hasDegree _ (snd_hasDegree _ (fields_hasDegree enc c hc))) + +theorem operands_hasDegree (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) + {n : ℕ} (args : Fin n → Fin r) (hc : c.HasDegree D) : + (operands enc c args).HasDegree D := + post_hasDegree _ _ (fst_hasDegree _ (snd_hasDegree _ (fields_hasDegree enc c hc))) + +theorem setCertificate_hasDegree (enc : M.Encoding) + (c : NativeCertificate s ei (encoding enc)) (d : Fin r) + (value : NativeCertificate v ei enc.value) (hc : c.HasDegree D) (hv : value.HasDegree D) : + (setCertificate enc c d value).HasDegree D := by + have hfs := fields_hasDegree enc c hc + exact post_hasDegree _ (pack enc).computes (prod_hasDegree _ _ (fst_hasDegree _ hfs) + (prod_hasDegree _ _ (post_hasDegree _ _ (prod_hasDegree _ _ + (fst_hasDegree _ (snd_hasDegree _ hfs)) hv)) (snd_hasDegree _ (snd_hasDegree _ hfs)))) + +theorem moveCertificate_hasDegree (enc : M.Encoding) (N : M.NativePrimitives enc) + (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) + (d : Fin r) (value : NativeCertificate v ei enc.value) (hD : 1 ≤ D) + (hN : N.HasDegree D) (hk : config.HasDegree D) (hc : c.HasDegree D) + (hv : value.HasDegree D) : + (moveCertificate enc N config c d value).HasDegree D := + branch_hasDegree _ _ _ + (comp_hasDegree N.validMove (prod config value) hN.validMove (prod_hasDegree _ _ hk hv)) + (some_hasDegree _ (setCertificate_hasDegree enc c d value hc hv)) + (const_hasDegree none hD) + +/-- The raw sparse-memory lookup is cubic in time and linear in space. -/ +theorem readRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : + (⟨SparseMemory.readTime enc.address enc.value, SparseMemory.readSpace enc.address enc.value, + SparseMemory.read_inO enc.address enc.value⟩ : + NativeCertificate (fun q : (M.Address × SparseMemory M.Address M.Value) × M.Value => + SparseMemory.read q.2 q.1.1 q.1.2) _ _).HasDegree D := by + refine hasDegree_of_space_linear _ (DegreeBounded.mono_deg ⟨32, fun q => ?_⟩ hD) + ⟨32, fun q => ?_⟩ (by omega) + · have hq : (SparseMemory.queryEncoding enc.address enc.value q.1).length ≤ + (SparseMemory.readEncoding enc.address enc.value q).length := by + simp only [SparseMemory.readEncoding, length_encPair]; omega + have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 + have ht := SparseMemory.scanTime_le_cube enc.address enc.value q.1 + have he : (SparseMemory.readEncoding enc.address enc.value q).length ≤ + ((SparseMemory.readEncoding enc.address enc.value q).length + 1) ^ 3 := by + ring_nf; omega + unfold SparseMemory.readTime + nlinarith + · have hs := SparseMemory.scanSpace_le_linear enc.address enc.value q.1 + simp only [SparseMemory.readSpace, SparseMemory.readEncoding, + length_encPair, pow_one] at hs ⊢ + omega + +/-- The raw sparse-memory update is cubic in time and linear in space. -/ +theorem writeRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : + (⟨SparseMemory.writeTime enc.address enc.value, SparseMemory.writeSpace enc.address enc.value, + SparseMemory.insert_inO enc.address enc.value⟩ : + NativeCertificate (fun q : (M.Address × M.Value) × SparseMemory M.Address M.Value => + q.2.insert q.1.1 q.1.2) _ _).HasDegree D := by + refine hasDegree_of_space_linear _ (DegreeBounded.mono_deg ⟨33, fun q => ?_⟩ hD) + ⟨33, fun q => ?_⟩ (by omega) + · have hq : (SparseMemory.queryEncoding enc.address enc.value (q.1.1, q.2)).length ≤ + (SparseMemory.writeEncoding enc.address enc.value q).length := by + simp only [SparseMemory.queryEncoding, SparseMemory.writeEncoding, length_encPair] + omega + have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 + have ht := SparseMemory.scanTime_le_cube enc.address enc.value (q.1.1, q.2) + have he : (SparseMemory.writeEncoding enc.address enc.value q).length ≤ + ((SparseMemory.writeEncoding enc.address enc.value q).length + 1) ^ 3 := by + ring_nf; omega + unfold SparseMemory.writeTime + nlinarith + · have hs := SparseMemory.scanSpace_le_linear enc.address enc.value (q.1.1, q.2) + simp only [SparseMemory.writeSpace, SparseMemory.queryEncoding, + SparseMemory.writeEncoding, length_encPair, pow_one] at hs ⊢ + omega + +theorem readCertificate_hasDegree (enc : M.Encoding) + (c : NativeCertificate s ei (encoding enc)) + {a : α → M.Address} (address : NativeCertificate a ei enc.address) (hD : 3 ≤ D) + (hc : c.HasDegree D) (ha : address.HasDegree D) : + (readCertificate enc c address).HasDegree D := by + have hfs := fields_hasDegree enc c hc + exact comp_hasDegree _ _ (readRaw_hasDegree enc hD) + (prod_hasDegree _ _ (prod_hasDegree _ _ ha + (snd_hasDegree _ (snd_hasDegree _ (snd_hasDegree _ hfs)))) + (fst_hasDegree _ (snd_hasDegree _ (snd_hasDegree _ hfs)))) + +theorem writeCertificate_hasDegree (enc : M.Encoding) + (c : NativeCertificate s ei (encoding enc)) + {a : α → M.Address} (address : NativeCertificate a ei enc.address) + (value : NativeCertificate v ei enc.value) (hD : 3 ≤ D) + (hc : c.HasDegree D) (ha : address.HasDegree D) (hv : value.HasDegree D) : + (writeCertificate enc c address value).HasDegree D := by + have hfs := fields_hasDegree enc c hc + have hmem := comp_hasDegree _ _ (writeRaw_hasDegree enc hD) + (prod_hasDegree _ _ (prod_hasDegree _ _ ha hv) + (snd_hasDegree _ (snd_hasDegree _ (snd_hasDegree _ hfs)))) + exact post_hasDegree _ (pack enc).computes (prod_hasDegree _ _ (fst_hasDegree _ hfs) + (prod_hasDegree _ _ (fst_hasDegree _ (snd_hasDegree _ hfs)) + (prod_hasDegree _ _ (fst_hasDegree _ (snd_hasDegree _ (snd_hasDegree _ hfs))) hmem))) + +theorem evalOpCertificate_hasDegree (enc : M.Encoding) + (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) + (c : NativeCertificate s ei (encoding enc)) (o : Op M r) (hD : 3 ≤ D) + (hN : N.HasDegree D) (hk : config.HasDegree D) (hc : c.HasDegree D) : + (evalOpCertificate enc N config c o).HasDegree D := by + have h1 : 1 ≤ D := by omega + cases o with + | const d literal => + refine (option_hasDegree _ _ _ + (comp_hasDegree _ _ (hN.constant literal) hk) + (const_hasDegree none h1) + (some_hasDegree _ (setCertificate_hasDegree enc _ d _ + (pull_hasDegree c hc h1) (payload_hasDegree ei enc.value h1))) h1).of_eq _ rfl rfl + fun a => ?_ + simp only [Function.comp_apply, evalOp] + cases M.checkedConstant literal (k a) <;> rfl + | copy d src => + exact moveCertificate_hasDegree enc N config c d (register enc c src) h1 hN hk hc + (register_hasDegree enc c src hc) + | alu op d args => + refine (option_hasDegree _ _ _ + (comp_hasDegree _ _ (hN.operation op) (prod_hasDegree _ _ hk + (operands_hasDegree enc c args hc))) + (const_hasDegree none h1) + (some_hasDegree _ (setCertificate_hasDegree enc _ d _ + (pull_hasDegree c hc h1) (payload_hasDegree ei enc.value h1))) h1).of_eq _ rfl rfl + fun a => ?_ + simp only [Function.comp_apply, evalOp] + cases M.checkedOp op (k a, (s a).regs ∘ args) <;> rfl + | load d a => + have hpullC := pull_hasDegree (ed := enc.address) c hc h1 + have hpullK := pull_hasDegree (ed := enc.address) config hk h1 + have hpay := payload_hasDegree ei enc.address h1 + refine (option_hasDegree _ _ _ + (comp_hasDegree _ _ hN.address (prod_hasDegree _ _ hk (register_hasDegree enc c a hc))) + (const_hasDegree none h1) + (moveCertificate_hasDegree enc N _ _ d _ h1 hN hpullK hpullC + (readCertificate_hasDegree enc _ _ hD hpullC hpay)) h1).of_eq _ rfl rfl fun x => ?_ + simp only [Function.comp_apply, evalOp] + cases M.address (k x) ((s x).regs a) <;> rfl + | store a src => + have hpullC := pull_hasDegree (ed := enc.address) c hc h1 + have hpullK := pull_hasDegree (ed := enc.address) config hk h1 + have hpay := payload_hasDegree ei enc.address h1 + refine (option_hasDegree _ _ _ + (comp_hasDegree _ _ hN.address (prod_hasDegree _ _ hk (register_hasDegree enc c a hc))) + (const_hasDegree none h1) + (branch_hasDegree _ _ _ + (comp_hasDegree _ _ hN.validMove (prod_hasDegree _ _ hpullK + (register_hasDegree enc _ src hpullC))) + (some_hasDegree _ (writeCertificate_hasDegree enc _ _ _ hD hpullC hpay + (register_hasDegree enc _ src hpullC))) + (const_hasDegree none h1)) h1).of_eq _ rfl rfl fun x => ?_ + simp only [Function.comp_apply, evalOp] + cases M.address (k x) ((s x).regs a) <;> rfl + +theorem resumeCertificate_hasDegree (enc : M.Encoding) (N : M.NativePrimitives enc) + (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) + (pc : ℕ) (hD : 1 ≤ D) (hN : N.HasDegree D) (hk : config.HasDegree D) + (hc : c.HasDegree D) : + (resumeCertificate enc N config c pc).HasDegree D := + branch_hasDegree _ _ _ + (comp_hasDegree _ _ hN.validPC (prod_hasDegree _ _ hk (const_hasDegree pc hD))) + (some_hasDegree _ (inl_hasDegree _ _ (post_hasDegree _ (pack enc).computes (prod_hasDegree _ _ + (const_hasDegree pc hD) (snd_hasDegree _ (fields_hasDegree enc c hc)))))) + (const_hasDegree none hD) + +theorem evalInstrCertificate_hasDegree (enc : M.Encoding) + (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) + (c : NativeCertificate s ei (encoding enc)) (nextPC : ℕ) (i : Instr M r) (hD : 3 ≤ D) + (hN : N.HasDegree D) (hk : config.HasDegree D) (hc : c.HasDegree D) : + (evalInstrCertificate enc N config c nextPC i).HasDegree D := by + have h1 : 1 ≤ D := by omega + cases i with + | op o => + refine (option_hasDegree _ _ _ + (evalOpCertificate_hasDegree enc N config c o hD hN hk hc) + (const_hasDegree none h1) + (resumeCertificate_hasDegree enc N _ _ nextPC h1 hN + (pull_hasDegree config hk h1) (payload_hasDegree ei (encoding enc) h1)) h1).of_eq _ + rfl rfl fun a => ?_ + simp only [evalInstr] + cases evalOp (k a) o (s a) <;> rfl + | jump target => + exact resumeCertificate_hasDegree enc N config c target h1 hN hk hc + | branch test target => + cases test with + | test f args => + have hpullK := pull_hasDegree (ed := encBool) config hk h1 + have hpullC := pull_hasDegree (ed := encBool) c hc h1 + refine (option_hasDegree _ _ _ + (comp_hasDegree _ _ (hN.test f) (prod_hasDegree _ _ hk + (operands_hasDegree enc c args hc))) + (const_hasDegree none h1) + (branch_hasDegree _ _ _ + (payload_hasDegree ei encBool h1) + (resumeCertificate_hasDegree enc N _ _ target h1 hN hpullK hpullC) + (resumeCertificate_hasDegree enc N _ _ nextPC h1 hN hpullK hpullC)) h1).of_eq _ + rfl rfl fun a => ?_ + simp only [Function.comp_apply, evalInstr] + cases h : M.evalTest (k a) f ((s a).regs ∘ args) with + | none => rfl + | some b => cases b <;> rfl + | halt idx => + exact branch_hasDegree _ _ _ + (comp_hasDegree _ _ hN.validMove (prod_hasDegree _ _ hk (register_hasDegree enc c idx hc))) + (some_hasDegree _ (inr_hasDegree _ _ (register_hasDegree enc c idx hc))) + (const_hasDegree none h1) + +theorem pcEquals_hasDegree (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) + (pc : ℕ) (hD : 2 ≤ D) (hc : c.HasDegree D) : + (pcEquals enc c pc).HasDegree D := by + have heq : (⟨fun p : ℕ × ℕ => ((encNat p.1).length + 1) * + ((encNat p.1).length + (encNat p.2).length + 1), + fun p : ℕ × ℕ => (encPair encNat encNat p).length, + ComputableInO.eq encNat⟩ : NativeCertificate (fun p : ℕ × ℕ => decide (p.1 = p.2)) + (encPair encNat encNat) encBool).HasDegree D := by + refine hasDegree_of_space_linear _ (DegreeBounded.mono_deg ⟨1, fun p => ?_⟩ hD) + ⟨1, fun p => by simp⟩ (by omega) + simp only [length_encPair] + nlinarith + exact comp_hasDegree _ _ heq (prod_hasDegree _ _ (fst_hasDegree _ (fields_hasDegree enc c hc)) + (const_hasDegree pc (by omega))) + +theorem dispatchCertificate_hasDegree (enc : M.Encoding) + (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) + (c : NativeCertificate s ei (encoding enc)) (p : Program M r) (pc : ℕ) (hD : 3 ≤ D) + (hN : N.HasDegree D) (hk : config.HasDegree D) (hc : c.HasDegree D) : + (dispatchCertificate enc N config c p pc).HasDegree D := by + induction p generalizing pc with + | nil => exact const_hasDegree none (by omega) + | cons i p ih => + refine congr_hasDegree _ _ ?_ + exact (branch_hasDegree _ _ _ + (pcEquals_hasDegree enc c pc (by omega) hc) + (evalInstrCertificate_hasDegree enc N config c (pc + 1) i hD hN hk hc) + (ih (pc + 1))) + +end Native + +/-- **One simulated step has degree `D`** when every primitive certificate has degree `D ≥ 3`. -/ +theorem stepCertificate_hasDegree (enc : M.Encoding) (N : M.NativePrimitives enc) + (p : Program M r) (hN : N.HasDegree D) (hD : 3 ≤ D) : + (stepCertificate enc N p).HasDegree D := by + have h1 : 1 ≤ D := by omega + have hcfg := linear_hasDegree (ComputableInO.fst enc.config (encoding (M := M) (r := r) enc)) h1 + have hst := linear_hasDegree (ComputableInO.snd enc.config (encoding (M := M) (r := r) enc)) h1 + exact branch_hasDegree _ _ _ + (comp_hasDegree _ _ hN.validPC + (prod_hasDegree _ _ hcfg (fst_hasDegree _ (Native.fields_hasDegree enc _ hst)))) + (Native.dispatchCertificate_hasDegree enc N _ _ p 0 hD hN hcfg hst) + (const_hasDegree none h1) + +/-- **One clocked round of the simulator has degree `D`** when every primitive certificate has +degree `D ≥ 3`. -/ +theorem roundCertificate_hasDegree (enc : M.Encoding) (N : M.NativePrimitives enc) + (p : Program M r) (hN : N.HasDegree D) (hD : 3 ≤ D) : + (roundCertificate enc N p).HasDegree D := by + have h1 : 1 ≤ D := by omega + have hcont : (continuingCertificate (M := M) (r := r) enc).HasDegree D := + hasDegree_of_space_linear _ (DegreeBounded.self.mono_deg h1) DegreeBounded.self h1 + have hres : (stepResultCertificate enc N p).HasDegree D := + (option_hasDegree _ _ _ + (comp_hasDegree _ _ hcont (snd_hasDegree _ (linear_hasDegree + (ComputableInO.of_eq (f := fun x : M.Config × Result M r => x) fun _ => rfl) h1))) + (snd_hasDegree _ (linear_hasDegree _ h1)) + (comp_hasDegree _ _ (stepCertificate_hasDegree enc N p hN hD) + (prod_hasDegree _ _ (fst_hasDegree _ (fst_hasDegree _ (linear_hasDegree + (ComputableInO.of_eq (f := fun x : (M.Config × Result M r) × FiniteState M r => x) + fun _ => rfl) h1))) + (snd_hasDegree _ (linear_hasDegree _ h1)))) h1).of_eq _ rfl rfl + fun q => (stepResult_eq q.1 p q.2).symm + exact prod_hasDegree _ _ (fst_hasDegree _ (linear_hasDegree _ h1)) hres + +/-! ## Clocked runs with explicit bounds -/ + +/-- The loop state after `j` rounds from a continuing state has the encoded length of the runtime +configuration and the `j`-step outcome. -/ +theorem length_loopEncoding_iterate_round (enc : M.Encoding) (p : Program M r) (j : ℕ) + (k : M.Config) (s : FiniteState M r) : + (loopEncoding enc ((round p)^[j] (k, Option.some (.inl s)))).length = + 2 * (enc.config k).length + 1 + (resultEncoding enc (run k p j s)).length := by + rw [iterate_round_inl, length_encPair] + +/-- **Explicit clocked run time.** If every round costs at most `C (ℓ + 1) ^ D` on a loop state of +encoded length `ℓ`, and the outcomes of the first `n` steps have encoded length at most `B`, then +`n` clocked steps cost at most `3 |input| + (n + 1) (C X ^ D + X + (|n| + 1) ^ 2)`, where +`X = 2 |k| + B + 2` bounds the encoded loop states plus one. -/ +theorem runTime_le (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {C : ℕ} + (hround : ∀ x, (roundCertificate enc N p).time x ≤ C * ((loopEncoding enc x).length + 1) ^ D) + (n : ℕ) (k : M.Config) (s : FiniteState M r) {B : ℕ} + (hB : ∀ j ≤ n, (resultEncoding enc (run k p j s)).length ≤ B) : + runTime enc N p (n, (k, s)) ≤ 3 * (runInputEncoding enc (n, (k, s))).length + + (n + 1) * (C * (2 * (enc.config k).length + B + 2) ^ D + + (2 * (enc.config k).length + B + 2) + ((encNat n).length + 1) ^ 2) := by + have hT := maxRoundTime_le (roundCertificate enc N p) n (k, Option.some (.inl s)) + (R := C * (2 * (enc.config k).length + B + 2) ^ D) fun j hj => by + refine (hround _).trans (Nat.mul_le_mul_left C (Nat.pow_le_pow_left ?_ D)) + have := hB j hj + rw [length_loopEncoding_iterate_round] + omega + have hL := maxStateLength_le (encPair enc.config (resultEncoding enc)) (round p) n + (k, Option.some (.inl s)) + (B := 2 * (enc.config k).length + B + 2) fun j hj => by + have := hB j hj + rw [length_loopEncoding_iterate_round] + omega + have hsum := Nat.mul_le_mul_left (n + 1) (Nat.add_le_add_right (Nat.add_le_add hT hL) + (((encNat n).length + 1) ^ 2)) + simp only [runTime, runCertificate, congr_time, snd_time, iterate_time, initLoopCertificate, + prod_time, fst_time, snd_time, some_time, inl_time, linear_time] + omega + +/-- **Explicit clocked run space.** The space analogue of `runTime_le`. -/ +theorem runSpace_le (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {C : ℕ} + (hround : ∀ x, (roundCertificate enc N p).space x ≤ C * ((loopEncoding enc x).length + 1) ^ D) + (n : ℕ) (k : M.Config) (s : FiniteState M r) {B : ℕ} + (hB : ∀ j ≤ n, (resultEncoding enc (run k p j s)).length ≤ B) : + runSpace enc N p (n, (k, s)) ≤ 3 * (runInputEncoding enc (n, (k, s))).length + + C * (2 * (enc.config k).length + B + 2) ^ D + (2 * (enc.config k).length + B + 2) + + (encNat n).length := by + have hS := maxRoundSpace_le (roundCertificate enc N p) n (k, Option.some (.inl s)) + (Q := C * (2 * (enc.config k).length + B + 2) ^ D) fun j hj => by + refine (hround _).trans (Nat.mul_le_mul_left C (Nat.pow_le_pow_left ?_ D)) + have := hB j hj + rw [length_loopEncoding_iterate_round] + omega + have hL := maxStateLength_le (encPair enc.config (resultEncoding enc)) (round p) n + (k, Option.some (.inl s)) + (B := 2 * (enc.config k).length + B + 2) fun j hj => by + have := hB j hj + rw [length_loopEncoding_iterate_round] + omega + simp only [runSpace, runCertificate, congr_space, snd_space, iterate_space, initLoopCertificate, + prod_space, fst_space, snd_space, some_space, inl_space, linear_space] + omega + +/-- **Whole-run transport with an explicit degree.** Suppose every primitive certificate of the +model has degree `D ≥ 3`, a halting run of `p` from `initState a` takes at most `steps a` +instructions, and the outcomes of its first `steps a` clocked steps have encoded length at most +`B a`. Then `f` is computable in time +`O(Tsteps + Tcfg + Tinit + |input| + (steps + 1) · (X ^ D + (|steps| + 1) ^ 2))`, where +`X = 2 |cfg| + B + 2` and `|input|` is the encoded length of `(steps, cfg, initState)`. Only the +constant factor is hidden. -/ +theorem transport_inO_of_hasDegree (enc : M.Encoding) (N : M.NativePrimitives enc) + (hN : N.HasDegree D) (hD : 3 ≤ D) (p : Program M r) + {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} + {steps : α → ℕ} + (cSteps : NativeCertificate steps ei encNat) + (cCfg : NativeCertificate cfg ei enc.config) + (cInit : NativeCertificate initState ei (encoding enc)) + (hExec : ∀ a, ∃ m ≤ steps a, + GenericRAM.Executes (cfg a) p (initState a).denote (f a) m) + {B : α → ℕ} + (hOutLen : ∀ a, ∀ j ≤ steps a, + (resultEncoding enc (run (cfg a) p j (initState a))).length ≤ B a) : + ComputableInO f ei enc.value + (fun a => cSteps.time a + cCfg.time a + cInit.time a + + (runInputEncoding enc (steps a, (cfg a, initState a))).length + + (steps a + 1) * ((2 * (enc.config (cfg a)).length + B a + 2) ^ D + + ((encNat (steps a)).length + 1) ^ 2)) + (fun a => cSteps.space a + cCfg.space a + cInit.space a + + (runInputEncoding enc (steps a, (cfg a, initState a))).length + + (2 * (enc.config (cfg a)).length + B a + 2) ^ D + (encNat (steps a)).length) := by + have hround := roundCertificate_hasDegree enc N p hN hD + obtain ⟨Ct, hCt⟩ := hround.time + obtain ⟨Cs, hCs⟩ := hround.space + refine (transport_inO enc N p cSteps cCfg cInit hExec).mono (Ct + Cs + 4) (fun a => ?_) + (fun a => ?_) + · have hrun := runTime_le enc N p hCt (steps a) (cfg a) (initState a) (hOutLen a) + set X := 2 * (enc.config (cfg a)).length + B a + 2 + have hX : X ≤ X ^ D := Nat.le_self_pow (by omega) X + have hmul := Nat.mul_le_mul_left (steps a + 1) + (show Ct * X ^ D + X + ((encNat (steps a)).length + 1) ^ 2 ≤ + (Ct + 1) * (X ^ D + ((encNat (steps a)).length + 1) ^ 2) by nlinarith) + have hc : (steps a + 1) * ((Ct + 1) * (X ^ D + ((encNat (steps a)).length + 1) ^ 2)) ≤ + (Ct + Cs + 4) * ((steps a + 1) * (X ^ D + ((encNat (steps a)).length + 1) ^ 2)) := by + rw [Nat.mul_left_comm] + exact Nat.mul_le_mul_right _ (by omega) + nlinarith + · have hrun := runSpace_le enc N p hCs (steps a) (cfg a) (initState a) (hOutLen a) + set X := 2 * (enc.config (cfg a)).length + B a + 2 + have hX : X ≤ X ^ D := Nat.le_self_pow (by omega) X + nlinarith + +end Cslib.GenericRAM.FiniteState diff --git a/Complexity/Computability/WordRAM/NativeDegree.lean b/Complexity/Computability/WordRAM/NativeDegree.lean new file mode 100644 index 0000000000..fd459dc23d --- /dev/null +++ b/Complexity/Computability/WordRAM/NativeDegree.lean @@ -0,0 +1,207 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Native +public import Complexity.Computability.GenericRAM.Native.Degree +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Pi + +/-! +# Word-RAM primitives with explicit degrees + +`WordRAM.Native` certifies each primitive of a word-RAM basis in polynomial time of unnamed degree. +Here the primitives get explicit degrees: on a unary word size and binary operands, the literal +check, the `eq`/`lt` tests, address extraction and the move and label checks all run in quadratic +time and space with output of linear length, and so do checked addition and truncated subtraction. +The fits test `v < 2 ^ w` compares the bit length of `v` with `w` in unary, without forming `2 ^ w`. + +`Basis.nativePrimitivesOfDegree` assembles a primitive bundle of degree `d ≥ 2` from degree-`d` +certificates for the operations of a basis; `Basis.additive.quadraticPrimitives` is the instance +with `d = 2`. The other bases need degree certificates for multiplication, division, +remainder, the bitwise operations and the shifts, which the machine library does not yet supply +except for multiplication. + +## Main definitions + +* `Cslib.WordRAM.Basis.nativePrimitivesOfDegree`: the primitive bundle of a basis from degree-`d` + certificates for its operations. +* `Cslib.WordRAM.Basis.additive.quadraticPrimitives`: the quadratic bundle of the additive basis. + +## Main results + +* `Cslib.WordRAM.fits_degree`: the fits test is quadratic. +* `Cslib.WordRAM.checkedAdd_degree`, `Cslib.WordRAM.checkedSub_degree`: checked addition and + subtraction are quadratic. +* `Cslib.WordRAM.Basis.nativePrimitivesOfDegree_hasDegree`, + `Cslib.WordRAM.Basis.additive.quadraticPrimitives_hasDegree`: the bundles have the stated + degree. +-/ + +@[expose] public section + +namespace Cslib.WordRAM + +open Cslib.GenericRAM Turing.MultiTapeTM ComputableInDegree + +/-- A linear-time, linear-space computation has cost and output degree one. -/ +private theorem degree_of_linear {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} + {f : α → β} (h : ComputableInO f ei eo (fun a => (ei a).length) (fun a => (ei a).length)) : + ComputableInDegree f ei eo 1 1 := + h.computableInDegree ⟨1, fun a => by simp⟩ ⟨1, fun a => by simp⟩ le_rfl + +/-- A computation in quadratic time and linear space has cost degree two and output degree one. -/ +private theorem degree_of_quadratic {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} + {f : α → β} + (h : ComputableInO f ei eo (fun a => ((ei a).length + 1) ^ 2) (fun a => (ei a).length + 1)) : + ComputableInDegree f ei eo 2 1 := + h.computableInDegree ⟨1, fun a => by simp⟩ ⟨1, fun a => by simp⟩ (by omega) + +/-- **The fits test `v < 2 ^ w` is quadratic** on a unary width and a binary value. It compares the +bit length of `v` with `w`. -/ +theorem fits_degree : + ComputableInDegree (fun p : ℕ × ℕ => decide (Fits p.1 p.2)) (encPair encUnary encNat) + encBool 2 1 := by + have hsize : ComputableInDegree (fun p : ℕ × ℕ => (encNat p.2).length) + (encPair encUnary encNat) encUnary 1 1 := + ((degree_of_linear (ComputableInO.lengthUnary.comp_enc encNat)).comp + (snd encUnary encNat)).mono + have hsub : ComputableInDegree (fun p : ℕ × ℕ => (encNat p.2).length - p.1) + (encPair encUnary encNat) encUnary 2 1 := + (unary_sub.comp (hsize.prod (fst encUnary encNat))).mono + have hzero : ComputableInDegree (fun p : ℕ × ℕ => decide ((encNat p.2).length - p.1 = 0)) + (encPair encUnary encNat) encBool 2 1 := + ((eq encUnary).comp (hsub.prod (const 0))).mono + convert hzero using 1 + funext p + refine decide_eq_decide.mpr ?_ + rw [fits_iff, encNat_apply, Nat.size_eq_bits_len, ← Nat.size_le] + omega + +/-- Checking that a quadratic word value fits the unary width is quadratic. -/ +private theorem checkFits_degree {k : ℕ} {val : ℕ × (Fin k → ℕ) → ℕ} + (hval : ComputableInDegree val (encPair encUnary (encPi encNat)) encNat 2 1) : + ComputableInDegree + (fun p : ℕ × (Fin k → ℕ) => if decide (Fits p.1 (val p)) then some (val p) else none) + (encPair encUnary (encPi encNat)) (encOption encNat) 2 1 := by + have htest : ComputableInDegree (fun p : ℕ × (Fin k → ℕ) => decide (Fits p.1 (val p))) + (encPair encUnary (encPi encNat)) encBool 2 1 := + (fits_degree.comp ((fst encUnary (encPi encNat (Index := Fin k))).prod hval)).mono + have hsome : ComputableInDegree (fun p : ℕ × (Fin k → ℕ) => some (val p)) + (encPair encUnary (encPi encNat)) (encOption encNat) 2 1 := + ((optionSome (enc₁ := encNat) (enc := encOption encNat)).comp hval).mono + exact ite_le htest hsome (const none) (by omega) (by omega) + +/-- An operand register of a binary operation, read in linear time. -/ +private theorem operand_degree (i : Fin 2) : + ComputableInDegree (fun p : ℕ × (Fin 2 → ℕ) => p.2 i) (encPair encUnary (encPi encNat)) + encNat 1 1 := + ((degree_of_linear (ComputableInO.pi_apply encNat i)).comp + (snd encUnary (encPi encNat))).mono + +/-- **Checked addition is quadratic** on a unary width and binary operands. -/ +theorem checkedAdd_degree : + ComputableInDegree (Basis.standard.genericModel.checkedOp (.bin .add)) + (encPair encUnary (encPi encNat)) (encOption encNat) 2 1 := + checkFits_degree (k := 2) (val := fun p : ℕ × (Fin 2 → ℕ) => p.2 0 + p.2 1) + (computableInDegree_add.comp ((operand_degree 0).prod (operand_degree 1))).mono + +/-- **Checked truncated subtraction is quadratic** on a unary width and binary operands. -/ +theorem checkedSub_degree : + ComputableInDegree (Basis.standard.genericModel.checkedOp (.bin .sub)) + (encPair encUnary (encPi encNat)) (encOption encNat) 2 1 := + checkFits_degree (k := 2) (val := fun p : ℕ × (Fin 2 → ℕ) => p.2 0 - p.2 1) + ((degree_of_quadratic ComputableInO.natSub).comp + ((operand_degree 1).prod (operand_degree 0))).mono + +/-- A literal is checked against the unary width in quadratic time. -/ +theorem checkedConstant_degree (B : Basis) (c : ℕ) : + ComputableInDegree (B.genericModel.checkedConstant c) encUnary (encOption encNat) 2 1 := by + have htest : ComputableInDegree (fun w : ℕ => decide (Fits w c)) encUnary encBool 2 1 := + (fits_degree.comp ((of_eq (f := fun w : ℕ => w) (encIn := encUnary) (encMid := encUnary) + fun _ => rfl).prod (const c))).mono + exact ite_le htest (const (some c)) (const none) (by omega) (by omega) + +/-- The word-RAM tests (`eq`, `lt` and the faulting test) are quadratic. -/ +theorem evalTest_degree (B : Basis) (t : Option Bool) : + ComputableInDegree (fun p => B.genericModel.evalTest p.1 t p.2) + (encPair encUnary (encPi encNat)) (encOption encBool) 2 1 := by + cases t with + | none => + change ComputableInDegree (fun _ : ℕ × (Fin 0 → ℕ) => (none : Option Bool)) + (encPair encUnary (encPi encNat (Index := Fin 0))) (encOption encBool) 2 1 + exact (const none).mono + | some b => + have hxy := (operand_degree 0).prod (operand_degree 1) + cases b + · change ComputableInDegree + (fun p : ℕ × (Fin 2 → ℕ) => some (decide (p.2 0 = p.2 1))) + (encPair encUnary (encPi encNat (Index := Fin 2))) (encOption encBool) 2 1 + exact ((optionSome (enc₁ := encBool) (enc := encOption encBool)).comp + ((of_linear ComputableInLinearTimeAndSpace.natEq).comp hxy)).mono + · change ComputableInDegree + (fun p : ℕ × (Fin 2 → ℕ) => some (decide (p.2 0 < p.2 1))) + (encPair encUnary (encPi encNat (Index := Fin 2))) (encOption encBool) 2 1 + exact ((optionSome (enc₁ := encBool) (enc := encOption encBool)).comp + ((degree_of_quadratic ComputableInO.natLt).comp hxy)).mono + +/-- Word-RAM address extraction is linear. -/ +theorem address_degree (B : Basis) : + ComputableInDegree (fun p => B.genericModel.address p.1 p.2) + (encPair encUnary encNat) (encOption encNat) 1 1 := + ((optionSome (enc₁ := encNat) (enc := encOption encNat)).comp (snd encUnary encNat)).mono + +/-- The primitive bundle of a basis from degree-`d` certificates for its checked operations, +`d ≥ 2`; the literal, test, address, move and label primitives are quadratic. -/ +noncomputable def Basis.nativePrimitivesOfDegree (B : Basis) {d : ℕ} (hd : 2 ≤ d) + (hop : ∀ op : B.Op, ComputableInDegree (B.genericModel.checkedOp op) + (encPair encUnary (encPi encNat)) (encOption encNat) d 1) : + B.genericModel.NativePrimitives B.encoding where + constant c := .ofDegree ((checkedConstant_degree B c).mono hd le_rfl) + operation op := .ofDegree (hop op) + test t := .ofDegree ((evalTest_degree B t).mono hd le_rfl) + address := .ofDegree ((address_degree B).mono (d' := d) (by omega) le_rfl) + validMove := .ofDegree ((const true).mono (d' := d) (e' := 1) (by omega) zero_le_one) + validPC := .ofDegree ((const true).mono (d' := d) (e' := 1) (by omega) zero_le_one) + +/-- `Basis.nativePrimitivesOfDegree` has degree `d`. -/ +theorem Basis.nativePrimitivesOfDegree_hasDegree (B : Basis) {d : ℕ} (hd : 2 ≤ d) + (hop : ∀ op : B.Op, ComputableInDegree (B.genericModel.checkedOp op) + (encPair encUnary (encPi encNat)) (encOption encNat) d 1) : + (B.nativePrimitivesOfDegree hd hop).HasDegree d := + ⟨fun c => NativeCertificate.ofDegree_hasDegree ((checkedConstant_degree B c).mono hd le_rfl), + fun op => NativeCertificate.ofDegree_hasDegree (hop op), + fun t => NativeCertificate.ofDegree_hasDegree ((evalTest_degree B t).mono hd le_rfl), + NativeCertificate.ofDegree_hasDegree ((address_degree B).mono (d' := d) (by omega) le_rfl), + NativeCertificate.ofDegree_hasDegree + ((const true).mono (d' := d) (e' := 1) (by omega) zero_le_one), + NativeCertificate.ofDegree_hasDegree + ((const true).mono (d' := d) (e' := 1) (by omega) zero_le_one)⟩ + +/-- Every checked operation of the additive basis is quadratic. -/ +theorem Basis.additive.checkedOp_degree (op : Basis.additive.Op) : + ComputableInDegree (Basis.additive.genericModel.checkedOp op) + (encPair encUnary (encPi encNat)) (encOption encNat) 2 1 := by + obtain ⟨f, hf⟩ := op + simp only [List.mem_cons, List.not_mem_nil, or_false] at hf + rcases hf with rfl | rfl + · exact checkedAdd_degree + · exact checkedSub_degree + +/-- The quadratic primitive bundle of the additive basis. -/ +noncomputable def Basis.additive.quadraticPrimitives : + Basis.additive.genericModel.NativePrimitives Basis.additive.encoding := + Basis.nativePrimitivesOfDegree Basis.additive le_rfl Basis.additive.checkedOp_degree + +/-- **Every primitive of the additive basis is quadratic.** -/ +theorem Basis.additive.quadraticPrimitives_hasDegree : + Basis.additive.quadraticPrimitives.HasDegree 2 := + Basis.nativePrimitivesOfDegree_hasDegree _ le_rfl Basis.additive.checkedOp_degree + +end Cslib.WordRAM diff --git a/Complexity/Computability/WordRAM/Turing/Overhead.lean b/Complexity/Computability/WordRAM/Turing/Overhead.lean new file mode 100644 index 0000000000..21aef001cb --- /dev/null +++ b/Complexity/Computability/WordRAM/Turing/Overhead.lean @@ -0,0 +1,466 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Turing +public import Complexity.Computability.WordRAM.NativeDegree +public import Complexity.Computability.GenericRAM.Simulation.Degree +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length + +/-! +# Explicit overhead of the word-RAM simulation by Turing machines + +`Program.ComputesInTime.turingComputableInPolyTime_of_width` simulates a word-RAM program by a +multi-tape Turing machine in polynomial time of unnamed degree. Here the degree is explicit. If +every primitive of the basis has degree `d` (`Model.NativePrimitives.HasDegree`), a run of at most +`T` instructions on `n` input words at word size `w` costs +`O((T + 1) · ((n + T + 1)(w + 1)) ^ max 3 d)` machine steps, on top of computing the word size, +the input words and the step budget. Only the constant factor is hidden. For `Basis.additive`, +whose primitives are quadratic (`Basis.additive.quadraticPrimitives`), the exponent is `3`. The +cube comes from scanning the association-list memory of the simulator +(`SparseMemory.scanTime_le_cube`), not from the word-RAM model. + +The simulation is the same as in `Complexity.Computability.WordRAM.Turing`. The new ingredients are +the degree-tracking certificates of `Complexity.Computability.GenericRAM.Simulation.Degree`, a +cubic initialization certificate (`initMemory_degree`, a counted fold), and quadratic certificates +for the conventions of `Complexity.Computability.WordRAM.Invariance` with logarithmic word size: +the bit list of the input as words (`bitsToNats_degree`) and the word size `k (size n + 1)` +(`logWidthBound_degree`). + +## Main results + +* `Cslib.WordRAM.initMemory_degree`: building the initial memory is cubic. +* `Cslib.WordRAM.Program.ComputesInTime.computableInO_of_width`: the simulation at a supplied + width schedule, with time `O(|x| + Tw + Te + Ts + (T + 1) · ((n + T + 1)(w + 1)) ^ max 3 d)`. +* `Cslib.WordRAM.Program.ComputesInTime.computableInO_of_width_additive`: the case of + `Basis.additive`, with exponent `3`. +* `Cslib.WordRAM.bitsToNats_degree`, `Cslib.WordRAM.logWidthBound_degree`: quadratic input + conversion and word size for the bit-list convention. + +## References + +* [S. A. Cook and R. A. Reckhow, *Time bounded random access machines*][CookReckhow1973] +-/ + +@[expose] public section + +namespace Cslib.WordRAM + +open Turing.MultiTapeTM Cslib.GenericRAM ComputableInDegree + +/-! ## Encoded lengths -/ + +section Lengths + +theorem length_encNat_le_self (n : ℕ) : (encNat n).length ≤ n := by + rw [encNat_apply, Nat.size_eq_bits_len] + exact Nat.size_le.mpr n.lt_two_pow_self + +theorem length_encNat_le_of_lt {w v : ℕ} (hv : v < 2 ^ w) : (encNat v).length ≤ w := by + rw [encNat_apply, Nat.size_eq_bits_len] + exact Nat.size_le.mpr hv + +/-- A word list that fits `w`-bit words has encoded length at most `n (2 w + 1)`. -/ +theorem length_encList_le_of_inputFits {w : ℕ} {l : List ℕ} (h : InputFits w l) : + (encList encNat l).length ≤ l.length * (2 * w + 1) := by + rw [length_encList] + have hle : ∀ x ∈ l, 2 * (encNat x).length + 1 ≤ 2 * w + 1 := fun x hx => by + have := length_encNat_le_of_lt (h.2 x hx) + omega + calc (l.map fun x => 2 * (encNat x).length + 1).sum + ≤ (l.map fun _ => 2 * w + 1).sum := List.sum_le_sum hle + _ = l.length * (2 * w + 1) := by simp + +/-- `stateBound` is linear in the number of stored cells and in the word size. -/ +theorem stateBound_le (r L w E : ℕ) : + stateBound r L w E ≤ (2 * (encNat L).length + 4 * r + 14) * ((E + 1) * (w + 1)) := by + unfold stateBound + have h1 : 1 ≤ (E + 1) * (w + 1) := Nat.one_le_iff_ne_zero.mpr (by positivity) + have h2 : w + 1 ≤ (E + 1) * (w + 1) := Nat.le_mul_of_pos_left _ (by omega) + have h3 : E + 1 ≤ (E + 1) * (w + 1) := Nat.le_mul_of_pos_right _ (by omega) + nlinarith + +end Lengths + +/-! ## Initialization with an explicit degree -/ + +section Init + +/-- One step of the counted fold that builds the stored cells of `State.init`. -/ +def initStep (q : ℕ × List (ℕ × ℕ)) (x : ℕ) : ℕ × List (ℕ × ℕ) := + (q.1 + 1, q.2 ++ [(q.1 + 1, x)]) + +theorem foldl_initStep (l : List ℕ) (k : ℕ) (acc : List (ℕ × ℕ)) : + l.foldl initStep (k, acc) = + (k + l.length, acc ++ (l.zipIdx k).map fun e => (e.2 + 1, e.1)) := by + induction l generalizing k acc with + | nil => simp + | cons x l ih => + rw [List.foldl_cons, initStep, ih, List.zipIdx_cons] + simp only [List.length_cons, List.map_cons, List.append_assoc, List.singleton_append, + Prod.mk.injEq, and_true] + omega + +/-- The stored cells of `State.init` as the result of the counted fold. -/ +theorem initEntries_eq_foldl (input : List ℕ) : + initEntries input = (0, (input.foldl initStep (0, [])).1) :: + (input.foldl initStep (0, [])).2 := by + simp [initEntries, foldl_initStep] + +private theorem length_encList_zipIdx_le (l : List ℕ) (k : ℕ) : + (encList (encPair encNat encNat) ((l.zipIdx k).map fun e => (e.2 + 1, e.1))).length ≤ + 2 * (encList encNat l).length + l.length * (4 * (k + l.length) + 3) := by + induction l generalizing k with + | nil => simp + | cons x l ih => + have h1 := length_encNat_le_self (k + 1) + have h2 := ih (k + 1) + simp only [List.zipIdx_cons, List.map_cons, length_encList, List.sum_cons, + List.length_cons, length_encPair] at h2 ⊢ + nlinarith + +private theorem length_encList_take_le (l : List ℕ) (i : ℕ) : + (encList encNat (l.take i)).length ≤ (encList encNat l).length := by + conv_rhs => rw [← List.take_append_drop i l] + rw [encList_append, List.length_append] + omega + +/-- The counted fold is cubic, with quadratic output. -/ +theorem initFold_degree : + ComputableInDegree (fun l : List ℕ => l.foldl initStep (0, [])) (encList encNat) + (encPair encNat (encList (encPair encNat encNat))) 3 2 := by + have hk : ComputableInDegree (fun p : (ℕ × List (ℕ × ℕ)) × ℕ => p.1.1 + 1) + (encPair (encPair encNat (encList (encPair encNat encNat))) encNat) encNat 1 1 := + (natSucc.comp ((fst _ _).comp (fst _ _))).mono + have hacc : ComputableInDegree (fun p : (ℕ × List (ℕ × ℕ)) × ℕ => p.1.2) + (encPair (encPair encNat (encList (encPair encNat encNat))) encNat) + (encList (encPair encNat encNat)) 1 1 := + ((snd _ _).comp (fst _ _)).mono + have hnew : ComputableInDegree (fun p : (ℕ × List (ℕ × ℕ)) × ℕ => p.1.2 ++ [(p.1.1 + 1, p.2)]) + (encPair (encPair encNat (encList (encPair encNat encNat))) encNat) + (encList (encPair encNat encNat)) 1 1 := + ((snoc (encPair encNat encNat)).comp (hacc.prod (hk.prod (snd _ _)))).mono + have hstep : ComputableInDegree (fun p : (ℕ × List (ℕ × ℕ)) × ℕ => initStep p.1 p.2) + (encPair (encPair encNat (encList (encPair encNat encNat))) encNat) + (encPair encNat (encList (encPair encNat encNat))) 1 1 := + (hk.prod hnew).mono + have h := foldl' (encA := encNat) (encL := encList encNat) + (encB := encPair encNat (encList (encPair encNat encNat))) + (list := fun l => l) (init := fun _ => ((0 : ℕ), ([] : List (ℕ × ℕ)))) (step := initStep) + (of_eq fun _ => rfl) (const _) hstep + (B := fun l => 8 * ((encList encNat l).length + 1) ^ 2) ⟨8, fun _ => le_rfl⟩ + (fun l i hi => by + rw [foldl_initStep] + have hlen := length_le_length_encList encNat l + have htake := length_encList_take_le l i + have hti : (l.take i).length ≤ l.length := List.length_take_le' i l + have hz := length_encList_zipIdx_le (l.take i) 0 + have hn := length_encNat_le_self (0 + (l.take i).length) + simp only [List.nil_append, length_encPair] at hz ⊢ + nlinarith) + exact h.mono + +/-- **Building the initial memory is cubic** in the encoded input words, with quadratic output. -/ +theorem initMemory_degree : + ComputableInDegree initMemory (encList encNat) (SparseMemory.encoding encNat encNat) 3 2 := by + have h : ComputableInDegree + (fun l : List ℕ => (0, (l.foldl initStep (0, [])).1) :: (l.foldl initStep (0, [])).2) + (encList encNat) (encList (encPair encNat encNat)) 3 2 := + ((cons (encPair encNat encNat)).comp ((((const 0).prod ((fst _ _).comp initFold_degree))).prod + ((snd _ _).comp initFold_degree))).mono + refine h.of_enc_eq fun l => ?_ + simp only [SparseMemory.encoding_apply, entries_initMemory, initEntries_eq_foldl] + +/-- The certificate of `initMemory`, cubic in the encoded input words. -/ +def initMemoryCertificate : + NativeCertificate initMemory (encList encNat) (SparseMemory.encoding encNat encNat) := + ⟨fun l => ((encList encNat l).length + 1) ^ 3, fun l => ((encList encNat l).length + 1) ^ 3, + initMemory_degree.inO⟩ + +end Init + +/-! ## The simulation with an explicit degree -/ + +section Main + +variable {B : Basis} {r : ℕ} {α : Type} {encIn : α ↪ List Bool} + +/-- **Word-RAM time gives Turing-machine time with an explicit polynomial overhead.** + +Let every primitive of the basis have degree `d` (`Model.NativePrimitives.HasDegree`), and let `p` +compute `f` (`Program.ComputesInTime`). Suppose a machine computes the word size `width a` in unary +in time `O(Tw a)`, the input words `encode (width a) a` in time `O(Te a)` and a step budget +`steps a ≥ time a (width a)` in binary in time `O(Ts a)`; the word size must be admitted and the +input words must fit it. Then `f` is computable with binary output in time +`O(|encIn a| + Tw a + Te a + Ts a + (steps a + 1) · R ^ max 3 d)`, where +`R = (n + steps a + 1) · (width a + 1)` and `n` is the number of input words. The degree is +explicit; only the constant factor is hidden. -/ +theorem Program.ComputesInTime.computableInO_of_width + {N : B.genericModel.NativePrimitives B.encoding} {d : ℕ} (hN : N.HasDegree d) + {p : Program B r} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} + {allowed : α → ℕ → Prop} {f : α → ℕ} + (h : p.ComputesInTime encode time allowed f) {width steps Tw Sw Te Se Ts Ss : α → ℕ} + (hwidth : Turing.MultiTapeTM.ComputableInO width encIn encUnary Tw Sw) + (hallowed : ∀ a, allowed a (width a)) + (hfits : ∀ a, InputFits (width a) (encode (width a) a)) + (hencode : Turing.MultiTapeTM.ComputableInO (fun a => encode (width a) a) encIn + (encList encNat) Te Se) + (hsteps : Turing.MultiTapeTM.ComputableInO steps encIn encNat Ts Ss) + (htime : ∀ a, time a (width a) ≤ steps a) : + Turing.MultiTapeTM.ComputableInO f encIn encNat + (fun a => (encIn a).length + Tw a + Te a + Ts a + (steps a + 1) * + (((encode (width a) a).length + steps a + 1) * (width a + 1)) ^ max 3 d) + (fun a => (encIn a).length + Sw a + Se a + Ss a + + (((encode (width a) a).length + steps a + 1) * (width a + 1)) ^ max 3 d) := by + have hD : 3 ≤ max 3 d := le_max_left _ _ + have hN' := hN.mono (le_max_right 3 d) + have hExec (a : α) : ∃ m ≤ steps a, GenericRAM.Executes (width a) p.toGeneric + (initState B r (encode (width a) a)).denote (f a) m := by + obtain ⟨m, hm, hle⟩ := h a (width a) (hallowed a) (hfits a) + refine ⟨m, hle.trans (htime a), ?_⟩ + rw [denote_initState] + exact executes_toGeneric_iff.mpr hm + -- Every simulated outcome is a word-bounded state with at most `n + 1 + steps` cells. + have hOutLen (a : α) (j : ℕ) (hj : j ≤ steps a) : + (FiniteState.resultEncoding B.encoding (FiniteState.run (width a) p.toGeneric j + (initState B r (encode (width a) a)))).length ≤ + stateBound r (labelBound p.toGeneric) (width a) + ((encode (width a) a).length + 1 + steps a) := by + have hrun := (wordBounded_initState (B := B) (r := r) (hfits a)).length_resultEncoding_run_le + (p := p.toGeneric) (by simp) j + rw [length_entries_initState] at hrun + refine hrun.trans ?_ + simp only [stateBound] + have := Nat.mul_le_mul_right (6 * width a + 3) + (show (encode (width a) a).length + 1 + j ≤ (encode (width a) a).length + 1 + steps a by + omega) + omega + have ht := FiniteState.transport_inO_of_hasDegree B.encoding N hN' hD p.toGeneric + (⟨Ts, Ss, hsteps⟩ : NativeCertificate steps encIn encNat) + (⟨Tw, Sw, hwidth⟩ : NativeCertificate width encIn encUnary) + (FiniteState.initConstCertificate (r := r) B.encoding (NativeCertificate.const 0) + (NativeCertificate.const 0) + (initMemoryCertificate.comp (⟨Te, Se, hencode⟩ : + NativeCertificate (fun a => encode (width a) a) encIn (encList encNat)))) + hExec hOutLen + -- The constants: the state-bound factor, and its `max 3 d`-th power. + set KL := 2 * (encNat (labelBound p.toGeneric)).length + 4 * r + 14 with hKL + set C := (2 * KL + 4) ^ max 3 d with hC + refine ht.mono (r + 2 * KL + C + 40) (fun a => ?_) (fun a => ?_) <;> + · -- Shared estimates, with `R = (n + steps + 1)(w + 1)` and `P = R ^ max 3 d`. + obtain ⟨R, hR⟩ : ∃ R, R = ((encode (width a) a).length + steps a + 1) * (width a + 1) := + ⟨_, rfl⟩ + have hR1 : 1 ≤ R := hR ▸ Nat.one_le_iff_ne_zero.mpr (by positivity) + have hwR : width a + 1 ≤ R := hR ▸ Nat.le_mul_of_pos_left _ (by omega) + have hTR : steps a + 1 ≤ R := hR ▸ (show steps a + 1 ≤ _ + steps a + 1 by omega).trans + (Nat.le_mul_of_pos_right _ (by omega)) + have hRP : R ≤ R ^ max 3 d := Nat.le_self_pow (by omega) R + have hBd : stateBound r (labelBound p.toGeneric) (width a) + ((encode (width a) a).length + 1 + steps a) ≤ KL * (2 * R) := by + refine (stateBound_le _ _ _ _).trans (Nat.mul_le_mul_left _ ?_) + rw [hR] + nlinarith + have hXD : (2 * width a + stateBound r (labelBound p.toGeneric) (width a) + ((encode (width a) a).length + 1 + steps a) + 2) ^ max 3 d ≤ C * R ^ max 3 d := by + rw [hC, ← Nat.mul_pow] + exact Nat.pow_le_pow_left (by nlinarith) _ + have hsq : ((encNat (steps a)).length + 1) ^ 2 ≤ R ^ max 3 d := by + have h1 := length_encNat_le_self (steps a) + calc ((encNat (steps a)).length + 1) ^ 2 ≤ R ^ 2 := Nat.pow_le_pow_left (by omega) 2 + _ ≤ R ^ max 3 d := Nat.pow_le_pow_right hR1 (by omega) + have hinit : ((encList encNat (encode (width a) a)).length + 1) ^ 3 ≤ 27 * R ^ max 3 d := by + have h1 := length_encList_le_of_inputFits (hfits a) + have h2 : (encList encNat (encode (width a) a)).length + 1 ≤ 3 * R := by + have : (encode (width a) a).length * (2 * width a + 1) ≤ 2 * R := by rw [hR]; nlinarith + omega + calc ((encList encNat (encode (width a) a)).length + 1) ^ 3 ≤ (3 * R) ^ 3 := + Nat.pow_le_pow_left h2 3 + _ = 27 * R ^ 3 := by ring + _ ≤ 27 * R ^ max 3 d := Nat.mul_le_mul_left 27 (Nat.pow_le_pow_right hR1 hD) + have hencS : (FiniteState.encoding B.encoding (initState B r (encode (width a) a))).length ≤ + stateBound r (labelBound p.toGeneric) (width a) + ((encode (width a) a).length + 1 + steps a) := by + have := hOutLen a 0 (Nat.zero_le _) + simp only [FiniteState.run_zero, FiniteState.resultEncoding, encOption_some, + encSum_inl, List.length_cons] at this + omega + have hQ := Nat.mul_le_mul_left (steps a + 1) (Nat.add_le_add hXD hsq) + have hPQ : R ^ max 3 d ≤ (steps a + 1) * R ^ max 3 d := Nat.le_mul_of_pos_left _ (by omega) + have hencT := length_encNat_le_self (steps a) + have hKLP : KL * (2 * R) ≤ 2 * (KL * R ^ max 3 d) := by + rw [Nat.mul_left_comm]; exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ hRP) + have hKLQ : KL * R ^ max 3 d ≤ KL * ((steps a + 1) * R ^ max 3 d) := + Nat.mul_le_mul_left _ hPQ + have hCQ : (steps a + 1) * (C * R ^ max 3 d + R ^ max 3 d) = + C * ((steps a + 1) * R ^ max 3 d) + (steps a + 1) * R ^ max 3 d := by ring + obtain ⟨K, hK⟩ : ∃ K, K = r + 2 * KL + C + 40 := ⟨_, rfl⟩ + have hK1 := Nat.mul_le_mul_right (encIn a).length (show r + 3 ≤ K by omega) + have hK2 := Nat.mul_le_mul_right ((steps a + 1) * R ^ max 3 d) + (show 2 * KL + C + 34 ≤ K by omega) + have hK3 := Nat.mul_le_mul_right (R ^ max 3 d) (show 2 * KL + C + 34 ≤ K by omega) + have hKpos : 1 ≤ K := by omega + have hKT (x : ℕ) : x ≤ K * x := Nat.le_mul_of_pos_left x hKpos + have hTw := hKT (Tw a) + have hTe := hKT (Te a) + have hTs := hKT (Ts a) + have hSw := hKT (Sw a) + have hSe := hKT (Se a) + have hSs := hKT (Ss a) + simp only [initState, FiniteState.initConstCertificate, FiniteState.initCertificate_time, + FiniteState.initCertificate_space, FiniteState.constRegsCertificate, + NativeCertificate.const_time, NativeCertificate.const_space, NativeCertificate.comp_time, + NativeCertificate.comp_space, initMemoryCertificate, Finset.sum_const, Finset.card_univ, + Fintype.card_fin, smul_eq_mul, FiniteState.runInputEncoding, FiniteState.inputEncoding, + length_encPair, Basis.encoding, encUnary_apply, List.length_replicate, Function.comp_apply, + ← hR, ← hK] at hencS ⊢ + linarith + +/-- **The additive word RAM with an explicit cubic overhead.** A run of `Basis.additive` within +`steps a` instructions on `n` input words at word size `w` costs +`O(|encIn a| + Tw a + Te a + Ts a + (steps a + 1) · ((n + steps a + 1)(w + 1)) ^ 3)` Turing-machine +steps; see `Program.ComputesInTime.computableInO_of_width`. -/ +theorem Program.ComputesInTime.computableInO_of_width_additive + {p : Program .additive r} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} + {allowed : α → ℕ → Prop} {f : α → ℕ} + (h : p.ComputesInTime encode time allowed f) {width steps Tw Sw Te Se Ts Ss : α → ℕ} + (hwidth : Turing.MultiTapeTM.ComputableInO width encIn encUnary Tw Sw) + (hallowed : ∀ a, allowed a (width a)) + (hfits : ∀ a, InputFits (width a) (encode (width a) a)) + (hencode : Turing.MultiTapeTM.ComputableInO (fun a => encode (width a) a) encIn + (encList encNat) Te Se) + (hsteps : Turing.MultiTapeTM.ComputableInO steps encIn encNat Ts Ss) + (htime : ∀ a, time a (width a) ≤ steps a) : + Turing.MultiTapeTM.ComputableInO f encIn encNat + (fun a => (encIn a).length + Tw a + Te a + Ts a + (steps a + 1) * + (((encode (width a) a).length + steps a + 1) * (width a + 1)) ^ 3) + (fun a => (encIn a).length + Sw a + Se a + Ss a + + (((encode (width a) a).length + steps a + 1) * (width a + 1)) ^ 3) := + h.computableInO_of_width Basis.additive.quadraticPrimitives_hasDegree hwidth hallowed hfits + hencode hsteps htime + +end Main + +/-! ## The bit-list convention with logarithmic word size -/ + +section Bits + +/-- A linear-time, linear-space computation has cost and output degree one. -/ +private theorem degree_of_linear {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} + {f : α → β} + (h : Turing.MultiTapeTM.ComputableInO f ei eo (fun a => (ei a).length) + (fun a => (ei a).length)) : + ComputableInDegree f ei eo 1 1 := + h.computableInDegree ⟨1, fun a => by simp⟩ ⟨1, fun a => by simp⟩ le_rfl + +private theorem foldl_snoc_map {β γ : Type} (g : β → γ) (l : List β) (acc : List γ) : + l.foldl (fun acc b => acc ++ [g b]) acc = acc ++ l.map g := by + induction l generalizing acc with + | nil => simp + | cons b l ih => simp [ih] + +private theorem foldl_succ (l : List Bool) (m : ℕ) : + l.foldl (fun n _ => n + 1) m = m + l.length := by + induction l generalizing m with + | nil => simp + | cons b l ih => simp only [List.foldl_cons, ih, List.length_cons]; omega + +/-- **The bits of a list as words, in quadratic time.** -/ +theorem bitsToNats_degree : + ComputableInDegree (fun l : List Bool => l.map Bool.toNat) encBits (encList encNat) 2 1 := by + have hstep : ComputableInDegree (fun p : List ℕ × Bool => p.1 ++ [p.2.toNat]) + (encPair (encList encNat) encBool) (encList encNat) 1 1 := + ((snoc encNat).comp ((fst _ _).prod ((of_finite Bool.toNat).comp (snd _ _)))).mono + have h := foldl' (encA := encBool) (encL := encBits) (encB := encList encNat) + (list := fun l => l) (init := fun _ => ([] : List ℕ)) + (step := fun acc b => acc ++ [b.toNat]) (of_eq fun _ => rfl) (const _) hstep + (B := fun l => 3 * (encBits l).length) (DegreeBounded.self.smul 3) + (fun l i hi => by + rw [foldl_snoc_map, List.nil_append, length_encList] + have hle : ∀ x ∈ (l.take i).map Bool.toNat, 2 * (encNat x).length + 1 ≤ 3 := by + intro x hx + obtain ⟨b, -, rfl⟩ := List.mem_map.mp hx + have := length_encNat_le_self b.toNat + cases b <;> simp_all + calc (((l.take i).map Bool.toNat).map fun x => 2 * (encNat x).length + 1).sum + ≤ (((l.take i).map Bool.toNat).map fun _ => 3).sum := List.sum_le_sum hle + _ ≤ 3 * (encBits l).length := by + simp only [List.map_const', List.sum_replicate, List.length_map, smul_eq_mul, + encBits_apply] + have := List.length_take_le' i l + omega) + convert h.mono (d' := 2) (e' := 1) using 1 + funext l + rw [foldl_snoc_map, List.nil_append] + +/-- The length of a bit list in binary, in quadratic time. -/ +theorem lengthBinary_degree : + ComputableInDegree (fun l : List Bool => l.length) encBits encNat 2 1 := by + have h := foldl' (encA := encBool) (encL := encBits) (encB := encNat) + (list := fun l => l) (init := fun _ => (0 : ℕ)) (step := fun n _ => n + 1) + (of_eq fun _ => rfl) (const _) ((natSucc.comp (fst encNat encBool)).mono (d' := 1) (e' := 1)) + (B := fun l => (encBits l).length) DegreeBounded.self + (fun l i hi => by + rw [foldl_succ, Nat.zero_add] + have := length_encNat_le_self (l.take i).length + have := List.length_take_le' i l + simp only [encBits_apply] + omega) + convert h.mono (d' := 2) (e' := 1) using 1 + funext l + rw [foldl_succ, Nat.zero_add] + +/-- Multiplying a unary number by a constant is linear. -/ +theorem unaryMulConst_degree (k : ℕ) : + ComputableInDegree (fun m : ℕ => k * m) encUnary encUnary 1 1 := by + induction k with + | zero => + convert (const (encIn := encUnary) (encMid := encUnary) 0).mono (d' := 1) (e' := 1) + using 1 + funext m + simp + | succ k ih => + convert unaryAdd ih (of_eq (f := fun m : ℕ => m) fun _ => rfl) (d := 1) (e := 1) + (by omega) (by omega) using 1 + funext m + rw [Nat.succ_mul] + +/-- **The word size `k (size n + 1)` of an input of length `n`, in unary, in quadratic time.** It +is at least the logarithmic threshold `logWidth k n`. -/ +theorem logWidthBound_degree (k : ℕ) : + ComputableInDegree (fun l : List Bool => k * (Nat.size l.length + 1)) encBits encUnary 2 1 := by + have hsize : ComputableInDegree (fun l : List Bool => (encNat l.length).length) encBits + encUnary 2 1 := + ((degree_of_linear (ComputableInO.lengthUnary.comp_enc encNat)).comp lengthBinary_degree).mono + have h := ((unaryMulConst_degree k).comp (unary_succ.comp hsize)).mono (d' := 2) (e' := 1) + convert h using 1 + funext l + simp [encNat_apply, Nat.size_eq_bits_len] + +/-- The logarithmic threshold is at most the word size `k (size n + 1)`. -/ +theorem logWidth_le_mul_size_succ (k n : ℕ) : logWidth k n ≤ k * (Nat.size n + 1) := by + refine Nat.mul_le_mul_left k (Nat.add_le_add_right ?_ 1) + rcases Nat.eq_zero_or_pos n with rfl | hn + · simp + · exact (Nat.log_lt_of_lt_pow (by omega) (Nat.lt_size_self n)).le + +/-- The bits of an input of length `n` fit words of `k (size n + 1)` bits when `k ≥ 1`. -/ +theorem inputFits_map_toNat {k : ℕ} (hk : 1 ≤ k) (l : List Bool) : + InputFits (k * (Nat.size l.length + 1)) (l.map Bool.toNat) := by + have hw : Nat.size l.length + 1 ≤ k * (Nat.size l.length + 1) := Nat.le_mul_of_pos_left _ hk + refine ⟨?_, fun v hv => ?_⟩ + · rw [fits_iff, List.length_map] + exact (Nat.lt_size_self _).trans_le (Nat.pow_le_pow_right (by omega) (by omega)) + · obtain ⟨b, -, rfl⟩ := List.mem_map.mp hv + rw [fits_iff] + calc b.toNat < 2 ^ 1 := by cases b <;> simp + _ ≤ _ := Nat.pow_le_pow_right (by omega) (by omega) + +end Bits + +end Cslib.WordRAM diff --git a/ComplexityTests/WordRAMTuringOverhead.lean b/ComplexityTests/WordRAMTuringOverhead.lean new file mode 100644 index 0000000000..18e6f6d5ee --- /dev/null +++ b/ComplexityTests/WordRAMTuringOverhead.lean @@ -0,0 +1,99 @@ +/- +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.Complexity.Classes.FunctionTime.WordRAM + +/-! +# Explicit-overhead word-RAM simulation clients + +The additive primitives are quadratic, and the counted initialization fold builds the memory of +`State.init`. A two-instruction additive program returning the input length, on the bits of the +input at logarithmic word size, puts the length function in an explicit `FTIME` class; a +two-branch additive decider puts emptiness in an explicit `DTIME` class. Both go through +`Program.ComputesInTime.computableInO_of_width_additive`, whose hypotheses these clients satisfy. +-/ + +namespace ComplexityTests.WordRAMTuringOverhead + +open Cslib.WordRAM Turing.MultiTapeTM Cslib.Complexity + +/-! ## Primitives and initialization -/ + +/-- The additive primitives are quadratic, so the simulator's exponent is `max 3 2 = 3`. -/ +example : Basis.additive.quadraticPrimitives.HasDegree 2 := + Basis.additive.quadraticPrimitives_hasDegree + +/-- The counted fold builds the stored cells of `State.init`. -/ +example : initEntries [5, 7] = [(0, 2), (1, 5), (2, 7)] := by + rw [initEntries_eq_foldl] + rfl + +/-- The fits test agrees with `v < 2 ^ w`: `5` fits three bits but not two. -/ +example : Fits 3 5 ∧ ¬Fits 2 5 := by decide + +/-! ## A constant clock -/ + +/-- A constant time bound is computable in linear time. -/ +theorem const_mem_FTIME (v : ℕ) : + (fun _ : List Bool => v) ∈ FTIME encBits encNat (fun n => n + 1) := by + obtain ⟨c, hc, -⟩ := (ComputableInDegree.const (encIn := encBits) (encMid := encNat) v).inO + exact ⟨c, c, fun n => c * ((n + 1) + 1), + hc.mono (fun l => by simp [Nat.mul_add]) (fun l => by simp)⟩ + +/-! ## A function: the input length -/ + +/-- Load the length from address `0` and return it. -/ +def lengthProgram : Program .additive 1 := [.op (.load 0 0), .halt 0] + +theorem lengthProgram_executes (w : ℕ) (l : List ℕ) : + Executes w lengthProgram (.init l) l.length 2 := by + refine Executes.head (t := ⟨1, (Data.init l).set 0 l.length⟩) ?_ (Executes.halt ?_) + · simp [Next, Cslib.WordRAM.step, lengthProgram, State.init] + · simp [Cslib.WordRAM.step, lengthProgram] + +theorem lengthProgram_computesInTime : + lengthProgram.ComputesInTime (fun _ (l : List Bool) => l.map Bool.toNat) (fun _ _ => 2) + (fun l w => logWidth 1 l.length ≤ w) List.length := + fun l w _ _ => ⟨2, by simpa only [List.length_map] using + lengthProgram_executes w (l.map Bool.toNat), le_rfl⟩ + +/-- **The length of a bit list is in an explicit function-time class**, through the two-instruction +additive program at logarithmic word size. -/ +example : List.length ∈ FTIME encBits encNat + (fun n => (n + 1) + (n + 2 + 1) ^ 4 * (1 * (Nat.size n + 1) + 1) ^ 3) := + lengthProgram_computesInTime.mem_FTIME (encIn := encBits) (T := fun _ => 2) le_rfl + (const_mem_FTIME 2) + +/-! ## A decision problem: emptiness -/ + +/-- Return `1` exactly when the input is empty, branching on its length. -/ +def emptyProgram : Program .additive 2 := + [.op (.load 0 0), .branch (.eq 0 1) 3, .halt 1, .op (.const 1 1), .halt 1] + +theorem emptyProgram_decidesInTime : + emptyProgram.DecidesInTime (fun _ (l : List Bool) => l.map Bool.toNat) {l | l = []} + (fun _ _ => 4) (fun l w => logWidth 1 l.length ≤ w) := by + intro l w hw _ + have hw1 : 1 ≤ w := le_trans (by simp [logWidth]) hw + rcases l with _ | ⟨x, l⟩ + · refine ⟨1, 4, ?_, le_rfl, le_rfl, by simp⟩ + refine .of_run (fuel := 4) ?_ + have h1 : Fits w 1 := (fits_iff.mpr (Nat.one_lt_two_pow (by omega))) + simp [run, Cslib.WordRAM.step, WordSizeDependentProgram.const, emptyProgram, Op.eval, + State.init, Data.put, h1] + · refine ⟨0, 3, ?_, by norm_num, by norm_num, by simp⟩ + refine .of_run (fuel := 3) ?_ + simp [run, Cslib.WordRAM.step, WordSizeDependentProgram.const, emptyProgram, Op.eval, + State.init] + +/-- **Emptiness of a bit list is in an explicit `DTIME` class**, through the additive decider at +logarithmic word size. -/ +example : {l : List Bool | l = []} ∈ DTIME encBits + (fun n => (n + 1) + (n + 4 + 1) ^ 4 * (1 * (Nat.size n + 1) + 1) ^ 3) := + emptyProgram_decidesInTime.mem_DTIME (encIn := encBits) (T := fun _ => 4) le_rfl + (const_mem_FTIME 4) + +end ComplexityTests.WordRAMTuringOverhead From c96fb9cdfe27643760ecaf947bce1c96ebd61a51 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:43:39 -0400 Subject: [PATCH 2/2] refactor(WordRAM): named components and shared length lemmas in the overhead (#739) Address the review of #2046. - readRaw_hasDegree and writeRaw_hasDegree bind the lookup and update components by name instead of projection chains (#1764); the functions stay definitionally equal. - Overhead reuses Turing.MultiTapeTM.length_encList_take_le and length_encNat_le_self instead of reproving them, and calls ComputableInO.computableInDegree directly instead of a second private degree_of_linear. - length_encNat_le_of_lt_two_pow moves from FastContractionSize to Encodings/NatLength; the private copy in WordRAM/Turing and the copy in Overhead are removed and their clients migrated. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../TensorNetwork/FastContractionSize.lean | 6 +--- .../GenericRAM/Simulation/Degree.lean | 12 +++++--- .../Turing/MultiTape/Encodings/NatLength.lean | 14 +++++++-- Complexity/Computability/WordRAM/Turing.lean | 15 ++++------ .../WordRAM/Turing/Overhead.lean | 30 ++++--------------- 5 files changed, 31 insertions(+), 46 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean index a4800c8085..471646d6cb 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionShape import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength import Mathlib.Data.List.GetD /-! @@ -49,11 +50,6 @@ theorem length_encNat_le {a b : ℕ} (h : a ≤ b) : (encNat a).length ≤ b := rw [encNat_apply, Nat.size_eq_bits_len] exact Nat.size_le.mpr (h.trans_lt Nat.lt_two_pow_self) -/-- A number below `2 ^ p` has at most `p` binary digits. -/ -theorem length_encNat_le_of_lt_two_pow {a p : ℕ} (h : a < 2 ^ p) : (encNat a).length ≤ p := by - rw [encNat_apply, Nat.size_eq_bits_len] - exact Nat.size_le.mpr h - /-- **A list of elements of encoded length at most `B`** has encoded length at most `k (2 B + 1)` for `k` elements. -/ theorem length_encList_le {α : Type*} (enc : α ↪ List Bool) {l : List α} {B : ℕ} diff --git a/Complexity/Computability/GenericRAM/Simulation/Degree.lean b/Complexity/Computability/GenericRAM/Simulation/Degree.lean index 83b01e719e..de54e3758d 100644 --- a/Complexity/Computability/GenericRAM/Simulation/Degree.lean +++ b/Complexity/Computability/GenericRAM/Simulation/Degree.lean @@ -87,8 +87,10 @@ theorem moveCertificate_hasDegree (enc : M.Encoding) (N : M.NativePrimitives enc theorem readRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : (⟨SparseMemory.readTime enc.address enc.value, SparseMemory.readSpace enc.address enc.value, SparseMemory.read_inO enc.address enc.value⟩ : - NativeCertificate (fun q : (M.Address × SparseMemory M.Address M.Value) × M.Value => - SparseMemory.read q.2 q.1.1 q.1.2) _ _).HasDegree D := by + NativeCertificate + (fun (((address, memory), defaultValue) : + (M.Address × SparseMemory M.Address M.Value) × M.Value) => + SparseMemory.read defaultValue address memory) _ _).HasDegree D := by refine hasDegree_of_space_linear _ (DegreeBounded.mono_deg ⟨32, fun q => ?_⟩ hD) ⟨32, fun q => ?_⟩ (by omega) · have hq : (SparseMemory.queryEncoding enc.address enc.value q.1).length ≤ @@ -110,8 +112,10 @@ theorem readRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : theorem writeRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : (⟨SparseMemory.writeTime enc.address enc.value, SparseMemory.writeSpace enc.address enc.value, SparseMemory.insert_inO enc.address enc.value⟩ : - NativeCertificate (fun q : (M.Address × M.Value) × SparseMemory M.Address M.Value => - q.2.insert q.1.1 q.1.2) _ _).HasDegree D := by + NativeCertificate + (fun (((address, value), memory) : + (M.Address × M.Value) × SparseMemory M.Address M.Value) => + memory.insert address value) _ _).HasDegree D := by refine hasDegree_of_space_linear _ (DegreeBounded.mono_deg ⟨33, fun q => ?_⟩ hD) ⟨33, fun q => ?_⟩ (by omega) · have hq : (SparseMemory.queryEncoding enc.address enc.value (q.1.1, q.2)).length ≤ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatLength.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatLength.lean index ef5dccbf5e..e238f7c935 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatLength.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatLength.lean @@ -15,12 +15,15 @@ import Mathlib.Tactic.NormNum /-! # Binary lengths of natural numbers -The binary encoding `encNat` of a number has `Nat.size` digits. Numbers at most `N` have at most -`log₂ N + 1` digits, and numbers at most `(N + 1) ^ d` at most `(d + 1) * (log₂ N + 1)`: counters -bounded by a polynomial in the length of the input are stored in logarithmic space. +The binary encoding `encNat` of a number has `Nat.size` digits, so numbers below `2 ^ p` have at +most `p` digits. Numbers at most `N` have at most `log₂ N + 1` digits, and numbers at most +`(N + 1) ^ d` at most `(d + 1) * (log₂ N + 1)`: counters bounded by a polynomial in the length of +the input are stored in logarithmic space. ## Main results +* `Turing.MultiTapeTM.length_encNat_le_of_lt_two_pow`: numbers below `2 ^ p` have at most `p` + digits. * `Turing.MultiTapeTM.length_encNat_le_log2`: numbers at most `N` have at most `log₂ N + 1` digits. * `Turing.MultiTapeTM.length_encNat_le_log2_add_two`: numbers at most `N + 1` have at most @@ -40,6 +43,11 @@ bounded by a polynomial in the length of the input are stored in logarithmic spa namespace Turing.MultiTapeTM +/-- A number below `2 ^ p` has at most `p` binary digits. -/ +theorem length_encNat_le_of_lt_two_pow {a p : ℕ} (h : a < 2 ^ p) : (encNat a).length ≤ p := by + rw [encNat_apply, Nat.size_eq_bits_len] + exact Nat.size_le.mpr h + /-- The binary length of a number at most `N` is at most `log₂ N + 1`. -/ theorem length_encNat_le_log2 {j N : ℕ} (h : j ≤ N) : (encNat j).length ≤ Nat.log2 N + 1 := by rw [encNat_apply, Nat.size_eq_bits_len, Nat.size_le] diff --git a/Complexity/Computability/WordRAM/Turing.lean b/Complexity/Computability/WordRAM/Turing.lean index 2ee77b033e..6d6915285b 100644 --- a/Complexity/Computability/WordRAM/Turing.lean +++ b/Complexity/Computability/WordRAM/Turing.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.WordRAM.Function public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat /-! @@ -312,10 +313,6 @@ private theorem listMax_le {α : Type*} {f : α → ℕ} {l : List α} {m : ℕ} simp only [listMax, List.map_cons, List.foldr_cons] at ih ⊢ exact max_le (h a (List.mem_cons_self ..)) (ih fun b hb => h b (List.mem_cons_of_mem _ hb)) -private theorem length_encNat_le_of_lt {v : ℕ} (hv : v < 2 ^ w) : (encNat v).length ≤ w := by - rw [encNat_apply, Nat.size_eq_bits_len] - exact Nat.size_le.mpr hv - /-- Encoded outcomes along a clocked run from a word-bounded state are bounded by `stateBound`, with at most one new stored cell per step. -/ theorem length_resultEncoding_run_le {p : GenericRAM.Program B.genericModel r} @@ -328,7 +325,7 @@ theorem length_resultEncoding_run_le {p : GenericRAM.Program B.genericModel r} | some u => cases u with | inr v => - have hv := length_encNat_le_of_lt (hinr v hrun) + have hv := length_encNat_le_of_lt_two_pow (hinr v hrun) simp only [resultEncoding, encOption_some, encSum_inr, List.length_cons, Basis.encoding, stateBound] omega @@ -336,16 +333,16 @@ theorem length_resultEncoding_run_le {p : GenericRAM.Program B.genericModel r} obtain ⟨ht, htpc⟩ := hinl t hrun have hE := length_entries_run_le hrun have hlen := FiniteState.length_encoding_le B.encoding t - (bound := w) fun i => length_encNat_le_of_lt (ht.regs_lt i) + (bound := w) fun i => length_encNat_le_of_lt_two_pow (ht.regs_lt i) have hpcl : (encNat t.pc).length ≤ (encNat (labelBound p)).length := by simp only [encNat_apply, Nat.size_eq_bits_len] exact Nat.size_le_size htpc have hdef : (B.encoding.value t.default).length ≤ w := - length_encNat_le_of_lt ht.default_lt + length_encNat_le_of_lt_two_pow ht.default_lt have hkey : SparseMemory.maxKeyLength B.encoding.address t.memory ≤ w := - listMax_le fun e he => length_encNat_le_of_lt (ht.entries_lt e he).1 + listMax_le fun e he => length_encNat_le_of_lt_two_pow (ht.entries_lt e he).1 have hval : SparseMemory.maxValueLength B.encoding.value t.memory ≤ w := - listMax_le fun e he => length_encNat_le_of_lt (ht.entries_lt e he).2 + listMax_le fun e he => length_encNat_le_of_lt_two_pow (ht.entries_lt e he).2 have hmul : (SparseMemory.entries t.memory).length * (4 * SparseMemory.maxKeyLength B.encoding.address t.memory + 2 * SparseMemory.maxValueLength B.encoding.value t.memory + 3) ≤ diff --git a/Complexity/Computability/WordRAM/Turing/Overhead.lean b/Complexity/Computability/WordRAM/Turing/Overhead.lean index 21aef001cb..11aa3e6c0a 100644 --- a/Complexity/Computability/WordRAM/Turing/Overhead.lean +++ b/Complexity/Computability/WordRAM/Turing/Overhead.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.WordRAM.NativeDegree public import Complexity.Computability.GenericRAM.Simulation.Degree import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength /-! # Explicit overhead of the word-RAM simulation by Turing machines @@ -58,20 +59,12 @@ open Turing.MultiTapeTM Cslib.GenericRAM ComputableInDegree section Lengths -theorem length_encNat_le_self (n : ℕ) : (encNat n).length ≤ n := by - rw [encNat_apply, Nat.size_eq_bits_len] - exact Nat.size_le.mpr n.lt_two_pow_self - -theorem length_encNat_le_of_lt {w v : ℕ} (hv : v < 2 ^ w) : (encNat v).length ≤ w := by - rw [encNat_apply, Nat.size_eq_bits_len] - exact Nat.size_le.mpr hv - /-- A word list that fits `w`-bit words has encoded length at most `n (2 w + 1)`. -/ theorem length_encList_le_of_inputFits {w : ℕ} {l : List ℕ} (h : InputFits w l) : (encList encNat l).length ≤ l.length * (2 * w + 1) := by rw [length_encList] have hle : ∀ x ∈ l, 2 * (encNat x).length + 1 ≤ 2 * w + 1 := fun x hx => by - have := length_encNat_le_of_lt (h.2 x hx) + have := length_encNat_le_of_lt_two_pow (h.2 x hx) omega calc (l.map fun x => 2 * (encNat x).length + 1).sum ≤ (l.map fun _ => 2 * w + 1).sum := List.sum_le_sum hle @@ -125,12 +118,6 @@ private theorem length_encList_zipIdx_le (l : List ℕ) (k : ℕ) : List.length_cons, length_encPair] at h2 ⊢ nlinarith -private theorem length_encList_take_le (l : List ℕ) (i : ℕ) : - (encList encNat (l.take i)).length ≤ (encList encNat l).length := by - conv_rhs => rw [← List.take_append_drop i l] - rw [encList_append, List.length_append] - omega - /-- The counted fold is cubic, with quadratic output. -/ theorem initFold_degree : ComputableInDegree (fun l : List ℕ => l.foldl initStep (0, [])) (encList encNat) @@ -158,7 +145,7 @@ theorem initFold_degree : (fun l i hi => by rw [foldl_initStep] have hlen := length_le_length_encList encNat l - have htake := length_encList_take_le l i + have htake := length_encList_take_le encNat l i have hti : (l.take i).length ≤ l.length := List.length_take_le' i l have hz := length_encList_zipIdx_le (l.take i) 0 have hn := length_encNat_le_self (0 + (l.take i).length) @@ -350,14 +337,6 @@ end Main section Bits -/-- A linear-time, linear-space computation has cost and output degree one. -/ -private theorem degree_of_linear {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} - {f : α → β} - (h : Turing.MultiTapeTM.ComputableInO f ei eo (fun a => (ei a).length) - (fun a => (ei a).length)) : - ComputableInDegree f ei eo 1 1 := - h.computableInDegree ⟨1, fun a => by simp⟩ ⟨1, fun a => by simp⟩ le_rfl - private theorem foldl_snoc_map {β γ : Type} (g : β → γ) (l : List β) (acc : List γ) : l.foldl (fun acc b => acc ++ [g b]) acc = acc ++ l.map g := by induction l generalizing acc with @@ -436,7 +415,8 @@ theorem logWidthBound_degree (k : ℕ) : ComputableInDegree (fun l : List Bool => k * (Nat.size l.length + 1)) encBits encUnary 2 1 := by have hsize : ComputableInDegree (fun l : List Bool => (encNat l.length).length) encBits encUnary 2 1 := - ((degree_of_linear (ComputableInO.lengthUnary.comp_enc encNat)).comp lengthBinary_degree).mono + (((ComputableInO.lengthUnary.comp_enc encNat).computableInDegree (d := 1) (e := 1) + ⟨1, fun _ => by simp⟩ ⟨1, fun _ => by simp⟩ le_rfl).comp lengthBinary_degree).mono have h := ((unaryMulConst_degree k).comp (unary_succ.comp hsize)).mono (d' := 2) (e' := 1) convert h using 1 funext l