Standard Form Programs

This file defines standard-form programs (those with bounded jump targets) and proves their execution properties.

Main definitions

• Program.IsStandardForm: all jump targets are bounded by program length
• Program.toStandardForm: convert a program to standard form

Main results

• straight_line_IsStandardForm: straight-line programs are standard form
• Halts.toStandardForm_iff: halting equivalence with normalized programs

Standard Form Definitions

def Cslib.URM.Program.IsStandardForm (p : Program) : Prop

A program is in standard form if all jump targets are bounded by the program length. Jumps can target any instruction (0..length-1) or the "virtual halt" position (length).

Equations

• p.IsStandardForm = ∀ instr ∈ p, Cslib.URM.Instr.JumpsBoundedBy (List.length p) instr

instance Cslib.URM.Program.instDecidableIsStandardForm (p : Program) : Decidable p.IsStandardForm

Equations

• p.instDecidableIsStandardForm = inferInstanceAs (Decidable (∀ instr ∈ p, Cslib.URM.Instr.JumpsBoundedBy (List.length p) instr))

def Cslib.URM.Program.toStandardForm (p : Program) : Program

Convert a program to standard form by capping all jump targets at the program length.

Equations

• p.toStandardForm = List.map (Cslib.URM.Instr.capJump (List.length p)) p

@[simp]

theorem Cslib.URM.Program.toStandardForm_length (p : Program) : List.length p.toStandardForm = List.length p

toStandardForm preserves program length.

theorem Cslib.URM.Program.toStandardForm_isStandardForm (p : Program) : p.toStandardForm.IsStandardForm

toStandardForm produces a standard form program.

theorem Cslib.URM.Program.getElem?_toStandardForm (p : Program) (i : ℕ) : p.toStandardForm[i]? = Option.map (Instr.capJump (List.length p)) p[i]?

Accessing an instruction in toStandardForm gives the capJump'd instruction.

@[simp]

theorem Cslib.URM.Program.toStandardForm_idempotent (p : Program) : p.toStandardForm.toStandardForm = p.toStandardForm

toStandardForm is idempotent: applying it twice equals applying it once.

Standard Form Properties

theorem Cslib.URM.straight_line_IsStandardForm {p : Program} (hsl : p.IsStraightLine) : p.IsStandardForm

Straight-line programs are in standard form.

Bisimulation

p and p.toStandardForm are bisimilar: each step in one program corresponds to a step in the other that either reaches the same state or reaches a halted state with the same registers. This bisimulation implies functional equivalence (eval_toStandardForm). The key insight is that jumps with target q > p.length land in halted states in both programs.

theorem Cslib.URM.Step.toStandardForm {p : Program} {s s' : State} (hstep : Step p s s') : Step p.toStandardForm s s' ∨ s'.isHalted p ∧ ∃ (s₂ : State), Step p.toStandardForm s s₂ ∧ s₂.isHalted p.toStandardForm ∧ s'.regs = s₂.regs

Forward step correspondence: if p steps from s to s', then either: (1) p.toStandardForm steps from s to s' (same step), or (2) s' is halted in p, and p.toStandardForm steps to a state that is also halted with the same registers (this only happens for jumps with unbounded targets).

theorem Cslib.URM.Steps.toStandardForm_halts {p : Program} {s s' : State} (hsteps : Steps p s s') (hhalted : s'.isHalted p) : ∃ (s₂ : State), Steps p.toStandardForm s s₂ ∧ s₂.isHalted p.toStandardForm ∧ s'.regs = s₂.regs

Forward halting: if p reaches a halted state, p.toStandardForm reaches a halted state with the same registers.

theorem Cslib.URM.Halts.toStandardForm {p : Program} {inputs : List ℕ} (h : Halts p inputs) : Halts p.toStandardForm inputs

Forward halting theorem.

theorem Cslib.URM.Step.from_toStandardForm {p : Program} {s s' : State} (hstep : Step p.toStandardForm s s') : Step p s s' ∨ s'.isHalted p.toStandardForm ∧ ∃ (s₂ : State), Step p s s₂ ∧ s₂.isHalted p ∧ s'.regs = s₂.regs

Reverse step correspondence: if p.toStandardForm steps from s to s', then either: (1) p steps from s to s' (same step), or (2) s' is halted in p.toStandardForm, and p steps to a state that is also halted with the same registers (this only happens for jumps with unbounded targets).

theorem Cslib.URM.Steps.from_toStandardForm_halts {p : Program} {s s' : State} (hsteps : Steps p.toStandardForm s s') (hhalted : s'.isHalted p.toStandardForm) : ∃ (s₂ : State), Steps p s s₂ ∧ s₂.isHalted p ∧ s'.regs = s₂.regs

Reverse halting: if p.toStandardForm reaches a halted state, p reaches a halted state with the same registers.

theorem Cslib.URM.Halts.of_toStandardForm {p : Program} {inputs : List ℕ} (h : Halts p.toStandardForm inputs) : Halts p inputs

Reverse halting theorem.

theorem Cslib.URM.Halts.toStandardForm_iff {p : Program} {inputs : List ℕ} : Halts p inputs ↔ Halts p.toStandardForm inputs

Halting equivalence: original halts iff standard form halts.

eval Preservation

theorem Cslib.URM.evalState_toStandardForm_regs {p : Program} {inputs : List ℕ} (hp : (evalState p inputs).Dom) (hq : (evalState p.toStandardForm inputs).Dom) : ((evalState p inputs).get hp).regs = ((evalState p.toStandardForm inputs).get hq).regs

Registers preservation: both reach states with the same registers.

theorem Cslib.URM.eval_toStandardForm {p : Program} {inputs : List ℕ} : eval p inputs = eval p.toStandardForm inputs

eval equality: both programs produce the same partial result.

theorem Cslib.URM.toStandardForm_equiv (p : Program) : p.toStandardForm ≈ p

A program is equivalent to its standard form.