Compiling additive word RAMs to logarithmic-cost RAMs

The additive fragment of Cslib.WordRAM uses constants, copying, addition, truncated subtraction, indirect memory, comparisons and control flow. Its compiler uses the existing natural-number Cslib.RAM with logarithmic instruction costs. This is a forward simulation of successful, bounded-word executions; it does not reflect overflow faults or simulate the word-width instruction, multiplication, division, bitwise operations or shifts.

Source registers occupy target registers 1, …, r. Register 0 is zero until the final output is copied to it. Four further registers hold 1, the fixed memory offset, and two scratch values. Source memory address a occupies target register r + 5 + a, so indirect stores cannot alias the source registers or compiler scratch space. Every source instruction occupies eight target instruction slots; jumps skip unused slots.

The source machine is adapted from the lean-trominoes formalization MIT–ULB CompGeom Group. The target is the natural-number RAM adaptation of Cook and Reckhow documented in Cslib.RAM, not literally their original integer/I/O model. Neither this compiler nor its cost bound is a Turing-machine simulation.

Main definitions

• Cslib.WordRAM.Instr.IsAdditive: the supported instruction fragment.
• Cslib.WordRAM.ToRAM.compile, Cslib.WordRAM.ToRAM.compileAdditive: fixed-block compilation, with explicit code placement.
• Cslib.WordRAM.ToRAM.paddedProgram, Cslib.WordRAM.ToRAM.paddedProgramAdditive: complete compiled programs using paddedInput.
• Cslib.WordRAM.ToRAM.Represents: the register and memory layout.

Main results

• Cslib.WordRAM.Fits.bitLength_le: a fitting word has RAM.bitLength at most w + 1.
• Cslib.WordRAM.Program.mapOp_additiveHomStandard_isAdditive: every program translated from Basis.additive belongs to the additive fragment.
• Cslib.WordRAM.ToRAM.executes_compile, Cslib.WordRAM.ToRAM.executes_compileAdditive: a successful bounded-word run is simulated by the actual compiled code with logarithmic cost at most 8 t (bitLength (r + 5) + w + 1).
• Cslib.WordRAM.ToRAM.haltsWithResultInTime_padded, Cslib.WordRAM.ToRAM.haltsWithResultInTime_padded_additive: the complete target program, including its register initialization, uses logarithmic cost at most 8 (bitLength (r + 5) + 1) (t + 1) (w + 1) on the stated padded input convention.

References

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

theorem Cslib.WordRAM.Fits.bitLength_le {w v : ℕ} (h : Fits w v) : RAM.bitLength v ≤ w + 1

A word fitting w bits has logarithmic RAM bit-length at most w + 1.

def Cslib.WordRAM.Instr.IsAdditive {r : ℕ} : Instr Basis.standard r → Prop

The fragment compiled to the logarithmic-cost natural-number RAM.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableIsAdditive {r : ℕ} (i : Instr Basis.standard r) : Decidable i.IsAdditive

def Cslib.WordRAM.Program.IsAdditive {r : ℕ} (p : Program Basis.standard r) : Prop

Every instruction belongs to the additive-memory fragment.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableIsAdditive_1 {r : ℕ} (p : Program Basis.standard r) : Decidable p.IsAdditive

theorem Cslib.WordRAM.Instr.mapOp_additiveHomStandard_isAdditive {r : ℕ} (i : Instr Basis.additive r) : (mapOp Basis.additiveHomStandard i).IsAdditive

Every instruction translated from Basis.additive belongs to the additive fragment.

theorem Cslib.WordRAM.Program.mapOp_additiveHomStandard_isAdditive {r : ℕ} (p : Program Basis.additive r) : (mapOp Basis.additiveHomStandard p).IsAdditive

Every program translated from Basis.additive belongs to the additive fragment.

theorem Cslib.WordRAM.Code.program_mapOp_additiveHomStandard_isAdditive {r : ℕ} (c : Code Basis.additive r) (out : Fin r) : ((mapOp Basis.additiveHomStandard c).program out).IsAdditive

Assembling a structured program over Basis.additive and translating to Basis.standard produces an additive-fragment program.

def Cslib.WordRAM.ToRAM.memoryBase (r : ℕ) : ℕ

