Straight-Line Programs

This file defines straight-line programs (those without jumps) and proves they always halt exactly at their length.

Main definitions

• Program.IsStraightLine: a program contains no jump instructions

Main results

• straight_line_halts: straight-line programs always halt
• straightLine_finalState: final state after running a straight-line program

Straight-Line Programs

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

A program is "straight-line" if it contains no jump instructions.

Equations

• p.IsStraightLine = ∀ i ∈ p, ¬i.IsJump

instance Cslib.URM.instDecidableIsStraightLine (p : Program) : Decidable p.IsStraightLine

Equations

• Cslib.URM.instDecidableIsStraightLine p = inferInstanceAs (Decidable (∀ i ∈ p, ¬i.IsJump))

theorem Cslib.URM.Program.IsStraightLine.append {p q : Program} (hp : p.IsStraightLine) (hq : q.IsStraightLine) : (p ++ q).IsStraightLine

Append preserves straight-line property.

theorem Cslib.URM.Program.IsStraightLine.cons {instr : Instr} {p : Program} (hinstr : ¬instr.IsJump) (hp : p.IsStraightLine) : IsStraightLine (instr :: p)

Cons of non-jumping instruction preserves straight-line.

theorem Cslib.URM.Program.IsStraightLine.singleton {instr : Instr} (h : ¬instr.IsJump) : IsStraightLine [instr]

Singleton non-jumping instruction is straight-line.

Straight-Line Program Execution

theorem Cslib.URM.Step.of_nonJump {p : Program} {s : State} (hlt : s.pc < List.length p) (hnonjump : ¬p[s.pc].IsJump) : ∃ (s' : State), Step p s s' ∧ s'.pc = s.pc + 1

A non-jumping instruction produces a step that increments PC by 1.

theorem Cslib.URM.straight_line_halts_from_regs {p : Program} (hsl : p.IsStraightLine) (r : Regs) : ∃ (s : State), Steps p { pc := 0, regs := r } s ∧ s.isHalted p ∧ s.pc = List.length p

Straight-line programs halt from any starting registers, not just State.init. Useful for chaining: after running one program, we can run the next straight-line segment from whatever registers we're in.

theorem Cslib.URM.straight_line_halts {p : Program} (hsl : p.IsStraightLine) (inputs : List ℕ) : Halts p inputs

A straight-line program halts on any input.

noncomputable def Cslib.URM.straightLine_finalState {p : Program} (hsl : p.IsStraightLine) (r : Regs) : State

The halting state for a straight-line program starting from registers r. Wraps Classical.choose to hide it from the API.

Equations

• Cslib.URM.straightLine_finalState hsl r = Classical.choose ⋯

theorem Cslib.URM.straightLine_finalState_spec {p : Program} (hsl : p.IsStraightLine) (r : Regs) : have s := straightLine_finalState hsl r; Steps p { pc := 0, regs := r } s ∧ s.isHalted p ∧ s.pc = List.length p

Specification: the state from straightLine_finalState satisfies Steps, isHalted, and has pc = p.length.

noncomputable def Cslib.URM.straightLine_finalRegs {p : Program} (hsl : p.IsStraightLine) (r : Regs) : Regs

The final registers after running a straight-line program from given starting registers.

Equations

• Cslib.URM.straightLine_finalRegs hsl r = (Cslib.URM.straightLine_finalState hsl r).regs

theorem Cslib.URM.straightLine_finalRegs_eq_of_halted {p : Program} (hsl : p.IsStraightLine) (r : Regs) (s : State) (hsteps : Steps p { pc := 0, regs := r } s) (hhalted : s.isHalted p) : s.regs = straightLine_finalRegs hsl r

For a straight-line program, s.regs equals straightLine_finalRegs if halted from r.

theorem Cslib.URM.straight_line_state_at_pc {p : Program} (hsl : p.IsStraightLine) (r : Regs) (targetPc : ℕ) (htarget : targetPc ≤ List.length p) : ∃ (s : State), Steps p { pc := 0, regs := r } s ∧ s.pc = targetPc

In a straight-line program, we can characterize the state at any intermediate pc. This gives us the state after executing instructions 0..pc-1.