Word-RAM simulation with charged input preparation

The fixed compiler is preceded by Cslib.RAM.Input.prepare, which moves the input length and words to the compiler's memory region and clears its workspace. Every relocation, clearing, compiler-initialization, simulation and output instruction is charged.

The external input convention still supplies five zero scratch registers followed by the length header and input words. Installing this fixed convention is uncharged, as for the underlying RAM; this is not a certified encoding reduction from an arbitrary bare list. The simulation is forward and restricted to successful bounded-word executions in the additive-memory fragment.

The source word RAM adapts MIT–ULB CompGeom Group. The target is the library's natural-number adaptation of Cook and Reckhow, with logarithmic cost. This does not establish equivalence with the original integer/I/O model or with Turing machines.

Main definitions

• Cslib.WordRAM.ToRAM.preparedProgram, Cslib.WordRAM.ToRAM.preparedProgramAdditive: input preparation followed by the fixed compiler.

Main results

• Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared_of_bitLength_le, Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared_of_bitLength_le_additive: the sum of preparation and simulation costs, keeping the input bit bound separate from the source word width.
• Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared, Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared_additive: logarithmic cost at most C_r (t + input.length + 1) (w + 1), for an explicit constant depending only on r.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines
• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

def Cslib.WordRAM.ToRAM.preparedProgram {r : ℕ} (p : Program Basis.standard r) : RAM.Program

A fixed target program that prepares the length-bearing input and then simulates p. Its external input convention is RAM.Input.encode 5; the installed scratch prefix is independent of the source program, register count, input and word width.

theorem Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared_of_bitLength_le {r : ℕ} {p : Program Basis.standard r} (hp : p.IsAdditive) {input : List ℕ} {w v n b : ℕ} (hi : InputFits w input) (h : Executes w p (State.init input) v n) (hlen : RAM.bitLength input.length ≤ b) (hinput : ∀ x ∈ input, RAM.bitLength x ≤ b) : have R := memoryBase r; RAM.HaltsWithResultInTime RAM.logCost (preparedProgram p) (RAM.Input.encode 5 input) v ((24 + R) * (RAM.bitLength (R + 5) + 2) * (input.length + 1) * b + 8 * (RAM.bitLength R + 1) * (n + 1) * (w + 1))

The charged preparation and simulation bound with a separate input bit-length bound. The fixed external layout is supplied; all subsequent target instructions are charged.

theorem Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared {r : ℕ} {p : Program Basis.standard r} (hp : p.IsAdditive) {input : List ℕ} {w v n : ℕ} (hi : InputFits w input) (h : Executes w p (State.init input) v n) : have R := memoryBase r; RAM.HaltsWithResultInTime RAM.logCost (preparedProgram p) (RAM.Input.encode 5 input) v (((24 + R) * (RAM.bitLength (R + 5) + 2) + 8 * (RAM.bitLength R + 1)) * (n + input.length + 1) * (w + 1))

Every successful fitting source run has logarithmic target cost C_r (t + input.length + 1) (w + 1), including input relocation and workspace clearing. The displayed constant depends only on the fixed source register count. The supplied external input is five zero words followed by its length header and words; installing it is uncharged.

def Cslib.WordRAM.ToRAM.preparedProgramAdditive {r : ℕ} (p : Program Basis.additive r) : RAM.Program

A fixed target program that prepares the length-bearing input and then simulates a source program over Basis.additive.

theorem Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared_of_bitLength_le_additive {r : ℕ} {p : Program Basis.additive r} {input : List ℕ} {w v n b : ℕ} (hi : InputFits w input) (h : Executes w p (State.init input) v n) (hlen : RAM.bitLength input.length ≤ b) (hinput : ∀ x ∈ input, RAM.bitLength x ≤ b) : have R := memoryBase r; RAM.HaltsWithResultInTime RAM.logCost (preparedProgramAdditive p) (RAM.Input.encode 5 input) v ((24 + R) * (RAM.bitLength (R + 5) + 2) * (input.length + 1) * b + 8 * (RAM.bitLength R + 1) * (n + 1) * (w + 1))

Charged preparation and simulation bound for a program over Basis.additive, with a separate input bit-length bound.

theorem Cslib.WordRAM.ToRAM.haltsWithResultInTime_prepared_additive {r : ℕ} {p : Program Basis.additive r} {input : List ℕ} {w v n : ℕ} (hi : InputFits w input) (h : Executes w p (State.init input) v n) : have R := memoryBase r; RAM.HaltsWithResultInTime RAM.logCost (preparedProgramAdditive p) (RAM.Input.encode 5 input) v (((24 + R) * (RAM.bitLength (R + 5) + 2) + 8 * (RAM.bitLength R + 1)) * (n + input.length + 1) * (w + 1))

Charged preparation and simulation bound for a program over Basis.additive.