Compiling structured word-RAM programs

A structured program (Cslib.WordRAM.Code) assembles into a flat program (Cslib.WordRAM.Code.assemble) whose conditionals and loops become branches and jumps to absolute instruction indices:

• branch c pos neg at pc becomes a branch on c to pos, then neg, then a jump past pos;
• loop c body at pc becomes a branch on c to body, a jump past the loop, body, and a jump back to the branch.

Every structured execution is a run of the assembled program with exactly the same number of instructions (Cslib.WordRAM.Exec.runs). A complete program ends with a halt (Cslib.WordRAM.Code.program), so a structured proof that a program answers a question (Cslib.WordRAM.Code.Answers) gives a flat program that answers it with one more instruction (Cslib.WordRAM.Code.Answers.program), and a uniform decision procedure (Cslib.WordRAM.Code.decidesInTime_program, Cslib.WordRAM.UniformDecidableInTime.of_code).

Main definitions

• Cslib.WordRAM.Code.assemble, Cslib.WordRAM.Code.program: assembly at a given position, and the complete program halting with a given register.
• Cslib.WordRAM.Program.Contains: a program contains another at a given position.
• Cslib.WordRAM.Code.Answers: a structured program answers a question in a register.

Main results

• Cslib.WordRAM.Exec.runs: structured executions are runs of the assembled program with the same instruction count.
• Cslib.WordRAM.Exec.executes: a structured execution followed by halt is a halting run.
• Cslib.WordRAM.Code.decidesInTime_program, Cslib.WordRAM.UniformDecidableInTime.of_code: structured decision procedures are uniform deciders. Width-indexed code with a uniform size bound gives Cslib.WordRAM.DecidableInTime.of_code.
• Cslib.WordRAM.Code.not_readsWidth_program: a compiled program reads the word size only if the structured program does.

References

• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino; the assembly and its exact-cost correctness are adapted from its accompanying Lean formalization.

Assembly

def Cslib.WordRAM.Code.assemble {B : Basis} {r : ℕ} : Code B r → ℕ → Program B r

Assemble a structured program to be placed at instruction index pc.

@[simp]

theorem Cslib.WordRAM.Code.length_assemble {B : Basis} {r : ℕ} (c : Code B r) (pc : ℕ) : List.length (c.assemble pc) = c.size

def Cslib.WordRAM.Code.program {B : Basis} {r : ℕ} (c : Code B r) (out : Fin r) : Program B r

The complete program: the assembled structured program followed by halt out.

def Cslib.WordRAM.Program.Contains {B : Basis} {r : ℕ} (p : Program B r) (base : ℕ) (q : Program B r) : Prop

p contains the program q starting at instruction index base.

theorem Cslib.WordRAM.Program.Contains.self {B : Basis} {r : ℕ} (p : Program B r) : p.Contains 0 p

theorem Cslib.WordRAM.Program.Contains.append_left {B : Basis} {r : ℕ} {p q₁ q₂ : Program B r} {base : ℕ} (h : p.Contains base (q₁ ++ q₂)) : p.Contains base q₁

theorem Cslib.WordRAM.Program.Contains.append_right {B : Basis} {r : ℕ} {p q₁ q₂ : Program B r} {base : ℕ} (h : p.Contains base (q₁ ++ q₂)) : p.Contains (base + List.length q₁) q₂

theorem Cslib.WordRAM.Program.Contains.cons_tail {B : Basis} {r : ℕ} {p q : Program B r} {base : ℕ} {i : Instr B r} (h : p.Contains base (i :: q)) : p.Contains (base + 1) q

theorem Cslib.WordRAM.Program.Contains.getElem? {B : Basis} {r : ℕ} {p q : Program B r} {base : ℕ} (h : p.Contains base q) {k : ℕ} (hk : k < List.length q) : p[base + k]? = q[k]?

theorem Cslib.WordRAM.Program.Contains.head {B : Basis} {r : ℕ} {p q : Program B r} {base : ℕ} {i : Instr B r} (h : p.Contains base (i :: q)) : p[base]? = some i

Correctness of assembly

theorem Cslib.WordRAM.Exec.runs {B : Basis} {r w : ℕ} {p : Program B r} {x : Data r} {pc : ℕ} {c : Code B r} {y : Data r} {n : ℕ} (h : Exec w c x y n) (hp : p.Contains pc (c.assemble pc)) : Runs w p { pc := pc, data := x } { pc := pc + c.size, data := y } n

Assembly is correct. A structured execution is a run of any program containing the assembled structured program, from its first instruction to the instruction after it, with exactly the same number of instructions.

theorem Cslib.WordRAM.Exec.executes {B : Basis} {r w : ℕ} {x : Data r} {c : Code B r} {y : Data r} {n : ℕ} (h : Exec w c x y n) (out : Fin r) : Executes w (c.program out) { pc := 0, data := x } (y.regs out) (n + 1)

A structured execution followed by halt out is a halting run of the complete program, with one more instruction.

Answering questions with structured programs

def Cslib.WordRAM.Code.Answers {B : Basis} {r : ℕ} (c : Code B r) (out : Fin r) (w : ℕ) (input : List ℕ) (b : Prop) (time : ℕ) : Prop

The structured program c, run at word size w from the initial data on input, leaves the answer to b in register out within time instructions: 1 if b holds and 0 otherwise.

theorem Cslib.WordRAM.Code.Answers.program {B : Basis} {r : ℕ} {c : Code B r} {out : Fin r} {w : ℕ} {input : List ℕ} {b : Prop} {time : ℕ} (h : c.Answers out w input b time) : (c.program out).Answers w input b (time + 1)

A structured program that answers a question gives a flat program that answers it, with one more instruction for the final halt.

theorem Cslib.WordRAM.Code.decidesInTime_program {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (c : Code B r) (out : Fin r) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → c.Answers out w (encode w a) (a ∈ A) (time a w)) : (c.program out).DecidesInTime encode A (fun (a : α) (w : ℕ) => time a w + 1) allowed

Structured answers give a fixed-program decision certificate, charging the final halt.

theorem Cslib.WordRAM.UniformDecidableInTime.of_code {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (c : Code B r) (out : Fin r) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → c.Answers out w (encode w a) (a ∈ A) (time a w)) : UniformDecidableInTime B A encode (fun (a : α) (w : ℕ) => time a w + 1) allowed

Structured decision procedures are uniform deciders.

theorem Cslib.WordRAM.DecidableInTime.of_code {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (c : ℕ → Code B r) (out : Fin r) (hc : ∃ (L : ℕ), ∀ (w : ℕ), (c w).size ≤ L) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → (c w).Answers out w (encode w a) (a ∈ A) (time a w)) : DecidableInTime B A encode (fun (a : α) (w : ℕ) => time a w + 1) allowed

Structured families with bounded compiled code give nonuniform deciders.

Reading the word size

theorem Cslib.WordRAM.Code.readsWidth_of_assemble {B : Basis} {r : ℕ} {c : Code B r} {pc : ℕ} (h : (c.assemble pc).ReadsWidth) : c.ReadsWidth

An assembled program reads the word size only if the structured program does.

theorem Cslib.WordRAM.Code.not_readsWidth_program {B : Basis} {r : ℕ} {c : Code B r} (hc : ¬c.ReadsWidth) (out : Fin r) : ¬(c.program out).ReadsWidth

A compiled program reads the word size only if the structured program does.