The first target register used to represent source memory.

def Cslib.WordRAM.ToRAM.one (r : ℕ) : ℕ

Target register holding the constant one.

def Cslib.WordRAM.ToRAM.offset (r : ℕ) : ℕ

Target register holding the memory offset.

def Cslib.WordRAM.ToRAM.address (r : ℕ) : ℕ

Scratch register holding a translated indirect address.

def Cslib.WordRAM.ToRAM.test (r : ℕ) : ℕ

Scratch register holding a truncated difference for a comparison.

def Cslib.WordRAM.ToRAM.entry (base pc : ℕ) : ℕ

The target instruction corresponding to a source program counter.

def Cslib.WordRAM.ToRAM.compileInstr {r : ℕ} (base length pc : ℕ) (i : Instr Basis.standard r) (k : ℕ) : RAM.Instr

One slot in the eight-instruction block for a source instruction.

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

Compile into blocks of eight instructions. base is the position where the result will be inserted in the target program; jump targets are absolute. The unsupported instructions have no correctness specification. The compiler is independent of word size and input.

@[simp]

theorem Cslib.WordRAM.ToRAM.length_compile {r : ℕ} (base : ℕ) (p : Program Basis.standard r) : List.length (compile base p) = 8 * List.length p

structure Cslib.WordRAM.ToRAM.Represents {r : ℕ} (x : Data r) (σ : URM.Regs) : Prop

The register/memory representation at source instruction boundaries. Scratch registers are deliberately unconstrained: each is overwritten before the compiler reads it.

• zero : σ.read 0 = 0

  Register zero remains zero until the final output copy.

• one : σ.read (ToRAM.one r) = 1

  A permanent positive register implements unconditional jumps.

• offset : σ.read (ToRAM.offset r) = memoryBase r

  The memory base is available for indirect addressing.

• regs (i : Fin r) : σ.read (↑i + 1) = x.regs i

  The finite source register file is disjoint from the other regions.

• mem (a : ℕ) : σ.read (memoryBase r + a) = x.mem a

  The source memory occupies the remaining target registers.

theorem Cslib.WordRAM.ToRAM.Represents.set {r : ℕ} {x : Data r} {σ : URM.Regs} (h : Represents x σ) (i : Fin r) (v : ℕ) : Represents (x.set i v) (σ.write (↑i + 1) v)

theorem Cslib.WordRAM.ToRAM.Represents.write {r : ℕ} {x : Data r} {σ : URM.Regs} (h : Represents x σ) (a v : ℕ) : Represents (x.write a v) (σ.write (memoryBase r + a) v)

theorem Cslib.WordRAM.ToRAM.executes_compile {r : ℕ} {p : Program Basis.standard r} (hp : p.IsAdditive) (pre : RAM.Program) {w v n : ℕ} {s : State r} {σ : URM.Regs} (hσ : Represents s.data σ) (hs : Data.Bounded w s.data) (h : Executes w p s v n) : ∃ (k : ℕ), (RAM.run (pre ++ compile (List.length pre) p) k { pc := entry (List.length pre) s.pc, regs := σ }).isHalted (pre ++ compile (List.length pre) p) ∧ (RAM.run (pre ++ compile (List.length pre) p) k { pc := entry (List.length pre) s.pc, regs := σ }).regs.output = v ∧ RAM.time RAM.logCost (pre ++ compile (List.length pre) p) k { pc := entry (List.length pre) s.pc, regs := σ } ≤ n * (8 * (RAM.bitLength (memoryBase r) + w + 1))

Successful bounded-word execution is simulated by the compiled code, wherever it is placed after pre. The initial target state represents the source state and starts at its compiled instruction; execution of pre is not included in this statement. The final output copy and jump past the end of the target program are included in the cost.

def Cslib.WordRAM.ToRAM.paddedInput (r : ℕ) (input : List ℕ) : List ℕ

The padded target input convention: zero working registers, followed by the source input length and words. Installing this list is uncharged; the compiler's two initialization instructions and all subsequent instructions are charged.

def Cslib.WordRAM.ToRAM.prologue (r : ℕ) : RAM.Program

Initialize the two permanent compiler registers.

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

A complete compiled program using paddedInput.

