Stepping through counter programs

The tactic cp_step takes one step of a counter program in a goal P.Reaches w Q (l, regs) s' (Turing.CounterProgram.Reaches). It applies the stepping rule of the instruction at l, proves the side conditions of the rule, and simplifies the configuration the step reaches, so that a straight-line part of a reachability proof is a sequence of cp_step calls instead of a refine Reaches.assign h hB ?_ and a simp only [eval_add, …] per instruction.

The rules are those of running configurations (Turing.CounterProgram.Reaches.assign, .lt, .read), of oblivious configurations (.oassign, .olt, .oread) and of shifted instructions (.sassign, .slt). A rule is tried only when the module proving it is imported, so this module imports neither CounterProgram.AllBranches nor CounterProgram.Block.

Main definitions

• cp_step, cp_step [h₁, h₂]: take one step, simplifying with the simp set cp_simps and the given lemmas, and deciding conditional labels by a hypothesis or omega.

def Turing.CounterProgram.StepTactic.cpStep : Lean.ParserDescr

cp_step takes one step of a counter program in a goal P.Reaches w Q (l, regs) s'. It applies the stepping rule of the instruction at l, given by a hypothesis P.instr l = i or by evaluation of P.instr l, then simplifies the configuration after the step and closes the goal by Reaches.refl or by a hypothesis when it can. The simplification uses the simp set cp_simps (expressions, reads of written-out register lists), numeral +, -, * and <, and the decided conditionals.

• cp_step [h₁, h₂] adds simp lemmas, typically the values of the registers read (regs.getD 0 0 = n) and the input bit read (w[k]? = some true), or simprocs such as Nat.reduceDiv. A fact about expressions that cp_simps evaluates, such as (const 0).eval regs < e.eval regs ↔ p, is passed as ↓h, to apply before they are evaluated.

A conditional label if c then l₁ else l₂ is decided when c or ¬c is a hypothesis or, for a comparison of natural numbers or integers, follows by omega: that of the configuration before the step, and after the step that of either configuration when the label of the other is l₁ or l₂. The goal is then closed when it can be; otherwise it is left with that label decided.

The side conditions of the rule must be proved automatically: a bound ∀ r ∈ regs, r ≤ B on the registers by a hypothesis, or entry by entry for regs'.set i x (from a bound on regs') and for a list written out, with the bounds on the entries by a hypothesis or omega; c ≤ B and i ≠ 0 by a hypothesis, decide or omega; and e.readsChoice = false by evaluation. Otherwise cp_step fails and names the rule and the condition. The rules are those of running configurations (Reaches.assign, Reaches.lt, Reaches.read), and, when their modules are imported, of oblivious configurations (Reaches.oassign, Reaches.olt, Reaches.oread) and of shifted instructions (Reaches.sassign, Reaches.slt). A label left undecided, or as a match on the bit read, stops cp_step with a diagnostic: split into cases first.