From c921b2afe93421de45b04a87539fa058c6780ad7 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 31 Oct 2026 10:53:39 -0400
Subject: [PATCH 1/2] feat(WordRAM): list-valued outputs and their
 Turing-machine simulation (#739)

A word-RAM program returns a list through memory: `halt` returns an address
holding a length-prefixed array, read from the pre-halt memory
(`outputList`, `ExecutesList`, `Program.ComputesListInTime`).
`Program.parkHalts` turns each halt into a self-loop recording the output
register, so the clocked finite-state simulator ends in a continuing state
holding the output. A native reader selects the register, reads the length
and iterates cubic single-cell reads. Polynomial word-RAM time with a
polynomially long list output gives `Turing.MultiTapeTM.ComputableInPolyTime`
with output `encList encNat`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
---
 Complexity.lean                               |   2 +
 .../Computability/WordRAM/ListOutput.lean     | 241 +++++++++
 .../WordRAM/Turing/ListOutput.lean            | 505 ++++++++++++++++++
 ComplexityTests/WordRAMListOutput.lean        | 143 +++++
 4 files changed, 891 insertions(+)
 create mode 100644 Complexity/Computability/WordRAM/ListOutput.lean
 create mode 100644 Complexity/Computability/WordRAM/Turing/ListOutput.lean
 create mode 100644 ComplexityTests/WordRAMListOutput.lean

diff --git a/Complexity.lean b/Complexity.lean
index 6d336ab1d..88807c2df 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2299,6 +2299,7 @@ public import Complexity.Computability.WordRAM.Heap
 public import Complexity.Computability.WordRAM.InputArray
 public import Complexity.Computability.WordRAM.Invariance
 public import Complexity.Computability.WordRAM.ListArray
+public import Complexity.Computability.WordRAM.ListOutput
 public import Complexity.Computability.WordRAM.MapOp
 public import Complexity.Computability.WordRAM.MemoryWindow
 public import Complexity.Computability.WordRAM.Multiword
@@ -2347,6 +2348,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.ListOutput
 public import Complexity.Computability.WordRAM.Width
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Crypto.Computational.CollisionResistant
diff --git a/Complexity/Computability/WordRAM/ListOutput.lean b/Complexity/Computability/WordRAM/ListOutput.lean
new file mode 100644
index 000000000..e4587bf49
--- /dev/null
+++ b/Complexity/Computability/WordRAM/ListOutput.lean
@@ -0,0 +1,241 @@
+/-
+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.Function
+public import Complexity.Computability.WordRAM.ListArray
+
+/-!
+# List-valued outputs of word-RAM programs
+
+A word-RAM program returns one word with `halt`. A list is returned through memory: `halt`
+returns an address `v`, and the output is the length-prefixed array
+`[mem (v + 1), …, mem (v + mem v)]` in the memory just before the halting step (`outputList`).
+This mirrors the input convention of `State.init`, with the length at address `0` and the words
+at `1, …, n`. In particular, returning address `0` without writing outputs the input itself
+(`outputList_init`).
+
+`Program.parkHalts` replaces every `halt i` by a jump to a self-loop at label `p.length + i`.
+A halting run of `p` becomes a run of `p.parkHalts` that reaches the *parked* state, which has
+the pre-halt data and a control label recording the output register, and stays there
+(`ExecutesList.runs_parkHalts`). A clocked simulator that only produces continuing states can
+therefore read the output from its final state.
+
+## Main definitions
+
+* `Cslib.WordRAM.outputList`: the length-prefixed array at an address.
+* `Cslib.WordRAM.ExecutesList`: a halting run returns the address of a given list.
+* `Cslib.WordRAM.Program.ComputesListInTime`: a fixed program computes a list-valued function.
+* `Cslib.WordRAM.UniformComputableListInPolyTime`: a fixed program computes it in polynomially
+  many instructions at every fitting width above a logarithmic threshold.
+* `Cslib.WordRAM.Program.parkHalts`: halts replaced by self-loops recording the output register.
+
+## Main results
+
+* `Cslib.WordRAM.outputList_eq_iff`: the convention in terms of `Block.HoldsList`.
+* `Cslib.WordRAM.Exec.executesList`, `Cslib.WordRAM.Code.computesListInTime_program`:
+  structured certificates, charging the final halt.
+* `Cslib.WordRAM.ExecutesList.runs_parkHalts`: a halting run of `n ≤ N` instructions gives an
+  `N`-step run of `p.parkHalts` to the parked pre-halt state.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM
+
+variable {B : Basis} {r : ℕ} {α : Type*}
+
+/-! ## The output convention -/
+
+/-- The length-prefixed array at address `v`: `[mem (v + 1), …, mem (v + mem v)]`. -/
+def outputList (mem : ℕ → ℕ) (v : ℕ) : List ℕ :=
+  (List.range (mem v)).map fun i => mem (v + 1 + i)
+
+@[simp] theorem length_outputList (mem : ℕ → ℕ) (v : ℕ) :
+    (outputList mem v).length = mem v := by
+  simp [outputList]
+
+theorem getElem_outputList (mem : ℕ → ℕ) (v i : ℕ) (hi : i < (outputList mem v).length) :
+    (outputList mem v)[i] = mem (v + 1 + i) := by
+  simp [outputList]
+
+/-- The array at `v` is `l` exactly when `v` holds the length of `l` and the following cells hold
+its entries. -/
+theorem outputList_eq_iff {mem : ℕ → ℕ} {v : ℕ} {l : List ℕ} :
+    outputList mem v = l ↔ mem v = l.length ∧ Block.HoldsList (v + 1) l mem := by
+  constructor
+  · rintro rfl
+    refine ⟨(length_outputList mem v).symm, fun i => ?_⟩
+    change mem (v + 1 + i.val) = (outputList mem v)[i.val]
+    rw [getElem_outputList]
+  · rintro ⟨hlen, hl⟩
+    refine List.ext_getElem (by simp [hlen]) fun i hi _ => ?_
+    rw [getElem_outputList]
+    exact hl.get i (by simpa [hlen] using hi)
+
+/-- Returning address `0` of the initial memory outputs the input. -/
+theorem outputList_init (input : List ℕ) :
+    outputList (Data.init input : Data r).mem 0 = input := by
+  refine outputList_eq_iff.2 ⟨rfl, fun i => ?_⟩
+  change (Data.init input : Data r).mem (0 + 1 + i.val) = input[i.val]
+  rw [Nat.zero_add, Nat.add_comm, Data.init_mem_succ]
+  simp [List.getD_eq_getElem?_getD]
+
+/-- `ExecutesList w p s l n`: running `p` at word size `w` from `s` halts after exactly `n`
+instructions, the final `halt` included, returning an address at which the memory just before
+halting holds `l` as a length-prefixed array. -/
+def ExecutesList (w : ℕ) (p : Program B r) (s : State r) (l : List ℕ) (n : ℕ) : Prop :=
+  ∃ t m v, Runs w p s t m ∧ step w p t = .halt v ∧ outputList t.data.mem v = l ∧ n = m + 1
+
+/-- A list-valued run is in particular a halting run, returning the address of the list. -/
+theorem ExecutesList.executes {w : ℕ} {p : Program B r} {s : State r} {l : List ℕ} {n : ℕ}
+    (h : ExecutesList w p s l n) : ∃ v, Executes w p s v n := by
+  obtain ⟨t, m, v, hr, hh, -, rfl⟩ := h
+  exact ⟨v, t, m, hr, hh, rfl⟩
+
+/-- One program returns the list `f a` at every admitted fitting width within `time a w`
+instructions. The final halt is counted; the mathematical input encoding is a convention. -/
+def Program.ComputesListInTime (p : Program B r) (encode : ℕ → α → List ℕ)
+    (time : α → ℕ → ℕ) (allowed : α → ℕ → Prop) (f : α → List ℕ) : Prop :=
+  ∀ a w, allowed a w → InputFits w (encode w a) →
+    ∃ n, ExecutesList w p (.init (encode w a)) (f a) n ∧ n ≤ time a w
+
+/-- A fixed program computes a list-valued function in polynomially many instructions in
+`size a`, at every fitting width above a positive logarithmic threshold. -/
+def UniformComputableListInPolyTime (B : Basis) (f : α → List ℕ) (encode : ℕ → α → List ℕ)
+    (size : α → ℕ) : Prop :=
+  ∃ T, PolynomiallyBounded T ∧ ∃ k, 0 < k ∧ ∃ r, ∃ p : Program B r,
+    p.ComputesListInTime encode (fun a _ => T (size a)) (fun a w => logWidth k (size a) ≤ w) f
+
+/-- Increase a fixed program's time bound and restrict its admitted widths. -/
+theorem Program.ComputesListInTime.mono {p : Program B r} {encode : ℕ → α → List ℕ}
+    {time time' : α → ℕ → ℕ} {allowed allowed' : α → ℕ → Prop} {f : α → List ℕ}
+    (h : p.ComputesListInTime encode time allowed f) (ht : ∀ a w, time a w ≤ time' a w)
+    (ha : ∀ a w, allowed' a w → allowed a w) :
+    p.ComputesListInTime encode time' allowed' f := by
+  intro a w hw hi
+  obtain ⟨n, he, hn⟩ := h a w (ha a w hw) hi
+  exact ⟨n, he, hn.trans (ht a w)⟩
+
+/-- A structured execution followed by `halt out` returns the array at the address in `out`,
+with one more instruction. -/
+theorem Exec.executesList {w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n)
+    (out : Fin r) :
+    ExecutesList w (c.program out) ⟨0, x⟩ (outputList y.mem (y.regs out)) (n + 1) := by
+  have hr := h.runs (pc := 0) (p := c.program out) (Program.Contains.self _).append_left
+  have hh : step w (c.program out) ⟨0 + c.size, y⟩ = .halt (y.regs out) :=
+    step_halt (by simp [Code.program])
+  exact ⟨_, n, _, hr, hh, rfl, rfl⟩
+
+/-- A structured certificate leaving the address of `f a` in register `out` computes `f`, with
+one more instruction for the final halt. -/
+theorem Code.computesListInTime_program {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ}
+    {allowed : α → ℕ → Prop} {f : α → List ℕ} (c : Code B r) (out : Fin r)
+    (h : ∀ a w, allowed a w → InputFits w (encode w a) →
+      ∃ y, ExecWithin w c (.init (encode w a)) y (time a w) ∧
+        outputList y.mem (y.regs out) = f a) :
+    (c.program out).ComputesListInTime encode (fun a w => time a w + 1) allowed f := by
+  intro a w hw hi
+  obtain ⟨y, ⟨n, hn, he⟩, hy⟩ := h a w hw hi
+  exact ⟨n + 1, hy ▸ he.executesList out, Nat.add_le_add_right hn 1⟩
+
+/-! ## Parking the halts -/
+
+/-- Replace `halt i` by a jump to label `L + i`; every other instruction is unchanged. -/
+def Instr.parkHalt (L : ℕ) : Instr B r → Instr B r
+  | .halt i => .jump (L + i)
+  | i => i
+
+/-- Replace every `halt i` of `p` by a jump to a self-loop at label `p.length + i`. Registers and
+all non-halting steps are unchanged; the parked label records the output register. -/
+def Program.parkHalts (p : Program B r) : Program B r :=
+  p.map (Instr.parkHalt p.length) ++ List.ofFn fun i : Fin r => .jump (p.length + i)
+
+namespace Program
+
+variable {p : Program B r}
+
+theorem length_parkHalts (p : Program B r) : p.parkHalts.length = p.length + r := by
+  simp [parkHalts]
+
+theorem getElem?_parkHalts_of_lt {pc : ℕ} (h : pc < p.length) :
+    p.parkHalts[pc]? = p[pc]?.map (Instr.parkHalt p.length) := by
+  rw [parkHalts, List.getElem?_append_left (by simpa using h), List.getElem?_map]
+
+theorem getElem?_parkHalts_park (i : Fin r) :
+    p.parkHalts[p.length + i]? = some (.jump (p.length + i)) := by
+  rw [parkHalts, List.getElem?_append_right (by simp), List.length_map,
+    Nat.add_sub_cancel_left, List.getElem?_ofFn]
+  simp
+
+/-- Every non-halting step of `p` is a step of `p.parkHalts`. -/
+theorem next_parkHalts {w : ℕ} {s t : State r} (h : Next w p s t) : Next w p.parkHalts s t := by
+  unfold Next step at h ⊢
+  cases hp : p[s.pc]? with
+  | none => simp [hp] at h
+  | some i =>
+    have hlt : s.pc < p.length := (List.getElem?_eq_some_iff.mp hp).1
+    rw [getElem?_parkHalts_of_lt hlt, hp, Option.map_some]
+    rw [hp] at h
+    cases i with
+    | halt => simp only at h; cases h
+    | _ => exact h
+
+/-- Every run of `p` is a run of `p.parkHalts`. -/
+theorem runs_parkHalts {w : ℕ} {s t : State r} {m : ℕ} (h : Runs w p s t m) :
+    Runs w p.parkHalts s t m :=
+  h.map id fun _ _ => next_parkHalts
+
+/-- A halting step of `p` becomes a step of `p.parkHalts` to the parked label of the output
+register. -/
+theorem next_parkHalts_of_halt {w v : ℕ} {s : State r} (h : step w p s = .halt v) :
+    ∃ i : Fin r, s.data.regs i = v ∧ Next w p.parkHalts s ⟨p.length + i, s.data⟩ := by
+  unfold step at h
+  cases hp : p[s.pc]? with
+  | none => simp [hp] at h
+  | some ins =>
+    have hlt : s.pc < p.length := (List.getElem?_eq_some_iff.mp hp).1
+    rw [hp] at h
+    cases ins with
+    | halt i =>
+      refine ⟨i, Outcome.halt.inj h, step_jump ?_⟩
+      rw [getElem?_parkHalts_of_lt hlt, hp, Option.map_some]
+      rfl
+    | op o => simp only at h; split at h <;> cases h
+    | jump => simp only at h; cases h
+    | branch => simp only at h; cases h
+    | rand => simp only at h; cases h
+
+/-- A parked state steps to itself. -/
+theorem next_parkHalts_park {w : ℕ} (i : Fin r) (x : Data r) :
+    Next w p.parkHalts ⟨p.length + i, x⟩ ⟨p.length + i, x⟩ :=
+  step_jump (getElem?_parkHalts_park i)
+
+theorem runs_parkHalts_park {w : ℕ} (i : Fin r) (x : Data r) (j : ℕ) :
+    Runs w p.parkHalts ⟨p.length + i, x⟩ ⟨p.length + i, x⟩ j := by
+  induction j with
+  | zero => exact .refl _
+  | succ j ih => exact ih.tail _ _ _ _ (next_parkHalts_park i x)
+
+end Program
+
+/-- **A list-valued run, parked.** If `p` returns `l` within `n ≤ N` instructions, then
+`p.parkHalts` runs for exactly `N` steps to a parked state: its label is `p.length + i` and its
+data holds `l` at the address in register `i`. -/
+theorem ExecutesList.runs_parkHalts {w : ℕ} {p : Program B r} {s : State r} {l : List ℕ} {n N : ℕ}
+    (h : ExecutesList w p s l n) (hN : n ≤ N) :
+    ∃ (i : Fin r) (x : Data r), Runs w p.parkHalts s ⟨p.length + i, x⟩ N ∧
+      outputList x.mem (x.regs i) = l := by
+  obtain ⟨t, m, v, hr, hh, hl, rfl⟩ := h
+  obtain ⟨i, hv, hn⟩ := Program.next_parkHalts_of_halt hh
+  refine ⟨i, t.data, ?_, hv ▸ hl⟩
+  have h₁ := (Program.runs_parkHalts hr).tail _ _ _ _ hn
+  have h₂ := h₁.trans (Program.runs_parkHalts_park i t.data (N - (m + 1)))
+  rwa [Nat.add_sub_cancel' hN] at h₂
+
+end Cslib.WordRAM
diff --git a/Complexity/Computability/WordRAM/Turing/ListOutput.lean b/Complexity/Computability/WordRAM/Turing/ListOutput.lean
new file mode 100644
index 000000000..ff8499ae4
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Turing/ListOutput.lean
@@ -0,0 +1,505 @@
+/-
+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.ListOutput
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+
+/-!
+# Word-RAM list outputs give Turing-machine polynomial time
+
+A fixed word-RAM program that returns a list (`Program.ComputesListInTime`: `halt` returns the
+address of a length-prefixed array) within polynomially many instructions gives a multi-tape
+Turing machine computing the same list-valued function in polynomial time, with output
+`encList encNat`. This extends `Complexity.Computability.WordRAM.Turing` from word outputs to
+list outputs.
+
+## Construction
+
+The simulating machine runs the parked program `p.parkHalts` for its full step budget with the
+clocked finite-state simulator `FiniteState.run`. Since the parked program never halts, the run
+ends in a continuing state holding the memory just before `p` halted, and its control label
+`p.length + i` records the output register `i` (`ExecutesList.runs_parkHalts`). The machine then
+selects that register by comparing labels (`parkedRegister`), reads the array length `L` at the
+returned address and iterates `L` single-cell reads (`readRound`), each a scan of the sparse
+memory. Everything is charged: the step budget, word size, input words and initial memory as in
+the word-output simulation, then the run, the selection and the `L` reads.
+
+## Conventions and limits
+
+The cost model, input convention and word-size choice are those of
+`Complexity.Computability.WordRAM.Turing`. The output length must be polynomially bounded in the
+encoded input length (`hlen`). This hypothesis is necessary, since a polynomial-time machine
+writes polynomially many output bits, and it does not follow from the instruction bound: the
+returned array may consist of cells that are never written and read as `0`, so its length is
+bounded only by `2 ^ w`.
+
+## Main definitions
+
+* `Cslib.WordRAM.parkedRegister`, `Cslib.WordRAM.parkedOutput`: the output register and the
+  output list of a parked finite state.
+* `Cslib.WordRAM.readRound`: one round of reading consecutive memory cells.
+* `Cslib.WordRAM.parkedOutputCertificate`: the native reader of a parked state.
+
+## Main results
+
+* `Cslib.WordRAM.runCertificateOf_isPolynomial`: a clocked run is polynomial when its step
+  budget and visited states are.
+* `Cslib.WordRAM.Program.ComputesListInTime.turingComputableInPolyTime_of_width`: the simulation at
+  a supplied polynomial-time width schedule.
+* `Cslib.WordRAM.Program.ComputesListInTime.turingComputableInPolyTime`,
+  `Cslib.WordRAM.UniformComputableListInPolyTime.turingComputableInPolyTime`: polynomial word-RAM
+  time with a list output gives `Turing.MultiTapeTM.ComputableInPolyTime` with output
+  `encList encNat`.
+
+## 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 NativeCertificate
+
+/-! ## Polynomiality of a clocked run -/
+
+section Run
+
+open GenericRAM.FiniteState
+
+variable {M : GenericRAM.Model.{0, 0, 0, 0}} {r : ℕ} {α : Type} {ei : α ↪ List Bool}
+
+/-- The clocked run of `p` for `steps a` steps from `initState a` at `cfg a`, as a native
+certificate on the original input. -/
+noncomputable def runCertificateOf (enc : M.Encoding) (N : M.NativePrimitives enc)
+    (p : GenericRAM.Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r}
+    {steps : α → ℕ} (cSteps : NativeCertificate steps ei encNat)
+    (cCfg : NativeCertificate cfg ei enc.config)
+    (cInit : NativeCertificate initState ei (FiniteState.encoding enc)) :
+    NativeCertificate (fun a => FiniteState.run (cfg a) p (steps a) (initState a)) ei
+      (FiniteState.resultEncoding enc) :=
+  (FiniteState.runCertificate enc N p).comp (prod cSteps (prod cCfg cInit))
+
+/-- A clocked run is polynomial when the scalar primitives, the step budget, the configuration
+and the initial state are, the budget is polynomially bounded, and so are the encoded outcomes
+along the run. This is the run part of `FiniteState.transportCertificate_isPolynomial`, without
+a halting hypothesis. -/
+theorem runCertificateOf_isPolynomial (enc : M.Encoding) (N : M.NativePrimitives enc)
+    (p : GenericRAM.Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r}
+    {steps : α → ℕ} (cSteps : NativeCertificate steps ei encNat)
+    (cCfg : NativeCertificate cfg ei enc.config)
+    (cInit : NativeCertificate initState ei (FiniteState.encoding enc))
+    (hN : N.IsPolynomial) (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial)
+    (hInit : cInit.IsPolynomial) (hStepsBound : PolyBounded (fun a => (ei a).length) steps)
+    {bound : α → ℕ} (hB : PolyBounded (fun a => (ei a).length) bound)
+    (hOutLen : ∀ a, ∀ j ≤ steps a,
+      (FiniteState.resultEncoding enc
+        (FiniteState.run (cfg a) p j (initState a))).length ≤ bound a) :
+    (runCertificateOf enc N p cSteps cCfg cInit).IsPolynomial := by
+  have hIter : (iterate cSteps (prod cCfg (some (inl cInit enc.value)))
+      (roundCertificate enc N p)).IsPolynomial :=
+    iterate_isPolynomial cSteps _ (roundCertificate enc N p)
+      hSteps (prod_isPolynomial _ _ hCfg (some_isPolynomial _ (inl_isPolynomial _ _ hInit)))
+      (roundCertificate_isPolynomial enc N p hN) hStepsBound
+      ((((PolyBounded.const 2).mul (cCfg.polyTime hCfg).polyBounded_length).add
+        (.const 1)).add hB)
+      fun a j hj => by
+        rw [iterate_round_inl]
+        have := hOutLen a j hj
+        simp only [loopEncoding, length_encPair]
+        omega
+  have hInLen : PolyBounded (fun a => (ei a).length)
+      (fun a => (runInputEncoding enc (steps a, (cfg a, initState a))).length) :=
+    ((prod cSteps (prod cCfg cInit)).polyTime
+      (prod_isPolynomial _ _ hSteps (prod_isPolynomial _ _ hCfg hInit))).polyBounded_length
+  refine ⟨(hIter.1.add ((PolyBounded.const 3).mul hInLen)).mono fun a => ?_,
+    (hIter.2.add ((PolyBounded.const 3).mul hInLen)).mono fun a => ?_⟩
+  · simp only [runCertificateOf, comp_time, runCertificate, congr_time, snd_time,
+      iterate_time, initLoopCertificate, prod_time, fst_time, some_time, inl_time,
+      linear_time, resultEncoding]
+    omega
+  · simp only [runCertificateOf, comp_space, runCertificate, congr_space, snd_space,
+      iterate_space, initLoopCertificate, prod_space, fst_space, some_space, inl_space,
+      linear_space, resultEncoding]
+    omega
+
+end Run
+
+/-! ## Reading the output of a parked state -/
+
+section Read
+
+open GenericRAM.FiniteState GenericRAM.FiniteState.Native
+
+variable {B : Basis} {r : ℕ}
+
+/-- The register recorded by a parked control label: register `i` at label `L + i`, the first
+match among `l`, or `0` if none matches. -/
+def parkedRegister (L : ℕ) (s : FiniteState B.genericModel r) : List (Fin r) → ℕ
+  | [] => 0
+  | i :: l => if s.pc = L + i then s.regs i else parkedRegister L s l
+
+theorem parkedRegister_eq {L : ℕ} {s : FiniteState B.genericModel r} {i : Fin r}
+    (hpc : s.pc = L + i) : ∀ {l : List (Fin r)}, i ∈ l → parkedRegister L s l = s.regs i
+  | j :: l, h => by
+    unfold parkedRegister
+    split
+    · next hj =>
+      have hji : j = i := Fin.ext (by omega)
+      rw [hji]
+    · next hj =>
+      have hij : i ≠ j := fun e => hj (e ▸ hpc)
+      exact parkedRegister_eq hpc ((List.mem_cons.mp h).resolve_left hij)
+
+theorem parkedRegister_lt {L w : ℕ} {s : FiniteState B.genericModel r}
+    (hs : ∀ i, s.regs i < 2 ^ w) : ∀ l, parkedRegister L s l < 2 ^ w
+  | [] => Nat.two_pow_pos w
+  | i :: l => by
+    unfold parkedRegister
+    split
+    · exact hs i
+    · exact parkedRegister_lt hs l
+
+/-- The output list of a parked finite state of a program of length `L`: the array at the address
+in the register recorded by the control label. -/
+def parkedOutput (L : ℕ) (s : FiniteState B.genericModel r) : List ℕ :=
+  outputList (fun a => SparseMemory.read s.default a s.memory)
+    (parkedRegister L s (List.finRange r))
+
+/-- A parked state at label `L + i` outputs the array at the address in register `i`. -/
+theorem parkedOutput_eq {L : ℕ} {s : FiniteState B.genericModel r} {i : Fin r}
+    (hpc : s.pc = L + i) :
+    parkedOutput L s = outputList (fun a => SparseMemory.read s.default a s.memory) (s.regs i) := by
+  rw [parkedOutput, parkedRegister_eq hpc (List.mem_finRange i)]
+
+/-- One round of reading consecutive memory cells, on `((default, memory), (address, read))`. -/
+def readRound (q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ)) :
+    (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) :=
+  (q.1, (q.2.1 + 1, q.2.2 ++ [SparseMemory.read q.1.1 q.2.1 q.1.2]))
+
+theorem iterate_readRound (j : ℕ) (q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ)) :
+    readRound^[j] q =
+      (q.1, (q.2.1 + j, q.2.2 ++ (List.range j).map fun i => SparseMemory.read q.1.1 (q.2.1 + i)
+        q.1.2)) := by
+  induction j with
+  | zero => simp
+  | succ j ih =>
+    rw [Function.iterate_succ_apply', ih]
+    simp [readRound, List.range_succ, Nat.add_assoc]
+
+/-- The encoding of the reading loop state. -/
+abbrev readLoopEncoding : ((ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ)) ↪ List Bool :=
+  encPair (encPair encNat (SparseMemory.encoding encNat encNat)) (encPair encNat (encList encNat))
+
+/-- One reading round is cubic, with linear output: one sparse-memory scan and linear copying. -/
+theorem readRound_degree : ComputableInDegree readRound readLoopEncoding readLoopEncoding 3 1 := by
+  have hread : ComputableInDegree
+      (fun q : (ℕ × SparseMemory ℕ ℕ) × ℕ => SparseMemory.read q.2 q.1.1 q.1.2)
+      (SparseMemory.readEncoding encNat encNat) encNat 3 1 :=
+    (SparseMemory.read_inO_cube encNat encNat).computableInDegree ⟨1, fun q => by simp⟩
+      ⟨1, fun q => by simp⟩ (by norm_num)
+  have harg : ComputableInDegree
+      (fun q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) => ((q.2.1, q.1.2), q.1.1))
+      readLoopEncoding (SparseMemory.readEncoding encNat encNat) 1 1 :=
+    ((((ComputableInDegree.fst _ _).comp (ComputableInDegree.snd _ _)).prod
+      ((ComputableInDegree.snd _ _).comp (ComputableInDegree.fst _ _))).prod
+      ((ComputableInDegree.fst _ _).comp (ComputableInDegree.fst _ _))).mono
+  have hacc : ComputableInDegree (fun q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) => q.2.2)
+      readLoopEncoding (encList encNat) 1 1 :=
+    ((ComputableInDegree.snd _ _).comp (ComputableInDegree.snd _ _)).mono
+  have hsnoc : ComputableInDegree
+      (fun q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) =>
+        q.2.2 ++ [SparseMemory.read q.1.1 q.2.1 q.1.2])
+      readLoopEncoding (encList encNat) 3 1 :=
+    ((ComputableInDegree.snoc encNat).comp (hacc.prod (hread.comp harg))).mono
+  have hsucc : ComputableInDegree (fun q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) => q.2.1 + 1)
+      readLoopEncoding encNat 1 1 :=
+    (ComputableInDegree.natSucc.comp
+      ((ComputableInDegree.fst _ _).comp (ComputableInDegree.snd _ _))).mono
+  exact ((ComputableInDegree.fst _ _).prod (hsucc.prod hsnoc)).mono
+
+/-- The native certificate of one reading round, cubic in the encoded loop state. -/
+def readRoundCertificate : NativeCertificate readRound readLoopEncoding readLoopEncoding :=
+  ⟨fun q => ((readLoopEncoding q).length + 1) ^ 3, fun q => ((readLoopEncoding q).length + 1) ^ 3,
+    readRound_degree.inO⟩
+
+theorem readRoundCertificate_isPolynomial : readRoundCertificate.IsPolynomial :=
+  ⟨.of_forall_le 1 3 (by simp [readRoundCertificate]),
+    .of_forall_le 1 3 (by simp [readRoundCertificate])⟩
+
+variable {α : Type} {encIn : α ↪ List Bool} {s : α → FiniteState B.genericModel r}
+
+/-- Select the register recorded by the control label among `l`, by label comparisons. -/
+noncomputable def parkedRegisterCertificate (L : ℕ)
+    (c : NativeCertificate s encIn (FiniteState.encoding B.encoding)) :
+    (l : List (Fin r)) → NativeCertificate (fun a => parkedRegister L (s a) l) encIn encNat
+  | [] => const 0
+  | i :: l => congr (branch (pcEquals B.encoding c (L + i)) (register B.encoding c i)
+      (parkedRegisterCertificate L c l)) fun a => by
+        simp only [parkedRegister, decide_eq_true_eq]
+
+theorem parkedRegisterCertificate_isPolynomial (L : ℕ)
+    (c : NativeCertificate s encIn (FiniteState.encoding B.encoding)) (hc : c.IsPolynomial) :
+    ∀ l, (parkedRegisterCertificate L c l).IsPolynomial
+  | [] => const_isPolynomial 0
+  | i :: l => congr_isPolynomial _ _ (branch_isPolynomial _ _ _
+      (pcEquals_isPolynomial _ c _ hc) (register_isPolynomial _ c i hc)
+      (parkedRegisterCertificate_isPolynomial L c hc l))
+
+/-- The initial reading loop state `((default, memory), (v + 1, []))` for the output address
+`v`. -/
+noncomputable def readInitCertificate (L : ℕ)
+    (c : NativeCertificate s encIn (FiniteState.encoding B.encoding)) :
+    NativeCertificate (fun a => (((s a).default, (s a).memory),
+      (parkedRegister L (s a) (List.finRange r) + 1, ([] : List ℕ)))) encIn readLoopEncoding :=
+  prod (prod (fst (snd (snd (fields B.encoding c)))) (snd (snd (snd (fields B.encoding c)))))
+    (prod (post (parkedRegisterCertificate L c (List.finRange r))
+      ComputableInDegree.natSucc.inO_one) (const []))
+
+/-- **The reader of a parked state**: select the output register, read the array length `L'` at
+its address, then read `L'` consecutive cells. -/
+noncomputable def parkedOutputCertificate (L : ℕ)
+    (c : NativeCertificate s encIn (FiniteState.encoding B.encoding)) :
+    NativeCertificate (fun a => parkedOutput L (s a)) encIn (encList encNat) :=
+  congr (snd (snd (iterate (readCertificate B.encoding c
+      (parkedRegisterCertificate L c (List.finRange r)))
+    (readInitCertificate L c) readRoundCertificate))) fun a => by
+      rw [iterate_readRound]
+      simp [parkedOutput, outputList]
+
+private 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
+
+/-- The reader is polynomial when its input state is, its states hold `W`-bit words with `W`
+polynomially bounded, and the output length is polynomially bounded. -/
+theorem parkedOutputCertificate_isPolynomial (L : ℕ)
+    (c : NativeCertificate s encIn (FiniteState.encoding B.encoding)) (hc : c.IsPolynomial)
+    {W : α → ℕ} (hW : PolyBounded (fun a => (encIn a).length) W)
+    (hs : ∀ a, WordBounded (W a) (s a))
+    (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (parkedOutput L (s a)).length)) :
+    (parkedOutputCertificate L c).IsPolynomial := by
+  have hv := parkedRegisterCertificate_isPolynomial L c hc (List.finRange r)
+  have hS : PolyBounded (fun a => (encIn a).length)
+      (fun a => (FiniteState.encoding B.encoding (s a)).length) :=
+    (c.polyTime hc).polyBounded_length
+  let bound : α → ℕ := fun a =>
+    6 * (FiniteState.encoding B.encoding (s a)).length + 2 * W a + 4 +
+      (parkedOutput L (s a)).length * (2 * W a + 1)
+  have hB : PolyBounded (fun a => (encIn a).length) bound :=
+    ((((PolyBounded.const 6).mul hS).add ((PolyBounded.const 2).mul hW)).add (.const 4)).add
+      (hlen.mul (((PolyBounded.const 2).mul hW).add (.const 1)))
+  refine congr_isPolynomial _ _ (snd_isPolynomial _ (snd_isPolynomial _
+    (iterate_isPolynomial _ _ _ (readCertificate_isPolynomial _ c _ hc hv)
+      (prod_isPolynomial _ _ (prod_isPolynomial _ _ hc hc)
+        (prod_isPolynomial _ _ hv (const_isPolynomial _)))
+      readRoundCertificate_isPolynomial ?_ hB ?_)))
+  · refine hlen.mono fun a => ?_
+    simp [parkedOutput]
+  · intro a j hj
+    rw [iterate_readRound]
+    have hsa := hs a
+    set v := parkedRegister L (s a) (List.finRange r) with hv_def
+    have hvlt : v < 2 ^ W a := parkedRegister_lt hsa.regs_lt _
+    have hlenEq : (parkedOutput L (s a)).length =
+        SparseMemory.read (s a).default v (s a).memory := by
+      simp [parkedOutput, ← hv_def]
+    have hjlt : j < 2 ^ W a := lt_of_le_of_lt (hj.trans_eq rfl) (hsa.read_lt v)
+    have haddr : (encNat (v + 1 + j)).length ≤ W a + 1 :=
+      length_encNat_le_of_lt' (by rw [Nat.pow_succ]; omega)
+    have hd : (encNat (s a).default).length ≤ W a := length_encNat_le_of_lt' hsa.default_lt
+    have hacc : (encList encNat ((List.range j).map fun i =>
+        SparseMemory.read (s a).default (v + 1 + i) (s a).memory)).length ≤ j * (2 * W a + 1) := by
+      rw [length_encList]
+      calc (((List.range j).map fun i =>
+              SparseMemory.read (s a).default (v + 1 + i) (s a).memory).map
+              fun x => 2 * (encNat x).length + 1).sum
+          ≤ (((List.range j).map fun i =>
+              SparseMemory.read (s a).default (v + 1 + i) (s a).memory).map
+              fun _ => 2 * W a + 1).sum :=
+            List.sum_le_sum fun x hx => by
+              obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx
+              have := length_encNat_le_of_lt' (hsa.read_lt (v + 1 + i))
+              omega
+        _ = j * (2 * W a + 1) := by simp [Function.comp_def]
+    have hmem : 2 * (encNat (s a).default).length +
+        (SparseMemory.encoding encNat encNat (s a).memory).length + 3 ≤
+          (FiniteState.encoding B.encoding (s a)).length := by
+      have := FiniteState.length_encoding B.encoding (s a)
+      change _ = 2 * (encNat (s a).pc).length + 2 * (encPi encNat (s a).regs).length +
+        2 * (encNat (s a).default).length +
+        (SparseMemory.encoding encNat encNat (s a).memory).length + 3 at this
+      omega
+    have hjL : j * (2 * W a + 1) ≤ (parkedOutput L (s a)).length * (2 * W a + 1) :=
+      Nat.mul_le_mul_right _ (by rw [hlenEq]; exact hj)
+    simp only [length_encPair, List.nil_append, bound]
+    omega
+
+end Read
+
+/-! ## Word RAM with list outputs ⇒ Turing machine -/
+
+section Main
+
+open GenericRAM.FiniteState
+
+variable {B : Basis} {r : ℕ} {α : Type} {encIn : α ↪ List Bool}
+
+/-- **Word-RAM time with a list output, at a polynomial-time width schedule, gives
+Turing-machine polynomial time.**
+
+Let `p` be a fixed program over a basis whose checked operations are polynomial-time on a unary
+width and binary operands. Suppose `width a` is computable in unary in polynomial time, is an
+admitted width for `a`, and the word list `encode (width a) a` fits it and is computable in
+polynomial time from `encIn a`. If `p` returns the list `f a` (`Program.ComputesListInTime`)
+within a time bound at `width a` polynomial in `|encIn a|`, and the length of `f a` is
+polynomially bounded in `|encIn a|`, then `f` is computable in polynomial time with output
+`encList encNat`. -/
+theorem Program.ComputesListInTime.turingComputableInPolyTime_of_width
+    (hop : ∀ op : B.Op, Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat))
+    {p : Program B r} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ}
+    {allowed : α → ℕ → Prop} {f : α → List ℕ}
+    (h : p.ComputesListInTime encode time allowed f) {width : α → ℕ}
+    (hwidth : Turing.MultiTapeTM.ComputableInPolyTime width encIn encUnary)
+    (hallowed : ∀ a, allowed a (width a))
+    (hfits : ∀ a, InputFits (width a) (encode (width a) a))
+    (hencode : Turing.MultiTapeTM.ComputableInPolyTime (fun a => encode (width a) a) encIn
+      (encList encNat))
+    (htime : PolyBounded (fun a => (encIn a).length) (fun a => time a (width a)))
+    (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (f a).length)) :
+    Turing.MultiTapeTM.ComputableInPolyTime f encIn (encList encNat) := by
+  -- The step budget: a polynomial of the input length, computed in unary.
+  obtain ⟨steps, hstepsU, hsteps⟩ := exists_unary_majorant htime
+  have hstepsT : Turing.MultiTapeTM.ComputableInPolyTime steps encIn encNat :=
+    Turing.MultiTapeTM.ComputableInPolyTime.unary_to_binary.comp hstepsU
+  -- Initialization: the memory `0 ↦ n, i + 1 ↦ xᵢ`, zero registers and default.
+  have hmem : Turing.MultiTapeTM.ComputableInPolyTime
+      (fun a => initMemory (encode (width a) a)) encIn (SparseMemory.encoding encNat encNat) :=
+    initMemory_polyTime.comp hencode
+  let cInit := FiniteState.initConstCertificate (r := r) B.encoding
+    (NativeCertificate.const (ei := encIn) 0) (NativeCertificate.const 0) (ofPolyTime hmem)
+  have hInit : cInit.IsPolynomial :=
+    FiniteState.initConstCertificate_isPolynomial _ _ _ _ (const_isPolynomial 0)
+      (const_isPolynomial 0) (ofPolyTime_isPolynomial hmem)
+  -- The clocked run of the parked program, and its final state.
+  let q := p.parkHalts.toGeneric
+  let cRun := runCertificateOf B.encoding (B.nativePrimitivesOfPolyTime hop) q
+    (ofPolyTime hstepsT) (ofPolyTime hwidth) cInit
+  let final : α → FiniteState B.genericModel r := fun a =>
+    (continuing (FiniteState.run (width a) q (steps a)
+      (initState B r (encode (width a) a)))).getD (initState B r [])
+  let cFinal : NativeCertificate final encIn (FiniteState.encoding B.encoding) :=
+    post (post cRun (continuingCertificate B.encoding).computes)
+      (ComputableInDegree.getD (enc₁ := FiniteState.encoding B.encoding)
+        (enc := encOption (FiniteState.encoding B.encoding)) (initState B r [])).inO_one
+  -- The run ends in the parked pre-halt state, which holds the output.
+  have hfinal (a : α) :
+      WordBounded (width a) (final a) ∧ f a = parkedOutput p.length (final a) := by
+    obtain ⟨m, hm, hle⟩ := h a (width a) (hallowed a) (hfits a)
+    obtain ⟨i, x, hruns, hout⟩ := hm.runs_parkHalts (hle.trans (hsteps a))
+    have hg := runs_toGeneric_iff.2 hruns
+    rw [← denote_initState] at hg
+    obtain ⟨t, hrun, hden⟩ := exists_run_eq_inl_of_runs hg
+    have hfa : final a = t := by simp only [final, q, hrun]; rfl
+    have hwb := ((wordBounded_initState (B := B) (r := r) (hfits a)).run (p := q) (by simp)
+      (steps a)).1 t hrun
+    refine ⟨hfa ▸ hwb.1, ?_⟩
+    rw [hfa, ← hout]
+    have hpc : t.pc = p.length + i := congrArg GenericRAM.State.pc hden
+    have hregs : t.regs = x.regs := congrArg (fun g => g.data.regs) hden
+    have hmem : (fun a => SparseMemory.read t.default a t.memory) = x.mem :=
+      congrArg (fun g => g.data.mem) hden
+    rw [parkedOutput_eq hpc, hregs, hmem]
+  -- Every simulated outcome is bounded by a polynomial in the input length.
+  let bound : α → ℕ := fun a => stateBound r (labelBound q) (width a)
+    ((encode (width a) a).length + 1 + steps a)
+  have hbound : PolyBounded (fun a => (encIn a).length) bound := by
+    have hw := hwidth.polyBounded
+    have hE : PolyBounded (fun a => (encIn a).length)
+        (fun a => (encode (width a) a).length + 1 + steps a) :=
+      ((hencode.polyBounded_length.mono fun a =>
+        length_le_length_encList encNat (encode (width a) a)).add (.const 1)).add
+          hstepsU.polyBounded
+    exact (((((PolyBounded.const _).add ((PolyBounded.const (2 * r)).mul
+      (((PolyBounded.const 2).mul hw).add (.const 1)))).add ((PolyBounded.const 2).mul hw)).add
+      (hE.mul (((PolyBounded.const 6).mul hw).add (.const 3)))).add hw).add (.const 5)
+  have hOutLen (a : α) (j : ℕ) (hj : j ≤ steps a) :
+      (FiniteState.resultEncoding B.encoding (FiniteState.run (width a) q j
+        (initState B r (encode (width a) a)))).length ≤ bound a := by
+    have hrun := (wordBounded_initState (B := B) (r := r) (hfits a)).length_resultEncoding_run_le
+      (p := q) (by simp) j
+    rw [length_entries_initState] at hrun
+    refine hrun.trans ?_
+    simp only [bound, 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 hRun : cRun.IsPolynomial :=
+    runCertificateOf_isPolynomial _ _ _ _ _ _ (B.nativePrimitivesOfPolyTime_isPolynomial hop)
+      (ofPolyTime_isPolynomial hstepsT) (ofPolyTime_isPolynomial hwidth) hInit
+      hstepsU.polyBounded hbound hOutLen
+  have hFinal : cFinal.IsPolynomial := hRun
+  have hOut := parkedOutputCertificate_isPolynomial p.length cFinal hFinal hwidth.polyBounded
+    (fun a => (hfinal a).1) (hlen.mono fun a => by rw [(hfinal a).2])
+  exact ((parkedOutputCertificate p.length cFinal).congr fun a => ((hfinal a).2).symm).polyTime
+    (congr_isPolynomial _ _ hOut)
+
+/-- **Polynomial word-RAM time with a list output gives Turing-machine polynomial time** for a
+fixed program.
+
+Let `p` be a fixed program over a basis whose checked operations are polynomial-time on a unary
+width and binary operands. Suppose that on every input `a` whose words fit, at every word size of
+at least `logWidth k (size a)`, `p` returns the list `f a` from `State.init (encode a)` within
+`T (size a)` instructions, where `T` is polynomially bounded. If the word list `encode a` is
+computable in polynomial time from the bit string `encIn a`, and `size a` and the length of
+`f a` are polynomially bounded in `|encIn a|`, then `f` is computable in polynomial time with
+output `encList encNat`. -/
+theorem Program.ComputesListInTime.turingComputableInPolyTime
+    (hop : ∀ op : B.Op, Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat))
+    {p : Program B r} {encode : α → List ℕ} {size : α → ℕ} {f : α → List ℕ} {T : ℕ → ℕ}
+    {k : ℕ} (hT : PolynomiallyBounded T) (hsize : PolyBounded (fun a => (encIn a).length) size)
+    (hencode : Turing.MultiTapeTM.ComputableInPolyTime encode encIn (encList encNat))
+    (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (f a).length))
+    (h : p.ComputesListInTime (fun _ => encode) (fun a _ => T (size a))
+      (fun a w => logWidth k (size a) ≤ w) f) :
+    Turing.MultiTapeTM.ComputableInPolyTime f encIn (encList encNat) := by
+  have hlog : PolyBounded (fun a => (encIn a).length) (fun a => logWidth k (size a)) :=
+    ((PolyBounded.const k).mul (hsize.add (.const 1))).mono fun a =>
+      Nat.mul_le_mul_left k (Nat.add_le_add_right (Nat.log_le_self 2 (size a)) 1)
+  obtain ⟨width, hwidth, hge⟩ := exists_unary_majorant
+    (hlog.add (hencode.polyBounded_length (encMid := encList encNat)))
+  exact h.turingComputableInPolyTime_of_width hop hwidth (fun a => by have := hge a; omega)
+    (fun a => inputFits_of_length_encList_le (by have := hge a; omega)) hencode
+    ((PolyBounded.of_polynomiallyBounded id hT).comp hsize) hlen
+
+/-- **Uniform polynomial word-RAM time with a list output gives Turing-machine polynomial time**,
+for a width-independent word encoding computable in polynomial time, a size measure and an output
+length polynomially bounded in the encoded input length. -/
+theorem UniformComputableListInPolyTime.turingComputableInPolyTime
+    (hop : ∀ op : B.Op, Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat))
+    {encode : α → List ℕ} {size : α → ℕ} {f : α → List ℕ}
+    (h : UniformComputableListInPolyTime B f (fun _ => encode) size)
+    (hsize : PolyBounded (fun a => (encIn a).length) size)
+    (hencode : Turing.MultiTapeTM.ComputableInPolyTime encode encIn (encList encNat))
+    (hlen : PolyBounded (fun a => (encIn a).length) (fun a => (f a).length)) :
+    Turing.MultiTapeTM.ComputableInPolyTime f encIn (encList encNat) := by
+  obtain ⟨T, hT, k, -, r, p, hp⟩ := h
+  exact hp.turingComputableInPolyTime hop hT hsize hencode hlen
+
+end Main
+
+end Cslib.WordRAM
diff --git a/ComplexityTests/WordRAMListOutput.lean b/ComplexityTests/WordRAMListOutput.lean
new file mode 100644
index 000000000..f72e0af4e
--- /dev/null
+++ b/ComplexityTests/WordRAMListOutput.lean
@@ -0,0 +1,143 @@
+/-
+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.WordRAM.Turing.ListOutput
+import Complexity.Computability.WordRAM.Copy
+
+/-!
+# Word-RAM list outputs and their Turing-machine simulation
+
+The length-prefixed output convention and halt parking on concrete programs, then two list-valued
+programs transferred to Turing-machine polynomial time. The one-instruction program returning
+address `0` outputs its input array, through the headline theorem. A copying program writes the
+input to a fresh block after it, with its length in front, and returns that block's address,
+through an explicit width schedule.
+-/
+
+namespace ComplexityTests.WordRAMListOutput
+
+open Cslib.WordRAM Turing.MultiTapeTM
+
+/-! ## The convention -/
+
+/-- The array at address `0` of a memory `[3, 7, 9, 0, …]`: three words, the last one never
+written. -/
+example : outputList (fun a => [3, 7, 9].getD a 0) 0 = [7, 9, 0] := by decide
+
+/-- The initial memory holds the input as the array at address `0`. -/
+example : outputList (Data.init [5, 7] : Data 1).mem 0 = [5, 7] := outputList_init _
+
+/-- Parking: each `halt i` jumps to a self-loop at `p.length + i`; the halt of register `1` is
+parked at label `2 + 1`. -/
+example : Program.parkHalts ([.op (.const 0 3), .halt 1] : Program .standard 2) =
+    [.op (.const 0 3), .jump 3, .jump 2, .jump 3] := rfl
+
+/-! ## The identity: return address `0` -/
+
+/-- Return address `0`, where the input array is stored. -/
+def idProgram : Program .standard 1 := [.halt 0]
+
+theorem idProgram_executesList (w : ℕ) (l : List ℕ) : ExecutesList w idProgram (.init l) l 1 :=
+  ⟨_, 0, 0, .refl _, rfl, outputList_init l, rfl⟩
+
+/-- A parked run of the identity reaches the self-loop and keeps the input array. -/
+example (w : ℕ) (l : List ℕ) :
+    ∃ (i : Fin 1) (x : Data 1), Runs w idProgram.parkHalts (.init l) ⟨1 + i, x⟩ 5 ∧
+      outputList x.mem (x.regs i) = l :=
+  (idProgram_executesList w l).runs_parkHalts (by omega)
+
+/-- The identity on framed lists of binary words is polynomial-time, through the headline
+theorem. -/
+example : Turing.MultiTapeTM.ComputableInPolyTime (fun l : List ℕ => l) (encList encNat)
+    (encList encNat) :=
+  UniformComputableListInPolyTime.turingComputableInPolyTime checkedOp_polyTime
+    (size := List.length)
+    ⟨fun _ => 1, .const 1, 1, one_pos, 1, idProgram,
+      fun l w _ _ => ⟨1, idProgram_executesList w l, le_rfl⟩⟩
+    (PolyBounded.self.mono fun l => length_le_length_encList encNat l) (.id' (encIn := _))
+    (PolyBounded.self.mono fun l => length_le_length_encList encNat l)
+
+/-! ## Copying to a fresh block -/
+
+section Copy
+
+open ArrayCopy
+
+/-- Copy the input array `1, …, n` to `n + 2, …, 2n + 1`, store `n` at `n + 1`, and leave the
+address `n + 1` in register `addr`. -/
+def copyCode : Code .standard 7 :=
+  .seq ram[ addr ← #0; len ← *addr; src ← #1; one ← #1; dst ← src + len; dst ← dst + one ]
+    (.seq ArrayCopy.program ram[ addr ← src + len; *addr ← len ])
+
+/-- The copying program returns the address of the copy. -/
+def copyProgram : Program .standard 7 := copyCode.program addr
+
+/-- The copy of the input is the array at the returned address, within `7 n + 12` instructions,
+whenever `2 n + 2` fits a word. -/
+theorem copyCode_exec {w : ℕ} (l : List ℕ) (hw : 2 * l.length + 2 < 2 ^ w) :
+    ∃ y, ExecWithin w copyCode (Data.init l) y (7 * l.length + 12) ∧
+      outputList y.mem (y.regs addr) = l := by
+  let x : Data 7 := Data.init l
+  have h1 : Fits w 1 := fits_iff.mpr (by omega)
+  have hn1 : Fits w (1 + l.length) := fits_iff.mpr (by omega)
+  have hn2 : Fits w (1 + l.length + 1) := fits_iff.mpr (by omega)
+  have hnn : Fits w (1 + l.length + 1 + l.length) := fits_iff.mpr (by omega)
+  let u := (((((x.set addr 0).set len l.length).set src 1).set one 1).set dst
+    (1 + l.length)).set dst (1 + l.length + 1)
+  have hi : ExecWithin w
+      (ram[ addr ← #0; len ← *addr; src ← #1; one ← #1; dst ← src + len; dst ← dst + one ])
+      x u 6 := by
+    ram_eval [u, x, Data.init_mem_zero, h1, hn1, hn2]
+  have hus : u.regs src = 1 := by simp +decide [u]
+  have hud : u.regs dst = 1 + l.length + 1 := by simp +decide [u]
+  have hul : u.regs len = l.length := by simp +decide [u]
+  have hum : u.mem = x.mem := by simp [u]
+  obtain ⟨y, hy, hym, hys, -, hyl⟩ := ArrayCopy.exec u h1 (by rw [hus, hul]; exact hn1)
+    (by rw [hud, hul]; exact hnn) (by rw [hus, hul, hud]; omega)
+  let z := (y.set addr (1 + l.length)).write (1 + l.length) l.length
+  have ht : ExecWithin w ram[ addr ← src + len; *addr ← len ] y z 2 := by
+    ram_eval [z, hys, hyl, hus, hul, hn1]
+  refine ⟨z, (hi.seq (hy.seq ht)).mono (by rw [hul]; omega), ?_⟩
+  have hza : z.regs addr = 1 + l.length := by simp [z]
+  rw [hza, outputList_eq_iff]
+  refine ⟨by simp [z], fun i => ?_⟩
+  have hi' : i.val < l.length := i.isLt
+  change z.mem (1 + l.length + 1 + i.val) = l[i.val]
+  simp only [z, Data.write_mem, Data.set_mem, Function.update_of_ne
+    (show 1 + l.length + 1 + i.val ≠ 1 + l.length by omega), hym, hus, hud, hul]
+  rw [ArrayCopy.copyPrefix_read hi', hum]
+  change (Data.init l : Data 7).mem (1 + i.val) = l[i.val]
+  rw [Nat.add_comm, Data.init_mem_succ]
+  simp [List.getD_eq_getElem?_getD, hi']
+
+/-- The copying program computes the identity on word lists, within `7 n + 13` instructions at
+every width where `2 n + 2` fits. -/
+theorem copyProgram_computesListInTime :
+    copyProgram.ComputesListInTime (fun _ l => l) (fun l _ => 7 * l.length + 13)
+      (fun l w => 2 * l.length + 2 < 2 ^ w) id :=
+  copyCode.computesListInTime_program addr fun l _ hw _ => copyCode_exec l hw
+
+/-- The copying program transfers to a polynomial-time Turing machine at the width schedule
+`|encList encNat l| + 2`, which admits every input. -/
+example : Turing.MultiTapeTM.ComputableInPolyTime (fun l : List ℕ => l) (encList encNat)
+    (encList encNat) :=
+  copyProgram_computesListInTime.turingComputableInPolyTime_of_width checkedOp_polyTime
+    (width := fun l => (encList encNat l).length + 2)
+    (Turing.MultiTapeTM.ComputableInPolyTime.unary_add'
+      (Turing.MultiTapeTM.ComputableInPolyTime.encoding_length _) (.const 2))
+    (fun l => by
+      have h1 := length_le_length_encList encNat l
+      have h2 := Nat.lt_two_pow_self (n := (encList encNat l).length)
+      rw [Nat.pow_add]
+      omega)
+    (fun l => (inputFits_of_length_encList_le le_rfl).mono (by omega)) (.id' (encIn := _))
+    (((PolyBounded.const 7).mul
+      (PolyBounded.self.mono fun l => length_le_length_encList encNat l)).add (.const 13))
+    (PolyBounded.self.mono fun l => length_le_length_encList encNat l)
+
+end Copy
+
+end ComplexityTests.WordRAMListOutput

From 9db5bc6c69c48c57d49d984fec7101bd3baca33f Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 31 Oct 2026 13:00:21 -0400
Subject: [PATCH 2/2] refactor(WordRAM): name readRound's components and reuse
 generic run polynomiality (#739)

- readRound binds ((fill, memory), (address, values)) by name, and
  iterate_readRound is stated on that named tuple (#1764).
- runCertificateOf and runCertificateOf_isPolynomial use only the generic RAM
  model, so they move to GenericRAM/Simulation/Run.lean. The proof of
  transportCertificate_isPolynomial now derives from them.
- The private copy of the encNat length bound is replaced by the public
  Turing.MultiTapeTM.length_encNat_le_of_lt_two_pow from main.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
---
 .../GenericRAM/Simulation/Run.lean            |  63 +++++++---
 .../WordRAM/Turing/ListOutput.lean            | 114 ++++--------------
 2 files changed, 74 insertions(+), 103 deletions(-)

diff --git a/Complexity/Computability/GenericRAM/Simulation/Run.lean b/Complexity/Computability/GenericRAM/Simulation/Run.lean
index de7fb24ba..3df623853 100644
--- a/Complexity/Computability/GenericRAM/Simulation/Run.lean
+++ b/Complexity/Computability/GenericRAM/Simulation/Run.lean
@@ -31,6 +31,8 @@ together with automatic whole-run algorithm transport (`FiniteState.transportCer
   certificates.
 * `FiniteState.runCertificate`, `FiniteState.evalCertificate`, `FiniteState.runTime`,
   `FiniteState.runSpace`: native clocked whole-run certificates and parameterized resource bounds.
+* `FiniteState.runCertificateOf`: the clocked run from computed step budget, configuration and
+  initial state, on the original input.
 * `FiniteState.transportCertificate`: automatic whole-run transport of `GenericRAM.Executes`
   certificates to native multitape Turing machines.
 
@@ -45,6 +47,8 @@ together with automatic whole-run algorithm transport (`FiniteState.transportCer
 * `FiniteState.step_polyTime`, `FiniteState.transport_inO`, `FiniteState.transport_polyTime`,
   `FiniteState.transport_polyTime_of_le_const`: parameterized and polynomial-time whole-run
   transport theorems.
+* `FiniteState.runCertificateOf_isPolynomial`: a clocked run, halting or not, is polynomial when
+  its step budget and the encoded outcomes along it are polynomially bounded.
 
 ## References
 
@@ -822,6 +826,16 @@ theorem le_runSpace_of_run_eq_inl (enc : M.Encoding) (N : M.NativePrimitives enc
 
 /-! ### Automatic whole-run algorithm transport -/
 
+/-- The clocked run of `p` for `steps a` steps from `initState a` at `cfg a`, as a native
+certificate on the original input. The run need not halt. -/
+def runCertificateOf (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r)
+    {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)) :
+    NativeCertificate (fun a => run (cfg a) p (steps a) (initState a)) ei (resultEncoding enc) :=
+  (runCertificate enc N p).comp (prod cSteps (prod cCfg cInit))
+
 theorem unoption_inO (ev : M.Value ↪ List Bool) :
     ComputableInO (fun o : Option M.Value => (encOption ev o).tail)
       (encOption ev) encBits
@@ -1155,25 +1169,22 @@ theorem initConstCertificate_isPolynomial (enc : M.Encoding)
   initCertificate_isPolynomial enc _ default memory
     (constRegsCertificate_isPolynomial enc initReg hreg) hdef hmem
 
-/-- Polynomial-time whole-run transport: if scalar primitives, step-budget certificate,
-configuration certificate, and initial-state certificate are polynomial, the step budget `steps a`
-is polynomially bounded, and the encoded outcomes along `0 ≤ j ≤ steps a` are bounded by a
-polynomially bounded function `B`, then the transported certificate is polynomial. -/
-theorem transportCertificate_isPolynomial (enc : M.Encoding) (N : M.NativePrimitives enc)
-    (p : Program M r) {f : α → M.Value} {cfg : α → M.Config}
-    {initState : α → FiniteState M r} {steps : α → ℕ}
+/-- **A clocked run is polynomial** when the scalar primitives, the step budget, the configuration
+and the initial state are, the step budget `steps a` is polynomially bounded, and the encoded
+outcomes along `0 ≤ j ≤ steps a` are bounded by a polynomially bounded function `B`. The run need
+not halt. -/
+theorem runCertificateOf_isPolynomial (enc : M.Encoding) (N : M.NativePrimitives enc)
+    (p : Program M r) {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)
     (hN : N.IsPolynomial)
     (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial)
     (hStepsBound : PolyBounded (fun a => (ei a).length) steps)
     {B : α → ℕ} (hB : PolyBounded (fun a => (ei a).length) B)
     (hOutLen : ∀ a, ∀ j ≤ steps a,
       (resultEncoding enc (run (cfg a) p j (initState a))).length ≤ B a) :
-    (transportCertificate enc N p cSteps cCfg cInit hExec).IsPolynomial := by
+    (runCertificateOf enc N p cSteps cCfg cInit).IsPolynomial := by
   have hIter : (iterate cSteps (prod cCfg (some (inl cInit enc.value)))
       (roundCertificate enc N p)).IsPolynomial :=
     iterate_isPolynomial cSteps _ (roundCertificate enc N p)
@@ -1191,15 +1202,39 @@ theorem transportCertificate_isPolynomial (enc : M.Encoding) (N : M.NativePrimit
       (prod_isPolynomial _ _ hSteps (prod_isPolynomial _ _ hCfg hInit))).polyBounded_length
   refine ⟨(hIter.1.add ((PolyBounded.const 3).mul hInLen)).mono fun a => ?_,
     (hIter.2.add ((PolyBounded.const 3).mul hInLen)).mono fun a => ?_⟩
-  · simp only [transportCertificate_time, runTime, runCertificate, congr_time, snd_time,
-      iterate_time, initLoopCertificate, prod_time, fst_time, snd_time, some_time, inl_time,
+  · simp only [runCertificateOf, comp_time, runCertificate, congr_time, snd_time,
+      iterate_time, initLoopCertificate, prod_time, fst_time, some_time, inl_time,
       linear_time, resultEncoding]
     omega
-  · simp only [transportCertificate_space, runSpace, runCertificate, congr_space, snd_space,
-      iterate_space, initLoopCertificate, prod_space, fst_space, snd_space, some_space, inl_space,
+  · simp only [runCertificateOf, comp_space, runCertificate, congr_space, snd_space,
+      iterate_space, initLoopCertificate, prod_space, fst_space, some_space, inl_space,
       linear_space, resultEncoding]
     omega
 
+/-- Polynomial-time whole-run transport: if scalar primitives, step-budget certificate,
+configuration certificate, and initial-state certificate are polynomial, the step budget `steps a`
+is polynomially bounded, and the encoded outcomes along `0 ≤ j ≤ steps a` are bounded by a
+polynomially bounded function `B`, then the transported certificate is polynomial. Its bounds are
+those of the run (`FiniteState.runCertificateOf_isPolynomial`). -/
+theorem transportCertificate_isPolynomial (enc : M.Encoding) (N : M.NativePrimitives enc)
+    (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)
+    (hN : N.IsPolynomial)
+    (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial)
+    (hStepsBound : PolyBounded (fun a => (ei a).length) steps)
+    {B : α → ℕ} (hB : PolyBounded (fun a => (ei a).length) B)
+    (hOutLen : ∀ a, ∀ j ≤ steps a,
+      (resultEncoding enc (run (cfg a) p j (initState a))).length ≤ B a) :
+    (transportCertificate enc N p cSteps cCfg cInit hExec).IsPolynomial :=
+  have h := runCertificateOf_isPolynomial enc N p cSteps cCfg cInit hN hSteps hCfg hInit
+    hStepsBound hB hOutLen
+  ⟨h.1.mono fun _ => le_rfl, h.2.mono fun _ => le_rfl⟩
+
 /-- Automatic `ComputableInPolyTime` transport corollary from `GenericRAM.Executes`. -/
 theorem transport_polyTime (enc : M.Encoding) (N : M.NativePrimitives enc)
     (p : Program M r) {f : α → M.Value} {cfg : α → M.Config}
diff --git a/Complexity/Computability/WordRAM/Turing/ListOutput.lean b/Complexity/Computability/WordRAM/Turing/ListOutput.lean
index ff8499ae4..c94df8f99 100644
--- a/Complexity/Computability/WordRAM/Turing/ListOutput.lean
+++ b/Complexity/Computability/WordRAM/Turing/ListOutput.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.WordRAM.Turing
 public import Complexity.Computability.WordRAM.ListOutput
 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
 
 /-!
@@ -25,13 +26,14 @@ list outputs.
 ## Construction
 
 The simulating machine runs the parked program `p.parkHalts` for its full step budget with the
-clocked finite-state simulator `FiniteState.run`. Since the parked program never halts, the run
-ends in a continuing state holding the memory just before `p` halted, and its control label
-`p.length + i` records the output register `i` (`ExecutesList.runs_parkHalts`). The machine then
-selects that register by comparing labels (`parkedRegister`), reads the array length `L` at the
-returned address and iterates `L` single-cell reads (`readRound`), each a scan of the sparse
-memory. Everything is charged: the step budget, word size, input words and initial memory as in
-the word-output simulation, then the run, the selection and the `L` reads.
+clocked finite-state simulator `FiniteState.run`, whose native certificate is polynomial by
+`Cslib.GenericRAM.FiniteState.runCertificateOf_isPolynomial`. Since the parked program never
+halts, the run ends in a continuing state holding the memory just before `p` halted, and its
+control label `p.length + i` records the output register `i` (`ExecutesList.runs_parkHalts`). The
+machine then selects that register by comparing labels (`parkedRegister`), reads the array length
+`L` at the returned address and iterates `L` single-cell reads (`readRound`), each a scan of the
+sparse memory. Everything is charged: the step budget, word size, input words and initial memory
+as in the word-output simulation, then the run, the selection and the `L` reads.
 
 ## Conventions and limits
 
@@ -51,8 +53,6 @@ bounded only by `2 ^ w`.
 
 ## Main results
 
-* `Cslib.WordRAM.runCertificateOf_isPolynomial`: a clocked run is polynomial when its step
-  budget and visited states are.
 * `Cslib.WordRAM.Program.ComputesListInTime.turingComputableInPolyTime_of_width`: the simulation at
   a supplied polynomial-time width schedule.
 * `Cslib.WordRAM.Program.ComputesListInTime.turingComputableInPolyTime`,
@@ -71,70 +71,6 @@ namespace Cslib.WordRAM
 
 open Turing.MultiTapeTM Cslib.GenericRAM NativeCertificate
 
-/-! ## Polynomiality of a clocked run -/
-
-section Run
-
-open GenericRAM.FiniteState
-
-variable {M : GenericRAM.Model.{0, 0, 0, 0}} {r : ℕ} {α : Type} {ei : α ↪ List Bool}
-
-/-- The clocked run of `p` for `steps a` steps from `initState a` at `cfg a`, as a native
-certificate on the original input. -/
-noncomputable def runCertificateOf (enc : M.Encoding) (N : M.NativePrimitives enc)
-    (p : GenericRAM.Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r}
-    {steps : α → ℕ} (cSteps : NativeCertificate steps ei encNat)
-    (cCfg : NativeCertificate cfg ei enc.config)
-    (cInit : NativeCertificate initState ei (FiniteState.encoding enc)) :
-    NativeCertificate (fun a => FiniteState.run (cfg a) p (steps a) (initState a)) ei
-      (FiniteState.resultEncoding enc) :=
-  (FiniteState.runCertificate enc N p).comp (prod cSteps (prod cCfg cInit))
-
-/-- A clocked run is polynomial when the scalar primitives, the step budget, the configuration
-and the initial state are, the budget is polynomially bounded, and so are the encoded outcomes
-along the run. This is the run part of `FiniteState.transportCertificate_isPolynomial`, without
-a halting hypothesis. -/
-theorem runCertificateOf_isPolynomial (enc : M.Encoding) (N : M.NativePrimitives enc)
-    (p : GenericRAM.Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r}
-    {steps : α → ℕ} (cSteps : NativeCertificate steps ei encNat)
-    (cCfg : NativeCertificate cfg ei enc.config)
-    (cInit : NativeCertificate initState ei (FiniteState.encoding enc))
-    (hN : N.IsPolynomial) (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial)
-    (hInit : cInit.IsPolynomial) (hStepsBound : PolyBounded (fun a => (ei a).length) steps)
-    {bound : α → ℕ} (hB : PolyBounded (fun a => (ei a).length) bound)
-    (hOutLen : ∀ a, ∀ j ≤ steps a,
-      (FiniteState.resultEncoding enc
-        (FiniteState.run (cfg a) p j (initState a))).length ≤ bound a) :
-    (runCertificateOf enc N p cSteps cCfg cInit).IsPolynomial := by
-  have hIter : (iterate cSteps (prod cCfg (some (inl cInit enc.value)))
-      (roundCertificate enc N p)).IsPolynomial :=
-    iterate_isPolynomial cSteps _ (roundCertificate enc N p)
-      hSteps (prod_isPolynomial _ _ hCfg (some_isPolynomial _ (inl_isPolynomial _ _ hInit)))
-      (roundCertificate_isPolynomial enc N p hN) hStepsBound
-      ((((PolyBounded.const 2).mul (cCfg.polyTime hCfg).polyBounded_length).add
-        (.const 1)).add hB)
-      fun a j hj => by
-        rw [iterate_round_inl]
-        have := hOutLen a j hj
-        simp only [loopEncoding, length_encPair]
-        omega
-  have hInLen : PolyBounded (fun a => (ei a).length)
-      (fun a => (runInputEncoding enc (steps a, (cfg a, initState a))).length) :=
-    ((prod cSteps (prod cCfg cInit)).polyTime
-      (prod_isPolynomial _ _ hSteps (prod_isPolynomial _ _ hCfg hInit))).polyBounded_length
-  refine ⟨(hIter.1.add ((PolyBounded.const 3).mul hInLen)).mono fun a => ?_,
-    (hIter.2.add ((PolyBounded.const 3).mul hInLen)).mono fun a => ?_⟩
-  · simp only [runCertificateOf, comp_time, runCertificate, congr_time, snd_time,
-      iterate_time, initLoopCertificate, prod_time, fst_time, some_time, inl_time,
-      linear_time, resultEncoding]
-    omega
-  · simp only [runCertificateOf, comp_space, runCertificate, congr_space, snd_space,
-      iterate_space, initLoopCertificate, prod_space, fst_space, some_space, inl_space,
-      linear_space, resultEncoding]
-    omega
-
-end Run
-
 /-! ## Reading the output of a parked state -/
 
 section Read
@@ -182,15 +118,19 @@ theorem parkedOutput_eq {L : ℕ} {s : FiniteState B.genericModel r} {i : Fin r}
     parkedOutput L s = outputList (fun a => SparseMemory.read s.default a s.memory) (s.regs i) := by
   rw [parkedOutput, parkedRegister_eq hpc (List.mem_finRange i)]
 
-/-- One round of reading consecutive memory cells, on `((default, memory), (address, read))`. -/
-def readRound (q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ)) :
-    (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) :=
-  (q.1, (q.2.1 + 1, q.2.2 ++ [SparseMemory.read q.1.1 q.2.1 q.1.2]))
-
-theorem iterate_readRound (j : ℕ) (q : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ)) :
-    readRound^[j] q =
-      (q.1, (q.2.1 + j, q.2.2 ++ (List.range j).map fun i => SparseMemory.read q.1.1 (q.2.1 + i)
-        q.1.2)) := by
+/-- One round of reading consecutive memory cells: on `((fill, memory), (address, values))`, where
+`fill` is the value of unwritten cells, append the cell at `address` to `values` and advance
+`address`. -/
+def readRound : (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ) → (ℕ × SparseMemory ℕ ℕ) × (ℕ × List ℕ)
+  | ((fill, memory), (address, values)) =>
+    ((fill, memory), (address + 1, values ++ [SparseMemory.read fill address memory]))
+
+/-- `j` reading rounds append the `j` cells from `address` on. -/
+theorem iterate_readRound (j fill : ℕ) (memory : SparseMemory ℕ ℕ) (address : ℕ)
+    (values : List ℕ) :
+    readRound^[j] ((fill, memory), (address, values)) =
+      ((fill, memory), (address + j,
+        values ++ (List.range j).map fun i => SparseMemory.read fill (address + i) memory)) := by
   induction j with
   | zero => simp
   | succ j ih =>
@@ -277,10 +217,6 @@ noncomputable def parkedOutputCertificate (L : ℕ)
       rw [iterate_readRound]
       simp [parkedOutput, outputList]
 
-private 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
-
 /-- The reader is polynomial when its input state is, its states hold `W`-bit words with `W`
 polynomially bounded, and the output length is polynomially bounded. -/
 theorem parkedOutputCertificate_isPolynomial (L : ℕ)
@@ -316,8 +252,8 @@ theorem parkedOutputCertificate_isPolynomial (L : ℕ)
       simp [parkedOutput, ← hv_def]
     have hjlt : j < 2 ^ W a := lt_of_le_of_lt (hj.trans_eq rfl) (hsa.read_lt v)
     have haddr : (encNat (v + 1 + j)).length ≤ W a + 1 :=
-      length_encNat_le_of_lt' (by rw [Nat.pow_succ]; omega)
-    have hd : (encNat (s a).default).length ≤ W a := length_encNat_le_of_lt' hsa.default_lt
+      length_encNat_le_of_lt_two_pow (by rw [Nat.pow_succ]; omega)
+    have hd : (encNat (s a).default).length ≤ W a := length_encNat_le_of_lt_two_pow hsa.default_lt
     have hacc : (encList encNat ((List.range j).map fun i =>
         SparseMemory.read (s a).default (v + 1 + i) (s a).memory)).length ≤ j * (2 * W a + 1) := by
       rw [length_encList]
@@ -329,7 +265,7 @@ theorem parkedOutputCertificate_isPolynomial (L : ℕ)
               fun _ => 2 * W a + 1).sum :=
             List.sum_le_sum fun x hx => by
               obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx
-              have := length_encNat_le_of_lt' (hsa.read_lt (v + 1 + i))
+              have := length_encNat_le_of_lt_two_pow (hsa.read_lt (v + 1 + i))
               omega
         _ = j * (2 * W a + 1) := by simp [Function.comp_def]
     have hmem : 2 * (encNat (s a).default).length +