Compiling signed RAM programs to the unsigned word RAM

Each source instruction occupies sixty-four target instruction slots. The live prefix uses the proved data/test blocks, followed by relocated control flow; the remaining slots are unreachable padding on successful source runs. Target control labels are natural instruction indices and need not fit a word. Source data occupies the register bank and encoded memory.

All instructions of GenericRAM.Signed.model (including all five signed arithmetic operations) are compiled. The compiler transfers successful runs; it does not promise to reproduce source faults.

Main definitions

• ToWordRAM.entry, ToWordRAM.rawBlock, ToWordRAM.block, ToWordRAM.compileFrom: fixed-size instruction blocks with relocated branches and jumps.

Main results

• ToWordRAM.runs_compile: run-prefix simulation preserving registers and memory.
• ToWordRAM.executes_compile: whole-run forward simulation with two extra bits.

References

The fixed-block organization follows the library's WordRAM.ToRAM compiler. The target translation and the signed representation are new; no alternative source machine is defined.

def Cslib.GenericRAM.Signed.ToWordRAM.entry (base pc : ℕ) : ℕ

Native instruction address of source instruction pc, with code placed after base.

def Cslib.GenericRAM.Signed.ToWordRAM.rawBlock {r : ℕ} (base pc : ℕ) : Instr model r → WordRAM.Program WordRAM.Basis.standard (r + 9)

The live prefix of an instruction block, including its terminal control instruction(s).

def Cslib.GenericRAM.Signed.ToWordRAM.block {r : ℕ} (base pc : ℕ) (i : Instr model r) : WordRAM.Program WordRAM.Basis.standard (r + 9)

A full sixty-four-slot block; successful runs never execute the padding.

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

Compile a suffix whose first source instruction has index pc.

theorem Cslib.GenericRAM.Signed.ToWordRAM.length_rawBlock_le {r : ℕ} (base pc : ℕ) (i : Instr model r) : List.length (rawBlock base pc i) ≤ 64

Every live prefix fits in its fixed-size block.

@[simp]

theorem Cslib.GenericRAM.Signed.ToWordRAM.length_block {r : ℕ} (base pc : ℕ) (i : Instr model r) : List.length (block base pc i) = 64

Every source instruction occupies exactly sixty-four target slots.

@[simp]

theorem Cslib.GenericRAM.Signed.ToWordRAM.length_compileFrom {r : ℕ} (base pc : ℕ) (p : Program model r) : List.length (compileFrom base pc p) = 64 * List.length p

Code size is linear in source instruction-list length.

theorem Cslib.GenericRAM.Signed.ToWordRAM.contains_compileFrom {r : ℕ} (pre : WordRAM.Program WordRAM.Basis.standard (r + 9)) {p : Program model r} {pc : ℕ} {i : Instr model r} (hi : p[pc]? = some i) : (pre ++ compileFrom (List.length pre) 0 p).Contains (entry (List.length pre) pc) (rawBlock (List.length pre) pc i)

The compiler places every live instruction prefix at its relocated address.

theorem Cslib.GenericRAM.Signed.ToWordRAM.runs_compile {r w n : ℕ} {p : Program model r} (pre : WordRAM.Program WordRAM.Basis.standard (r + 9)) {s t : State model r} {x : WordRAM.Data (r + 9)} (hx : Represents w s.data x) (hr : Runs w p s t n) : ∃ (y : WordRAM.Data (r + 9)), ∃ k ≤ 32 * n, WordRAM.Runs (w + 2) (pre ++ compileFrom (List.length pre) 0 p) { pc := entry (List.length pre) s.pc, data := x } { pc := entry (List.length pre) t.pc, data := y } k ∧ Represents w t.data y

Every successful source run prefix preserves the represented register file and memory at the translated instruction boundary, within thirty-two target instructions per step. Execution of the supplied prefix pre is not included.

theorem Cslib.GenericRAM.Signed.ToWordRAM.executes_compile {r w n : ℕ} {p : Program model r} (pre : WordRAM.Program WordRAM.Basis.standard (r + 9)) {s : State model r} {x : WordRAM.Data (r + 9)} {v : ℤ} (hx : Represents w s.data x) (hr : Executes w p s v n) : ∃ k ≤ 32 * n, WordRAM.Executes (w + 2) (pre ++ compileFrom (List.length pre) 0 p) { pc := entry (List.length pre) s.pc, data := x } (WordRAM.Signed.encode v) k

Every successful source run of a signed RAM program transfers to the compiled unsigned program at width w + 2 in at most thirty-two target instructions per source instruction, including the final halt. Execution of pre is not charged here; the target starts at the translated source instruction with already represented data.