Shifting counter programs above a choice register

A nondeterministic counter program reads its choice bit in register 0. Deterministic code written for registers 0, 1, … runs unchanged inside such a program once each register i is renamed to i + 1. Expr.shift and Instr.shift perform this renaming, keeping labels. padded b code places code at label b of a standalone program, so that existing deterministic correctness lemmas apply to it, and Reaches.unpad transfers their runs to the shifted copy placed at the same label of another program, as oblivious runs that never read the choice.

Main definitions

• Turing.CounterProgram.Expr.shift, Turing.CounterProgram.Instr.shift: register renaming.
• Turing.CounterProgram.padded: code placed at a label after halting padding.

Main results

• Turing.CounterProgram.Reaches.shift: deterministic runs lift to shifted code.
• Turing.CounterProgram.Reaches.unpad: runs of padded code lift to its shifted placement.

def Turing.CounterProgram.Expr.shift : Expr → Expr

Rename every register i to i + 1.

@[simp]

theorem Turing.CounterProgram.Expr.eval_shift (e : Expr) (c : ℕ) (regs : List ℕ) : eval (c :: regs) e.shift = eval regs e

@[simp]

theorem Turing.CounterProgram.Expr.readsChoice_shift (e : Expr) : e.shift.readsChoice = false

def Turing.CounterProgram.Instr.shift : Instr → Instr

Rename every register i to i + 1, keeping the labels.

@[simp]

theorem Turing.CounterProgram.Instr.readsChoice_shift (i : Instr) : i.shift.readsChoice = false

theorem Turing.CounterProgram.Instr.isStep_shift {i : Instr} (h : i.IsStep) : i.shift.IsStep

theorem Turing.CounterProgram.Instr.exec_shift (i : Instr) (l c : ℕ) (regs : List ℕ) (b : Option Bool) : i.shift.exec (l, c :: regs) b = ((i.exec (l, regs) b).1, c :: (i.exec (l, regs) b).2)

theorem Turing.CounterProgram.Instr.query_shift (i : Instr) (c : ℕ) (regs : List ℕ) : i.shift.query (c :: regs) = i.query regs

theorem Turing.CounterProgram.Instr.halts_shift (i : Instr) : i.shift.halts = i.halts

theorem Turing.CounterProgram.step_shift {P Q : CounterProgram} {w : List Bool} {l : ℕ} {regs : List ℕ} (c : ℕ) (h : Q.instr l = (P.instr l).shift) : Q.step w (l, c :: regs) = ((P.step w (l, regs)).1, c :: (P.step w (l, regs)).2)

A step of shifted code is the step of the original code, below a register c.

theorem Turing.CounterProgram.Reaches.shift {P Q : CounterProgram} {w : List Bool} {B c : ℕ} {s s' : Config} (hcB : c ≤ B) (hQ : ∀ (l : ℕ), (P.instr l).IsStep → Q.instr l = (P.instr l).shift) (h : P.Reaches w (P.Running B) s s') : Q.Reaches w (Q.Oblivious B) (s.1, c :: s.2) (s'.1, c :: s'.2)

Deterministic runs of code lift to its shift, below a register c at most B.

def Turing.CounterProgram.padded (b : ℕ) (l : List Instr) : CounterProgram

A list of instructions placed at the label b, after halts.

theorem Turing.CounterProgram.codeAt_padded (b : ℕ) (l : List Instr) : (padded b l).CodeAt b l

theorem Turing.CounterProgram.padded_instr_of_isStep {Q : CounterProgram} {b : ℕ} {l : List Instr} (hQ : Q.CodeAt b (List.map Instr.shift l)) {i : ℕ} (hi : ((padded b l).instr i).IsStep) : Q.instr i = ((padded b l).instr i).shift

theorem Turing.CounterProgram.Reaches.unpad {Q : CounterProgram} {w : List Bool} {B c b : ℕ} {l : List Instr} {s s' : Config} (hcB : c ≤ B) (hQ : Q.CodeAt b (List.map Instr.shift l)) (h : (padded b l).Reaches w ((padded b l).Running B) s s') : Q.Reaches w (Q.Oblivious B) (s.1, c :: s.2) (s'.1, c :: s'.2)

Unpadding: a deterministic run of code placed by padded is an oblivious run of its shift placed in another program.