theorem Cslib.WordRAM.ToRAM.executes_compile_from_paddedInput {r : ℕ} {p : Program Basis.standard r} (hp : p.IsAdditive) (pre : RAM.Program) {input : List ℕ} {w v n : ℕ} (hi : InputFits w input) (h : Executes w p (State.init input) v n) : have q := pre ++ prologue r ++ compile (List.length pre + 2) p; have s := { pc := List.length pre, regs := URM.Regs.ofInputs (paddedInput r input) }; ∃ (k : ℕ), (RAM.run q k s).isHalted q ∧ (RAM.run q k s).regs.output = v ∧ RAM.time RAM.logCost q k s ≤ 8 * (RAM.bitLength (memoryBase r) + 1) * (n + 1) * (w + 1)

Start the compiled simulation after an arbitrary already-executed prefix, from the supplied padded register layout. The prefix itself is not charged by this theorem; the two-instruction prologue, compiled source execution and final output are charged. This is the composition interface for a separately certified input-preparation program.

theorem Cslib.WordRAM.ToRAM.haltsWithResultInTime_padded {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) : RAM.HaltsWithResultInTime RAM.logCost (paddedProgram p) (paddedInput r input) v (8 * (RAM.bitLength (memoryBase r) + 1) * (n + 1) * (w + 1))

The padded-input logarithmic-cost simulation. The compiler and constant depend only on the source program (in fact, the constant depends only on its number of named registers). The input convention explicitly supplies the length and zero workspace; construction of that convention is not a reduction certified by this theorem.

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

Compile a program over Basis.additive directly to RAM.Program.

@[simp]

theorem Cslib.WordRAM.ToRAM.length_compileAdditive {r : ℕ} (base : ℕ) (p : Program Basis.additive r) : List.length (compileAdditive base p) = 8 * List.length p

theorem Cslib.WordRAM.ToRAM.executes_compileAdditive {r : ℕ} {p : Program Basis.additive r} (pre : RAM.Program) {w v n : ℕ} {s : State r} {σ : URM.Regs} (hσ : Represents s.data σ) (hs : Data.Bounded w s.data) (h : Executes w p s v n) : ∃ (k : ℕ), (RAM.run (pre ++ compileAdditive (List.length pre) p) k { pc := entry (List.length pre) s.pc, regs := σ }).isHalted (pre ++ compileAdditive (List.length pre) p) ∧ (RAM.run (pre ++ compileAdditive (List.length pre) p) k { pc := entry (List.length pre) s.pc, regs := σ }).regs.output = v ∧ RAM.time RAM.logCost (pre ++ compileAdditive (List.length pre) p) k { pc := entry (List.length pre) s.pc, regs := σ } ≤ n * (8 * (RAM.bitLength (memoryBase r) + w + 1))

Successful bounded-word execution of a program over Basis.additive is simulated by compileAdditive, without a separate IsAdditive side condition.

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

A complete compiled program over Basis.additive using paddedInput.

theorem Cslib.WordRAM.ToRAM.executes_compile_from_paddedInput_additive {r : ℕ} {p : Program Basis.additive r} (pre : RAM.Program) {input : List ℕ} {w v n : ℕ} (hi : InputFits w input) (h : Executes w p (State.init input) v n) : have q := pre ++ prologue r ++ compileAdditive (List.length pre + 2) p; have s := { pc := List.length pre, regs := URM.Regs.ofInputs (paddedInput r input) }; ∃ (k : ℕ), (RAM.run q k s).isHalted q ∧ (RAM.run q k s).regs.output = v ∧ RAM.time RAM.logCost q k s ≤ 8 * (RAM.bitLength (memoryBase r) + 1) * (n + 1) * (w + 1)

Start the compiled simulation of a Basis.additive program after an arbitrary already-executed prefix, from the supplied padded register layout.

theorem Cslib.WordRAM.ToRAM.haltsWithResultInTime_padded_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) : RAM.HaltsWithResultInTime RAM.logCost (paddedProgramAdditive p) (paddedInput r input) v (8 * (RAM.bitLength (memoryBase r) + 1) * (n + 1) * (w + 1))

The padded-input logarithmic-cost simulation for programs over Basis.additive.