Preparing length-prefixed RAM inputs

The external convention Cslib.RAM.Input.encode 5 input reserves five zero scratch registers, then stores a length header and the input words. Installing this convention is uncharged, as in the underlying RAM; it is not a certified encoding reduction. The program below charges every instruction used to relocate the header and words to a fixed address R ≥ 5 and clear the prefix. It copies backwards so that overlapping source and destination intervals are safe.

This uses the existing natural-number adaptation of Cook and Reckhow's RAM and its logarithmic cost measure, not their charged finite-alphabet input/output convention.

Main definitions

• Cslib.RAM.Input.encode: zero prefix, length header, and input words.
• Cslib.RAM.Input.prepare: backward relocation followed by prefix clearing.
• Cslib.RAM.Input.prepareSteps: the exact number of executed instructions.

Main results

• Cslib.RAM.Input.run_prepare_append: preparation works before arbitrary appended code.
• Cslib.RAM.Input.time_prepare_append_le: the charged logarithmic cost of preparation.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines

def Cslib.RAM.Input.encode (R : ℕ) (input : List ℕ) : List ℕ

A zero prefix followed by the input length and input words. Installing this external input convention incurs no instruction cost.

def Cslib.RAM.Input.prepare (R : ℕ) : Program

Relocate the length header and input from address 5 to R, then clear registers below R. Registers 0 through 4 hold one, the remaining word count, source and destination pointers, and the current word. The six-instruction loop copies backwards; the final straight-line block clears the prefix, including all scratch registers. The correctness theorem requires 5 ≤ R.

def Cslib.RAM.Input.prepareSteps (R : ℕ) (input : List ℕ) : ℕ

The number of preparation instructions executed on input.

@[simp]

theorem Cslib.RAM.Input.length_prepare (R : ℕ) : List.length (prepare R) = 12 + R

theorem Cslib.RAM.Input.run_prepare_append {R : ℕ} (hR : 5 ≤ R) (tail : Program) (input : List ℕ) : run (prepare R ++ tail) (prepareSteps R input) (State.init (encode 5 input)) = { pc := List.length (prepare R), regs := URM.Regs.ofInputs (encode R input) }

Before arbitrary appended code, preparation reaches its exact entry point with the relocated length header and words and a zero prefix. This includes overlapping ranges and empty input.

theorem Cslib.RAM.Input.time_prepare_append_le {R b : ℕ} (hR : 5 ≤ R) (tail : Program) (input : List ℕ) (hlen : bitLength input.length ≤ b) (hinput : ∀ v ∈ input, bitLength v ≤ b) : time logCost (prepare R ++ tail) (prepareSteps R input) (State.init (encode 5 input)) ≤ (24 + R) * (bitLength (R + 5) + 2) * (input.length + 1) * b

Preparation costs at most a constant depending only on R times the number of input words (including the header) times their bit-length bound. The length bound already implies 1 ≤ b. Every relocation and clearing instruction is charged; external input installation remains free.