Complete signed-program translation with charged input preparation

The input words are encoded individually, using one unsigned word per source integer. Both machines install their inputs without charging instructions. Their length headers differ: the unsigned machine supplies the natural length, while the source representation needs its signed encoding. A five-instruction prologue converts that header in place. The final native halt returns the encoded signed output and is included in the simulation bound.

Main definitions

• ToWordRAM.prologue, ToWordRAM.compile: input preparation and the complete fixed program.

Main results

• ToWordRAM.runs_compile_input: run-prefix simulation preserving all memory and registers.
• ToWordRAM.executes_compile_input: every successful source execution transfers with two extra bits and at most 32 * t + 5 target instructions.

References

The translation uses the existing signed RAM input convention and unsigned compiler.

def Cslib.GenericRAM.Signed.ToWordRAM.prologue {r : ℕ} : WordRAM.Code WordRAM.Basis.standard (r + 9)

Convert the native unsigned length header to its signed encoding in five instructions.

def Cslib.GenericRAM.Signed.ToWordRAM.compile {r : ℕ} (p : Program model r) : WordRAM.Program WordRAM.Basis.standard (r + 9)

The complete program, with a charged header conversion and fixed-size instruction blocks. Callers supply input.map encode and decode the returned word, including for nonnegative values.

theorem Cslib.GenericRAM.Signed.ToWordRAM.runs_compile_input {r w n : ℕ} {p : Program model r} {input : List ℤ} (hi : InputFits w input) {t : State model r} (hr : Runs w p (initial input) t n) : ∃ (y : WordRAM.Data (r + 9)), ∃ k ≤ 32 * n + 5, WordRAM.Runs (w + 2) (compile p) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) { pc := entry 5 t.pc, data := y } k ∧ Represents w t.data y

Complete run-prefix simulation preserves every source memory cell and register, with charged header preparation and the translated instruction counter. This supports clients whose observable output is a memory block rather than just the returned register.

theorem Cslib.GenericRAM.Signed.ToWordRAM.inputFits_encode {w : ℕ} {input : List ℤ} (hi : InputFits w input) : WordRAM.InputFits (w + 2) (List.map WordRAM.Signed.encode input)

The encoded source input fits the target width, including its native length header.

theorem Cslib.GenericRAM.Signed.ToWordRAM.executes_compile_input {r w n : ℕ} {p : Program model r} {input : List ℤ} (hi : InputFits w input) {v : ℤ} (hr : Executes w p (initial input) v n) : ∃ k ≤ 32 * n + 5, WordRAM.Executes (w + 2) (compile p) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) (WordRAM.Signed.encode v) k

Complete execution, starting from the ordinary unsigned input convention, costs at most 32 * t + 5 instructions at width w + 2 and returns the encoded signed output. Forward correctness transfers successful runs without claiming reflection of source faults.