Straight-line blocks of assignments

assignsCode b r k e assigns the value of e i to register r + i for each i < k, one instruction each, starting at label b. When no expression reads a register being assigned, the block writes every value as evaluated before the block, whatever the order of the assignments.

Main definitions

• Turing.CounterProgram.assignsCode: the block of assignments.

Main results

• Turing.CounterProgram.reaches_assignsCode: running the block.

def Turing.CounterProgram.assignsCode (b r k : ℕ) (e : ℕ → Expr) : List Instr

Straight-line assignments of e i to register r + i for i < k, placed at label b.

@[simp]

theorem Turing.CounterProgram.length_assignsCode (b r k : ℕ) (e : ℕ → Expr) : (assignsCode b r k e).length = k

theorem Turing.CounterProgram.reaches_assignsCode {P : CounterProgram} {w : List Bool} {B b r : ℕ} {e : ℕ → Expr} {k : ℕ} : P.CodeAt b (assignsCode b r k e) → ∀ {regs : List ℕ}, r + k ≤ regs.length → (∀ i < k, ∀ (regs' : List ℕ), (∀ (j : ℕ), j < r ∨ r + k ≤ j → regs'.getD j 0 = regs.getD j 0) → Expr.eval regs' (e i) = Expr.eval regs (e i)) → (∀ x ∈ regs, x ≤ B) → (∀ i < k, Expr.eval regs (e i) ≤ B) → ∃ (regs' : List ℕ), P.Reaches w (P.Running B) (b, regs) (b + k, regs') ∧ regs'.length = regs.length ∧ (∀ (j : ℕ), j < r ∨ r + k ≤ j → regs'.getD j 0 = regs.getD j 0) ∧ (∀ i < k, regs'.getD (r + i) 0 = Expr.eval regs (e i)) ∧ ∀ x ∈ regs', x ≤ B

Running a block of assignments, when no expression reads a register being assigned.